diff options
| author | Hugo Herbelin | 2020-09-13 14:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-29 22:24:02 +0200 |
| commit | 5cac24428e448c12ab292265bb2ffd1146b38c25 (patch) | |
| tree | 43713dc6730d53db67fa2a910650154dee1b91a1 /plugins/funind | |
| parent | bee9998b0cde3c86888fcad8c0dccbeebb351032 (diff) | |
Almost fully moving funind to new proof engine.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 621 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.mli | 14 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 320 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 618 |
6 files changed, 744 insertions, 841 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 72e6006b7e..118a2f3a2e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Printer open CErrors open Util @@ -8,9 +18,7 @@ open Vars open Namegen open Names open Pp -open Tacmach open Termops -open Tacticals open Tactics open Indfun_common open Libnames @@ -27,7 +35,7 @@ let make_refl_eq constructor type_of_t t = mkApp (constructor, [|type_of_t; t|]) type pte_info = - {proving_tac : Id.t list -> Tacmach.tactic; is_valid : constr -> bool} + {proving_tac : Id.t list -> unit Proofview.tactic; is_valid : constr -> bool} type ptes_info = pte_info Id.Map.t @@ -36,16 +44,15 @@ type 'a dynamic_info = type body_info = constr dynamic_info -let observe_tac s = observe_tac (fun _ _ -> Pp.str s) +let observe_tac s = New.observe_tac ~header:(str "observation") (fun _ _ -> Pp.str s) -let finish_proof dynamic_infos g = - observe_tac "finish" (Proofview.V82.of_tactic assumption) g +let finish_proof dynamic_infos = + observe_tac "finish" assumption let refine c = - Proofview.V82.of_tactic - (Logic.refiner ~check:true EConstr.Unsafe.(to_constr c)) + Logic.refiner ~check:true EConstr.Unsafe.(to_constr c) -let thin l = Proofview.V82.of_tactic (Tactics.clear l) +let thin = clear let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v let is_trivial_eq sigma t = @@ -83,37 +90,40 @@ let is_incompatible_eq env sigma t = if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t); res -let change_hyp_with_using msg hyp_id t tac : tactic = - fun g -> - let prov_id = pf_get_new_id hyp_id g in - tclTHENS - ((* observe_tac msg *) Proofview.V82.of_tactic - (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac)))) - [ tclTHENLIST +let pf_get_new_id id env = + next_ident_away id (Id.Set.of_list (Termops.ids_of_named_context env)) + +let change_hyp_with_using msg hyp_id t tac = + Proofview.Goal.enter (fun gl -> + let prov_id = pf_get_new_id hyp_id (Proofview.Goal.hyps gl) in + Tacticals.New.tclTHENS + ((* observe_tac msg *) + (assert_by (Name prov_id) t (Tacticals.New.tclCOMPLETE tac))) + [ Tacticals.New.tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) - thin [hyp_id] + Tactics.clear [hyp_id] ; (* observe_tac "change_hyp_with_using rename " *) - Proofview.V82.of_tactic (rename_hyp [(prov_id, hyp_id)]) ] ] - g + rename_hyp [(prov_id, hyp_id)] ] ]) exception TOREMOVE let prove_trivial_eq h_id context (constructor, type_of_term, term) = let nb_intros = List.length context in - tclTHENLIST - [ tclDO nb_intros (Proofview.V82.of_tactic intro) + Tacticals.New.tclTHENLIST + [ Tacticals.New.tclDO nb_intros intro ; (* introducing context *) - (fun g -> + Proofview.Goal.enter (fun g -> + let hyps = Proofview.Goal.hyps g in let context_hyps = fst - (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) + (list_chop ~msg:"prove_trivial_eq : " nb_intros (ids_of_named_context hyps)) in let context_hyps' = mkApp (constructor, [|type_of_term; term|]) :: List.map mkVar context_hyps in let to_refine = applist (mkVar h_id, List.rev context_hyps') in - refine to_refine g) ] + refine to_refine) ] let find_rectype env sigma c = let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in @@ -257,11 +267,11 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type = in tclTHEN (Proofview.Unsafe.tclEVARS evm) - (Proofview.V82.tactic (refine to_refine)))) + (refine to_refine))) in let simpl_eq_tac = change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp - (Proofview.V82.of_tactic prove_new_hyp) + prove_new_hyp in (* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) (* str "removing an equation " ++ fnl ()++ *) @@ -294,30 +304,31 @@ let isLetIn sigma t = match EConstr.kind sigma t with LetIn _ -> true | _ -> false let h_reduce_with_zeta cl = - Proofview.V82.of_tactic - (reduce - (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) - cl) + reduce + (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) + cl -let rewrite_until_var arg_num eq_ids : tactic = +let rewrite_until_var arg_num eq_ids : unit Proofview.tactic = + let open Tacticals.New in (* tests if the declares recursive argument is neither a Constructor nor an applied Constructor since such a form for the recursive argument will break the Guard when trying to save the Lemma. *) let test_var g = - let sigma = project g in - let _, args = destApp sigma (pf_concl g) in + let sigma = Proofview.Goal.sigma g in + let _, args = destApp sigma (Proofview.Goal.concl g) in not (isConstruct sigma args.(arg_num) || isAppConstruct sigma args.(arg_num)) in - let rec do_rewrite eq_ids g = - if test_var g then tclIDTAC g + let rec do_rewrite eq_ids = + Proofview.Goal.enter (fun g -> + if test_var g then Proofview.tclUNIT () else match eq_ids with | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.") | eq_id :: eq_ids -> tclTHEN - (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) - (do_rewrite eq_ids) g + (tclTRY (Equality.rewriteRL (mkVar eq_id))) + (do_rewrite eq_ids)) in do_rewrite eq_ids @@ -336,7 +347,8 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in - let rec scan_type context type_of_hyp : tactic = + let open Tacticals.New in + let rec scan_type context type_of_hyp : unit Proofview.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 = @@ -362,28 +374,28 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let prove_new_type_of_hyp = let context_length = List.length context in tclTHENLIST - [ tclDO context_length (Proofview.V82.of_tactic intro) - ; (fun g -> + [ tclDO context_length intro + ; Proofview.Goal.enter (fun g -> + let hyps = Proofview.Goal.hyps g in let context_hyps_ids = fst (list_chop ~msg:"rec hyp : context_hyps" context_length - (pf_ids_of_hyps g)) + (ids_of_named_context hyps)) in - let rec_pte_id = pf_get_new_id rec_pte_id g in + let rec_pte_id = pf_get_new_id rec_pte_id hyps in let to_refine = applist ( mkVar hyp_id , List.rev_map mkVar (rec_pte_id :: context_hyps_ids) ) in (* observe_tac "rec hyp " *) - (tclTHENS - (Proofview.V82.of_tactic - (assert_before (Name rec_pte_id) t_x)) + tclTHENS + (assert_before (Name rec_pte_id) t_x) [ (* observe_tac "prove rec hyp" *) prove_rec_hyp eq_hyps ; (* observe_tac "prove rec hyp" *) refine to_refine ]) - g) ] + ] in tclTHENLIST [ (* observe_tac "hyp rec" *) @@ -408,19 +420,20 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let prove_trivial = let nb_intro = List.length context in tclTHENLIST - [ tclDO nb_intro (Proofview.V82.of_tactic intro) - ; (fun g -> + [ tclDO nb_intro intro + ; Proofview.Goal.enter (fun g -> + let hyps = Proofview.Goal.hyps g in let context_hyps = fst (list_chop ~msg:"removing True : context_hyps " nb_intro - (pf_ids_of_hyps g)) + (ids_of_named_context hyps)) in let to_refine = applist ( mkVar hyp_id , List.rev (coq_I :: List.map mkVar context_hyps) ) in - refine to_refine g) ] + refine to_refine) ] in tclTHENLIST [ change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp @@ -455,8 +468,11 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = try (scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id]) with TOREMOVE -> (thin [hyp_id], []) -let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) g = - let env = pf_env g and sigma = project g in +let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> + let env = Proofview.Goal.env g in + let sigma = Proofview.Goal.sigma g in let tac, new_hyps = List.fold_left (fun (hyps_tac, new_hyps) hyp_id -> @@ -470,88 +486,80 @@ let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) g = {dyn_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps} in tclTHENLIST - [tac; (* observe_tac "clean_hyp_with_heq continue" *) continue_tac new_infos] - g + [tac; (* observe_tac "clean_hyp_with_heq continue" *) continue_tac new_infos]) let heq_id = Id.of_string "Heq" -let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g = +let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in tclTHENLIST [ (* We first introduce the variables *) tclDO nb_first_intro - (Proofview.V82.of_tactic - (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))) + (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)) ; (* Then the equation itself *) - Proofview.V82.of_tactic - (intro_using_then heq_id + (intro_using_then heq_id (* we get the fresh name with onLastHypId *) (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP - (fun id -> Proofview.V82.of_tactic (introduction id)) + introduction dyn_infos.rec_hyps - ; observe_tac "after_introduction" (fun g' -> + ; observe_tac "after_introduction" + (Proofview.Goal.enter (fun g' -> + let env = Proofview.Goal.env g' in + let sigma = Proofview.Goal.sigma g' in (* We get infos on the equations introduced*) - let new_term_value_eq = pf_get_hyp_typ g' heq_id in + let new_term_value_eq = Tacmach.New.pf_get_hyp_typ heq_id g' in (* compute the new value of the body *) let new_term_value = - match EConstr.kind (project g') new_term_value_eq with + match EConstr.kind sigma new_term_value_eq with | App (f, [|_; _; args2|]) -> args2 | _ -> observe ( str "cannot compute new term value : " - ++ pr_gls g' ++ fnl () ++ str "last hyp is" - ++ pr_leconstr_env (pf_env g') (project g') - new_term_value_eq ); + ++ Tacmach.New.pr_gls g' ++ fnl () ++ str "last hyp is" + ++ pr_leconstr_env env sigma new_term_value_eq ); anomaly (Pp.str "cannot compute new term value.") in - let g', termtyp = tac_type_of g' term in + tclTYPEOFTHEN term (fun sigma termtyp -> let fun_body = mkLambda ( make_annot Anonymous Sorts.Relevant , termtyp - , Termops.replace_term (project g') term (mkRel 1) + , Termops.replace_term sigma term (mkRel 1) dyn_infos.info ) in let new_body = - pf_nf_betaiota g' (mkApp (fun_body, [|new_term_value|])) + Reductionops.nf_betaiota env sigma (mkApp (fun_body, [|new_term_value|])) in let new_infos = { dyn_infos with info = new_body ; eq_hyps = heq_id :: dyn_infos.eq_hyps } in - clean_goal_with_heq ptes_infos continue_tac new_infos g') ]) - ] - g + clean_goal_with_heq ptes_infos continue_tac new_infos))) ]) + ]) -let my_orelse tac1 tac2 g = - try tac1 g - with e when CErrors.noncritical e -> - (* observe (str "using snd tac since : " ++ CErrors.print e); *) - tac2 g - -let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id = +let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic) hyps args_id = let args = Array.of_list (List.map mkVar args_id) in + let open Tacticals.New in let instantiate_one_hyp hid = - my_orelse - (fun (* we instantiate the hyp if possible *) - g -> - let prov_hid = pf_get_new_id hid g in + tclORELSE0 + (* we instantiate the hyp if possible *) + (Proofview.Goal.enter (fun g -> + let prov_hid = Tacmach.New.pf_get_new_id hid g in let c = mkApp (mkVar hid, args) in - let evm, _ = pf_apply Typing.type_of g c in - let open Tacticals.New in - Proofview.V82.of_tactic - (tclTHENLIST - [ Proofview.Unsafe.tclEVARS evm - ; pose_proof (Name prov_hid) c - ; clear [hid] - ; rename_hyp [(prov_hid, hid)] ]) - g) - (fun (* + (* Check typing *) + tclTYPEOFTHEN c (fun _ _ -> + tclTHENLIST + [ pose_proof (Name prov_hid) c + ; thin [hid] + ; rename_hyp [(prov_hid, hid)]]))) + (* if not then we are in a mutual function block and this hyp is a recursive hyp on an other function. @@ -559,9 +567,8 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id = principle so that we can trash it *) - g -> (* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) - thin [hid] g) + (thin [hid]) in if List.is_empty args_id then tclTHENLIST @@ -571,61 +578,59 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id = tclTHENLIST [ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps ; tclMAP instantiate_one_hyp hyps - ; (fun g -> + ; Proofview.Goal.enter (fun g -> let all_g_hyps_id = - List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty + List.fold_right Id.Set.add (Tacmach.New.pf_ids_of_hyps g) Id.Set.empty in let remaining_hyps = List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps in - do_prove remaining_hyps g) ] + do_prove remaining_hyps) ] let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos - dyn_infos : tactic = - let rec build_proof_aux do_finalize dyn_infos : tactic = - fun g -> - let env = pf_env g in - let sigma = project g in + dyn_infos : unit Proofview.tactic = + let open Tacticals.New in + let rec build_proof_aux do_finalize dyn_infos : unit Proofview.tactic = + Proofview.Goal.enter (fun g -> + let env = Proofview.Goal.env g in + let sigma = Proofview.Goal.sigma g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) match EConstr.kind sigma dyn_infos.info with | Case (ci, ct, iv, t, cb) -> - let do_finalize_t dyn_info' g = + let do_finalize_t dyn_info' = + Proofview.Goal.enter (fun g -> let t = dyn_info'.info in let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in - let g_nb_prod = nb_prod (project g) (pf_concl g) in - let g, type_of_term = tac_type_of g t in + let g_nb_prod = nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in + tclTYPEOFTHEN t (fun _ type_of_term -> let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in tclTHENLIST - [ Proofview.V82.of_tactic - (generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)) + [ generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps) ; thin dyn_infos.rec_hyps - ; Proofview.V82.of_tactic - (pattern_option [(Locus.AllOccurrencesBut [1], t)] None) - ; (fun g -> - observe_tac "toto" + ; pattern_option [(Locus.AllOccurrencesBut [1], t)] None + ; observe_tac "toto" (tclTHENLIST - [ Proofview.V82.of_tactic (Simple.case t) - ; (fun g' -> - let g'_nb_prod = nb_prod (project g') (pf_concl g') in + [ Simple.case t + ; Proofview.Goal.enter (fun g' -> + let g'_nb_prod = nb_prod (Proofview.Goal.sigma g') (Proofview.Goal.concl g') in let nb_instantiate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case ptes_infos nb_instantiate_partial (build_proof do_finalize) t dyn_infos) - g') ]) - g) ] - g + ) ]) + ])) in - build_proof do_finalize_t {dyn_infos with info = t} g + build_proof do_finalize_t {dyn_infos with info = t} | Lambda (n, t, b) -> ( - match EConstr.kind sigma (pf_concl g) with + match EConstr.kind sigma (Proofview.Goal.concl g) with | Prod _ -> tclTHEN - (Proofview.V82.of_tactic intro) - (fun g' -> + intro + (Proofview.Goal.enter (fun g' -> let open Context.Named.Declaration in - let id = pf_last_hyp g' |> get_id in + let id = Tacmach.New.pf_last_hyp g' |> get_id in let new_term = - pf_nf_betaiota g' (mkApp (dyn_infos.info, [|mkVar id|])) + Reductionops.nf_betaiota (Proofview.Goal.env g') (Proofview.Goal.sigma g') (mkApp (dyn_infos.info, [|mkVar id|])) in let new_infos = {dyn_infos with info = new_term} in let do_prove new_hyps = @@ -635,14 +640,13 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos ; nb_rec_hyps = List.length new_hyps } in (* observe_tac "Lambda" *) - (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' - (* build_proof do_finalize new_infos g' *)) - g - | _ -> do_finalize dyn_infos g ) - | Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t} g + (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) + (* build_proof do_finalize new_infos g' *))) + | _ -> do_finalize dyn_infos) + | Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t} | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ - |Float _ -> - do_finalize dyn_infos g + | Float _ -> + do_finalize dyn_infos | App (_, _) -> ( let f, args = decompose_app sigma dyn_infos.info in match EConstr.kind sigma f with @@ -655,15 +659,15 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> let new_infos = {dyn_infos with info = (f, args)} in - build_proof_args env sigma do_finalize new_infos g + build_proof_args env sigma do_finalize new_infos | Const (c, _) when not (List.mem_f Constant.equal c fnames) -> let new_infos = {dyn_infos with info = (f, args)} in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) - build_proof_args env sigma do_finalize new_infos g - | Const _ -> do_finalize dyn_infos g + build_proof_args env sigma do_finalize new_infos + | Const _ -> do_finalize dyn_infos | Lambda _ -> let new_term = Reductionops.nf_beta env sigma dyn_infos.info in - build_proof do_finalize {dyn_infos with info = new_term} g + build_proof do_finalize {dyn_infos with info = new_term} | LetIn _ -> let new_infos = { dyn_infos with @@ -675,18 +679,17 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos dyn_infos.rec_hyps ; h_reduce_with_zeta Locusops.onConcl ; build_proof do_finalize new_infos ] - g - | Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b} g + | Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b} | Case _ | Fix _ | CoFix _ -> let new_finalize dyn_infos = let new_infos = {dyn_infos with info = (dyn_infos.info, args)} in build_proof_args env sigma do_finalize new_infos in - build_proof new_finalize {dyn_infos with info = f} g ) + build_proof new_finalize {dyn_infos with info = f}) | Fix _ | CoFix _ -> user_err Pp.(str "Anonymous local (co)fixpoints are not handled yet") | Proj _ -> user_err Pp.(str "Prod") - | Prod _ -> do_finalize dyn_infos g + | Prod _ -> do_finalize dyn_infos | LetIn _ -> let new_infos = { dyn_infos with @@ -698,24 +701,20 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos dyn_infos.rec_hyps ; h_reduce_with_zeta Locusops.onConcl ; build_proof do_finalize new_infos ] - g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") - | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet") - and build_proof do_finalize dyn_infos g = + | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet")) + and build_proof do_finalize dyn_infos = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - Indfun_common.observe_tac + Indfun_common.New.observe_tac ~header:(str "observation") (fun env sigma -> str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info) (build_proof_aux do_finalize dyn_infos) - g - and build_proof_args env sigma do_finalize dyn_infos : tactic = + and build_proof_args env sigma do_finalize dyn_infos : unit Proofview.tactic = (* f_args' args *) - fun g -> + Proofview.Goal.enter (fun g -> let f_args', args = dyn_infos.info in - let tac : tactic = - fun g -> - match args with - | [] -> do_finalize {dyn_infos with info = f_args'} g + let tac = match args with + | [] -> do_finalize {dyn_infos with info = f_args'} | arg :: args -> (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *) (* fnl () ++ *) @@ -727,16 +726,15 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos build_proof_args env sigma do_finalize {dyn_infos with info = (mkApp (f_args', [|new_arg|]), args)} in - build_proof do_finalize {dyn_infos with info = arg} g + build_proof do_finalize {dyn_infos with info = arg} in - (* observe_tac "build_proof_args" *) tac g + (* observe_tac "build_proof_args" *) tac) in let do_finish_proof dyn_infos = (* tclTRYD *) clean_goal_with_heq ptes_infos finish_proof dyn_infos in (* observe_tac "build_proof" *) - fun g -> - build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g + build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos (* Proof of principles from structural functions *) @@ -750,21 +748,25 @@ type static_fix_info = ; num_in_block : int } let prove_rec_hyp_for_struct fix_info eq_hyps = - tclTHEN (rewrite_until_var fix_info.idx eq_hyps) (fun g -> - let _, pte_args = destApp (project g) (pf_concl g) in + let open Tacticals.New in + tclTHEN (rewrite_until_var fix_info.idx eq_hyps) + (Proofview.Goal.enter (fun g -> + let _, pte_args = destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in let rec_hyp_proof = mkApp (mkVar fix_info.name, array_get_start pte_args) in - refine rec_hyp_proof g) + refine rec_hyp_proof)) let prove_rec_hyp fix_info = {proving_tac = prove_rec_hyp_for_struct fix_info; is_valid = (fun _ -> true)} -let generalize_non_dep hyp g = +let generalize_non_dep hyp = + Proofview.Goal.enter (fun g -> (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_get_hyp_typ g hyp in + let sigma = Proofview.Goal.sigma g in + let hyp_typ = Tacmach.New.pf_get_hyp_typ hyp g in let to_revert, _ = let open Context.Named.Declaration in Environ.fold_named_context_reverse @@ -773,29 +775,28 @@ let generalize_non_dep hyp g = let hyp = get_id decl in if Id.List.mem hyp hyps - || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep - || Termops.occur_var env (project g) hyp hyp_typ + || List.exists (Termops.occur_var_in_decl env sigma hyp) keep + || Termops.occur_var env sigma hyp hyp_typ || Termops.is_section_variable hyp (* should be dangerous *) then (clear, decl :: keep) else (hyp :: clear, keep)) - ~init:([], []) (pf_env g) + ~init:([], []) (Proofview.Goal.env g) in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) - tclTHEN - ((* observe_tac "h_generalize" *) Proofview.V82.of_tactic + Tacticals.New.tclTHEN + ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert))) - ((* observe_tac "thin" *) thin to_revert) - g + ((* observe_tac "thin" *) clear to_revert)) let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id let var_of_decl = id_of_decl %> mkVar let revert idl = - tclTHEN (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) (thin idl) + Tacticals.New.tclTHEN (generalize (List.map mkVar idl)) (clear idl) -let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num - = +let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num = + let open Tacticals.New in (* observe (str "nb_args := " ++ str (string_of_int nb_args)); *) (* observe (str "nb_params := " ++ str (string_of_int nb_params)); *) (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) @@ -843,16 +844,15 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in let prove_replacement = tclTHENLIST - [ tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro) - ; observe_tac "" (fun g -> - let rec_id = pf_nth_hyp_id g 1 in + [ tclDO (nb_params + rec_args_num + 1) intro + ; observe_tac "" (onNthHypId 1 (fun rec_id -> tclTHENLIST [ observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id) ; observe_tac "h_case" - (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))) - ; Proofview.V82.of_tactic intros_reflexivity ] - g) ] + (simplest_case (mkVar rec_id)) + ; intros_reflexivity ])) + ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) @@ -863,9 +863,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type () in let lemma = Declare.Proof.start ~cinfo ~info evd in - let lemma, _ = - Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma - in + let lemma, _ = Declare.Proof.by prove_replacement lemma in let (_ : _ list) = Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None @@ -873,7 +871,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num evd let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num - all_funs g = + all_funs = + Proofview.Goal.enter (fun g -> let equation_lemma = try let finfos = @@ -918,29 +917,32 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num evd := sigma; res in - let nb_intro_to_do = nb_prod (project g) (pf_concl g) in + let nb_intro_to_do = nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) in + let open Tacticals.New in tclTHEN - (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro)) - (fun g' -> - let just_introduced = nLastDecls nb_intro_to_do g' in + (tclDO nb_intro_to_do intro) + (Proofview.Goal.enter (fun g' -> + let just_introduced = Tacticals.New.nLastDecls g' nb_intro_to_do in let open Context.Named.Declaration in let just_introduced_id = List.map get_id just_introduced in tclTHEN - (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) - (revert just_introduced_id) - g') - g + (* Hack to synchronize the goal with the global env *) + (Proofview.V82.tactic (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))) + (revert just_introduced_id)))) let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num - fnames all_funs _nparams : tactic = - fun g -> - let princ_type = pf_concl g in + fnames all_funs _nparams : unit Proofview.tactic = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> + let princ_type = Proofview.Goal.concl g in + let env = Proofview.Goal.env g in + let sigma = Proofview.Goal.sigma g in (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *) (* Pp.msgnl (str "all_funs "); *) (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *) - let princ_info = compute_elim_sig (project g) princ_type in + let princ_info = compute_elim_sig sigma princ_type in let fresh_id = - let avoid = ref (pf_ids_of_hyps g) in + let avoid = ref (Tacmach.New.pf_ids_of_hyps g) in fun na -> let new_id = match na with @@ -969,7 +971,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in let fbody = get_body fnames.(fun_num) in - let f_ctxt, f_body = decompose_lam (project g) fbody in + let f_ctxt, f_body = decompose_lam sigma fbody in let f_ctxt_length = List.length f_ctxt in let diff_params = princ_info.nparams - f_ctxt_length in let full_params, princ_params, fbody_with_full_params = @@ -1013,12 +1015,12 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num in let fix_offset = List.length princ_params in let ptes_to_fix, infos = - match EConstr.kind (project g) fbody_with_full_params with + match EConstr.kind sigma fbody_with_full_params with | Fix ((idxs, i), (names, typess, bodies)) -> let bodies_with_all_params = Array.map (fun body -> - Reductionops.nf_betaiota (pf_env g) (project g) + Reductionops.nf_betaiota env sigma (applist ( substl (List.rev (Array.to_list all_funs_with_full_params)) @@ -1030,7 +1032,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num Array.mapi (fun i types -> let types = - prod_applist (project g) types + prod_applist sigma types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset @@ -1038,7 +1040,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num ; types ; offset = fix_offset ; nb_realargs = - List.length (fst (decompose_lam (project g) bodies.(i))) + List.length (fst (decompose_lam sigma bodies.(i))) - fix_offset ; body_with_param = bodies_with_all_params.(i) ; num_in_block = i }) @@ -1049,7 +1051,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num (fun i (acc_map, acc_info) decl -> let pte = RelDecl.get_name decl in let infos = info_array.(i) in - let type_args, _ = decompose_prod (project g) infos.types in + let type_args, _ = decompose_prod sigma infos.types in let nargs = List.length type_args in let f = applist @@ -1062,12 +1064,12 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num let body_with_param, num = let body = get_body fnames.(i) in let body_with_full_params = - Reductionops.nf_betaiota (pf_env g) (project g) + Reductionops.nf_betaiota env sigma (applist (body, List.rev_map var_of_decl full_params)) in - match EConstr.kind (project g) body_with_full_params with + match EConstr.kind sigma body_with_full_params with | Fix ((_, num), (_, _, bs)) -> - ( Reductionops.nf_betaiota (pf_env g) (project g) + ( Reductionops.nf_betaiota env sigma (applist ( substl (List.rev (Array.to_list all_funs_with_full_params)) @@ -1091,10 +1093,10 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num (pte_to_fix, List.rev rev_info) | _ -> (Id.Map.empty, []) in - let mk_fixes : tactic = + let mk_fixes : unit Proofview.tactic = let pre_info, infos = list_chop fun_num infos in match (pre_info, infos) with - | _, [] -> tclIDTAC + | _, [] -> Proofview.tclUNIT () | _, this_fix_info :: others_infos -> let other_fix_infos = List.map @@ -1102,51 +1104,48 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num (pre_info @ others_infos) in if List.is_empty other_fix_infos then - if this_fix_info.idx + 1 = 0 then tclIDTAC + if this_fix_info.idx + 1 = 0 then Proofview.tclUNIT () (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - Indfun_common.observe_tac + Indfun_common.New.observe_tac ~header:(str "observation") (fun _ _ -> str "h_fix " ++ int (this_fix_info.idx + 1)) - (Proofview.V82.of_tactic - (fix this_fix_info.name (this_fix_info.idx + 1))) + (fix this_fix_info.name (this_fix_info.idx + 1)) else - Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) in - let first_tac : tactic = + let first_tac : unit Proofview.tactic = (* every operations until fix creations *) (* names are already refreshed *) tclTHENLIST [ observe_tac "introducing params" - (Proofview.V82.of_tactic - (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))) - ; observe_tac "introducing predictes" - (Proofview.V82.of_tactic + (intros_mustbe_force (List.rev_map id_of_decl princ_info.params)) + ; observe_tac "introducing predicates" (intros_mustbe_force - (List.rev_map id_of_decl princ_info.predicates))) + (List.rev_map id_of_decl princ_info.predicates)) ; observe_tac "introducing branches" - (Proofview.V82.of_tactic - (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches)) ; observe_tac "building fixes" mk_fixes ] in - let intros_after_fixes : tactic = - fun gl -> - let ctxt, pte_app = decompose_prod_assum (project gl) (pf_concl gl) in - let pte, pte_args = decompose_app (project gl) pte_app in + let intros_after_fixes : unit Proofview.tactic = + Proofview.Goal.enter (fun gl -> + let sigma = Proofview.Goal.sigma gl in + let ccl = Proofview.Goal.concl gl in + let ctxt, pte_app = decompose_prod_assum sigma ccl in + let pte, pte_args = decompose_app sigma pte_app in try let pte = - try destVar (project gl) pte + try destVar sigma pte with DestKO -> anomaly (Pp.str "Property is not a variable.") in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENLIST [ (* observe_tac ("introducing args") *) - tclDO nb_args (Proofview.V82.of_tactic intro) - ; (fun g -> + tclDO nb_args intro + ; Proofview.Goal.enter (fun g -> (* replacement of the function by its body *) - let args = nLastDecls nb_args g in + let args = Tacticals.New.nLastDecls g nb_args in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) let open Context.Named.Declaration in @@ -1155,7 +1154,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num { nb_rec_hyps = -100 ; rec_hyps = [] ; info = - Reductionops.nf_betaiota (pf_env g) (project g) + Reductionops.nf_betaiota (Proofview.Goal.env g) (Proofview.Goal.sigma g) (applist (fix_body, List.rev_map mkVar args_id)) ; eq_hyps = [] } in @@ -1169,7 +1168,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num princ_params ) all_funs.(fix_info.num_in_block) fix_info.num_in_block all_funs) - ; (let do_prove = + ; let do_prove = build_proof interactive_proof (Array.to_list fnames) (Id.Map.map prove_rec_hyp ptes_to_fix) in @@ -1192,23 +1191,24 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num (* observe_tac "instancing" *) instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id)) ] - g) ] - gl + (List.rev args_id) ] + ) ] with Not_found -> let nb_args = min princ_info.nargs (List.length ctxt) in tclTHENLIST - [ tclDO nb_args (Proofview.V82.of_tactic intro) - ; (fun g -> + [ tclDO nb_args intro + ; Proofview.Goal.enter (fun g -> + let env = Proofview.Goal.env g in + let sigma = Proofview.Goal.sigma g in (* replacement of the function by its body *) - let args = nLastDecls nb_args g in + let args = Tacticals.New.nLastDecls g nb_args in let open Context.Named.Declaration in let args_id = List.map get_id args in let dyn_infos = { nb_rec_hyps = -100 ; rec_hyps = [] ; info = - Reductionops.nf_betaiota (pf_env g) (project g) + Reductionops.nf_betaiota env sigma (applist ( fbody_with_full_params , List.rev_map var_of_decl princ_params @@ -1216,13 +1216,12 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num ; eq_hyps = [] } in let fname = - destConst (project g) - (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) + destConst sigma + (fst (decompose_app sigma (List.hd (List.rev pte_args)))) in tclTHENLIST - [ Proofview.V82.of_tactic - (unfold_in_concl - [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]) + [ unfold_in_concl + [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))] ; (let do_prove = build_proof interactive_proof (Array.to_list fnames) (Id.Map.map prove_rec_hyp ptes_to_fix) @@ -1240,10 +1239,9 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] - g) ] - gl + ) ]) in - tclTHEN first_tac intros_after_fixes g + tclTHEN first_tac intros_after_fixes) (* Proof of principles of general functions *) (* let hrec_id = Recdef.hrec_id *) @@ -1254,11 +1252,11 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num (* and list_rewrite = Recdef.list_rewrite *) (* and evaluable_of_global_reference = Recdef.evaluable_of_global_reference *) -let prove_with_tcc tcc_lemma_constr eqs : tactic = +let prove_with_tcc tcc_lemma_constr eqs : unit Proofview.tactic = + let open Tacticals.New in match !tcc_lemma_constr with | Undefined -> anomaly (Pp.str "No tcc proof !!") | Value lemma -> - fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) tclTHENLIST @@ -1271,66 +1269,61 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Proofview.V82.of_tactic (Eauto.gen_eauto (false, 5) [] (Some [])) ] - gls - | Not_needed -> tclIDTAC + Eauto.gen_eauto (false, 5) [] (Some []) ] + | Not_needed -> Proofview.tclUNIT () -let backtrack_eqs_until_hrec hrec eqs : tactic = - fun gls -> +let backtrack_eqs_until_hrec hrec eqs : unit Proofview.tactic = + let open Tacticals.New in + Proofview.Goal.enter (fun gls -> + let sigma = Proofview.Goal.sigma gls in let eqs = List.map mkVar eqs in - let rewrite = - tclFIRST - (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs) - in - let _, hrec_concl = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in - let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in - let f = fst (destApp (project gls) f_app) in - let rec backtrack : tactic = - fun g -> - let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in - match EConstr.kind (project g) f_app with - | App (f', _) when eq_constr (project g) f' f -> tclIDTAC g - | _ -> tclTHEN rewrite backtrack g + let rewrite = tclFIRST (List.map Equality.rewriteRL eqs) in + let _, hrec_concl = decompose_prod sigma (Tacmach.New.pf_get_hyp_typ hrec gls) in + let f_app = Array.last (snd (destApp sigma hrec_concl)) in + let f = fst (destApp sigma f_app) in + let rec backtrack () : unit Proofview.tactic = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma gls in + let f_app = Array.last (snd (destApp sigma (Proofview.Goal.concl g))) in + match EConstr.kind sigma f_app with + | App (f', _) when eq_constr sigma f' f -> Proofview.tclUNIT () + | _ -> tclTHEN rewrite (backtrack ())) in - backtrack gls + backtrack ()) let rec rewrite_eqs_in_eqs eqs = + let open Tacticals.New in match eqs with - | [] -> tclIDTAC + | [] -> Proofview.tclUNIT () | eq :: eqs -> tclTHEN (tclMAP - (fun id gl -> + (fun id -> observe_tac (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) (tclTRY - (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences true (* dep proofs also: *) true id (mkVar eq) false))) - gl) eqs) (rewrite_eqs_in_eqs eqs) -let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = - fun gls -> - (tclTHENLIST +let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : unit Proofview.tactic = + let open Tacticals.New in + tclTHENLIST [ backtrack_eqs_until_hrec hrec eqs ; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) tclTHENS (* We must have exactly ONE subgoal !*) - (Proofview.V82.of_tactic (apply (mkVar hrec))) + (apply (mkVar hrec)) [ tclTHENLIST - [ Proofview.V82.of_tactic (keep (tcc_hyps @ eqs)) - ; Proofview.V82.of_tactic (apply (Lazy.force acc_inv)) - ; (fun g -> - if is_mes then - Proofview.V82.of_tactic + [ keep (tcc_hyps @ eqs) + ; apply (Lazy.force acc_inv) + ; if is_mes then (unfold_in_concl [ ( Locus.AllOccurrences , evaluable_of_global_reference (delayed_force ltof_ref) ) ]) - g - else tclIDTAC g) + else Proofview.tclUNIT () ; observe_tac "rew_and_finish" (tclTHENLIST [ tclTRY @@ -1339,12 +1332,10 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = ; observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs) ; observe_tac "finishing using" (tclCOMPLETE - ( Proofview.V82.of_tactic - @@ Eauto.eauto_with_bases (true, 5) + (Eauto.eauto_with_bases (true, 5) [(fun _ sigma -> (sigma, Lazy.force refl_equal))] [ Hints.Hint_db.empty TransparentState.empty - false ] )) ]) ] ] ]) - gls + false ] )) ]) ] ] ] let is_valid_hypothesis sigma predicates_name = let predicates_name = @@ -1367,11 +1358,13 @@ let is_valid_hypothesis sigma predicates_name = is_valid_hypothesis let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes - rec_arg_num rec_arg_type relation gl = - let princ_type = pf_concl gl in - let princ_info = compute_elim_sig (project gl) princ_type in + rec_arg_num rec_arg_type relation = + Proofview.Goal.enter (fun gl -> + let sigma = Proofview.Goal.sigma gl in + let princ_type = Proofview.Goal.concl gl in + let princ_info = compute_elim_sig sigma princ_type in let fresh_id = - let avoid = ref (pf_ids_of_hyps gl) in + let avoid = ref (Tacmach.New.pf_ids_of_hyps gl) in fun na -> let new_id = match na with @@ -1391,8 +1384,7 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes in let wf_tac = if is_mes then fun b -> - Proofview.V82.of_tactic - @@ Recdef.tclUSER_if_not_mes Tacticals.New.tclIDTAC b None + Recdef.tclUSER_if_not_mes Tacticals.New.tclIDTAC b None else fun _ -> prove_with_tcc tcc_lemma_ref [] in let real_rec_arg_num = rec_arg_num - princ_info.nparams in @@ -1429,28 +1421,25 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id)))) in + let open Tacticals.New in let revert l = tclTHEN - (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) - (Proofview.V82.of_tactic (clear l)) + (Tactics.generalize (List.map mkVar l)) + (clear l) in let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in - let prove_rec_arg_acc g = - ((* observe_tac "prove_rec_arg_acc" *) + let prove_rec_arg_acc = + (* observe_tac "prove_rec_arg_acc" *) tclCOMPLETE (tclTHEN - (Proofview.V82.of_tactic (assert_by (Name wf_thm_id) (mkApp (delayed_force well_founded, [|input_type; relation|])) - (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) - (tclCOMPLETE (wf_tac is_mes)) g)))) + (tclCOMPLETE (wf_tac is_mes))) ((* observe_tac *) (* "apply wf_thm" *) - Proofview.V82.of_tactic (Tactics.Simple.apply - (mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|])))))) - g + (mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|]))))) in let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in let lemma = @@ -1472,24 +1461,24 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes (* f::(list_diff r check_list) *) (* in *) let tcc_list = ref [] in - let start_tac gls = - let hyps = pf_ids_of_hyps gls in + let start_tac = + Proofview.Goal.enter (fun gls -> + let hyps = Tacmach.New.pf_ids_of_hyps gls in let hid = next_ident_away_in_goal (Id.of_string "prov") (Id.Set.of_list hyps) in tclTHENLIST - [ Proofview.V82.of_tactic (generalize [lemma]) - ; Proofview.V82.of_tactic (Simple.intro hid) - ; Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)) - ; (fun g -> - let new_hyps = pf_ids_of_hyps g in + [ generalize [lemma] + ; Simple.intro hid + ; Elim.h_decompose_and (mkVar hid) + ; Proofview.Goal.enter (fun g -> + let new_hyps = Tacmach.New.pf_ids_of_hyps g in tcc_list := List.rev (List.subtract Id.equal new_hyps (hid :: hyps)); if List.is_empty !tcc_list then begin tcc_list := [hid]; - tclIDTAC g + Proofview.tclUNIT () end - else thin [hid] g) ] - gls + else clear [hid]) ]) in tclTHENLIST [ observe_tac "start_tac" start_tac @@ -1498,18 +1487,17 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes (get_name %> Nameops.Name.get_id) ( princ_info.args @ princ_info.branches @ princ_info.predicates @ princ_info.params )) - ; Proofview.V82.of_tactic - (assert_by (Name acc_rec_arg_id) + ; assert_by (Name acc_rec_arg_id) (mkApp (delayed_force acc_rel, [|input_type; relation; mkVar rec_arg_id|])) - (Proofview.V82.tactic prove_rec_arg_acc)) + prove_rec_arg_acc ; revert (List.rev (acc_rec_arg_id :: args_ids)) - ; Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1)) + ; fix fix_id (List.length args_ids + 1) ; h_intros (List.rev (acc_rec_arg_id :: args_ids)) - ; Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)) - ; (fun gl' -> + ; Equality.rewriteLR (mkConst eq_ref) + ; Proofview.Goal.enter (fun gl' -> let body = - let _, args = destApp (project gl') (pf_concl gl') in + let _, args = destApp (Proofview.Goal.sigma gl') (Proofview.Goal.concl gl') in Array.last args in let body_info rec_hyps = @@ -1547,7 +1535,7 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes (princ_info.args @ princ_info.params) @ [acc_rec_arg_id] ) eqs) - ; is_valid = is_valid_hypothesis (project gl') predicates_names } + ; is_valid = is_valid_hypothesis (Proofview.Goal.sigma gl') predicates_names } in let ptes_info : pte_info Id.Map.t = List.fold_left @@ -1561,5 +1549,4 @@ let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes (instantiate_hyps_with_args make_proof (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids)) - gl') ] - gl + ) ]) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 52089ca7fb..096ea5fed5 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Names val prove_princ_for_struct : @@ -7,7 +17,7 @@ val prove_princ_for_struct : -> Constant.t array -> EConstr.constr array -> int - -> Tacmach.tactic + -> unit Proofview.tactic val prove_principle_for_gen : Constant.t * Constant.t * Constant.t @@ -22,6 +32,6 @@ val prove_principle_for_gen : -> (* the type of the recursive argument *) EConstr.constr -> (* the wf relation used to prove the function *) - Tacmach.tactic + unit Proofview.tactic (* val is_pte : rel_declaration -> bool *) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 45b1713441..402082d01e 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -13,7 +13,8 @@ open Names open Indfun_common module RelDecl = Context.Rel.Declaration -let observe_tac s = observe_tac (fun _ _ -> Pp.str s) +let observe_tac s = + New.observe_tac ~header:(Pp.str "observation") (fun _ _ -> Pp.str s) (* Construct a fixpoint as a Glob_term @@ -210,9 +211,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs (EConstr.of_constr new_principle_type) in let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - let ftac = - Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams) - in + let ftac = proof_tac (Array.map map funs) mutr_nparams in let env = Global.env () in let uctx = Evd.evar_universe_context sigma in let typ = EConstr.of_constr new_principle_type in @@ -335,7 +334,7 @@ let generate_principle (evd : Evd.evar_map ref) pconstants on_error is_general -> Names.Constant.t array -> EConstr.constr array -> int - -> Tacmach.tactic) : unit = + -> unit Proofview.tactic) : unit = let names = List.map (function {Vernacexpr.fname = {CAst.v = name}} -> name) fix_rec_l in @@ -442,7 +441,7 @@ let register_struct is_rec fixpoint_exprl = let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type relation (_ : int) (_ : Names.Constant.t array) (_ : EConstr.constr array) (_ : int) : - Tacmach.tactic = + unit Proofview.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation @@ -593,14 +592,14 @@ let rec generate_fresh_id x avoid i = id :: generate_fresh_id x (id :: avoid) (pred i) let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : - Tacmach.tactic = + unit Proofview.tactic = let open Constr in let open EConstr in let open Context.Rel.Declaration in - let open Tacmach in + let open Tacmach.New in let open Tactics in - let open Tacticals in - fun g -> + let open Tacticals.New in + Proofview.Goal.enter (fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\] @@ -614,7 +613,7 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : 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 = Termops.nb_prod (project g) (pf_concl g) - 2 in + let nb_fun_args = Termops.nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names @ pf_ids_of_hyps g in (* Since we cannot ensure that the functional principle is defined in the @@ -646,7 +645,7 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : (* The next to referencies will be used to find out which constructor to apply in each branch *) let ind_number = ref 0 and min_constr_number = ref 0 in (* The tactic to prove the ith branch of the principle *) - let prove_branche i g = + let prove_branch i pat = (* We get the identifiers of this branch *) let pre_args = List.fold_right @@ -654,7 +653,7 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : match pat with | Tactypes.IntroNaming (Namegen.IntroIdentifier id) -> id :: acc | _ -> CErrors.anomaly (Pp.str "Not an identifier.")) - (List.nth intro_pats (pred i)) + pat [] in (* and get the real args of the branch by unfolding the defined constant *) @@ -668,8 +667,8 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_get_hyp_typ g hid in - let sigma = project g in + let type_of_hid = pf_get_hyp_typ hid g in + let sigma = Proofview.Goal.sigma g in match EConstr.kind sigma type_of_hid with | Prod (_, _, t') -> ( match EConstr.kind sigma t' with @@ -733,33 +732,28 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *) (tclTHENLIST [ observe_tac "h_intro_patterns " - (let l = List.nth intro_pats (pred i) in - match l with + (match pat with | [] -> tclIDTAC - | _ -> Proofview.V82.of_tactic (intro_patterns false l)) + | _ -> intro_patterns false pat) ; (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) - Proofview.V82.of_tactic - (reduce + reduce (Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false ; Genredexpr.rConst = [] }) - Locusops.onConcl) - ; observe_tac "toto " tclIDTAC + Locusops.onConcl + ; observe_tac "toto " (Proofview.tclUNIT ()) ; (* introducing the result of the graph and the equality hypothesis *) observe_tac "introducing" - (tclMAP - (fun x -> Proofview.V82.of_tactic (Simple.intro x)) - [res; hres]) + (tclMAP Simple.intro [res; hres]) ; (* replacing [res] with its value *) observe_tac "rewriting res value" - (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))) + (Equality.rewriteLR (mkVar hres)) ; (* Conclusion *) - observe_tac "exact" (fun g -> - Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ]) - g + observe_tac "exact" (Proofview.Goal.enter (fun g -> + exact_check (app_constructor g))) ]) in (* end of branche proof *) let lemmas = @@ -808,7 +802,7 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in - ( Reductionops.nf_zeta (pf_env g) (project g) p :: bindings + ( Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g) p :: bindings , id :: avoid )) ([], avoid) princ_infos.predicates lemmas)) in @@ -816,27 +810,20 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : in tclTHENLIST [ observe_tac "principle" - (Proofview.V82.of_tactic - (assert_by (Name principle_id) princ_type - (exact_check f_principle))) + (assert_by (Name principle_id) princ_type + (exact_check f_principle)) ; observe_tac "intro args_names" - (tclMAP - (fun id -> Proofview.V82.of_tactic (Simple.intro id)) - args_names) + (tclMAP Simple.intro args_names) ; (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) observe_tac "idtac" tclIDTAC - ; tclTHEN_i - (observe_tac "functional_induction" (fun gl -> + ; tclTHENS + (observe_tac "functional_induction" (Proofview.Goal.enter (fun gl -> let term = mkApp (mkVar principle_id, Array.of_list bindings) in - let gl', _ty = - pf_eapply (Typing.type_of ~refresh:true) gl term - in - Proofview.V82.of_tactic (apply term) gl')) - (fun i g -> - observe_tac - ("proving branche " ^ string_of_int i) - (prove_branche i) g) ] - g + tclTYPEOFTHEN ~refresh:true term (fun _ _ -> + apply term)))) + (List.map_i (fun i pat -> observe_tac + ("proving branch " ^ string_of_int i) + (prove_branch i pat)) 1 intro_pats) ]) (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] is the tactic used to prove completeness lemma. @@ -865,7 +852,7 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : *) -let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl +let thin = Tactics.clear (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis (unfolding, substituting, destructing cases \ldots) @@ -882,160 +869,146 @@ let tauto = (* [generalize_dependent_of x hyp g] generalize every hypothesis which depends of [x] but [hyp] *) -let generalize_dependent_of x hyp g = +let generalize_dependent_of x hyp = let open Context.Named.Declaration in - let open Tacmach in - let open Tacticals in + let open Tacticals.New in + Proofview.Goal.enter (fun g -> tclMAP (function | LocalAssum ({Context.binder_name = id}, t) when (not (Id.equal id hyp)) - && Termops.occur_var (pf_env g) (project g) x t -> + && Termops.occur_var (Proofview.Goal.env g) (Proofview.Goal.sigma g) x t -> tclTHEN - (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) + (Tactics.generalize [EConstr.mkVar id]) (thin [id]) - | _ -> tclIDTAC) - (pf_hyps g) g + | _ -> Proofview.tclUNIT ()) + (Proofview.Goal.hyps g)) -let rec intros_with_rewrite g = - observe_tac "intros_with_rewrite" intros_with_rewrite_aux g +let rec intros_with_rewrite () = + observe_tac "intros_with_rewrite" (intros_with_rewrite_aux ()) -and intros_with_rewrite_aux : Tacmach.tactic = +and intros_with_rewrite_aux () : unit Proofview.tactic = let open Constr in let open EConstr in - let open Tacmach in + let open Tacmach.New in let open Tactics in - let open Tacticals in - fun g -> + let open Tacticals.New in + Proofview.Goal.enter (fun g -> let eq_ind = make_eq () in - let sigma = project g in - match EConstr.kind sigma (pf_concl g) with + let sigma = Proofview.Goal.sigma g in + match EConstr.kind sigma (Proofview.Goal.concl g) with | Prod (_, t, t') -> ( match EConstr.kind sigma t with | App (eq, args) when EConstr.eq_constr sigma eq eq_ind -> - if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) then + if Reductionops.is_conv (Proofview.Goal.env g) (Proofview.Goal.sigma g) args.(1) args.(2) then let id = pf_get_new_id (Id.of_string "y") g in tclTHENLIST - [ Proofview.V82.of_tactic (Simple.intro id) + [ Simple.intro id ; thin [id] - ; intros_with_rewrite ] - g + ; intros_with_rewrite () ] else if isVar sigma args.(1) - && Environ.evaluable_named (destVar sigma args.(1)) (pf_env g) + && Environ.evaluable_named (destVar sigma args.(1)) (Proofview.Goal.env g) then tclTHENLIST - [ Proofview.V82.of_tactic - (unfold_in_concl + [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ]) + , Names.EvalVarRef (destVar sigma args.(1)) ) ] ; tclMAP (fun id -> tclTRY - (Proofview.V82.of_tactic - (unfold_in_hyp + (unfold_in_hyp [ ( Locus.AllOccurrences , Names.EvalVarRef (destVar sigma args.(1)) ) ] - (destVar sigma args.(1), Locus.InHyp)))) + (destVar sigma args.(1), Locus.InHyp))) (pf_ids_of_hyps g) - ; intros_with_rewrite ] - g + ; intros_with_rewrite () ] else if isVar sigma args.(2) - && Environ.evaluable_named (destVar sigma args.(2)) (pf_env g) + && Environ.evaluable_named (destVar sigma args.(2)) (Proofview.Goal.env g) then tclTHENLIST - [ Proofview.V82.of_tactic - (unfold_in_concl + [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ]) + , Names.EvalVarRef (destVar sigma args.(2)) ) ] ; tclMAP (fun id -> tclTRY - (Proofview.V82.of_tactic - (unfold_in_hyp + (unfold_in_hyp [ ( Locus.AllOccurrences , Names.EvalVarRef (destVar sigma args.(2)) ) ] - (destVar sigma args.(2), Locus.InHyp)))) + (destVar sigma args.(2), Locus.InHyp))) (pf_ids_of_hyps g) - ; intros_with_rewrite ] - g + ; intros_with_rewrite () ] else if isVar sigma args.(1) then let id = pf_get_new_id (Id.of_string "y") g in tclTHENLIST - [ Proofview.V82.of_tactic (Simple.intro id) + [ Simple.intro id ; generalize_dependent_of (destVar sigma args.(1)) id - ; tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))) - ; intros_with_rewrite ] - g + ; tclTRY (Equality.rewriteLR (mkVar id)) + ; intros_with_rewrite () ] else if isVar sigma args.(2) then let id = pf_get_new_id (Id.of_string "y") g in tclTHENLIST - [ Proofview.V82.of_tactic (Simple.intro id) + [ Simple.intro id ; generalize_dependent_of (destVar sigma args.(2)) id - ; tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))) - ; intros_with_rewrite ] - g + ; tclTRY (Equality.rewriteRL (mkVar id)) + ; intros_with_rewrite () ] else let id = pf_get_new_id (Id.of_string "y") g in tclTHENLIST - [ Proofview.V82.of_tactic (Simple.intro id) - ; tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))) - ; intros_with_rewrite ] - g + [ Simple.intro id + ; tclTRY (Equality.rewriteLR (mkVar id)) + ; intros_with_rewrite () ] | 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 + tauto | Case (_, _, _, v, _) -> tclTHENLIST - [Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite] - g + [simplest_case v; intros_with_rewrite ()] | LetIn _ -> tclTHENLIST - [ Proofview.V82.of_tactic - (reduce + [ reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) - Locusops.onConcl) - ; intros_with_rewrite ] - g + Locusops.onConcl + ; intros_with_rewrite () ] | _ -> let id = pf_get_new_id (Id.of_string "y") g in tclTHENLIST - [Proofview.V82.of_tactic (Simple.intro id); intros_with_rewrite] - g ) + [Simple.intro id; intros_with_rewrite ()] + ) | LetIn _ -> tclTHENLIST - [ Proofview.V82.of_tactic - (reduce + [ reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) - Locusops.onConcl) - ; intros_with_rewrite ] - g - | _ -> tclIDTAC g + Locusops.onConcl + ; intros_with_rewrite () ] + | _ -> Proofview.tclUNIT ()) -let rec reflexivity_with_destruct_cases g = +let rec reflexivity_with_destruct_cases () = let open Constr in let open EConstr in - let open Tacmach in + let open Tacmach.New in let open Tactics in - let open Tacticals in + let open Tacticals.New in + Proofview.Goal.enter (fun g -> let destruct_case () = try match - EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) + EConstr.kind (Proofview.Goal.sigma g) (snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(2) with | Case (_, _, _, v, _) -> tclTHENLIST - [ Proofview.V82.of_tactic (simplest_case v) - ; Proofview.V82.of_tactic intros + [ simplest_case v + ; intros ; observe_tac "reflexivity_with_destruct_cases" - reflexivity_with_destruct_cases ] - | _ -> Proofview.V82.of_tactic reflexivity - with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity + (reflexivity_with_destruct_cases ()) ] + | _ -> reflexivity + with e when CErrors.noncritical e -> reflexivity in let eq_ind = make_eq () in let my_inj_flags = @@ -1048,29 +1021,29 @@ let rec reflexivity_with_destruct_cases g = } in let discr_inject = - Tacticals.onAllHypsAndConcl (fun sc g -> + onAllHypsAndConcl (fun sc -> match sc with - | None -> tclIDTAC g - | Some id -> ( - match EConstr.kind (project g) (pf_get_hyp_typ g id) with - | App (eq, [|_; t1; t2|]) when EConstr.eq_constr (project g) eq eq_ind + | None -> Proofview.tclUNIT () + | Some id -> + Proofview.Goal.enter (fun g -> + match EConstr.kind (Proofview.Goal.sigma g) (pf_get_hyp_typ id g) with + | App (eq, [|_; t1; t2|]) when EConstr.eq_constr (Proofview.Goal.sigma g) eq eq_ind -> - if Equality.discriminable (pf_env g) (project g) t1 t2 then - Proofview.V82.of_tactic (Equality.discrHyp id) g + if Equality.discriminable (Proofview.Goal.env g) (Proofview.Goal.sigma g) t1 t2 then + Equality.discrHyp id else if - Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 + Equality.injectable (Proofview.Goal.env g) (Proofview.Goal.sigma g) ~keep_proofs:None t1 t2 then tclTHENLIST - [ Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id) + [ Equality.injHyp my_inj_flags None id ; thin [id] - ; intros_with_rewrite ] - g - else tclIDTAC g - | _ -> tclIDTAC g )) + ; intros_with_rewrite () ] + else Proofview.tclUNIT () + | _ -> Proofview.tclUNIT ())) in - (tclFIRST + tclFIRST [ observe_tac "reflexivity_with_destruct_cases : reflexivity" - (Proofview.V82.of_tactic reflexivity) + reflexivity ; observe_tac "reflexivity_with_destruct_cases : destruct_case" (destruct_case ()) ; (* We reach this point ONLY if @@ -1080,38 +1053,37 @@ let rec reflexivity_with_destruct_cases g = either at least an injectable one and we do the injection before continuing *) observe_tac "reflexivity_with_destruct_cases : others" - (tclTHEN (tclPROGRESS discr_inject) reflexivity_with_destruct_cases) ]) - g + (tclTHEN (tclPROGRESS discr_inject) (reflexivity_with_destruct_cases ())) ]) let prove_fun_complete funcs graphs schemes lemmas_types_infos i : - Tacmach.tactic = + unit Proofview.tactic = let open EConstr in - let open Tacmach in + let open Tacmach.New in let open Tactics in - let open Tacticals in - fun g -> + let open Tacticals.New in + Proofview.Goal.enter (fun g -> (* We compute the types of the different mutually recursive lemmas in $\zeta$ normal form *) let lemmas = Array.map (fun (_, (ctxt, concl)) -> - Reductionops.nf_zeta (pf_env g) (project g) + Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma 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 = - Reductionops.nf_zeta (pf_env g) (project g) + Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g) (EConstr.of_constr schemes.(i)) in - let g, princ_type = tac_type_of g graph_principle in - let princ_infos = Tactics.compute_elim_sig (project g) princ_type in + tclTYPEOFTHEN graph_principle (fun sigma princ_type -> + let princ_infos = Tactics.compute_elim_sig sigma princ_type in (* Then we get the number of argument of the function and compute a fresh name for each of them *) - let nb_fun_args = Termops.nb_prod (project g) (pf_concl g) - 2 in + let nb_fun_args = Termops.nb_prod sigma (Proofview.Goal.concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names @ pf_ids_of_hyps g in (* and fresh names for res H and the principle (cf bug bug #1174) *) @@ -1130,17 +1102,17 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : List.map (fun id -> id) (generate_fresh_id (Id.of_string "y") ids - (Termops.nb_prod (project g) (RelDecl.get_type decl)))) + (Termops.nb_prod (Proofview.Goal.sigma g) (RelDecl.get_type decl)))) branches in (* We will need to change the function by its body using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite *) - let rewrite_tac j ids : Tacmach.tactic = + let rewrite_tac j ids : unit Proofview.tactic = let graph_def = graphs.(j) in let infos = - match find_Function_infos (fst (destConst (project g) funcs.(j))) with + match find_Function_infos (fst (destConst (Proofview.Goal.sigma g) funcs.(j))) with | None -> CErrors.user_err Pp.(str "No graph found") | Some infos -> infos in @@ -1155,27 +1127,25 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : CErrors.anomaly (Pp.str "Cannot find equation lemma.") in tclTHENLIST - [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids - ; Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)) + [ tclMAP Simple.intro ids + ; Equality.rewriteLR (mkConst eq_lemma) ; (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - Proofview.V82.of_tactic - (reduce + reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) - Locusops.onConcl) - ; Proofview.V82.of_tactic (generalize (List.map mkVar ids)) + Locusops.onConcl + ; generalize (List.map mkVar ids) ; thin ids ] else - Proofview.V82.of_tactic - (unfold_in_concl + unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef (fst (destConst (project g) f)) ) ]) + , Names.EvalConstRef (fst (destConst (Proofview.Goal.sigma g) f)) ) ] in (* The proof of each branche itself *) let ind_number = ref 0 in let min_constr_number = ref 0 in - let prove_branche i g = + let prove_branch i this_branche_ids = (* we fist compute the inductive corresponding to the branch *) let this_ind_number = let constructor_num = i - !min_constr_number in @@ -1189,40 +1159,33 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : !ind_number end in - let this_branche_ids = List.nth intro_pats (pred i) in tclTHENLIST [ (* we expand the definition of the function *) observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids) ; (* introduce hypothesis with some rewrite *) - observe_tac "intros_with_rewrite (all)" intros_with_rewrite + observe_tac "intros_with_rewrite (all)" (intros_with_rewrite ()) ; (* The proof is (almost) complete *) - observe_tac "reflexivity" reflexivity_with_destruct_cases ] - g + observe_tac "reflexivity" (reflexivity_with_destruct_cases ()) ] in let params_names = fst (List.chop princ_infos.nparams args_names) in let open EConstr in let params = List.map mkVar params_names in tclTHENLIST - [ tclMAP - (fun id -> Proofview.V82.of_tactic (Simple.intro id)) - (args_names @ [res; hres]) + [ tclMAP Simple.intro (args_names @ [res; hres]) ; observe_tac "h_generalize" - (Proofview.V82.of_tactic (generalize [ mkApp ( applist (graph_principle, params) - , Array.map (fun c -> applist (c, params)) lemmas ) ])) - ; Proofview.V82.of_tactic (Simple.intro graph_principle_id) + , Array.map (fun c -> applist (c, params)) lemmas ) ]) + ; Simple.intro graph_principle_id ; observe_tac "" - (tclTHEN_i + (tclTHENS (observe_tac "elim" - (Proofview.V82.of_tactic (elim false None (mkVar hres, Tactypes.NoBindings) - (Some (mkVar graph_principle_id, Tactypes.NoBindings))))) - (fun i g -> observe_tac "prove_branche" (prove_branche i) g)) ] - g + (Some (mkVar graph_principle_id, Tactypes.NoBindings)))) + (List.map_i (fun i pat -> observe_tac "prove_branch" (prove_branch i pat)) 1 intro_pats)) ])) exception No_graph_found @@ -1524,7 +1487,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in let lemma = Declare.Proof.start ~cinfo ~info !evd in let lemma = - fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma + fst @@ Declare.Proof.by (proving_tac i) lemma in let (_ : _ list) = Declare.Proof.save_regular ~proof:lemma @@ -1592,10 +1555,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lemma = fst (Declare.Proof.by - (Proofview.V82.tactic (observe_tac ("prove completeness (" ^ Id.to_string f_id ^ ")") - (proving_tac i))) + (proving_tac i)) lemma) in let (_ : _ list) = diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index af53f16e1f..fadf0d0b3e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -395,8 +395,7 @@ let jmeq_refl () = with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = - Proofview.V82.of_tactic - (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l) + Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" @@ -428,13 +427,12 @@ let evaluable_of_global_reference r = | _ -> assert false let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) = - let open Tacticals in + let open Tacticals.New in (tclREPEAT (List.fold_right (fun (eq, b) i -> tclORELSE - (Proofview.V82.of_tactic - ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) + ((if b then Equality.rewriteLR else Equality.rewriteRL) eq) i) (if rev then List.rev eqs else eqs) (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"]) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 396db55458..7b7044fdaf 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -90,7 +90,7 @@ exception Defining_principle of exn exception ToShow of exn val is_strict_tcc : unit -> bool -val h_intros : Names.Id.t list -> Tacmach.tactic +val h_intros : Names.Id.t list -> unit Proofview.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed @@ -102,7 +102,7 @@ val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference -val list_rewrite : bool -> (EConstr.constr * bool) list -> Tacmach.tactic +val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic val decompose_lam_n : Evd.evar_map diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 066ade07d2..90a8d82700 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -23,8 +23,7 @@ open Nameops open CErrors open Util open UnivGen -open Tacticals -open Tacmach +open Tacticals.New open Tactics open Nametab open Tacred @@ -94,7 +93,7 @@ let const_of_ref = function (* Generic values *) let pf_get_new_ids idl g = - let ids = pf_ids_of_hyps g in + let ids = Tacmach.New.pf_ids_of_hyps g in let ids = Id.Set.of_list ids in List.fold_right (fun id acc -> @@ -105,8 +104,8 @@ let next_ident_away_in_goal ids avoid = next_ident_away_in_goal ids (Id.Set.of_list avoid) let compute_renamed_type gls id = - rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty - (*no rels*) [] (pf_get_hyp_typ gls id) + rename_bound_vars_as_displayed (Proofview.Goal.sigma gls) (*no avoid*) Id.Set.empty + (*no rels*) [] (Tacmach.New.pf_get_hyp_typ id gls) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" @@ -218,20 +217,6 @@ let (declare_f : fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref) -let observe_tclTHENLIST s tacl = - if do_observe () then - let rec aux n = function - | [] -> tclIDTAC - | [tac] -> - observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) tac - | tac :: tacl -> - observe_tac - (fun env sigma -> s env sigma ++ spc () ++ int n) - (tclTHEN tac (aux (succ n) tacl)) - in - aux 0 tacl - else tclTHENLIST tacl - module New = struct open Tacticals.New @@ -364,11 +349,11 @@ type ('a, 'b) journey_info_tac = -> (* the arguments of the constructor *) 'b infos -> (* infos of the caller *) - ('b infos -> tactic) + ('b infos -> unit Proofview.tactic) -> (* the continuation tactic of the caller *) 'b infos -> (* argument of the tactic *) - tactic + unit Proofview.tactic (* journey_info : specifies the actions to do on the different term constructors during the traveling of the term *) @@ -376,7 +361,7 @@ type journey_info = { letiN : (Name.t * constr * types * constr, constr) journey_info_tac ; lambdA : (Name.t * types * constr, constr) journey_info_tac ; casE : - ((constr infos -> tactic) -> constr infos -> tactic) + ((constr infos -> unit Proofview.tactic) -> constr infos -> unit Proofview.tactic) -> ( case_info * constr * (constr, EInstance.t) case_invert @@ -397,9 +382,9 @@ let add_vars sigma forbidden e = in aux forbidden e -let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = - fun g -> - let rev_context, b = decompose_lam_n (project g) nb_lam e in +let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : unit Proofview.tactic = + Proofview.Goal.enter (fun g -> + let rev_context, b = decompose_lam_n (Proofview.Goal.sigma g) nb_lam e in let ids = List.fold_left (fun acc (na, _) -> @@ -411,27 +396,27 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = in let rev_ids = pf_get_new_ids (List.rev ids) g in let new_b = substl (List.map mkVar rev_ids) b in - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ h_intros (List.rev rev_ids) - ; Proofview.V82.of_tactic - (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())) - ; onLastHypId (fun heq -> - observe_tclTHENLIST + ; intro_using_then teq_id (fun _ -> Proofview.tclUNIT ()) + ; Tacticals.New.onLastHypId (fun heq -> + New.observe_tclTHENLIST (fun _ _ -> str "treat_case2") - [ Proofview.V82.of_tactic (clear to_intros) + [ clear to_intros ; h_intros to_intros - ; (fun g' -> - let ty_teq = pf_get_hyp_typ g' heq in + ; Proofview.Goal.enter (fun g' -> + let sigma = Proofview.Goal.sigma g' in + let ty_teq = Tacmach.New.pf_get_hyp_typ heq g' in let teq_lhs, teq_rhs = let _, args = - try destApp (project g') ty_teq + try destApp sigma ty_teq with DestKO -> assert false in (args.(1), args.(2)) in let new_b' = - Termops.replace_term (project g') teq_lhs teq_rhs new_b + Termops.replace_term sigma teq_lhs teq_rhs new_b in let new_infos = { infos with @@ -439,15 +424,15 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = ; eqs = heq :: infos.eqs ; forbidden_ids = ( if forbid_new_ids then - add_vars (project g') infos.forbidden_ids new_b' + add_vars sigma infos.forbidden_ids new_b' else infos.forbidden_ids ) } in - finalize_tac new_infos g') ]) ] - g + finalize_tac new_infos) ]) ]) -let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = - let sigma = project g in - let env = pf_env g in +let rec travel_aux jinfo continuation_tac (expr_info : constr infos) = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in + let env = Proofview.Goal.env g in match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") @@ -459,14 +444,13 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = in travel jinfo new_continuation_tac {expr_info with info = b; is_final = false} - g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") | Prod _ -> ( try check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) expr_info.info; - jinfo.otherS () expr_info continuation_tac expr_info g + jinfo.otherS () expr_info continuation_tac expr_info with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" ( str "the term " @@ -478,7 +462,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) expr_info.info; - jinfo.otherS () expr_info continuation_tac expr_info g + jinfo.otherS () expr_info continuation_tac expr_info with e when CErrors.noncritical e -> user_err ~hdr:"Recdef.travel" ( str "the term " @@ -491,11 +475,10 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = in travel jinfo continuation_tac_a {expr_info with info = a; is_main_branch = false; is_final = false} - g | App _ -> ( let f, args = decompose_app sigma expr_info.info in if EConstr.eq_constr sigma f expr_info.f_constr then - jinfo.app_reC (f, args) expr_info continuation_tac expr_info g + jinfo.app_reC (f, args) expr_info continuation_tac expr_info else match EConstr.kind sigma f with | App _ -> assert false (* f is coming from a decompose_app *) @@ -506,7 +489,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = jinfo.apP (f, args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac - new_infos g + new_infos | Case _ -> user_err ~hdr:"Recdef.travel" ( str "the term " @@ -519,11 +502,11 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = ( Pp.str "travel_aux : unexpected " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str "." ) ) - | Cast (t, _, _) -> travel jinfo continuation_tac {expr_info with info = t} g + | Cast (t, _, _) -> travel jinfo continuation_tac {expr_info with info = t} | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ |Float _ -> let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in - new_continuation_tac expr_info g + new_continuation_tac expr_info) and travel_args jinfo is_final continuation_tac infos = let f_args', args = infos.info in @@ -538,97 +521,92 @@ and travel_args jinfo is_final continuation_tac infos = travel jinfo new_continuation_tac {infos with info = arg; is_final = false} and travel jinfo continuation_tac expr_info = - observe_tac + New.observe_tac (fun env sigma -> str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) -let rec prove_lt hyple g = - let sigma = project g in +let rec prove_lt hyple = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in begin try let varx, varz = - match decompose_app sigma (pf_concl g) with + match decompose_app sigma (Proofview.Goal.concl g) with | _, x :: z :: _ when isVar sigma x && isVar sigma z -> (x, z) | _ -> assert false in let h = List.find (fun id -> - match decompose_app sigma (pf_get_hyp_typ g id) with + match decompose_app sigma (Tacmach.New.pf_get_hyp_typ id g) with | _, t :: _ -> EConstr.eq_constr sigma t varx | _ -> false) hyple in let y = - List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h)))) + List.hd (List.tl (snd (decompose_app sigma (Tacmach.New.pf_get_hyp_typ h g)))) in - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "prove_lt1") - [ Proofview.V82.of_tactic - (apply (mkApp (le_lt_trans (), [|varx; y; varz; mkVar h|]))) - ; observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ] + [ apply (mkApp (le_lt_trans (), [|varx; y; varz; mkVar h|])) + ; New.observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ] with Not_found -> - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "prove_lt2") - [ Proofview.V82.of_tactic (apply (delayed_force lt_S_n)) - ; observe_tac - (fun _ _ -> str "assumption: " ++ Printer.pr_goal g) - (Proofview.V82.of_tactic assumption) ] - end - g - -let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g = + [ apply (delayed_force lt_S_n) + ; New.observe_tac + (fun _ _ -> str "assumption: " ++ Printer.pr_goal Evd.{it = Proofview.Goal.goal g; sigma}) + assumption ] + end) + +let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> match lbounds with | [] -> - let ids = pf_ids_of_hyps g in + let ids = Tacmach.New.pf_ids_of_hyps g in let s_max = mkApp (delayed_force coq_S, [|bound|]) in let k = next_ident_away_in_goal k_id ids in let ids = k :: ids in let h' = next_ident_away_in_goal h'_id ids in let ids = h' :: ids in let def = next_ident_away_in_goal def_id ids in - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux1") - [ Proofview.V82.of_tactic (split (ImplicitBindings [s_max])) - ; Proofview.V82.of_tactic - (intro_then (fun id -> - Proofview.V82.tactic - (observe_tac + [ split (ImplicitBindings [s_max]) + ; intro_then (fun id -> + (New.observe_tac (fun _ _ -> str "destruct_bounds_aux") (tclTHENS - (Proofview.V82.of_tactic (simplest_case (mkVar id))) - [ observe_tclTHENLIST + (simplest_case (mkVar id)) + [ New.observe_tclTHENLIST (fun _ _ -> str "") - [ Proofview.V82.of_tactic - (intro_using_then h_id + [ intro_using_then h_id (* We don't care about the refreshed name, accessed only through auto? *) - (fun _ -> Proofview.tclUNIT ())) - ; Proofview.V82.of_tactic - (simplest_elim - (mkApp (delayed_force lt_n_O, [|s_max|]))) - ; Proofview.V82.of_tactic default_full_auto ] - ; observe_tclTHENLIST + (fun _ -> Proofview.tclUNIT ()) + ; simplest_elim + (mkApp (delayed_force lt_n_O, [|s_max|])) + ; default_full_auto ] + ; New.observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux2") - [ observe_tac + [ New.observe_tac (fun _ _ -> str "clearing k ") - (Proofview.V82.of_tactic (clear [id])) + (clear [id]) ; h_intros [k; h'; def] - ; observe_tac + ; New.observe_tac (fun _ _ -> str "simple_iter") - (Proofview.V82.of_tactic - (simpl_iter Locusops.onConcl)) - ; observe_tac + (simpl_iter Locusops.onConcl) + ; New.observe_tac (fun _ _ -> str "unfold functional") - (Proofview.V82.of_tactic - (unfold_in_concl + (unfold_in_concl [ ( Locus.OnlyOccurrences [1] , evaluable_of_global_reference - infos.func ) ])) - ; observe_tclTHENLIST + infos.func ) ]) + ; New.observe_tclTHENLIST (fun _ _ -> str "test") [ list_rewrite true (List.fold_right @@ -638,29 +616,26 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g = ; (* list_rewrite true *) (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *) (* ; *) - observe_tac + New.observe_tac (fun _ _ -> str "finishing") (tclORELSE - (Proofview.V82.of_tactic - intros_reflexivity) - (observe_tac + intros_reflexivity + (New.observe_tac (fun _ _ -> str "calling prove_lt") - (prove_lt hyple))) ] ] ])))) ] - g + (prove_lt hyple))) ] ] ]))) ] | (_, v_bound) :: l -> - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux3") - [ Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)) - ; Proofview.V82.of_tactic (clear [v_bound]) - ; tclDO 2 (Proofview.V82.of_tactic intro) + [ simplest_elim (mkVar v_bound) + ; clear [v_bound] + ; tclDO 2 intro ; onNthHypId 1 (fun p_hyp -> onNthHypId 2 (fun p -> - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux4") - [ Proofview.V82.of_tactic - (simplest_elim - (mkApp (delayed_force max_constr, [|bound; mkVar p|]))) - ; tclDO 3 (Proofview.V82.of_tactic intro) + [ simplest_elim + (mkApp (delayed_force max_constr, [|bound; mkVar p|])) + ; tclDO 3 intro ; onNLastHypsId 3 (fun lids -> match lids with | [hle2; hle1; pmax] -> @@ -669,8 +644,7 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g = , hle1 :: hle2 :: hyple , mkVar p_hyp :: rechyps ) l - | _ -> assert false) ])) ] - g + | _ -> assert false) ])) ]) let destruct_bounds infos = destruct_bounds_aux infos @@ -679,32 +653,33 @@ let destruct_bounds infos = let terminate_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "terminate_app1") [ continuation_tac infos - ; observe_tac + ; New.observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))) - ; observe_tac + (split (ImplicitBindings [infos.info])) + ; New.observe_tac (fun _ _ -> str "destruct_bounds (1)") (destruct_bounds infos) ] else continuation_tac infos let terminate_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "terminate_others") [ continuation_tac infos - ; observe_tac + ; New.observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))) - ; observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos) + (split (ImplicitBindings [infos.info])) + ; New.observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos) ] else continuation_tac infos -let terminate_letin (na, b, t, e) expr_info continuation_tac info g = - let sigma = project g in - let env = pf_env g in +let terminate_letin (na, b, t, e) expr_info continuation_tac info = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in + let env = Proofview.Goal.env g in let new_e = subst1 info.info e in let new_forbidden = let forbid = @@ -719,7 +694,7 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g = | Name id -> id :: info.forbidden_ids else info.forbidden_ids in - continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g + continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}) let pf_type c tac = let open Tacticals.New in @@ -729,9 +704,6 @@ let pf_type c tac = let evars, ty = Typing.type_of env sigma c in tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty)) -let pf_type c tac = - Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty))) - let pf_typel l tac = let rec aux tys l = match l with @@ -745,8 +717,8 @@ let pf_typel l tac = modified hypotheses are generalized in the process and should be introduced back later; the result is the pair of the tactic and the list of hypotheses that have been generalized and cleared. *) -let mkDestructEq not_on_hyp expr g = - let hyps = pf_hyps g in +let mkDestructEq not_on_hyp env sigma expr = + let hyps = EConstr.named_context env in let to_revert = Util.List.map_filter (fun decl -> @@ -754,38 +726,37 @@ let mkDestructEq not_on_hyp expr g = let id = get_id decl in if Id.List.mem id not_on_hyp - || not (Termops.dependent (project g) expr (get_type decl)) + || not (Termops.dependent sigma expr (get_type decl)) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in - let g, type_of_expr = tac_type_of g expr in + let sigma, type_of_expr = Typing.type_of env sigma expr in let new_hyps = mkApp (Lazy.force refl_equal, [|type_of_expr; expr|]) :: to_revert_constr in let tac = pf_typel new_hyps (fun _ -> - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "mkDestructEq") - [ Proofview.V82.of_tactic (generalize new_hyps) - ; (fun g2 -> + [ generalize new_hyps + ; Proofview.Goal.enter (fun g2 -> let changefun patvars env sigma = pattern_occs [(Locus.AllOccurrencesBut [1], expr)] - (pf_env g2) sigma (pf_concl g2) + (Proofview.Goal.env g2) sigma (Proofview.Goal.concl g2) in - Proofview.V82.of_tactic - (change_in_concl ~check:true None changefun) - g2) - ; Proofview.V82.of_tactic (simplest_case expr) ]) + change_in_concl ~check:true None changefun) + ; simplest_case expr ]) in - (g, tac, to_revert) + (sigma, tac, to_revert) -let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos - g = - let sigma = project g in - let env = pf_env g in +let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in + let env = Proofview.Goal.env g in let f_is_present = try check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) a; @@ -799,21 +770,21 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos ; is_main_branch = expr_info.is_main_branch ; is_final = expr_info.is_final } in - let g, destruct_tac, rev_to_thin_intro = - mkDestructEq [expr_info.rec_arg_id] a' g + let sigma, destruct_tac, rev_to_thin_intro = + mkDestructEq [expr_info.rec_arg_id] env sigma a' in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac + New.observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str ")" ++ spc () - ++ Printer.pr_leconstr_env (pf_env g) sigma a') + ++ Printer.pr_leconstr_env env sigma a') ( try tclTHENS destruct_tac (List.map_i (fun i e -> - observe_tac + New.observe_tac (fun _ _ -> str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) @@ -823,20 +794,21 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos | UserError (Some "Refiner.thensn_tac3", _) |UserError (Some "Refiner.tclFAIL_s", _) -> - observe_tac + New.observe_tac (fun _ _ -> str "is computable " ++ Printer.pr_leconstr_env env sigma new_info.info) (next_step continuation_tac { new_info with info = - Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info }) - ) - g + Reductionops.nf_betaiotazeta env sigma new_info.info }) + )) -let terminate_app_rec (f, args) expr_info continuation_tac _ g = - let sigma = project g in - let env = pf_env g in +let terminate_app_rec (f, args) expr_info continuation_tac _ = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in + let env = Proofview.Goal.env g in List.iter (check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids)) args; @@ -847,34 +819,30 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g = args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec") [ continuation_tac new_infos ; ( if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec1") - [ observe_tac + [ New.observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic - (split (ImplicitBindings [new_infos.info]))) - ; observe_tac + (split (ImplicitBindings [new_infos.info])) + ; New.observe_tac (fun _ _ -> str "destruct_bounds (3)") (destruct_bounds new_infos) ] - else tclIDTAC ) ] - g + else Proofview.tclUNIT () ) ] with Not_found -> - observe_tac + New.observe_tac (fun _ _ -> str "terminate_app_rec not found") (tclTHENS - (Proofview.V82.of_tactic - (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))) - [ observe_tclTHENLIST + (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args))) + [ New.observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2") - [ Proofview.V82.of_tactic - (intro_using_then rec_res_id + [ intro_using_then rec_res_id (* refreshed name gotten from onNthHypId *) - (fun _ -> Proofview.tclUNIT ())) - ; Proofview.V82.of_tactic intro + (fun _ -> Proofview.tclUNIT ()) + ; intro ; onNthHypId 1 (fun v_bound -> onNthHypId 2 (fun v -> let new_infos = @@ -885,42 +853,38 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g = ; args_assoc = (args, mkVar v) :: expr_info.args_assoc } in - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec3") [ continuation_tac new_infos ; ( if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec4") - [ observe_tac + [ New.observe_tac (fun _ _ -> str "first split") - (Proofview.V82.of_tactic - (split - (ImplicitBindings [new_infos.info]))) - ; observe_tac + (split (ImplicitBindings [new_infos.info])) + ; New.observe_tac (fun _ _ -> str "destruct_bounds (2)") (destruct_bounds new_infos) ] - else tclIDTAC ) ])) ] - ; observe_tac + else Proofview.tclUNIT () ) ])) ] + ; New.observe_tac (fun _ _ -> str "proving decreasing") (tclTHENS (* proof of args < formal args *) - (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) - [ observe_tac + (apply (Lazy.force expr_info.acc_inv)) + [ New.observe_tac (fun _ _ -> str "assumption") - (Proofview.V82.of_tactic assumption) - ; observe_tclTHENLIST + assumption + ; New.observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec5") [ tclTRY (list_rewrite true (List.map (fun e -> (mkVar e, true)) expr_info.eqs)) - ; Proofview.V82.of_tactic - @@ tclUSER expr_info.concl_tac true + ; tclUSER expr_info.concl_tac true (Some ( expr_info.ih :: expr_info.acc_id :: (fun (x, y) -> y) (List.split expr_info.values_and_bounds) )) - ] ]) ]) - g + ] ]) ])) let terminate_info = { message = "prove_terminate with term " @@ -936,19 +900,21 @@ let prove_terminate = travel terminate_info (* Equation proof *) let equation_case next_step case expr_info continuation_tac infos = - observe_tac + New.observe_tac (fun _ _ -> str "equation case") (terminate_case next_step case expr_info continuation_tac infos) -let rec prove_le g = - let sigma = project g in +let rec prove_le () = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in let x, z = - let _, args = decompose_app sigma (pf_concl g) in + let _, args = decompose_app sigma (Proofview.Goal.concl g) in (List.hd args, List.hd (List.tl args)) in tclFIRST - [ Proofview.V82.of_tactic assumption - ; Proofview.V82.of_tactic (apply (delayed_force le_n)) + [ assumption + ; apply (delayed_force le_n) ; begin try let matching_fun c = @@ -960,32 +926,30 @@ let rec prove_le g = | _ -> false in let h, t = - List.find (fun (_, t) -> matching_fun t) (pf_hyps_types g) + List.find (fun (_, t) -> matching_fun t) (Tacmach.New.pf_hyps_types g) in - let h = h.binder_name in let y = let _, args = decompose_app sigma t in List.hd (List.tl args) in - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "prove_le") - [ Proofview.V82.of_tactic - (apply (mkApp (le_trans (), [|x; y; z; mkVar h|]))) - ; observe_tac (fun _ _ -> str "prove_le (rec)") prove_le ] - with Not_found -> tclFAIL 0 (mt ()) - end ] - g + [ apply (mkApp (le_trans (), [|x; y; z; mkVar h|])) + ; New.observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le ()) ] + with Not_found -> Tacticals.New.tclFAIL 0 (mt ()) + end ]) let rec make_rewrite_list expr_info max = function - | [] -> tclIDTAC + | [] -> Proofview.tclUNIT () | (_, p, hp) :: l -> - observe_tac + let open Tacticals.New in + New.observe_tac (fun _ _ -> str "make_rewrite_list") (tclTHENS - (observe_tac + (New.observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p) - (fun g -> - let sigma = project g in + (Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in let t_eq = compute_renamed_type g hp in let k, def = let k_na, _, t = destProd sigma t_eq in @@ -994,32 +958,31 @@ let rec make_rewrite_list expr_info max = function ( Nameops.Name.get_id k_na.binder_name , Nameops.Name.get_id def_na.binder_name ) in - Proofview.V82.of_tactic - (general_rewrite_bindings false Locus.AllOccurrences true + general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true ( mkVar hp , ExplicitBindings [ CAst.make @@ (NamedHyp def, expr_info.f_constr) ; CAst.make @@ (NamedHyp k, f_S max) ] ) - false) - g)) + false))) [ make_rewrite_list expr_info max l - ; observe_tclTHENLIST + ; New.observe_tclTHENLIST (fun _ _ -> str "make_rewrite_list") [ (* x < S max proof *) - Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)) - ; observe_tac (fun _ _ -> str "prove_le(2)") prove_le ] ]) + apply (delayed_force le_lt_n_Sm) + ; New.observe_tac (fun _ _ -> str "prove_le(2)") (prove_le ()) ] ]) let make_rewrite expr_info l hp max = + let open Tacticals.New in tclTHENFIRST - (observe_tac + (New.observe_tac (fun _ _ -> str "make_rewrite") (make_rewrite_list expr_info max l)) - (observe_tac + (New.observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS - (fun g -> - let sigma = project g in + (Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in let t_eq = compute_renamed_type g hp in let k, def = let k_na, _, t = destProd sigma t_eq in @@ -1028,102 +991,101 @@ let make_rewrite expr_info l hp max = ( Nameops.Name.get_id k_na.binder_name , Nameops.Name.get_id def_na.binder_name ) in - observe_tac + New.observe_tac (fun _ _ -> str "general_rewrite_bindings") - (Proofview.V82.of_tactic - (general_rewrite_bindings false Locus.AllOccurrences true + (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true ( mkVar hp , ExplicitBindings [ CAst.make @@ (NamedHyp def, expr_info.f_constr) ; CAst.make @@ (NamedHyp k, f_S (f_S max)) ] ) - false)) - g) - [ observe_tac + false))) + [ New.observe_tac (fun _ _ -> str "make_rewrite finalize") ((* tclORELSE( h_reflexivity) *) - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "make_rewrite") - [ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl) - ; observe_tac + [ simpl_iter Locusops.onConcl + ; New.observe_tac (fun _ _ -> str "unfold functional") - (Proofview.V82.of_tactic - (unfold_in_concl + (unfold_in_concl [ ( Locus.OnlyOccurrences [1] - , evaluable_of_global_reference expr_info.func ) ])) + , evaluable_of_global_reference expr_info.func ) ]) ; list_rewrite true (List.map (fun e -> (mkVar e, true)) expr_info.eqs) - ; observe_tac + ; New.observe_tac (fun _ _ -> str "h_reflexivity") - (Proofview.V82.of_tactic intros_reflexivity) ]) - ; observe_tclTHENLIST + intros_reflexivity ]) + ; New.observe_tclTHENLIST (fun _ _ -> str "make_rewrite1") [ (* x < S (S max) proof *) - Proofview.V82.of_tactic - (apply (EConstr.of_constr (delayed_force le_lt_SS))) - ; observe_tac (fun _ _ -> str "prove_le (3)") prove_le ] ])) + apply (EConstr.of_constr (delayed_force le_lt_SS)) + ; New.observe_tac (fun _ _ -> str "prove_le (3)") (prove_le ()) ] ])) let rec compute_max rew_tac max l = match l with | [] -> rew_tac max | (_, p, _) :: l -> - observe_tclTHENLIST + let open Tacticals.New in + New.observe_tclTHENLIST (fun _ _ -> str "compute_max") - [ Proofview.V82.of_tactic - (simplest_elim (mkApp (delayed_force max_constr, [|max; mkVar p|]))) - ; tclDO 3 (Proofview.V82.of_tactic intro) + [ simplest_elim (mkApp (delayed_force max_constr, [|max; mkVar p|])) + ; tclDO 3 intro ; onNLastHypsId 3 (fun lids -> match lids with | [hle2; hle1; pmax] -> compute_max rew_tac (mkVar pmax) l | _ -> assert false) ] let rec destruct_hex expr_info acc l = + let open Tacticals.New in match l with | [] -> ( match List.rev acc with - | [] -> tclIDTAC + | [] -> Proofview.tclUNIT () | (_, p, hp) :: tl -> - observe_tac + New.observe_tac (fun _ _ -> str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) ) | (v, hex) :: l -> - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "destruct_hex") - [ Proofview.V82.of_tactic (simplest_case (mkVar hex)) - ; Proofview.V82.of_tactic (clear [hex]) - ; tclDO 2 (Proofview.V82.of_tactic intro) + [ simplest_case (mkVar hex) + ; clear [hex] + ; tclDO 2 intro ; onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> - observe_tac + New.observe_tac (fun _ _ -> str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) (destruct_hex expr_info ((v, p, hp) :: acc) l))) ] let rec intros_values_eq expr_info acc = + let open Tacticals.New in tclORELSE - (observe_tclTHENLIST + (New.observe_tclTHENLIST (fun _ _ -> str "intros_values_eq") - [ tclDO 2 (Proofview.V82.of_tactic intro) + [ tclDO 2 intro ; onNthHypId 1 (fun hex -> onNthHypId 2 (fun v -> intros_values_eq expr_info ((v, hex) :: acc))) ]) (tclCOMPLETE (destruct_hex expr_info [] acc)) let equation_others _ expr_info continuation_tac infos = + let open Tacticals.New in if expr_info.is_final && expr_info.is_main_branch then - observe_tac + New.observe_tac (fun env sigma -> str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac + (New.observe_tac (fun env sigma -> str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []))) else - observe_tac + New.observe_tac (fun env sigma -> str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) @@ -1131,13 +1093,14 @@ let equation_others _ expr_info continuation_tac infos = let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tac + New.observe_tac (fun _ _ -> str "intros_values_eq equation_app") (intros_values_eq expr_info []) else continuation_tac infos -let equation_app_rec (f, args) expr_info continuation_tac info g = - let sigma = project g in +let equation_app_rec (f, args) expr_info continuation_tac info = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in try let v = List.assoc_f @@ -1145,33 +1108,29 @@ let equation_app_rec (f, args) expr_info continuation_tac info g = args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g + New.observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) with Not_found -> if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "equation_app_rec") - [ Proofview.V82.of_tactic - (simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))) + [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args)) ; continuation_tac { expr_info with args_assoc = (args, delayed_force coq_O) :: expr_info.args_assoc } - ; observe_tac + ; New.observe_tac (fun _ _ -> str "app_rec intros_values_eq") (intros_values_eq expr_info []) ] - g else - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "equation_app_rec1") - [ Proofview.V82.of_tactic - (simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))) - ; observe_tac + [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args)) + ; New.observe_tac (fun _ _ -> str "app_rec not_found") (continuation_tac { expr_info with args_assoc = - (args, delayed_force coq_O) :: expr_info.args_assoc }) ] - g + (args, delayed_force coq_O) :: expr_info.args_assoc }) ]) let equation_info = { message = "prove_equation with term " @@ -1231,8 +1190,9 @@ let compute_terminate_type nb_args func = compose_prod rev_args value let termination_proof_header is_mes input_type ids args_id relation rec_arg_num - rec_arg_id tac wf_tac : tactic = - fun g -> + rec_arg_id tac wf_tac : unit Proofview.tactic = + let open Tacticals.New in + Proofview.Goal.enter (fun g -> let nargs = List.length args_id in let pre_rec_args = List.rev_map mkVar (fst (List.chop (rec_arg_num - 1) args_id)) @@ -1253,51 +1213,46 @@ let termination_proof_header is_mes input_type ids args_id relation rec_arg_num in tclTHEN (h_intros args_id) (tclTHENS - (observe_tac + (New.observe_tac (fun _ _ -> str "first assert") - (Proofview.V82.of_tactic - (assert_before (Name wf_rec_arg) + (assert_before (Name wf_rec_arg) (mkApp ( delayed_force acc_rel - , [|input_type; relation; mkVar rec_arg_id|] ))))) + , [|input_type; relation; mkVar rec_arg_id|] )))) [ (* accesibility proof *) tclTHENS - (observe_tac + (New.observe_tac (fun _ _ -> str "second assert") - (Proofview.V82.of_tactic - (assert_before (Name wf_thm) + (assert_before (Name wf_thm) (mkApp - (delayed_force well_founded, [|input_type; relation|]))))) + (delayed_force well_founded, [|input_type; relation|])))) [ (* interactive proof that the relation is well_founded *) - observe_tac + New.observe_tac (fun _ _ -> str "wf_tac") (wf_tac is_mes (Some args_id)) ; (* this gives the accessibility argument *) - observe_tac + New.observe_tac (fun _ _ -> str "apply wf_thm") - (Proofview.V82.of_tactic - (Simple.apply (mkApp (mkVar wf_thm, [|mkVar rec_arg_id|])))) + (Simple.apply (mkApp (mkVar wf_thm, [|mkVar rec_arg_id|]))) ] ; (* rest of the proof *) - observe_tclTHENLIST + New.observe_tclTHENLIST (fun _ _ -> str "rest of proof") - [ observe_tac + [ New.observe_tac (fun _ _ -> str "generalize") (onNLastHypsId (nargs + 1) (tclMAP (fun id -> tclTHEN - (Proofview.V82.of_tactic - (Tactics.generalize [mkVar id])) - (Proofview.V82.of_tactic (clear [id]))))) - ; observe_tac + (Tactics.generalize [mkVar id]) + (clear [id])))) + ; New.observe_tac (fun _ _ -> str "fix") - (Proofview.V82.of_tactic (fix hrec (nargs + 1))) + (fix hrec (nargs + 1)) ; h_intros args_id - ; Proofview.V82.of_tactic (Simple.intro wf_rec_arg) - ; observe_tac + ; Simple.intro wf_rec_arg + ; New.observe_tac (fun _ _ -> str "tac") - (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ]) - g + (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ])) let rec instantiate_lambda sigma t l = match l with @@ -1307,10 +1262,11 @@ let rec instantiate_lambda sigma t l = instantiate_lambda sigma (subst1 a body) l let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num : - tactic = - fun g -> - let sigma = project g in - let ids = Termops.ids_of_named_context (pf_hyps g) in + unit Proofview.tactic = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in + let hyps = Proofview.Goal.hyps g in + let ids = Termops.ids_of_named_context hyps in let func_body = def_of_const (constr_of_monomorphic_global func) in let func_body = EConstr.of_constr func_body in let f_name, _, body1 = destLambda sigma func_body in @@ -1337,9 +1293,9 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num : in termination_proof_header is_mes input_type ids n_ids relation rec_arg_num rec_arg_id - (fun rec_arg_id hrec acc_id acc_inv g -> + (fun rec_arg_id hrec acc_id acc_inv -> (prove_terminate - (fun infos -> tclIDTAC) + (fun infos -> Proofview.tclUNIT ()) { is_main_branch = true ; (* we are on the main branche (i.e. still on a match ... with .... end *) is_final = true @@ -1359,10 +1315,8 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num : ; values_and_bounds = [] ; eqs = [] ; forbidden_ids = [] - ; args_assoc = [] }) - g) - (fun b ids -> Proofview.V82.of_tactic (tclUSER_if_not_mes concl_tac b ids)) - g + ; args_assoc = [] })) + (fun b ids -> tclUSER_if_not_mes concl_tac b ids)) let get_current_subgoals_types pstate = let p = Declare.Proof.get pstate in @@ -1397,9 +1351,8 @@ let build_and_l sigma l = let c, tac, nb = f pl in ( mk_and p1 c , tclTHENS - (Proofview.V82.of_tactic (apply - (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))) + (EConstr.of_constr (constr_of_monomorphic_global conj_constr))) [tclIDTAC; tac] , nb + 1 ) in @@ -1521,18 +1474,16 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name let lemma = Declare.Proof.start ~cinfo ~info sigma in let lemma = if Indfun_common.is_strict_tcc () then - fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma + fst @@ Declare.Proof.by tclIDTAC lemma else fst @@ Declare.Proof.by - (Proofview.V82.tactic (fun g -> - tclTHEN decompose_and_tac + (tclTHEN decompose_and_tac (tclORELSE (tclFIRST (List.map (fun c -> - Proofview.V82.of_tactic - (Tacticals.New.tclTHENLIST + Tacticals.New.tclTHENLIST [ intros ; Simple.apply (fst @@ -1540,10 +1491,9 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name Evd.empty c)) (*FIXME*) ; Tacticals.New.tclCOMPLETE Auto.default_auto - ])) + ]) using_lemmas)) - tclIDTAC) - g)) + tclIDTAC)) lemma in if Declare.Proof.get_open_goals lemma = 0 then (defined lemma; None) @@ -1568,11 +1518,10 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes in fst @@ Declare.Proof.by - (Proofview.V82.tactic - (observe_tac + (New.observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref input_type - relation rec_arg_num))) + relation rec_arg_num)) lemma in let lemma = @@ -1591,31 +1540,29 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes if interactive_proof then Some lemma else (defined lemma; None) let start_equation (f : GlobRef.t) (term_f : GlobRef.t) - (cont_tactic : Id.t list -> tactic) g = - let sigma = project g in - let ids = pf_ids_of_hyps g in + (cont_tactic : Id.t list -> unit Proofview.tactic) = + Proofview.Goal.enter (fun g -> + let sigma = Proofview.Goal.sigma g in + let ids = Tacmach.New.pf_ids_of_hyps g in let terminate_constr = constr_of_monomorphic_global term_f in let terminate_constr = EConstr.of_constr terminate_constr in let nargs = - nb_prod (project g) + nb_prod sigma (EConstr.of_constr (type_of_const sigma terminate_constr)) in let x = n_x_id ids nargs in - observe_tac + New.observe_tac (fun _ _ -> str "start_equation") - (observe_tclTHENLIST + (New.observe_tclTHENLIST (fun _ _ -> str "start_equation") [ h_intros x - ; Proofview.V82.of_tactic - (unfold_in_concl - [(Locus.AllOccurrences, evaluable_of_global_reference f)]) - ; observe_tac + ; unfold_in_concl + [(Locus.AllOccurrences, evaluable_of_global_reference f)] + ; New.observe_tac (fun _ _ -> str "simplest_case") - (Proofview.V82.of_tactic - (simplest_case - (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))) - ; observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x) ]) - g + (simplest_case + (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))) + ; New.observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x) ])) let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = @@ -1638,10 +1585,9 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let lemma = fst @@ Declare.Proof.by - (Proofview.V82.tactic - (start_equation f_ref terminate_ref (fun x -> + (start_equation f_ref terminate_ref (fun x -> prove_eq - (fun _ -> tclIDTAC) + (fun _ -> Proofview.tclUNIT ()) { nb_arg ; f_terminate = EConstr.of_constr @@ -1666,7 +1612,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref ; f_id = Id.of_string "______" ; rec_arg_id = Id.of_string "______" ; is_mes = false - ; ih = Id.of_string "______" }))) + ; ih = Id.of_string "______" })) lemma in let _ = |