summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/interpreter.ml2
-rw-r--r--test/c/empty_list.expect5
-rw-r--r--test/c/empty_list.sail21
3 files changed, 27 insertions, 1 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml
index b0faabce..fb798b65 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -748,7 +748,7 @@ and pattern_match env (P_aux (p_aux, (l, _)) as pat) value =
let hd_match, hd_bind = pattern_match env hd_pat hd_value in
let tl_match, tl_bind = pattern_match env tl_pat (V_list tl_values) in
hd_match && tl_match, Bindings.merge combine hd_bind tl_bind
- | None -> failwith "Cannot match cons pattern against non-list"
+ | None -> false, Bindings.empty
end
| P_string_append _ -> assert false (* TODO *)
diff --git a/test/c/empty_list.expect b/test/c/empty_list.expect
new file mode 100644
index 00000000..e9c361a4
--- /dev/null
+++ b/test/c/empty_list.expect
@@ -0,0 +1,5 @@
+end
+.
+.
+.
+end
diff --git a/test/c/empty_list.sail b/test/c/empty_list.sail
new file mode 100644
index 00000000..a6ce0a91
--- /dev/null
+++ b/test/c/empty_list.sail
@@ -0,0 +1,21 @@
+default Order dec
+$include <prelude.sail>
+$include <string.sail>
+
+val list_test : list(int) -> unit
+
+function list_test(xs) =
+ match xs {
+ x :: xs => {
+ print_endline(".");
+ list_test(xs)
+ },
+ [||] => print_endline("end")
+ }
+
+val main : unit -> unit
+
+function main() = {
+ list_test([||]);
+ list_test([|1, 2, 3|])
+}