aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml6
-rw-r--r--pretyping/evarconv.ml5
-rw-r--r--pretyping/evarsolve.ml9
-rw-r--r--pretyping/globEnv.ml8
-rw-r--r--pretyping/reductionops.ml31
-rw-r--r--pretyping/reductionops.mli10
-rw-r--r--pretyping/tacred.ml19
7 files changed, 33 insertions, 55 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2c7b689c04..2661000a39 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -397,6 +397,10 @@ and apply_env env t =
| _ ->
map_with_binders subs_lift apply_env env t
+let rec strip_app = function
+ | APP (args,st) -> APP (args,strip_app st)
+ | s -> TOP
+
(* The main recursive functions
*
* Go under applications and cases/projections (pushed in the stack),
@@ -442,7 +446,7 @@ let rec norm_head info env t stack =
| Const sp ->
Reductionops.reduction_effect_hook info.env info.sigma
- (fst sp) (lazy (reify_stack t stack));
+ (fst sp) (lazy (reify_stack t (strip_app stack)));
norm_head_ref 0 info env stack (ConstKey sp) t
| LetIn (_, b, _, c) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2feae8cc25..489e8de602 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1352,9 +1352,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
(Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
let args = List.map (nf_evar evd) args in
- let vars = List.map NamedDecl.get_id ctxt in
- let argsubst = List.map2 (fun id c -> (id, c)) vars args in
- let instance = List.map mkVar vars in
+ let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in
+ let instance = evar_identity_subst evi in
let rhs = nf_evar evd rhs in
if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
(* Ensure that any progress made by Typing.e_solve_evars will not contradict
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 79839099f7..989fb05c3d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -216,9 +216,6 @@ type 'a update =
| UpdateWith of 'a
| NoUpdate
-open Context.Named.Declaration
-let inst_of_vars sign = List.map (get_id %> mkVar) sign
-
let restrict_evar_key evd evk filter candidates =
match filter, candidates with
| None, NoUpdate -> evd, evk
@@ -701,8 +698,7 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in
let t_in_env = whd_evar evd t_in_env in
let evd = define_fun env evd None (evk, inst_in_env) t_in_env in
- let ctxt = named_context_of_val sign in
- let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
+ let inst_in_sign = evar_identity_subst (Evd.find evd evk) in
let evar_in_sign = mkEvar (evk, inst_in_sign) in
(evd,whd_evar evd evar_in_sign)
@@ -735,9 +731,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let sign1 = evar_hyps evi1 in
let filter1 = evar_filter evi1 in
let src = subterm_source evk1 evi1.evar_source in
- let ids1 = List.map get_id (named_context_of_val sign1) in
let avoid = Environ.ids_of_named_context_val sign1 in
- let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
+ let inst_in_sign = evar_identity_subst evi1 in
let open Context.Rel.Declaration in
let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 81a62a7048..34fae613bf 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -33,8 +33,6 @@ type t = {
(** For locating indices *)
renamed_env : env;
(** For name management *)
- renamed_vars : EConstr.t list Lazy.t;
- (** Identity instance of named_context of renamed_env, to maximize sharing *)
extra : ext_named_context Lazy.t;
(** Delay the computation of the evar extended environment *)
lvar : ltac_var_map;
@@ -45,11 +43,9 @@ let make ~hypnaming env sigma lvar =
let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
(rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
- let open Context.Named.Declaration in
{
static_env = env;
renamed_env = env;
- renamed_vars = lazy (List.map (get_id %> mkVar) (named_context env));
extra = lazy (get_extra env sigma);
lvar = lvar;
}
@@ -76,7 +72,6 @@ let push_rel ~hypnaming sigma d env =
let env = {
static_env = push_rel d env.static_env;
renamed_env = push_rel d' env.renamed_env;
- renamed_vars = env.renamed_vars;
extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
lvar = env.lvar;
} in
@@ -89,7 +84,6 @@ let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
let env = {
static_env = push_rel_context ctx env.static_env;
renamed_env = push_rel_context ctx' env.renamed_env;
- renamed_vars = env.renamed_vars;
extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
lvar = env.lvar;
} in
@@ -102,7 +96,7 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env =
Array.map get_annot ctx, env
let new_evar env sigma ?src ?naming typ =
- let lazy inst_vars = env.renamed_vars in
+ let inst_vars = EConstr.identity_subst_val (named_context_val env.renamed_env) in
let rec rel_list n accu =
if n <= 0 then accu
else rel_list (n - 1) (mkRel n :: accu)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fdc770dba6..aeb18ec322 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -499,13 +499,6 @@ let beta_applist sigma (c,l) =
(* Iota reduction tools *)
-type 'a miota_args = {
- mP : constr; (* the result type *)
- mconstr : constr; (* the constructor *)
- mci : case_info; (* special info to re-build pattern *)
- mcargs : 'a list; (* the constructor's arguments *)
- mlf : 'a array } (* the branch code vector *)
-
let reducible_mind_case sigma c = match EConstr.kind sigma c with
| Construct _ | CoFix _ -> true
| _ -> false
@@ -514,10 +507,7 @@ let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j =
let ind = nbodies-j-1 in
- if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
- else
- let bd = mkCoFix (ind,typedbodies) in
- bd
+ mkCoFix (ind,typedbodies)
in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -530,18 +520,6 @@ let reduce_and_refold_cofix recfun env sigma cofix sk =
(fun _ (t,sk') -> recfun (t,sk'))
[] sigma raw_answer sk
-let reduce_mind_case sigma mia =
- match EConstr.kind sigma mia.mconstr with
- | Construct ((ind_sp,i),u) ->
-(* let ncargs = (fst mia.mci).(i-1) in*)
- let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
- applist (mia.mlf.(i-1),real_cargs)
- | CoFix cofix ->
- let cofix_def = contract_cofix sigma cofix in
- (* XXX Is NoInvert OK here? *)
- mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
- | _ -> assert false
-
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
@@ -549,10 +527,7 @@ let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies)
let nbodies = Array.length recindices in
let make_Fi j =
let ind = nbodies-j-1 in
- if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
- else
- let bd = mkFix ((recindices,ind),typedbodies) in
- bd
+ mkFix ((recindices,ind),typedbodies)
in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -757,7 +732,7 @@ let rec whd_state_gen flags env sigma =
| None -> fold ())
| Const (c,u as const) ->
reduction_effect_hook env sigma c
- (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
+ (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack)))));
if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
let u' = EInstance.kind sigma u in
match constant_value_in env (c, u') with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 0f288cdd46..d404a7e414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,22 +217,14 @@ val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
(** Raises [Invalid_argument] *)
-
-type 'a miota_args = {
- mP : constr; (** the result type *)
- mconstr : constr; (** the constructor *)
- mci : case_info; (** special info to re-build pattern *)
- mcargs : 'a list; (** the constructor's arguments *)
- mlf : 'a array } (** the branch code vector *)
-
val reducible_mind_case : evar_map -> constr -> bool
-val reduce_mind_case : evar_map -> constr miota_args -> constr
val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term
val is_arity : env -> evar_map -> constr -> bool
val is_sort : env -> evar_map -> types -> bool
val contract_fix : evar_map -> fixpoint -> constr
+val contract_cofix : evar_map -> cofixpoint -> constr
(** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
val is_transparent : Environ.env -> Constant.t tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e4b5dc1edf..9d15e98373 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -458,6 +458,25 @@ let contract_cofix_use_function env sigma f
substl_checking_arity env (List.rev subbodies)
sigma (nf_beta env sigma bodies.(bodynum))
+type 'a miota_args = {
+ mP : constr; (** the result type *)
+ mconstr : constr; (** the constructor *)
+ mci : case_info; (** special info to re-build pattern *)
+ mcargs : 'a list; (** the constructor's arguments *)
+ mlf : 'a array } (** the branch code vector *)
+
+let reduce_mind_case sigma mia =
+ match EConstr.kind sigma mia.mconstr with
+ | Construct ((ind_sp,i),u) ->
+(* let ncargs = (fst mia.mci).(i-1) in*)
+ let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
+ applist (mia.mlf.(i-1),real_cargs)
+ | CoFix cofix ->
+ let cofix_def = contract_cofix sigma cofix in
+ (* XXX Is NoInvert OK here? *)
+ mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+ | _ -> assert false
+
let reduce_mind_case_use_function func env sigma mia =
match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:18:14 +0000