use mode for constructor pattern elaborations + add undefined

hazelgrove · Jul 25, 2024 · 13b0d28 · 13b0d28
1 parent 64f5d13
commit 13b0d28
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -455,11 +455,16 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
       | InHole(Common(NoType(FreeConstructor(_)))) =>
         Some(BadConstructor(u, 0, name))
       | _ =>
-        let dc =
+        let ty =
           switch (Ctx.lookup_ctr(ctx, name)) {
-          | None => DHPat.Constructor(name, Unknown(Internal))
-          | Some({typ, _}) =>
-            DHPat.Constructor(name, Typ.normalize(ctx, typ))
+          | 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);
       }

diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -315,6 +315,7 @@ let rec typ_of_dhexp =
     } else {
       None;
     };
+  | Undefined => Some(Typ.Unknown(Internal))
   };
 };
-Original file line number
+Diff line change
@@ Expand Up / @@ -315,6 +315,7 @@ let rec typ_of_dhexp = @@
         } else {
           None;
         };
+      | Undefined => Some(Typ.Unknown(Internal))
       };
     };
@@ Expand Down @@