Fix C compilation for CHERI and MIPS

First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.

Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.

Finally support for vector literals that are non-bitvectors has been
added.

5 files changed, 47 insertions, 3 deletions

diff --git a/test/c/gvectorlit.expect b/test/c/gvectorlit.expect
new file mode 100644
index 00000000..d3a1e9ab
--- /dev/null
+++ b/test/c/gvectorlit.expect
@@ -0,0 +1,2 @@
+x[0] = 0xAB
+x[1] = 0xCD
diff --git a/test/c/gvectorlit.sail b/test/c/gvectorlit.sail
new file mode 100644
index 00000000..097919ef
--- /dev/null
+++ b/test/c/gvectorlit.sail
@@ -0,0 +1,12 @@
+
+default Order dec
+
+$include <vector_dec.sail>
+
+val main : unit -> unit
+
+function main() = {
+  let x : vector(2, dec, bits(8)) = [0xAB, 0xCD];
+  print_bits("x[0] = ", x[0]);
+  print_bits("x[1] = ", x[1]);
+}
\ No newline at end of file
diff --git a/test/c/sail.h b/test/c/sail.h
index c0f2674b..b5328377 100644
--- a/test/c/sail.h
+++ b/test/c/sail.h
@@ -42,7 +42,11 @@ unit sail_exit(const unit u) {
 }
 
 void elf_entry(mpz_t *rop, const unit u) {
-  mpz_set_ui(*rop, 0x400168ul);
+  mpz_set_ui(*rop, 0x400130ul);
+}
+
+void elf_tohost(mpz_t *rop, const unit u) {
+  mpz_set_ui(*rop, 0x0ul);
 }
 
 // Sail bits are mapped to uint64_t where bitzero = 0ul and bitone = 1ul
@@ -102,12 +106,17 @@ bool eq_string(const sail_string str1, const sail_string str2) {
   return strcmp(str1, str2) == 0;
 }
 
-unit print_endline(sail_string str) {
+unit print_endline(const sail_string str) {
   printf("%s\n", str);
   return UNIT;
 }
 
-unit prerr_endline(sail_string str) {
+unit print_string(const sail_string str1, const sail_string str2) {
+  printf("%s%s\n", str1, str2);
+  return UNIT;
+}
+
+unit prerr_endline(const sail_string str) {
   fprintf(stderr, "%s\n", str);
   return UNIT;
 }
@@ -170,6 +179,10 @@ int64_t convert_int64_t_of_mpz_t(const mpz_t op) {
   return mpz_get_si(op);
 }
 
+void convert_mpz_t_of_int64_t(mpz_t *rop, const int64_t op) {
+  mpz_set_si(*rop, op);
+}
+
 // ***** Sail builtins for integers *****
 
 bool eq_int(const mpz_t op1, const mpz_t op2) {
@@ -384,6 +397,12 @@ void zero_extend(bv_t *rop, const bv_t op, const mpz_t len) {
   mpz_set(*rop->bits, *op.bits);
 }
 
+/* FIXME */
+void sign_extend(bv_t *rop, const bv_t op, const mpz_t len) {
+  rop->len = mpz_get_ui(len);
+  mpz_set(*rop->bits, *op.bits);
+}
+
 void clear_bv_t(bv_t *rop) {
   mpz_clear(*rop->bits);
   free(rop->bits);
diff --git a/test/c/tl_let.expect b/test/c/tl_let.expect
new file mode 100644
index 00000000..459d7e5f
--- /dev/null
+++ b/test/c/tl_let.expect
@@ -0,0 +1 @@
+cap_size = 32
diff --git a/test/c/tl_let.sail b/test/c/tl_let.sail
new file mode 100644
index 00000000..2f38f48e
--- /dev/null
+++ b/test/c/tl_let.sail
@@ -0,0 +1,10 @@
+
+val "print_int" : (string, int) -> unit
+
+let 'cap_size = 32
+
+val main : unit -> unit
+
+function main() = {
+  print_int("cap_size = ", cap_size);
+}
\ No newline at end of file