diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/float64.ml | 16 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 12 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
3 files changed, 21 insertions, 13 deletions
diff --git a/kernel/float64.ml b/kernel/float64.ml index 3e36373b77..cc661aeba3 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -12,7 +12,10 @@ format *) type t = float -let is_nan f = f <> f +(* The [f : float] type annotation enable the compiler to compile f <> f + as comparison on floats rather than the polymorphic OCaml comparison + which is much slower. *) +let is_nan (f : float) = f <> f let is_infinity f = f = infinity let is_neg_infinity f = f = neg_infinity @@ -42,19 +45,20 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable -let eq x y = x = y +(* See above comment on [is_nan] for the [float] type annotations. *) +let eq (x : float) (y : float) = x = y [@@ocaml.inline always] -let lt x y = x < y +let lt (x : float) (y : float) = x < y [@@ocaml.inline always] -let le x y = x <= y +let le (x : float) (y : float) = x <= y [@@ocaml.inline always] (* inspired by lib/util.ml; see also #10471 *) -let pervasives_compare = compare +let pervasives_compare (x : float) (y : float) = compare x y -let compare x y = +let compare (x : float) (y : float) = if x < y then FLt else ( diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f6f2058c13..8db8a044a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -321,6 +321,8 @@ let universes_of_private eff = let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env +let structure_body_of_safe_env env = env.revstruct + let sections_of_safe_env senv = senv.sections let get_section = function @@ -757,7 +759,7 @@ let translate_direct_opaque env kn ce = let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } -let export_side_effects mb env (b_ctx, eff) = +let export_side_effects mb env eff = let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl @@ -774,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) = in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, b_ctx + | [] -> List.rev acc | eff :: rest -> if Int.equal sl 0 then let env, cb = @@ -803,8 +805,8 @@ let push_opaque_proof pf senv = let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in senv, o -let export_private_constants ce senv = - let exported, ce = export_side_effects senv.revstruct senv.env ce in +let export_private_constants eff senv = + let exported = export_side_effects senv.revstruct senv.env eff in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> let local = empty_private c.const_universes in @@ -817,7 +819,7 @@ let export_private_constants ce senv = let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) let senv = List.fold_left add_constant_aux senv bodies in - (ce, exported), senv + exported, senv let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 92bbd264fa..e472dfd5e5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env val sections_of_safe_env : safe_environment -> section_data Section.t option +val structure_body_of_safe_env : safe_environment -> Declarations.structure_body + (** The safe_environment state monad *) type safe_transformer0 = safe_environment -> safe_environment @@ -84,8 +86,8 @@ type side_effect_declaration = type exported_private_constant = Constant.t val export_private_constants : - private_constants Entries.proof_output -> - (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer + private_constants -> + exported_private_constant list safe_transformer (** returns the main constant *) val add_constant : |