diff options
| author | Alasdair Armstrong | 2018-09-10 16:53:39 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-09-10 16:58:00 +0100 |
| commit | 11618832e390711c198f816c1b7fb38e8c79a6aa (patch) | |
| tree | b8079d00ae37abf4581ce3de07f0b7b9690f362e /src/sail_lib.ml | |
| parent | ba30f984f8fd98d9c35b9660d8e7db498369c2b9 (diff) | |
Various fixes
C: Don't print usage message and quit when called with no arguments,
as this is used for testing C output
OCaml: Fix generation of datatypes with multiple type arguments
OCaml: Generate P_cons pattern correctly
C: Fix constant propagation to not propagate letbindings with type
annotations. This behaviour could cause type errors due to how type
variables are introduced. Now we only propagate letbindings when the
type of the propagated variable is guaranteed to be the same as the
inferred type of the binding.
Tests: Add OCaml tests to the C end-to-end tests (which really
shouldn't be in test/c/ any more, something like test/compile might be
better). Currently some issues with reals there like interpreter.
Tests: Rename list.sail -> list_test.sail because ocaml doesn't want
to compile files called list.ml.
Diffstat (limited to 'src/sail_lib.ml')
| -rw-r--r-- | src/sail_lib.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 505227ef..f1203725 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -51,6 +51,8 @@ let trace_call str = type bit = B0 | B1 +let eq_anything (a, b) = a = b + let eq_bit (a, b) = a = b let and_bit = function @@ -540,6 +542,9 @@ let gteq_real (x, y) = Rational.geq x y let to_real x = Rational.of_int (Big_int.to_int x) (* FIXME *) let negate_real x = Rational.neg x +let print_real (str, r) = print_string "REAL\n" +let prerr_real (str, r) = prerr_string "REAL\n" + let round_down x = Rational.floor x (* Num.big_int_of_num (Num.floor_num x) *) let round_up x = Rational.ceiling x (* Num.big_int_of_num (Num.ceiling_num x) *) let quotient_real (x, y) = Rational.div x y |