Merge branch 'param_types_update' into dev

src/haz3lcore/dynamics/DHExp.re

@@ -69,7 +69,7 @@ let rec strip_casts =
         | Filter(_)
         | Let(_)
         | FixF(_)
-        | TyAlias(_)
+        | TyDef(_)
         | Fun(_)
         | Ap(_)
         | Deferral(_)
@@ -159,7 +159,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | FailedCast(_, _, _)
           | MultiHole(_)
           | Deferral(_)
-          | TyAlias(_)
+          | TyDef(_)
           | DeferredAp(_)
           | Parens(_)
           | UnOp(_) => continue(exp)

src/haz3lcore/dynamics/FilterMatcher.re

@@ -328,9 +328,9 @@ let rec matches_exp =
 
     | (Undefined, _) => false
 
-    | (TyAlias(dtp, dut, dd), TyAlias(ftp, fut, fd)) =>
+    | (TyDef(dtp, dut, dd), TyDef(ftp, fut, fd)) =>
       dtp == ftp && dut == fut && matches_exp(dd, fd)
-    | (TyAlias(_), _) => false
+    | (TyDef(_), _) => false
     };
   };
 }

src/haz3lcore/dynamics/Substitution.re

@@ -141,9 +141,9 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
     let d5' = subst_var(m, d1, x, d5);
     let d6' = subst_var(m, d1, x, d6);
     If(d4', d5', d6') |> rewrap;
-  | TyAlias(tp, ut, d4) =>
+  | TyDef(tp, ut, d4) =>
     let d4' = subst_var(m, d1, x, d4);
-    TyAlias(tp, ut, d4') |> rewrap;
+    TyDef(tp, ut, d4') |> rewrap;
   | Parens(d4) =>
     let d4' = subst_var(m, d1, x, d4);
     Parens(d4') |> rewrap;

src/haz3lcore/dynamics/Transition.re

@@ -726,7 +726,7 @@ module Transition = (EV: EV_MODE) => {
     | Parens(d) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveParens, is_value: false});
-    | TyAlias(_, _, d) =>
+    | TyDef(_, _, d) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveTypeAlias, is_value: false});
     | Filter(f1, d1) =>

src/haz3lcore/dynamics/TypeAssignment.re

@@ -343,7 +343,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     } else {
       None;
     };
-  | TyAlias(_, _, d) => typ_of_dhexp(ctx, m, d)
+  | TyDef(_, _, d) => typ_of_dhexp(ctx, m, d)
   | Parens(d) => typ_of_dhexp(ctx, m, d)
   };
 };

src/haz3lcore/dynamics/Unboxing.re

@@ -223,7 +223,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
         Let(_) |
         Fun(_, _, _, None) |
         FixF(_) |
-        TyAlias(_) |
+        TyDef(_) |
         Ap(_) |
         If(_) |
         Seq(_) |

src/haz3lcore/lang/term/TPat.re

@@ -3,6 +3,7 @@ type cls =
   | Invalid
   | EmptyHole
   | MultiHole
+  | Ap
   | Var;
 
 include TermBase.TPat;
@@ -21,11 +22,13 @@ let cls_of_term: term => cls =
   | Invalid(_) => Invalid
   | EmptyHole => EmptyHole
   | MultiHole(_) => MultiHole
-  | Var(_) => Var;
+  | Var(_) => Var
+  | Ap(_, _) => Ap;
 
 let show_cls: cls => string =
   fun
   | Invalid => "Invalid type alias"
   | MultiHole => "Broken type alias"
   | EmptyHole => "Empty type alias hole"
+  | Ap => "Type substitution"
   | Var => "Type alias";

src/haz3lcore/lang/term/Typ.re

@@ -514,6 +514,11 @@ let rec needs_parens = (ty: t): bool =>
 let pretty_print_tvar = (tv: TPat.t): string =>
   switch (IdTagged.term_of(tv)) {
   | Var(x) => x
+  | Ap(_, x) =>
+    switch (x) {
+    | Var(y) => y
+    | _ => "?" //double check for doubly recursive types? maybe?
+    }
   | Invalid(_)
   | EmptyHole
   | MultiHole(_) => "?"

src/haz3lcore/pretty/ExpToSegment.re

@@ -310,7 +310,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     [mk_form("fix", id, [p])]
     @ e
     |> fold_fun_if(settings.fold_fn_bodies, name);
-  | TyAlias(tp, t, e) =>
+  | TyDef(tp, t, e) =>
     // TODO: Add optional newlines
     let id = exp |> Exp.rep_id;
     let+ tp = tpat_to_pretty(~settings: Settings.t, tp)
@@ -730,7 +730,7 @@ let rec external_precedence = (exp: Exp.t): Precedence.t => {
 
   // Top-level things
   | Filter(_)
-  | TyAlias(_)
+  | TyDef(_)
   | Let(_) => Precedence.let_
 
   // Matt: I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
@@ -885,8 +885,8 @@ let rec parenthesize = (~show_filters: bool, exp: Exp.t): Exp.t => {
       c // TODO: Parenthesize through closure
     )
     |> rewrap
-  | TyAlias(tp, t, e) =>
-    TyAlias(
+  | TyDef(tp, t, e) =>
+    TyDef(
       tp,
       parenthesize_typ(t) |> paren_typ_at(Precedence.min),
       parenthesize(e) |> paren_assoc_at(Precedence.let_),

src/haz3lcore/statics/Elaborator.re

@@ -314,7 +314,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
       FixF(p', fresh_cast(e', tye, typ), env) |> rewrap |> cast_from(typ);
-    | TyAlias(_, _, e) =>
+    | TyDef(_, _, e) =>
       let (e', tye) = elaborate(m, e);
       e' |> cast_from(tye);
     | Ap(dir, f, a) =>

src/haz3lcore/statics/Info.re

@@ -170,7 +170,7 @@ type type_var_err =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type shadow_src =
   | BaseTyp
-  | TyAlias
+  | TyDef
   | TyVar;
 
 /* Type pattern term errors */
@@ -183,7 +183,8 @@ type error_tpat =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type ok_tpat =
   | Empty
-  | Var(string);
+  | Var(string)
+  | Ap(string, string);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type status_tpat =
@@ -502,13 +503,28 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat =>
     if (Form.is_base_typ(name)) {
       f(BaseTyp);
     } else if (Ctx.is_alias(ctx, name)) {
-      f(TyAlias);
+      f(TyDef);
     } else {
       f(TyVar);
     };
   | Var(name) => NotInHole(Var(name))
   | Invalid(_) => InHole(NotAVar(NotCapitalized))
   | MultiHole(_) => InHole(NotAVar(Other))
+  | Ap(arg1, arg2) =>
+    switch (arg1, arg2) {
+    | (Var(name), _)
+        when Form.is_base_typ(name) || Ctx.lookup_alias(ctx, name) != None =>
+      let f = src => InHole(ShadowsType(name, src));
+      if (Form.is_base_typ(name)) {
+        f(BaseTyp);
+      } else if (Ctx.is_alias(ctx, name)) {
+        f(TyDef);
+      } else {
+        f(TyVar);
+      };
+    | (Var(x), Var(y)) => NotInHole(Ap(x, y))
+    | _ => InHole(NotAVar(Other))
+    }
   };
 
 /* Determines whether any term is in an error hole. */

src/haz3lcore/statics/MakeTerm.re

@@ -229,7 +229,7 @@ and exp_term: unsorted => (Exp.term, list(Id.t)) = {
         | (["debug", "in"], [Exp(filter)]) =>
           Filter(Filter({act: (Step, All), pat: filter}), r)
         | (["type", "=", "in"], [TPat(tpat), Typ(def)]) =>
-          TyAlias(tpat, def, r)
+          TyDef(tpat, def, r)
         | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) =>
           If(cond, conseq, r)
         | _ => hole(tm)

src/haz3lcore/statics/Statics.re

@@ -599,7 +599,7 @@ and uexp_to_info_map =
         (unwrapped_self, m);
       };
     add'(~self, ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs), m);
-  | TyAlias(typat, utyp, body) =>
+  | TyDef(typat, utyp, body) =>
     let m = utpat_to_info_map(~ctx, ~ancestors, typat, m) |> snd;
     switch (typat.term) {
     | Var(name) when !Ctx.shadows_typ(ctx, name) =>
@@ -660,6 +660,139 @@ and uexp_to_info_map =
         go'(~ctx, ~mode, body, m);
       let m = utyp_to_info_map(~ctx, ~ancestors, utyp, m) |> snd;
       add(~self=Just(ty_body), ~co_ctx, m);
+    | Ap(t1, t2) =>
+      let name =
+        switch (t1) {
+        | Var(s) => s
+        | _ => ""
+        };
+      let arg =
+        switch (t2) {
+        | Var(s) => s
+        | _ => ""
+        };
+      let utyp_without_ap = UTyp.remove_ap_in_def(name, arg, utyp);
+      let (ty_def, ctx_def, ctx_body) = {
+        let ty_pre =
+          UTyp.to_typ(
+            Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg),
+            utyp,
+          );
+        switch (utyp.term) {
+        | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) =>
+          let ty_pre =
+            UTyp.to_typ(
+              Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg),
+              utyp_without_ap,
+            );
+          let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
+          let ctx_def =
+            Ctx.extend_higher_kind(
+              ctx,
+              name,
+              arg,
+              UTPat.rep_id(typat),
+              ty_rec,
+            );
+          (ty_rec, ctx_def, ctx_def);
+        | _ => (
+            ty_pre,
+            Ctx.extend_higher_kind(
+              ctx,
+              name,
+              arg,
+              UTPat.rep_id(typat),
+              ty_pre,
+            ),
+            Ctx.extend_higher_kind(
+              ctx,
+              name,
+              arg,
+              UTPat.rep_id(typat),
+              ty_pre,
+            ),
+          )
+        };
+      };
+      let ctx_body = {
+        let ty_pre =
+          UTyp.to_typ(
+            Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg),
+            utyp,
+          );
+
+        switch (ty_pre) {
+        | Sum(sm_map) =>
+          Ctx.add_ctr_with_typ_parameter(
+            ctx_body,
+            name,
+            UTyp.rep_id(utyp),
+            sm_map,
+            arg,
+          )
+        | _ => ctx_body
+        };
+      };
+      let ({co_ctx, ty: ty_body, _}: Info.exp, m) =
+        go'(~ctx=ctx_body, ~mode, body, m);
+      /* Make sure types don't escape their scope */
+      let ty_escape = Typ.subst(ty_def, name, ty_body);
+      let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd;
+      add(~self=Just(ty_escape), ~co_ctx, m);
+
+      //  let (ty_def, ctx_def, ctx_body) = {
+      //         switch (utyp.term) {
+      //         | Sum(_) when List.mem(name, Typ.free_vars(utyp)) =>
+      //           /* NOTE: When debugging type system issues it may be beneficial to
+      //              use a different name than the alias for the recursive parameter */
+      //           //let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
+      //           let ty_rec =
+      //             Rec((Var(name): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp;
+      //           let ctx_def =
+      //             Ctx.extend_alias(ctx, name, TPat.rep_id(typat), ty_rec);
+      //           (ty_rec, ctx_def, ctx_def);
+      //         | _ => (
+      //             utyp,
+      //             ctx,
+      //             Ctx.extend_alias(ctx, name, TPat.rep_id(typat), utyp),
+      //           )
+
+      let (ty_def, ctx_def, ctx_body) = {
+        switch (utyp.term) {
+        | Sum(_) when List.mem(constructor, Typ.free_vars(utyp)) =>
+          let ty_rec =
+            Rec((Var("α"): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp; //worried because
+          let ctx_def =
+            Ctx.extend_alias(ctx, constructor, TPat.rep_id(typat), ty_rec);
+          (ty_rec, ctx_def, ctx_def);
+
+        | _ =>
+          let ty = Typ.to_typ(ctx, utyp);
+          (
+            utyp, //not sure about the usage of utyp here
+            ctx,
+            Ctx.extend_alias(ctx, constructor, TPat.rep_id(typat), ty),
+          );
+        };
+      };
+      //Printf.printf(
+      //  "ty_def: %s, ctx_def: %s, ctx_body: %s \n",
+      //  Typ.show(ty_def),
+      //  Ctx.show(ctx_def),
+      //  Ctx.show(ctx_body),
+      //);
+      let ctx_body =
+        switch (Typ.get_sum_constructors(ctx, ty_def)) {
+        | Some(sm) =>
+          Ctx.add_ctrs(ctx_body, constructor, UTyp.rep_id(utyp), sm)
+        | None => ctx_body
+        };
+      let ({co_ctx, ty: ty_body, _}: Info.exp, m) =
+        go'(~ctx=ctx_body, ~mode, body, m);
+      /* Make sure types don't escape their scope */
+      let ty_escape = Typ.subst(ty_def, constructor, ty_body);
+      let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd;
+      add(~self=Just(ty_escape), ~co_ctx, m);
     };
   };
 }