summaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r--plugins/funind/recdef.ml124
1 files changed, 66 insertions, 58 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 065d0fe5..fa84e4dd 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -16,7 +16,7 @@ open Names
open Libnames
open Globnames
open Nameops
-open Errors
+open CErrors
open Util
open Tacticals
open Tacmach
@@ -29,6 +29,7 @@ open Proof_type
open Pfedit
open Glob_term
open Pretyping
+open Termops
open Constrintern
open Misctypes
open Genredexpr
@@ -38,7 +39,8 @@ open Auto
open Eauto
open Indfun_common
-
+open Sigma.Notations
+open Context.Rel.Declaration
(* Ugly things which should not be here *)
@@ -90,15 +92,15 @@ let const_of_ref = function
let nf_zeta env =
- Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
env
Evd.empty
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
let clos_norm_flags flgs env sigma t =
- Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
- clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
+ CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
@@ -159,7 +161,7 @@ let rec n_x_id ids n =
let simpl_iter clause =
reduce
(Lazy
- {rBeta=true;rIota=true;rZeta= true; rDelta=false;
+ {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=true;rDelta=false;
rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
clause
@@ -179,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) =
)
in
let context = List.map
- (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al))
+ (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al))
in
let env = Environ.push_rel_context context (Global.env ()) in
let glob_body =
@@ -206,23 +208,23 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob
(* Debugging mechanism *)
let debug_queue = Stack.create ()
-let rec print_debug_queue b e =
+let print_debug_queue b e =
if not (Stack.is_empty debug_queue)
then
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
else
begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
end;
(* print_debug_queue false e; *)
end
let observe strm =
if do_observe ()
- then Pp.msg_debug strm
+ then Feedback.msg_debug strm
else ()
@@ -236,9 +238,9 @@ let do_observe_tac s tac g =
ignore(Stack.pop debug_queue);
v
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
if not (Stack.is_empty debug_queue)
- then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+ then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise));
iraise reraise
let observe_tac s tac g =
@@ -265,8 +267,8 @@ let observe_tclTHENLIST s tacl =
let tclUSER tac is_mes l g =
let clear_tac =
match l with
- | None -> clear []
- | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
+ | None -> tclIDTAC
+ | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l)
in
observe_tclTHENLIST (str "tclUSER1")
[
@@ -274,8 +276,8 @@ let tclUSER tac is_mes l g =
if is_mes
then observe_tclTHENLIST (str "tclUSER2")
[
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
- (delayed_force Indfun_common.ltof_ref))];
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
+ (delayed_force Indfun_common.ltof_ref))]);
tac
]
else tac
@@ -397,7 +399,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
Proofview.V82.of_tactic (intro_using teq_id);
onLastHypId (fun heq ->
observe_tclTHENLIST (str "treat_case2")[
- thin to_intros;
+ Proofview.V82.of_tactic (clear to_intros);
h_intros to_intros;
(fun g' ->
let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
@@ -439,7 +441,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
end
| Lambda(n,t,b) ->
@@ -447,7 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
end
| Case(ci,t,a,l) ->
@@ -558,12 +560,12 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
Proofview.V82.of_tactic default_full_auto];
observe_tclTHENLIST (str "destruct_bounds_aux2")[
- observe_tac (str "clearing k ") (clear [id]);
+ observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
h_intros [k;h';def];
- observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
+ observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
observe_tac (str "unfold functional")
- (unfold_in_concl[(Locus.OnlyOccurrences [1],
- evaluable_of_global_reference infos.func)]);
+ (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+ evaluable_of_global_reference infos.func)]));
(
observe_tclTHENLIST (str "test")[
list_rewrite true
@@ -587,7 +589,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
| (_,v_bound)::l ->
observe_tclTHENLIST (str "destruct_bounds_aux3")[
Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
- clear [v_bound];
+ Proofview.V82.of_tactic (clear [v_bound]);
tclDO 2 (Proofview.V82.of_tactic intro);
onNthHypId 1
(fun p_hyp ->
@@ -643,7 +645,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b;
true
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
in
if forbid
then
@@ -676,8 +678,10 @@ let mkDestructEq :
let hyps = pf_hyps g in
let to_revert =
Util.List.map_filter
- (fun (id, _, t) ->
- if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
+ (fun decl ->
+ let open Context.Named.Declaration in
+ let id = get_id decl in
+ if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl))
then None else Some id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
let type_of_expr = pf_unsafe_type_of g expr in
@@ -685,11 +689,13 @@ let mkDestructEq :
to_revert_constr in
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (str "mkDestructEq")
- [Simple.generalize new_hyps;
+ [Proofview.V82.of_tactic (generalize new_hyps);
(fun g2 ->
- Proofview.V82.of_tactic (change_in_concl None
- (fun patvars sigma ->
- pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2);
+ let changefun patvars = { run = fun sigma ->
+ let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+ redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
+ } in
+ Proofview.V82.of_tactic (change_in_concl None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -698,7 +704,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
false
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
true
in
let a' = infos.info in
@@ -897,10 +903,10 @@ let make_rewrite expr_info l hp max =
[observe_tac(str "make_rewrite finalize") (
(* tclORELSE( h_reflexivity) *)
(observe_tclTHENLIST (str "make_rewrite")[
- simpl_iter Locusops.onConcl;
+ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
observe_tac (str "unfold functional")
- (unfold_in_concl[(Locus.OnlyOccurrences [1],
- evaluable_of_global_reference expr_info.func)]);
+ (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+ evaluable_of_global_reference expr_info.func)]));
(list_rewrite true
(List.map (fun e -> mkVar e,true) expr_info.eqs));
@@ -942,7 +948,7 @@ let rec destruct_hex expr_info acc l =
| (v,hex)::l ->
observe_tclTHENLIST (str "destruct_hex")[
Proofview.V82.of_tactic (simplest_case (mkVar hex));
- clear [hex];
+ Proofview.V82.of_tactic (clear [hex]);
tclDO 2 (Proofview.V82.of_tactic intro);
onNthHypId 1 (fun hp ->
onNthHypId 2 (fun p ->
@@ -1110,10 +1116,10 @@ let termination_proof_header is_mes input_type ids args_id relation
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
- tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id]))
+ tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
))
;
- observe_tac (str "fix") (fix (Some hrec) (nargs+1));
+ observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
h_intros args_id;
Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
@@ -1248,7 +1254,7 @@ let clear_goals =
then Termops.pop b'
else if b' == b then t
else mkProd(na,t',b')
- | _ -> map_constr clear_goal t
+ | _ -> Term.map_constr clear_goal t
in
List.map clear_goal
@@ -1275,12 +1281,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| Some s -> s
| None ->
try add_suffix current_proof_name "_subproof"
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
anomaly (Pp.str "open_new_goal with an unamed theorem")
in
let na = next_global_ident_away name [] in
if Termops.occur_existential gls_type then
- Errors.error "\"abstract\" cannot handle existentials";
+ CErrors.error "\"abstract\" cannot handle existentials";
let hook _ _ =
let opacity =
let na_ref = Libnames.Ident (Loc.ghost,na) in
@@ -1300,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
observe_tclTHENLIST (str "")
[
- Simple.generalize [lemma];
+ Proofview.V82.of_tactic (generalize [lemma]);
Proofview.V82.of_tactic (Simple.intro hid);
(fun g ->
let ids = pf_ids_of_hyps g in
@@ -1327,10 +1333,10 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
tclFIRST[
tclTHEN
(Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
- e_assumption;
+ (Proofview.V82.of_tactic e_assumption);
Eauto.eauto_with_bases
(true,5)
- [Evd.empty,Lazy.force refl_equal]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
]
)
@@ -1420,7 +1426,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let x = n_x_id ids nargs in
observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
h_intros x;
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
observe_tac (str "simplest_case")
(Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
Array.of_list (List.map mkVar x)))));
@@ -1484,7 +1490,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let env = Global.env() in
let evd = ref (Evd.from_env env) in
let function_type = interp_type_evars env evd type_of_f in
- let env = push_named (function_name,None,function_type) env in
+ let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
let ty = interp_type_evars env evd ~impls:rec_impls eq in
let evm, nf = Evarutil.nf_evars_and_universes !evd in
@@ -1492,7 +1498,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let function_type = nf function_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) -> (x,None,y)) res_vars) env 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' 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'); *)
@@ -1510,29 +1516,31 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
- let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in
- let relation =
- fst (*FIXME*)(interp_constr
- env_with_pre_rec_args
- (Evd.from_env env_with_pre_rec_args)
- r)
+ (* Refresh the global universes, now including those of _F *)
+ let evm = Evd.from_env (Global.env ()) in
+ let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
+ let relation, evuctx =
+ interp_constr env_with_pre_rec_args evm r
in
+ let evm = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref None in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
- let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
+ let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
(* message "start second proof"; *)
let stop =
try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
false
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
if do_observe ()
- then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
- else anomaly (Pp.str "Cannot create equation Lemma")
+ then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
+ else CErrors.errorlabstrm "Cannot create equation Lemma"
+ (str "Cannot create equation lemma." ++ spc () ++
+ str "This may be because the function is nested-recursive.")
;
true
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 23:47:51 +0000