aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml29
-rw-r--r--plugins/funind/functional_principles_types.ml20
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/merge.ml7
-rw-r--r--plugins/funind/recdef.ml3
5 files changed, 36 insertions, 31 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 188368082..cc29d68f5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -95,6 +95,7 @@ let list_chop ?(msg="") n l =
with Failure (msg') ->
failwith (msg ^ msg')
+let pop t = Vars.lift (-1) t
let make_refl_eq constructor type_of_t t =
(* let refl_equal_term = Lazy.force refl_equal in *)
@@ -289,7 +290,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
in
let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
let sub = compute_substitution sub (fst t1) (fst t2) in
- let end_of_type_with_pop = Termops.pop (EConstr.of_constr end_of_type) in (*the equation will be removed *)
+ let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
let new_end_of_type =
(* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
Can be safely replaced by the next comment for Ocaml >= 3.08.4
@@ -311,9 +312,9 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
try
let witness = Int.Map.find i sub in
if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
- (Termops.pop (EConstr.of_constr end_of_type),ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
+ (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
with Not_found ->
- (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
+ (Term.mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
)
1
(new_end_of_type,0,witness_fun)
@@ -416,7 +417,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
let coq_I = Coqlib.build_coq_I () in
let rec scan_type context type_of_hyp : tactic =
if isLetIn type_of_hyp then
- let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
+ let real_type_of_hyp = Term.it_mkProd_or_LetIn type_of_hyp context in
let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
(* length of context didn't change ? *)
let new_context,new_typ_of_hyp =
@@ -429,13 +430,13 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
then
begin
let (x,t_x,t') = destProd type_of_hyp in
- let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
+ let actual_real_type_of_hyp = Term.it_mkProd_or_LetIn t' context in
if is_property ptes_infos t_x actual_real_type_of_hyp then
begin
let pte,pte_args = (destApp t_x) in
let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in
- let popped_t' = Termops.pop (EConstr.of_constr t') in
- let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
+ let popped_t' = pop t' in
+ let real_type_of_hyp = Term.it_mkProd_or_LetIn popped_t' context in
let prove_new_type_of_hyp =
let context_length = List.length context in
tclTHENLIST
@@ -486,9 +487,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
(* observe (str "In "++Ppconstr.pr_id hyp_id++ *)
(* str " removing useless precond True" *)
(* ); *)
- let popped_t' = Termops.pop (EConstr.of_constr t') in
+ let popped_t' = pop t' in
let real_type_of_hyp =
- it_mkProd_or_LetIn popped_t' context
+ Term.it_mkProd_or_LetIn popped_t' context
in
let prove_trivial =
let nb_intro = List.length context in
@@ -515,9 +516,9 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
]
else if is_trivial_eq t_x
then (* t_x := t = t => we remove this precond *)
- let popped_t' = Termops.pop (EConstr.of_constr t') in
+ let popped_t' = pop t' in
let real_type_of_hyp =
- it_mkProd_or_LetIn popped_t' context
+ Term.it_mkProd_or_LetIn popped_t' context
in
let hd,args = destApp t_x in
let get_args hd args =
@@ -616,8 +617,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
let fun_body =
mkLambda(Anonymous,
pf_unsafe_type_of g' term,
- Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
- )
+ EConstr.Unsafe.to_constr (Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
+ ))
in
let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in
let new_body = EConstr.Unsafe.to_constr new_body in
@@ -988,7 +989,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(nb_params + nb_args) t,evd
in
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
- let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
+ let lemma_type = Term.it_mkProd_or_LetIn eqn type_ctxt in
(* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
let f_id = Label.to_id (con_label (fst (destConst f))) in
let prove_replacement =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b4eb77870..8683f68c6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -23,6 +23,8 @@ let observe s =
if do_observe ()
then Feedback.msg_debug s
+let pop t = Vars.lift (-1) t
+
(*
Transform an inductive induction principle into
a functional one
@@ -111,7 +113,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
let dummy_var = mkVar (Id.of_string "________") in
let mk_replacement c i args =
- let res = mkApp(rel_to_fun.(i), Array.map (fun c -> Termops.pop (EConstr.of_constr c)) (array_get_start args)) in
+ let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res);
res
in
@@ -169,25 +171,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_env = Environ.push_rel (LocalAssum (x,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (Termops.pop (EConstr.of_constr new_b)), filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+ then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
else
(
bind_fun(new_x,new_t,new_b),
list_union_eq
eq_constr
binders_to_remove_from_t
- (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+ (List.map pop binders_to_remove_from_b)
)
with
| Toberemoved ->
(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
- new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+ new_b, List.map pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
- new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+ new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
end
and compute_new_princ_type_for_letin remove env x v t b =
begin
@@ -198,25 +200,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (Termops.pop (EConstr.of_constr new_b)),filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
else
(
mkLetIn(new_x,new_v,new_t,new_b),
list_union_eq
eq_constr
(list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
- (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+ (List.map pop binders_to_remove_from_b)
)
with
| Toberemoved ->
(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
- new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b
+ new_b, List.map pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
- new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b)
+ new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
end
and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) =
let new_e,to_remove_from_e = compute_new_princ_type remove env e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c02b64c1f..ca066c4cc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -399,8 +399,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
match ctxt with
| [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
| hres::res::decl::ctxt ->
- let res = Termops.it_mkLambda_or_LetIn
- (Termops.it_mkProd_or_LetIn concl [hres;res])
+ let res = Term.it_mkLambda_or_LetIn
+ (Term.it_mkProd_or_LetIn concl [hres;res])
(LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
in
res
@@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
in
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
- let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+ let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in
let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
@@ -861,7 +861,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
let type_of_lemma =
- Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+ Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3688b8c15..2840193a9 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -32,7 +32,8 @@ module RelDecl = Context.Rel.Declaration
(** {2 Useful operations on constr and glob_constr} *)
-let rec popn i c = if i<=0 then c else EConstr.of_constr (pop (popn (i-1) c))
+let pop c = Vars.lift (-1) c
+let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
(** Substitutions in constr *)
let compare_constr_nosub t1 t2 =
@@ -986,13 +987,13 @@ let relprinctype_to_funprinctype relprinctype nfuns =
(* first remove indarg and indarg_in_concl *)
let relinfo_noindarg = { relinfo with
indarg_in_concl = false; indarg = None;
- concl = EConstr.of_constr (remove_last_arg (pop relinfo.concl)); } in
+ concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in
(* the nfuns last induction arguments are functional ones: remove them *)
let relinfo_argsok = { relinfo_noindarg with
nargs = relinfo_noindarg.nargs - nfuns;
(* args is in reverse order, so remove fst *)
args = remove_n_fst_list nfuns relinfo_noindarg.args;
- concl = popn nfuns relinfo_noindarg.concl;
+ concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl));
} in
let new_branches =
List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c71174fef..23b308efb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -408,6 +408,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
args.(1),args.(2)
in
let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in
+ let new_b' = EConstr.Unsafe.to_constr new_b' in
let new_infos = {
infos with
info = new_b';
@@ -1253,7 +1254,7 @@ let clear_goals =
| Prod(Name id as na,t',b) ->
let b' = clear_goal b in
if noccurn 1 b' && (is_rec_res id)
- then Termops.pop (EConstr.of_constr b')
+ then Vars.lift (-1) b'
else if b' == b then t
else mkProd(na,t',b')
| _ -> Term.map_constr clear_goal t
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 22:46:52 +0000