From cf95f2a791c263c7aaa3b488d1b09eaafc29be2b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 16:30:32 +0200 Subject: closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a --- dev/printers.mllib | 2 +- dev/top_printers.ml | 4 +- kernel/cClosure.ml | 1071 +++++++++++++++++++++++ kernel/cClosure.mli | 244 ++++++ kernel/closure.ml | 1072 ------------------------ kernel/closure.mli | 244 ------ kernel/kernel.mllib | 2 +- kernel/reduction.ml | 6 +- ltac/rewrite.ml | 2 +- plugins/cc/cctac.ml | 8 +- plugins/decl_mode/decl_interp.ml | 4 +- plugins/decl_mode/decl_proof_instr.ml | 8 +- plugins/firstorder/formula.ml | 10 +- plugins/firstorder/formula.mli | 2 +- plugins/firstorder/ground.ml | 4 +- plugins/funind/functional_principles_proofs.ml | 6 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/recdef.ml | 6 +- plugins/rtauto/refl_tauto.ml | 8 +- plugins/setoid_ring/newring.ml | 2 +- pretyping/cbv.ml | 2 +- pretyping/cbv.mli | 2 +- pretyping/evarconv.ml | 2 +- pretyping/reductionops.ml | 78 +- pretyping/reductionops.mli | 6 +- pretyping/tacred.ml | 2 +- pretyping/tacred.mli | 2 +- pretyping/unification.ml | 6 +- proofs/redexpr.ml | 2 +- toplevel/obligations.ml | 2 +- toplevel/vernacentries.ml | 4 +- 32 files changed, 1408 insertions(+), 1409 deletions(-) create mode 100644 kernel/cClosure.ml create mode 100644 kernel/cClosure.mli delete mode 100644 kernel/closure.ml delete mode 100644 kernel/closure.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 9b4998c67..a2a7437fb 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -86,7 +86,7 @@ Nativecode Nativelib Cbytegen Environ -Closure +CClosure Reduction Nativeconv Type_errors diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7c010e6a4..023835af7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -80,7 +80,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; @@ -457,7 +457,7 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml new file mode 100644 index 000000000..d475f097c --- /dev/null +++ b/kernel/cClosure.ml @@ -0,0 +1,1071 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + + (* [r_const=(true,cl)] means all constants but those in [cl] *) + (* [r_const=(false,cl)] means only those in [cl] *) + (* [r_delta=true] just mean [r_const=(true,[])] *) + + type reds = { + r_beta : bool; + r_delta : bool; + r_eta : bool; + r_const : transparent_state; + r_zeta : bool; + r_match : bool; + r_fix : bool; + r_cofix : bool } + + type red_kind = BETA | DELTA | ETA | MATCH | FIX + | COFIX | ZETA + | CONST of constant | VAR of Id.t + let fBETA = BETA + let fDELTA = DELTA + let fETA = ETA + let fMATCH = MATCH + let fFIX = FIX + let fCOFIX = COFIX + let fZETA = ZETA + let fCONST kn = CONST kn + let fVAR id = VAR id + let no_red = { + r_beta = false; + r_delta = false; + r_eta = false; + r_const = all_opaque; + r_zeta = false; + r_match = false; + r_fix = false; + r_cofix = 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 + { red with r_const = l1, Cpred.add kn l2 } + | MATCH -> { red with r_match = true } + | FIX -> { red with r_fix = true } + | COFIX -> { red with r_cofix = true } + | ZETA -> { red with r_zeta = true } + | VAR id -> + let (l1,l2) = red.r_const in + { 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 + { red with r_const = l1, Cpred.remove kn l2 } + | MATCH -> { red with r_match = false } + | FIX -> { red with r_fix = false } + | COFIX -> { red with r_cofix = false } + | ZETA -> { red with r_zeta = false } + | VAR id -> + let (l1,l2) = red.r_const in + { red with r_const = Id.Pred.remove id l1, l2 } + + let red_add_transparent red tr = + { red with r_const = tr } + + let mkflags = List.fold_left red_add no_red + + 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 = Id.Pred.mem id l in + 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 + + let red_projection red p = + if Projection.unfolded p then true + else red_set red (fCONST (Projection.constant p)) + +end : RedFlagsSig) + +open RedFlags + +let all = mkflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX] +let allnolet = mkflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX] +let beta = mkflags [fBETA] +let betadeltazeta = mkflags [fBETA;fDELTA;fZETA] +let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX] +let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let betazeta = mkflags [fBETA;fZETA] +let delta = mkflags [fDELTA] +let zeta = mkflags [fZETA] +let nored = no_red + +(* Removing fZETA for finer behaviour would break many developments *) +let unfold_side_flags = [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let unfold_side_red = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let unfold_red kn = + let flag = match kn with + | EvalVarRef id -> fVAR id + | EvalConstRef kn -> fCONST kn in + mkflags (flag::unfold_side_flags) + +(* Flags of reduction and cache of constants: 'a is a type that may be + * mapped to constr. 'a infos implements a cache for constants and + * abstractions, storing a representation (of type 'a) of the body of + * this constant or abstraction. + * * i_tab is the cache table of the results + * * 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 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 + * be unfolded, returns None, but does not store this failure. * This + * doesn't take the RESET into account. You mustn't keep such a table + * after a Reset. * This type is not exported. Only its two + * instantiations (cbv or lazy) are. + *) + +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 + +module KeyTable = Hashtbl.Make(IdKeyHash) + +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 : 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 + +open Context.Named.Declaration + +let rec assoc_defined id = function +| [] -> raise Not_found +| LocalAssum _ :: ctxt -> assoc_defined id ctxt +| LocalDef (id', 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 (KeyTable.find cache.i_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 + | VarKey id -> assoc_defined id (named_context 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; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + +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 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 } + + +(**********************************************************************) +(* Lazy reduction: the one used in kernel operations *) + +(* type of shared terms. fconstr and frterm are mutually recursive. + * Clone of the constr structure, but completely mutable, and + * annotated with reduction state (reducible or not). + * - FLIFT is a delayed shift; allows sharing between 2 lifted copies + * of a given term. + * - FCLOS is a delayed substitution applied to a constr + * - FLOCKED is used to erase the content of a reference that must + * be updated. This is to allow the garbage collector to work + * before the term is computed. + *) + +(* Norm means the term is fully normalized and cannot create a redex + when substituted + Cstr means the term is in head normal form and that it can + create a redex when substituted (i.e. constructor, fix, lambda) + Whnf means we reached the head normal form and that it cannot + create a redex when substituted + Red is used for terms that might be reduced +*) +type red_state = Norm | Cstr | Whnf | Red + +let neutr = function + | (Whnf|Norm) -> Whnf + | (Red|Cstr) -> Red + +type fconstr = { + mutable norm: red_state; + mutable term: fterm } + +and fterm = + | FRel of int + | FAtom of constr (* Metas and Sorts *) + | FCast of fconstr * cast_kind * fconstr + | FFlex of table_key + | 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 + | 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 + | FLOCKED + +let fterm_of v = v.term +let set_norm v = v.norm <- Norm +let is_val v = match v.norm with Norm -> true | _ -> false + +let mk_atom c = {norm=Norm;term=FAtom c} +let mk_red f = {norm=Red;term=f} + +(* Could issue a warning if no is still Red, pointing out that we loose + sharing. *) +let update v1 no t = + if !share then + (v1.norm <- no; + v1.term <- t; + v1) + else {norm=no;term=t} + +(**********************************************************************) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) + +type stack_member = + | Zapp of 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 + +and stack = stack_member list + +let empty_stack = [] +let append_stack v s = + 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 + +(* Collapse the shifts in the stack *) +let zshift n s = + match (n,s) with + (0,_) -> s + | (_,Zshift(k)::s) -> Zshift(n+k)::s + | _ -> Zshift(n)::s + +let rec stack_args_size = function + | Zapp v :: s -> Array.length v + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + +(* When used as an argument stack (only Zapp can appear) *) +let rec decomp_stack = function + | Zapp v :: s -> + (match Array.length v with + 0 -> decomp_stack s + | 1 -> Some (v.(0), s) + | _ -> + Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) + | _ -> None +let array_of_stack s = + let rec stackrec = function + | [] -> [] + | Zapp args :: s -> args :: (stackrec s) + | _ -> assert false + in Array.concat (stackrec s) +let rec stack_assign s p c = match s with + | Zapp args :: s -> + let q = Array.length args in + if p >= q then + Zapp args :: stack_assign s (p-q) c + else + (let nargs = Array.copy args in + nargs.(p) <- c; + Zapp nargs :: s) + | _ -> s +let rec stack_tail p s = + if Int.equal p 0 then s else + match s with + | Zapp args :: s -> + let q = Array.length args in + if p >= q then stack_tail (p-q) s + else Zapp (Array.sub args p (q-p)) :: s + | _ -> failwith "stack_tail" +let rec stack_nth s p = match s with + | Zapp args :: s -> + let q = Array.length args in + if p >= q then stack_nth s (p-q) + else args.(p) + | _ -> raise Not_found + +(* Lifting. Preserves sharing (useful only for cell with norm=Red). + lft_fconstr always create a new cell, while lift_fconstr avoids it + when the lift is 0. *) +let rec lft_fconstr n ft = + match ft.term with + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft + | FRel i -> {norm=Norm;term=FRel(i+n)} + | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))} + | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))} + | 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)} +let lift_fconstr k f = + if Int.equal k 0 then f else lft_fconstr k f +let lift_fconstr_vect k 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 + | Inl(n,mt) -> lift_fconstr n mt + | Inr(k,None) -> {norm=Norm; term= FRel k} + | Inr(k,Some p) -> + lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)} + +(* since the head may be reducible, we might introduce lifts of 0 *) +let compact_stack head stk = + let rec strip_rec depth = function + | Zshift(k)::s -> strip_rec (depth+k) s + | Zupdate(m)::s -> + (* 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 + 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 && 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 + +let mk_lambda env t = + let (rvars,t') = decompose_lam t in + FLambda(List.length rvars, List.rev rvars, t', env) + +let destFLambda clos_fun t = + match t.term with + FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) + | FLambda(n,(na,ty)::tys,b,e) -> + (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) + | _ -> assert false + (* t must be a FLambda and binding list cannot be empty *) + +(* Optimization: do not enclose variables in a closure. + Makes variable access much faster *) +let mk_clos e t = + match kind_of_term t with + | Rel i -> clos_rel e i + | Var x -> { norm = Red; term = FFlex (VarKey x) } + | Const c -> { norm = Red; term = FFlex (ConstKey c) } + | 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 _|Proj _) -> + {norm = Red; term = FCLOS(t,e)} + +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 + subterms. + Could be used insted of mk_clos. *) +let mk_clos_deep clos_fun env t = + match kind_of_term t with + | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> + mk_clos env t + | Cast (a,k,b) -> + { norm = Red; + term = FCast (clos_fun env a, k, clos_fun env b)} + | 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 = FCaseT (ci, p, clos_fun env c, v, env) } + | Fix fx -> + { norm = Cstr; term = FFix (fx, env) } + | CoFix cfx -> + { norm = Cstr; term = FCoFix(cfx,env) } + | Lambda _ -> + { norm = Cstr; term = mk_lambda env t } + | Prod (n,t,c) -> + { norm = Whnf; + term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } + | LetIn (n,b,t,c) -> + { norm = Red; + term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } + | Evar ev -> + { norm = Red; term = FEvar(ev,env) } + +(* A better mk_clos? *) +let mk_clos2 = mk_clos_deep mk_clos + +(* The inverse of mk_clos_deep: move back to constr *) +let rec to_constr constr_fun lfts v = + match v.term with + | FRel i -> mkRel (reloc_rel i lfts) + | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) + | FFlex (VarKey x) -> mkVar x + | FAtom c -> exliftn lfts c + | FCast (a,k,b) -> + mkCast (constr_fun lfts a, k, constr_fun lfts b) + | FFlex (ConstKey op) -> mkConstU op + | FInd op -> mkIndU op + | FConstruct op -> mkConstructU op + | 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 = 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, 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 = 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, CArray.Fun1.map constr_fun lfts ftys, + CArray.Fun1.map constr_fun lfts' fbds)) + | 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, + constr_fun (el_lift lfts) bd) + | FProd (n,t,c) -> + mkProd (n, constr_fun lfts t, + constr_fun (el_lift lfts) c) + | FLetIn (n,b,t,f,e) -> + let fc = mk_clos2 (subs_lift e) f in + mkLetIn (n, constr_fun lfts b, + constr_fun lfts t, + constr_fun (el_lift lfts) fc) + | FEvar ((ev,args),env) -> + mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) + | 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 + to_constr constr_fun lfts unfv + | 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, + then we directly return the constr to avoid possibly huge + reallocation. *) +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 -> + 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 + term_of_fconstr_lift el_id + + + +(* fstrong applies unfreeze_fun recursively on the (freeze) term and + * yields a term. Assumes that the unfreeze_fun never returns a + * FCLOS term. +let rec fstrong unfreeze_fun lfts v = + to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) +*) + +let rec zip m stk = + match stk with + | [] -> m + | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} 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 + +let fapp_stack (m,stk) = zip m stk + +(*********************************************************************) + +(* The assertions in the functions below are granted because they are + called only when m is a constructor, a cofix + (strip_update_shift_app), a fix (get_nth_arg) or an abstraction + (strip_update_shift, through get_arg). *) + +(* optimised for the case where there are no shifts... *) +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 + | (Zapp args :: s) -> + 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 + | 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 (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 + | Zapp args::s' -> + let q = Array.length args in + if n >= q + then + strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s' + else + let bef = Array.sub args 0 n in + let aft = Array.sub args (n+1) (q-n-1) in + let stk' = + 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 + | s -> (None, List.rev rstk @ s) in + strip_rec [] head n stk + +(* Beta reduction: look for an applied argument in the stack. + Since the encountered update marks are removed, h must be a whnf *) +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 + get_args n tys f e s + | Zshift k :: s -> + get_args n tys f (subs_shft (k,e)) s + | Zapp l :: s -> + let na = Array.length l in + if n == na then (Inl (subs_cons(l,e)),s) + else if n < na then (* more arguments *) + let args = Array.sub l 0 n in + 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 + 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 _ | ZcaseT _ | Zproj _ + | Zshift _ | Zupdate _ as e) :: s -> + e :: eta_expand_stack s + | [] -> + [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] + +(* Iota reduction: extract the arguments to be passed to the Case + branches *) +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 Int.equal k depth then s else reloc_rargs_rec (depth-k) s + | _ -> stk + +let reloc_rargs depth stk = + if Int.equal depth 0 then stk else reloc_rargs_rec depth stk + +let rec try_drop_parameters depth n argstk = + match argstk with + Zapp args::s -> + let q = Array.length args in + 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 -> 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") + +(** [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 + 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.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 + 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 + * evaluated: its first variables are the fixpoint bodies + * + * FCLOS(fix Fi {F0 := T0 .. Fn-1 := Tn-1}, S) + * -> (S. FCLOS(F0,S) . ... . FCLOS(Fn-1,S), Ti) + *) +(* does not deal with FLIFT *) +let contract_fix_vect fix = + let (thisbody, make_body, env, nfix) = + match fix with + | FFix (((reci,i),(_,_,bds as rdcl)),env) -> + (bds.(i), + (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), + env, Array.length bds) + | FCoFix ((i,(_,_,bds as rdcl)),env) -> + (bds.(i), + (fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }), + env, Array.length bds) + | _ -> assert false + 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 info m stk = + match m.term with + | 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 info a (append_stack b (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 info arg (Zfix(m,pars)::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) + +(* cases where knh stops *) + | (FFlex _|FLetIn _|FConstruct _|FEvar _| + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> + (m, stk) + +(* The same for pure terms *) +and knht info e t stk = + match kind_of_term t with + | App(a,b) -> + knht info e a (append_stack (mk_clos_vect e b) stk) + | Case(ci,p,t,br) -> + 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) + + +(************************************************************************) + +(* Computes a weak head normal form from the result of knh. *) +let rec knr info 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 + | 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 + | 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 + | 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 + | None -> (set_norm m; (m,stk))) + | FConstruct((ind,c),u) -> + let use_match = red_set info.i_flags fMATCH in + let use_fix = red_set info.i_flags fFIX in + if use_match || use_fix then + (match strip_update_shift_app m stk with + | (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) + | (_, 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' + | (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 + | (_,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') + | (_,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.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 info m stk in + knr info hm s +and knit info e t stk = + let (ht,s) = knht info e t stk in + knr info ht s + +let kh info v stk = fapp_stack(kni info v stk) + +(************************************************************************) + +let rec zip_term zfun m stk = + match stk with + | [] -> m + | Zapp args :: s -> + 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 + 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 + | Zshift(n)::s -> + zip_term zfun (lift n m) s + | Zupdate(rf)::s -> + zip_term zfun m s + +(* Computes the strong normal form of a term. + 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 = + 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 + +(* no redex: go up for atoms and already normalized terms, go down + otherwise. *) +and norm_head info 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)) + (e,[]) tys in + let bd = kl info (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) + | FProd(na,dom,rng) -> + mkProd(na, kl info dom, kl info 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)) + | 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)) + | 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 *) + +(* weak reduction *) +let whd_val info v = + with_stats (lazy (term_of_fconstr (kh info v []))) + +(* strong reduction *) +let norm_val info v = + with_stats (lazy (kl info 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! *) + 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 +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 diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli new file mode 100644 index 000000000..077756ac7 --- /dev/null +++ b/kernel/cClosure.mli @@ -0,0 +1,244 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a + +(** {6 ... } *) +(** Delta implies all consts (both global (= by + [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. + Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of + a LetIn expression is Letin reduction *) + + + +val all_opaque : transparent_state +val all_transparent : transparent_state + +val is_transparent_variable : transparent_state -> variable -> bool +val is_transparent_constant : transparent_state -> constant -> bool + +(** Sets of reduction kinds. *) +module type RedFlagsSig = sig + type reds + type red_kind + + (** {7 The different kinds of reduction } *) + + val fBETA : red_kind + val fDELTA : red_kind + val fETA : red_kind + (** The fETA flag is never used by the kernel reduction but pretyping does *) + val fMATCH : red_kind + val fFIX : red_kind + val fCOFIX : red_kind + val fZETA : red_kind + val fCONST : constant -> red_kind + val fVAR : Id.t -> red_kind + + (** No reduction at all *) + val no_red : reds + + (** Adds a reduction kind to a set *) + val red_add : reds -> red_kind -> reds + + (** Removes a reduction kind to a set *) + val red_sub : reds -> red_kind -> reds + + (** Adds a reduction kind to a set *) + val red_add_transparent : reds -> transparent_state -> reds + + (** Build a reduction set from scratch = iter [red_add] on [no_red] *) + val mkflags : red_kind list -> reds + + (** Tests if a reduction kind is set *) + val red_set : reds -> red_kind -> bool + + (** This tests if the projection is in unfolded state already or + is unfodable due to delta. *) + val red_projection : reds -> projection -> bool +end + +module RedFlags : RedFlagsSig +open RedFlags + +(* These flags do not contain eta *) +val all : reds +val allnolet : reds +val beta : reds +val betadeltazeta : reds +val betaiota : reds +val betaiotazeta : reds +val betazeta : reds +val delta : reds +val zeta : reds +val nored : reds + + +val unfold_side_red : reds +val unfold_red : evaluable_global_reference -> reds + +(***********************************************************************) +type table_key = constant puniverses tableKey + +type 'a infos_cache +type 'a infos = { + i_flags : reds; + i_cache : 'a infos_cache } + +val ref_value_cache: 'a infos -> table_key -> 'a option +val create: ('a infos -> constr -> 'a) -> reds -> env -> + (existential -> constr option) -> 'a infos +val evar_value : 'a infos_cache -> existential -> constr option + +val info_env : 'a infos -> env +val info_flags: 'a infos -> reds + +(*********************************************************************** + s Lazy reduction. *) + +(** [fconstr] is the type of frozen constr *) + +type fconstr + +(** [fconstr] can be accessed by using the function [fterm_of] and by + matching on type [fterm] *) + +type fterm = + | FRel of int + | FAtom of constr (** Metas and Sorts *) + | FCast of fconstr * cast_kind * fconstr + | FFlex of table_key + | FInd of inductive puniverses + | FConstruct of constructor puniverses + | FApp of fconstr * fconstr array + | FProj of projection * 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 *) + | 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 + | FLOCKED + +(*********************************************************************** + s A [stack] is a context of arguments, arguments are pushed by + [append_stack] one array at a time but popped with [decomp_stack] + one by one *) + +type stack_member = + | Zapp of 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 + +and stack = stack_member list + +val empty_stack : stack +val append_stack : fconstr array -> stack -> stack + +val decomp_stack : stack -> (fconstr * stack) option +val array_of_stack : stack -> fconstr array +val stack_assign : stack -> int -> fconstr -> stack +val stack_args_size : stack -> int +val stack_tail : int -> stack -> stack +val stack_nth : stack -> int -> fconstr +val zip_term : (fconstr -> constr) -> constr -> stack -> constr +val eta_expand_stack : stack -> stack + +(** To lazy reduce a constr, create a [clos_infos] with + [create_clos_infos], inject the term to reduce with [inject]; then use + a reduction function *) + +val inject : constr -> fconstr + +(** mk_atom: prevents a term from being evaluated *) +val mk_atom : constr -> fconstr + +(** mk_red: makes a reducible term (used in newring) *) +val mk_red : fterm -> fconstr + +val fterm_of : fconstr -> fterm +val term_of_fconstr : fconstr -> constr +val destFLambda : + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr + +(** Global and local constant cache *) +type clos_infos = fconstr infos +val create_clos_infos : + ?evars:(existential->constr option) -> reds -> env -> clos_infos +val oracle_of_infos : clos_infos -> Conv_oracle.oracle + +val env_of_infos : clos_infos -> env + +val infos_with_reds : clos_infos -> reds -> clos_infos + +(** Reduction function *) + +(** [norm_val] is for strong normalization *) +val norm_val : clos_infos -> fconstr -> constr + +(** [whd_val] is for weak head normalization *) +val whd_val : clos_infos -> fconstr -> constr + +(** [whd_stack] performs weak head normalization in a given stack. It + stops whenever a reduction is blocked. *) +val whd_stack : + clos_infos -> fconstr -> stack -> fconstr * stack + +(** [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 a rigid 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. + *) +val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> + (fconstr * stack) -> stack * stack + +(** Conversion auxiliary functions to do step by step normalisation *) + +(** [unfold_reference] unfolds references in a [fconstr] *) +val unfold_reference : clos_infos -> table_key -> fconstr option + +val eq_table_key : table_key -> table_key -> bool + +(*********************************************************************** + i This is for lazy debug *) + +val lift_fconstr : int -> fconstr -> fconstr +val lift_fconstr_vect : int -> fconstr array -> fconstr array + +val mk_clos : fconstr subs -> constr -> fconstr +val mk_clos_vect : fconstr subs -> constr array -> fconstr array +val mk_clos_deep : + (fconstr subs -> constr -> fconstr) -> + fconstr subs -> constr -> fconstr + +val kni: clos_infos -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> fconstr -> stack -> fconstr * stack +val kl : clos_infos -> fconstr -> constr + +val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr + +(** End of cbn debug section i*) diff --git a/kernel/closure.ml b/kernel/closure.ml deleted file mode 100644 index 04c1bb657..000000000 --- a/kernel/closure.ml +++ /dev/null @@ -1,1072 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 - - (* [r_const=(true,cl)] means all constants but those in [cl] *) - (* [r_const=(false,cl)] means only those in [cl] *) - (* [r_delta=true] just mean [r_const=(true,[])] *) - - type reds = { - r_beta : bool; - r_delta : bool; - r_eta : bool; - r_const : transparent_state; - r_zeta : bool; - r_match : bool; - r_fix : bool; - r_cofix : bool } - - type red_kind = BETA | DELTA | ETA | MATCH | FIX - | COFIX | ZETA - | CONST of constant | VAR of Id.t - let fBETA = BETA - let fDELTA = DELTA - let fETA = ETA - let fMATCH = MATCH - let fFIX = FIX - let fCOFIX = COFIX - let fZETA = ZETA - let fCONST kn = CONST kn - let fVAR id = VAR id - let no_red = { - r_beta = false; - r_delta = false; - r_eta = false; - r_const = all_opaque; - r_zeta = false; - r_match = false; - r_fix = false; - r_cofix = 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 - { red with r_const = l1, Cpred.add kn l2 } - | MATCH -> { red with r_match = true } - | FIX -> { red with r_fix = true } - | COFIX -> { red with r_cofix = true } - | ZETA -> { red with r_zeta = true } - | VAR id -> - let (l1,l2) = red.r_const in - { 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 - { red with r_const = l1, Cpred.remove kn l2 } - | MATCH -> { red with r_match = false } - | FIX -> { red with r_fix = false } - | COFIX -> { red with r_cofix = false } - | ZETA -> { red with r_zeta = false } - | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.remove id l1, l2 } - - let red_add_transparent red tr = - { red with r_const = tr } - - let mkflags = List.fold_left red_add no_red - - 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 = Id.Pred.mem id l in - 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 - - let red_projection red p = - if Projection.unfolded p then true - else red_set red (fCONST (Projection.constant p)) - -end : RedFlagsSig) - -open RedFlags - -let all = mkflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX] -let allnolet = mkflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX] -let beta = mkflags [fBETA] -let betadeltazeta = mkflags [fBETA;fDELTA;fZETA] -let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX] -let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] -let betazeta = mkflags [fBETA;fZETA] -let delta = mkflags [fDELTA] -let zeta = mkflags [fZETA] -let nored = no_red - -(* Removing fZETA for finer behaviour would break many developments *) -let unfold_side_flags = [fBETA;fMATCH;fFIX;fCOFIX;fZETA] -let unfold_side_red = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] -let unfold_red kn = - let flag = match kn with - | EvalVarRef id -> fVAR id - | EvalConstRef kn -> fCONST kn in - mkflags (flag::unfold_side_flags) - -(* Flags of reduction and cache of constants: 'a is a type that may be - * mapped to constr. 'a infos implements a cache for constants and - * abstractions, storing a representation (of type 'a) of the body of - * this constant or abstraction. - * * i_tab is the cache table of the results - * * 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 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 - * be unfolded, returns None, but does not store this failure. * This - * doesn't take the RESET into account. You mustn't keep such a table - * after a Reset. * This type is not exported. Only its two - * instantiations (cbv or lazy) are. - *) - -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 - -module KeyTable = Hashtbl.Make(IdKeyHash) - -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 : 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 - -open Context.Named.Declaration - -let rec assoc_defined id = function -| [] -> raise Not_found -| LocalAssum _ :: ctxt -> assoc_defined id ctxt -| LocalDef (id', 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 (KeyTable.find cache.i_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 - | VarKey id -> assoc_defined id (named_context 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; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - -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 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 } - - -(**********************************************************************) -(* Lazy reduction: the one used in kernel operations *) - -(* type of shared terms. fconstr and frterm are mutually recursive. - * Clone of the constr structure, but completely mutable, and - * annotated with reduction state (reducible or not). - * - FLIFT is a delayed shift; allows sharing between 2 lifted copies - * of a given term. - * - FCLOS is a delayed substitution applied to a constr - * - FLOCKED is used to erase the content of a reference that must - * be updated. This is to allow the garbage collector to work - * before the term is computed. - *) - -(* Norm means the term is fully normalized and cannot create a redex - when substituted - Cstr means the term is in head normal form and that it can - create a redex when substituted (i.e. constructor, fix, lambda) - Whnf means we reached the head normal form and that it cannot - create a redex when substituted - Red is used for terms that might be reduced -*) -type red_state = Norm | Cstr | Whnf | Red - -let neutr = function - | (Whnf|Norm) -> Whnf - | (Red|Cstr) -> Red - -type fconstr = { - mutable norm: red_state; - mutable term: fterm } - -and fterm = - | FRel of int - | FAtom of constr (* Metas and Sorts *) - | FCast of fconstr * cast_kind * fconstr - | FFlex of table_key - | 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 - | 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 - | FLOCKED - -let fterm_of v = v.term -let set_norm v = v.norm <- Norm -let is_val v = match v.norm with Norm -> true | _ -> false - -let mk_atom c = {norm=Norm;term=FAtom c} -let mk_red f = {norm=Red;term=f} - -(* Could issue a warning if no is still Red, pointing out that we loose - sharing. *) -let update v1 no t = - if !share then - (v1.norm <- no; - v1.term <- t; - v1) - else {norm=no;term=t} - -(**********************************************************************) -(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) - -type stack_member = - | Zapp of 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 - -and stack = stack_member list - -let empty_stack = [] -let append_stack v s = - 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 - -(* Collapse the shifts in the stack *) -let zshift n s = - match (n,s) with - (0,_) -> s - | (_,Zshift(k)::s) -> Zshift(n+k)::s - | _ -> Zshift(n)::s - -let rec stack_args_size = function - | Zapp v :: s -> Array.length v + stack_args_size s - | Zshift(_)::s -> stack_args_size s - | Zupdate(_)::s -> stack_args_size s - | _ -> 0 - -(* When used as an argument stack (only Zapp can appear) *) -let rec decomp_stack = function - | Zapp v :: s -> - (match Array.length v with - 0 -> decomp_stack s - | 1 -> Some (v.(0), s) - | _ -> - Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | _ -> None -let array_of_stack s = - let rec stackrec = function - | [] -> [] - | Zapp args :: s -> args :: (stackrec s) - | _ -> assert false - in Array.concat (stackrec s) -let rec stack_assign s p c = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then - Zapp args :: stack_assign s (p-q) c - else - (let nargs = Array.copy args in - nargs.(p) <- c; - Zapp nargs :: s) - | _ -> s -let rec stack_tail p s = - if Int.equal p 0 then s else - match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_tail (p-q) s - else Zapp (Array.sub args p (q-p)) :: s - | _ -> failwith "stack_tail" -let rec stack_nth s p = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_nth s (p-q) - else args.(p) - | _ -> raise Not_found - -(* Lifting. Preserves sharing (useful only for cell with norm=Red). - lft_fconstr always create a new cell, while lift_fconstr avoids it - when the lift is 0. *) -let rec lft_fconstr n ft = - match ft.term with - | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft - | FRel i -> {norm=Norm;term=FRel(i+n)} - | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))} - | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))} - | 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)} -let lift_fconstr k f = - if Int.equal k 0 then f else lft_fconstr k f -let lift_fconstr_vect k 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 - | Inl(n,mt) -> lift_fconstr n mt - | Inr(k,None) -> {norm=Norm; term= FRel k} - | Inr(k,Some p) -> - lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)} - -(* since the head may be reducible, we might introduce lifts of 0 *) -let compact_stack head stk = - let rec strip_rec depth = function - | Zshift(k)::s -> strip_rec (depth+k) s - | Zupdate(m)::s -> - (* 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 - 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 && 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 - -let mk_lambda env t = - let (rvars,t') = decompose_lam t in - FLambda(List.length rvars, List.rev rvars, t', env) - -let destFLambda clos_fun t = - match t.term with - FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) - | FLambda(n,(na,ty)::tys,b,e) -> - (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) - | _ -> assert false - (* t must be a FLambda and binding list cannot be empty *) - -(* Optimization: do not enclose variables in a closure. - Makes variable access much faster *) -let mk_clos e t = - match kind_of_term t with - | Rel i -> clos_rel e i - | Var x -> { norm = Red; term = FFlex (VarKey x) } - | Const c -> { norm = Red; term = FFlex (ConstKey c) } - | 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 _|Proj _) -> - {norm = Red; term = FCLOS(t,e)} - -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 - subterms. - Could be used insted of mk_clos. *) -let mk_clos_deep clos_fun env t = - match kind_of_term t with - | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> - mk_clos env t - | Cast (a,k,b) -> - { norm = Red; - term = FCast (clos_fun env a, k, clos_fun env b)} - | 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 = FCaseT (ci, p, clos_fun env c, v, env) } - | Fix fx -> - { norm = Cstr; term = FFix (fx, env) } - | CoFix cfx -> - { norm = Cstr; term = FCoFix(cfx,env) } - | Lambda _ -> - { norm = Cstr; term = mk_lambda env t } - | Prod (n,t,c) -> - { norm = Whnf; - term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } - | LetIn (n,b,t,c) -> - { norm = Red; - term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar ev -> - { norm = Red; term = FEvar(ev,env) } - -(* A better mk_clos? *) -let mk_clos2 = mk_clos_deep mk_clos - -(* The inverse of mk_clos_deep: move back to constr *) -let rec to_constr constr_fun lfts v = - match v.term with - | FRel i -> mkRel (reloc_rel i lfts) - | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) - | FFlex (VarKey x) -> mkVar x - | FAtom c -> exliftn lfts c - | FCast (a,k,b) -> - mkCast (constr_fun lfts a, k, constr_fun lfts b) - | FFlex (ConstKey op) -> mkConstU op - | FInd op -> mkIndU op - | FConstruct op -> mkConstructU op - | 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 = 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, 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 = 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, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) - | 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, - constr_fun (el_lift lfts) bd) - | FProd (n,t,c) -> - mkProd (n, constr_fun lfts t, - constr_fun (el_lift lfts) c) - | FLetIn (n,b,t,f,e) -> - let fc = mk_clos2 (subs_lift e) f in - mkLetIn (n, constr_fun lfts b, - constr_fun lfts t, - constr_fun (el_lift lfts) fc) - | FEvar ((ev,args),env) -> - mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) - | 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 - to_constr constr_fun lfts unfv - | 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, - then we directly return the constr to avoid possibly huge - reallocation. *) -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 -> - 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 - term_of_fconstr_lift el_id - - - -(* fstrong applies unfreeze_fun recursively on the (freeze) term and - * yields a term. Assumes that the unfreeze_fun never returns a - * FCLOS term. -let rec fstrong unfreeze_fun lfts v = - to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) -*) - -let rec zip m stk = - match stk with - | [] -> m - | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} 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 - -let fapp_stack (m,stk) = zip m stk - -(*********************************************************************) - -(* The assertions in the functions below are granted because they are - called only when m is a constructor, a cofix - (strip_update_shift_app), a fix (get_nth_arg) or an abstraction - (strip_update_shift, through get_arg). *) - -(* optimised for the case where there are no shifts... *) -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 - | (Zapp args :: s) -> - 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 - | 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 (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 - | Zapp args::s' -> - let q = Array.length args in - if n >= q - then - strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s' - else - let bef = Array.sub args 0 n in - let aft = Array.sub args (n+1) (q-n-1) in - let stk' = - 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 - | s -> (None, List.rev rstk @ s) in - strip_rec [] head n stk - -(* Beta reduction: look for an applied argument in the stack. - Since the encountered update marks are removed, h must be a whnf *) -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 - get_args n tys f e s - | Zshift k :: s -> - get_args n tys f (subs_shft (k,e)) s - | Zapp l :: s -> - let na = Array.length l in - if n == na then (Inl (subs_cons(l,e)),s) - else if n < na then (* more arguments *) - let args = Array.sub l 0 n in - 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 - 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 _ | ZcaseT _ | Zproj _ - | Zshift _ | Zupdate _ as e) :: s -> - e :: eta_expand_stack s - | [] -> - [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] - -(* Iota reduction: extract the arguments to be passed to the Case - branches *) -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 Int.equal k depth then s else reloc_rargs_rec (depth-k) s - | _ -> stk - -let reloc_rargs depth stk = - if Int.equal depth 0 then stk else reloc_rargs_rec depth stk - -let rec try_drop_parameters depth n argstk = - match argstk with - Zapp args::s -> - let q = Array.length args in - 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 -> 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") - -(** [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 - 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.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 - 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 - * evaluated: its first variables are the fixpoint bodies - * - * FCLOS(fix Fi {F0 := T0 .. Fn-1 := Tn-1}, S) - * -> (S. FCLOS(F0,S) . ... . FCLOS(Fn-1,S), Ti) - *) -(* does not deal with FLIFT *) -let contract_fix_vect fix = - let (thisbody, make_body, env, nfix) = - match fix with - | FFix (((reci,i),(_,_,bds as rdcl)),env) -> - (bds.(i), - (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), - env, Array.length bds) - | FCoFix ((i,(_,_,bds as rdcl)),env) -> - (bds.(i), - (fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }), - env, Array.length bds) - | _ -> assert false - 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 info m stk = - match m.term with - | 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 info a (append_stack b (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 info arg (Zfix(m,pars)::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) - -(* cases where knh stops *) - | (FFlex _|FLetIn _|FConstruct _|FEvar _| - FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> - (m, stk) - -(* The same for pure terms *) -and knht info e t stk = - match kind_of_term t with - | App(a,b) -> - knht info e a (append_stack (mk_clos_vect e b) stk) - | Case(ci,p,t,br) -> - 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) - - -(************************************************************************) - -(* Computes a weak head normal form from the result of knh. *) -let rec knr info 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 - | 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 - | 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 - | 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 - | None -> (set_norm m; (m,stk))) - | FConstruct((ind,c),u) -> - let use_match = red_set info.i_flags fMATCH in - let use_fix = red_set info.i_flags fFIX in - if use_match || use_fix then - (match strip_update_shift_app m stk with - | (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) - | (_, 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' - | (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 - | (_,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') - | (_,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.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 info m stk in - knr info hm s -and knit info e t stk = - let (ht,s) = knht info e t stk in - knr info ht s - -let kh info v stk = fapp_stack(kni info v stk) - -(************************************************************************) - -let rec zip_term zfun m stk = - match stk with - | [] -> m - | Zapp args :: s -> - 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 - 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 - | Zshift(n)::s -> - zip_term zfun (lift n m) s - | Zupdate(rf)::s -> - zip_term zfun m s - -(* Computes the strong normal form of a term. - 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 = - 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 - -(* no redex: go up for atoms and already normalized terms, go down - otherwise. *) -and norm_head info 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)) - (e,[]) tys in - let bd = kl info (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) - | FProd(na,dom,rng) -> - mkProd(na, kl info dom, kl info 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)) - | 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)) - | 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 *) - -(* weak reduction *) -let whd_val info v = - with_stats (lazy (term_of_fconstr (kh info v []))) - -(* strong reduction *) -let norm_val info v = - with_stats (lazy (kl info 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! *) - 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 -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 - diff --git a/kernel/closure.mli b/kernel/closure.mli deleted file mode 100644 index 76145e3f8..000000000 --- a/kernel/closure.mli +++ /dev/null @@ -1,244 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a - -(** {6 ... } *) -(** Delta implies all consts (both global (= by - [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. - Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of - a LetIn expression is Letin reduction *) - - - -val all_opaque : transparent_state -val all_transparent : transparent_state - -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool - -(** Sets of reduction kinds. *) -module type RedFlagsSig = sig - type reds - type red_kind - - (** {7 The different kinds of reduction } *) - - val fBETA : red_kind - val fDELTA : red_kind - val fETA : red_kind - (** The fETA flag is never used by the kernel reduction but pretyping does *) - val fMATCH : red_kind - val fFIX : red_kind - val fCOFIX : red_kind - val fZETA : red_kind - val fCONST : constant -> red_kind - val fVAR : Id.t -> red_kind - - (** No reduction at all *) - val no_red : reds - - (** Adds a reduction kind to a set *) - val red_add : reds -> red_kind -> reds - - (** Removes a reduction kind to a set *) - val red_sub : reds -> red_kind -> reds - - (** Adds a reduction kind to a set *) - val red_add_transparent : reds -> transparent_state -> reds - - (** Build a reduction set from scratch = iter [red_add] on [no_red] *) - val mkflags : red_kind list -> reds - - (** Tests if a reduction kind is set *) - val red_set : reds -> red_kind -> bool - - (** This tests if the projection is in unfolded state already or - is unfodable due to delta. *) - val red_projection : reds -> projection -> bool -end - -module RedFlags : RedFlagsSig -open RedFlags - -(* These flags do not contain eta *) -val all : reds -val allnolet : reds -val beta : reds -val betadeltazeta : reds -val betaiota : reds -val betaiotazeta : reds -val betazeta : reds -val delta : reds -val zeta : reds -val nored : reds - - -val unfold_side_red : reds -val unfold_red : evaluable_global_reference -> reds - -(***********************************************************************) -type table_key = constant puniverses tableKey - -type 'a infos_cache -type 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -val ref_value_cache: 'a infos -> table_key -> 'a option -val create: ('a infos -> constr -> 'a) -> reds -> env -> - (existential -> constr option) -> 'a infos -val evar_value : 'a infos_cache -> existential -> constr option - -val info_env : 'a infos -> env -val info_flags: 'a infos -> reds - -(*********************************************************************** - s Lazy reduction. *) - -(** [fconstr] is the type of frozen constr *) - -type fconstr - -(** [fconstr] can be accessed by using the function [fterm_of] and by - matching on type [fterm] *) - -type fterm = - | FRel of int - | FAtom of constr (** Metas and Sorts *) - | FCast of fconstr * cast_kind * fconstr - | FFlex of table_key - | FInd of inductive puniverses - | FConstruct of constructor puniverses - | FApp of fconstr * fconstr array - | FProj of projection * 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 *) - | 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 - | FLOCKED - -(*********************************************************************** - s A [stack] is a context of arguments, arguments are pushed by - [append_stack] one array at a time but popped with [decomp_stack] - one by one *) - -type stack_member = - | Zapp of 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 - -and stack = stack_member list - -val empty_stack : stack -val append_stack : fconstr array -> stack -> stack - -val decomp_stack : stack -> (fconstr * stack) option -val array_of_stack : stack -> fconstr array -val stack_assign : stack -> int -> fconstr -> stack -val stack_args_size : stack -> int -val stack_tail : int -> stack -> stack -val stack_nth : stack -> int -> fconstr -val zip_term : (fconstr -> constr) -> constr -> stack -> constr -val eta_expand_stack : stack -> stack - -(** To lazy reduce a constr, create a [clos_infos] with - [create_clos_infos], inject the term to reduce with [inject]; then use - a reduction function *) - -val inject : constr -> fconstr - -(** mk_atom: prevents a term from being evaluated *) -val mk_atom : constr -> fconstr - -(** mk_red: makes a reducible term (used in newring) *) -val mk_red : fterm -> fconstr - -val fterm_of : fconstr -> fterm -val term_of_fconstr : fconstr -> constr -val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr - -(** Global and local constant cache *) -type clos_infos = fconstr infos -val create_clos_infos : - ?evars:(existential->constr option) -> reds -> env -> clos_infos -val oracle_of_infos : clos_infos -> Conv_oracle.oracle - -val env_of_infos : clos_infos -> env - -val infos_with_reds : clos_infos -> reds -> clos_infos - -(** Reduction function *) - -(** [norm_val] is for strong normalization *) -val norm_val : clos_infos -> fconstr -> constr - -(** [whd_val] is for weak head normalization *) -val whd_val : clos_infos -> fconstr -> constr - -(** [whd_stack] performs weak head normalization in a given stack. It - stops whenever a reduction is blocked. *) -val whd_stack : - clos_infos -> fconstr -> stack -> fconstr * stack - -(** [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 a rigid 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. - *) -val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> - (fconstr * stack) -> stack * stack - -(** Conversion auxiliary functions to do step by step normalisation *) - -(** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> table_key -> fconstr option - -val eq_table_key : table_key -> table_key -> bool - -(*********************************************************************** - i This is for lazy debug *) - -val lift_fconstr : int -> fconstr -> fconstr -val lift_fconstr_vect : int -> fconstr array -> fconstr array - -val mk_clos : fconstr subs -> constr -> fconstr -val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val mk_clos_deep : - (fconstr subs -> constr -> fconstr) -> - fconstr subs -> constr -> fconstr - -val kni: clos_infos -> fconstr -> stack -> fconstr * stack -val knr: clos_infos -> fconstr -> stack -> fconstr * stack -val kl : clos_infos -> fconstr -> constr - -val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr - -(** End of cbn debug section i*) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 1e132e3ab..15f213ce9 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -25,7 +25,7 @@ Nativelambda Nativecode Nativelib Environ -Closure +CClosure Reduction Nativeconv Type_errors diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 67b05e526..6c664f791 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -21,7 +21,7 @@ open Names open Term open Vars open Environ -open Closure +open CClosure open Esubst open Context.Rel.Declaration @@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible -> (* else the oracle tells which constant is to be expanded *) - let oracle = Closure.oracle_of_infos infos in + let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with @@ -537,7 +537,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = else raise NotConvertible let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = - let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in + let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index e0ae98ffa..0556191be 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1466,7 +1466,7 @@ let solve_constraints env (evars,cstrs) = (Typeclasses.mark_resolvables ~filter evars) let nf_zeta = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) exception RewriteFailure of Pp.std_ppcmds diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6f6122d50..aff60eaa4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -38,12 +38,12 @@ let _True = reference ["Init";"Logic"] "True" let _I = reference ["Init";"Logic"] "I" let whd env= - let infos=Closure.create_clos_infos Closure.betaiotazeta env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let whd_delta env= - let infos=Closure.create_clos_infos Closure.all env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) (* decompose member of equality in an applicative format *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 10c09c8d6..a862423e9 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c = fst (understand env sigma (fst c)) let special_whd env = - let infos=Closure.create_clos_infos Closure.all env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5ed426c1d..97c9d5f4a 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -84,12 +84,12 @@ let tcl_erase_info gls = tcl_change_info_gen info_gen gls let special_whd gl= - let infos=Closure.create_clos_infos Closure.all (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let is_good_inductive env ind = let mib,oib = Inductive.lookup_mind_specif env ind in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 2ed436c6b..58744b575 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -19,7 +19,7 @@ open Context.Rel.Declaration let qflag=ref true -let red_flags=ref Closure.betaiotazeta +let red_flags=ref CClosure.betaiotazeta let (=?) f g i1 i2 j1 j2= let c=f i1 i2 in @@ -59,12 +59,12 @@ let ind_hyps nevar ind largs gls= Array.map myhyps types let special_nf gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let special_whd gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) type kind_of_formula= Arrow of constr*constr diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 0f70d3ea0..5db8ff59a 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -11,7 +11,7 @@ open Globnames val qflag : bool ref -val red_flags: Closure.RedFlags.reds ref +val red_flags: CClosure.RedFlags.reds ref val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index d7da85b4f..628af4e71 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -24,8 +24,8 @@ let update_flags ()= in List.iter f (Classops.coercions ()); red_flags:= - Closure.RedFlags.red_add_transparent - Closure.betaiotazeta + CClosure.RedFlags.red_add_transparent + CClosure.betaiotazeta (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq gl= diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 13bc81019..215c850b6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -223,8 +223,8 @@ let isAppConstruct ?(env=Global.env ()) t = let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) let clos_norm_flags flgs env sigma t = - Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty + CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty @@ -1085,7 +1085,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam match Global.body_of_constant const with | Some body -> Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.empty) body diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 18ef53276..5e72b8672 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -400,7 +400,7 @@ let get_funs_constant mp dp = match Global.body_of_constant const with | Some body -> let body = Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) (Evd.from_env (Global.env ())) body diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ad5d077d6..e0c60d6d5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -90,7 +90,7 @@ let observe_tac s tac g = (* [nf_zeta] $\zeta$-normalization of a term *) let nf_zeta = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) Environ.empty_env Evd.empty diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5562100e9..027fe5677 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -92,15 +92,15 @@ let const_of_ref = function let nf_zeta env = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) env Evd.empty let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) let clos_norm_flags flgs env sigma t = - Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty + CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 7367a47ea..4ed907951 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -67,12 +67,12 @@ let l_D_Or = lazy (constant "D_Or") let special_whd gl= - let infos=Closure.create_clos_infos Closure.all (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) type atom_env= {mutable next:int; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index c08813f6e..90f5f8e63 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -12,7 +12,7 @@ open Util open Names open Term open Vars -open Closure +open CClosure open Environ open Libnames open Globnames diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 132147487..84bf849e7 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -10,7 +10,7 @@ open Util open Names open Term open Vars -open Closure +open CClosure open Esubst (**** Call by value reduction ****) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index de37d1fc5..87a03abbd 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -9,7 +9,7 @@ open Names open Term open Environ -open Closure +open CClosure open Esubst (*********************************************************************** diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8abe6116b..0fea2ba22 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -11,7 +11,7 @@ open Util open Names open Term open Vars -open Closure +open CClosure open Reduction open Reductionops open Termops diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 76c4304c4..5484e70b6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -619,7 +619,7 @@ let rec strong_prodspine redfun sigma c = (*** Reduction using bindingss ***) (*************************************) -let eta = Closure.RedFlags.mkflags [Closure.RedFlags.fETA] +let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA] (* Beta Reduction tools *) @@ -798,11 +798,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (s,cst_l) in match kind_of_term x with - | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> + | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA -> (match lookup_rel n env with | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack) | _ -> fold ()) - | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) -> + | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) | _ -> fold ()) @@ -814,7 +814,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (match safe_meta_value sigma ev with | Some body -> whrec cst_l (body, stack) | None -> fold ()) - | Const (c,u as const) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST c) -> + | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> (match constant_opt_value_in env const with | None -> fold () | Some body -> @@ -854,7 +854,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s') ) - | Proj (p, c) when Closure.RedFlags.red_projection flags p -> + | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in let kn = Projection.constant p in let npars = pb.Declarations.proj_npars @@ -895,7 +895,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, Stack.append_app [|c|] bef,cst_l)::s')) - | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> apply_subst whrec [b] cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> @@ -904,9 +904,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (f, Stack.append_app cl stack) | Lambda (na,t,c) -> (match Stack.decomp stack with - | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> apply_subst whrec [] cst_l x stack - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> let env' = push_rel (LocalAssum (na,t)) env in let whrec' = whd_state_gen tactic_mode flags env' sigma in (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with @@ -934,8 +934,8 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s')) | Construct ((ind,c),u) -> - let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in - let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in + let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> @@ -978,7 +978,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = else fold () | CoFix cofix -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then + if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> reduce_and_refold_cofix whrec env cst_l cofix stack @@ -996,15 +996,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> stacklam whrec [b] c stack | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, Stack.append_app cl stack) | Lambda (_,_,c) -> (match Stack.decomp stack with - | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + | Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> stacklam whrec [a] c m - | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with | App (f,cl) -> let napp = Array.length cl in @@ -1020,7 +1020,7 @@ let local_whd_state_gen flags sigma = | _ -> s) | _ -> s) - | Proj (p,c) when Closure.RedFlags.red_projection flags p -> + | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p (Global.env ()) in whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p, Cst_stack.empty) @@ -1045,8 +1045,8 @@ let local_whd_state_gen flags sigma = | None -> s) | Construct ((ind,c),u) -> - let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in - let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in + let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> @@ -1061,7 +1061,7 @@ let local_whd_state_gen flags sigma = else s | CoFix cofix -> - if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then + if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ | Stack.Proj _)::s') -> whrec (contract_cofix cofix, stack) @@ -1093,27 +1093,27 @@ let red_of_state_red f sigma x = (* 0. No Reduction Functions *) -let whd_nored_state = local_whd_state_gen Closure.nored +let whd_nored_state = local_whd_state_gen CClosure.nored let whd_nored_stack = stack_red_of_state_red whd_nored_state let whd_nored = red_of_state_red whd_nored_state (* 1. Beta Reduction Functions *) -let whd_beta_state = local_whd_state_gen Closure.beta +let whd_beta_state = local_whd_state_gen CClosure.beta let whd_beta_stack = stack_red_of_state_red whd_beta_state let whd_beta = red_of_state_red whd_beta_state -let whd_betalet_state = local_whd_state_gen Closure.betazeta +let whd_betalet_state = local_whd_state_gen CClosure.betazeta let whd_betalet_stack = stack_red_of_state_red whd_betalet_state let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) -let whd_delta_state e = raw_whd_state_gen Closure.delta e +let whd_delta_state e = raw_whd_state_gen CClosure.delta e let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env) let whd_delta env = red_of_state_red (whd_delta_state env) -let whd_betadeltazeta_state e = raw_whd_state_gen Closure.betadeltazeta e +let whd_betadeltazeta_state e = raw_whd_state_gen CClosure.betadeltazeta e let whd_betadeltazeta_stack env = stack_red_of_state_red (whd_betadeltazeta_state env) let whd_betadeltazeta env = @@ -1122,21 +1122,21 @@ let whd_betadeltazeta env = (* 3. Iota reduction Functions *) -let whd_betaiota_state = local_whd_state_gen Closure.betaiota +let whd_betaiota_state = local_whd_state_gen CClosure.betaiota let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state let whd_betaiota = red_of_state_red whd_betaiota_state -let whd_betaiotazeta_state = local_whd_state_gen Closure.betaiotazeta +let whd_betaiotazeta_state = local_whd_state_gen CClosure.betaiotazeta let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state -let whd_all_state env = raw_whd_state_gen Closure.all env +let whd_all_state env = raw_whd_state_gen CClosure.all env let whd_all_stack env = stack_red_of_state_red (whd_all_state env) let whd_all env = red_of_state_red (whd_all_state env) -let whd_allnolet_state env = raw_whd_state_gen Closure.allnolet env +let whd_allnolet_state env = raw_whd_state_gen CClosure.allnolet env let whd_allnolet_stack env = stack_red_of_state_red (whd_allnolet_state env) let whd_allnolet env = @@ -1148,7 +1148,7 @@ let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) (* 5. Zeta Reduction Functions *) -let whd_zeta_state = local_whd_state_gen Closure.zeta +let whd_zeta_state = local_whd_state_gen CClosure.zeta let whd_zeta_stack = stack_red_of_state_red whd_zeta_state let whd_zeta = red_of_state_red whd_zeta_state @@ -1166,16 +1166,16 @@ let nf_evar = Evarutil.nf_evar let clos_norm_flags flgs env sigma t = try let evars ev = safe_evar_value sigma ev in - Closure.norm_val - (Closure.create_clos_infos ~evars flgs env) - (Closure.inject t) + CClosure.norm_val + (CClosure.create_clos_infos ~evars flgs env) + (CClosure.inject t) with e when is_anomaly e -> error "Tried to normalize ill-typed term" -let nf_beta = clos_norm_flags Closure.beta (Global.env ()) -let nf_betaiota = clos_norm_flags Closure.betaiota (Global.env ()) -let nf_betaiotazeta = clos_norm_flags Closure.betaiotazeta (Global.env ()) +let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) +let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) +let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) let nf_all env sigma = - clos_norm_flags Closure.all env sigma + clos_norm_flags CClosure.all env sigma (********************************************************************) @@ -1469,19 +1469,19 @@ let is_sort env sigma t = let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let rec whrec csts s = - let (t, stack as s),csts' = whd_state_gen ~csts false Closure.betaiota env sigma s in + let (t, stack as s),csts' = whd_state_gen ~csts false CClosure.betaiota env sigma s in match Stack.strip_app stack with |args, (Stack.Case _ :: _ as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in + (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Fix _ :: _ as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in + (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Proj (n,m,p,_) :: stack'') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false - (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in + (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if isConstruct t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index fdfa77412..874ea6815 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -134,15 +134,15 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a -val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds -> +val whd_state_gen : ?csts:Cst_stack.t -> bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t -val iterate_whd_gen : bool -> Closure.RedFlags.reds -> +val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> Term.constr -> Term.constr (** {6 Generic Optimized Reduction Function using Closures } *) -val clos_norm_flags : Closure.RedFlags.reds -> reduction_function +val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : local_reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2d07bf4d5..820a81b5d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -18,7 +18,7 @@ open Termops open Find_subterm open Namegen open Environ -open Closure +open CClosure open Reductionops open Cbv open Patternops diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 195b21bbf..f8dfe1adf 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -66,7 +66,7 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function (** Rem: Lazy strategies are defined in Reduction *) (** Call by value strategy (uses Closures) *) -val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function +val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function val cbv_beta : local_reduction_function val cbv_betaiota : local_reduction_function val cbv_betadeltaiota : reduction_function diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c17879739..0c1ce0d2f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -460,7 +460,7 @@ let use_metas_pattern_unification flags nb l = Array.for_all (fun c -> isRel c && destRel c <= nb) l type key = - | IsKey of Closure.table_key + | IsKey of CClosure.table_key | IsProj of projection * constr let expand_table_key env = function @@ -1210,8 +1210,8 @@ let applyHead env (type r) (evd : r Sigma.t) n c = let is_mimick_head ts f = match kind_of_term f with - | Const (c,u) -> not (Closure.is_transparent_constant ts c) - | Var id -> not (Closure.is_transparent_variable ts id) + | Const (c,u) -> not (CClosure.is_transparent_constant ts c) + | Var id -> not (CClosure.is_transparent_variable ts id) | (Rel _|Construct _|Ind _) -> true | _ -> false diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ba883b5b2..8a9ce4f94 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -17,7 +17,7 @@ open Genredexpr open Pattern open Reductionops open Tacred -open Closure +open CClosure open RedFlags open Libobject open Misctypes diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 750f7a60c..1be5226de 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -262,7 +262,7 @@ let pperror cmd = CErrors.errorlabstrm "Program" cmd let error s = pperror (str s) let reduce c = - Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c + Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c exception NoObligations of Id.t option diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 04c01f3cd..e4a2ca5a0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1287,8 +1287,8 @@ let _ = optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !Closure.share); - optwrite = (fun b -> Closure.share := b) } + optread = (fun () -> !CClosure.share); + optwrite = (fun b -> CClosure.share := b) } (* No more undo limit in the new proof engine. The command still exists for compatibility (e.g. with ProofGeneral) *) -- cgit v1.2.3