incomplete module type created for dot analyzing

hazelgrove · May 20, 2024 · 5e567bf · 5e567bf
1 parent 450701b
commit 5e567bf
Show file tree

Hide file tree

Showing 9 changed files with 155 additions and 91 deletions.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
@@ -312,7 +312,7 @@ let rec dhexp_of_uexp =
           switch (Id.Map.find_opt(Term.UPat.rep_id(p), m)) {
           | Some(InfoPat({ty, _})) =>
             switch (ty) {
-            | Module(c) => c
+            | Module(c) => c.inner_ctx
             | _ => []
             }
           | _ => []

diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
@@ -103,17 +103,19 @@ module CastHelpers = {
   let grounded_List = NotGroundOrHole(List(Unknown(Internal)));
   let grounded_Module = (ctx: Ctx.t) =>
     NotGroundOrHole(
-      Typ.Module(
-        List.map(
-          fun
-          | Ctx.VarEntry(var_entry) =>
-            Ctx.VarEntry({...var_entry, typ: Unknown(Internal)})
-          | Ctx.ConstructorEntry(var_entry) =>
-            Ctx.ConstructorEntry({...var_entry, typ: Unknown(Internal)})
-          | Ctx.TVarEntry(tvar_entry) => Ctx.TVarEntry(tvar_entry),
-          ctx,
-        ),
-      ),
+      Typ.Module({
+        inner_ctx:
+          List.map(
+            fun
+            | Ctx.VarEntry(var_entry) =>
+              Ctx.VarEntry({...var_entry, typ: Unknown(Internal)})
+            | Ctx.ConstructorEntry(var_entry) =>
+              Ctx.ConstructorEntry({...var_entry, typ: Unknown(Internal)})
+            | Ctx.TVarEntry(tvar_entry) => Ctx.TVarEntry(tvar_entry),
+            ctx,
+          ),
+        incomplete: false,
+      }),
     );
 
   let rec ground_cases_of = (ty: Typ.t): ground_cases => {
@@ -144,19 +146,8 @@ module CastHelpers = {
       } else {
         tys |> List.length |> grounded_Prod;
       }
-    | Module(ctx) =>
-      if (List.for_all(
-            fun
-            | Ctx.VarEntry(var_entry)
-            | Ctx.ConstructorEntry(var_entry) =>
-              var_entry.typ == Unknown(Internal)
-            | Ctx.TVarEntry(_) => true,
-            ctx,
-          )) {
-        Ground;
-      } else {
-        grounded_Module(ctx);
-      }
+    | Module({inner_ctx: [], incomplete: true}) => Ground
+    | Module(_) => NotGroundOrHole(Module({inner_ctx: [], incomplete: true}))
     | Sum(sm) =>
       sm |> ConstructorMap.is_ground(is_ground_arg)
         ? Ground : grounded_Sum(sm)
@@ -311,12 +302,12 @@ module Transition = (EV: EV_MODE) => {
       | (Cast(d3', Module(ctx), Module(ctx')), BoundVar(name))
       | (Cast(d3', Module(ctx), Module(ctx')), Constructor(name)) =>
         let ty =
-          switch (Ctx.lookup_var(ctx, name)) {
+          switch (Ctx.lookup_var(ctx.inner_ctx, name)) {
           | None => Typ.Unknown(Internal)
           | Some(var) => var.typ
           };
         let ty' =
-          switch (Ctx.lookup_var(ctx', name)) {
+          switch (Ctx.lookup_var(ctx'.inner_ctx, name)) {
           | None => Typ.Unknown(Internal)
           | Some(var) => var.typ
           };

diff --git a/src/haz3lcore/statics/Module.re b/src/haz3lcore/statics/Module.re
@@ -31,7 +31,7 @@ let rec get_module =
   | Constructor(tag_name)
   | Var(tag_name) =>
     switch (Ctx.lookup_var(ctx, tag_name)) {
-    | Some({typ: Module(inner_ctx), _}) =>
+    | Some({typ: Module({inner_ctx, _}), _}) =>
       Some((name ++ tag_name ++ ".", Some(inner_ctx)))
     | _ => Some((name ++ tag_name ++ ".", None))
     }
@@ -41,7 +41,7 @@ let rec get_module =
     let inner_ctx = {
       let* ctx = ctx;
       switch (Ctx.lookup_var(ctx, tag_name)) {
-      | Some({typ: Module(inner_ctx), _}) => Some(inner_ctx)
+      | Some({typ: Module({inner_ctx, _}), _}) => Some(inner_ctx)
       | _ => None
       };
     };
@@ -51,5 +51,8 @@ let rec get_module =
   };
 };
 let mk = (name: Var.t, id: Id.t) => {
-  Typ.Module([VarEntry({name, id, typ: Unknown(Internal)})]);
+  Typ.Module({
+    inner_ctx: [VarEntry({name, id, typ: Unknown(Internal)})],
+    incomplete: true,
+  });
 };
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
@@ -524,7 +524,7 @@ and uexp_to_info_map =
       };
     };
     switch (ty) {
-    | Module(inner_ctx) =>
+    | Module({inner_ctx, _}) =>
       let (body, m) = go'(~ctx=inner_ctx, ~mode, e_mem, m);
       let m =
         e_mem.ids
@@ -744,7 +744,7 @@ and upat_to_info_map =
       add the type alias to the current context */
       let ctx = {
         switch (ctx_typ) {
-        | Module(inner_ctx) =>
+        | Module({inner_ctx, _}) =>
           switch (Ctx.lookup_tvar(inner_ctx, ctr)) {
           | Some({kind: Singleton(ty), _}) =>
             /** Currently all type shadowing are disallowed. See TyAlias */
@@ -977,7 +977,7 @@ and uexp_to_module =
       m: Map.t,
       inner_ctx: Ctx.t,
     )
-    : (Ctx.t, Info.exp, Map.t) => {
+    : (Typ.module_typ, Info.exp, Map.t) => {
   let mode =
     switch (mode) {
     | Ana(Unknown(SynSwitch)) => Mode.Syn
@@ -1018,7 +1018,7 @@ and uexp_to_module =
       // Var like patterns are looked up in the module context.
       | Var(name)
       | Constructor(name) =>
-        switch (Ctx.lookup_var(m, name)) {
+        switch (Ctx.lookup_var(m.inner_ctx, name)) {
         | Some(t) => Ana(t.typ)
         | None => Syn
         }
@@ -1286,7 +1286,7 @@ and uexp_to_module =
       let expects: Info.typ_expects =
         switch (mode) {
         | Ana(Module(m)) =>
-          switch (Ctx.lookup_alias(m, name)) {
+          switch (Ctx.lookup_alias(m.inner_ctx, name)) {
           | Some(ty) =>
             /* This check is moved here because utyp_to_info_map
                does not handle recursion. */
@@ -1342,7 +1342,7 @@ and uexp_to_module =
     (
       switch (mode) {
       | Ana(Module(m)) => m
-      | _ => inner_ctx
+      | _ => {inner_ctx, incomplete: false}
       },
       info,
       m,

diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
@@ -247,12 +247,14 @@ module UTyp = {
           List.hd(ids);
         };
         let rec upat_to_ctx =
-                ((outer_ctx: Ctx.t, inner_ctx: Ctx.t), upat: TermBase.UPat.t) => {
+                (
+                  (outer_ctx: Ctx.t, inner_ctx: Ctx.t, incomplete: bool),
+                  upat: TermBase.UPat.t,
+                ) => {
           switch (upat.term) {
           | Invalid(_)
           | EmptyHole
           | MultiHole(_)
-          | Wild
           | Int(_)
           | Float(_)
           | Bool(_)
@@ -261,7 +263,9 @@ module UTyp = {
           | ListLit(_)
           | Cons(_)
           | Tuple(_)
-          | Ap(_) => (outer_ctx, inner_ctx)
+          | Wild
+          | Ap(_) => (outer_ctx, inner_ctx, incomplete)
+          // | Wild => (outer_ctx, inner_ctx, true) // disabled due to casting issues.
           | TypeAnn(var, utyp1) =>
             switch (var.term, utyp1.term) {
             | (Var(name), _)
@@ -276,15 +280,17 @@ module UTyp = {
                   }),
                   ...inner_ctx,
                 ],
+                incomplete,
               )
-            | _ => (outer_ctx, inner_ctx)
+            | _ => (outer_ctx, inner_ctx, incomplete)
             }
           | Var(name) => (
               outer_ctx,
               [
                 VarEntry({name, id: rep_id_p(upat), typ: Unknown(TypeHole)}),
                 ...inner_ctx,
               ],
+              incomplete,
             )
           | Constructor(name) => (
               outer_ctx,
@@ -296,6 +302,7 @@ module UTyp = {
                 }),
                 ...inner_ctx,
               ],
+              incomplete,
             )
           | TyAlias(typat, utyp) =>
             switch (typat.term) {
@@ -339,22 +346,23 @@ module UTyp = {
               | Some(sm) => (
                   Ctx.add_ctrs(ctx_body, name, rep_id(utyp), sm),
                   Ctx.add_ctrs(new_inner, name, rep_id(utyp), sm),
+                  incomplete,
                 )
-              | None => (ctx_body, new_inner)
+              | None => (ctx_body, new_inner, incomplete)
               };
 
-            | _ => (outer_ctx, inner_ctx)
+            | _ => (outer_ctx, inner_ctx, incomplete)
             }
-          | Parens(p) => upat_to_ctx((outer_ctx, inner_ctx), p)
+          | Parens(p) => upat_to_ctx((outer_ctx, inner_ctx, incomplete), p)
           };
         };
         let rec get_Tuple: TermBase.UPat.t => Typ.t = (
           ut =>
             switch (ut.term) {
             | Tuple(us) =>
-              let (_, module_ctx) =
-                List.fold_left(upat_to_ctx, (ctx, []), us);
-              Module(module_ctx);
+              let (_, inner_ctx, incomplete) =
+                List.fold_left(upat_to_ctx, (ctx, [], false), us);
+              Module({inner_ctx, incomplete});
             | Parens(p) => get_Tuple(p)
             | TypeAnn(_)
             | Var(_)
@@ -372,8 +380,9 @@ module UTyp = {
             | ListLit(_)
             | Cons(_)
             | Ap(_) =>
-              let (_, module_ctx) = upat_to_ctx((ctx, []), ut);
-              Module(module_ctx);
+              let (_, inner_ctx, incomplete) =
+                upat_to_ctx((ctx, [], false), ut);
+              Module({inner_ctx, incomplete});
             }
         );
         get_Tuple(u);