From 13b0d28ac59b6aa506c359d96d896de1c6ec83d1 Mon Sep 17 00:00:00 2001
From: Cyrus Omar <cyology@gmail.com>
Date: Thu, 25 Jul 2024 13:52:45 -0400
Subject: [PATCH] use mode for constructor pattern elaborations + add undefined

---
 src/haz3lcore/dynamics/Elaborator.re     | 13 +++++++++----
 src/haz3lcore/dynamics/TypeAssignment.re |  1 +
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 5c34d3f6b7..d2f9767ccb 100644
--- 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
index 3ce335dbc1..eb24d66990 100644
--- 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))
   };
 };