Fix #1510 (while maintaining performance)

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),
@@ -241,6 +250,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/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)
+  };