From a05625c5e8f67448eda077f8374bfb06c475dad5 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 1 Feb 2018 19:43:41 +0000
Subject: 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).
---
 lib/flow.sail | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index 10badc93..52c98753 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -28,6 +28,11 @@ val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> boo
 val eq_range = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
 val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
 
+val lteq_int = "lteq" : (int, int) -> bool
+val gteq_int = "gteq" : (int, int) -> bool
+val lt_int = "lt" : (int, int) -> bool
+val gt_int = "lt" : (int, int) -> bool
+
 overload operator == = {eq_atom, eq_range, eq_int}
 
 $ifdef TEST
-- 
cgit v1.2.3