Add Lem builtins for operations on reals

... that match the names in lib/real.sail.

Also fix the lem mapping for abs_int_atom and a Lem syntax error with
nested record updates.

1 files changed, 21 insertions, 9 deletions

diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 7bd950d7..9e1f20c0 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -35,15 +35,27 @@ let power_int_nat l r = integerPow l r
 let power_int_int l r = integerPow l (nat_of_int 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 max_int l r = integerMax l r*)
+
+let inline add_real l r = realAdd l r
+let inline sub_real l r = realMinus l r
+let inline mult_real l r = realMult l r
+let inline div_real l r = realDiv l r
+let inline neg_real r = realNegate r
+let inline abs_real r = realAbs r
+let inline real_power b e = realPowInteger b e
+let inline sqrt_real r = realSqrt r
+
+let inline eq_real l r = realEq l r
+let inline lt_real l r = realLess l r
+let inline gt_real l r = realLessEqual l r
+let inline lteq_real l r = realGreater l r
+let inline gteq_real l r = realGreaterEqual l r
+
+let inline to_real i = realFromInteger i
+
+let inline round_down r = realFloor r
+let inline round_up r = realCeiling r
 
 val print_endline : string -> unit
 let print_endline _ = ()