diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 16:30:32 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:14:05 +0200 |
commit | cf95f2a791c263c7aaa3b488d1b09eaafc29be2b (patch) | |
tree | 72515081ec6bf1e2d75362767aa2bcc0ce08b48d /pretyping | |
parent | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (diff) |
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
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cbv.ml | 2 | ||||
-rw-r--r-- | pretyping/cbv.mli | 2 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 78 | ||||
-rw-r--r-- | pretyping/reductionops.mli | 6 | ||||
-rw-r--r-- | pretyping/tacred.ml | 2 | ||||
-rw-r--r-- | pretyping/tacred.mli | 2 | ||||
-rw-r--r-- | pretyping/unification.ml | 6 |
8 files changed, 50 insertions, 50 deletions
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 |