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.

1 files changed, 5 insertions, 2 deletions

diff --git a/mips/main.sail b/mips/main.sail
index 2df5c0f8..e3ffa262 100644
--- a/mips/main.sail
+++ b/mips/main.sail
@@ -9,7 +9,7 @@ function fetch_and_execute () = {
     branchPending = 0b0;
     nextPC = if inBranchDelay then delayedPC else PC + 4;
     cp2_next_pc();
-    
+
     print_bits("PC: ", PC);
     try {
       let pc_pa = TranslatePC(PC);
@@ -36,7 +36,10 @@ function fetch_and_execute () = {
   skip_wmvt();
 }
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+val elf_entry = {
+  ocaml: "Elf_loader.elf_entry",
+  c: "elf_entry"
+} : unit -> int
 
 val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}