Type Slicing

src/haz3lcore/TyDi/ErrorPrint.re

@@ -48,7 +48,7 @@ let common_error: Info.error_common => string =
   | DuplicateLabel(_, _) => "Duplicate label"
   | TupleLabelError(_) => "Invalid tuple label"
   | NoType(BadToken(token)) => prn("\"%s\" isn't a valid token", token)
-  | Inconsistent(WithArrow(ty)) =>
+  | Inconsistent(WithArrow(ty, _slc)) =>
     prn("type %s is not consistent with arrow type", Print.typ(ty))
   | Inconsistent(CompareFun(ty)) =>
     prn("values of type %s cannot be compared", Print.typ(ty))
@@ -87,7 +87,7 @@ let exp_error: Info.error_exp => string =
 
 let pat_error: Info.error_pat => string =
   fun
-  | ExpectedConstructor => "Expected a constructor"
+  | ExpectedConstructor(_slc) => "Expected a constructor"
   | Redundant(_) => "Redundant" //TODO: elaborate
   | Common(error) => common_error(error);
 

src/haz3lcore/TyDi/TyDiCtx.re

@@ -71,14 +71,17 @@ let bound_constructors =
 let bound_aps = (ty_expect: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
   List.filter_map(
     fun
-    | 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) => {
+    | Ctx.VarEntry({typ: ty_arr, name, _}) =>
+      switch (ty_arr |> Typ.term_of) {
+      | Arrow(_, ty_out)
+          when
+            Typ.is_consistent(ctx, ty_expect, ty_out)
+            && !Typ.is_consistent(ctx, ty_expect, ty_arr) =>
         Some({
           content: name ++ "(",
           strategy: Exp(Common(FromCtxAp(ty_out))),
-        });
+        })
+      | _ => None
       }
     | _ => None,
     ctx.entries,
@@ -88,18 +91,18 @@ let bound_constructor_aps =
     (wrap, ty: Typ.t, ctx: Ctx.t): list(TyDiSuggestion.t) =>
   List.filter_map(
     fun
-    | 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) =>
-      Some({
-        content: name ++ "(",
-        strategy: wrap(FromCtxAp(ty_out)),
-      })
+    | Ctx.ConstructorEntry({typ: ty_arr, name, _}) =>
+      switch (ty_arr |> Typ.term_of) {
+      | Arrow(_, ty_out)
+          when
+            Typ.is_consistent(ctx, ty, ty_out)
+            && !Typ.is_consistent(ctx, ty, ty_arr) =>
+        Some({
+          content: name ++ "(",
+          strategy: wrap(FromCtxAp(ty_out)),
+        })
+      | _ => None
+      }
     | _ => None,
     ctx.entries,
   );
@@ -165,7 +168,7 @@ let suggest_lookahead_variable = (ci: Info.t): list(TyDiSuggestion.t) => {
   let ctx = Info.ctx_of(ci);
   switch (ci) {
   | InfoExp({ana, _}) =>
-    let exp_refs = ty =>
+    let exp_refs = (ty: Typ.t) =>
       bound_variables(ty, ctx)
       @ bound_constructors(x => Exp(Common(x)), ty, ctx);
     let exp_aps = ty =>
@@ -182,14 +185,14 @@ let suggest_lookahead_variable = (ci: Info.t): list(TyDiSuggestion.t) => {
       @ List.map(restrategize(commas), exp_refs(ty));
     | Atom(Bool) =>
       /* TODO: Find a UI to make these less confusing */
-      exp_refs(Atom(Int) |> Typ.fresh)
-      @ exp_refs(Atom(SInt) |> Typ.fresh)
-      @ exp_refs(Atom(Nat) |> Typ.fresh)
-      @ exp_refs(Atom(Float) |> Typ.fresh)
-      @ exp_refs(Atom(String) |> Typ.fresh)
-      @ exp_aps(Atom(Int) |> Typ.fresh)
-      @ exp_aps(Atom(Float) |> Typ.fresh)
-      @ exp_aps(Atom(String) |> Typ.fresh)
+      exp_refs(Atom(Int) |> Typ.fresh_empty)
+      @ exp_refs(Atom(SInt) |> Typ.fresh_empty)
+      @ exp_refs(Atom(Nat) |> Typ.fresh_empty)
+      @ exp_refs(Atom(Float) |> Typ.fresh_empty)
+      @ exp_refs(Atom(String) |> Typ.fresh_empty)
+      @ exp_aps(Atom(Int) |> Typ.fresh_empty)
+      @ exp_aps(Atom(Float) |> Typ.fresh_empty)
+      @ exp_aps(Atom(String) |> Typ.fresh_empty)
     | _ => []
     };
   | InfoPat({ana, co_ctx, _}) =>

src/haz3lcore/TyDi/TyDiForms.re

@@ -10,25 +10,26 @@ let leading_expander = " ";
  * running Statics, but for now, new forms e.g. operators must be added
  * below manually.  */
 module Typ = {
-  let unk: Typ.t = Unknown(Internal) |> Typ.fresh;
+  let fresh_empty = Typ.fresh_empty;
+  let unk: Typ.t = Unknown(Internal) |> Typ.fresh_empty;
 
   let of_const_mono_delim: list((Token.t, Typ.t)) = [
-    ("true", Atom(Bool) |> Typ.fresh),
-    ("false", Atom(Bool) |> Typ.fresh),
+    ("true", Atom(Bool) |> Typ.fresh_empty),
+    ("false", Atom(Bool) |> Typ.fresh_empty),
     //("[]", 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 */
-    ("\"\"", Atom(String) |> Typ.fresh), /* NOTE: Irrelevent as second quote appears automatically */
+    ("\"\"", Atom(String) |> Typ.fresh_empty), /* NOTE: Irrelevent as second quote appears automatically */
     ("_", unk),
   ];
 
   /* Only need to add forms here if they have a non-trivial type */
   let of_leading_delim: list((Token.t, Typ.t)) = [
-    ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
+    ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh_empty),
     (
       "typfun" ++ leading_expander,
-      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh_empty,
     ),
-    ("test" ++ leading_expander, Prod([]) |> Typ.fresh),
+    ("test" ++ leading_expander, Prod([]) |> Typ.fresh_empty),
   ];
 
   let of_infix_delim: list((Token.t, Typ.term)) = [
@@ -71,7 +72,7 @@ module Typ = {
     fun
     | InfoExp({ana, _})
     | InfoPat({ana, _}) => ana
-    | _ => Unknown(Internal) |> Typ.fresh;
+    | _ => Unknown(Internal) |> Typ.fresh_empty;
 
   let filter_by =
       (
@@ -218,7 +219,7 @@ let suggest_operator: Info.t => list(TyDiSuggestion.t) =
       [] // Stop completing (a= to (a==
     | _ =>
       suggest_form(
-        List.map(((a, b)) => (a, IdTagged.fresh(b)), Typ.of_infix_delim),
+        List.map(((a, b)) => (a, Typ.fresh_empty(b)), Typ.of_infix_delim),
         Delims.infix,
         info,
       )

src/haz3lcore/lang/MakeTerm.re

@@ -140,9 +140,18 @@ let should_instrument = (id: Id.t): bool =>
 
 let parse_sum_term: Typ.t => ConstructorMap.variant(Typ.t) =
   fun
-  | {term: Var(ctr), annotation: {ids, _}} => Variant(ctr, ids, None)
+  | {term: {typ: Var(ctr), _}, annotation: {ids, _}} =>
+    Variant(ctr, ids, None)
   | {
-      term: Ap({term: Var(ctr), annotation: {ids: ids_ctr, _}}, u),
+      term:
+        {
+          typ:
+            Ap(
+              {term: {typ: Var(ctr), _}, annotation: {ids: ids_ctr, _}},
+              u,
+            ),
+          _,
+        },
       annotation: {ids: ids_ap, _},
     } =>
     Variant(ctr, ids_ctr @ ids_ap, Some(u))
@@ -153,11 +162,11 @@ let mk_bad = (ctr, ids, value) => {
     annotation: {
       ids: ids,
     },
-    term: Var(ctr),
+    term: Var(ctr) |> Typ.empty,
   };
   switch (value) {
   | None => t
-  | Some(u) => Ap(t, u) |> Typ.fresh
+  | Some(u) => Ap(t, u) |> Typ.fresh_empty
   };
 };
 
@@ -581,22 +590,22 @@ and pat_term: unsorted => (Pat.term, list(Id.t)) = {
     }
   | tm => ret(hole(tm));
 }
-and typ = unsorted => {
+and typ = (unsorted): Typ.t => {
   let (term, inner_ids) = typ_term(unsorted);
   let ids = ids(unsorted) @ inner_ids;
   let t =
     return(
       ty => Typ(ty),
       ids,
       {
-        term,
+        term: Typ.empty(term),
         annotation: {
           ids: ids,
         },
       },
     );
   switch (term) {
-  | TupLabel(_) => Prod([t]) |> Typ.fresh
+  | TupLabel(_) => Prod([t]) |> Typ.fresh_empty
   | _ => t
   };
 }
@@ -618,7 +627,7 @@ and typ_term: unsorted => (Typ.term, list(Id.t)) = {
         | (["Nat"], []) => Atom(Nat)
         | ([t], []) when Form.is_typ_var(t) => Var(t)
         | (["(", ")"], [Typ(body)]) => Parens(body)
-        | (label, [Typ(body)]) when is_probe_wrap(label) => body.term
+        | (label, [Typ(body)]) when is_probe_wrap(label) => body.term.typ
         | (["[", "]"], [Typ(body)]) => List(body)
         | ([t], []) when is_hole_label(t) => hole(tm)
         | ([t], []) => Unknown(Hole(Invalid(t)))
@@ -639,7 +648,7 @@ and typ_term: unsorted => (Typ.term, list(Id.t)) = {
     ret(Forall(tpat, t))
   | Pre(([(_id, (["rec", "->"], [TPat(tpat)]))], []), Typ(t)) =>
     ret(Rec(tpat, t))
-  | Pre(tiles, Typ({term: Sum(t0), annotation: {ids, _}})) as tm =>
+  | Pre(tiles, Typ({term: {typ: Sum(t0), _}, annotation: {ids, _}})) as tm =>
     /* Case for leading prefix + preceeding a sum */
     switch (tiles) {
     | ([(_, (["+"], []))], []) => (Sum(t0), ids)
@@ -671,7 +680,14 @@ and typ_term: unsorted => (Typ.term, list(Id.t)) = {
         @ [r]
         |> List.map((child: Typ.t) => {
              switch (child) {
-             | {term: Prod([{term: TupLabel(_), _} as tl]), _} => tl
+             | {
+                 term:
+                   {
+                     typ: Prod([{term: {typ: TupLabel(_), _}, _} as tl]),
+                     _,
+                   },
+                 _,
+               } => tl
              | _ => child
              }
            });
@@ -681,13 +697,13 @@ and typ_term: unsorted => (Typ.term, list(Id.t)) = {
       switch (tiles) {
       | ([(_id, (["->"], []))], []) => ret(Arrow(l, r))
       | ([(_id, (["="], []))], []) =>
-        switch (l.term) {
+        switch (l.term.typ) {
         | Var(name) =>
           ret(
             TupLabel(
               {
                 annotation: l.annotation,
-                term: Label(name),
+                term: Typ.empty(Label(name)),
               },
               r,
             ),
@@ -864,7 +880,7 @@ let for_projection =
           }
         | Typ =>
           switch (typ(unsorted)) {
-          | {term: Prod(_), _} => None
+          | {term: {typ: Prod(_), _}, _} => None
           | _ => Some(Typ(typ(unsorted)))
           }
         | TPat =>

src/haz3lcore/pretty/ExpToSegment.re

@@ -153,6 +153,10 @@ let external_precedence_typ = (tp: Typ.t) =>
   | Unknown(Hole(MultiHole(_))) => Precedence.min
   };
 
+let external_precedence_Typ = (s: Typ.t) => {
+  s |> external_precedence_typ;
+};
+
 let paren_at = (internal_precedence: Precedence.t, exp: Exp.t): Exp.t =>
   external_precedence(exp) >= internal_precedence
     ? Exp.fresh(Parens(exp)) : exp;
@@ -172,12 +176,21 @@ let paren_pat_assoc_at =
 
 let paren_typ_at = (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
   external_precedence_typ(typ) >= internal_precedence
-    ? Typ.fresh(Parens(typ)) : typ;
+    ? Typ.fresh_empty(Parens(typ)) : typ;
 
 let paren_typ_assoc_at =
     (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
   external_precedence_typ(typ) > internal_precedence
-    ? Typ.fresh(Parens(typ)) : typ;
+    ? Typ.fresh_empty(Parens(typ)) : typ;
+
+let paren_Typ_at = (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
+  external_precedence_Typ(typ) >= internal_precedence
+    ? Typ.fresh_empty(Parens(typ)) : typ;
+
+let paren_Typ_assoc_at =
+    (internal_precedence: Precedence.t, typ: Typ.t): Typ.t =>
+  external_precedence_Typ(typ) > internal_precedence
+    ? Typ.fresh_empty(Parens(typ)) : typ;
 
 let rec parenthesize =
         (~show_filters: bool, ~already_paren=false, exp: Exp.t): Exp.t => {
@@ -459,10 +472,13 @@ and parenthesize_pat =
 }
 
 and parenthesize_typ =
-    (~show_filters: bool, ~already_paren=false, typ: Typ.t): Typ.t => {
+    (~show_filters: bool, ~already_paren=false): (Typ.t => Typ.t) => {
+  Typ.map(parenthesize_typ_term(~show_filters, ~already_paren));
+}
+and parenthesize_typ_term =
+    (~show_filters: bool, ~already_paren=false, typ: Typ.term): Typ.term => {
   let parenthesize_typ = parenthesize_typ(~show_filters);
-  let (term, rewrap) = Typ.unwrap(typ);
-  switch (term) {
+  switch (typ) {
   // Indivisible forms dont' change
   | Var(_)
   | Unknown(Hole(Invalid(_)))
@@ -477,47 +493,40 @@ and parenthesize_typ =
       parenthesize_typ(~already_paren=true, t)
       |> paren_typ_at(Precedence.min),
     )
-    |> rewrap
-  | List(t) =>
-    List(parenthesize_typ(t) |> paren_typ_at(Precedence.min)) |> rewrap
+
+  | List(t) => List(parenthesize_typ(t) |> paren_typ_at(Precedence.min))
   | Prod([]) => typ
   | Prod(ts) =>
-    let inner =
+    let inner: Typ.term =
       Prod(
         ts
         |> List.map(parenthesize_typ)
         |> List.map(paren_typ_at(Precedence.comma)),
-      )
-      |> rewrap;
-    already_paren ? inner : Parens(inner) |> Typ.fresh;
+      );
+    already_paren ? inner : Parens(inner |> Typ.fresh_empty);
   | Label(_) => typ
   | TupLabel(l, t) =>
     TupLabel(l, parenthesize_typ(t) |> paren_typ_at(Precedence.min))
-    |> rewrap
   | Ap(t1, t2) =>
     Ap(
       parenthesize_typ(t1) |> paren_typ_assoc_at(Precedence.type_sum_ap),
       parenthesize_typ(t2) |> paren_typ_at(Precedence.min),
     )
-    |> rewrap
   | Rec(tp, t) =>
     Rec(
       tp,
       parenthesize_typ(t) |> paren_typ_assoc_at(Precedence.type_binder),
     )
-    |> rewrap
   | Forall(tp, t) =>
     Forall(
       tp,
       parenthesize_typ(t) |> paren_typ_assoc_at(Precedence.type_binder),
     )
-    |> rewrap
   | Arrow(t1, t2) =>
     Arrow(
       parenthesize_typ(t1) |> paren_typ_at(Precedence.type_arrow),
       parenthesize_typ(t2) |> paren_typ_assoc_at(Precedence.type_arrow),
     )
-    |> rewrap
   | Sum(ts) =>
     Sum(
       ConstructorMap.map(
@@ -528,12 +537,10 @@ and parenthesize_typ =
         ts,
       ),
     )
-    |> rewrap
   | Unknown(Hole(MultiHole(xs))) =>
     Unknown(
       Hole(MultiHole(List.map(parenthesize_any(~show_filters), xs))),
     )
-    |> rewrap
   };
 }