summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair2020-11-01 15:00:11 +0000
committerAlasdair2020-11-01 15:01:05 +0000
commit12edcd22c20f480ca73bcfdfb08477fb0480657d (patch)
tree1dc46bb7708edfa3c377c55b145facfa2fabb7d6
parent29137641777155badb5863fd38ecb422e23cd1ca (diff)
Fix interpreter pattern matching bug
-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|])
+}