merge with dev + fix bug with constructor elaboration

src/haz3lcore/dynamics/PatternMatch.re

@@ -29,15 +29,10 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
   | String(s) =>
     let* s' = Unboxing.unbox(String, d);
     s == s' ? Matches(Environment.empty) : DoesNotMatch;
-  | Cast({term: ListLit([] as xs), _}, _, _) // Shortcut for empty list pattern match perf
   | ListLit(xs) =>
-    let* s' = Unboxing.unbox(List, d);
-    if (List.length(xs) == List.length(s')) {
-      List.map2(matches, xs, s')
-      |> List.fold_left(combine_result, Matches(Environment.empty));
-    } else {
-      DoesNotMatch;
-    };
+    let* s' = Unboxing.unbox(ListLit(List.length(xs)), d);
+    List.map2(matches, xs, s')
+    |> List.fold_left(combine_result, Matches(Environment.empty));
   | Cons(x, xs) =>
     let* (x', xs') = Unboxing.unbox(Cons, d);
     let* m_x = matches(x, x');

src/haz3lcore/dynamics/Unboxing.re

@@ -35,6 +35,7 @@ type unbox_request('a) =
   | Tuple(int): unbox_request(list(DHExp.t))
   | TupLabel(DHPat.t): unbox_request(DHExp.t)
   | List: unbox_request(list(DHExp.t))
+  | ListLit(int): unbox_request(list(DHExp.t)) // This request is used for performance reasons to prevent casting lists of the wrong length
   | Cons: unbox_request((DHExp.t, DHExp.t))
   | SumNoArg(string): unbox_request(unit)
   | SumWithArg(string): unbox_request(DHExp.t)
@@ -104,14 +105,22 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
 
     /* Lists can be either lists or list casts */
     | (List, ListLit(l)) => Matches(l)
+    | (ListLit(n), ListLit(l)) when ListUtil.is_length(n, l) => Matches(l)
+    | (ListLit(_), ListLit(_)) => DoesNotMatch
     | (Cons, ListLit([x, ...xs])) =>
       Matches((x, ListLit(xs) |> DHExp.fresh))
     | (Cons, ListLit([])) => DoesNotMatch
+
     | (List, Cast(l, {term: List(t1), _}, {term: List(t2), _})) =>
       let* l = unbox(List, l);
       let l = List.map(d => Cast(d, t1, t2) |> DHExp.fresh, l);
       let l = List.map(fixup_cast, l);
       Matches(l);
+    | (ListLit(n), Cast(l, {term: List(t1), _}, {term: List(t2), _})) =>
+      let* l = unbox(ListLit(n), l);
+      let l = List.map(d => Cast(d, t1, t2) |> DHExp.fresh, l);
+      let l = List.map(fixup_cast, l);
+      Matches(l);
     | (
         Cons,
         Cast(l, {term: List(t1), _} as ct1, {term: List(t2), _} as ct2),
@@ -196,6 +205,8 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
     | (Fun, DeferredAp(d1, ds)) => Matches(DeferredAp(d1, ds))
 
     /* TypFun-like things can look like the following when values */
+    | (TypFun, Closure(env', {term: TypFun(utpat, tfbody, name), _})) =>
+      Matches(TypFun(utpat, Closure(env', tfbody) |> Exp.fresh, name))
     | (TypFun, TypFun(utpat, tfbody, name)) =>
       Matches(TypFun(utpat, tfbody, name))
     // Note: We might be able to handle this cast like other casts
@@ -242,6 +253,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
       | Label => raise(EvaluatorError.Exception(InvalidBoxedLabel(expr)))
       | Tuple(_) => raise(EvaluatorError.Exception(InvalidBoxedTuple(expr)))
       | List
+      | ListLit(_)
       | Cons => raise(EvaluatorError.Exception(InvalidBoxedListLit(expr)))
       | SumNoArg(_)
       | SumWithArg(_) =>

src/haz3lcore/statics/Elaborator.re

@@ -242,7 +242,12 @@ let rec elaborate_pattern =
         switch (Mode.ctr_ana_typ(ctx, mode, c), Ctx.lookup_ctr(ctx, c)) {
         | (Some(ana_ty), _) => ana_ty
         | (_, Some({typ: syn_ty, _})) => syn_ty
-        | _ => Unknown(Internal) |> Typ.temp
+        | _ =>
+          Sum([
+            ConstructorMap.Variant(c, [Id.invalid], None),
+            ConstructorMap.BadEntry(Unknown(Internal) |> Typ.temp),
+          ])
+          |> Typ.temp
         };
       let t = t |> Typ.normalize(ctx);
       Constructor(c, Some(t)) |> rewrap |> cast_from(t);
@@ -331,12 +336,14 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
         };
       let t =
         switch (Mode.ctr_ana_typ(ctx, mode, c), Ctx.lookup_ctr(ctx, c)) {
-        | (Some(ana_ty), _) => ana_ty
-        | (_, Some({typ: syn_ty, _})) => syn_ty
-        | _ => Unknown(Internal) |> Typ.temp
+        | (Some(ana_ty), _) => Some(Typ.normalize(ctx, ana_ty))
+        | (_, Some({typ: syn_ty, _})) => Some(Typ.normalize(ctx, syn_ty))
+        | _ => None
         };
-      let t = t |> Typ.normalize(ctx) |> Typ.all_ids_temp;
-      Constructor(c, Some(t)) |> rewrap |> cast_from(t);
+      switch (t) {
+      | Some(ty) => Constructor(c, t) |> rewrap |> cast_from(ty)
+      | None => Constructor(c, t) |> rewrap
+      };
     | Fun(p, e, _, n) =>
       let (p', typ) = elaborate_pattern(m, p, false);
       let (e', tye) = elaborate(m, e);

src/haz3lcore/statics/Info.re

@@ -691,7 +691,18 @@ let fixed_typ_ok: ok_pat => Typ.t =
 
 let fixed_typ_err_common: error_common => Typ.t =
   fun
-  | NoType(_) => Unknown(Internal) |> Typ.temp
+  | NoType(FreeConstructor(c)) =>
+    Sum([
+      ConstructorMap.Variant(c, [Id.invalid], None),
+      ConstructorMap.BadEntry(Unknown(Internal) |> Typ.temp),
+    ])
+    |> Typ.temp
+  | NoType(BadToken(_))
+  | NoType(BadTrivAp(_))
+  | NoType(WantTuple)
+  | NoType(LabelNotFound(_))
+  | NoType(BadLabel(_))
+  | NoType(InvalidLabel(_)) => Unknown(Internal) |> Typ.temp
   | TupleLabelError({typ, _})
   | DuplicateLabel(_, typ) => typ
   | Inconsistent(Expectation({ana, _})) => ana

src/haz3lcore/statics/Mode.re

@@ -146,17 +146,6 @@ let ctr_ana_typ = (ctx: Ctx.t, mode: t, ctr: Constructor.t): option(Typ.t) => {
     | None => ty_ana
     | Some(ty_in) => Arrow(ty_in, ty_ana) |> Typ.temp
     };
-  /* let ty_ana =
-       switch (Typ.matched_arrow_strict(ctx, ty_ana)) {
-       | Some((_, ty_ana)) => ty_ana
-       | None => ty_ana
-       };
-     let+ ctrs = Typ.get_sum_constructors(ctx, ty_ana);
-     let ty_entry = ConstructorMap.get_entry(ctr, ctrs);
-     switch (ty_entry) {
-     | None => ty_ana
-     | Some(ty_in) => Arrow(ty_in, ty_ana) |> Typ.temp
-     }; */
   | _ => None
   };
 };

src/util/JsUtil.re

@@ -3,16 +3,24 @@ open Virtual_dom.Vdom;
 
 let get_elem_by_id = id => {
   let doc = Dom_html.document;
-  Js.Opt.get(doc##getElementById(Js.string(id)), () => {
-    failwith("Could not find element by ID: " ++ id)
-  });
+  Js.Opt.get(
+    doc##getElementById(Js.string(id)),
+    () => {
+      print_endline("Could not find element by ID: " ++ id);
+      assert(false);
+    },
+  );
 };
 
 let get_elem_by_selector = selector => {
   let doc = Dom_html.document;
-  Js.Opt.get(doc##querySelector(Js.string(selector)), () => {
-    failwith("Selector could not be found: " ++ selector)
-  });
+  Js.Opt.get(
+    doc##querySelector(Js.string(selector)),
+    () => {
+      print_endline("Selector could not be found: " ++ selector);
+      assert(false);
+    },
+  );
 };
 
 let get_child_with_class = (element: Js.t(Dom_html.element), className) => {

src/util/ListUtil.re

@@ -591,3 +591,12 @@ let minimum = (f: 'a => int, xs: list('a)): option('a) =>
       };
     loop(x, f(x), xs);
   };
+
+// for performance, doesn't check the whole list if already above length
+let rec is_length = (n: int, xs: list('a)): bool =>
+  switch (xs) {
+  | [] when n == 0 => true
+  | _ when n <= 0 => false
+  | [] => false
+  | [_, ...xs] => is_length(n - 1, xs)
+  };

test/Test_Elaboration.re

@@ -994,7 +994,7 @@ module MenhirElaborationTests = {
       failed_cast_uexp,
     );
 
-  let constructor_str = "X ~ ?";
+  let constructor_str = "X";
   let constructor_uexp: Exp.t = Constructor("X", None) |> Exp.fresh;
   let constructor_menhir = () =>
     alco_check_menhir(
@@ -1170,8 +1170,8 @@ x
       `Quick,
       dynamic_error_hole_menhir,
     ),
-    test_case("Constructor test (menhir)", `Quick, constructor_menhir),
     test_case("Failed cast test (menhir)", `Quick, failed_cast_menhir),
+    test_case("Constructor test (menhir)", `Quick, constructor_menhir),
     test_case("Type ap test (menhir)", `Quick, typ_ap_menhir),
     test_case("Let expression for a tuple (menhir)", `Quick, let_exp_menhir),
     test_case("Single integer (menhir)", `Quick, single_integer_menhir),

test/Test_Evaluator.re

@@ -290,6 +290,44 @@ let test_unevaluated_if = () =>
     |> Exp.fresh,
   );
 
+let test_invalid_constructor_match = () => {
+  let invalid_constructor_match =
+    Let(
+      Constructor("T", Some(Unknown(Internal) |> Typ.fresh)) |> Pat.fresh,
+      Int(1) |> Exp.fresh,
+      EmptyHole |> Exp.fresh,
+    )
+    |> Exp.fresh
+    |> elaborate;
+  evaluation_test(
+    "let T = 1 in ?",
+    invalid_constructor_match,
+    invalid_constructor_match,
+  );
+};
+
+let test_typfun_application = () =>
+  evaluation_test(
+    "(typfun T -> fun x -> 1)@<Int>(2)",
+    Int(1) |> Exp.fresh,
+    Ap(
+      Forward,
+      TypAp(
+        TypFun(
+          Var("T") |> TPat.fresh,
+          Fun(Var("x") |> Pat.fresh, Int(1) |> Exp.fresh, None, None)
+          |> Exp.fresh,
+          None,
+        )
+        |> Exp.fresh,
+        Int |> Typ.fresh,
+      )
+      |> Exp.fresh,
+      Int(2) |> Exp.fresh,
+    )
+    |> Exp.fresh,
+  );
+
 let tests = (
   "Evaluator",
   [
@@ -340,6 +378,12 @@ in fn("hello")|},
     test_case("Variable capture", `Quick, test_variable_capture),
     test_case("Unbound lookup", `Quick, test_unbound_lookup),
     test_case("Unevaluated if closure", `Quick, test_unevaluated_if),
+    test_case(
+      "Invalid constructor match",
+      `Quick,
+      test_invalid_constructor_match,
+    ),
+    test_case("Typfun application", `Quick, test_typfun_application),
     test_case("Negative integer literal", `Quick, () =>
       evaluation_test(
         "-8",