[move specs] Add first-class quantifiers to Move AST (not yet produce…

…d by parser)

language/move-lang/src/expansion/ast.rs

@@ -3,7 +3,7 @@
 
 use crate::{
     parser::ast::{
-        BinOp, ConstantName, Field, FunctionName, FunctionVisibility, Kind, ModuleIdent,
+        BinOp, ConstantName, Field, FunctionName, FunctionVisibility, Kind, ModuleIdent, QuantKind,
         ResourceLoc, SpecApplyPattern, SpecBlockTarget, SpecConditionKind, StructName, UnaryOp,
         Var,
     },
@@ -215,6 +215,11 @@ pub type LValue = Spanned<LValue_>;
 pub type LValueList_ = Vec<LValue>;
 pub type LValueList = Spanned<LValueList_>;
 
+pub type LValueWithRange_ = (LValue, Exp);
+pub type LValueWithRange = Spanned<LValueWithRange_>;
+pub type LValueWithRangeList_ = Vec<LValueWithRange>;
+pub type LValueWithRangeList = Spanned<LValueWithRangeList_>;
+
 #[derive(Debug, Clone, PartialEq)]
 #[allow(clippy::large_enum_variant)]
 pub enum ExpDotted_ {
@@ -256,7 +261,8 @@ pub enum Exp_ {
     While(Box<Exp>, Box<Exp>),
     Loop(Box<Exp>),
     Block(Sequence),
-    Lambda(LValueList, Box<Exp>), // spec only
+    Lambda(LValueList, Box<Exp>),                    // spec only
+    Quant(QuantKind, LValueWithRangeList, Box<Exp>), // spec only
 
     Assign(LValueList, Box<Exp>),
     FieldMutate(Box<ExpDotted>, Box<Exp>),
@@ -806,6 +812,13 @@ impl AstDebug for Exp_ {
                 w.write(" ");
                 e.ast_debug(w);
             }
+            E::Quant(kind, sp!(_, rs), e) => {
+                kind.ast_debug(w);
+                w.write(" ");
+                rs.ast_debug(w);
+                w.write(": ");
+                e.ast_debug(w);
+            }
             E::ExpList(es) => {
                 w.write("(");
                 w.comma(es, |w, e| e.ast_debug(w));
@@ -952,3 +965,24 @@ impl AstDebug for LValue_ {
         }
     }
 }
+
+impl AstDebug for Vec<LValueWithRange> {
+    fn ast_debug(&self, w: &mut AstWriter) {
+        let parens = self.len() != 1;
+        if parens {
+            w.write("(");
+        }
+        w.comma(self, |w, b| b.ast_debug(w));
+        if parens {
+            w.write(")");
+        }
+    }
+}
+
+impl AstDebug for (LValue, Exp) {
+    fn ast_debug(&self, w: &mut AstWriter) {
+        self.0.ast_debug(w);
+        w.write(" in ");
+        self.1.ast_debug(w);
+    }
+}

language/move-lang/src/expansion/translate.rs

@@ -1190,6 +1190,22 @@ fn exp_(context: &mut Context, sp!(loc, pe_): P::Exp) -> E::Exp {
                 }
             }
         }
+        PE::Quant(k, prs, pe) => {
+            if !context.require_spec_context(loc, "expression only allowed in specifications") {
+                assert!(context.has_errors());
+                EE::UnresolvedError
+            } else {
+                let rs_opt = bind_with_range_list(context, prs);
+                let e = exp_(context, *pe);
+                match rs_opt {
+                    Some(rs) => EE::Quant(k, rs, Box::new(e)),
+                    None => {
+                        assert!(context.has_errors());
+                        EE::UnresolvedError
+                    }
+                }
+            }
+        }
         PE::ExpList(pes) => {
             assert!(pes.len() > 1);
             EE::ExpList(exps(context, pes))
@@ -1340,6 +1356,21 @@ fn bind_list(context: &mut Context, sp!(loc, pbs_): P::BindList) -> Option<E::LV
     Some(sp(loc, bs_?))
 }
 
+fn bind_with_range_list(
+    context: &mut Context,
+    sp!(loc, prs_): P::BindWithRangeList,
+) -> Option<E::LValueWithRangeList> {
+    let rs_: Option<Vec<E::LValueWithRange>> = prs_
+        .into_iter()
+        .map(|sp!(loc, (pb, pr))| -> Option<E::LValueWithRange> {
+            let b = bind(context, pb)?;
+            let r = exp_(context, pr);
+            Some(sp(loc, (b, r)))
+        })
+        .collect();
+    Some(sp(loc, rs_?))
+}
+
 fn bind(context: &mut Context, sp!(loc, pb_): P::Bind) -> Option<E::LValue> {
     use E::LValue_ as EL;
     use P::Bind_ as PB;
@@ -1516,6 +1547,11 @@ fn unbound_names_exp(unbound: &mut BTreeSet<Name>, sp!(_, e_): &E::Exp) {
             // remove anything in `ls`
             unbound_names_binds(unbound, ls);
         }
+        EE::Quant(_, rs, er) => {
+            unbound_names_exp(unbound, er);
+            // remove anything in `rs`
+            unbound_names_binds_with_range(unbound, rs);
+        }
         EE::Assign(ls, er) => {
             unbound_names_exp(unbound, er);
             // remove anything in `ls`
@@ -1576,6 +1612,16 @@ fn unbound_names_binds(unbound: &mut BTreeSet<Name>, sp!(_, ls_): &E::LValueList
         .for_each(|l| unbound_names_bind(unbound, l))
 }
 
+fn unbound_names_binds_with_range(
+    unbound: &mut BTreeSet<Name>,
+    sp!(_, rs_): &E::LValueWithRangeList,
+) {
+    rs_.iter().rev().for_each(|sp!(_, (b, r))| {
+        unbound_names_exp(unbound, r);
+        unbound_names_bind(unbound, b)
+    })
+}
+
 fn unbound_names_bind(unbound: &mut BTreeSet<Name>, sp!(_, l_): &E::LValue) {
     use E::LValue_ as EL;
     match l_ {

language/move-lang/src/naming/translate.rs

@@ -908,7 +908,7 @@ fn exp_(context: &mut Context, e: E::Exp) -> N::Exp {
             NE::UnresolvedError
         }
         // `Name` matches name variants only allowed in specs (we handle the allowed ones above)
-        EE::Index(..) | EE::Lambda(..) | EE::Name(_, Some(_)) => {
+        EE::Index(..) | EE::Lambda(..) | EE::Quant(..) | EE::Name(_, Some(_)) => {
             panic!("ICE unexpected specification construct")
         }
     };

language/move-lang/src/parser/ast.rs

@@ -380,6 +380,9 @@ pub type Bind = Spanned<Bind_>;
 // b1, ..., bn
 pub type BindList = Spanned<Vec<Bind>>;
 
+pub type BindWithRange = Spanned<(Bind, Exp)>;
+pub type BindWithRangeList = Spanned<Vec<BindWithRange>>;
+
 #[derive(Debug, Clone, PartialEq)]
 pub enum Value_ {
     // 0x<hex representation up to 64 digits with padding 0s>
@@ -457,6 +460,13 @@ pub enum BinOp_ {
 }
 pub type BinOp = Spanned<BinOp_>;
 
+#[derive(Debug, PartialEq, Copy, Clone)]
+pub enum QuantKind_ {
+    Forall,
+    Exists,
+}
+pub type QuantKind = Spanned<QuantKind_>;
+
 #[derive(Debug, Clone, PartialEq)]
 #[allow(clippy::large_enum_variant)]
 pub enum Exp_ {
@@ -487,6 +497,8 @@ pub enum Exp_ {
     Block(Sequence),
     // fun (x1, ..., xn) e
     Lambda(BindList, Box<Exp>), // spec only
+    // forall/exists x1 : e1, ..., xn : en.
+    Quant(QuantKind, BindWithRangeList, Box<Exp>), // spec only
     // (e1, ..., en)
     ExpList(Vec<Exp>),
     // ()
@@ -1336,6 +1348,13 @@ impl AstDebug for Exp_ {
                 w.write(" ");
                 e.ast_debug(w);
             }
+            E::Quant(kind, sp!(_, rs), e) => {
+                kind.ast_debug(w);
+                w.write(" ");
+                rs.ast_debug(w);
+                w.write(" ");
+                e.ast_debug(w);
+            }
             E::ExpList(es) => {
                 w.write("(");
                 w.comma(es, |w, e| e.ast_debug(w));
@@ -1428,6 +1447,36 @@ impl AstDebug for UnaryOp_ {
     }
 }
 
+impl AstDebug for QuantKind_ {
+    fn ast_debug(&self, w: &mut AstWriter) {
+        match self {
+            QuantKind_::Forall => w.write("forall"),
+            QuantKind_::Exists => w.write("exists"),
+        }
+    }
+}
+
+impl AstDebug for Vec<BindWithRange> {
+    fn ast_debug(&self, w: &mut AstWriter) {
+        let parens = self.len() != 1;
+        if parens {
+            w.write("(");
+        }
+        w.comma(self, |w, b| b.ast_debug(w));
+        if parens {
+            w.write(")");
+        }
+    }
+}
+
+impl AstDebug for (Bind, Exp) {
+    fn ast_debug(&self, w: &mut AstWriter) {
+        self.0.ast_debug(w);
+        w.write(" in ");
+        self.1.ast_debug(w);
+    }
+}
+
 impl AstDebug for Value_ {
     fn ast_debug(&self, w: &mut AstWriter) {
         use Value_ as V;