name field of AIR's DeclaredX::Fun

verus-lang · Oct 27, 2024 · da2e55a · da2e55a
1 parent d8a87ad
commit da2e55a
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 11 deletions.
diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs
@@ -76,7 +76,7 @@ pub(crate) struct ClosureTermX {
 // The function declarations live in scope outside the expression scope, so
 // we need to insert them into the typing's outer scope:
 fn insert_fun_typing(ctxt: &mut Context, x: &Ident, typs: &Typs, typ: &Typ) {
-    let fun = DeclaredX::Fun(typs.clone(), typ.clone(), false);
+    let fun = DeclaredX::Fun { params: typs.clone(), ret: typ.clone(), field_accessor: false };
 
     // the maps that aren't ctxt.typing.decls (e.g. apply_map) are still in the outer scope,
     // so use one of them as the outer scope index:
@@ -521,7 +521,7 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex
         }
         ExprX::Apply(x, args) => {
             let typ = match ctxt.typing.get(x) {
-                Some(DeclaredX::Fun(_, typ, _)) => typ.clone(),
+                Some(DeclaredX::Fun { params: _, ret, field_accessor: _ }) => ret.clone(),
                 _ => panic!("internal error: missing function {}", x),
             };
             let (es, ts) = simplify_exprs(ctxt, state, &**args);

diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs
@@ -18,7 +18,7 @@ pub(crate) type Declared = Arc<DeclaredX>;
 pub(crate) enum DeclaredX {
     Type,
     Var { typ: Typ, mutable: bool },
-    Fun(Typs, Typ, bool), //args, ret, accessor
+    Fun { params: Typs, ret: Typ, field_accessor: bool }, //args, ret, accessor
 }
 
 pub struct Typing {
@@ -214,7 +214,9 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result<Typ, TypeError> {
             (true, _) => Err(format!("use of undeclared variable {}", x)),
         },
         ExprX::Apply(x, es) => match typing.get(x).cloned() {
-            Some(DeclaredX::Fun(f_typs, f_typ, _)) => check_exprs(typing, x, &f_typs, &f_typ, es),
+            Some(DeclaredX::Fun { params, ret, field_accessor: _ }) => {
+                check_exprs(typing, x, &params, &ret, es)
+            }
             _ => Err(format!("use of undeclared function {}", x)),
         },
         ExprX::ApplyFun(t, e0, es) => {
@@ -274,10 +276,12 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result<Typ, TypeError> {
                 _ => return Err(format!("in field update, the destination is not a datatype")),
             }
 
-            if let Some(DeclaredX::Fun(a, t, true)) = typing.get(field_ident) {
+            if let Some(DeclaredX::Fun { params, ret, field_accessor: true }) =
+                typing.get(field_ident)
+            {
                 // t is the type of the field
-                if let [s] = &a[..] {
-                    if t1 == *s && t2 == *t {
+                if let [s] = &params[..] {
+                    if t1 == *s && t2 == *ret {
                         return Ok(t1);
                     }
                 }
@@ -635,15 +639,27 @@ pub(crate) fn add_decl<'ctx>(
                 for variant in datatype.a.iter() {
                     let typ = Arc::new(TypX::Named(datatype.name.clone()));
                     let typs = vec_map(&variant.a, |field| field.a.clone());
-                    let fun = DeclaredX::Fun(Arc::new(typs), typ.clone(), false);
+                    let fun = DeclaredX::Fun {
+                        params: Arc::new(typs),
+                        ret: typ.clone(),
+                        field_accessor: false,
+                    };
                     context.typing.insert(&variant.name, Arc::new(fun))?;
                     let is_variant = Arc::new("is-".to_string() + &variant.name.to_string());
-                    let fun = DeclaredX::Fun(Arc::new(vec![typ.clone()]), bt(), false);
+                    let fun = DeclaredX::Fun {
+                        params: Arc::new(vec![typ.clone()]),
+                        ret: bt(),
+                        field_accessor: false,
+                    };
                     context.typing.insert(&is_variant, Arc::new(fun))?;
                     for field in variant.a.iter() {
                         check_typ(&context.typing, &field.a)?;
                         let typs: Typs = Arc::new(vec![typ.clone()]);
-                        let fun = DeclaredX::Fun(typs, field.a.clone(), true);
+                        let fun = DeclaredX::Fun {
+                            params: typs,
+                            ret: field.a.clone(),
+                            field_accessor: true,
+                        };
                         context.typing.insert(&field.name, Arc::new(fun))?;
                     }
                 }
@@ -654,7 +670,8 @@ pub(crate) fn add_decl<'ctx>(
             context.typing.insert(x, var)?;
         }
         DeclX::Fun(x, typs, typ) => {
-            let fun = DeclaredX::Fun(typs.clone(), typ.clone(), false);
+            let fun =
+                DeclaredX::Fun { params: typs.clone(), ret: typ.clone(), field_accessor: false };
             context.typing.insert(x, Arc::new(fun))?;
         }
         DeclX::Var(x, typ) => {