Unboxing fixes

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),
@@ -195,6 +204,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
@@ -241,6 +252,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, t) |> rewrap |> cast_from(t);
@@ -333,7 +338,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.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
+        | _ =>
+          Sum([
+            ConstructorMap.Variant(c, [Id.invalid], None),
+            ConstructorMap.BadEntry(Unknown(Internal) |> Typ.temp),
+          ])
+          |> Typ.temp
         };
       let t = t |> Typ.normalize(ctx) |> Typ.all_ids_temp;
       Constructor(c, t) |> rewrap |> cast_from(t);

src/haz3lcore/statics/Info.re

@@ -676,7 +676,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/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

@@ -995,16 +995,6 @@ module MenhirElaborationTests = {
       failed_cast_uexp,
     );
 
-  let constructor_str = "X";
-  let constructor_uexp: Exp.t =
-    Constructor("X", Unknown(Internal) |> Typ.fresh) |> Exp.fresh;
-  let constructor_menhir = () =>
-    alco_check_menhir(
-      "Constructor test (menhir)",
-      constructor_str,
-      constructor_uexp,
-    );
-
   /*
    <<1 / 2 ? `a`>>
        */
@@ -1172,7 +1162,6 @@ 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("Type ap test (menhir)", `Quick, typ_ap_menhir),
     test_case("Let expression for a tuple (menhir)", `Quick, let_exp_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", 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",