diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 34 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 14 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg (renamed from plugins/funind/g_indfun.ml4) | 122 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 14 |
7 files changed, 116 insertions, 82 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b12364d04a..ad1114b733 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in + let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -638,11 +638,11 @@ let my_orelse tac1 tac2 g = (* observe (str "using snd tac since : " ++ CErrors.print e); *) tac2 g -let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = +let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let args = Array.of_list (List.map mkVar args_id) in - let instanciate_one_hyp hid = + let instantiate_one_hyp hid = my_orelse - ( (* we instanciate the hyp if possible *) + ( (* we instantiate the hyp if possible *) fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in @@ -678,7 +678,7 @@ let instanciate_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 instanciate_one_hyp hyps; + tclMAP instantiate_one_hyp hyps; (fun g -> let all_g_hyps_id = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty @@ -722,11 +722,11 @@ let build_proof tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); (fun g' -> let g'_nb_prod = nb_prod (project g') (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + let nb_instantiate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case ptes_infos - nb_instanciate_partial + nb_instantiate_partial (build_proof do_finalize) t dyn_infos) @@ -760,7 +760,7 @@ let build_proof nb_rec_hyps = List.length new_hyps } in -(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' +(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' (* build_proof do_finalize new_infos g' *) ) g | _ -> @@ -1120,7 +1120,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in (full_params, (* real params *) princ_params, (* the params of the principle which are not params of the function *) - substl (* function instanciated with real params *) + substl (* function instantiated with real params *) (List.map var_of_decl full_params) f_body ) @@ -1130,7 +1130,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let f_body = compose_lam f_ctxt_other f_body in (princ_info.params, (* real params *) [],(* all params are full params *) - substl (* function instanciated with real params *) + substl (* function instantiated with real params *) (List.map var_of_decl princ_info.params) f_body ) @@ -1321,7 +1321,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) (* ); *) - (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac + (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] @@ -1371,7 +1371,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam do_prove dyn_infos in - instanciate_hyps_with_args prove_tac + instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id) ] @@ -1605,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) @@ -1728,8 +1728,8 @@ let prove_principle_for_gen ptes_info (body_info rec_hyps) in - (* observe_tac "instanciate_hyps_with_args" *) - (instanciate_hyps_with_args + (* observe_tac "instantiate_hyps_with_args" *) + (instantiate_hyps_with_args make_proof (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9ca91d62da..d57b931785 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -676,11 +676,15 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) + try (let open GlobRef in + match Smartlocate.global_with_alias f with + | ConstRef c -> c + | IndRef _ | ConstructRef _ | VarRef _ -> assert false) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_qualid f) in - let first_fun,u = destConst funs in + let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in + let first_fun = funs in let funs_mp = Constant.modpath first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in let this_block_funs_indexes = get_funs_constant funs_mp first_fun in @@ -688,7 +692,7 @@ let build_case_scheme fa = let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes + List.assoc_f Constant.equal funs this_block_funs_indexes in let (ind, sf) = let ind = first_fun_kn,funs_indexes in @@ -700,7 +704,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - UnivGen.new_sort_in_family x + fst @@ UnivGen.fresh_sort_in_family x ) fa in @@ -718,7 +722,7 @@ let build_case_scheme fa = (Some princ_name) this_block_funs 0 - (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|]) + (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|]) in () diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.mlg index a2d31780dd..857215751a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.mlg @@ -7,23 +7,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) + +{ + open Ltac_plugin open Util open Pp open Constrexpr open Indfun_common open Indfun -open Genarg open Stdarg open Tacarg open Tactypes -open Pcoq open Pcoq.Prim open Pcoq.Constr open Pltac +} + DECLARE PLUGIN "recdef_plugin" +{ + let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () @@ -44,26 +49,27 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = let (_, b) = b env evd in spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) +} ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option - PRINTED BY pr_fun_ind_using_typed - RAW_TYPED AS constr_with_bindings_opt - RAW_PRINTED BY pr_fun_ind_using - GLOB_TYPED AS constr_with_bindings_opt - GLOB_PRINTED BY pr_fun_ind_using -| [ "using" constr_with_bindings(c) ] -> [ Some c ] -| [ ] -> [ None ] + PRINTED BY { pr_fun_ind_using_typed } + RAW_PRINTED BY { pr_fun_ind_using } + GLOB_PRINTED BY { pr_fun_ind_using } +| [ "using" constr_with_bindings(c) ] -> { Some c } +| [ ] -> { None } END TACTIC EXTEND newfuninv - [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> - [ +| [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> + { Proofview.V82.tactic (Invfun.invfun hyp fname) - ] + } END +{ + let pr_intro_as_pat _prc _ _ pat = match pat with | Some pat -> @@ -75,56 +81,70 @@ let out_disjunctive = CAst.map (function | IntroAction (IntroOrAndPattern l) -> l | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")) -ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat -| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] -| [] ->[ None ] +} + +ARGUMENT EXTEND with_names TYPED AS intropattern option PRINTED BY { pr_intro_as_pat } +| [ "as" simple_intropattern(ipat) ] -> { Some ipat } +| [] -> { None } END +{ + let functional_induction b c x pat = Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat)) +} TACTIC EXTEND newfunind - ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ +| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + { let c = match cl with | [] -> assert false | [c] -> c | c::cl -> EConstr.applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] + Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl } END (***** debug only ***) TACTIC EXTEND snewfunind - ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ +| ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + { let c = match cl with | [] -> assert false | [c] -> c | c::cl -> EConstr.applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] + Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl } END +{ let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc +} + ARGUMENT EXTEND constr_comma_sequence' - TYPED AS constr_list - PRINTED BY pr_constr_comma_sequence -| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ] -| [ constr(c) ] -> [ [c] ] + TYPED AS constr list + PRINTED BY { pr_constr_comma_sequence } +| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l } +| [ constr(c) ] -> { [c] } END +{ + let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc +} + ARGUMENT EXTEND auto_using' - TYPED AS constr_list - PRINTED BY pr_auto_using -| [ "using" constr_comma_sequence'(l) ] -> [ l ] -| [ ] -> [ [] ] + TYPED AS constr list + PRINTED BY { pr_auto_using } +| [ "using" constr_comma_sequence'(l) ] -> { l } +| [ ] -> { [] } END +{ + module Gram = Pcoq.Gram module Vernac = Pvernac.Vernac_ module Tactic = Pltac @@ -137,23 +157,29 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar let function_rec_definition_loc = Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]] + [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]] ; END +{ + let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer +} + (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function - ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] - => [ let hard = List.exists (function +| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] + => { let hard = List.exists (function | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match @@ -162,20 +188,25 @@ VERNAC COMMAND EXTEND Function with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) - | x -> x ] - -> [ do_generate_principle false (List.map snd recsl) ] + | x -> x } + -> { do_generate_principle false (List.map snd recsl) } END +{ + let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ Termops.pr_sort_family s +} + VERNAC ARGUMENT EXTEND fun_scheme_arg -PRINTED BY pr_fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ] +PRINTED BY { pr_fun_scheme_arg } +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> { (princ_name,fun_name,s) } END +{ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in @@ -190,12 +221,13 @@ let warning_error names e = warn_cannot_define_principle (names,error) | _ -> raise e +} VERNAC COMMAND EXTEND NewFunctionalScheme - ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] - => [ Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater ] +| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] + => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater } -> - [ + { begin try Functional_principles_types.build_scheme fas @@ -223,17 +255,17 @@ VERNAC COMMAND EXTEND NewFunctionalScheme warning_error names e end - ] + } END (***** debug only ***) VERNAC COMMAND EXTEND NewFunctionalCase - ["Functional" "Case" fun_scheme_arg(fas) ] - => [ Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater ] - -> [ Functional_principles_types.build_case_scheme fas ] +| ["Functional" "Case" fun_scheme_arg(fas) ] + => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater } + -> { Functional_principles_types.build_case_scheme fas } END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ] +| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 03a64988e4..a385a61ae0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -116,7 +116,7 @@ let def_of_const t = [@@@ocaml.warning "-3"] let coq_constant s = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -441,7 +441,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) @@ -449,7 +449,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") [@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" [@@@ocaml.warning "+3"] diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7e52ee224f..1b4c1248a5 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - unit Lemmas.declaration_hook CEphemeron.key -> unit + Lemmas.declaration_hook CEphemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..b0842c3721 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 89dfb58017..f9df3aed45 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -24,6 +24,7 @@ open Globnames open Nameops open CErrors open Util +open UnivGen open Tacticals open Tacmach open Tactics @@ -50,7 +51,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "RecursiveDefinition" m s let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] @@ -62,7 +63,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -96,10 +97,7 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constr_of_global x = - fst (Global.constr_of_global_in_context (Global.env ()) x) - -let constant sl s = constr_of_global (find_reference sl s) +let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn @@ -1243,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in @@ -1320,7 +1318,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | None -> try add_suffix current_proof_name "_subproof" with e when CErrors.noncritical e -> - anomaly (Pp.str "open_new_goal with an unamed theorem.") + anomaly (Pp.str "open_new_goal with an unnamed theorem.") in let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then |