From 6b5b4db599333546334bcdbd852be72ddb39d9dc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 11 Oct 2018 18:13:12 +0200 Subject: Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro. Those optional arguments did not really make sense. It was pretty clear from our code base, as all instances where triplicating the same type for TYPED, RAW_TYPED and GLOB_TYPED. --- plugins/firstorder/g_ground.ml4 | 2 -- 1 file changed, 2 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index fdeef5f0ac..ff106404c8 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -138,9 +138,7 @@ let warn_deprecated_syntax = ARGUMENT EXTEND firstorder_using TYPED AS reference_list PRINTED BY pr_firstorder_using_typed - RAW_TYPED AS reference_list RAW_PRINTED BY pr_firstorder_using_raw - GLOB_TYPED AS reference_list GLOB_PRINTED BY pr_firstorder_using_glob | [ "using" reference(a) ] -> [ [a] ] | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] -- cgit v1.2.3 From dba567555fed9c88887b463a975c3d7e0852ebd3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 11 Oct 2018 19:17:47 +0200 Subject: Plug ARGUMENT EXTEND into the argument extension API. --- plugins/firstorder/g_ground.ml4 | 1 - 1 file changed, 1 deletion(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index ff106404c8..db753fc672 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -123,7 +123,6 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) -open Genarg open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid -- cgit v1.2.3 From 4da233a9685cd193a84def037ec18a27c9225dce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 12 Oct 2018 09:22:56 +0200 Subject: Port remaining EXTEND ml4 files to coqpp. Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code. --- plugins/firstorder/g_ground.ml4 | 164 ------------------------------------- plugins/firstorder/g_ground.mlg | 173 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 173 insertions(+), 164 deletions(-) delete mode 100644 plugins/firstorder/g_ground.ml4 create mode 100644 plugins/firstorder/g_ground.mlg (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 deleted file mode 100644 index db753fc672..0000000000 --- a/plugins/firstorder/g_ground.ml4 +++ /dev/null @@ -1,164 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Some !ground_depth); - optwrite= - (function - None->ground_depth:=3 - | Some i->ground_depth:=(max i 0))} - in - declare_int_option gdopt - - -let _= - let congruence_depth=ref 100 in - let gdopt= - { optdepr=true; (* noop *) - optname="Congruence Depth"; - optkey=["Congruence";"Depth"]; - optread=(fun ()->Some !congruence_depth); - optwrite= - (function - None->congruence_depth:=0 - | Some i->congruence_depth:=(max i 0))} - in - declare_int_option gdopt - -let default_intuition_tac = - let tac _ _ = Auto.h_auto None [] None in - let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in - let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in - Tacenv.register_ml_tactic name [| tac |]; - Tacexpr.TacML (Loc.tag (entry, [])) - -let (set_default_solver, default_solver, print_default_solver) = - Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" - -VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF -| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ - fun ~atts ~st -> let open Vernacinterp in - set_default_solver - (Locality.make_section_locality atts.locality) - (Tacintern.glob_tactic t); - st - ] -END - -VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY -| [ "Print" "Firstorder" "Solver" ] -> [ - Feedback.msg_info - (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] -END - -let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") - -let gen_ground_tac flag taco ids bases = - let backup= !qflag in - Proofview.tclOR begin - Proofview.Goal.enter begin fun gl -> - qflag:=flag; - let solver= - match taco with - Some tac-> tac - | None-> snd (default_solver ()) in - let startseq k = - Proofview.Goal.enter begin fun gl -> - let seq=empty_seq !ground_depth in - let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in - let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in - tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq) - end - in - let result=ground_tac solver startseq in - qflag := backup; - result - end - end - (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e) - -(* special for compatibility with Intuition - -let constant str = Coqlib.get_constr str - -let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "core.not.type")); - [],EvalConstRef (destConst (constant "core.iff.type"))] - -let normalize_evaluables= - onAllHypsAndConcl - (function - None->unfold_in_concl (Lazy.force defined_connectives) - | Some id-> - unfold_in_hyp (Lazy.force defined_connectives) - (Tacexpr.InHypType id)) *) - -open Ppconstr -open Printer -let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid -let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) -let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global - -let warn_deprecated_syntax = - CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" - (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator") - - -ARGUMENT EXTEND firstorder_using - TYPED AS reference_list - PRINTED BY pr_firstorder_using_typed - RAW_PRINTED BY pr_firstorder_using_raw - GLOB_PRINTED BY pr_firstorder_using_glob -| [ "using" reference(a) ] -> [ [a] ] -| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] -| [ "using" reference(a) reference(b) reference_list(l) ] -> [ - warn_deprecated_syntax (); - a::b::l - ] -| [ ] -> [ [] ] -END - -TACTIC EXTEND firstorder - [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ] -| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ] -| [ "firstorder" tactic_opt(t) firstorder_using(l) - "with" ne_preident_list(l') ] -> - [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ] -END - -TACTIC EXTEND gintuition - [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ] -END diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg new file mode 100644 index 0000000000..c41687e721 --- /dev/null +++ b/plugins/firstorder/g_ground.mlg @@ -0,0 +1,173 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Some !ground_depth); + optwrite= + (function + None->ground_depth:=3 + | Some i->ground_depth:=(max i 0))} + in + declare_int_option gdopt + + +let _= + let congruence_depth=ref 100 in + let gdopt= + { optdepr=true; (* noop *) + optname="Congruence Depth"; + optkey=["Congruence";"Depth"]; + optread=(fun ()->Some !congruence_depth); + optwrite= + (function + None->congruence_depth:=0 + | Some i->congruence_depth:=(max i 0))} + in + declare_int_option gdopt + +let default_intuition_tac = + let tac _ _ = Auto.h_auto None [] None in + let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in + let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in + Tacenv.register_ml_tactic name [| tac |]; + Tacexpr.TacML (Loc.tag (entry, [])) + +let (set_default_solver, default_solver, print_default_solver) = + Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" + +} + +VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF +| [ "Set" "Firstorder" "Solver" tactic(t) ] -> { + let open Vernacinterp in + set_default_solver + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t) + } +END + +VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY +| [ "Print" "Firstorder" "Solver" ] -> { + Feedback.msg_info + (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) } +END + +{ + +let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") + +let gen_ground_tac flag taco ids bases = + let backup= !qflag in + Proofview.tclOR begin + Proofview.Goal.enter begin fun gl -> + qflag:=flag; + let solver= + match taco with + Some tac-> tac + | None-> snd (default_solver ()) in + let startseq k = + Proofview.Goal.enter begin fun gl -> + let seq=empty_seq !ground_depth in + let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in + let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq) + end + in + let result=ground_tac solver startseq in + qflag := backup; + result + end + end + (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e) + +(* special for compatibility with Intuition + +let constant str = Coqlib.get_constr str + +let defined_connectives=lazy + [[],EvalConstRef (destConst (constant "core.not.type")); + [],EvalConstRef (destConst (constant "core.iff.type"))] + +let normalize_evaluables= + onAllHypsAndConcl + (function + None->unfold_in_concl (Lazy.force defined_connectives) + | Some id-> + unfold_in_hyp (Lazy.force defined_connectives) + (Tacexpr.InHypType id)) *) + +open Ppconstr +open Printer +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid +let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) +let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global + +let warn_deprecated_syntax = + CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" + (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator") + +} + +ARGUMENT EXTEND firstorder_using + TYPED AS reference list + PRINTED BY { pr_firstorder_using_typed } + RAW_PRINTED BY { pr_firstorder_using_raw } + GLOB_PRINTED BY { pr_firstorder_using_glob } +| [ "using" reference(a) ] -> { [a] } +| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l } +| [ "using" reference(a) reference(b) reference_list(l) ] -> { + warn_deprecated_syntax (); + a::b::l + } +| [ ] -> { [] } +END + +TACTIC EXTEND firstorder +| [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> + { gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] } +| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> + { gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l } +| [ "firstorder" tactic_opt(t) firstorder_using(l) + "with" ne_preident_list(l') ] -> + { gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' } +END + +TACTIC EXTEND gintuition +| [ "gintuition" tactic_opt(t) ] -> + { gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] } +END -- cgit v1.2.3