aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml20
-rw-r--r--plugins/funind/indfun_common.ml10
-rw-r--r--plugins/funind/invfun.ml22
-rw-r--r--plugins/funind/plugin_base.dune1
-rw-r--r--plugins/funind/recdef.ml29
5 files changed, 29 insertions, 53 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 98d68d3db7..d4e410bd69 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -229,10 +229,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
true
with Not_found -> false
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env
-
-
exception NoChange
let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
@@ -414,13 +410,13 @@ let rewrite_until_var arg_num eq_ids : tactic =
let rec_pte_id = Id.of_string "Hrec"
let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
- let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in
- let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in
- let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in
+ let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in
+ let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in
+ let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in
let rec scan_type context type_of_hyp : tactic =
if isLetIn sigma type_of_hyp then
let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
- let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
+ let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in
(* length of context didn't change ? *)
let new_context,new_typ_of_hyp =
decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp
@@ -800,7 +796,7 @@ let build_proof
g
| LetIn _ ->
let new_infos =
- { dyn_infos with info = nf_betaiotazeta dyn_infos.info }
+ { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
in
tclTHENLIST
@@ -834,7 +830,7 @@ let build_proof
| LetIn _ ->
let new_infos =
{ dyn_infos with
- info = nf_betaiotazeta dyn_infos.info
+ info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info
}
in
@@ -977,7 +973,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "body " ++ pr_lconstr bodies.(num)); *)
let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in
(* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *)
- let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
+ let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
let (type_ctxt,type_of_f),evd =
let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
@@ -1605,7 +1601,7 @@ let prove_principle_for_gen
match !tcc_lemma_ref with
| Undefined -> user_err Pp.(str "No tcc proof !!")
| Value lemma -> EConstr.of_constr lemma
- | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I")
+ | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I")
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 03a64988e4..28a9542167 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -116,7 +116,7 @@ let def_of_const t =
[@@@ocaml.warning "-3"]
let coq_constant s =
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition"
Coqlib.init_modules s;;
@@ -311,7 +311,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr_env env sigma
- (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
+ (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -441,7 +441,7 @@ let jmeq () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.lib_ref "core.JMeq.type"
with e when CErrors.noncritical e -> raise (ToShow e)
@@ -449,7 +449,7 @@ let jmeq_refl () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.lib_ref "core.JMeq.refl"
with e when CErrors.noncritical e -> raise (ToShow e)
@@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
[@@@ocaml.warning "-3"]
-let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
[@@@ocaml.warning "+3"]
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b8973a18dc..96eb7fbc60 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -63,12 +63,6 @@ let observe_tac s tac g =
then do_observe_tac (str s) tac g
else tac g
-(* [nf_zeta] $\zeta$-normalization of a term *)
-let nf_zeta =
- Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- Environ.empty_env
- (Evd.from_env Environ.empty_env)
-
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
@@ -81,7 +75,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
let make_eq () =
try
- EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type"))
+ EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
with _ -> assert false
(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
@@ -219,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
let mib,_ = Global.lookup_inductive graph_ind in
(* and the principle to use in this lemma in $\zeta$ normal form *)
let f_principle,princ_type = schemes.(i) in
- let princ_type = nf_zeta princ_type in
+ let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
let princ_infos = Tactics.compute_elim_sig evd princ_type in
(* The number of args of the function is then easily computable *)
let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
@@ -397,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.rev (fst (List.fold_left2
(fun (bindings,avoid) decl p ->
let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
- (nf_zeta p)::bindings,id::avoid)
+ (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
(lemmas)))
@@ -511,7 +505,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
intros_with_rewrite
] g
end
- | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENLIST[
@@ -630,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
*)
let lemmas =
Array.map
- (fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt))
+ (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt))
lemmas_types_infos
in
(* We get the constant and the principle corresponding to this lemma *)
let f = funcs.(i) in
- let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in
+ let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in
let princ_type = pf_unsafe_type_of g graph_principle in
let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
(* Then we get the number of argument of the function
@@ -771,7 +765,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
evd := sigma;
- let type_of_lemma = nf_zeta type_of_lemma in
+ let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
)
@@ -838,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_of_lemma =
EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
- let type_of_lemma = nf_zeta type_of_lemma in
+ let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
type_of_lemma,type_info
)
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..9f583234d8 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -2,4 +2,5 @@
(name recdef_plugin)
(public_name coq.plugins.recdef)
(synopsis "Coq's functional induction plugin")
+ (flags :standard -open Gramlib)
(libraries coq.plugins.extraction))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ca3160f4c4..63a3e0582d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,7 +51,7 @@ open Context.Rel.Declaration
(* Ugly things which should not be here *)
[@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
Coqlib.find_reference "RecursiveDefinition" m s
let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -63,7 +63,7 @@ let pr_leconstr_rd =
let coq_init_constant s =
EConstr.of_constr (
- constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
[@@@ocaml.warning "+3"]
@@ -97,27 +97,12 @@ let type_of_const sigma t =
Typeops.type_of_constant_in (Global.env()) (sp, u)
|_ -> assert false
-let constant sl s = constr_of_global (find_reference sl s)
+let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s)
let const_of_ref = function
ConstRef kn -> kn
| _ -> anomaly (Pp.str "ConstRef expected.")
-
-let nf_zeta env =
- Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env (Evd.from_env env)
-
-
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env
- (Evd.from_env Environ.empty_env)
-
-
-
-
-
-
(* Generic values *)
let pf_get_new_ids idl g =
let ids = pf_ids_of_hyps g in
@@ -747,7 +732,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
with
| UserError(Some "Refiner.thensn_tac3",_)
| UserError(Some "Refiner.tclFAIL_s",_) ->
- (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+ (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} )
))
g
@@ -1241,7 +1226,7 @@ let get_current_subgoals_types () =
exception EmptySubgoals
let build_and_l sigma l =
- let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in
+ let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in
let conj_constr = Coqlib.build_coq_conj () in
let mk_and p1 p2 =
mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
@@ -1537,13 +1522,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
let evd = Evd.minimize_universes evd in
- let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in
+ let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
- let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
+ let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in
let eq' = EConstr.Unsafe.to_constr eq' in
let res =
(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:53:50 +0000