diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/Bintree.v | 3 | ||||
| -rw-r--r-- | plugins/rtauto/Rtauto.v | 21 | ||||
| -rw-r--r-- | plugins/rtauto/g_rtauto.mlg (renamed from plugins/rtauto/g_rtauto.ml4) | 5 | ||||
| -rw-r--r-- | plugins/rtauto/plugin_base.dune | 5 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 2 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 80 |
6 files changed, 69 insertions, 47 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 600e8993b4..99c02995fb 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -319,6 +319,9 @@ Arguments F_empty [A]. Arguments F_push [A] a S _. Arguments In [A] x S F. +Register empty as plugins.rtauto.empty. +Register push as plugins.rtauto.push. + Section Map. Variables A B:Set. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 06cdf76b4e..f027a4a46e 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -387,3 +387,24 @@ exact (Reflect (empty \ A \ B \ C) Qed. Print toto. *) + +Register Reflect as plugins.rtauto.Reflect. + +Register Atom as plugins.rtauto.Atom. +Register Arrow as plugins.rtauto.Arrow. +Register Bot as plugins.rtauto.Bot. +Register Conjunct as plugins.rtauto.Conjunct. +Register Disjunct as plugins.rtauto.Disjunct. + +Register Ax as plugins.rtauto.Ax. +Register I_Arrow as plugins.rtauto.I_Arrow. +Register E_Arrow as plugins.rtauto.E_Arrow. +Register D_Arrow as plugins.rtauto.D_Arrow. +Register E_False as plugins.rtauto.E_False. +Register I_And as plugins.rtauto.I_And. +Register E_And as plugins.rtauto.E_And. +Register D_And as plugins.rtauto.D_And. +Register I_Or_l as plugins.rtauto.I_Or_l. +Register I_Or_r as plugins.rtauto.I_Or_r. +Register E_Or as plugins.rtauto.E_Or. +Register D_Or as plugins.rtauto.D_Or. diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.mlg index aa67576348..9c9fdcfa2f 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.mlg @@ -8,12 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ open Ltac_plugin +} + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto - [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] +| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } END diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/plugin_base.dune new file mode 100644 index 0000000000..233845ae0f --- /dev/null +++ b/plugins/rtauto/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name rtauto_plugin) + (public_name coq.plugins.rtauto) + (synopsis "Coq's rtauto plugin") + (libraries coq.plugins.ltac)) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3de5923968..aab1e47555 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -54,7 +54,7 @@ let opt_pruning= optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} -let _ = declare_bool_option opt_pruning +let () = declare_bool_option opt_pruning type form= Atom of int diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 946b6dff42..e66fa10d5b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,49 +26,39 @@ let step_count = ref 0 let node_count = ref 0 -let logic_constant s = Universes.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s +let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type")) -let li_False = lazy (destInd (logic_constant "False")) -let li_and = lazy (destInd (logic_constant "and")) -let li_or = lazy (destInd (logic_constant "or")) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) -let pos_constant s = Universes.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s +let l_xI = gen_constant "num.pos.xI" +let l_xO = gen_constant "num.pos.xO" +let l_xH = gen_constant "num.pos.xH" -let l_xI = lazy (pos_constant "xI") -let l_xO = lazy (pos_constant "xO") -let l_xH = lazy (pos_constant "xH") +let l_empty = gen_constant "plugins.rtauto.empty" +let l_push = gen_constant "plugins.rtauto.push" -let store_constant s = Universes.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s +let l_Reflect = gen_constant "plugins.rtauto.Reflect" -let l_empty = lazy (store_constant "empty") -let l_push = lazy (store_constant "push") +let l_Atom = gen_constant "plugins.rtauto.Atom" +let l_Arrow = gen_constant "plugins.rtauto.Arrow" +let l_Bot = gen_constant "plugins.rtauto.Bot" +let l_Conjunct = gen_constant "plugins.rtauto.Conjunct" +let l_Disjunct = gen_constant "plugins.rtauto.Disjunct" -let constant s = Universes.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s - -let l_Reflect = lazy (constant "Reflect") - -let l_Atom = lazy (constant "Atom") -let l_Arrow = lazy (constant "Arrow") -let l_Bot = lazy (constant "Bot") -let l_Conjunct = lazy (constant "Conjunct") -let l_Disjunct = lazy (constant "Disjunct") - -let l_Ax = lazy (constant "Ax") -let l_I_Arrow = lazy (constant "I_Arrow") -let l_E_Arrow = lazy (constant "E_Arrow") -let l_D_Arrow = lazy (constant "D_Arrow") -let l_E_False = lazy (constant "E_False") -let l_I_And = lazy (constant "I_And") -let l_E_And = lazy (constant "E_And") -let l_D_And = lazy (constant "D_And") -let l_I_Or_l = lazy (constant "I_Or_l") -let l_I_Or_r = lazy (constant "I_Or_r") -let l_E_Or = lazy (constant "E_Or") -let l_D_Or = lazy (constant "D_Or") +let l_Ax = gen_constant "plugins.rtauto.Ax" +let l_I_Arrow = gen_constant "plugins.rtauto.I_Arrow" +let l_E_Arrow = gen_constant "plugins.rtauto.E_Arrow" +let l_D_Arrow = gen_constant "plugins.rtauto.D_Arrow" +let l_E_False = gen_constant "plugins.rtauto.E_False" +let l_I_And = gen_constant "plugins.rtauto.I_And" +let l_E_And = gen_constant "plugins.rtauto.E_And" +let l_D_And = gen_constant "plugins.rtauto.D_And" +let l_I_Or_l = gen_constant "plugins.rtauto.I_Or_l" +let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r" +let l_E_Or = gen_constant "plugins.rtauto.E_Or" +let l_D_Or = gen_constant "plugins.rtauto.D_Or" let special_whd gl c = @@ -246,7 +236,7 @@ let opt_verbose= optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} -let _ = declare_bool_option opt_verbose +let () = declare_bool_option opt_verbose let check = ref false @@ -257,7 +247,7 @@ let opt_check= optread=(fun () -> !check); optwrite=(fun b -> check:=b)} -let _ = declare_bool_option opt_check +let () = declare_bool_option opt_check open Pp @@ -265,7 +255,7 @@ let rtauto_tac gls= Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; let gamma={next=1;env=[]} in let gl=pf_concl gls in - let _= + let () = if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in @@ -277,7 +267,7 @@ let rtauto_tac gls= | Tactic_debug.DebugOn 0 -> Search.debug_depth_first | _ -> Search.depth_first in - let _ = + let () = begin reset_info (); if !verbose then @@ -289,7 +279,7 @@ let rtauto_tac gls= with Not_found -> user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); @@ -297,7 +287,7 @@ let rtauto_tac gls= Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in - let _ = step_count := 0; node_count := 0 in + let () = step_count := 0; node_count := 0 in let main = mkApp (force node_count l_Reflect, [|build_env gamma; build_form formula; @@ -305,7 +295,7 @@ let rtauto_tac gls= let term= applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in - let _ = if !verbose then + let () = if !verbose then begin Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ @@ -324,7 +314,7 @@ let rtauto_tac gls= else Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in - let _ = + let () = if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then Feedback.msg_info (str "Internal tactic executed in " ++ |