Add support for real numbers to Lem backend

Requires version of Lem with real number support, currently at

https://bitbucket.org/bauereiss/lem/branch/reals

5 files changed, 45 insertions, 30 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 9a79f81b..215f63b2 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -125,11 +125,11 @@ val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect p
 (* Arithmetic *)
 
 val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
-    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add"
+    ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add_int"
 
-val extern (nat, nat) -> nat effect pure add_nat = "add"
+val extern (nat, nat) -> nat effect pure add_nat = "add_int"
 
-val extern (int, int) -> int effect pure add_int = "add"
+val extern (int, int) -> int effect pure add_int
 
 val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
@@ -144,9 +144,9 @@ val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec
 
 val extern forall Num 'n, Num 'm, Num 'o, Num 'p.
-    ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub_range = "sub"
+    ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub_range = "sub_int"
 
-val extern (int, int) -> int effect pure sub_int = "sub"
+val extern (int, int) -> int effect pure sub_int = "sub_int"
 
 val forall Num 'n, Num 'm, Order 'ord.
     (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int
@@ -177,7 +177,7 @@ overload (deinfix -) [
 
 val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU"
 
-val (int, int) -> int effect pure mult_int
+val extern (int, int) -> int effect pure mult_int
 val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> [:'n * 'm:] effect pure mult_range = "mult_int"
 val forall Num 'n, Num 'o, Order 'ord.
     (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mult_vec
@@ -296,7 +296,7 @@ val extern (int, int) -> int effect pure min_int = "min"
 
 overload min [min_range_atom; min_int]
 
-val extern (int, int) -> int effect pure quotient
+val extern (int, int) -> int effect pure quotient = "quotient_int"
 
 overload (deinfix quot) [quotient]
 
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 7b117726..f14ef2e4 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -197,18 +197,8 @@ let extz_bl (start, len, bits) = Vector bits start false
 let exts_bl (start, len, bits) = Vector bits start false
 
 
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+let modulo (l,r) = hardware_mod l r
 
 let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
   let (l',r') = (to_num sign l, to_num sign r) in
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index b4d1c9a4..4d1cc713 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -240,18 +240,8 @@ let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
 let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
 let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
 
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
 let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+let modulo (l,r) = hardware_mod l r
 
 (* TODO: this, and the definitions that use it, currently require Size for
    to_vec, which I'd rather avoid in favour of library versions; the
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 1e7dc2b9..95a61eca 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,6 +13,26 @@ let pow m n = m ** (natFromInteger n)
 
 let pow2 n = pow 2 n
 
+let add_int (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub_int (l,r) = integerMinus l r
+let mult_int (l,r) = integerMult l r
+let quotient_int (l,r) = integerDiv l r
+let quotient_nat (l,r) = natDiv l r
+let power_int_nat (l,r) = integerPow l r
+let power_int_int (l, r) = integerPow l (natFromInteger r)
+let negate_int i = integerNegate i
+let min_int (l, r) = integerMin l r
+let max_int (l, r) = integerMax l r
+
+let add_real (l, r) = realAdd l r
+let sub_real (l, r) = realMinus l r
+let mult_real (l, r) = realMult l r
+let div_real (l, r) = realDiv l r
+let negate_real r = realNegate r
+let abs_real r = realAbs r
+let power_real (b, e) = realPowInteger b e
+
 let bool_or (l, r) = (l || r)
 let bool_and (l, r) = (l && r)
 let bool_xor (l, r) = xor l r
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c74cceb9..451be476 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -289,7 +289,22 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
               (doc_tannot_lem sequential mwords false typ)))
        | _ -> utf8string "(failwith \"undefined value of unsupported type\")")
   | L_string s -> utf8string ("\"" ^ s ^ "\"")
-  | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *)
+  | L_real s ->
+    (* Lem does not support decimal syntax, so we translate a string
+       of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y).
+       The OCaml library has a conversion function from strings to floats, but
+       not from floats to ratios. ZArith's Q library does have the latter, but
+       using this would require adding a dependency on ZArith to Sail. *)
+    let parts = Util.split_on_char '.' s in
+    let (num, denom) = match parts with
+    | [i] -> (big_int_of_string i, unit_big_int)
+    | [i;f] ->
+      let denom = power_int_positive_int 10 (String.length f) in
+      (add_big_int (mult_big_int (big_int_of_string i) denom) (big_int_of_string f), denom)
+    | _ ->
+      raise (Reporting_basic.Fatal_error
+        (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in
+    separate space (List.map string ["realFromFrac"; string_of_big_int num; string_of_big_int denom])
 
 (* typ_doc is the doc for the type being quantified *)
 let doc_quant_item (QI_aux (qi, _)) = match qi with