aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/closure.ml')
-rw-r--r--kernel/closure.ml217
1 files changed, 164 insertions, 53 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 7b94ecfb8..fd3ab525e 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -206,32 +206,39 @@ let unfold_red kn =
* instantiations (cbv or lazy) are.
*)
-type table_key = id_key
+type table_key = constant puniverses tableKey
+let eq_pconstant_key (c,u) (c',u') =
+ eq_constant_key c c' && Univ.Instance.eq u u'
+
module IdKeyHash =
struct
- type t = id_key
- let equal = Names.eq_id_key
open Hashset.Combine
+ type t = table_key
+ let equal = Names.eq_table_key eq_pconstant_key
let hash = function
- | ConstKey c -> combinesmall 1 (Constant.UserOrd.hash c)
+ | ConstKey (c, _) -> combinesmall 1 (Constant.UserOrd.hash c)
| VarKey id -> combinesmall 2 (Id.hash id)
| RelKey i -> combinesmall 3 (Int.hash i)
end
module KeyTable = Hashtbl.Make(IdKeyHash)
-let eq_table_key = Names.eq_id_key
+let eq_table_key = IdKeyHash.equal
-type 'a infos = {
- i_flags : reds;
+type 'a infos_cache = {
i_repr : 'a infos -> constr -> 'a;
i_env : env;
i_sigma : existential -> constr option;
i_rels : constr option array;
i_tab : 'a KeyTable.t }
+and 'a infos = {
+ i_flags : reds;
+ i_cache : 'a infos_cache }
+
let info_flags info = info.i_flags
+let info_env info = info.i_cache.i_env
let rec assoc_defined id = function
| [] -> raise Not_found
@@ -239,34 +246,34 @@ let rec assoc_defined id = function
| (id', Some c, _) :: ctxt ->
if Id.equal id id' then c else assoc_defined id ctxt
-let ref_value_cache info ref =
+let ref_value_cache ({i_cache = cache} as infos) ref =
try
- Some (KeyTable.find info.i_tab ref)
+ Some (KeyTable.find cache.i_tab ref)
with Not_found ->
try
let body =
match ref with
| RelKey n ->
- let len = Array.length info.i_rels in
+ 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 info.i_rels i with
+ begin match Array.unsafe_get cache.i_rels i with
| None -> raise Not_found
| Some t -> lift n t
end
- | VarKey id -> assoc_defined id (named_context info.i_env)
- | ConstKey cst -> constant_value info.i_env cst
+ | VarKey id -> assoc_defined id (named_context cache.i_env)
+ | ConstKey cst -> constant_value_in cache.i_env cst
in
- let v = info.i_repr info body in
- KeyTable.add info.i_tab ref v;
+ let v = cache.i_repr infos body in
+ KeyTable.add cache.i_tab ref v;
Some v
with
| Not_found (* List.assoc *)
| NotEvaluableConst _ (* Const *)
-> None
-let evar_value info ev =
- info.i_sigma ev
+let evar_value cache ev =
+ cache.i_sigma ev
let defined_rels flags env =
(* if red_local_const (snd flags) then*)
@@ -282,12 +289,13 @@ let defined_rels flags env =
(* else (0,[])*)
let create mk_cl flgs env evars =
- { i_flags = flgs;
- i_repr = mk_cl;
- i_env = env;
- i_sigma = evars;
- i_rels = defined_rels flgs env;
- i_tab = KeyTable.create 17 }
+ let cache =
+ { i_repr = mk_cl;
+ i_env = env;
+ i_sigma = evars;
+ i_rels = defined_rels flgs env;
+ i_tab = KeyTable.create 17 }
+ in { i_flags = flgs; i_cache = cache }
(**********************************************************************)
@@ -327,9 +335,10 @@ and fterm =
| FAtom of constr (* Metas and Sorts *)
| FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
- | FInd of inductive
- | FConstruct of constructor
+ | FInd of pinductive
+ | FConstruct of pconstructor
| FApp of fconstr * fconstr array
+ | FProj of constant * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCases of case_info * fconstr * fconstr * fconstr array
@@ -362,6 +371,7 @@ let update v1 no t =
type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
+ | Zproj of int * int * constant
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -494,6 +504,9 @@ let rec compact_constr (lg, subs as s) c k =
let (s, f') = compact_constr s f k in
let (s, v') = compact_vect s v k in
if f==f' && v==v' then s, c else s, mkApp(f',v')
+ | Proj (p,t) ->
+ let (s, t') = compact_constr s t k in
+ if t'==t then s, c else s, mkProj (p,t')
| Lambda(n,a,b) ->
let (s, a') = compact_constr s a k in
let (s, b') = compact_constr s b (k+1) in
@@ -559,7 +572,7 @@ let mk_clos e t =
| Meta _ | Sort _ -> { norm = Norm; term = FAtom t }
| Ind kn -> { norm = Norm; term = FInd kn }
| Construct kn -> { norm = Cstr; term = FConstruct kn }
- | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) ->
+ | (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
@@ -578,6 +591,9 @@ let mk_clos_deep clos_fun env t =
| App (f,v) ->
{ norm = Red;
term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) }
+ | Proj (p,c) ->
+ { norm = Red;
+ term = FProj (p, clos_fun env c) }
| Case (ci,p,c,v) ->
{ norm = Red;
term = FCases (ci, clos_fun env p, clos_fun env c,
@@ -609,9 +625,9 @@ let rec to_constr constr_fun lfts v =
| FAtom c -> exliftn lfts c
| FCast (a,k,b) ->
mkCast (constr_fun lfts a, k, constr_fun lfts b)
- | FFlex (ConstKey op) -> mkConst op
- | FInd op -> mkInd op
- | FConstruct op -> mkConstruct op
+ | FFlex (ConstKey op) -> mkConstU op
+ | FInd op -> mkIndU op
+ | FConstruct op -> mkConstructU op
| FCases (ci,p,c,ve) ->
mkCase (ci, constr_fun lfts p,
constr_fun lfts c,
@@ -633,6 +649,9 @@ let rec to_constr constr_fun lfts v =
| FApp (f,ve) ->
mkApp (constr_fun lfts f,
CArray.Fun1.map constr_fun lfts ve)
+ | FProj (p,c) ->
+ mkProj (p,constr_fun lfts c)
+
| FLambda _ ->
let (na,ty,bd) = destFLambda mk_clos2 v in
mkLambda (na, constr_fun lfts ty,
@@ -688,6 +707,8 @@ let rec zip m stk rem = match stk with
| Zcase(ci,p,br)::s ->
let t = FCases(ci, p, m, br) in
zip {norm=neutr m.norm; term=t} s rem
+| Zproj (i,j,cst) :: s ->
+ zip {norm=neutr m.norm; term=FProj (cst,m)} s rem
| Zfix(fx,par)::s ->
zip fx par ((Zapp [|m|] :: s) :: rem)
| Zshift(n)::s ->
@@ -774,7 +795,7 @@ let rec get_args n tys f e stk =
(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
let rec eta_expand_stack = function
- | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+ | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ | Zproj _ as e) :: s ->
e :: eta_expand_stack s
| [] ->
[Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
@@ -808,6 +829,64 @@ let rec drop_parameters depth n argstk =
| _ -> assert false
(* strip_update_shift_app only produces Zapp and Zshift items *)
+let rec get_parameters depth n argstk =
+ match argstk with
+ Zapp args::s ->
+ let q = Array.length args in
+ if n > q then Array.append args (get_parameters depth (n-q) s)
+ else if Int.equal n q then [||]
+ else Array.sub args 0 n
+ | Zshift(k)::s ->
+ get_parameters (depth-k) n s
+ | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
+ if Int.equal n 0 then [||]
+ else raise Not_found (* Trying to eta-expand a partial application..., should do
+ eta expansion first? *)
+ | _ -> assert false
+ (* strip_update_shift_app only produces Zapp and Zshift items *)
+
+let eta_expand_ind_stack env lft (ind,u) m s (lft, h) =
+ let mib = lookup_mind (fst ind) env in
+ match mib.Declarations.mind_record with
+ | None -> raise Not_found
+ | Some (exp,_) ->
+ let pars = mib.Declarations.mind_nparams in
+ let h' = fapp_stack h in
+ let (depth, args, _) = strip_update_shift_app m s in
+ let paramargs = get_parameters depth pars args in
+ let subs = subs_cons (Array.append paramargs [|h'|], subs_id 0) in
+ let fexp = mk_clos subs exp in
+ (lft, (fexp, []))
+
+let eta_expand_ind_stacks env ind m s h =
+ let mib = lookup_mind (fst ind) env in
+ match mib.Declarations.mind_record with
+ | Some (exp,projs) when Array.length projs > 0 ->
+ let pars = mib.Declarations.mind_nparams in
+ let h' = fapp_stack h in
+ let (depth, args, _) = strip_update_shift_app m s in
+ let primitive = Environ.is_projection projs.(0) env in
+ if primitive then
+ let s' = drop_parameters depth pars args in
+ (* Construct, pars1 .. parsm :: arg1...argn :: s ~= (t, []) ->
+ arg1..argn :: s ~= (proj1 t...projn t) s
+ *)
+ let hstack = Array.map (fun p -> { norm = Red;
+ term = FProj (p, h') }) projs in
+ s', [Zapp hstack]
+ else raise Not_found (* disallow eta-exp for non-primitive records *)
+ | _ -> raise Not_found
+
+let rec project_nth_arg n argstk =
+ match argstk with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if n >= q then project_nth_arg (n - q) s
+ else (* n < q *) args.(n)
+ | _ -> assert false
+ (* After drop_parameters we have a purely applicative stack *)
+
+
(* Iota reduction: expansion of a fixpoint.
* Given a fixpoint and a substitution, returns the corresponding
* fixpoint body, and the substitution in which it should be
@@ -832,39 +911,48 @@ let contract_fix_vect fix =
in
(subs_cons(Array.init nfix make_body, env), thisbody)
-
(*********************************************************************)
(* A machine that inspects the head of a term until it finds an
atom or a subterm that may produce a redex (abstraction,
constructor, cofix, letin, constant), or a neutral term (product,
inductive) *)
-let rec knh m stk =
+let rec knh info m stk =
match m.term with
- | FLIFT(k,a) -> knh a (zshift k stk)
- | FCLOS(t,e) -> knht e t (zupdate m stk)
+ | FLIFT(k,a) -> knh info a (zshift k stk)
+ | FCLOS(t,e) -> knht info e t (zupdate m stk)
| FLOCKED -> assert false
- | FApp(a,b) -> knh a (append_stack b (zupdate m stk))
- | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk)
+ | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
+ | FCases(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
| FFix(((ri,n),(_,_,_)),_) ->
(match get_nth_arg m ri.(n) stk with
- (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk')
+ (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
| (None, stk') -> (m,stk'))
- | FCast(t,_,_) -> knh t stk
+ | FCast(t,_,_) -> knh info t stk
+ | FProj (p,c) ->
+ if red_set info.i_flags (fCONST 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, p)
+ :: zupdate m stk))
+ else (m,stk)
+
(* cases where knh stops *)
| (FFlex _|FLetIn _|FConstruct _|FEvar _|
FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) ->
(m, stk)
(* The same for pure terms *)
-and knht e t stk =
+and knht info e t stk =
match kind_of_term t with
| App(a,b) ->
- knht e a (append_stack (mk_clos_vect e b) stk)
+ knht info e a (append_stack (mk_clos_vect e b) stk)
| Case(ci,p,t,br) ->
- knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
- | Fix _ -> knh (mk_clos2 e t) stk
- | Cast(a,_,_) -> knht e a stk
- | Rel n -> knh (clos_rel e n) stk
+ knht info e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
+ | Fix _ -> knh info (mk_clos2 e t) stk
+ | Cast(a,_,_) -> knht info e a stk
+ | Rel n -> knh info (clos_rel e n) stk
+ | Proj (p,c) -> knh info (mk_clos2 e t) stk
| (Lambda _|Prod _|Construct _|CoFix _|Ind _|
LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
(mk_clos2 e t, stk)
@@ -879,8 +967,8 @@ let rec knr info m stk =
(match get_args n tys f e stk with
Inl e', s -> knit info e' f s
| Inr lam, s -> (lam,s))
- | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) ->
- (match ref_value_cache info (ConstKey kn) with
+ | 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
| None -> (set_norm m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
@@ -891,7 +979,7 @@ let rec knr info m stk =
(match ref_value_cache info (RelKey k) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
- | FConstruct(ind,c) when red_set info.i_flags fIOTA ->
+ | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
(match strip_update_shift_app m stk with
(depth, args, Zcase(ci,_,br)::s) ->
assert (ci.ci_npar>=0);
@@ -902,6 +990,10 @@ let rec knr info m stk =
let stk' = par @ append_stack [|rarg|] s in
let (fxe,fxbd) = contract_fix_vect fx.term in
knit info fxe fxbd stk'
+ | (depth, args, Zproj (n, m, cst)::s) ->
+ let rargs = drop_parameters depth n args in
+ let rarg = project_nth_arg m rargs in
+ kni info rarg s
| (_,args,s) -> (m,args@s))
| FCoFix _ when red_set info.i_flags fIOTA ->
(match strip_update_shift_app m stk with
@@ -912,17 +1004,17 @@ let rec knr info m stk =
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
knit info (subs_cons([|v|],e)) bd stk
| FEvar(ev,env) ->
- (match evar_value info ev with
+ (match evar_value info.i_cache ev with
Some c -> knit info env c stk
| None -> (m,stk))
| _ -> (m,stk)
(* Computes the weak head normal form of a term *)
and kni info m stk =
- let (hm,s) = knh m stk in
+ let (hm,s) = knh info m stk in
knr info hm s
and knit info e t stk =
- let (ht,s) = knht e t stk in
+ let (ht,s) = knht info e t stk in
knr info ht s
let kh info v stk = fapp_stack(kni info v stk)
@@ -937,6 +1029,9 @@ let rec zip_term zfun m stk =
| Zcase(ci,p,br)::s ->
let t = mkCase(ci, zfun p, m, Array.map zfun br) in
zip_term zfun t s
+ | Zproj(_,_,p)::s ->
+ let t = mkProj (p, m) in
+ 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
@@ -985,6 +1080,8 @@ and norm_head info m =
mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
| FEvar((i,args),env) ->
mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
+ | FProj (p,c) ->
+ mkProj (p, kl info c)
| t -> term_of_fconstr m
(* Initialization and then normalization *)
@@ -1009,6 +1106,20 @@ type clos_infos = fconstr infos
let create_clos_infos ?(evars=fun _ -> None) flgs env =
create (fun _ -> inject) flgs env evars
-let oracle_of_infos { i_env } = Environ.oracle i_env
-
-let unfold_reference = ref_value_cache
+let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
+
+let infos_with_reds infos reds =
+ { infos with i_flags = reds }
+
+let unfold_reference info key =
+ match key with
+ | ConstKey (kn,_) ->
+ if red_set info.i_flags (fCONST kn) then
+ ref_value_cache info key
+ else None
+ | VarKey i ->
+ if red_set info.i_flags (fVAR i) then
+ ref_value_cache info key
+ else None
+ | _ -> ref_value_cache info key
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 06:57:08 +0000