Fix and merge ploy-adt-after2

hazelgrove · Mar 7, 2024 · 233f55a · 233f55a
1 parent e711929
commit 233f55a
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 6 deletions.
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
@@ -279,6 +279,9 @@ module Transition = (EV: EV_MODE) => {
           /* Treat a hole or invalid tyvar name as a unique type variable that doesn't appear anywhere else. Thus instantiating it at anything doesn't produce any substitutions. */
           Step({apply: () => tfbody, kind: TypFunAp, value: false})
         }
+      | Constructor(name) =>
+        /* Rule ITTCon */
+        Step({apply: () => Constructor(name), kind: TypFunAp, value: false})
       | Cast(d'', Forall(x, t), Forall(x', t')) =>
         /* Rule ITTApCast */
         Step({

diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
@@ -217,10 +217,10 @@ let bad_token_cls: string => bad_token_cls =
    Order in this list determines relative remolding
    priority for forms with overlapping regexps */
 let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
-  //("ty_var", (is_typ_var, [mk_op(Typ, [])])),
-  //("ty_var_p", (is_typ_var, [mk_op(TPat, [])])),
-  //("ctr", (is_ctr, [mk_op(Exp, []), mk_op(Pat, [])])),
-  //("type", (is_base_typ, [mk_op(Typ, [])])),
+  ("ty_var", (is_typ_var, [mk_op(Typ, [])])),
+  ("ty_var_p", (is_typ_var, [mk_op(TPat, [])])),
+  ("ctr", (is_ctr, [mk_op(Exp, []), mk_op(Pat, [])])),
+  ("type", (is_base_typ, [mk_op(Typ, [])])),
   ("var", (is_var, [mk_op(Exp, []), mk_op(Pat, [])])),
   (
     "explicit_hole",

diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
@@ -408,6 +408,7 @@ and tpat = unsorted => {
   return(ty => TPat(ty), ids, {ids, term});
 }
 and tpat_term = (unsorted: unsorted): UTPat.term => {
+  Printf.printf("tpat_term: %s\n", show_unsorted(unsorted));
   let ret = (term: UTPat.term) => term;
   let hole = unsorted => Term.UTPat.hole(kids_of_unsorted(unsorted));
   switch (unsorted) {
@@ -431,7 +432,7 @@ and tpat_term = (unsorted: unsorted): UTPat.term => {
         switch (tile) {
         | (["(", ")"], [TPat(arg)]) =>
           switch (arg.term) {
-          | Invalid(s) when Form.is_type_input(s) =>
+          | Var(s) when Form.is_type_input(s) =>
             Ap(l, {ids: arg.ids, term: Var(s)})
           | _ => ret(hole(tm))
           }

diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re
@@ -366,7 +366,9 @@ module rec Typ: {
     | (ty2, Ap(Var(name), ty))
     | (Ap(Var(name), ty), ty2) =>
       switch (Ctx.lookup_higher_kind(ctx, name)) {
-      | Some((arg, ty_out)) => join'(subst(ty, arg, ty_out), ty2)
+      | Some((arg, ty_out)) =>
+        Printf.printf("ty2: %s\n", show(ty2));
+        join'(subst(ty, arg, ty_out), ty2);
       | _ => None
       }
     | (ty, Ap(Forall(name, t1), t2))