Merge branch 'mappings' into sail2

2 files changed, 10 insertions, 13 deletions

diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index 05c7bc9e..cf64b577 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -3,6 +3,13 @@ default Order dec
 $include <prelude.sail>
 
 val eq_string = "eq_string" : (string, string) -> bool
+val string_startswith = "string_startswith" : (string, string) -> bool
+val string_drop = "string_drop" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = "string_append" : (string, string) -> string
+val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat))
+val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat))
+val maybe_int_of_string = "maybe_int_of_string" : string -> option(int)
 
 val eq_real = "eq_real" : (real, real) -> bool
 
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 96b1ecf1..ac41114f 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -1,6 +1,6 @@
-default Order inc
+default Order dec
 
-infix 4 ==
+$include <prelude.sail>
 
 register n : nat
 
@@ -8,16 +8,6 @@ register x : nat
 
 register y : nat
 
-val eq_int = {lem: "eq", coq: "Z.eqb"} : (int, int) -> bool
-val eq_vec = {lem: "eq_vec", coq: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool
-
-overload operator == = {eq_int, eq_vec}
-
-val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
-
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc", coq: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
-  (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit)
-
 type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)}
 
 let word : wordsize = 8 : range(0, 8)
@@ -46,7 +36,7 @@ function main () = {
     32 => x = 128
   };
   match 0b010101 {
-    0b01 @ _ : vector(1, inc, bit) @ 0b101 => n = 42,
+    0b01 @ _ : vector(1, dec, bit) @ 0b101 => n = 42,
     _ => n = 0
   };
   n = 3;