diff options
| -rw-r--r-- | lib/smt.sail | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail2_values.lem | 30 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 2 |
3 files changed, 23 insertions, 11 deletions
diff --git a/lib/smt.sail b/lib/smt.sail index 93fe0827..2e72e791 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -23,7 +23,7 @@ val emod_int = { val abs_int_atom = { ocaml: "abs_int", interpreter: "abs_int", - lem: "abs_int", + lem: "integerAbs", c: "abs_int", coq: "abs_with_eq" } : forall 'n. int('n) -> int(abs('n)) 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 _ = () diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 993934f5..34ccc5ba 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -901,7 +901,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_record tid env -> tid | _ -> raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in - anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + anglebars (space ^^ doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps) ^^ space) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = |