Got riscv spec to typecheck with sail2

Fix a typechecking bug involving constraints attached to type synonyms
within existentials.

1 files changed, 16 insertions, 1 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index b4e36507..ff11cf7e 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -276,9 +276,11 @@ val cast ex_int : int -> {'n, true. atom('n)}
 
 function ex_int 'n = n
 
+/*
 val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)}
 
 function ex_range (n as 'N) = n
+*/
 
 val coerce_int_nat : int -> nat effect {escape}
 
@@ -297,6 +299,7 @@ val print_int = "print_int" : (string, int) -> unit
 union exception = {
   Error_not_implemented : string,
   Error_misaligned_access,
+  Error_EBREAK,
 }
 
 val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
@@ -313,4 +316,16 @@ function operator <_u  (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigne
 function operator >=_u (x : bits('n), y : bits('n)) -> forall 'n. bool = unsigned(x) >= unsigned(y)
 
 val cast bool_to_bits : bool -> bits(1)
-function bool_to_bits x = if x then 0b1 else 0b0
\ No newline at end of file
+function bool_to_bits x = if x then 0b1 else 0b0
+
+val cast bit_to_bool : bit -> bool
+function bit_to_bool bitone  = true
+and      bit_to_bool bitzero = false
+
+infix 7 >>
+infix 7 <<
+
+val operator >> : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val vector64 : int -> bits(64)
\ No newline at end of file