Fix all tests with type checking changes

2 files changed, 15 insertions, 35 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index ae86adbe..82b838b9 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -64,13 +64,13 @@ coverage: _sbuild/coverage.native
 	mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out
 
 riscv.c: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@
+	$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@
 
 riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile
 	gcc $(C_WARNINGS) -O2 riscv.c $(C_SRCS) ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
 
 riscv_model.c: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@
+	$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@
 
 riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
 	gcc -g $(C_WARNINGS) $(C_FLAGS) -O2 riscv_model.c riscv_sim.c $(C_SRCS) ../lib/*.c $(C_LIBS) -o $@
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index a2117bec..5779609d 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -710,16 +710,6 @@ function hex_bits_64_backwards s =
       Some (bv, n) if n == string_length(s) => bv
   }
 
-
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-val eq_int = {ocaml: "eq_int", lem: "eq", coq: "Z.eqb", c: "eq_int"} : (int, int) -> bool
-val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool
-
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec", coq: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool
 
 val eq_string = {c: "eq_string", ocaml: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool
@@ -738,7 +728,7 @@ val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
 /* sneaky deref with no effect necessary for bitfield writes */
 val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
-overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything}
+overload operator == = {eq_vec, eq_string, eq_real, eq_anything}
 
 val vector_subrange = {
   ocaml: "subrange",
@@ -866,10 +856,8 @@ val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> r
 
 overload operator ^ = {xor_vec, int_power, real_power, concat_str}
 
-val add_range = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val add_int = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int
+val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
+  (int('n), int('m)) -> int('n + 'm)
 
 val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -877,10 +865,10 @@ val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n),
 
 val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real
 
-overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
+overload operator + = {add_atom, add_vec, add_vec_int, add_real}
 
-val sub_range = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
+val sub_atom = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm.
+  (int('n), int('m)) -> int('n - 'm)
 
 val sub_int = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
 val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
@@ -893,13 +881,13 @@ val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n),
 
 val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real
 
-val negate_range = {ocaml: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
+val negate_atom = {ocaml: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. atom('n) -> atom(- 'n)
 
 val negate_int = {ocaml: "negate", lem: "integerNegate", coq: "Z.opp"} : int -> int
 
 val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real
 
-overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
+overload operator - = {sub_atom, sub_int, sub_vec, sub_vec_int, sub_real}
 
 overload negate = {negate_range, negate_int, negate_real}
 
@@ -914,29 +902,21 @@ overload operator * = {mult_atom, mult_int, mult_real}
 
 val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real
 
-val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool
-
 val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool
 
-overload operator >= = {gteq_atom, gteq_int, gteq_real}
-
-val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool
+overload operator >= = {gteq_real}
 
 val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool
 
-overload operator <= = {lteq_atom, lteq_int, lteq_real}
-
-val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool
+overload operator <= = {lteq_real}
 
 val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool
 
-overload operator > = {gt_atom, gt_int, gt_real}
-
-val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool
+overload operator > = {gt_real}
 
 val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool
 
-overload operator < = {lt_atom, lt_int, lt_real}
+overload operator < = {lt_real}
 
 val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int
 
@@ -1137,7 +1117,7 @@ function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
 val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
 
-val n_leading_spaces : string -> nat
+val n_leading_spaces : string -> {'n, 'n >= 0. int('n)}
 function n_leading_spaces s =
   match s {
     "" => 0,