Coq: limited support for existentially-typed tuples

- in particular at monadic interfaces (i.e., sufficient for instruction
  ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
  example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)

2 files changed, 37 insertions, 12 deletions

diff --git a/test/coq/pass/ast_with_dep_tuple.sail b/test/coq/pass/ast_with_dep_tuple.sail
new file mode 100644
index 00000000..22627847
--- /dev/null
+++ b/test/coq/pass/ast_with_dep_tuple.sail
@@ -0,0 +1,37 @@
+default Order dec
+$include <prelude.sail>
+
+/*type reg = {'n, 0 <= 'n < 16. int('n)}*/
+type reg = range(0,15)
+
+union instr = {
+  Mov : {'d, 'd in {8,16}. (int('d), reg, bits('d))}
+}
+
+register regs : vector(16,dec,bits(32))
+
+val exec : instr -> unit effect {wreg}
+
+function exec(Mov(sz,r,imm)) =
+  regs[r] = sail_zero_extend(imm,32)
+
+val decode : bits(32) -> instr
+
+function decode(0x0000 @ (x : bits(16))) = Mov(16,0,x)
+and      decode(0x10000 @ (r : bits(4)) @ (x : bits(8))) = Mov(8, unsigned(r), x)
+
+/* Versions that construct/match the tuple separately from the variant.
+   Not currently supported.
+val exec2 : instr -> unit effect {wreg}
+
+function exec2(Mov(tuple)) =
+  let (sz,r,imm) = tuple in
+  regs[r] = sail_zero_extend(imm,32)
+
+val decode2 : bits(32) -> instr
+
+function decode2(0x0000 @ (x : bits(16))) =
+  let tup : {'d, 'd in {8,16}. (int('d), reg, bits('d))} = (16,0,x) in
+  Mov(tup)
+and      decode2(0x10000 @ (r : bits(4)) @ (x : bits(8))) = Mov(8, unsigned(r), x)
+*/
diff --git a/test/coq/skip b/test/coq/skip
index 259df4b0..b99c87ad 100644
--- a/test/coq/skip
+++ b/test/coq/skip
@@ -1,21 +1,11 @@
-XXXXX tests with full generic equality
-decode_patterns.sail
 XXXXX tests with deliberate redundant pattern match clause
 option_tuple.sail
 pat_completeness.sail
 XXXXX tests which need inline extern definitions adjusted
 patternrefinement.sail
 vector_subrange_gen.sail
-XXXXX currently unsupported use of a bitvector in a parametric vector type
-pure_record.sail
-pure_record2.sail
-pure_record3.sail
-vector_access_dec.sail
-vector_access.sail
 XXXXX unsupported existential quantification of a vector length
 bind_typ_var.sail
-XXXXX needs impliciation in constraints fixed
-bool_constraint.sail
 XXXXX needs some smart existential instantiation
 complex_exist_sat.sail
 XXXXX needs name collision avoidance due to type/constructor punning
@@ -23,14 +13,12 @@ constraint_ctor.sail
 XXXXX Complex existential type - probably going to need this for ARM instruction ASTs
 execute_decode_hard.sail
 existential_ast.sail
-existential_ast2.sail
 existential_ast3.sail
 XXXXX Needs an existential witness
 exist1.sail
 exist2.sail
 XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere
 exist_synonym.sail
-reg_32_64.sail
 XXXXX Examples where int(...) should be expanded internally, but not yet supported
 exit1.sail
 exit2.sail