type assignment for internal expressions (#1121)

hazelgrove · Jul 25, 2024 · f98760f · f98760f
2 parents c7ed9ed + 13b0d28
commit f98760f
Show file tree

Hide file tree

Showing 10 changed files with 385 additions and 23 deletions.
diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
@@ -40,7 +40,7 @@ module rec DHExp: {
     | ListConcat(t, t)
     | Tuple(list(t))
     | Prj(t, int)
-    | Constructor(string)
+    | Constructor(string, Typ.t)
     | ConsistentCase(case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
@@ -102,7 +102,7 @@ module rec DHExp: {
     | ListConcat(t, t)
     | Tuple(list(t))
     | Prj(t, int)
-    | Constructor(string)
+    | Constructor(string, Typ.t)
     | ConsistentCase(case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)

diff --git a/src/haz3lcore/dynamics/DHPat.re b/src/haz3lcore/dynamics/DHPat.re
@@ -15,7 +15,7 @@ type t =
   | ListLit(Typ.t, list(t))
   | Cons(t, t)
   | Tuple(list(t))
-  | Constructor(string)
+  | Constructor(string, Typ.t)
   | Ap(t, t);
 
 let mk_tuple: list(t) => t =

diff --git a/src/haz3lcore/dynamics/Delta.re b/src/haz3lcore/dynamics/Delta.re
@@ -4,5 +4,9 @@ type hole_sort =
   | PatternHole;
 
 [@deriving sexp]
-type t = MetaVarMap.t((hole_sort, Typ.t, VarCtx.t));
+type val_ty = (hole_sort, Typ.t, Ctx.t);
+
+[@deriving sexp]
+type t = MetaVarMap.t(val_ty);
+
 let empty: t = (MetaVarMap.empty: t);
diff --git a/src/haz3lcore/dynamics/Delta.rei b/src/haz3lcore/dynamics/Delta.rei
@@ -4,6 +4,9 @@ type hole_sort =
   | PatternHole;
 
 [@deriving sexp]
-type t = MetaVarMap.t((hole_sort, Typ.t, VarCtx.t));
+type val_ty = (hole_sort, Typ.t, Ctx.t);
+
+[@deriving sexp]
+type t = MetaVarMap.t(val_ty);
 
 let empty: t;
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -172,6 +172,7 @@ let rec dhexp_of_uexp =
         let* dp = dhpat_of_upat(m, p);
         let* d1 = dhexp_of_uexp(m, body);
         let+ ty = fixed_pat_typ(m, p);
+        let ty = Typ.normalize(ctx, ty);
         DHExp.Fun(dp, ty, d1, None);
       | TypFun(tpat, body) =>
         let+ d1 = dhexp_of_uexp(m, body);
@@ -189,8 +190,10 @@ let rec dhexp_of_uexp =
         DHExp.ListConcat(dc1, dc2);
       | UnOp(Meta(Unquote), e) =>
         switch (e.term) {
-        | Var("e") when in_filter => Some(Constructor("$e"))
-        | Var("v") when in_filter => Some(Constructor("$v"))
+        | Var("e") when in_filter =>
+          Some(Constructor("$e", Unknown(Internal)))
+        | Var("v") when in_filter =>
+          Some(Constructor("$v", Unknown(Internal)))
         | _ => Some(DHExp.EmptyHole(id, 0))
         }
       | UnOp(Int(Minus), e) =>
@@ -235,7 +238,17 @@ let rec dhexp_of_uexp =
         switch (err_status) {
         | InHole(Common(NoType(FreeConstructor(_)))) =>
           Some(FreeVar(id, 0, name))
-        | _ => Some(Constructor(name))
+        | _ =>
+          let ty =
+            switch (Ctx.lookup_ctr(ctx, name)) {
+            | None => Typ.Unknown(Internal)
+            | Some({typ, _}) => Typ.normalize(ctx, typ)
+            };
+          switch (mode) {
+          | Ana(ana_ty) =>
+            Some(Constructor(name, Typ.normalize(ctx, ana_ty)))
+          | _ => Some(Constructor(name, ty))
+          };
         }
       | Let(p, def, body) =>
         let add_name: (option(string), DHExp.t) => DHExp.t = (
@@ -262,6 +275,7 @@ let rec dhexp_of_uexp =
             dbody,
           );
         } else {
+          let ty = Typ.normalize(ctx, ty);
           switch (Term.UPat.get_bindings(p) |> Option.get) {
           | [f] =>
             /* simple recursion */
@@ -440,7 +454,19 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
       switch (err_status) {
       | InHole(Common(NoType(FreeConstructor(_)))) =>
         Some(BadConstructor(u, 0, name))
-      | _ => wrap(Constructor(name))
+      | _ =>
+        let ty =
+          switch (Ctx.lookup_ctr(ctx, name)) {
+          | None => Typ.Unknown(Internal)
+          | Some({typ, _}) => Typ.normalize(ctx, typ)
+          };
+        let dc =
+          switch (mode) {
+          | Ana(ana_ty) =>
+            DHPat.Constructor(name, Typ.normalize(ctx, ana_ty))
+          | _ => DHPat.Constructor(name, ty)
+          };
+        wrap(dc);
       }
     | Cons(hd, tl) =>
       let* d_hd = dhpat_of_upat(m, hd);

diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -12,8 +12,8 @@ let rec matches_exp =
     true;
   } else {
     switch (d, f) {
-    | (Constructor("$e"), _) => failwith("$e in matched expression")
-    | (Constructor("$v"), _) => failwith("$v in matched expression")
+    | (Constructor("$e", _), _) => failwith("$e in matched expression")
+    | (Constructor("$v", _), _) => failwith("$v in matched expression")
 
     // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps
     | (FixF(dp, dt, dc), FixF(fp, ft, fc)) =>
@@ -30,15 +30,15 @@ let rec matches_exp =
     | (d, FixF(fp, _, fc)) =>
       matches_exp(d, ~fenv=fenv |> ClosureEnvironment.without_keys([fp]), fc)
 
-    | (_, Constructor("$v")) =>
+    | (_, Constructor("$v", _)) =>
       switch (ValueChecker.check_value(denv, d)) {
       | Indet
       | Value => true
       | Expr => false
       }
 
     | (_, EmptyHole(_))
-    | (_, Constructor("$e")) => true
+    | (_, Constructor("$e", _)) => true
 
     | (Cast(d, _, _), Cast(f, _, _)) => matches_exp(d, f)
     | (Closure(denv, d), Closure(fenv, f)) =>
@@ -147,8 +147,8 @@ let rec matches_exp =
     | (StringLit(dv), StringLit(fv)) => dv == fv
     | (StringLit(_), _) => false
 
-    | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true
-    | (Constructor(dt), Constructor(ft)) => dt == ft
+    | (Constructor(_), Ap(Constructor("~MVal", _), Tuple([]))) => true
+    | (Constructor(dt, _), Constructor(ft, _)) => dt == ft
     | (Constructor(_), _) => false
 
     | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn
@@ -317,7 +317,7 @@ and matches_pat = (d: DHPat.t, f: DHPat.t): bool => {
     | res => matches_typ(dty1, fty1) && res
     }
   | (ListLit(_), _) => false
-  | (Constructor(dt), Constructor(ft)) => dt == ft
+  | (Constructor(dt, _), Constructor(ft, _)) => dt == ft
   | (Constructor(_), _) => false
   | (Var(_), Var(_)) => true
   | (Var(_), _) => false

diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re
@@ -112,7 +112,7 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result =>
       }
     }
   | (
-      Ap(Constructor(ctr), dp_opt),
+      Ap(Constructor(ctr, _), dp_opt),
       Cast(d, Sum(sm1) | Rec(_, Sum(sm1)), Sum(sm2) | Rec(_, Sum(sm2))),
     ) =>
     switch (cast_sum_maps(sm1, sm2)) {
@@ -125,10 +125,10 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result =>
     matches(dp, d)
   | (Ap(_, _), _) => DoesNotMatch
 
-  | (Constructor(ctr), Constructor(ctr')) =>
+  | (Constructor(ctr, _), Constructor(ctr', _)) =>
     ctr == ctr' ? Matches(Environment.empty) : DoesNotMatch
   | (
-      Constructor(ctr),
+      Constructor(ctr, _),
       Cast(d, Sum(sm1) | Rec(_, Sum(sm1)), Sum(sm2) | Rec(_, Sum(sm2))),
     ) =>
     switch (cast_sum_maps(sm1, sm2)) {
@@ -210,7 +210,7 @@ and matches_cast_Sum =
     )
     : match_result =>
   switch (d) {
-  | Constructor(ctr') =>
+  | Constructor(ctr', _) =>
     switch (
       dp,
       castmaps |> List.map(ConstructorMap.find_opt(ctr')) |> OptUtil.sequence,
@@ -219,7 +219,7 @@ and matches_cast_Sum =
       ctr == ctr' ? Matches(Environment.empty) : DoesNotMatch
     | _ => DoesNotMatch
     }
-  | Ap(Constructor(ctr'), d') =>
+  | Ap(Constructor(ctr', _), d') =>
     switch (
       dp,
       castmaps |> List.map(ConstructorMap.find_opt(ctr')) |> OptUtil.sequence,