aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml10
-rw-r--r--pretyping/coercion.ml6
-rw-r--r--pretyping/coercionops.ml23
-rw-r--r--pretyping/coercionops.mli4
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml6
-rw-r--r--pretyping/indrec.ml7
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/reductionops.ml62
-rw-r--r--pretyping/reductionops.mli49
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml16
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typing.ml8
-rw-r--r--pretyping/typing.mli2
-rw-r--r--pretyping/unification.ml54
16 files changed, 129 insertions, 134 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fc64022ed4..5e3fb9dae3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1066,7 +1066,7 @@ let adjust_impossible_cases sigma pb pred tomatch submat =
(* with .. end *)
(* *)
(*****************************************************************************)
-let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
+let specialize_predicate env newtomatchs (names,depna) arsign cs tms ccl =
(* Assume some gamma st: gamma |- PI [X,x:I(X)]. PI tms. ccl *)
let nrealargs = List.length names in
let l = match depna with Anonymous -> 0 | Name _ -> 1 in
@@ -1091,7 +1091,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
(* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *)
(* Note: applying the substitution in tms is not important (is it sure?) *)
let ccl'' =
- whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
+ whd_betaiota env Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
(* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *)
let ccl''' = liftn_predicate n (n+1) ccl'' tms in
(* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*)
@@ -1099,7 +1099,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
let find_predicate loc env sigma p current (IndType (indf,realargs)) dep tms =
let pred = abstract_predicate env sigma indf current realargs dep tms p in
- (pred, whd_betaiota sigma
+ (pred, whd_betaiota !!env sigma
(applist (pred, realargs@[current])))
(* Take into account that a type has been discovered to be inductive, leading
@@ -1255,7 +1255,7 @@ let rec generalize_problem names sigma pb = function
| LocalDef ({binder_name=Anonymous},_,_) -> pb', deps
| _ ->
(* for better rendering *)
- let d = RelDecl.map_type (fun c -> whd_betaiota sigma c) d in
+ let d = RelDecl.map_type (fun c -> whd_betaiota !!(pb.env) sigma c) d in
let tomatch = lift_tomatch_stack 1 pb'.tomatch in
let tomatch = relocate_index_tomatch sigma (i+1) 1 tomatch in
{ pb' with
@@ -1352,7 +1352,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname)
(* Do the specialization for the predicate *)
let pred =
- specialize_predicate typs' (realnames,curname) arsign const_info tomatch pb.pred in
+ specialize_predicate !!(pb.env) typs' (realnames,curname) arsign const_info tomatch pb.pred in
let currents = List.map (fun x -> Pushed (false,x)) typs' in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2a844402a8..f931a32bf8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -108,7 +108,7 @@ let app_opt env sigma f t =
| None -> sigma, t
| Some f -> f sigma t
in
- sigma, whd_betaiota sigma t
+ sigma, whd_betaiota env sigma t
let pair_of_array a = (a.(0), a.(1))
@@ -130,7 +130,7 @@ let disc_subset sigma x =
exception NoSubtacCoercion
let hnf env sigma c = whd_all env sigma c
-let hnf_nodelta env sigma c = whd_betaiota sigma c
+let hnf_nodelta env sigma c = whd_betaiota env sigma c
let lift_args n sign =
let rec liftrec k = function
@@ -343,7 +343,7 @@ let app_coercion env sigma coercion v =
| Some f ->
let sigma, v' = f sigma v in
let sigma, v' = Typing.solve_evars env sigma v' in
- sigma, whd_betaiota sigma v'
+ sigma, whd_betaiota env sigma v'
let coerce_itf ?loc env sigma v t c1 =
let sigma, coercion = coerce ?loc env sigma t c1 in
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 49401a9937..0c3eaa1da9 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -164,9 +164,9 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab
(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)
-let find_class_type sigma t =
+let find_class_type env sigma t =
let open EConstr in
- let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
+ let t', args = Reductionops.whd_betaiotazeta_stack env sigma t in
match EConstr.kind sigma t' with
| Var id -> CL_SECVAR id, EInstance.empty, args
| Const (sp,u) -> CL_CONST sp, u, args
@@ -178,7 +178,7 @@ let find_class_type sigma t =
| _ -> raise Not_found
-let subst_cl_typ subst ct = match ct with
+let subst_cl_typ env subst ct = match ct with
CL_SORT
| CL_FUN
| CL_SECVAR _ -> ct
@@ -190,7 +190,7 @@ let subst_cl_typ subst ct = match ct with
if c' == c then ct else (match t with
| None -> CL_CONST c'
| Some t ->
- pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
+ pi1 (find_class_type env Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
| CL_IND i ->
let i' = subst_ind subst i in
if i' == i then ct else CL_IND i'
@@ -204,12 +204,12 @@ let subst_coe_typ subst t = subst_global_reference subst t
let class_of env sigma t =
let (t, n1, i, u, args) =
try
- let (cl, u, args) = find_class_type sigma t in
+ let (cl, u, args) = find_class_type env sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, u, args)
with Not_found ->
let t = Tacred.hnf_constr env sigma t in
- let (cl, u, args) = find_class_type sigma t in
+ let (cl, u, args) = find_class_type env sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, u, args)
in
@@ -217,7 +217,7 @@ let class_of env sigma t =
let inductive_class_of ind = fst (class_info (CL_IND ind))
-let class_args_of env sigma c = pi3 (find_class_type sigma c)
+let class_args_of env sigma c = pi3 (find_class_type env sigma c)
let string_of_class = function
| CL_FUN -> "Funclass"
@@ -249,14 +249,14 @@ let lookup_path_to_sort_from_class s =
let apply_on_class_of env sigma t cont =
try
- let (cl,u,args) = find_class_type sigma t in
+ let (cl,u,args) = find_class_type env sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
t, cont i
with Not_found ->
(* Is it worth to be more incremental on the delta steps? *)
let t = Tacred.hnf_constr env sigma t in
- let (cl, u, args) = find_class_type sigma t in
+ let (cl, u, args) = find_class_type env sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
t, cont i
@@ -390,9 +390,10 @@ type coercion = {
}
let subst_coercion subst c =
+ let env = Global.env () in
let coe = subst_coe_typ subst c.coercion_type in
- let cls = subst_cl_typ subst c.coercion_source in
- let clt = subst_cl_typ subst c.coercion_target in
+ let cls = subst_cl_typ env subst c.coercion_source in
+ let clt = subst_cl_typ env subst c.coercion_target in
let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
if c.coercion_type == coe && c.coercion_source == cls &&
c.coercion_target == clt && c.coercion_is_proj == clp
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 247ef4df75..31600dd17f 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -26,7 +26,7 @@ type cl_typ =
(** Equality over [cl_typ] *)
val cl_typ_eq : cl_typ -> cl_typ -> bool
-val subst_cl_typ : substitution -> cl_typ -> cl_typ
+val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
(** Comparison of [cl_typ] *)
val cl_typ_ord : cl_typ -> cl_typ -> int
@@ -64,7 +64,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
(** [find_class_type env sigma c] returns the head reference of [c],
its universe instance and its arguments *)
-val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list
+val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list
(** raises [Not_found] if not convertible to a class *)
val class_of : env -> evar_map -> types -> types * cl_index
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f1506f5f59..36dc01e272 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -136,7 +136,7 @@ let flex_kind_of_term flags env evd c sk =
| Cast _ | App _ | Case _ -> assert false
let apprec_nohdbeta flags env evd c =
- let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
+ let (t,sk as appr) = Reductionops.whd_nored_state env evd (c, []) in
if flags.modulo_betaiota && Stack.not_purely_applicative sk
then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state
flags.open_ts env evd appr)
@@ -496,8 +496,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
let term2 = apprec_nohdbeta flags env evd term2 in
let default () =
evar_eqappr_x flags env evd pbty
- (whd_nored_state evd (term1,Stack.empty))
- (whd_nored_state evd (term2,Stack.empty))
+ (whd_nored_state env evd (term1,Stack.empty))
+ (whd_nored_state env evd (term2,Stack.empty))
in
begin match EConstr.kind evd term1, EConstr.kind evd term2 with
| Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
@@ -556,7 +556,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
let out1 = whd_betaiota_deltazeta_for_iota_state
flags.open_ts env' evd (c'1, Stack.empty) in
- let out2, _ = whd_nored_state evd
+ let out2, _ = whd_nored_state env' evd
(lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
Cst_stack.empty in
if onleft then evar_eqappr_x flags env' evd CONV out1 out2
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 34684e4a34..348d7c0b2f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -633,7 +633,7 @@ let solve_pattern_eqn env sigma l c =
l c in
(* Warning: we may miss some opportunity to eta-reduce more since c'
is not in normal form *)
- shrink_eta c'
+ shrink_eta env c'
(*****************************************)
(* Refining/solving unification problems *)
@@ -1632,7 +1632,7 @@ let rec invert_definition unify flags choose imitate_defs
map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
imitate envk t
in
- let rhs = whd_beta evd rhs (* heuristic *) in
+ let rhs = whd_beta env evd rhs (* heuristic *) in
let fast rhs =
let filter_ctxt = evar_filtered_context evi in
let names = ref Id.Set.empty in
@@ -1758,7 +1758,7 @@ let reconsider_unif_constraints unify flags evd =
let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true)
env evd (pbty,(evk1,args1 as ev1),t2) =
try
- let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
+ let t2 = whd_betaiota env evd t2 in (* includes whd_evar *)
let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in
reconsider_unif_constraints unify flags evd
with
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b5d81f762a..6132365b27 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -283,9 +283,10 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
in
(match optionpos with
| None ->
+ let env' = push_rel d env in
mkLambda_name env
- (n,t,process_constr (push_rel d env) (i+1)
- (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)])))))
+ (n,t,process_constr env' (i+1)
+ (EConstr.Unsafe.to_constr (whd_beta env' Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)])))))
(cprest,rest))
| Some(_,f_0) ->
let nF = lift (i+1+decF) f_0 in
@@ -293,7 +294,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let arg = process_pos env' nF (lift 1 t) in
mkLambda_name env
(n,t,process_constr env' (i+1)
- (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg])))))
+ (EConstr.Unsafe.to_constr (whd_beta env' Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg])))))
(cprest,rest)))
| (LocalDef (n,c,t) as d)::cprest, rest ->
mkLetIn
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f7e3d651ff..1b6c17fcf9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1025,7 +1025,7 @@ struct
| [], [] -> []
| _ -> assert false
in aux 1 1 (List.rev nal) cs.cs_args, true in
- let fsign = Context.Rel.map (whd_betaiota sigma) fsign in
+ let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in
let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
let obj ind rci p v f =
@@ -1134,7 +1134,7 @@ struct
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist sigma (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
- let cs_args = Context.Rel.map (whd_betaiota sigma) cs_args in
+ let cs_args = Context.Rel.map (whd_betaiota !!env sigma) cs_args in
let csgn =
List.map (set_name Anonymous) cs_args
in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f7456ef35e..4d083664f7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -603,8 +603,7 @@ end
(** The type of (machine) states (= lambda-bar-calculus' cuts) *)
type state = constr * constr Stack.t
-type contextual_reduction_function = env -> evar_map -> constr -> constr
-type reduction_function = contextual_reduction_function
+type reduction_function = env -> evar_map -> constr -> constr
type local_reduction_function = evar_map -> constr -> constr
type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -1225,7 +1224,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
(** reduction machine without global env and refold machinery *)
-let local_whd_state_gen flags sigma =
+let local_whd_state_gen flags _env sigma =
let rec whrec (x, stack) =
let c0 = EConstr.kind sigma x in
let s = (EConstr.of_kind c0, stack) in
@@ -1308,7 +1307,7 @@ let raw_whd_state_gen flags env =
f
let stack_red_of_state_red f =
- let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in
+ let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
f
(* Drops the Cst_stack *)
@@ -1319,8 +1318,8 @@ let iterate_whd_gen refold flags env sigma s =
Stack.zip sigma ~refold (hd,whd_sk)
in aux s
-let red_of_state_red f sigma x =
- Stack.zip sigma (f sigma (x,Stack.empty))
+let red_of_state_red f env sigma x =
+ Stack.zip sigma (f env sigma (x,Stack.empty))
(* 0. No Reduction Functions *)
@@ -1341,15 +1340,12 @@ let whd_betalet = red_of_state_red whd_betalet_state
(* 2. Delta Reduction Functions *)
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 CClosure.betadeltazeta e
-let whd_betadeltazeta_stack env =
- stack_red_of_state_red (whd_betadeltazeta_state env)
-let whd_betadeltazeta env =
- red_of_state_red (whd_betadeltazeta_state env)
+let whd_delta_stack = stack_red_of_state_red whd_delta_state
+let whd_delta = red_of_state_red whd_delta_state
+let whd_betadeltazeta_state = raw_whd_state_gen CClosure.betadeltazeta
+let whd_betadeltazeta_stack = stack_red_of_state_red whd_betadeltazeta_state
+let whd_betadeltazeta = red_of_state_red whd_betadeltazeta_state
(* 3. Iota reduction Functions *)
@@ -1361,21 +1357,19 @@ 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 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_all_state = raw_whd_state_gen CClosure.all
+let whd_all_stack = stack_red_of_state_red whd_all_state
+let whd_all = red_of_state_red whd_all_state
-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 =
- red_of_state_red (whd_allnolet_state env)
+let whd_allnolet_state = raw_whd_state_gen CClosure.allnolet
+let whd_allnolet_stack = stack_red_of_state_red whd_allnolet_state
+let whd_allnolet = red_of_state_red whd_allnolet_state
(* 4. Ad-hoc eta reduction, does not substitute evars *)
-let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty))
+let shrink_eta env c =
+ let evd = Evd.from_env env in
+ Stack.zip evd (local_whd_state_gen eta env evd (c,Stack.empty))
(* 5. Zeta Reduction Functions *)
@@ -1627,9 +1621,9 @@ let plain_instance sigma s c =
empty map).
*)
-let instance sigma s c =
+let instance env sigma s c =
(* if s = [] then c else *)
- local_strong whd_betaiota sigma (plain_instance sigma s c)
+ strong whd_betaiota env sigma (plain_instance sigma s c)
(* pseudo-reduction rule:
* [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -1795,23 +1789,23 @@ let is_arity env sigma c =
(*************************************)
(* Metas *)
-let meta_value evd mv =
+let meta_value env evd mv =
let rec valrec mv =
match meta_opt_fvalue evd mv with
| Some (b,_) ->
let metas = Metamap.bind valrec b.freemetas in
- instance evd metas b.rebus
+ instance env evd metas b.rebus
| None -> mkMeta mv
in
valrec mv
-let meta_instance sigma b =
+let meta_instance env sigma b =
let fm = b.freemetas in
if Metaset.is_empty fm then b.rebus
else
- let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
- instance sigma c_sigma b.rebus
+ let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in
+ instance env sigma c_sigma b.rebus
-let nf_meta sigma c =
+let nf_meta env sigma c =
let cl = mk_freelisted c in
- meta_instance sigma { cl with rebus = cl.rebus }
+ meta_instance env sigma { cl with rebus = cl.rebus }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 243a2745f0..555c4be971 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -127,8 +127,7 @@ end
type state = constr * constr Stack.t
-type contextual_reduction_function = env -> evar_map -> constr -> constr
-type reduction_function = contextual_reduction_function
+type reduction_function = env -> evar_map -> constr -> constr
type local_reduction_function = evar_map -> constr -> constr
type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -181,30 +180,30 @@ val nf_evar : evar_map -> constr -> constr
(** Lazy strategy, weak head reduction *)
val whd_evar : evar_map -> constr -> constr
-val whd_nored : local_reduction_function
-val whd_beta : local_reduction_function
-val whd_betaiota : local_reduction_function
-val whd_betaiotazeta : local_reduction_function
-val whd_all : contextual_reduction_function
-val whd_allnolet : contextual_reduction_function
-val whd_betalet : local_reduction_function
+val whd_nored : reduction_function
+val whd_beta : reduction_function
+val whd_betaiota : reduction_function
+val whd_betaiotazeta : reduction_function
+val whd_all : reduction_function
+val whd_allnolet : reduction_function
+val whd_betalet : reduction_function
(** Removes cast and put into applicative form *)
-val whd_nored_stack : local_stack_reduction_function
-val whd_beta_stack : local_stack_reduction_function
-val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazeta_stack : local_stack_reduction_function
+val whd_nored_stack : contextual_stack_reduction_function
+val whd_beta_stack : contextual_stack_reduction_function
+val whd_betaiota_stack : contextual_stack_reduction_function
+val whd_betaiotazeta_stack : contextual_stack_reduction_function
val whd_all_stack : contextual_stack_reduction_function
val whd_allnolet_stack : contextual_stack_reduction_function
-val whd_betalet_stack : local_stack_reduction_function
+val whd_betalet_stack : contextual_stack_reduction_function
-val whd_nored_state : local_state_reduction_function
-val whd_beta_state : local_state_reduction_function
-val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazeta_state : local_state_reduction_function
+val whd_nored_state : state_reduction_function
+val whd_beta_state : state_reduction_function
+val whd_betaiota_state : state_reduction_function
+val whd_betaiotazeta_state : state_reduction_function
val whd_all_state : state_reduction_function
val whd_allnolet_state : state_reduction_function
-val whd_betalet_state : local_state_reduction_function
+val whd_betalet_state : state_reduction_function
(** {6 Head normal forms } *)
@@ -214,11 +213,11 @@ val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
val whd_betadeltazeta_state : state_reduction_function
val whd_betadeltazeta : reduction_function
-val whd_zeta_stack : local_stack_reduction_function
-val whd_zeta_state : local_state_reduction_function
-val whd_zeta : local_reduction_function
+val whd_zeta_stack : stack_reduction_function
+val whd_zeta_state : state_reduction_function
+val whd_zeta : reduction_function
-val shrink_eta : constr -> constr
+val shrink_eta : Environ.env -> constr -> constr
(** Various reduction functions *)
@@ -314,5 +313,5 @@ val whd_betaiota_deltazeta_for_iota_state :
TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
(** {6 Meta-related reduction functions } *)
-val meta_instance : evar_map -> constr freelisted -> constr
-val nf_meta : evar_map -> constr -> constr
+val meta_instance : env -> evar_map -> constr freelisted -> constr
+val nf_meta : env -> evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 1f091c3df8..5ec5005b3e 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -134,7 +134,7 @@ let retype ?(polyprop=true) sigma =
let n = inductive_nrealdecls env (fst (fst (dest_ind_family indf))) in
let t = betazetaevar_applist sigma n p realargs in
(match EConstr.kind sigma (whd_all env sigma (type_of env t)) with
- | Prod _ -> whd_beta sigma (applist (t, [c]))
+ | Prod _ -> whd_beta env sigma (applist (t, [c]))
| _ -> t)
| Lambda (name,c1,c2) ->
mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2c717b8774..5b9bc91b84 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -252,7 +252,7 @@ let invert_name labs l {binder_name=na0} env sigma ref na =
| None -> None
| Some c ->
let labs',ccl = decompose_lam sigma c in
- let _, l' = whd_betalet_stack sigma ccl in
+ let _, l' = whd_betalet_stack env sigma ccl in
let labs' = List.map snd labs' in
(* ppedrot: there used to be generic equality on terms here *)
let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in
@@ -288,7 +288,7 @@ let compute_consteval_direct env sigma ref =
let compute_consteval_mutual_fix env sigma ref =
let rec srec env minarg labs ref c =
- let c',l = whd_betalet_stack sigma c in
+ let c',l = whd_betalet_stack env sigma c in
let nargs = List.length l in
match EConstr.kind sigma c' with
| Lambda (na,t,g) when List.is_empty l ->
@@ -424,7 +424,7 @@ let solve_arity_problem env sigma fxminargs c =
let evm = ref sigma in
let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
let rec check strict c =
- let c' = whd_betaiotazeta sigma c in
+ let c' = whd_betaiotazeta env sigma c in
let (h,rcargs) = decompose_app_vect sigma c' in
match EConstr.kind sigma h with
Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -725,7 +725,7 @@ let rec red_elim_const env sigma ref u largs =
if evaluable_reference_eq sigma ref refgoal then
(c,args)
else
- let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
+ let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in
descend (destEvalRefU sigma c') lrest in
let (_, midargs as s) = descend (ref,u) largs in
let d, lrest = whd_nothing_for_iota env sigma (applist s) in
@@ -736,11 +736,11 @@ let rec red_elim_const env sigma ref u largs =
| Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
| NotAnElimination when unfold_nonelim ->
let c = reference_value env sigma ref u in
- (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
+ (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase
| _ -> raise Redelimination
with Redelimination when unfold_anyway ->
let c = reference_value env sigma ref u in
- (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
+ (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase
and reduce_params env sigma stack l =
let len = List.length stack in
@@ -849,7 +849,7 @@ and whd_construct_stack env sigma s =
let try_red_product env sigma c =
let simpfun c = clos_norm_flags betaiotazeta env sigma c in
let rec redrec env x =
- let x = whd_betaiota sigma x in
+ let x = whd_betaiota env sigma x in
match EConstr.kind sigma x with
| App (f,l) ->
(match EConstr.kind sigma f with
@@ -875,7 +875,7 @@ let try_red_product env sigma c =
| _ -> redrec env c
in
let npars = Projection.npars p in
- (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack sigma c') [] with
+ (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack env sigma c') [] with
| Reduced s -> simpfun (applist s)
| NotReducible -> raise Redelimination)
| _ ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index afd6c33821..d1b65775bd 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -179,7 +179,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
| None -> []
| Some (rels, ((tc,u), args)) ->
let instapp =
- Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
+ Reductionops.whd_beta env sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
in
let instapp = EConstr.Unsafe.to_constr instapp in
let projargs = Array.of_list (args @ [instapp]) in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 99a35849e0..f0882d4594 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -29,11 +29,11 @@ open Context.Rel.Declaration
module GR = Names.GlobRef
-let meta_type evd mv =
+let meta_type env evd mv =
let ty =
try Evd.meta_ftype evd mv
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
- meta_instance evd ty
+ meta_instance env evd ty
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
@@ -175,7 +175,7 @@ let type_case_branches env sigma (ind,largs) pj c =
let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
let lc = Array.map EConstr.of_constr lc in
let n = (snd specif).Declarations.mind_nrealdecls in
- let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
+ let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
sigma, (lc, ty, Sorts.relevance_of_sort ps)
let judge_of_case env sigma ci pj cj lfj =
@@ -335,7 +335,7 @@ let rec execute env sigma cstr =
let cstr = whd_evar sigma cstr in
match EConstr.kind sigma cstr with
| Meta n ->
- sigma, { uj_val = cstr; uj_type = meta_type sigma n }
+ sigma, { uj_val = cstr; uj_type = meta_type env sigma n }
| Evar ev ->
let ty = EConstr.existential_type sigma ev in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 96222f7bf6..5916f0e867 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -35,7 +35,7 @@ val check : env -> evar_map -> constr -> types -> evar_map
val type_of_variable : env -> variable -> types
(** Returns the instantiated type of a metavariable *)
-val meta_type : evar_map -> metavariable -> types
+val meta_type : env -> evar_map -> metavariable -> types
(** Solve existential variables using typing *)
val solve_evars : env -> evar_map -> constr -> evar_map * constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f5aaac315a..ab99bdc777 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -708,8 +708,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let stM,stN = extract_instance_status pb in
let sigma =
if opt.with_types && flags.check_applied_meta_types then
- let tyM = Typing.meta_type sigma k1 in
- let tyN = Typing.meta_type sigma k2 in
+ let tyM = Typing.meta_type curenv sigma k1 in
+ let tyN = Typing.meta_type curenv sigma k2 in
let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in
check_compatibility curenv CUMUL flags substn l r
else sigma
@@ -721,7 +721,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
- let tyM = Typing.meta_type sigma k in
+ let tyM = Typing.meta_type curenv sigma k in
let tyN = get_type_of curenv ~lax:true sigma cN in
check_compatibility curenv CUMUL flags substn tyN tyM
with RetypeError _ ->
@@ -742,7 +742,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = get_type_of curenv ~lax:true sigma cM in
- let tyN = Typing.meta_type sigma k in
+ let tyN = Typing.meta_type curenv sigma k in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma)
@@ -1040,33 +1040,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
unirec_rec curenvnb pb opt substn
- (whd_betaiotazeta sigma (mkApp(c,l1))) cN
+ (whd_betaiotazeta curenv sigma (mkApp(c,l1))) cN
| None ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
unirec_rec curenvnb pb opt substn cM
- (whd_betaiotazeta sigma (mkApp(c,l2)))
+ (whd_betaiotazeta curenv sigma (mkApp(c,l2)))
| None ->
error_cannot_unify curenv sigma (cM,cN)))
| Some false ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
unirec_rec curenvnb pb opt substn cM
- (whd_betaiotazeta sigma (mkApp(c,l2)))
+ (whd_betaiotazeta curenv sigma (mkApp(c,l2)))
| None ->
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
unirec_rec curenvnb pb opt substn
- (whd_betaiotazeta sigma (mkApp(c,l1))) cN
+ (whd_betaiotazeta curenv sigma (mkApp(c,l1))) cN
| None ->
error_cannot_unify curenv sigma (cM,cN)))
and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
if isApp_or_Proj sigma cM then
- let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
+ let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
if is_open_canonical_projection curenv sigma f1l1 then
- let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
+ let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1080,9 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
else
try f1 () with e when precatchable_exception e ->
if isApp_or_Proj sigma cN then
- let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
+ let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
if is_open_canonical_projection curenv sigma f2l2 then
- let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
+ let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1306,18 +1306,18 @@ let w_coerce_to_type env evd c cty mvty =
let w_coerce env evd mv c =
let cty = get_type_of env evd c in
- let mvty = Typing.meta_type evd mv in
+ let mvty = Typing.meta_type env evd mv in
w_coerce_to_type env evd c cty mvty
let unify_to_type env sigma flags c status u =
let sigma, c = refresh_universes (Some false) env sigma c in
- let t = get_type_of env sigma (nf_meta sigma c) in
- let t = nf_betaiota env sigma (nf_meta sigma t) in
+ let t = get_type_of env sigma (nf_meta env sigma c) in
+ let t = nf_betaiota env sigma (nf_meta env sigma t) in
unify_0 env sigma CUMUL flags t u
let unify_type env sigma flags mv status c =
- let mvty = Typing.meta_type sigma mv in
- let mvty = nf_meta sigma mvty in
+ let mvty = Typing.meta_type env sigma mv in
+ let mvty = nf_meta env sigma mvty in
unify_to_type env sigma
(set_flags_for_type flags)
c status mvty
@@ -1476,20 +1476,20 @@ let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
[clenv_typed_unify M N clenv] expects in addition that expected
types of metavars are unifiable with the types of their instances *)
-let head_app sigma m =
- fst (whd_nored_state sigma (m, Stack.empty))
+let head_app env sigma m =
+ fst (whd_nored_state env sigma (m, Stack.empty))
let isEvar_or_Meta sigma c = match EConstr.kind sigma c with
| Evar _ | Meta _ -> true
| _ -> false
let check_types env flags (sigma,_,_ as subst) m n =
- if isEvar_or_Meta sigma (head_app sigma m) then
+ if isEvar_or_Meta sigma (head_app env sigma m) then
unify_0_with_initial_metas subst true env CUMUL
flags
(get_type_of env sigma n)
(get_type_of env sigma m)
- else if isEvar_or_Meta sigma (head_app sigma n) then
+ else if isEvar_or_Meta sigma (head_app env sigma n) then
unify_0_with_initial_metas subst true env CUMUL
flags
(get_type_of env sigma m)
@@ -1947,7 +1947,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
(* Remove delta when looking for a subterm *)
let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in
let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
- let typp = Typing.meta_type evd' p in
+ let typp = Typing.meta_type env evd' p in
let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
match infer_conv ~pb:CUMUL env evd' predtyp typp with
| None ->
@@ -1958,7 +1958,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
(evd',[p,pred,(Conv,TypeProcessed)],[])
let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
- let typp = Typing.meta_type evd p in
+ let typp = Typing.meta_type env evd p in
let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
w_merge env false flags.merge_unify_flags
(evd,[p,pred,(Conv,TypeProcessed)],[])
@@ -1968,8 +1968,8 @@ let secondOrderAbstractionAlgo dep =
if dep then secondOrderDependentAbstraction else secondOrderAbstraction
let w_unify2 env evd flags dep cv_pb ty1 ty2 =
- let c1, oplist1 = whd_nored_stack evd ty1 in
- let c2, oplist2 = whd_nored_stack evd ty2 in
+ let c1, oplist1 = whd_nored_stack env evd ty1 in
+ let c2, oplist2 = whd_nored_stack env evd ty2 in
match EConstr.kind evd c1, EConstr.kind evd c2 with
| Meta p1, _ ->
(* Find the predicate *)
@@ -2000,8 +2000,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
- let hd1,l1 = decompose_app_vect evd (whd_nored evd ty1) in
- let hd2,l2 = decompose_app_vect evd (whd_nored evd ty2) in
+ let hd1,l1 = decompose_app_vect evd (whd_nored env evd ty1) in
+ let hd2,l2 = decompose_app_vect evd (whd_nored env evd ty2) in
let is_empty1 = Array.is_empty l1 in
let is_empty2 = Array.is_empty l2 in
match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:18:14 +0000