aboutsummaryrefslogtreecommitdiff
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r--kernel/cClosure.ml186
1 files changed, 163 insertions, 23 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 3fd613e905..af08ea18c1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -53,10 +53,10 @@ let reset () =
let stop() =
Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
- str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
- int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++
+ str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
+ int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++
str " cofix=" ++ int !cofix ++ str" prune=" ++ int !prune ++
- str"]")
+ str"]")
let incr_cnt red cnt =
if red then begin
@@ -119,7 +119,7 @@ module RedFlags : RedFlagsSig = struct
type red_kind = BETA | DELTA | ETA | MATCH | FIX
| COFIX | ZETA
- | CONST of Constant.t | VAR of Id.t
+ | CONST of Constant.t | VAR of Id.t
let fBETA = BETA
let fDELTA = DELTA
let fETA = ETA
@@ -181,16 +181,16 @@ module RedFlags : RedFlagsSig = struct
| ETA -> incr_cnt red.r_eta eta
| CONST kn ->
let c = is_transparent_constant red.r_const kn in
- incr_cnt c delta
+ incr_cnt c delta
| VAR id -> (* En attendant d'avoir des kn pour les Var *)
let c = is_transparent_variable red.r_const id in
- incr_cnt c delta
+ incr_cnt c delta
| ZETA -> incr_cnt red.r_zeta zeta
| MATCH -> incr_cnt red.r_match nb_match
| FIX -> incr_cnt red.r_fix fix
| COFIX -> incr_cnt red.r_cofix cofix
| DELTA -> (* Used for Rel/Var defined in context *)
- incr_cnt red.r_delta delta
+ incr_cnt red.r_delta delta
let red_projection red p =
if Projection.unfolded p then true
@@ -348,6 +348,7 @@ and fterm =
| FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
| FEvar of existential * fconstr subs
| FInt of Uint63.t
+ | FFloat of Float64.t
| FLIFT of int * fconstr
| FCLOS of constr * fconstr subs
| FLOCKED
@@ -428,7 +429,7 @@ let rec stack_args_size = function
let rec lft_fconstr n ft =
let r = Mark.relevance ft.mark in
match ft.term with
- | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft
+ | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft
| FRel i -> {mark=mark Norm r;term=FRel(i+n)}
| FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))}
| FFix(fx,e) ->
@@ -499,6 +500,7 @@ let mk_clos e t =
| Ind kn -> {mark = mark Norm KnownR; term = FInd kn }
| Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
| Int i -> {mark = mark Cstr Unknown; term = FInt i}
+ | Float f -> {mark = mark Cstr Unknown; term = FFloat f}
| (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
{mark = mark Red Unknown; term = FCLOS(t,e)}
@@ -616,6 +618,8 @@ let rec to_constr lfts v =
| FInt i ->
Constr.mkInt i
+ | FFloat f ->
+ Constr.mkFloat f
| FCLOS (t,env) ->
if is_subs_id env && is_lift_id lfts then t
@@ -820,10 +824,10 @@ let rec try_drop_parameters depth n = function
reloc_rargs depth (append_stack aft s)
| Zshift(k)::s -> try_drop_parameters (depth-k) n s
| [] ->
- if Int.equal n 0 then []
- else raise Not_found
+ if Int.equal n 0 then []
+ else raise Not_found
| (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ -> assert false
- (* strip_update_shift_app only produces Zapp and Zshift items *)
+ (* strip_update_shift_app only produces Zapp and Zshift items *)
let drop_parameters depth n argstk =
try try_drop_parameters depth n argstk
@@ -848,7 +852,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
match Declareops.inductive_make_projections ind mib with
| Some projs ->
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
- arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+ arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.Declarations.mind_nparams in
let right = fapp_stack (f, s') in
let (depth, args, _s) = strip_update_shift_app m s in
@@ -865,8 +869,8 @@ let eta_expand_ind_stack env ind m s (f, s') =
let rec project_nth_arg n = function
| Zapp args :: s ->
let q = Array.length args in
- if n >= q then project_nth_arg (n - q) s
- else (* n < q *) args.(n)
+ if n >= q then project_nth_arg (n - q) s
+ else (* n < q *) args.(n)
| (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false
(* After drop_parameters we have a purely applicative stack *)
@@ -887,12 +891,12 @@ let contract_fix_vect fix =
(bds.(i),
(fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance);
term = FFix (((reci,j),rdcl),env) }),
- env, Array.length bds)
+ env, Array.length bds)
| FCoFix ((i,(nas,_,bds as rdcl)),env) ->
(bds.(i),
(fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance);
term = FCoFix ((j,rdcl),env) }),
- env, Array.length bds)
+ env, Array.length bds)
| _ -> assert false
in
(subs_cons(Array.init nfix make_body, env), thisbody)
@@ -926,7 +930,7 @@ let rec knh info m stk =
(* cases where knh stops *)
| (FFlex _|FLetIn _|FConstruct _|FEvar _|
- FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _) ->
+ FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) ->
(m, stk)
(* The same for pure terms *)
@@ -940,7 +944,7 @@ and knht info e t stk =
| Cast(a,_,_) -> knht info e a stk
| Rel n -> knh info (clos_rel e n) stk
| Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk
- | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk)
+ | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk)
| CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk
| Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk
| Prod (n, t, c) ->
@@ -969,6 +973,11 @@ module FNativeEntries =
| FInt i -> i
| _ -> raise Primred.NativeDestKO
+ let get_float () e =
+ match [@ocaml.warning "-4"] e.term with
+ | FFloat f -> f
+ | _ -> raise Primred.NativeDestKO
+
let dummy = {mark = mark Norm KnownR; term = FRel 0}
let current_retro = ref Retroknowledge.empty
@@ -982,6 +991,16 @@ module FNativeEntries =
fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
| None -> defined_int := false
+ let defined_float = ref false
+ let ffloat = ref dummy
+
+ let init_float retro =
+ match retro.Retroknowledge.retro_float64 with
+ | Some c ->
+ defined_float := true;
+ ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+ | None -> defined_float := false
+
let defined_bool = ref false
let ftrue = ref dummy
let ffalse = ref dummy
@@ -1020,6 +1039,7 @@ module FNativeEntries =
let fEq = ref dummy
let fLt = ref dummy
let fGt = ref dummy
+ let fcmp = ref dummy
let init_cmp retro =
match retro.Retroknowledge.retro_cmp with
@@ -1027,9 +1047,54 @@ module FNativeEntries =
defined_cmp := true;
fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) };
fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) };
- fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }
+ fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) };
+ let (icmp, _) = cEq in
+ fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
| None -> defined_cmp := false
+ let defined_f_cmp = ref false
+ let fFEq = ref dummy
+ let fFLt = ref dummy
+ let fFGt = ref dummy
+ let fFNotComparable = ref dummy
+
+ let init_f_cmp retro =
+ match retro.Retroknowledge.retro_f_cmp with
+ | Some (cFEq, cFLt, cFGt, cFNotComparable) ->
+ defined_f_cmp := true;
+ fFEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFEq) };
+ fFLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFLt) };
+ fFGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFGt) };
+ fFNotComparable :=
+ { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) };
+ | None -> defined_f_cmp := false
+
+ let defined_f_class = ref false
+ let fPNormal = ref dummy
+ let fNNormal = ref dummy
+ let fPSubn = ref dummy
+ let fNSubn = ref dummy
+ let fPZero = ref dummy
+ let fNZero = ref dummy
+ let fPInf = ref dummy
+ let fNInf = ref dummy
+ let fNaN = ref dummy
+
+ let init_f_class retro =
+ match retro.Retroknowledge.retro_f_class with
+ | Some (cPNormal, cNNormal, cPSubn, cNSubn, cPZero, cNZero,
+ cPInf, cNInf, cNaN) ->
+ defined_f_class := true;
+ fPNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPNormal) };
+ fNNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNNormal) };
+ fPSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPSubn) };
+ fNSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNSubn) };
+ fPZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPZero) };
+ fNZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNZero) };
+ fPInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPInf) };
+ fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) };
+ fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) };
+ | None -> defined_f_class := false
let defined_refl = ref false
let frefl = ref dummy
@@ -1044,10 +1109,13 @@ module FNativeEntries =
let init env =
current_retro := env.retroknowledge;
init_int !current_retro;
+ init_float !current_retro;
init_bool !current_retro;
init_carry !current_retro;
init_pair !current_retro;
init_cmp !current_retro;
+ init_f_cmp !current_retro;
+ init_f_class !current_retro;
init_refl !current_retro
let check_env env =
@@ -1057,6 +1125,10 @@ module FNativeEntries =
check_env env;
assert (!defined_int)
+ let check_float env =
+ check_env env;
+ assert (!defined_float)
+
let check_bool env =
check_env env;
assert (!defined_bool)
@@ -1073,10 +1145,22 @@ module FNativeEntries =
check_env env;
assert (!defined_cmp)
+ let check_f_cmp env =
+ check_env env;
+ assert (!defined_f_cmp)
+
+ let check_f_class env =
+ check_env env;
+ assert (!defined_f_class)
+
let mkInt env i =
check_int env;
{ mark = mark Cstr KnownR; term = FInt i }
+ let mkFloat env f =
+ check_float env;
+ { mark = mark Norm KnownR; term = FFloat f }
+
let mkBool env b =
check_bool env;
if b then !ftrue else !ffalse
@@ -1090,6 +1174,11 @@ module FNativeEntries =
check_pair env;
{ mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) }
+ let mkFloatIntPair env f i =
+ check_pair env;
+ check_float env;
+ { mark = mark Cstr KnownR; term = FApp(!fPair, [|!ffloat;!fint;f;i|]) }
+
let mkLt env =
check_cmp env;
!fLt
@@ -1102,6 +1191,57 @@ module FNativeEntries =
check_cmp env;
!fGt
+ let mkFLt env =
+ check_f_cmp env;
+ !fFLt
+
+ let mkFEq env =
+ check_f_cmp env;
+ !fFEq
+
+ let mkFGt env =
+ check_f_cmp env;
+ !fFGt
+
+ let mkFNotComparable env =
+ check_f_cmp env;
+ !fFNotComparable
+
+ let mkPNormal env =
+ check_f_class env;
+ !fPNormal
+
+ let mkNNormal env =
+ check_f_class env;
+ !fNNormal
+
+ let mkPSubn env =
+ check_f_class env;
+ !fPSubn
+
+ let mkNSubn env =
+ check_f_class env;
+ !fNSubn
+
+ let mkPZero env =
+ check_f_class env;
+ !fPZero
+
+ let mkNZero env =
+ check_f_class env;
+ !fNZero
+
+ let mkPInf env =
+ check_f_class env;
+ !fPInf
+
+ let mkNInf env =
+ check_f_class env;
+ !fNInf
+
+ let mkNaN env =
+ check_f_class env;
+ !fNaN
end
module FredNative = RedNative(FNativeEntries)
@@ -1164,7 +1304,7 @@ let rec knr info tab m stk =
(match info.i_cache.i_sigma ev with
Some c -> knit info tab env c stk
| None -> (m,stk))
- | FInt _ ->
+ | FInt _ | FFloat _ ->
(match [@ocaml.warning "-4"] strip_update_shift_app m stk with
| (_, _, Zprimitive(op,c,rargs,nargs)::s) ->
let (rargs, nargs) = skip_native_args (m::rargs) nargs in
@@ -1207,11 +1347,11 @@ let rec zip_term zfun m stk =
zip_term zfun (mkApp(m, Array.map zfun args)) s
| ZcaseT(ci,p,br,e)::s ->
let t = mkCase(ci, zfun (mk_clos e p), m,
- Array.map (fun b -> zfun (mk_clos e b)) br) in
+ Array.map (fun b -> zfun (mk_clos e b)) br) in
zip_term zfun t s
| Zproj p::s ->
let t = mkProj (Projection.make p true, m) in
- zip_term zfun t s
+ zip_term zfun t s
| Zfix(fx,par)::s ->
let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
zip_term zfun h s
@@ -1270,7 +1410,7 @@ and norm_head info tab m =
| FProj (p,c) ->
mkProj (p, kl info tab c)
| FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
- | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ -> term_of_fconstr m
+ | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m
(* Initialization and then normalization *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:57:53 +0000