summaryrefslogtreecommitdiff
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r--kernel/cClosure.ml228
1 files changed, 122 insertions, 106 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index fe9ec579..08114abc 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Created by Bruno Barras with Benjamin Werner's account to implement
@@ -23,7 +25,7 @@ open CErrors
open Util
open Pp
open Names
-open Term
+open Constr
open Vars
open Environ
open Esubst
@@ -85,15 +87,16 @@ module type RedFlagsSig = sig
val fFIX : red_kind
val fCOFIX : red_kind
val fZETA : red_kind
- val fCONST : constant -> red_kind
+ val fCONST : Constant.t -> red_kind
val fVAR : Id.t -> red_kind
val no_red : reds
val red_add : reds -> red_kind -> reds
val red_sub : reds -> red_kind -> reds
val red_add_transparent : reds -> transparent_state -> reds
+ val red_transparent : reds -> transparent_state
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
- val red_projection : reds -> projection -> bool
+ val red_projection : reds -> Projection.t -> bool
end
module RedFlags = (struct
@@ -114,7 +117,7 @@ module RedFlags = (struct
type red_kind = BETA | DELTA | ETA | MATCH | FIX
| COFIX | ZETA
- | CONST of constant | VAR of Id.t
+ | CONST of Constant.t | VAR of Id.t
let fBETA = BETA
let fDELTA = DELTA
let fETA = ETA
@@ -164,6 +167,8 @@ module RedFlags = (struct
let (l1,l2) = red.r_const in
{ red with r_const = Id.Pred.remove id l1, l2 }
+ let red_transparent red = red.r_const
+
let red_add_transparent red tr =
{ red with r_const = tr }
@@ -234,7 +239,7 @@ let unfold_red kn =
* instantiations (cbv or lazy) are.
*)
-type table_key = constant puniverses tableKey
+type table_key = Constant.t Univ.puniverses tableKey
let eq_pconstant_key (c,u) (c',u') =
eq_constant_key c c' && Univ.Instance.equal u u'
@@ -254,12 +259,14 @@ module KeyTable = Hashtbl.Make(IdKeyHash)
let eq_table_key = IdKeyHash.equal
+type 'a infos_tab = 'a KeyTable.t
+
type 'a infos_cache = {
- i_repr : 'a infos -> constr -> 'a;
+ i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
i_env : env;
i_sigma : existential -> constr option;
- i_rels : constr option array;
- i_tab : 'a KeyTable.t }
+ i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
+}
and 'a infos = {
i_flags : reds;
@@ -274,26 +281,29 @@ let assoc_defined id env = match Environ.lookup_named id env with
| LocalDef (_, c, _) -> c
| _ -> raise Not_found
-let ref_value_cache ({i_cache = cache} as infos) ref =
+let ref_value_cache ({i_cache = cache} as infos) tab ref =
try
- Some (KeyTable.find cache.i_tab ref)
+ Some (KeyTable.find tab ref)
with Not_found ->
try
let body =
match ref with
| RelKey n ->
- let len = Array.length cache.i_rels in
- let i = n - 1 in
- let () = if i < 0 || len <= i then raise Not_found in
- begin match Array.unsafe_get cache.i_rels i with
- | None -> raise Not_found
- | Some t -> lift n t
- end
+ let open Context.Rel.Declaration in
+ let i = n - 1 in
+ let (d, _) =
+ try Range.get cache.i_rels i
+ with Invalid_argument _ -> raise Not_found
+ in
+ begin match d with
+ | LocalAssum _ -> raise Not_found
+ | LocalDef (_, t, _) -> lift n t
+ end
| VarKey id -> assoc_defined id cache.i_env
| ConstKey cst -> constant_value_in cache.i_env cst
in
- let v = cache.i_repr infos body in
- KeyTable.add cache.i_tab ref v;
+ let v = cache.i_repr infos tab body in
+ KeyTable.add tab ref v;
Some v
with
| Not_found (* List.assoc *)
@@ -303,27 +313,14 @@ let ref_value_cache ({i_cache = cache} as infos) ref =
let evar_value cache ev =
cache.i_sigma ev
-let defined_rels flags env =
-(* if red_local_const (snd flags) then*)
- let ctx = rel_context env in
- let len = List.length ctx in
- let ans = Array.make len None in
- let open Context.Rel.Declaration in
- let iter i = function
- | LocalAssum _ -> ()
- | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
- in
- let () = List.iteri iter ctx in
- ans
-(* else (0,[])*)
-
let create mk_cl flgs env evars =
+ let open Pre_env in
let cache =
{ i_repr = mk_cl;
i_env = env;
i_sigma = evars;
- i_rels = defined_rels flgs env;
- i_tab = KeyTable.create 17 }
+ i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
+ }
in { i_flags = flgs; i_cache = cache }
@@ -367,7 +364,7 @@ and fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of projection * fconstr
+ | FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
@@ -401,7 +398,7 @@ let update v1 no t =
type stack_member =
| Zapp of fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * constant
+ | Zproj of int * int * Constant.t
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -480,7 +477,8 @@ let rec lft_fconstr n ft =
| FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
| FLIFT(k,m) -> lft_fconstr (n+k) m
| FLOCKED -> assert false
- | _ -> {norm=ft.norm; term=FLIFT(n,ft)}
+ | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+ | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
if Int.equal k 0 then f else lft_fconstr k f
let lift_fconstr_vect k v =
@@ -516,7 +514,7 @@ let zupdate m s =
else s
let mk_lambda env t =
- let (rvars,t') = decompose_lam t in
+ let (rvars,t') = Term.decompose_lam t in
FLambda(List.length rvars, List.rev rvars, t', env)
let destFLambda clos_fun t =
@@ -530,7 +528,7 @@ let destFLambda clos_fun t =
(* Optimization: do not enclose variables in a closure.
Makes variable access much faster *)
let mk_clos e t =
- match kind_of_term t with
+ match kind t with
| Rel i -> clos_rel e i
| Var x -> { norm = Red; term = FFlex (VarKey x) }
| Const c -> { norm = Red; term = FFlex (ConstKey c) }
@@ -540,14 +538,23 @@ let mk_clos e t =
| (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
{norm = Red; term = FCLOS(t,e)}
-let mk_clos_vect env v = CArray.Fun1.map mk_clos env v
+(** Hand-unrolling of the map function to bypass the call to the generic array
+ allocation *)
+let mk_clos_vect env v = match v with
+| [||] -> [||]
+| [|v0|] -> [|mk_clos env v0|]
+| [|v0; v1|] -> [|mk_clos env v0; mk_clos env v1|]
+| [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|]
+| [|v0; v1; v2; v3|] ->
+ [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
+| v -> CArray.Fun1.map mk_clos env v
(* Translate the head constructor of t from constr to fconstr. This
function is parameterized by the function to apply on the direct
subterms.
Could be used insted of mk_clos. *)
let mk_clos_deep clos_fun env t =
- match kind_of_term t with
+ match kind t with
| (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) ->
mk_clos env t
| Cast (a,k,b) ->
@@ -646,7 +653,7 @@ let term_of_fconstr =
match v.term with
| FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
| FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
- compose_lam (List.rev tys) f
+ Term.compose_lam (List.rev tys) f
| FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx
| FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx
| _ -> to_constr term_of_fconstr_lift lfts v in
@@ -785,7 +792,7 @@ let drop_parameters depth n argstk =
try try_drop_parameters depth n argstk
with Not_found ->
(* we know that n < stack_args_size(argstk) (if well-typed term) *)
- anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
+ anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.")
(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
to the conversion of the eta expansion of t, considered as an inhabitant
@@ -793,14 +800,14 @@ let drop_parameters depth n argstk =
s.
@assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive
of the constructor term [c]
- @raises Not_found if the inductive is not a primitive record, or if the
+ @raise Not_found if the inductive is not a primitive record, or if the
constructor is partially applied.
*)
let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
| Some (Some (_,projs,pbs)) when
- mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+ mib.Declarations.mind_finite == Declarations.BiFinite ->
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.Declarations.mind_nparams in
@@ -847,6 +854,14 @@ let contract_fix_vect fix =
in
(subs_cons(Array.init nfix make_body, env), thisbody)
+let unfold_projection info p =
+ if red_projection info.i_flags p
+ then
+ let open Declarations in
+ let pb = lookup_projection p (info_env info) in
+ Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
+ else None
+
(*********************************************************************)
(* A machine that inspects the head of a term until it finds an
atom or a subterm that may produce a redex (abstraction,
@@ -865,15 +880,9 @@ let rec knh info m stk =
| (None, stk') -> (m,stk'))
| FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
- let unf = Projection.unfolded p in
- if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
- (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
- | None -> (m, stk)
- | Some pb ->
- knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
- Projection.constant p)
- :: zupdate m stk))
- else (m,stk)
+ (match unfold_projection info p with
+ | None -> (m, stk)
+ | Some s -> knh info c (s :: zupdate m stk))
(* cases where knh stops *)
| (FFlex _|FLetIn _|FConstruct _|FEvar _|
@@ -882,7 +891,7 @@ let rec knh info m stk =
(* The same for pure terms *)
and knht info e t stk =
- match kind_of_term t with
+ match kind t with
| App(a,b) ->
knht info e a (append_stack (mk_clos_vect e b) stk)
| Case(ci,p,t,br) ->
@@ -899,23 +908,23 @@ and knht info e t stk =
(************************************************************************)
(* Computes a weak head normal form from the result of knh. *)
-let rec knr info m stk =
+let rec knr info tab m stk =
match m.term with
| FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
(match get_args n tys f e stk with
- Inl e', s -> knit info e' f s
+ Inl e', s -> knit info tab e' f s
| Inr lam, s -> (lam,s))
| FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) ->
- (match ref_value_cache info (ConstKey c) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (ConstKey c) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
- (match ref_value_cache info (VarKey id) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (VarKey id) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FFlex(RelKey k) when red_set info.i_flags fDELTA ->
- (match ref_value_cache info (RelKey k) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (RelKey k) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FConstruct((ind,c),u) ->
let use_match = red_set info.i_flags fMATCH in
@@ -925,41 +934,44 @@ let rec knr info m stk =
| (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
assert (ci.ci_npar>=0);
let rargs = drop_parameters depth ci.ci_npar args in
- knit info e br.(c-1) (rargs@s)
+ knit info tab e br.(c-1) (rargs@s)
| (_, cargs, Zfix(fx,par)::s) when use_fix ->
let rarg = fapp_stack(m,cargs) in
let stk' = par @ append_stack [|rarg|] s in
let (fxe,fxbd) = contract_fix_vect fx.term in
- knit info fxe fxbd stk'
+ knit info tab fxe fxbd stk'
| (depth, args, Zproj (n, m, cst)::s) when use_match ->
let rargs = drop_parameters depth n args in
let rarg = project_nth_arg m rargs in
- kni info rarg s
+ kni info tab rarg s
| (_,args,s) -> (m,args@s))
else (m,stk)
| FCoFix _ when red_set info.i_flags fCOFIX ->
(match strip_update_shift_app m stk with
(_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
let (fxe,fxbd) = contract_fix_vect m.term in
- knit info fxe fxbd (args@stk')
+ knit info tab fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
- knit info (subs_cons([|v|],e)) bd stk
+ knit info tab (subs_cons([|v|],e)) bd stk
| FEvar(ev,env) ->
(match evar_value info.i_cache ev with
- Some c -> knit info env c stk
+ Some c -> knit info tab env c stk
| None -> (m,stk))
- | _ -> (m,stk)
+ | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
+ | FCLOS _ -> (m, stk)
+
(* Computes the weak head normal form of a term *)
-and kni info m stk =
+and kni info tab m stk =
let (hm,s) = knh info m stk in
- knr info hm s
-and knit info e t stk =
+ knr info tab hm s
+and knit info tab e t stk =
let (ht,s) = knht info e t stk in
- knr info ht s
+ knr info tab ht s
-let kh info v stk = fapp_stack(kni info v stk)
+let kh info tab v stk = fapp_stack(kni info tab v stk)
(************************************************************************)
@@ -987,68 +999,72 @@ let rec zip_term zfun m stk =
1- Calls kni
2- tries to rebuild the term. If a closure still has to be computed,
calls itself recursively. *)
-let rec kl info m =
+let rec kl info tab m =
if is_val m then (incr prune; term_of_fconstr m)
else
- let (nm,s) = kni info m [] in
- let _ = fapp_stack(nm,s) in (* to unlock Zupdates! *)
- zip_term (kl info) (norm_head info nm) s
+ let (nm,s) = kni info tab m [] in
+ let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
+ zip_term (kl info tab) (norm_head info tab nm) s
(* no redex: go up for atoms and already normalized terms, go down
otherwise. *)
-and norm_head info m =
+and norm_head info tab m =
if is_val m then (incr prune; term_of_fconstr m) else
match m.term with
| FLambda(n,tys,f,e) ->
let (e',rvtys) =
List.fold_left (fun (e,ctxt) (na,ty) ->
- (subs_lift e, (na,kl info (mk_clos e ty))::ctxt))
+ (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt))
(e,[]) tys in
- let bd = kl info (mk_clos e' f) in
+ let bd = kl info tab (mk_clos e' f) in
List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
| FLetIn(na,a,b,f,e) ->
let c = mk_clos (subs_lift e) f in
- mkLetIn(na, kl info a, kl info b, kl info c)
+ mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
| FProd(na,dom,rng) ->
- mkProd(na, kl info dom, kl info rng)
+ mkProd(na, kl info tab dom, kl info tab rng)
| FCoFix((n,(na,tys,bds)),e) ->
let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
- mkCoFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+ mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FFix((n,(na,tys,bds)),e) ->
let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
- mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+ mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FEvar((i,args),env) ->
- mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
+ mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
| FProj (p,c) ->
- mkProj (p, kl info c)
- | t -> term_of_fconstr m
+ mkProj (p, kl info tab c)
+ | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+ | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
(* Initialization and then normalization *)
(* weak reduction *)
-let whd_val info v =
- with_stats (lazy (term_of_fconstr (kh info v [])))
+let whd_val info tab v =
+ with_stats (lazy (term_of_fconstr (kh info tab v [])))
(* strong reduction *)
-let norm_val info v =
- with_stats (lazy (kl info v))
+let norm_val info tab v =
+ with_stats (lazy (kl info tab v))
let inject c = mk_clos (subs_id 0) c
-let whd_stack infos m stk =
- let k = kni infos m stk in
- let _ = fapp_stack k in (* to unlock Zupdates! *)
+let whd_stack infos tab m stk =
+ let k = kni infos tab m stk in
+ let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
k
(* cache of constants: the body is computed only when needed. *)
type clos_infos = fconstr infos
let create_clos_infos ?(evars=fun _ -> None) flgs env =
- create (fun _ -> inject) flgs env evars
+ create (fun _ _ c -> inject c) flgs env evars
+
+let create_tab () = KeyTable.create 17
+
let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
let env_of_infos infos = infos.i_cache.i_env
@@ -1056,14 +1072,14 @@ let env_of_infos infos = infos.i_cache.i_env
let infos_with_reds infos reds =
{ infos with i_flags = reds }
-let unfold_reference info key =
+let unfold_reference info tab key =
match key with
| ConstKey (kn,_) ->
if red_set info.i_flags (fCONST kn) then
- ref_value_cache info key
+ ref_value_cache info tab key
else None
| VarKey i ->
if red_set info.i_flags (fVAR i) then
- ref_value_cache info key
+ ref_value_cache info tab key
else None
- | _ -> ref_value_cache info key
+ | _ -> ref_value_cache info tab key
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 22:05:48 +0000