[move-prover] allow ExpTranslator to recognize generics in expressions

The `ExpTranslator` now accepts two forms of generics:

- `type_params / type_params_table` represent the generic types in the
  enclosing function when translating this expression. For example, if
  the expression is associated with a `fun foo<T>()`, then `T` is
  captured as a `Type::TypeParameter` in the `type_params` store.

- `type_locals / type_locals_table` represent the generic types in the
  expression itself. For example, the expression is a generic invariant
  `invariant<t> is_operating() => exists<S<t>>(0x1)`, then the `t` is
  captured as a `Type::TypeLocal` in the `type_locals` store.

The reason we need to separate them is that the genericity come from
different sources. We use `TypeParameter` to track that the genericity
is introduced in the Move code, and re-purpose `TypeLocal` to indicate
that the genericity is introduced by the Spec code.

Besides signaling different origins, it seems necessary (or rather,
makes our lives much easier) to assign different `Type`s for generic
types coming from different sources.

Consider the following example:

```
fun foo<T>() {
    borrow_global_mut<S<T>>(@0x1, ...);
}

spec {
    invariant<T> exists<S<T>>(0x1) ==> ...;
}
```

The `T` in `foo<T>` and `invariant<T>` are essentially two different
things although they share the same symbol and positional index in the
genericity type list.

language/move-model/src/ast.rs

@@ -648,7 +648,8 @@ impl ExpData {
                 t.visit_pre_post(visitor);
                 e.visit_pre_post(visitor);
             }
-            _ => {}
+            // Explicitly list all enum variants
+            Value(..) | LocalVar(..) | Temporary(..) | SpecVar(..) | Invalid(..) => {}
         }
         visitor(true, self);
     }

language/move-model/src/builder/exp_translator.rs

@@ -33,6 +33,10 @@ pub(crate) struct ExpTranslator<'env, 'translator, 'module_translator> {
     pub type_params_table: BTreeMap<Symbol, Type>,
     /// Type parameters in sequence they have been added.
     pub type_params: Vec<(Symbol, Type)>,
+    /// A symbol table for type locals.
+    pub type_locals_table: BTreeMap<Symbol, Type>,
+    /// Type locals for this exp translation context in the order they are added
+    pub type_locals: Vec<Type>,
     /// A scoped symbol table for local names. The first element in the list contains the most
     /// inner scope.
     pub local_table: LinkedList<BTreeMap<Symbol, LocalVarEntry>>,
@@ -77,6 +81,8 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
             parent,
             type_params_table: BTreeMap::new(),
             type_params: vec![],
+            type_locals_table: BTreeMap::new(),
+            type_locals: vec![],
             local_table: LinkedList::new(),
             result_type: None,
             old_status: OldExpStatus::NotSupported,
@@ -329,12 +335,90 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
 
     /// Defines a type parameter.
     pub fn define_type_param(&mut self, loc: &Loc, name: Symbol, ty: Type) {
-        self.type_params.push((name, ty.clone()));
-        if self.type_params_table.insert(name, ty).is_some() {
+        if let Type::TypeParameter(..) = &ty {
+            if self.type_locals_table.contains_key(&name) {
+                let param_name = name.display(self.symbol_pool());
+                self.parent.parent.error(
+                    loc,
+                    &format!(
+                        "duplicate declaration of type parameter `{}`, \
+                        previously found in type locals",
+                        param_name
+                    ),
+                );
+                return;
+            }
+            if self.type_params_table.insert(name, ty.clone()).is_some() {
+                let param_name = name.display(self.symbol_pool());
+                self.parent.parent.error(
+                    loc,
+                    &format!(
+                        "duplicate declaration of type parameter `{}`, \
+                        previously found in type parameters",
+                        param_name
+                    ),
+                );
+                return;
+            }
+            self.type_params.push((name, ty));
+        } else {
             let param_name = name.display(self.symbol_pool());
-            self.parent
-                .parent
-                .error(loc, &format!("duplicate declaration of `{}`", param_name));
+            let context = TypeDisplayContext::WithEnv {
+                env: self.parent.parent.env,
+                type_param_names: None,
+            };
+            self.parent.parent.error(
+                loc,
+                &format!(
+                    "expect type placeholder `{}` to be a `TypeParameter`, found `{}`",
+                    param_name,
+                    ty.display(&context)
+                ),
+            );
+        }
+    }
+
+    /// Defines a type local.
+    pub fn define_type_local(&mut self, loc: &Loc, ty: Type) {
+        if let Type::TypeLocal(name) = &ty {
+            let name = *name;
+            if self.type_params_table.contains_key(&name) {
+                let local_name = name.display(self.symbol_pool());
+                self.parent.parent.error(
+                    loc,
+                    &format!(
+                        "duplicate declaration of type local `{}`, \
+                        previously found in type parameters",
+                        local_name
+                    ),
+                );
+                return;
+            }
+            if self.type_locals_table.insert(name, ty.clone()).is_some() {
+                let local_name = name.display(self.symbol_pool());
+                self.parent.parent.error(
+                    loc,
+                    &format!(
+                        "duplicated declaration of type local `{}`, \
+                        previously found in type locals",
+                        local_name
+                    ),
+                );
+                return;
+            }
+            self.type_locals.push(ty);
+        } else {
+            let context = TypeDisplayContext::WithEnv {
+                env: self.parent.parent.env,
+                type_param_names: None,
+            };
+            self.parent.parent.error(
+                loc,
+                &format!(
+                    "expect type generics declared in an invariant to be a `TypeLocal`, found `{}`",
+                    ty.display(&context)
+                ),
+            );
         }
     }
 
@@ -623,7 +707,13 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo
                     if let Some(ty) = self.type_params_table.get(&sym).cloned() {
                         return check_zero_args(self, ty);
                     }
+                    // Attempt to resolve as a type local
+                    if let Some(ty) = self.type_locals_table.get(&sym).cloned() {
+                        return check_zero_args(self, ty);
+                    }
+
                     // Attempt to resolve as a type value.
+                    // TODO(mengxu): remove this logic once porting to generic invariant is done
                     if let Some(entry) = self.lookup_local(sym, false) {
                         let ty = entry.type_.clone();
                         self.check_type(

language/move-model/src/builder/module_builder.rs

@@ -1251,7 +1251,22 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
 
                 et
             }
-            Module => ExpTranslator::new_with_old(self, allows_old),
+            Module => {
+                let mut et = ExpTranslator::new_with_old(self, allows_old);
+
+                // define the type locals
+                match kind {
+                    ConditionKind::GlobalInvariant(tys)
+                    | ConditionKind::GlobalInvariantUpdate(tys) => {
+                        for ty in tys {
+                            et.define_type_local(loc, ty.clone());
+                        }
+                    }
+                    _ => (),
+                }
+
+                et
+            }
             Schema(name) => {
                 let entry = self
                     .parent
@@ -1267,6 +1282,13 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
                     et.define_type_param(loc, n, ty);
                 }
 
+                // define the type locals
+                if let ConditionKind::SchemaInvariant(tys) = kind {
+                    for ty in tys {
+                        et.define_type_local(loc, ty.clone());
+                    }
+                }
+
                 et.enter_scope();
                 for (n, entry) in all_vars {
                     et.define_local(loc, n, entry.type_, None, None);