Merge DHExp and UExp (#1197)

hazelgrove · Jul 31, 2024 · 40d1896 · 40d1896
2 parents 2bfaef4 + 73826ea
commit 40d1896
Show file tree

Hide file tree

Showing 133 changed files with 7,016 additions and 7,665 deletions.
diff --git a/src/haz3lcore/TermMap.re b/src/haz3lcore/TermMap.re
@@ -1,5 +1,5 @@
 include Id.Map;
-type t = Id.Map.t(Term.t);
+type t = Id.Map.t(Any.t);
 
-let add_all = (ids: list(Id.t), tm: Term.t, map: t) =>
+let add_all = (ids: list(Id.t), tm: Any.t, map: t) =>
   ids |> List.fold_left((map, id) => add(id, tm, map), map);
diff --git a/src/haz3lcore/Unicode.re b/src/haz3lcore/Unicode.re
@@ -8,6 +8,7 @@ let zwsp = "";
 
 let typeArrowSym = "→"; // U+2192 "Rightwards Arrow"
 let castArrowSym = "⇨";
+let castBackArrowSym = "⇦";
 
 let ellipsis = "\xE2\x80\xA6";
 

diff --git a/src/haz3lcore/assistant/AssistantCtx.re b/src/haz3lcore/assistant/AssistantCtx.re
@@ -50,7 +50,7 @@ let bound_constructors =
 let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
   List.filter_map(
     fun
-    | Ctx.VarEntry({typ: Arrow(_, ty_out) as ty_arr, name, _})
+    | Ctx.VarEntry({typ: {term: Arrow(_, ty_out), _} as ty_arr, name, _})
         when
           Typ.is_consistent(ctx, ty_expect, ty_out)
           && !Typ.is_consistent(ctx, ty_expect, ty_arr) => {
@@ -66,7 +66,11 @@ let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
 let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
   List.filter_map(
     fun
-    | Ctx.ConstructorEntry({typ: Arrow(_, ty_out) as ty_arr, name, _})
+    | Ctx.ConstructorEntry({
+        typ: {term: Arrow(_, ty_out), _} as ty_arr,
+        name,
+        _,
+      })
         when
           Typ.is_consistent(ctx, ty, ty_out)
           && !Typ.is_consistent(ctx, ty, ty_arr) =>
@@ -141,7 +145,7 @@ let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
     let exp_aps = ty =>
       bound_aps(ty, ctx)
       @ bound_constructor_aps(x => Exp(Common(x)), ty, ctx);
-    switch (Mode.ty_of(mode)) {
+    switch (Mode.ty_of(mode) |> Typ.term_of) {
     | List(ty) =>
       List.map(restrategize(" )::"), exp_aps(ty))
       @ List.map(restrategize("::"), exp_refs(ty))
@@ -152,20 +156,20 @@ let suggest_lookahead_variable = (ci: Info.t): list(Suggestion.t) => {
       @ List.map(restrategize(commas), exp_refs(ty));
     | Bool =>
       /* TODO: Find a UI to make these less confusing */
-      exp_refs(Int)
-      @ exp_refs(Float)
-      @ exp_refs(String)
-      @ exp_aps(Int)
-      @ exp_aps(Float)
-      @ exp_aps(String)
+      exp_refs(Int |> Typ.fresh)
+      @ exp_refs(Float |> Typ.fresh)
+      @ exp_refs(String |> Typ.fresh)
+      @ exp_aps(Int |> Typ.fresh)
+      @ exp_aps(Float |> Typ.fresh)
+      @ exp_aps(String |> Typ.fresh)
     | _ => []
     };
   | InfoPat({mode, co_ctx, _}) =>
     let pat_refs = ty =>
       free_variables(ty, ctx, co_ctx)
       @ bound_constructors(x => Pat(Common(x)), ty, ctx);
     let pat_aps = ty => bound_constructor_aps(x => Pat(Common(x)), ty, ctx);
-    switch (Mode.ty_of(mode)) {
+    switch (Mode.ty_of(mode) |> Typ.term_of) {
     | List(ty) =>
       List.map(restrategize(" )::"), pat_aps(ty))
       @ List.map(restrategize("::"), pat_refs(ty))

diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re
@@ -11,33 +11,36 @@ let leading_expander = " " ++ AssistantExpander.c;
  * running Statics, but for now, new forms e.g. operators must be added
  * below manually.  */
 module Typ = {
-  let unk: Typ.t = Unknown(Internal);
+  let unk: Typ.t = Unknown(Internal) |> Typ.fresh;
 
   let of_const_mono_delim: list((Token.t, Typ.t)) = [
-    ("true", Bool),
-    ("false", Bool),
+    ("true", Bool |> Typ.fresh),
+    ("false", Bool |> Typ.fresh),
     //("[]", List(unk)), / *NOTE: would need to refactor buffer for this to show up */
     //("()", Prod([])), /* NOTE: would need to refactor buffer for this to show up */
-    ("\"\"", String), /* NOTE: Irrelevent as second quote appears automatically */
+    ("\"\"", String |> Typ.fresh), /* NOTE: Irrelevent as second quote appears automatically */
     ("_", unk),
   ];
 
   let of_leading_delim: list((Token.t, Typ.t)) = [
     ("case" ++ leading_expander, unk),
-    ("fun" ++ leading_expander, Arrow(unk, unk)),
-    ("typfun" ++ leading_expander, Forall("", unk)),
+    ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
+    (
+      "typfun" ++ leading_expander,
+      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+    ),
     ("if" ++ leading_expander, unk),
     ("let" ++ leading_expander, unk),
-    ("test" ++ leading_expander, Prod([])),
+    ("test" ++ leading_expander, Prod([]) |> Typ.fresh),
     ("type" ++ leading_expander, unk),
   ];
 
-  let of_infix_delim: list((Token.t, Typ.t)) = [
-    ("|>", unk), /* */
+  let of_infix_delim: list((Token.t, Typ.term)) = [
+    ("|>", Unknown(Internal)), /* */
     (",", Prod([unk, unk])), /* NOTE: Current approach doesn't work for this, but irrelevant as 1-char */
     ("::", List(unk)),
     ("@", List(unk)),
-    (";", unk),
+    (";", Unknown(Internal)),
     ("&&", Bool),
     ("\\/", Bool),
     ("||", Bool),
@@ -72,7 +75,7 @@ module Typ = {
     fun
     | InfoExp({mode, _})
     | InfoPat({mode, _}) => Mode.ty_of(mode)
-    | _ => Unknown(Internal);
+    | _ => Unknown(Internal) |> Typ.fresh;
 
   let filter_by =
       (
@@ -194,7 +197,10 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => {
 };
 
 let suggest_operator: Info.t => list(Suggestion.t) =
-  suggest_form(Typ.of_infix_delim, Delims.infix);
+  suggest_form(
+    List.map(((a, b)) => (a, IdTagged.fresh(b)), Typ.of_infix_delim),
+    Delims.infix,
+  );
 
 let suggest_operand: Info.t => list(Suggestion.t) =
   suggest_form(Typ.of_const_mono_delim, Delims.const_mono);