More work on C compilation

Can now compile things like early returns. The same approach should
work for exception handling as well. Once that's in place, just need
to work a bit more on getting union types to work + the library of
builtins, then we should be able to compile and run some of our specs
via C. Also added some documentation in comments for the general
approach taken when compiling (need many more though).

1 files changed, 0 insertions, 8 deletions

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index a09209d6..46d12375 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -204,26 +204,18 @@ overload operator * = {mult_range, mult_int, mult_real}
 
 val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real
 
-val gteq_int = "gteq" : (int, int) -> bool
-
 val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool
 
 overload operator >= = {gteq_atom, gteq_int, gteq_real}
 
-val lteq_int = "lteq" : (int, int) -> bool
-
 val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool
 
 overload operator <= = {lteq_atom, lteq_int, lteq_real}
 
-val gt_int = "gt" : (int, int) -> bool
-
 val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool
 
 overload operator > = {gt_atom, gt_int, gt_real}
 
-val lt_int = "lt" : (int, int) -> bool
-
 val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool
 
 overload operator < = {lt_atom, lt_int, lt_real}