summaryrefslogtreecommitdiff
path: root/kernel/closure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/closure.ml')
-rw-r--r--kernel/closure.ml523
1 files changed, 310 insertions, 213 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 9e2af94b..f06b13d8 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -19,11 +19,12 @@
(* This file implements a lazy reduction for the Calculus of Inductive
Constructions *)
+open Errors
open Util
open Pp
-open Term
open Names
-open Declarations
+open Term
+open Vars
open Environ
open Esubst
@@ -33,6 +34,7 @@ let share = ref true
(* Profiling *)
let beta = ref 0
let delta = ref 0
+let eta = ref 0
let zeta = ref 0
let evar = ref 0
let iota = ref 0
@@ -43,9 +45,10 @@ let reset () =
prune := 0
let stop() =
- msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
- str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
- str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
+ msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+ str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
+ int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++
+ str"]")
let incr_cnt red cnt =
if red then begin
@@ -63,10 +66,10 @@ let with_stats c =
end else
Lazy.force c
-let all_opaque = (Idpred.empty, Cpred.empty)
-let all_transparent = (Idpred.full, Cpred.full)
+let all_opaque = (Id.Pred.empty, Cpred.empty)
+let all_transparent = (Id.Pred.full, Cpred.full)
-let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
module type RedFlagsSig = sig
@@ -74,16 +77,18 @@ module type RedFlagsSig = sig
type red_kind
val fBETA : red_kind
val fDELTA : red_kind
+ val fETA : red_kind
val fIOTA : red_kind
val fZETA : red_kind
val fCONST : constant -> red_kind
- val fVAR : identifier -> 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 mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
+ val red_projection : reds -> projection -> bool
end
module RedFlags = (struct
@@ -95,14 +100,16 @@ module RedFlags = (struct
type reds = {
r_beta : bool;
r_delta : bool;
+ r_eta : bool;
r_const : transparent_state;
r_zeta : bool;
r_iota : bool }
- type red_kind = BETA | DELTA | IOTA | ZETA
- | CONST of constant | VAR of identifier
+ type red_kind = BETA | DELTA | ETA | IOTA | ZETA
+ | CONST of constant | VAR of Id.t
let fBETA = BETA
let fDELTA = DELTA
+ let fETA = ETA
let fIOTA = IOTA
let fZETA = ZETA
let fCONST kn = CONST kn
@@ -110,12 +117,14 @@ module RedFlags = (struct
let no_red = {
r_beta = false;
r_delta = false;
+ r_eta = false;
r_const = all_opaque;
r_zeta = false;
r_iota = false }
let red_add red = function
| BETA -> { red with r_beta = true }
+ | ETA -> { red with r_eta = true }
| DELTA -> { red with r_delta = true; r_const = all_transparent }
| CONST kn ->
let (l1,l2) = red.r_const in
@@ -124,10 +133,11 @@ module RedFlags = (struct
| ZETA -> { red with r_zeta = true }
| VAR id ->
let (l1,l2) = red.r_const in
- { red with r_const = Idpred.add id l1, l2 }
+ { red with r_const = Id.Pred.add id l1, l2 }
let red_sub red = function
| BETA -> { red with r_beta = false }
+ | ETA -> { red with r_eta = false }
| DELTA -> { red with r_delta = false }
| CONST kn ->
let (l1,l2) = red.r_const in
@@ -136,7 +146,7 @@ module RedFlags = (struct
| ZETA -> { red with r_zeta = false }
| VAR id ->
let (l1,l2) = red.r_const in
- { red with r_const = Idpred.remove id l1, l2 }
+ { red with r_const = Id.Pred.remove id l1, l2 }
let red_add_transparent red tr =
{ red with r_const = tr }
@@ -145,19 +155,24 @@ module RedFlags = (struct
let red_set red = function
| BETA -> incr_cnt red.r_beta beta
+ | ETA -> incr_cnt red.r_eta eta
| CONST kn ->
let (_,l) = red.r_const in
let c = Cpred.mem kn l in
incr_cnt c delta
| VAR id -> (* En attendant d'avoir des kn pour les Var *)
let (l,_) = red.r_const in
- let c = Idpred.mem id l in
+ let c = Id.Pred.mem id l in
incr_cnt c delta
| ZETA -> incr_cnt red.r_zeta zeta
| IOTA -> incr_cnt red.r_iota iota
| DELTA -> (* Used for Rel/Var defined in context *)
incr_cnt red.r_delta delta
+ let red_projection red p =
+ if Projection.unfolded p then true
+ else red_set red (fCONST (Projection.constant p))
+
end : RedFlagsSig)
open RedFlags
@@ -185,9 +200,8 @@ let unfold_red kn =
* * i_repr is the function to get the representation from the current
* state of the cache and the body of the constant. The result
* is stored in the table.
- * * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables
- * and only those with index 1 and 3 have bodies which are c and d resp.
- * * i_vars is the list of _defined_ named variables.
+ * * i_rels is the array of free rel variables together with their optional
+ * body
*
* ref_value_cache searchs in the tab, otherwise uses i_repr to
* compute the result and store it in the table. If the constant can't
@@ -197,72 +211,96 @@ 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.equal u u'
+
+module IdKeyHash =
+struct
+ 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)
+ | VarKey id -> combinesmall 2 (Id.hash id)
+ | RelKey i -> combinesmall 3 (Int.hash i)
+end
-let eq_table_key = Names.eq_id_key
+module KeyTable = Hashtbl.Make(IdKeyHash)
-type 'a infos = {
- i_flags : reds;
+let eq_table_key = IdKeyHash.equal
+
+type 'a infos_cache = {
i_repr : 'a infos -> constr -> 'a;
i_env : env;
i_sigma : existential -> constr option;
- i_rels : int * (int * constr) list;
- i_vars : (identifier * constr) list;
- i_tab : (table_key, 'a) Hashtbl.t }
+ 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 ref_value_cache info ref =
+let rec assoc_defined id = function
+| [] -> raise Not_found
+| (_, None, _) :: ctxt -> assoc_defined id ctxt
+| (id', Some c, _) :: ctxt ->
+ if Id.equal id id' then c else assoc_defined id ctxt
+
+let ref_value_cache ({i_cache = cache} as infos) ref =
try
- Some (Hashtbl.find info.i_tab ref)
+ Some (KeyTable.find cache.i_tab ref)
with Not_found ->
try
let body =
match ref with
| RelKey n ->
- let (s,l) = info.i_rels in lift n (List.assoc (s-n) l)
- | VarKey id -> List.assoc id info.i_vars
- | ConstKey cst -> constant_value info.i_env cst
+ 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
+ | 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
- Hashtbl.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 defined_vars flags env =
-(* if red_local_const (snd flags) then*)
- Sign.fold_named_context
- (fun (id,b,_) e ->
- match b with
- | None -> e
- | Some body -> (id, body)::e)
- (named_context env) ~init:[]
-(* else []*)
+let evar_value cache ev =
+ cache.i_sigma ev
let defined_rels flags env =
(* if red_local_const (snd flags) then*)
- Sign.fold_rel_context
- (fun (id,b,t) (i,subs) ->
- match b with
- | None -> (i+1, subs)
- | Some body -> (i+1, (i,body) :: subs))
- (rel_context env) ~init:(0,[])
+ let ctx = rel_context env in
+ let len = List.length ctx in
+ let ans = Array.make len None in
+ let iter i (_, b, _) = match b with
+ | None -> ()
+ | Some _ -> Array.unsafe_set ans i b
+ in
+ let () = List.iteri iter ctx in
+ ans
(* 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_vars = defined_vars flgs env;
- i_tab = Hashtbl.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 }
(**********************************************************************)
@@ -302,15 +340,17 @@ 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 projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCases of case_info * fconstr * fconstr * fconstr array
- | FLambda of int * (name * constr) list * constr * fconstr subs
- | FProd of name * fconstr * fconstr
- | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+ | FCase of case_info * fconstr * fconstr * fconstr array
+ | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
+ | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+ | FProd of Name.t * fconstr * fconstr
+ | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
| FEvar of existential * fconstr subs
| FLIFT of int * fconstr
| FCLOS of constr * fconstr subs
@@ -318,13 +358,13 @@ and fterm =
let fterm_of v = v.term
let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
+let is_val v = match v.norm with Norm -> true | _ -> false
let mk_atom c = {norm=Norm;term=FAtom c}
(* Could issue a warning if no is still Red, pointing out that we loose
sharing. *)
-let update v1 (no,t) =
+let update v1 no t =
if !share then
(v1.norm <- no;
v1.term <- t;
@@ -337,6 +377,8 @@ let update v1 (no,t) =
type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
+ | ZcaseT of case_info * constr * constr array * fconstr subs
+ | Zproj of int * int * constant
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -345,7 +387,7 @@ and stack = stack_member list
let empty_stack = []
let append_stack v s =
- if Array.length v = 0 then s else
+ if Int.equal (Array.length v) 0 then s else
match s with
| Zapp l :: s -> Zapp (Array.append v l) :: s
| _ -> Zapp v :: s
@@ -389,7 +431,7 @@ let rec stack_assign s p c = match s with
Zapp nargs :: s)
| _ -> s
let rec stack_tail p s =
- if p = 0 then s else
+ if Int.equal p 0 then s else
match s with
| Zapp args :: s ->
let q = Array.length args in
@@ -417,9 +459,9 @@ let rec lft_fconstr n ft =
| FLOCKED -> assert false
| _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
- if k=0 then f else lft_fconstr k f
+ if Int.equal k 0 then f else lft_fconstr k f
let lift_fconstr_vect k v =
- if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
+ if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v
let clos_rel e i =
match expand_rel i e with
@@ -436,88 +478,21 @@ let compact_stack head stk =
(* Be sure to create a new cell otherwise sharing would be
lost by the update operation *)
let h' = lft_fconstr depth head in
- let _ = update m (h'.norm,h'.term) in
+ let _ = update m h'.norm h'.term in
strip_rec depth s
| stk -> zshift depth stk in
strip_rec 0 stk
(* Put an update mark in the stack, only if needed *)
let zupdate m s =
- if !share & m.norm = Red
+ if !share && begin match m.norm with Red -> true | _ -> false end
then
let s' = compact_stack m s in
let _ = m.term <- FLOCKED in
Zupdate(m)::s'
else s
-(* Closure optimization: *)
-let rec compact_constr (lg, subs as s) c k =
- match kind_of_term c with
- Rel i ->
- if i < k then c,s else
- (try mkRel (k + lg - list_index (i-k+1) subs), (lg,subs)
- with Not_found -> mkRel (k+lg), (lg+1, (i-k+1)::subs))
- | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
- | Evar(ev,v) ->
- let (v',s) = compact_vect s v k in
- if v==v' then c,s else mkEvar(ev,v'),s
- | Cast(a,ck,b) ->
- let (a',s) = compact_constr s a k in
- let (b',s) = compact_constr s b k in
- if a==a' && b==b' then c,s else mkCast(a', ck, b'), s
- | App(f,v) ->
- let (f',s) = compact_constr s f k in
- let (v',s) = compact_vect s v k in
- if f==f' && v==v' then c,s else mkApp(f',v'), s
- | Lambda(n,a,b) ->
- let (a',s) = compact_constr s a k in
- let (b',s) = compact_constr s b (k+1) in
- if a==a' && b==b' then c,s else mkLambda(n,a',b'), s
- | Prod(n,a,b) ->
- let (a',s) = compact_constr s a k in
- let (b',s) = compact_constr s b (k+1) in
- if a==a' && b==b' then c,s else mkProd(n,a',b'), s
- | LetIn(n,a,ty,b) ->
- let (a',s) = compact_constr s a k in
- let (ty',s) = compact_constr s ty k in
- let (b',s) = compact_constr s b (k+1) in
- if a==a' && ty==ty' && b==b' then c,s else mkLetIn(n,a',ty',b'), s
- | Fix(fi,(na,ty,bd)) ->
- let (ty',s) = compact_vect s ty k in
- let (bd',s) = compact_vect s bd (k+Array.length ty) in
- if ty==ty' && bd==bd' then c,s else mkFix(fi,(na,ty',bd')), s
- | CoFix(i,(na,ty,bd)) ->
- let (ty',s) = compact_vect s ty k in
- let (bd',s) = compact_vect s bd (k+Array.length ty) in
- if ty==ty' && bd==bd' then c,s else mkCoFix(i,(na,ty',bd')), s
- | Case(ci,p,a,br) ->
- let (p',s) = compact_constr s p k in
- let (a',s) = compact_constr s a k in
- let (br',s) = compact_vect s br k in
- if p==p' && a==a' && br==br' then c,s else mkCase(ci,p',a',br'),s
-and compact_vect s v k = compact_v [] s v k (Array.length v - 1)
-and compact_v acc s v k i =
- if i < 0 then
- let v' = Array.of_list acc in
- if array_for_all2 (==) v v' then v,s else v',s
- else
- let (a',s') = compact_constr s v.(i) k in
- compact_v (a'::acc) s' v k (i-1)
-
-(* Computes the minimal environment of a closure.
- Idea: if the subs is not identity, the term will have to be
- reallocated entirely (to propagate the substitution). So,
- computing the set of free variables does not change the
- complexity. *)
-let optimise_closure env c =
- if is_subs_id env then (env,c) else
- let (c',(_,s)) = compact_constr (0,[]) c 1 in
- let env' =
- Array.map (fun i -> clos_rel env i) (Array.of_list s) in
- (subs_cons (env', subs_id 0),c')
-
let mk_lambda env t =
- let (env,t) = optimise_closure env t in
let (rvars,t') = decompose_lam t in
FLambda(List.length rvars, List.rev rvars, t', env)
@@ -539,10 +514,10 @@ 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 = Array.map (mk_clos env) v
+let mk_clos_vect env 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
@@ -557,11 +532,13 @@ let mk_clos_deep clos_fun env t =
term = FCast (clos_fun env a, k, clos_fun env b)}
| App (f,v) ->
{ norm = Red;
- term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
+ 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,
- Array.map (clos_fun env) v) }
+ term = FCaseT (ci, p, clos_fun env c, v, env) }
| Fix fx ->
{ norm = Cstr; term = FFix (fx, env) }
| CoFix cfx ->
@@ -589,30 +566,37 @@ 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
- | FCases (ci,p,c,ve) ->
+ | FFlex (ConstKey op) -> mkConstU op
+ | FInd op -> mkIndU op
+ | FConstruct op -> mkConstructU op
+ | FCase (ci,p,c,ve) ->
mkCase (ci, constr_fun lfts p,
constr_fun lfts c,
- Array.map (constr_fun lfts) ve)
+ CArray.Fun1.map constr_fun lfts ve)
+ | FCaseT (ci,p,c,ve,env) ->
+ mkCase (ci, constr_fun lfts (mk_clos env p),
+ constr_fun lfts c,
+ Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
| FFix ((op,(lna,tys,bds)),e) ->
let n = Array.length bds in
- let ftys = Array.map (mk_clos e) tys in
- let fbds = Array.map (mk_clos (subs_liftn n e)) bds in
+ let ftys = CArray.Fun1.map mk_clos e tys in
+ let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
let lfts' = el_liftn n lfts in
- mkFix (op, (lna, Array.map (constr_fun lfts) ftys,
- Array.map (constr_fun lfts') fbds))
+ mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
+ CArray.Fun1.map constr_fun lfts' fbds))
| FCoFix ((op,(lna,tys,bds)),e) ->
let n = Array.length bds in
- let ftys = Array.map (mk_clos e) tys in
- let fbds = Array.map (mk_clos (subs_liftn n e)) bds in
+ let ftys = CArray.Fun1.map mk_clos e tys in
+ let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
let lfts' = el_liftn (Array.length bds) lfts in
- mkCoFix (op, (lna, Array.map (constr_fun lfts) ftys,
- Array.map (constr_fun lfts') fbds))
+ mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
+ CArray.Fun1.map constr_fun lfts' fbds))
| FApp (f,ve) ->
mkApp (constr_fun lfts f,
- Array.map (constr_fun lfts) ve)
+ 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,
@@ -630,9 +614,9 @@ let rec to_constr constr_fun lfts v =
| FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
| FCLOS (t,env) ->
let fr = mk_clos2 env t in
- let unfv = update v (fr.norm,fr.term) in
+ let unfv = update v fr.norm fr.term in
to_constr constr_fun lfts unfv
- | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*)
+ | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
(* This function defines the correspondance between constr and
fconstr. When we find a closure whose substitution is the identity,
@@ -641,11 +625,11 @@ let rec to_constr constr_fun lfts v =
let term_of_fconstr =
let rec term_of_fconstr_lift lfts v =
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 ->
+ | 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
- | 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
+ | 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
term_of_fconstr_lift el_id
@@ -663,14 +647,19 @@ let rec zip m stk =
| [] -> m
| Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
| Zcase(ci,p,br)::s ->
- let t = FCases(ci, p, m, br) in
+ let t = FCase(ci, p, m, br) in
+ zip {norm=neutr m.norm; term=t} s
+ | ZcaseT(ci,p,br,e)::s ->
+ let t = FCaseT(ci, p, m, br, e) in
zip {norm=neutr m.norm; term=t} s
+ | Zproj (i,j,cst) :: s ->
+ zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s
| Zfix(fx,par)::s ->
zip fx (par @ append_stack [|m|] s)
| Zshift(n)::s ->
zip (lift_fconstr n m) s
| Zupdate(rf)::s ->
- zip (update rf (m.norm,m.term)) s
+ zip (update rf m.norm m.term) s
let fapp_stack (m,stk) = zip m stk
@@ -682,8 +671,7 @@ let fapp_stack (m,stk) = zip m stk
(strip_update_shift, through get_arg). *)
(* optimised for the case where there are no shifts... *)
-let strip_update_shift_app head stk =
- assert (head.norm <> Red);
+let strip_update_shift_app_red head stk =
let rec strip_rec rstk h depth = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
@@ -691,13 +679,16 @@ let strip_update_shift_app head stk =
strip_rec (Zapp args :: rstk)
{norm=h.norm;term=FApp(h,args)} depth s
| Zupdate(m)::s ->
- strip_rec rstk (update m (h.norm,h.term)) depth s
+ strip_rec rstk (update m h.norm h.term) depth s
| stk -> (depth,List.rev rstk, stk) in
strip_rec [] head 0 stk
+let strip_update_shift_app head stack =
+ assert (match head.norm with Red -> false | _ -> true);
+ strip_update_shift_app_red head stack
let get_nth_arg head n stk =
- assert (head.norm <> Red);
+ assert (match head.norm with Red -> false | _ -> true);
let rec strip_rec rstk h n = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) n s
@@ -710,10 +701,10 @@ let get_nth_arg head n stk =
let bef = Array.sub args 0 n in
let aft = Array.sub args (n+1) (q-n-1) in
let stk' =
- List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
+ List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in
(Some (stk', args.(n)), append_stack aft s')
| Zupdate(m)::s ->
- strip_rec rstk (update m (h.norm,h.term)) n s
+ strip_rec rstk (update m h.norm h.term) n s
| s -> (None, List.rev rstk @ s) in
strip_rec [] head n stk
@@ -722,7 +713,7 @@ let get_nth_arg head n stk =
let rec get_args n tys f e stk =
match stk with
Zupdate r :: s ->
- let _hd = update r (Cstr,FLambda(n,tys,f,e)) in
+ let _hd = update r Cstr (FLambda(n,tys,f,e)) in
get_args n tys f e s
| Zshift k :: s ->
get_args n tys f (subs_shft (k,e)) s
@@ -734,13 +725,14 @@ let rec get_args n tys f e stk =
let eargs = Array.sub l n (na-n) in
(Inl (subs_cons(args,e)), Zapp eargs :: s)
else (* more lambdas *)
- let etys = list_skipn na tys in
+ let etys = List.skipn na tys in
get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(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 _ | ZcaseT _ | Zproj _
+ | Zshift _ | Zupdate _ as e) :: s ->
e :: eta_expand_stack s
| [] ->
[Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
@@ -751,29 +743,88 @@ let rec reloc_rargs_rec depth stk =
match stk with
Zapp args :: s ->
Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s
- | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
+ | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s
| _ -> stk
let reloc_rargs depth stk =
- if depth = 0 then stk else reloc_rargs_rec depth stk
+ if Int.equal depth 0 then stk else reloc_rargs_rec depth stk
-let rec drop_parameters depth n argstk =
+let rec try_drop_parameters depth n argstk =
match argstk with
Zapp args::s ->
let q = Array.length args in
- if n > q then drop_parameters depth (n-q) s
- else if n = q then reloc_rargs depth s
+ if n > q then try_drop_parameters depth (n-q) s
+ else if Int.equal n q then reloc_rargs depth s
else
let aft = Array.sub args n (q-n) in
reloc_rargs depth (append_stack aft s)
- | Zshift(k)::s -> drop_parameters (depth-k) n s
+ | Zshift(k)::s -> try_drop_parameters (depth-k) n s
+ | [] ->
+ if Int.equal n 0 then []
+ else raise Not_found
+ | _ -> assert false
+ (* strip_update_shift_app only produces Zapp and Zshift items *)
+
+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")
+
+
+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 n=0 then []
- else anomaly
- "ill-typed term: found a match on a partially applied constructor"
+ 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 *)
+
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
+ to the conversion of the eta expansion of t, considered as an inhabitant
+ of ind, and the Constructor c of this inductive type applied to arguments
+ 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
+ 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.CoFinite ->
+ (* (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
+ let right = fapp_stack (f, s') in
+ let (depth, args, s) = strip_update_shift_app m s in
+ (** Try to drop the params, might fail on partially applied constructors. *)
+ let argss = try_drop_parameters depth pars args in
+ let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+ term = FProj (Projection.make p true, right) }) projs in
+ argss, [Zapp hstack]
+ | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+
+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
@@ -798,39 +849,51 @@ 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))
+ | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
+ | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::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) ->
+ 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)
+
(* 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 (ZcaseT(ci, p, br, e)::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)
@@ -845,8 +908,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) ->
@@ -857,38 +920,46 @@ 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);
let rargs = drop_parameters depth ci.ci_npar args in
kni info br.(c-1) (rargs@s)
+ | (depth, args, ZcaseT(ci,_,br,e)::s) ->
+ assert (ci.ci_npar>=0);
+ let rargs = drop_parameters depth ci.ci_npar args in
+ knit info e br.(c-1) (rargs@s)
| (_, cargs, Zfix(fx,par)::s) ->
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'
+ | (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
- (_, args, ((Zcase _::_) as stk')) ->
+ (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
let (fxe,fxbd) = contract_fix_vect m.term in
knit info 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
| 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)
@@ -903,6 +974,13 @@ 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
+ | 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
+ zip_term zfun t s
+ | Zproj(_,_,p)::s ->
+ let t = mkProj (Projection.make p true, 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
@@ -940,17 +1018,19 @@ and norm_head info m =
| FProd(na,dom,rng) ->
mkProd(na, kl info dom, kl info rng)
| FCoFix((n,(na,tys,bds)),e) ->
- let ftys = Array.map (mk_clos e) tys in
+ let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
- Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
- mkCoFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) 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))
| FFix((n,(na,tys,bds)),e) ->
- let ftys = Array.map (mk_clos e) tys in
+ let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
- Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
- mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) 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))
| 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 *)
@@ -963,7 +1043,7 @@ let whd_val info v =
let norm_val info v =
with_stats (lazy (kl info v))
-let inject = mk_clos (subs_id 0)
+let inject c = mk_clos (subs_id 0) c
let whd_stack infos m stk =
let k = kni infos m stk in
@@ -975,5 +1055,22 @@ type clos_infos = fconstr infos
let create_clos_infos ?(evars=fun _ -> None) flgs env =
create (fun _ -> inject) flgs env evars
-
-let unfold_reference = ref_value_cache
+let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
+
+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 =
+ 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 2025-01-01 08:23:05 +0000