updates after Andrew's review + removed Fresh modules

src/haz3lcore/dynamics/TypeAssignment.re

@@ -77,13 +77,10 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) =>
         List.map(dhp => {dhpat_var_entry(dhp, t)}, l) |> OptUtil.sequence;
       Some(List.concat(l));
     | Ap({term: Constructor(name, _), _}, dhp) =>
-      // TODO: make this stricter
       let* ctrs = Typ.get_sum_constructors(ctx, ty);
       let* typ = ConstructorMap.get_entry(name, ctrs);
-      switch (typ) {
-      | None => None
-      | Some(typ) => dhpat_var_entry(dhp, typ)
-      };
+      let* typ' = typ;
+      dhpat_var_entry(dhp, typ');
     | Ap(_) => None
     | EmptyHole
     | Wild

src/haz3lcore/lang/term/TPat.re

@@ -11,25 +11,6 @@ let rep_id: t => Id.t = IdTagged.rep_id;
 
 let fresh: term => t = IdTagged.fresh;
 
-module Fresh = {
-  open TermBase;
-  let tpinvalid = s => Invalid(s) |> fresh;
-  let tpempty_hole = () => EmptyHole |> fresh;
-  let tpmulti_hole = tms => MultiHole(tms) |> fresh;
-  let tpvar = x => Var(x) |> fresh;
-
-  // The following function exists only as a reminder to update the above when a new constructor is added.
-  let ok = (_: 'a) => failwith("covered should never be called");
-  let covered = (e: tpat_term) => {
-    switch (e) {
-    | Invalid(_) => ok(tpinvalid)
-    | EmptyHole => ok(tpempty_hole)
-    | MultiHole(_) => ok(tpmulti_hole)
-    | Var(_) => ok(tpvar)
-    };
-  };
-};
-
 let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term =>
   switch (tms) {
   | [] => EmptyHole

src/haz3lcore/lang/term/Typ.re

@@ -37,52 +37,6 @@ let fresh: term => t = IdTagged.fresh;
    shortly after, it makes sense to use it. */
 let temp: term => t = term => {term, ids: [Id.invalid], copied: false};
 
-module Fresh = {
-  open TermBase;
-  let tunknown = (p: type_provenance) => Unknown(p) |> fresh;
-  let tint = () => Int |> fresh;
-  let tfloat = () => Float |> fresh;
-  let tbool = () => Bool |> fresh;
-  let tstring = () => String |> fresh;
-  let tvar = x => Var(x) |> fresh;
-  let tlist = t => List(t) |> fresh;
-  let tarrow = (t1, t2) => Arrow(t1, t2) |> fresh;
-  let tsum = ctrs => Sum(ctrs) |> fresh;
-  let tprod = ts => Prod(ts) |> fresh;
-  let tparens = t => Parens(t) |> fresh;
-  let tap = (t1, t2) => Ap(t1, t2) |> fresh;
-  let trec = (tp, t) => Rec(tp, t) |> fresh;
-  let tforall = (tp, t) => Forall(tp, t) |> fresh;
-  let tlabel = l => Label(l) |> fresh;
-  let ttup_label = (l, t) => TupLabel(l, t) |> fresh;
-
-  let tvariant = (ctr, arg: option(Typ.t)) =>
-    ConstructorMap.Variant(ctr, [Id.mk()], arg);
-
-  // The following function exists only as a reminder to update the above when a new constructor is added.
-  let ok = (_: 'a) => failwith("covered should never be called");
-  let covered = (e: typ_term) => {
-    switch (e) {
-    | Unknown(_) => ok(tunknown)
-    | Int => ok(tint)
-    | Float => ok(tfloat)
-    | Bool => ok(tbool)
-    | String => ok(tstring)
-    | Var(_) => ok(tvar)
-    | List(_) => ok(tlist)
-    | Arrow(_, _) => ok(tarrow)
-    | Sum(_) => ok(tsum)
-    | Prod(_) => ok(tprod)
-    | Parens(_) => ok(tparens)
-    | Ap(_, _) => ok(tap)
-    | Rec(_, _) => ok(trec)
-    | Forall(_, _) => ok(tforall)
-    | Label(_) => ok(tlabel)
-    | TupLabel(_, _) => ok(ttup_label)
-    };
-  };
-};
-
 let all_ids_temp = {
   let f:
     'a.

src/haz3lcore/statics/ConstructorMap.re

@@ -199,6 +199,7 @@ let map = (f: option('a) => option('b), m: t('a)): t('b) => {
   );
 };
 
+// TODO: maybe define a variant here instead of double option
 let get_entry = (ctr, m) =>
   List.find_map(
     fun

src/haz3lcore/statics/Coverage.re

@@ -77,12 +77,12 @@ module Ctr = {
 
   let arity_of = (ctr, all_ctrs: all_ctrs): arity =>
     switch (all_ctrs) {
-    | Unknown => List.init(ctr.num_args, _ => Typ.Fresh.tunknown(Internal))
-    | Infinite => List.init(ctr.num_args, _ => Typ.Fresh.tunknown(Internal))
+    | Unknown => List.init(ctr.num_args, _ => Unknown(Internal) |> Typ.temp)
+    | Infinite => List.init(ctr.num_args, _ => Unknown(Internal) |> Typ.temp)
     | Finite(all_ctrs) =>
       switch (Map.find_opt(ctr, all_ctrs)) {
       | Some(arity) => arity
-      | None => List.init(ctr.num_args, _ => Typ.Fresh.tunknown(Internal))
+      | None => List.init(ctr.num_args, _ => Unknown(Internal) |> Typ.temp)
       }
     };
 
@@ -109,12 +109,12 @@ module Ctr = {
       Finite(
         Map.of_list([
           (nil_ctr, []),
-          (cons_ctr, [Typ.Fresh.tprod([elt_ty, ty])]),
+          (cons_ctr, [Prod([elt_ty, ty]) |> Typ.temp]),
         ]),
       )
     | Bool => Finite(Map.of_list([(true_ctr, []), (false_ctr, [])]))
     | Unknown(_) => Unknown
-    | Int
+    | Int // technically int and float are finite, but ya know
     | Float
     | String
     | Arrow(_)
@@ -146,7 +146,7 @@ type redundant_rows = list(int);
 module Matrix = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type row = {
-    idx: int,
+    idx: int, // retaining row index from original matrix when constructing submatrices
     cols: list(Constraint.t),
   };
 

src/haz3lcore/statics/Info.re

@@ -666,20 +666,6 @@ let is_error = (ci: t): bool => {
   };
 };
 
-let error = (ci: t): option(error) => {
-  switch (ci) {
-  | InfoExp({status: InHole(err), _}) => Some(Exp(err))
-  | InfoPat({status: InHole(err), _}) => Some(Pat(err))
-  | InfoTyp({status: InHole(err), _}) => Some(Typ(err))
-  | InfoTPat({status: InHole(err), _}) => Some(TPat(err))
-  | InfoExp({status: NotInHole(_), _}) => None
-  | InfoPat({status: NotInHole(_), _}) => None
-  | InfoTyp({status: NotInHole(_), _}) => None
-  | InfoTPat({status: NotInHole(_), _}) => None
-  | Secondary(_) => None
-  };
-};
-
 /* Determined the type of an expression or pattern 'after hole fixing';
    that is, some ill-typed terms are considered to be 'wrapped in
    non-empty holes', i.e. assigned Unknown type. */
@@ -738,24 +724,6 @@ let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t => {
   };
 };
 
-// let fixed_constraint_pat =
-//     (
-//       upat: Pat.t,
-//       ctx,
-//       mode: Mode.t,
-//       self: Self.pat,
-//       constraint_: Coverage.Constraint.t,
-//     )
-//     : Coverage.Constraint.t =>
-//   switch (upat.term) {
-//   | Cast(_) => constraint_
-//   | _ =>
-//     switch (fixed_typ_pat(ctx, mode, self) |> Typ.term_of) {
-//     | Unknown(_) => Constraint.Hole
-//     | _ => constraint_
-//     }
-//   };
-
 let fixed_typ_exp = (ctx, mode: Mode.t, self: Self.exp): Typ.t =>
   switch (status_exp(ctx, mode, self)) {
   | InHole(err) => fixed_typ_err(err)
@@ -814,7 +782,6 @@ let derived_pat =
     : pat => {
   let cls = Cls.Pat(Pat.cls_of_term(upat.term));
   let status = status_pat(ctx, mode, self);
-  // print_endline("Status: " ++ show_status_pat(status));
   let ty = fixed_typ_pat(ctx, mode, self);
   {
     cls,

src/haz3lcore/statics/Self.re

@@ -121,6 +121,7 @@ let of_exp_var = (ctx: Ctx.t, name: Var.t): exp =>
 
 let of_ctr =
     (ctx: Ctx.t, name: Constructor.t, mode: Mode.t, ty: option(Typ.t)): t =>
+  // this has gotten a bit complex, depends on mode
   IsConstructor({
     name,
     syn_ty:

src/haz3lcore/statics/Term.re

@@ -33,53 +33,6 @@ module Pat = {
 
   let fresh: term => t = IdTagged.fresh;
 
-  module Fresh = {
-    open TermBase;
-    let pinvalid = s => Invalid(s) |> fresh;
-    let pempty_hole = () => EmptyHole |> fresh;
-    let pmulti_hole = tms => MultiHole(tms) |> fresh;
-    let pwild = () => Wild |> fresh;
-    let pint = i => Int(i) |> fresh;
-    let pfloat = f => Float(f) |> fresh;
-    let pbool = b => Bool(b) |> fresh;
-    let pstring = s => String(s) |> fresh;
-    let plist_lit = ts => ListLit(ts) |> fresh;
-    let pconstructor = (c, ty) => Constructor(c, ty) |> fresh;
-    let pcons = (hd, tl) => Cons(hd, tl) |> fresh;
-    let pvar = x => Var(x) |> fresh;
-    let ptuple = ps => Tuple(ps) |> fresh;
-    let pparens = p => Parens(p) |> fresh;
-    let pap = (f, x) => Ap(f, x) |> fresh;
-    let pcast = (e, t1, t2) => Cast(e, t1, t2) |> fresh;
-    let pasc = (e, t) => pcast(e, t, Unknown(Internal) |> IdTagged.fresh);
-    let plabel = l => Label(l) |> fresh;
-    let ptup_label = (l, p) => TupLabel(l, p) |> fresh;
-    // The following function exists only as a reminder to update the above when a new constructor is added.
-    let ok = (_: 'a) => failwith("covered should never be called");
-    let covered = (e: pat_term) => {
-      switch (e) {
-      | Invalid(_) => ok(pinvalid)
-      | EmptyHole => ok(pempty_hole)
-      | MultiHole(_) => ok(pmulti_hole)
-      | Wild => ok(pwild)
-      | Int(_) => ok(pint)
-      | Float(_) => ok(pfloat)
-      | Bool(_) => ok(pbool)
-      | String(_) => ok(pstring)
-      | ListLit(_) => ok(plist_lit)
-      | Constructor(_, _) => ok(pconstructor)
-      | Cons(_, _) => ok(pcons)
-      | Var(_) => ok(pvar)
-      | Tuple(_) => ok(ptuple)
-      | Parens(_) => ok(pparens)
-      | Ap(_, _) => ok(pap)
-      | Cast(_, _, _) => ok(pcast)
-      | Label(_) => ok(plabel)
-      | TupLabel(_, _) => ok(ptup_label)
-      };
-    };
-  };
-
   let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term =>
     switch (tms) {
     | [] => EmptyHole
@@ -430,95 +383,6 @@ module Exp = {
   let temp: term => t = term => {term, ids: [Id.invalid], copied: false};
   let fresh: term => t = IdTagged.fresh;
 
-  module Fresh = {
-    open TermBase;
-    let invalid = s => Invalid(s) |> fresh;
-    let empty_hole = () => EmptyHole |> fresh;
-    let multi_hole = tms => MultiHole(tms) |> fresh;
-    let dynamic_error_hole = (e, err) => DynamicErrorHole(e, err) |> fresh;
-    let failed_cast = (e, ty1, ty2) => FailedCast(e, ty1, ty2) |> fresh;
-    let deferral = position => Deferral(position) |> fresh;
-    let undefined = () => Undefined |> fresh;
-    let bool = b => Bool(b) |> fresh;
-    let int = i => Int(i) |> fresh;
-    let float = f => Float(f) |> fresh;
-    let string = s => String(s) |> fresh;
-    let list_lit = es => ListLit(es) |> fresh;
-    let constructor = (s, ty) => Constructor(s, ty) |> fresh;
-    let fun_ = (p, e, ty, v) => Fun(p, e, ty, v) |> fresh;
-    let typ_fun = (p, e, x) => TypFun(p, e, x) |> fresh;
-    let tuple = es => Tuple(es) |> fresh;
-    let var = s => Var(s) |> fresh;
-    let let_ = (p, e, b) => Let(p, e, b) |> fresh;
-    let fix_f = (f, x, e) => FixF(f, x, e) |> fresh;
-    let ty_alias = (p, ty, e) => TyAlias(p, ty, e) |> fresh;
-    let ap = (d, f, x) => Ap(d, f, x) |> fresh;
-    let typ_ap = (f, x) => TypAp(f, x) |> fresh;
-    let deferred_ap = (f, x) => DeferredAp(f, x) |> fresh;
-    let if_ = (c, t, e) => If(c, t, e) |> fresh;
-    let seq = (e1, e2) => Seq(e1, e2) |> fresh;
-    let test = e => Test(e) |> fresh;
-    let filter = (k, e) => Filter(k, e) |> fresh;
-    let closure = (env, e) => Closure(env, e) |> fresh;
-    let parens = e => Parens(e) |> fresh;
-    let cons = (h, t) => Cons(h, t) |> fresh;
-    let list_concat = (e1, e2) => ListConcat(e1, e2) |> fresh;
-    let un_op = (op, e) => UnOp(op, e) |> fresh;
-    let bin_op = (op, e1, e2) => BinOp(op, e1, e2) |> fresh;
-    let builtin_fun = s => BuiltinFun(s) |> fresh;
-    let match_ = (e, bs) => Match(e, bs) |> fresh;
-    let cast = (e, t1, t2) => Cast(e, t1, t2) |> fresh;
-    let label = s => Label(s) |> fresh;
-    let tup_label = (l, e) => TupLabel(l, e) |> fresh;
-    let dot = (e1, e2) => Dot(e1, e2) |> fresh;
-
-    // The following function exists only as a reminder to update the above when a new constructor is added.
-    let ok = (_: 'a) => failwith("covered should never be called");
-    let covered = (e: exp_term) => {
-      switch (e) {
-      | Invalid(_) => ok(invalid)
-      | EmptyHole => ok(empty_hole)
-      | MultiHole(_) => ok(multi_hole)
-      | DynamicErrorHole(_, _) => ok(dynamic_error_hole)
-      | FailedCast(_, _, _) => ok(failed_cast)
-      | Deferral(_) => ok(deferral)
-      | Undefined => ok(undefined)
-      | Bool(_) => ok(bool)
-      | Int(_) => ok(int)
-      | Float(_) => ok(float)
-      | String(_) => ok(string)
-      | ListLit(_) => ok(list_lit)
-      | Constructor(_, _) => ok(constructor)
-      | Fun(_, _, _, _) => ok(fun_)
-      | TypFun(_, _, _) => ok(typ_fun)
-      | Tuple(_) => ok(tuple)
-      | Var(_) => ok(var)
-      | Let(_, _, _) => ok(let_)
-      | FixF(_, _, _) => ok(fix_f)
-      | TyAlias(_, _, _) => ok(ty_alias)
-      | Ap(_, _, _) => ok(ap)
-      | TypAp(_, _) => ok(typ_ap)
-      | DeferredAp(_, _) => ok(deferred_ap)
-      | If(_, _, _) => ok(if_)
-      | Seq(_, _) => ok(seq)
-      | Test(_) => ok(test)
-      | Filter(_, _) => ok(filter)
-      | Closure(_, _) => ok(closure)
-      | Parens(_) => ok(parens)
-      | Cons(_, _) => ok(cons)
-      | ListConcat(_, _) => ok(list_concat)
-      | UnOp(_, _) => ok(un_op)
-      | BinOp(_, _, _) => ok(bin_op)
-      | BuiltinFun(_) => ok(builtin_fun)
-      | Match(_, _) => ok(match_)
-      | Cast(_, _, _) => ok(cast)
-      | Label(_) => ok(label)
-      | TupLabel(_, _) => ok(tup_label)
-      | Dot(_, _) => ok(dot)
-      };
-    };
-  };
-
   let hole = (tms: list(TermBase.Any.t)): term =>
     switch (tms) {
     | [] => EmptyHole
@@ -1073,10 +937,3 @@ module Any = {
     | Rul(tm) => Rul.rep_id(~any_ids=ids, tm)
     | Any () => raise(Invalid_argument("Term.rep_id"));
 };
-
-module Fresh = {
-  include TPat.Fresh;
-  include Pat.Fresh;
-  include Typ.Fresh;
-  include Exp.Fresh;
-};