Work in progress on the coq backend

- originally based on the Lem backend
- added externs to some of the library files and tests
- added wildcard to extern valspecs in parser
- added Type_check.get_val_spec_orig to return the valspec with the
  function's original names for bound type variables

Note that most of the tests will fail currently

4 files changed, 9 insertions, 9 deletions

diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail
index d93143f0..2021bf67 100644
--- a/test/typecheck/pass/arm_FPEXC1.sail
+++ b/test/typecheck/pass/arm_FPEXC1.sail
@@ -1,12 +1,12 @@
 default Order dec
 
-val vector_access = {ocaml: "access", lem: "access_vec_dec"}: forall ('n : Int).
+val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int).
   (vector('n, dec, bit), int) -> bit
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1.
   (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit)
 
-val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit)
 
 register _FPEXC32_EL2 : vector(32, dec, bit)
diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail
index 4e030a60..d2549e01 100644
--- a/test/typecheck/pass/atomcase.sail
+++ b/test/typecheck/pass/atomcase.sail
@@ -2,7 +2,7 @@ default Order dec
 
 infix 4 ==
 
-val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
+val eq_atom = {ocaml: "eq_atom", lem: "eq", coq: "Z.eqb"}: forall ('n : Int) ('m : Int).
   (atom('n), atom('m)) -> bool
 
 overload operator == = {eq_atom}
diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
index 991cd828..261e3b44 100644
--- a/test/typecheck/pass/deinfix_plus.sail
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val bv_add = {ocaml: "add_vec", lem: "add_vec", coq: "add_vec"}: forall ('n : Int).
   (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit)
 
 overload operator + = {bv_add}
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
index 47343e02..96b1ecf1 100644
--- a/test/typecheck/pass/exist_pattern.sail
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -8,14 +8,14 @@ register x : nat
 
 register y : nat
 
-val eq_int = {lem: "eq"} : (int, int) -> bool
-val eq_vec = {lem: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool
+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" : (bool, bool) -> bool
+val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
+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)}