diff options
| author | Alasdair Armstrong | 2018-02-01 19:43:41 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-02-01 19:46:38 +0000 |
| commit | a05625c5e8f67448eda077f8374bfb06c475dad5 (patch) | |
| tree | bd71243c0cd4bee6134a5af14e997bde2b0cd6eb /lib | |
| parent | 55edbc7607e4faa9dc28d790ec994d462920b390 (diff) | |
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).
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flow.sail | 5 |
1 files changed, 5 insertions, 0 deletions
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 |