diff options
| author | Emilio Jesus Gallego Arias | 2018-10-16 01:04:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-16 01:04:47 +0200 |
| commit | 1b4e757a90d8c0a5fc8599fffcda75618b468032 (patch) | |
| tree | dcb3956c54c6a07c26dc4f342f3bd1d330a46cc2 /plugins | |
| parent | da4c6c4022625b113b7df4a61c93ec351a6d194b (diff) | |
| parent | 41b640b46f9152c62271adaa930aa8e86a88f3e5 (diff) | |
Merge PR #8733: Implement ARGUMENT EXTEND in coqpp
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/g_extraction.mlg (renamed from plugins/extraction/g_extraction.ml4) | 81 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.mlg (renamed from plugins/firstorder/g_ground.ml4) | 58 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg (renamed from plugins/funind/g_indfun.ml4) | 122 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.mlg (renamed from plugins/ltac/extraargs.ml4) | 172 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.mlg (renamed from plugins/ltac/extratactics.ml4) | 461 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.mlg (renamed from plugins/ltac/g_auto.ml4) | 146 | ||||
| -rw-r--r-- | plugins/ltac/g_class.mlg (renamed from plugins/ltac/g_class.ml4) | 64 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg (renamed from plugins/ltac/g_ltac.ml4) | 358 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.mlg (renamed from plugins/ltac/g_obligations.ml4) | 80 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg (renamed from plugins/ltac/g_rewrite.ml4) | 221 | ||||
| -rw-r--r-- | plugins/ltac/ltac_plugin.mlpack | 2 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac_tactics.mlg (renamed from plugins/ltac/profile_ltac_tactics.ml4) | 34 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 93 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 59 | ||||
| -rw-r--r-- | plugins/setoid_ring/g_newring.mlg (renamed from plugins/setoid_ring/g_newring.ml4) | 82 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg (renamed from plugins/ssr/ssrparser.ml4) | 1291 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg (renamed from plugins/ssr/ssrvernac.ml4) | 224 | ||||
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mlg (renamed from plugins/ssrmatching/g_ssrmatching.ml4) | 87 | ||||
| -rw-r--r-- | plugins/syntax/g_numeral.mlg (renamed from plugins/syntax/g_numeral.ml4) | 14 |
19 files changed, 2236 insertions, 1413 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.mlg index 93909f3e64..1445dffefa 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.mlg @@ -8,14 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Pcoq.Prim +} + DECLARE PLUGIN "extraction_plugin" +{ + (* ML names *) open Ltac_plugin -open Genarg open Stdarg open Pp open Names @@ -24,23 +29,31 @@ open Extract_env let pr_mlname _ _ _ s = spc () ++ qs s +} + ARGUMENT EXTEND mlname TYPED AS string - PRINTED BY pr_mlname -| [ preident(id) ] -> [ id ] -| [ string(s) ] -> [ s ] + PRINTED BY { pr_mlname } +| [ preident(id) ] -> { id } +| [ string(s) ] -> { s } END +{ + let pr_int_or_id _ _ _ = function | ArgInt i -> int i | ArgId id -> Id.print id +} + ARGUMENT EXTEND int_or_id - PRINTED BY pr_int_or_id -| [ preident(id) ] -> [ ArgId (Id.of_string id) ] -| [ integer(i) ] -> [ ArgInt i ] + PRINTED BY { pr_int_or_id } +| [ preident(id) ] -> { ArgId (Id.of_string id) } +| [ integer(i) ] -> { ArgInt i } END +{ + let pr_language = function | Ocaml -> str "OCaml" | Haskell -> str "Haskell" @@ -52,117 +65,119 @@ let warn_deprecated_ocaml_spelling = (fun () -> strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) +} + VERNAC ARGUMENT EXTEND language -PRINTED BY pr_language -| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ] -| [ "OCaml" ] -> [ Ocaml ] -| [ "Haskell" ] -> [ Haskell ] -| [ "Scheme" ] -> [ Scheme ] -| [ "JSON" ] -> [ JSON ] +PRINTED BY { pr_language } +| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } +| [ "OCaml" ] -> { Ocaml } +| [ "Haskell" ] -> { Haskell } +| [ "Scheme" ] -> { Scheme } +| [ "JSON" ] -> { JSON } END (* Extraction commands *) VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY (* Extraction in the Coq toplevel *) -| [ "Extraction" global(x) ] -> [ simple_extraction x ] -| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ] +| [ "Extraction" global(x) ] -> { simple_extraction x } +| [ "Recursive" "Extraction" ne_global_list(l) ] -> { full_extraction None l } (* Monolithic extraction to a file *) | [ "Extraction" string(f) ne_global_list(l) ] - -> [ full_extraction (Some f) l ] + -> { full_extraction (Some f) l } (* Extraction to a temporary file and OCaml compilation *) | [ "Extraction" "TestCompile" ne_global_list(l) ] - -> [ extract_and_compile l ] + -> { extract_and_compile l } END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY (* Same, with content splitted in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] - -> [ separate_extraction l ] + -> { separate_extraction l } END (* Modular extraction (one Coq library = one ML module) *) VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY | [ "Extraction" "Library" ident(m) ] - -> [ extraction_library false m ] + -> { extraction_library false m } END VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY | [ "Recursive" "Extraction" "Library" ident(m) ] - -> [ extraction_library true m ] + -> { extraction_library true m } END (* Target Language *) VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF | [ "Extraction" "Language" language(l) ] - -> [ extraction_language l ] + -> { extraction_language l } END VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF (* Custom inlining directives *) | [ "Extraction" "Inline" ne_global_list(l) ] - -> [ extraction_inline true l ] + -> { extraction_inline true l } END VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF | [ "Extraction" "NoInline" ne_global_list(l) ] - -> [ extraction_inline false l ] + -> { extraction_inline false l } END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> [Feedback. msg_info (print_extraction_inline ()) ] + -> {Feedback. msg_info (print_extraction_inline ()) } END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF | [ "Reset" "Extraction" "Inline" ] - -> [ reset_extraction_inline () ] + -> { reset_extraction_inline () } END VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF (* Custom implicit arguments of some csts/inds/constructors *) | [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ] - -> [ extraction_implicit r l ] + -> { extraction_implicit r l } END VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF (* Force Extraction to not use some filenames *) | [ "Extraction" "Blacklist" ne_ident_list(l) ] - -> [ extraction_blacklist l ] + -> { extraction_blacklist l } END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> [ Feedback.msg_info (print_extraction_blacklist ()) ] + -> { Feedback.msg_info (print_extraction_blacklist ()) } END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF | [ "Reset" "Extraction" "Blacklist" ] - -> [ reset_extraction_blacklist () ] + -> { reset_extraction_blacklist () } END (* Overriding of a Coq object by an ML one *) VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] - -> [ extract_constant_inline false x idl y ] + -> { extract_constant_inline false x idl y } END VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] - -> [ extract_constant_inline true x [] y ] + -> { extract_constant_inline true x [] y } END VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF | [ "Extract" "Inductive" global(x) "=>" mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] - -> [ extract_inductive x id idl o ] + -> { extract_inductive x id idl o } END (* Show the extraction of the current proof *) VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY | [ "Show" "Extraction" ] - -> [ show_extraction () ] + -> { show_extraction () } END diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.mlg index fdeef5f0ac..c41687e721 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.mlg @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ open Ltac_plugin open Formula @@ -21,10 +22,14 @@ open Stdarg open Tacarg open Pcoq.Prim +} + DECLARE PLUGIN "ground_plugin" (* declaring search depth as a global option *) +{ + let ground_depth=ref 3 let _= @@ -65,22 +70,25 @@ let default_intuition_tac = 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 +} + +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); - st - ] + (Tacintern.glob_tactic t) + } END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY -| [ "Print" "Firstorder" "Solver" ] -> [ +| [ "Print" "Firstorder" "Solver" ] -> { Feedback.msg_info - (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] + (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 = @@ -123,7 +131,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 @@ -134,34 +141,33 @@ 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_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 ] -| [ "using" reference(a) reference(b) reference_list(l) ] -> [ + 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) 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 ] + { 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' ] + { 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) [] [] ] +| [ "gintuition" tactic_opt(t) ] -> + { gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] } END 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/ltac/extraargs.ml4 b/plugins/ltac/extraargs.mlg index f4555509cc..c4c4e51ecc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.mlg @@ -8,8 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Pp -open Genarg open Stdarg open Tacarg open Pcoq.Prim @@ -62,22 +63,29 @@ let pr_orient _prc _prlc _prt = function | true -> Pp.mt () | false -> Pp.str " <-" -ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient -| [ "->" ] -> [ true ] -| [ "<-" ] -> [ false ] -| [ ] -> [ true ] +} + +ARGUMENT EXTEND orient TYPED AS bool PRINTED BY { pr_orient } +| [ "->" ] -> { true } +| [ "<-" ] -> { false } +| [ ] -> { true } END +{ + let pr_int _ _ _ i = Pp.int i let _natural = Pcoq.Prim.natural -ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int -| [ _natural(i) ] -> [ i ] +} + +ARGUMENT EXTEND natural TYPED AS int PRINTED BY { pr_int } +| [ _natural(i) ] -> { i } END -let pr_orient = pr_orient () () () +{ +let pr_orient = pr_orient () () () let pr_int_list = Pp.pr_sequence Pp.int let pr_int_list_full _prc _prlc _prt l = pr_int_list l @@ -116,21 +124,25 @@ let glob_occs ist l = l let subst_occs evm l = l +} + ARGUMENT EXTEND occurrences TYPED AS int list - PRINTED BY pr_int_list_full + PRINTED BY { pr_int_list_full } - INTERPRETED BY interp_occs - GLOBALIZED BY glob_occs - SUBSTITUTED BY subst_occs + INTERPRETED BY { interp_occs } + GLOBALIZED BY { glob_occs } + SUBSTITUTED BY { subst_occs } - RAW_PRINTED BY pr_occurrences - GLOB_PRINTED BY pr_occurrences + RAW_PRINTED BY { pr_occurrences } + GLOB_PRINTED BY { pr_occurrences } -| [ ne_integer_list(l) ] -> [ ArgArg l ] -| [ var(id) ] -> [ ArgVar id ] +| [ ne_integer_list(l) ] -> { ArgArg l } +| [ var(id) ] -> { ArgVar id } END +{ + let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c @@ -147,49 +159,61 @@ let pr_lconstr _ prc _ c = prc c let subst_glob = Tacsubst.subst_glob_constr_and_expr +} + ARGUMENT EXTEND glob - PRINTED BY pr_globc + PRINTED BY { pr_globc } - INTERPRETED BY interp_glob - GLOBALIZED BY glob_glob - SUBSTITUTED BY subst_glob + INTERPRETED BY { interp_glob } + GLOBALIZED BY { glob_glob } + SUBSTITUTED BY { subst_glob } - RAW_PRINTED BY pr_gen - GLOB_PRINTED BY pr_gen - [ constr(c) ] -> [ c ] + RAW_PRINTED BY { pr_gen } + GLOB_PRINTED BY { pr_gen } +| [ constr(c) ] -> { c } END +{ + let l_constr = Pcoq.Constr.lconstr +} + ARGUMENT EXTEND lconstr TYPED AS constr - PRINTED BY pr_lconstr - [ l_constr(c) ] -> [ c ] + PRINTED BY { pr_lconstr } +| [ l_constr(c) ] -> { c } END ARGUMENT EXTEND lglob TYPED AS glob - PRINTED BY pr_globc + PRINTED BY { pr_globc } - INTERPRETED BY interp_glob - GLOBALIZED BY glob_glob - SUBSTITUTED BY subst_glob + INTERPRETED BY { interp_glob } + GLOBALIZED BY { glob_glob } + SUBSTITUTED BY { subst_glob } - RAW_PRINTED BY pr_gen - GLOB_PRINTED BY pr_gen - [ lconstr(c) ] -> [ c ] + RAW_PRINTED BY { pr_gen } + GLOB_PRINTED BY { pr_gen } +| [ lconstr(c) ] -> { c } END +{ + let interp_casted_constr ist gl c = interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c +} + ARGUMENT EXTEND casted_constr TYPED AS constr - PRINTED BY pr_gen - INTERPRETED BY interp_casted_constr - [ constr(c) ] -> [ c ] + PRINTED BY { pr_gen } + INTERPRETED BY { interp_casted_constr } +| [ constr(c) ] -> { c } END +{ + type 'id gen_place= ('id * hyp_location_flag,unit) location type loc_place = lident gen_place @@ -228,70 +252,84 @@ let warn_deprecated_instantiate_syntax = ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") ) +} + ARGUMENT EXTEND hloc - PRINTED BY pr_place - INTERPRETED BY interp_place - GLOBALIZED BY intern_place - SUBSTITUTED BY subst_place - RAW_PRINTED BY pr_loc_place - GLOB_PRINTED BY pr_loc_place - [ ] -> - [ ConclLocation () ] + PRINTED BY { pr_place } + INTERPRETED BY { interp_place } + GLOBALIZED BY { intern_place } + SUBSTITUTED BY { subst_place } + RAW_PRINTED BY { pr_loc_place } + GLOB_PRINTED BY { pr_loc_place } +| [ ] -> + { ConclLocation () } | [ "in" "|-" "*" ] -> - [ ConclLocation () ] + { ConclLocation () } | [ "in" ident(id) ] -> - [ HypLocation ((CAst.make id),InHyp) ] + { HypLocation ((CAst.make id),InHyp) } | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ warn_deprecated_instantiate_syntax ("Type","type",id); - HypLocation ((CAst.make id),InHypTypeOnly) ] + { warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) } | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ warn_deprecated_instantiate_syntax ("Value","value",id); - HypLocation ((CAst.make id),InHypValueOnly) ] + { warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) } | [ "in" "(" "type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] + { HypLocation ((CAst.make id),InHypTypeOnly) } | [ "in" "(" "value" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypValueOnly) ] + { HypLocation ((CAst.make id),InHypValueOnly) } END +{ + let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m +} + ARGUMENT EXTEND rename - TYPED AS ident * ident - PRINTED BY pr_rename -| [ ident(n) "into" ident(m) ] -> [ (n, m) ] + TYPED AS (ident * ident) + PRINTED BY { pr_rename } +| [ ident(n) "into" ident(m) ] -> { (n, m) } END (* Julien: Mise en commun des differentes version de replace with in by *) +{ + let pr_by_arg_tac _prc _prlc prtac opt_c = match opt_c with | None -> mt () | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) +} + ARGUMENT EXTEND by_arg_tac - TYPED AS tactic_opt - PRINTED BY pr_by_arg_tac -| [ "by" tactic3(c) ] -> [ Some c ] -| [ ] -> [ None ] + TYPED AS tactic option + PRINTED BY { pr_by_arg_tac } +| [ "by" tactic3(c) ] -> { Some c } +| [ ] -> { None } END +{ + let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl let in_clause' = Pltac.in_clause +} + ARGUMENT EXTEND in_clause TYPED AS clause_dft_concl - PRINTED BY pr_in_top_clause - RAW_TYPED AS clause_dft_concl - RAW_PRINTED BY pr_in_clause - GLOB_TYPED AS clause_dft_concl - GLOB_PRINTED BY pr_in_clause -| [ in_clause'(cl) ] -> [ cl ] + PRINTED BY { pr_in_top_clause } + RAW_PRINTED BY { pr_in_clause } + GLOB_PRINTED BY { pr_in_clause } +| [ in_clause'(cl) ] -> { cl } END +{ + let local_test_lpar_id_colon = let err () = raise Stream.Failure in Pcoq.Gram.Entry.of_parser "lpar_id_colon" @@ -308,6 +346,8 @@ let local_test_lpar_id_colon = let pr_lpar_id_colon _ _ _ _ = mt () -ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon -| [ local_test_lpar_id_colon(x) ] -> [ () ] +} + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon } +| [ local_test_lpar_id_colon(x) ] -> { () } END diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.mlg index e5b032e638..b660865e8b 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Pp open Constr open Genarg @@ -30,8 +32,14 @@ open Tactics open Proofview.Notations open Vernacinterp +let wit_hyp = wit_var + +} + DECLARE PLUGIN "ltac_plugin" +{ + (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) (* cutrewrite, dependent rewrite *) @@ -43,7 +51,7 @@ let with_delayed_uconstr ist c tac = use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true - } in + } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -54,26 +62,30 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac = let replace_term ist dir_opt c cl = with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) +} + TACTIC EXTEND replace - ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] +| ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] +-> { replace_in_clause_maybe_by ist c1 c2 cl tac } END TACTIC EXTEND replace_term_left - [ "replace" "->" uconstr(c) clause(cl) ] - -> [ replace_term ist (Some true) c cl ] +| [ "replace" "->" uconstr(c) clause(cl) ] + -> { replace_term ist (Some true) c cl } END TACTIC EXTEND replace_term_right - [ "replace" "<-" uconstr(c) clause(cl) ] - -> [ replace_term ist (Some false) c cl ] +| [ "replace" "<-" uconstr(c) clause(cl) ] + -> { replace_term ist (Some false) c cl } END TACTIC EXTEND replace_term - [ "replace" uconstr(c) clause(cl) ] - -> [ replace_term ist None c cl ] +| [ "replace" uconstr(c) clause(cl) ] + -> { replace_term ist None c cl } END +{ + let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n | NamedHyp id -> None,ElimOnIdent (CAst.make id) @@ -94,28 +106,36 @@ let elimOnConstrWithHoles tac with_evars c = Tacticals.New.tclDELAYEDWITHHOLES with_evars c (fun c -> tac with_evars (Some (None,ElimOnConstr c))) +} + TACTIC EXTEND simplify_eq - [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ] -| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ] +| [ "simplify_eq" ] -> { dEq ~keep_proofs:None false None } +| [ "simplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) false c } END TACTIC EXTEND esimplify_eq -| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ] -| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ] +| [ "esimplify_eq" ] -> { dEq ~keep_proofs:None true None } +| [ "esimplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) true c } END +{ + let discr_main c = elimOnConstrWithHoles discr_tac false c +} + TACTIC EXTEND discriminate -| [ "discriminate" ] -> [ discr_tac false None ] +| [ "discriminate" ] -> { discr_tac false None } | [ "discriminate" destruction_arg(c) ] -> - [ mytclWithHoles discr_tac false c ] + { mytclWithHoles discr_tac false c } END TACTIC EXTEND ediscriminate -| [ "ediscriminate" ] -> [ discr_tac true None ] +| [ "ediscriminate" ] -> { discr_tac true None } | [ "ediscriminate" destruction_arg(c) ] -> - [ mytclWithHoles discr_tac true c ] + { mytclWithHoles discr_tac true c } END +{ + let discrHyp id = Proofview.tclEVARMAP >>= fun sigma -> discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) @@ -123,39 +143,45 @@ let discrHyp id = let injection_main with_evars c = elimOnConstrWithHoles (injClause None None) with_evars c +} + TACTIC EXTEND injection -| [ "injection" ] -> [ injClause None None false None ] -| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ] +| [ "injection" ] -> { injClause None None false None } +| [ "injection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) false c } END TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause None None true None ] -| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ] +| [ "einjection" ] -> { injClause None None true None } +| [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c } END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - [ injClause None (Some ipat) false None ] + { injClause None (Some ipat) false None } | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause None (Some ipat)) false c ] + { mytclWithHoles (injClause None (Some ipat)) false c } END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - [ injClause None (Some ipat) true None ] + { injClause None (Some ipat) true None } | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause None (Some ipat)) true c ] + { mytclWithHoles (injClause None (Some ipat)) true c } END TACTIC EXTEND simple_injection -| [ "simple" "injection" ] -> [ simpleInjClause None false None ] -| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ] +| [ "simple" "injection" ] -> { simpleInjClause None false None } +| [ "simple" "injection" destruction_arg(c) ] -> { mytclWithHoles (simpleInjClause None) false c } END +{ + let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) +} + TACTIC EXTEND dependent_rewrite -| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] +| [ "dependent" "rewrite" orient(b) constr(c) ] -> { rewriteInConcl b c } | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] - -> [ rewriteInHyp b c id ] + -> { rewriteInHyp b c id } END (** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to @@ -163,43 +189,53 @@ END "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ] +| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> [ cutRewriteInHyp b eqn id ] + -> { cutRewriteInHyp b eqn id } END (**********************************************************************) (* Decompose *) TACTIC EXTEND decompose_sum -| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ] +| [ "decompose" "sum" constr(c) ] -> { Elim.h_decompose_or c } END TACTIC EXTEND decompose_record -| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ] +| [ "decompose" "record" constr(c) ] -> { Elim.h_decompose_and c } END (**********************************************************************) (* Contradiction *) +{ + open Contradiction +} + TACTIC EXTEND absurd - [ "absurd" constr(c) ] -> [ absurd c ] +| [ "absurd" constr(c) ] -> { absurd c } END +{ + let onSomeWithHoles tac = function | None -> tac None | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) +} + TACTIC EXTEND contradiction - [ "contradiction" constr_with_bindings_opt(c) ] -> - [ onSomeWithHoles contradiction c ] +| [ "contradiction" constr_with_bindings_opt(c) ] -> + { onSomeWithHoles contradiction c } END (**********************************************************************) (* AutoRewrite *) +{ + open Autorewrite let pr_orient _prc _prlc _prt = function @@ -209,50 +245,58 @@ let pr_orient _prc _prlc _prt = function let pr_orient_string _prc _prlc _prt (orient, s) = pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s -ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_string -| [ orient(r) preident(i) ] -> [ r, i ] +} + +ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY { pr_orient_string } +| [ orient(r) preident(i) ] -> { r, i } END TACTIC EXTEND autorewrite | [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> - [ auto_multi_rewrite l ( cl) ] + { auto_multi_rewrite l ( cl) } | [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> - [ + { auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl - ] + } END TACTIC EXTEND autorewrite_star | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] -> - [ auto_multi_rewrite ~conds:AllMatches l cl ] + { auto_multi_rewrite ~conds:AllMatches l cl } | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> - [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl ] + { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl } END (**********************************************************************) (* Rewrite star *) +{ + let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in with_delayed_uconstr ist c (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) +} + TACTIC EXTEND rewrite_star | [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ] + { rewrite_star ist (Some id) o (occurrences_of occ) c tac } | [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ] + { rewrite_star ist (Some id) o (occurrences_of occ) c tac } | [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o Locus.AllOccurrences c tac ] + { rewrite_star ist (Some id) o Locus.AllOccurrences c tac } | [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> - [ rewrite_star ist None o (occurrences_of occ) c tac ] + { rewrite_star ist None o (occurrences_of occ) c tac } | [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] -> - [ rewrite_star ist None o Locus.AllOccurrences c tac ] + { rewrite_star ist None o Locus.AllOccurrences c tac } END (**********************************************************************) (* Hint Rewrite *) +{ + let add_rewrite_hint ~poly bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in @@ -274,21 +318,25 @@ let add_rewrite_hint ~poly bases ort t lcsr = let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater -VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint - [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ] +} + +VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:atts.polymorphic bl o None l } | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ] + { add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l } | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ] + { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l } | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ] + { add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l } END (**********************************************************************) (* Refine *) +{ + open EConstr open Vars @@ -304,7 +352,7 @@ let refine_tac ist simple with_classes c = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = - { constr_flags () with Pretyping.use_typeclasses = with_classes } in + { (constr_flags ()) with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in let update = begin fun sigma -> @@ -317,125 +365,141 @@ let refine_tac ist simple with_classes c = Proofview.shelve_unifiable end +} + TACTIC EXTEND refine | [ "refine" uconstr(c) ] -> - [ refine_tac ist false true c ] + { refine_tac ist false true c } END TACTIC EXTEND simple_refine | [ "simple" "refine" uconstr(c) ] -> - [ refine_tac ist true true c ] + { refine_tac ist true true c } END TACTIC EXTEND notcs_refine | [ "notypeclasses" "refine" uconstr(c) ] -> - [ refine_tac ist false false c ] + { refine_tac ist false false c } END TACTIC EXTEND notcs_simple_refine | [ "simple" "notypeclasses" "refine" uconstr(c) ] -> - [ refine_tac ist true false c ] + { refine_tac ist true false c } END (* Solve unification constraints using heuristics or fail if any remain *) TACTIC EXTEND solve_constraints -[ "solve_constraints" ] -> [ Refine.solve_constraints ] +| [ "solve_constraints" ] -> { Refine.solve_constraints } END (**********************************************************************) (* Inversion lemmas (Leminv) *) +{ + open Inv open Leminv let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater +} + (*VERNAC ARGUMENT EXTEND sort_family -| [ "Set" ] -> [ InSet ] -| [ "Prop" ] -> [ InProp ] -| [ "Type" ] -> [ InType ] +| [ "Set" ] -> { InSet } +| [ "Prop" ] -> { InProp } +| [ "Type" ] -> { InType } END*) -VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear +VERNAC COMMAND EXTEND DeriveInversionClear | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> + => { seff na } + -> { let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ] + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac } -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ fun ~atts ~st -> +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } + -> { let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ] + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac } END -VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion +VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> + => { seff na } + -> { let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ] + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac } -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ fun ~atts ~st -> +| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } + -> { let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ] + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac } END -VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion +VERNAC COMMAND EXTEND DeriveDependentInversion | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> + => { seff na } + -> { let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ] + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac } END -VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear +VERNAC COMMAND EXTEND DeriveDependentInversionClear | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> + => { seff na } + -> { let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ] + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac } END (**********************************************************************) (* Subst *) TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> [ subst l ] -| [ "subst" ] -> [ subst_all () ] +| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ] -> { subst_all () } END +{ + let simple_subst_tactic_flags = { only_leibniz = true; rewrite_dependent_proof = false } +} + TACTIC EXTEND simple_subst -| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags () ] +| [ "simple" "subst" ] -> { subst_all ~flags:simple_subst_tactic_flags () } END +{ + open Evar_tactics +} + (**********************************************************************) (* Evar creation *) (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ] -| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ] +| [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> { let_evar (Name.Name id) typ } +| [ "evar" constr(typ) ] -> { let_evar Name.Anonymous typ } END TACTIC EXTEND instantiate - [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> - [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ] +| [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> + { Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals } | [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> - [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ] -| [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ] + { Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals } +| [ "instantiate" ] -> { Proofview.V82.nf_evar_goals } END (**********************************************************************) (** Nijmegen "step" tactic for setoid rewriting *) +{ + open Tactics open Glob_term open Libobject @@ -489,28 +553,32 @@ let add_transitivity_lemma left lem = let lem' = EConstr.to_constr sigma lem' in add_anonymous_leaf (inTransitivity (left,lem')) +} + (* Vernacular syntax *) TACTIC EXTEND stepl -| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ] -| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ] +| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) } +| ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) } END TACTIC EXTEND stepr -| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ] -| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ] +| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) } +| ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) } END VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF | [ "Declare" "Left" "Step" constr(t) ] -> - [ add_transitivity_lemma true t ] + { add_transitivity_lemma true t } END VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF | [ "Declare" "Right" "Step" constr(t) ] -> - [ add_transitivity_lemma false t ] + { add_transitivity_lemma false t } END +{ + let cache_implicit_tactic (_,tac) = match tac with | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) | None -> Pfedit.clear_implicit_tactic () @@ -537,9 +605,11 @@ let clear_implicit_tactic () = let () = warn_deprecated_implicit_tactic () in Lib.add_anonymous_leaf (inImplicitTactic None) +} + VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ] -| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ] +| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac } +| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () } END @@ -549,16 +619,16 @@ END (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs -| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ] +| ["generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false id } END TACTIC EXTEND dep_generalize_eqs -| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ] +| ["dependent" "generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false ~force_dep:true id } END TACTIC EXTEND generalize_eqs_vars -| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ] +| ["generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~generalize_vars:true id } END TACTIC EXTEND dep_generalize_eqs_vars -| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ] +| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~force_dep:true ~generalize_vars:true id } END (** Tactic to automatically simplify hypotheses of the form [ΠΔ, x_i = t_i -> T] @@ -566,7 +636,7 @@ END during dependent induction. For internal use. *) TACTIC EXTEND specialize_eqs -[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ] +| [ "specialize_eqs" hyp(id) ] -> { specialize_eqs id } END (**********************************************************************) @@ -577,6 +647,8 @@ END (* Contributed by Chung-Kil Hur (Winter 2009) *) (**********************************************************************) +{ + let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in @@ -593,7 +665,7 @@ let subst_var_with_hole occ tid t = Evar_kinds.qm_obligation=Evar_kinds.Define true; Evar_kinds.qm_name=Anonymous; Evar_kinds.qm_record_field=None; - }, IntroAnonymous, None))) + }, IntroAnonymous, None))) else x | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t @@ -608,7 +680,7 @@ let subst_hole_with_term occ tc t = Evar_kinds.qm_obligation=Evar_kinds.Define true; Evar_kinds.qm_name=Anonymous; Evar_kinds.qm_record_field=None; - }, IntroAnonymous, s) -> + }, IntroAnonymous, s) -> decr occref; if Int.equal !occref 0 then tc else @@ -618,7 +690,7 @@ let subst_hole_with_term occ tc t = Evar_kinds.qm_obligation=Evar_kinds.Define true; Evar_kinds.qm_name=Anonymous; Evar_kinds.qm_record_field=None; - },IntroAnonymous,s)) + },IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t @@ -659,9 +731,11 @@ let hResolve_auto id c t = in resolve_auto 1 +} + TACTIC EXTEND hresolve_core -| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c occ t ] -| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ] +| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t } +| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> { hResolve_auto id c t } END (** @@ -669,7 +743,7 @@ END *) TACTIC EXTEND hget_evar -| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ] +| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n } END (**********************************************************************) @@ -682,6 +756,8 @@ END (* Contributed by Julien Forest and Pierre Courtieu (july 2010) *) (**********************************************************************) +{ + exception Found of unit Proofview.tactic let rewrite_except h = @@ -763,9 +839,11 @@ let destauto_in id = destauto ctype end +} + TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ] -| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] +| [ "destauto" ] -> { Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end } +| [ "destauto" "in" hyp(id) ] -> { destauto_in id } END (**********************************************************************) @@ -776,116 +854,116 @@ END (**********************************************************************) TACTIC EXTEND transparent_abstract -| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] -| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] +| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } END (* ********************************************************************* *) TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] +| [ "constr_eq" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:false x y } END TACTIC EXTEND constr_eq_strict -| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] +| [ "constr_eq_strict" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:true x y } END TACTIC EXTEND constr_eq_nounivs -| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [ +| [ "constr_eq_nounivs" constr(x) constr(y) ] -> { Proofview.tclEVARMAP >>= fun sigma -> - if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] + if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") } END TACTIC EXTEND is_evar -| [ "is_evar" constr(x) ] -> [ +| [ "is_evar" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Evar _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") - ] + } END TACTIC EXTEND has_evar -| [ "has_evar" constr(x) ] -> [ +| [ "has_evar" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> if Evarutil.has_undefined_evars sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") -] +} END TACTIC EXTEND is_hyp -| [ "is_var" constr(x) ] -> [ +| [ "is_var" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Var _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ] + | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") } END TACTIC EXTEND is_fix -| [ "is_fix" constr(x) ] -> [ +| [ "is_fix" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Fix _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] -END;; + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") } +END TACTIC EXTEND is_cofix -| [ "is_cofix" constr(x) ] -> [ +| [ "is_cofix" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | CoFix _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] -END;; + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") } +END TACTIC EXTEND is_ind -| [ "is_ind" constr(x) ] -> [ +| [ "is_ind" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Ind _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ] -END;; + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") } +END TACTIC EXTEND is_constructor -| [ "is_constructor" constr(x) ] -> [ +| [ "is_constructor" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Construct _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ] -END;; + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") } +END TACTIC EXTEND is_proj -| [ "is_proj" constr(x) ] -> [ +| [ "is_proj" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Proj _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ] -END;; + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") } +END TACTIC EXTEND is_const -| [ "is_const" constr(x) ] -> [ +| [ "is_const" constr(x) ] -> { Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with | Const _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ] -END;; + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") } +END (* Command to grab the evars left unresolved at the end of a proof. *) (* spiwack: I put it in extratactics because it is somewhat tied with the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -[ "Grab" "Existential" "Variables" ] - => [ Vernac_classifier.classify_as_proofstep ] - -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] +| [ "Grab" "Existential" "Variables" ] + => { Vernac_classifier.classify_as_proofstep } + -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } END (* Shelves all the goals under focus. *) TACTIC EXTEND shelve | [ "shelve" ] -> - [ Proofview.shelve ] + { Proofview.shelve } END (* Shelves the unifiable goals under focus, i.e. the goals which @@ -893,25 +971,25 @@ END considered). *) TACTIC EXTEND shelve_unifiable | [ "shelve_unifiable" ] -> - [ Proofview.shelve_unifiable ] + { Proofview.shelve_unifiable } END (* Unshelves the goal shelved by the tactic. *) TACTIC EXTEND unshelve | [ "unshelve" tactic1(t) ] -> - [ + { Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> let gls = List.map Proofview.with_empty_state gls in Proofview.Unsafe.tclGETGOALS >>= fun ogls -> Proofview.Unsafe.tclSETGOALS (gls @ ogls) - ] + } END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve -[ "Unshelve" ] - => [ Vernac_classifier.classify_as_proofstep ] - -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ] +| [ "Unshelve" ] + => { Vernac_classifier.classify_as_proofstep } + -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } END (* Gives up on the goals under focus: the goals are considered solved, @@ -919,24 +997,26 @@ END these goals. *) TACTIC EXTEND give_up | [ "give_up" ] -> - [ Proofview.give_up ] + { Proofview.give_up } END (* cycles [n] goals *) TACTIC EXTEND cycle -| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle n ] +| [ "cycle" int_or_var(n) ] -> { Proofview.cycle n } END (* swaps goals number [i] and [j] *) TACTIC EXTEND swap -| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap i j ] +| [ "swap" int_or_var(i) int_or_var(j) ] -> { Proofview.swap i j } END (* reverses the list of focused goals *) TACTIC EXTEND revgoals -| [ "revgoals" ] -> [ Proofview.revgoals ] +| [ "revgoals" ] -> { Proofview.revgoals } END +{ + type cmp = | Eq | Lt | Le @@ -965,29 +1045,35 @@ let pr_itest = pr_test_gen Pp.int let pr_itest' _prc _prlc _prt = pr_itest +} - -ARGUMENT EXTEND comparison PRINTED BY pr_cmp' -| [ "=" ] -> [ Eq ] -| [ "<" ] -> [ Lt ] -| [ "<=" ] -> [ Le ] -| [ ">" ] -> [ Gt ] -| [ ">=" ] -> [ Ge ] +ARGUMENT EXTEND comparison PRINTED BY { pr_cmp' } +| [ "=" ] -> { Eq } +| [ "<" ] -> { Lt } +| [ "<=" ] -> { Le } +| [ ">" ] -> { Gt } +| [ ">=" ] -> { Ge } END +{ + let interp_test ist gls = function | Test (c,x,y) -> project gls , Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y) +} + ARGUMENT EXTEND test - PRINTED BY pr_itest' - INTERPRETED BY interp_test - RAW_PRINTED BY pr_test' - GLOB_PRINTED BY pr_test' -| [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ] + PRINTED BY { pr_itest' } + INTERPRETED BY { interp_test } + RAW_PRINTED BY { pr_test' } + GLOB_PRINTED BY { pr_test' } +| [ int_or_var(x) comparison(c) int_or_var(y) ] -> { Test(c,x,y) } END +{ + let interp_cmp = function | Eq -> Int.equal | Lt -> ((<):int->int->bool) @@ -1005,11 +1091,14 @@ let guard tst = let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in Tacticals.New.tclZEROMSG msg +} TACTIC EXTEND guard -| [ "guard" test(tst) ] -> [ guard tst ] +| [ "guard" test(tst) ] -> { guard tst } END +{ + let decompose l c = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in @@ -1021,14 +1110,16 @@ let decompose l c = Elim.h_decompose l c end +} + TACTIC EXTEND decompose -| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] +| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> { decompose l c } END (** library/keys *) VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF -| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ +| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> { let get_key c = let env = Global.env () in let evd = Evd.from_env env in @@ -1040,26 +1131,30 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF let k2 = get_key c' in match k1, k2 with | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 - | _ -> () ] + | _ -> () } END VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY -| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ] +| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) } END VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] -> - [ Proof_global.compact_the_proof () ] -| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> - [ Gc.compact () ] +| [ "Optimize" "Proof" ] => { Vernac_classifier.classify_as_proofstep } -> + { Proof_global.compact_the_proof () } +| [ "Optimize" "Heap" ] => { Vernac_classifier.classify_as_proofstep } -> + { Gc.compact () } END (** tactic analogous to "OPTIMIZE HEAP" *) +{ + let tclOPTIMIZE_HEAP = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) +} + TACTIC EXTEND optimize_heap -| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ] +| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP } END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.mlg index 35ed14fc18..c07b653f3a 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.mlg @@ -8,38 +8,49 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Pp open Constr -open Genarg open Stdarg open Pcoq.Prim open Pcoq.Constr open Pltac open Hints +let wit_hyp = wit_var + +} + DECLARE PLUGIN "ltac_plugin" (* Hint bases *) TACTIC EXTEND eassumption -| [ "eassumption" ] -> [ Eauto.e_assumption ] +| [ "eassumption" ] -> { Eauto.e_assumption } END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ] +| [ "eexact" constr(c) ] -> { Eauto.e_give_exact c } END +{ + let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases +} + ARGUMENT EXTEND hintbases - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ "with" "*" ] -> [ None ] -| [ "with" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ Some [] ] + TYPED AS preident list option + PRINTED BY { pr_hintbases } +| [ "with" "*" ] -> { None } +| [ "with" ne_preident_list(l) ] -> { Some l } +| [ ] -> { Some [] } END +{ + let eval_uconstrs ist cs = let flags = { Pretyping.use_typeclasses = false; @@ -59,104 +70,108 @@ let pr_auto_using _ _ _ = Pptactic.pr_auto_using (let sigma, env = Pfedit.get_current_context () in Printer.pr_closed_glob_env env sigma) +} + ARGUMENT EXTEND auto_using - TYPED AS uconstr_list - PRINTED BY pr_auto_using - RAW_TYPED AS uconstr_list - RAW_PRINTED BY pr_auto_using_raw - GLOB_TYPED AS uconstr_list - GLOB_PRINTED BY pr_auto_using_glob -| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] -| [ ] -> [ [] ] + TYPED AS uconstr list + PRINTED BY { pr_auto_using } + RAW_PRINTED BY { pr_auto_using_raw } + GLOB_PRINTED BY { pr_auto_using_glob } +| [ "using" ne_uconstr_list_sep(l, ",") ] -> { l } +| [ ] -> { [] } END (** Auto *) TACTIC EXTEND trivial | [ "trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial (eval_uconstrs ist lems) db ] + { Auto.h_trivial (eval_uconstrs ist lems) db } END TACTIC EXTEND info_trivial | [ "info_trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ] + { Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db } END TACTIC EXTEND debug_trivial | [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ] + { Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db } END TACTIC EXTEND auto | [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto n (eval_uconstrs ist lems) db ] + { Auto.h_auto n (eval_uconstrs ist lems) db } END TACTIC EXTEND info_auto | [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ] + { Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db } END TACTIC EXTEND debug_auto | [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ] + { Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db } END (** Eauto *) TACTIC EXTEND prolog | [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> - [ Eauto.prolog_tac (eval_uconstrs ist l) n ] + { Eauto.prolog_tac (eval_uconstrs ist l) n } END +{ + let make_depth n = snd (Eauto.make_dimension n None) +} + TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] + { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND new_eauto | [ "new" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ match db with + { match db with | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems) - | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l ] + | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l } END TACTIC EXTEND debug_eauto | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] + { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND info_eauto | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] + { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND dfs_eauto | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db ] + { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db } END TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ] +| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl } END TACTIC EXTEND autounfold_one | [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> - [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) ] + { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) } | [ "autounfold_one" hintbases(db) ] -> - [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] + { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None } END TACTIC EXTEND unify -| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] -| ["unify" constr(x) constr(y) "with" preident(base) ] -> [ +| ["unify" constr(x) constr(y) ] -> { Tactics.unify x y } +| ["unify" constr(x) constr(y) "with" preident(base) ] -> { let table = try Some (Hints.searchtable_map base) with Not_found -> None in match table with | None -> @@ -165,65 +180,70 @@ TACTIC EXTEND unify | Some t -> let state = Hints.Hint_db.transparent_state t in Tactics.unify ~state x y - ] + } END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] +| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast } END +{ + let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global let glob_hints_path_atom ist = Hints.glob_hints_path_atom +} + ARGUMENT EXTEND hints_path_atom - PRINTED BY pr_hints_path_atom + PRINTED BY { pr_hints_path_atom } - GLOBALIZED BY glob_hints_path_atom + GLOBALIZED BY { glob_hints_path_atom } - RAW_PRINTED BY pr_pre_hints_path_atom - GLOB_PRINTED BY pr_hints_path_atom -| [ ne_global_list(g) ] -> [ Hints.PathHints g ] -| [ "_" ] -> [ Hints.PathAny ] + RAW_PRINTED BY { pr_pre_hints_path_atom } + GLOB_PRINTED BY { pr_hints_path_atom } +| [ ne_global_list(g) ] -> { Hints.PathHints g } +| [ "_" ] -> { Hints.PathAny } END +{ + let pr_hints_path prc prx pry c = Hints.pp_hints_path c let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c let glob_hints_path ist = Hints.glob_hints_path +} + ARGUMENT EXTEND hints_path -PRINTED BY pr_hints_path +PRINTED BY { pr_hints_path } -GLOBALIZED BY glob_hints_path -RAW_PRINTED BY pr_pre_hints_path -GLOB_PRINTED BY pr_hints_path +GLOBALIZED BY { glob_hints_path } +RAW_PRINTED BY { pr_pre_hints_path } +GLOB_PRINTED BY { pr_hints_path } -| [ "(" hints_path(p) ")" ] -> [ p ] -| [ hints_path(p) "*" ] -> [ Hints.PathStar p ] -| [ "emp" ] -> [ Hints.PathEmpty ] -| [ "eps" ] -> [ Hints.PathEpsilon ] -| [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ] -| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] -| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] +| [ "(" hints_path(p) ")" ] -> { p } +| [ hints_path(p) "*" ] -> { Hints.PathStar p } +| [ "emp" ] -> { Hints.PathEmpty } +| [ "eps" ] -> { Hints.PathEpsilon } +| [ hints_path(p) "|" hints_path(q) ] -> { Hints.PathOr (p, q) } +| [ hints_path_atom(a) ] -> { Hints.PathAtom a } +| [ hints_path(p) hints_path(q) ] -> { Hints.PathSeq (p, q) } END ARGUMENT EXTEND opthints - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ ":" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ None ] + TYPED AS preident list option + PRINTED BY { pr_hintbases } +| [ ":" ne_preident_list(l) ] -> { Some l } +| [ ] -> { None } END -VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF -| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - fun ~atts ~st -> begin +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let open Vernacinterp in let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in Hints.add_hints ~local:(Locality.make_section_locality atts.locality) (match dbnames with None -> ["core"] | Some l -> l) entry; - st - end - ] + } END diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.mlg index 1c2f90b670..9ecc36bdf3 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.mlg @@ -8,87 +8,103 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Class_tactics open Stdarg open Tacarg +} + DECLARE PLUGIN "ltac_plugin" (** Options: depth, debug and transparency settings. *) +{ + let set_transparency cl b = List.iter (fun r -> let gr = Smartlocate.global_with_alias r in let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl +} + VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ - set_transparency cl true ] +| [ "Typeclasses" "Transparent" reference_list(cl) ] -> { + set_transparency cl true } END VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ - set_transparency cl false ] +| [ "Typeclasses" "Opaque" reference_list(cl) ] -> { + set_transparency cl false } END -open Genarg +{ let pr_debug _prc _prlc _prt b = if b then Pp.str "debug" else Pp.mt() -ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug -| [ "debug" ] -> [ true ] -| [ ] -> [ false ] +} + +ARGUMENT EXTEND debug TYPED AS bool PRINTED BY { pr_debug } +| [ "debug" ] -> { true } +| [ ] -> { false } END +{ + let pr_search_strategy _prc _prlc _prt = function | Some Dfs -> Pp.str "dfs" | Some Bfs -> Pp.str "bfs" | None -> Pp.mt () -ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy -| [ "(bfs)" ] -> [ Some Bfs ] -| [ "(dfs)" ] -> [ Some Dfs ] -| [ ] -> [ None ] +} + +ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } +| [ "(bfs)" ] -> { Some Bfs } +| [ "(dfs)" ] -> { Some Dfs } +| [ ] -> { None } END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth - ] + } END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto ~strategy:Bfs ~depth:d l ] + { typeclasses_eauto ~strategy:Bfs ~depth:d l } | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto ~depth:d l ] - | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [ - typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ] + { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { + typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] } END TACTIC EXTEND head_of_constr - [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ] +| [ "head_of_constr" ident(h) constr(c) ] -> { head_of_constr h c } END TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ not_evar ty ] +| [ "not_evar" constr(ty) ] -> { not_evar ty } END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ is_ground ty ] +| [ "is_ground" constr(ty) ] -> { is_ground ty } END TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ] +| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } END +{ + (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) open Constr @@ -114,6 +130,8 @@ let progress_evars t = in t <*> check end +} + TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] +| [ "progress_evars" tactic(t) ] -> { progress_evars (Tacinterp.tactic_of_value ist t) } END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.mlg index 929390b1c4..d62f985350 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.mlg @@ -10,6 +10,8 @@ DECLARE PLUGIN "ltac_plugin" +{ + open Util open Pp open Glob_term @@ -80,282 +82,288 @@ let test_bracket_ident = let hint = G_proofs.hint -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector operconstr; tactic_then_last: - [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> - Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) - | -> [||] + [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } + | -> { [||] } ] ] ; tactic_then_gen: - [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last) - | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l)) - | ".."; l = tactic_then_last -> ([], Some (TacId [], l)) - | ta = tactic_expr -> ([ta], None) - | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last) - | -> ([TacId []], None) + [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } + | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } + | ta = tactic_expr -> { ([ta], None) } + | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | -> { ([TacId []], None) } ] ] ; tactic_then_locality: (* [true] for the local variant [TacThens] and [false] for [TacExtend] *) - [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] + [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] ; tactic_expr: [ "5" RIGHTA - [ te = binder_tactic -> te ] + [ te = binder_tactic -> { te } ] | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) - | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } + | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + let (first,tail) = tg in match l , tail with | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) | false , None -> TacThen (ta0,TacDispatch first) - | true , None -> TacThens (ta0,first) ] + | true , None -> TacThens (ta0,first) } ] | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> TacTry ta - | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) - | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta) - | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta - | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "once"; ta = tactic_expr -> TacOnce ta - | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta - | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta + [ IDENT "try"; ta = tactic_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } + | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } + | IDENT "once"; ta = tactic_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } (*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) + | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (tc,Some s) - | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ] + { TacAbstract (tc,Some s) } + | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } | IDENT "tryif" ; ta = tactic_expr ; "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] + "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchGoal (b,false,mrl) + { TacMatchGoal (b,false,mrl) } | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchGoal (b,true,mrl) + { TacMatchGoal (b,true,mrl) } | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> - TacMatch (b,c,mrl) + { TacMatch (b,c,mrl) } | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacFirst l + { TacFirst l } | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacSolve l - | IDENT "idtac"; l = LIST0 message_token -> TacId l - | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; - l = LIST0 message_token -> TacFail (g,n,l) - | st = simple_tactic -> st - | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a) + { TacSolve l } + | IDENT "idtac"; l = LIST0 message_token -> { TacId l } + | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; + l = LIST0 message_token -> { TacFail (g,n,l) } + | st = simple_tactic -> { st } + | a = tactic_arg -> { TacArg(Loc.tag ~loc a) } | r = reference; la = LIST0 tactic_arg_compat -> - TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ] + { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ] | "0" - [ "("; a = tactic_expr; ")" -> a - | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> + [ "("; a = tactic_expr; ")" -> { a } + | "["; ">"; tg = tactic_then_gen; "]" -> { + let (tf,tail) = tg in begin match tail with | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) | None -> TacDispatch tf - end - | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ] + end } + | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ] ; failkw: - [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] + [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: [ RIGHTA [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> - TacFun (it,body) - | "let"; isrec = [IDENT "rec" -> true | -> false]; + { TacFun (it,body) } + | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) - | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] + body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } + | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ] ; (* Tactic arguments to the right of an application *) tactic_arg_compat: - [ [ a = tactic_arg -> a - | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) + [ [ a = tactic_arg -> { a } + | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } (* Unambiguous entries: tolerated w/o "ltac:" modifier *) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] + | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) tactic_arg: - [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l - | IDENT "type_term"; c=uconstr -> TacPretype c - | IDENT "numgoals" -> TacNumgoals ] ] + [ [ c = constr_eval -> { ConstrMayEval c } + | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } + | IDENT "type_term"; c=uconstr -> { TacPretype c } + | IDENT "numgoals" -> { TacNumgoals } ] ] ; (* If a qualid is given, use its short name. TODO: have the shortest non ambiguous name where dots are replaced by "_"? Probably too verbose most of the time. *) fresh_id: - [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) - | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] + [ [ s = STRING -> { Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) } + | qid = qualid -> { Locus.ArgVar (CAst.make ~loc @@ Libnames.qualid_basename qid) } ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrEval (rtc,c) + { ConstrEval (rtc,c) } | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrContext (id,c) + { ConstrContext (id,c) } | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrTypeOf c ] ] + { ConstrTypeOf c } ] ] ; constr_may_eval: (* For extensions *) - [ [ c = constr_eval -> c - | c = Constr.constr -> ConstrTerm c ] ] + [ [ c = constr_eval -> { c } + | c = Constr.constr -> { ConstrTerm c } ] ] ; tactic_atom: - [ [ n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[])) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] + [ [ n = integer -> { TacGeneric (genarg_of_int n) } + | r = reference -> { TacCall (Loc.tag ~loc (r,[])) } + | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] ; match_key: - [ [ "match" -> Once - | "lazymatch" -> Select - | "multimatch" -> General ] ] + [ [ "match" -> { Once } + | "lazymatch" -> { Select } + | "multimatch" -> { General } ] ] ; input_fun: - [ [ "_" -> Name.Anonymous - | l = ident -> Name.Name l ] ] + [ [ "_" -> { Name.Anonymous } + | l = ident -> { Name.Name l } ] ] ; let_clause: [ [ idr = identref; ":="; te = tactic_expr -> - (CAst.map (fun id -> Name id) idr, arg_of_expr te) - | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr -> - (na, arg_of_expr te) + { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + { (na, arg_of_expr te) } | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ] + { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - Subterm (oid, pc) - | pc = Constr.lconstr_pattern -> Term pc ] ] + { Subterm (oid, pc) } + | pc = Constr.lconstr_pattern -> { Term pc } ] ] ; match_hyps: - [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) - | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) + [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } + | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } | na = name; ":="; mpv = match_pattern -> - let t, ty = + { let t, ty = match mpv with | Term t -> (match t with | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) + in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) } ] ] ; match_context_rule: [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> Pat (largs, mp, te) + "=>"; te = tactic_expr -> { Pat (largs, mp, te) } | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "_"; "=>"; te = tactic_expr -> All te ] ] + "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = tactic_expr -> { All te } ] ] ; match_context_list: - [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] + [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } + | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] ; match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) - | "_"; "=>"; te = tactic_expr -> All te ] ] + [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = tactic_expr -> { All te } ] ] ; match_list: - [ [ mrl = LIST1 match_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] + [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } + | "|"; mrl = LIST1 match_rule SEP "|" -> { mrl } ] ] ; message_token: - [ [ id = identref -> MsgIdent id - | s = STRING -> MsgString s - | n = integer -> MsgInt n ] ] + [ [ id = identref -> { MsgIdent id } + | s = STRING -> { MsgString s } + | n = integer -> { MsgInt n } ] ] ; ltac_def_kind: - [ [ ":=" -> false - | "::=" -> true ] ] + [ [ ":=" -> { false } + | "::=" -> { true } ] ] ; (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) + { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in - Tacexpr.TacticDefinition (id, TacFun (it, body)) + Tacexpr.TacticDefinition (id, TacFun (it, body)) } | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - if redef then Tacexpr.TacticRedefinition (name, body) + { if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in - Tacexpr.TacticDefinition (id, body) + Tacexpr.TacticDefinition (id, body) } ] ] ; tactic: - [ [ tac = tactic_expr -> tac ] ] + [ [ tac = tactic_expr -> { tac } ] ] ; range_selector: - [ [ n = natural ; "-" ; m = natural -> (n, m) - | n = natural -> (n, n) ] ] + [ [ n = natural ; "-" ; m = natural -> { (n, m) } + | n = natural -> { (n, n) } ] ] ; (* We unfold a range selectors list once so that we can make a special case * for a unique SelectNth selector. *) range_selector_or_nth: [ [ n = natural ; "-" ; m = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - Goal_select.SelectList ((n, m) :: Option.default [] l) + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { Goal_select.SelectList ((n, m) :: Option.default [] l) } | n = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - let open Goal_select in - Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { let open Goal_select in + Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] ; selector_body: - [ [ l = range_selector_or_nth -> l - | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ] + [ [ l = range_selector_or_nth -> { l } + | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] ; selector: - [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] + [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] ; toplevel_selector: - [ [ sel = selector_body; ":" -> sel - | "!"; ":" -> Goal_select.SelectAlreadyFocused - | IDENT "all"; ":" -> Goal_select.SelectAll ] ] + [ [ sel = selector_body; ":" -> { sel } + | "!"; ":" -> { Goal_select.SelectAlreadyFocused } + | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g - | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { tac g } + | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSubproof g } ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), l) + l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] -> + { Vernacexpr.VernacProof (Some (in_tac ta), l) } | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> - Vernacexpr.VernacProof (ta,Some l) ] ] + ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] -> + { Vernacexpr.VernacProof (ta,Some l) } ] ] ; hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - Hints.HintsExtern (n,c, in_tac tac) ] ] + { Hints.HintsExtern (n,c, in_tac tac) } ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> - let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in - CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] + { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in + CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] ; END +{ + open Stdarg open Tacarg open Vernacexpr @@ -390,24 +398,36 @@ let vernac_solve n info tcom b = let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s -VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector -| [ toplevel_selector(s) ] -> [ s ] +} + +VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector } +| [ toplevel_selector(s) ] -> { s } END +{ + let pr_ltac_info n = str "Info" ++ spc () ++ int n -VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info -| [ "Info" natural(n) ] -> [ n ] +} + +VERNAC ARGUMENT EXTEND ltac_info PRINTED BY { pr_ltac_info } +| [ "Info" natural(n) ] -> { n } END +{ + let pr_ltac_use_default b = if b then (* Bug: a space is inserted before "..." *) str ".." else mt () -VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default -| [ "." ] -> [ false ] -| [ "..." ] -> [ true ] +} + +VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default } +| [ "." ] -> { false } +| [ "..." ] -> { true } END +{ + let is_anonymous_abstract = function | TacAbstract (_,None) -> true | TacSolve [TacAbstract (_,None)] -> true @@ -418,36 +438,44 @@ let rm_abstract = function | x -> x let is_explicit_terminator = function TacSolve _ -> true | _ -> false -VERNAC tactic_mode EXTEND VernacSolve -| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => - [ classify_as_proofstep ] -> [ +} + +VERNAC { tactic_mode } EXTEND VernacSolve +| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => + { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in vernac_solve g n t def - ] -| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => - [ + } +| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => + { let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in let parallel = `Yes (solving_tac,anon_abstracting_tac) in let pbr = if solving_tac then Some "par" else None in VtProofStep{ parallel = parallel; proof_block_detection = pbr }, VtLater - ] -> [ + } -> { let t = rm_abstract t in vernac_solve Goal_select.SelectAll n t def - ] + } END +{ + let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")" -VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level -| [ "(" "at" "level" natural(n) ")" ] -> [ n ] +} + +VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY { pr_ltac_tactic_level } +| [ "(" "at" "level" natural(n) ")" ] -> { n } END VERNAC ARGUMENT EXTEND ltac_production_sep -| [ "," string(sep) ] -> [ sep ] +| [ "," string(sep) ] -> { sep } END +{ + let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) | Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg @@ -459,35 +487,38 @@ let pr_ltac_production_item = function in str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" -VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item -| [ string(s) ] -> [ Tacentries.TacTerm s ] +} + +VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item } +| [ string(s) ] -> { Tacentries.TacTerm s } | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ] + { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) } | [ ident(nt) ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] + { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) } END -VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation +VERNAC COMMAND EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtSideff [], VtNow ] -> - [ fun ~atts ~st -> let open Vernacinterp in + { VtSideff [], VtNow } -> + { let open Vernacinterp in let n = Option.default 0 n in let deprecation = atts.deprecated in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; - st - ] + } END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac r) ] + { Feedback.msg_notice (Tacintern.print_ltac r) } END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY | [ "Locate" "Ltac" reference(r) ] -> - [ Tacentries.print_located_tactic r ] + { Tacentries.print_located_tactic r } END +{ + let pr_ltac_ref = Libnames.pr_qualid let pr_tacdef_body tacdef_body = @@ -506,23 +537,24 @@ let pr_tacdef_body tacdef_body = ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ Pptactic.pr_raw_tactic body +} + VERNAC ARGUMENT EXTEND ltac_tacdef_body -PRINTED BY pr_tacdef_body -| [ tacdef_body(t) ] -> [ t ] +PRINTED BY { pr_tacdef_body } +| [ tacdef_body(t) ] -> { t } END -VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ +VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater - ] -> [ fun ~atts ~st -> let open Vernacinterp in + } -> { let open Vernacinterp in let deprecation = atts.deprecated in Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; - st - ] + } END VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY -| [ "Print" "Ltac" "Signatures" ] -> [ Tacentries.print_ltacs () ] +| [ "Print" "Ltac" "Signatures" ] -> { Tacentries.print_ltacs () } END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.mlg index 1f56244c75..26f2b08d3a 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.mlg @@ -12,6 +12,8 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) +{ + open Constrexpr open Constrexpr_ops open Stdarg @@ -57,22 +59,26 @@ let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: withtac; withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] + [ [ "with"; t = Tactic.tactic -> { Some t } + | -> { None } ] ] ; Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [CLocalAssum ([id], default_binder_kind, typ)] + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> { + let typ = mkAppC (sigref loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [CLocalAssum ([id], default_binder_kind, typ)] } ] ]; END +{ + open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac @@ -80,77 +86,81 @@ let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl +} + +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> - [ obligation (num, Some name, Some t) tac ] + { obligation (num, Some name, Some t) tac } | [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> - [ obligation (num, Some name, None) tac ] + { obligation (num, Some name, None) tac } | [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> - [ obligation (num, None, Some t) tac ] + { obligation (num, None, Some t) tac } | [ "Obligation" integer(num) withtac(tac) ] -> - [ obligation (num, None, None) tac ] + { obligation (num, None, None) tac } | [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] + { next_obligation (Some name) tac } +| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF | [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] + { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) } | [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] + { try_solve_obligation num None (Some (Tacinterp.interp t)) } END VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] + { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) } | [ "Solve" "Obligations" "with" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] + { try_solve_obligations None (Some (Tacinterp.interp t)) } | [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] + { try_solve_obligations None None } END VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF | [ "Solve" "All" "Obligations" "with" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] + { solve_all_obligations (Some (Tacinterp.interp t)) } | [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] + { solve_all_obligations None } END VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] +| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) } +| [ "Admit" "Obligations" ] -> { admit_obligations None } END -VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - fun ~atts ~st -> begin +VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> { let open Vernacinterp in set_default_tactic (Locality.make_section_locality atts.locality) (Tacintern.glob_tactic t); - st - end] + } END +{ + open Pp +} + VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY -| [ "Show" "Obligation" "Tactic" ] -> [ - Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] +| [ "Show" "Obligation" "Tactic" ] -> { + Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) } END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY -| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] -| [ "Obligations" ] -> [ show_obligations None ] +| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } +| [ "Obligations" ] -> { show_obligations None } END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ] +| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) } +| [ "Preterm" ] -> { Feedback.msg_info (show_term None) } END -open Pp +{ (* Declare a printer for the content of Program tactics *) let () = @@ -159,3 +169,5 @@ let () = | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac in Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer + +} diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.mlg index f1634f1561..3e47724c4c 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.mlg @@ -10,6 +10,8 @@ (* Syntax for rewriting with strategies *) +{ + open Names open Locus open Constrexpr @@ -25,8 +27,14 @@ open Pcoq.Constr open Pvernac.Vernac_ open Pltac +let wit_hyp = wit_var + +} + DECLARE PLUGIN "ltac_plugin" +{ + type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings @@ -43,19 +51,23 @@ let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings let subst_glob_constr_with_bindings s c = Tacsubst.subst_glob_with_bindings s c +} + ARGUMENT EXTEND glob_constr_with_bindings - PRINTED BY pr_glob_constr_with_bindings_sign + PRINTED BY { pr_glob_constr_with_bindings_sign } - INTERPRETED BY interp_glob_constr_with_bindings - GLOBALIZED BY glob_glob_constr_with_bindings - SUBSTITUTED BY subst_glob_constr_with_bindings + INTERPRETED BY { interp_glob_constr_with_bindings } + GLOBALIZED BY { glob_glob_constr_with_bindings } + SUBSTITUTED BY { subst_glob_constr_with_bindings } - RAW_PRINTED BY pr_constr_expr_with_bindings - GLOB_PRINTED BY pr_glob_constr_with_bindings + RAW_PRINTED BY { pr_constr_expr_with_bindings } + GLOB_PRINTED BY { pr_glob_constr_with_bindings } - [ constr_with_bindings(bl) ] -> [ bl ] +| [ constr_with_bindings(bl) ] -> { bl } END +{ + type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast @@ -78,53 +90,61 @@ let pr_glob_strategy prc prlc _ (s : glob_strategy) = in Rewrite.pr_strategy prc prr s +} + ARGUMENT EXTEND rewstrategy - PRINTED BY pr_strategy - - INTERPRETED BY interp_strategy - GLOBALIZED BY glob_strategy - SUBSTITUTED BY subst_strategy - - RAW_PRINTED BY pr_raw_strategy - GLOB_PRINTED BY pr_glob_strategy - - [ glob(c) ] -> [ StratConstr (c, true) ] - | [ "<-" constr(c) ] -> [ StratConstr (c, false) ] - | [ "subterms" rewstrategy(h) ] -> [ StratUnary (Subterms, h) ] - | [ "subterm" rewstrategy(h) ] -> [ StratUnary (Subterm, h) ] - | [ "innermost" rewstrategy(h) ] -> [ StratUnary(Innermost, h) ] - | [ "outermost" rewstrategy(h) ] -> [ StratUnary(Outermost, h) ] - | [ "bottomup" rewstrategy(h) ] -> [ StratUnary(Bottomup, h) ] - | [ "topdown" rewstrategy(h) ] -> [ StratUnary(Topdown, h) ] - | [ "id" ] -> [ StratId ] - | [ "fail" ] -> [ StratFail ] - | [ "refl" ] -> [ StratRefl ] - | [ "progress" rewstrategy(h) ] -> [ StratUnary (Progress, h) ] - | [ "try" rewstrategy(h) ] -> [ StratUnary (Try, h) ] - | [ "any" rewstrategy(h) ] -> [ StratUnary (Any, h) ] - | [ "repeat" rewstrategy(h) ] -> [ StratUnary (Repeat, h) ] - | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary (Compose, h, h') ] - | [ "(" rewstrategy(h) ")" ] -> [ h ] - | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary (Choice, h, h') ] - | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ] - | [ "hints" preident(h) ] -> [ StratHints (false, h) ] - | [ "terms" constr_list(h) ] -> [ StratTerms h ] - | [ "eval" red_expr(r) ] -> [ StratEval r ] - | [ "fold" constr(c) ] -> [ StratFold c ] + PRINTED BY { pr_strategy } + + INTERPRETED BY { interp_strategy } + GLOBALIZED BY { glob_strategy } + SUBSTITUTED BY { subst_strategy } + + RAW_PRINTED BY { pr_raw_strategy } + GLOB_PRINTED BY { pr_glob_strategy } + + | [ glob(c) ] -> { StratConstr (c, true) } + | [ "<-" constr(c) ] -> { StratConstr (c, false) } + | [ "subterms" rewstrategy(h) ] -> { StratUnary (Subterms, h) } + | [ "subterm" rewstrategy(h) ] -> { StratUnary (Subterm, h) } + | [ "innermost" rewstrategy(h) ] -> { StratUnary(Innermost, h) } + | [ "outermost" rewstrategy(h) ] -> { StratUnary(Outermost, h) } + | [ "bottomup" rewstrategy(h) ] -> { StratUnary(Bottomup, h) } + | [ "topdown" rewstrategy(h) ] -> { StratUnary(Topdown, h) } + | [ "id" ] -> { StratId } + | [ "fail" ] -> { StratFail } + | [ "refl" ] -> { StratRefl } + | [ "progress" rewstrategy(h) ] -> { StratUnary (Progress, h) } + | [ "try" rewstrategy(h) ] -> { StratUnary (Try, h) } + | [ "any" rewstrategy(h) ] -> { StratUnary (Any, h) } + | [ "repeat" rewstrategy(h) ] -> { StratUnary (Repeat, h) } + | [ rewstrategy(h) ";" rewstrategy(h') ] -> { StratBinary (Compose, h, h') } + | [ "(" rewstrategy(h) ")" ] -> { h } + | [ "choice" rewstrategy(h) rewstrategy(h') ] -> { StratBinary (Choice, h, h') } + | [ "old_hints" preident(h) ] -> { StratHints (true, h) } + | [ "hints" preident(h) ] -> { StratHints (false, h) } + | [ "terms" constr_list(h) ] -> { StratTerms h } + | [ "eval" red_expr(r) ] -> { StratEval r } + | [ "fold" constr(c) ] -> { StratFold c } END (* By default the strategy for "rewrite_db" is top-down *) +{ + let db_strat db = StratUnary (Topdown, StratHints (false, db)) let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) +} + TACTIC EXTEND rewrite_strat -| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] -| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ] -| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ] -| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ] +| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) } +| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None } +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) } +| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None } END +{ + let clsubstitute o c = Proofview.Goal.enter begin fun gl -> let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in @@ -137,59 +157,63 @@ let clsubstitute o c = (None :: List.map (fun id -> Some id) hyps) end +} + TACTIC EXTEND substitute -| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] +| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> { clsubstitute o c } END (* Compatibility with old Setoids *) TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] - -> [ cl_rewrite_clause c o AllOccurrences None ] + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] + -> { cl_rewrite_clause c o AllOccurrences None } | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ cl_rewrite_clause c o AllOccurrences (Some id) ] + { cl_rewrite_clause c o AllOccurrences (Some id) } | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> - [ cl_rewrite_clause c o (occurrences_of occ) None ] + { cl_rewrite_clause c o (occurrences_of occ) None } | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> - [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] + { cl_rewrite_clause c o (occurrences_of occ) (Some id) } | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> - [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] + { cl_rewrite_clause c o (occurrences_of occ) (Some id) } END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ] + { declare_relation a aeq n (Some lemma1) (Some lemma2) None } | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) None None ] + { declare_relation a aeq n (Some lemma1) None None } | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - [ declare_relation a aeq n None None None ] + { declare_relation a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation a aeq n None (Some lemma2) None ] + { declare_relation a aeq n None (Some lemma2) None } | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ] + { declare_relation a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ] + { declare_relation a aeq n (Some lemma1) None (Some lemma3) } | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] + { declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n None None (Some lemma3) ] + { declare_relation a aeq n None None (Some lemma3) } END +{ + type binders_argtype = local_binder_expr list let wit_binders = @@ -203,95 +227,92 @@ let () = open Pcoq -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: binders; binders: - [ [ b = Pcoq.Constr.binders -> b ] ]; + [ [ b = Pcoq.Constr.binders -> { b } ] ]; END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ] + { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None } | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) None None ] + { declare_relation ~binders:b a aeq n (Some lemma1) None None } | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None None None ] + { declare_relation ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None (Some lemma2) None ] + { declare_relation ~binders:b a aeq n None (Some lemma2) None } | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ] + { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ] + { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) } | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] + { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] + { declare_relation ~binders:b a aeq n None None (Some lemma3) } END -VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ fun ~atts ~st -> let open Vernacinterp in +VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF + | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { let open Vernacinterp in add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; - st - ] + } | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ fun ~atts ~st -> let open Vernacinterp in + { let open Vernacinterp in add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; - st - ] + } | [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ fun ~atts ~st -> let open Vernacinterp in + => { Vernacexpr.VtUnknown, Vernacexpr.VtNow } + -> { let open Vernacinterp in add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; - st - ] + } | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ fun ~atts ~st -> let open Vernacinterp in + => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + -> { let open Vernacinterp in add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; - st - ] + } | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ fun ~atts ~st -> let open Vernacinterp in + => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + -> { let open Vernacinterp in add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; - st - ] + } END TACTIC EXTEND setoid_symmetry - [ "setoid_symmetry" ] -> [ setoid_symmetry ] - | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] + | [ "setoid_symmetry" ] -> { setoid_symmetry } + | [ "setoid_symmetry" "in" hyp(n) ] -> { setoid_symmetry_in n } END TACTIC EXTEND setoid_reflexivity -[ "setoid_reflexivity" ] -> [ setoid_reflexivity ] +| [ "setoid_reflexivity" ] -> { setoid_reflexivity } END TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] -| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] +| [ "setoid_transitivity" constr(t) ] -> { setoid_transitivity (Some t) } +| [ "setoid_etransitivity" ] -> { setoid_transitivity None } END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> - [ let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] +| [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) } END diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index ec96e1bbdd..e83eab20dc 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -7,10 +7,10 @@ Pltac Taccoerce Tactic_debug Tacintern -Tacentries Profile_ltac Tactic_matching Tacinterp +Tacentries Evar_tactics Tactic_option Extraargs diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.mlg index 983e1578be..2713819c7b 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -8,13 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + (** Ltac profiling entrypoints *) open Profile_ltac open Stdarg +} + DECLARE PLUGIN "ltac_plugin" +{ + let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) @@ -33,42 +39,44 @@ let tclRESTART_TIMER s = let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) +} + TACTIC EXTEND start_ltac_profiling -| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] +| [ "start" "ltac" "profiling" ] -> { tclSET_PROFILING true } END TACTIC EXTEND stop_ltac_profiling -| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] +| [ "stop" "ltac" "profiling" ] -> { tclSET_PROFILING false } END TACTIC EXTEND reset_ltac_profile -| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ] +| [ "reset" "ltac" "profile" ] -> { tclRESET_PROFILE } END TACTIC EXTEND show_ltac_profile -| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ] -| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ] -| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ] +| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff } +| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } +| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s } END TACTIC EXTEND restart_timer -| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ] +| [ "restart_timer" string_opt(s) ] -> { tclRESTART_TIMER s } END TACTIC EXTEND finish_timing -| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ] -| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ] +| [ "finish_timing" string_opt(s) ] -> { tclFINISH_TIMING ~prefix:"Timer" s } +| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> { tclFINISH_TIMING ~prefix s } END VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ] +| [ "Reset" "Ltac" "Profile" ] -> { reset_profile () } END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] -| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] +| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff } +| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) } END VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY - [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] +| [ "Show" "Ltac" "Profile" string(s) ] -> { print_results_tactic s } END diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a77a9c2f45..16cff420bd 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -673,3 +673,96 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name + + +(** ARGUMENT EXTEND *) + +open Geninterp + +type ('a, 'b, 'c) argument_printer = + 'a Pptactic.raw_extra_genarg_printer * + 'b Pptactic.glob_extra_genarg_printer * + 'c Pptactic.extra_genarg_printer + +type ('a, 'b) argument_intern = +| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern +| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern + +type 'b argument_subst = +| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst +| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst + +type ('b, 'c) argument_interp = +| ArgInterpRet : ('c, 'c) argument_interp +| ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp +| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp +| ArgInterpLegacy : + (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + +type ('a, 'b, 'c) tactic_argument = { + arg_parsing : 'a Vernacentries.argument_rule; + arg_tag : 'c Val.tag option; + arg_intern : ('a, 'b) argument_intern; + arg_subst : 'b argument_subst; + arg_interp : ('b, 'c) argument_interp; + arg_printer : ('a, 'b, 'c) argument_printer; +} + +let intern_fun (type a b c) name (arg : (a, b, c) tactic_argument) : (a, b) Genintern.intern_fun = +match arg.arg_intern with +| ArgInternFun f -> f +| ArgInternWit wit -> + fun ist v -> + let ans = Genarg.out_gen (glbwit wit) (Tacintern.intern_genarg ist (Genarg.in_gen (rawwit wit) v)) in + (ist, ans) + +let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Genintern.subst_fun = +match arg.arg_subst with +| ArgSubstFun f -> f +| ArgSubstWit wit -> + fun s v -> + let ans = Genarg.out_gen (glbwit wit) (Tacsubst.subst_genarg s (Genarg.in_gen (glbwit wit) v)) in + ans + +let interp_fun (type a b c) name (arg : (a, b, c) tactic_argument) (tag : c Val.tag) : (b, Val.t) interp_fun = +match arg.arg_interp with +| ArgInterpRet -> (fun ist v -> Ftactic.return (Geninterp.Val.inject tag v)) +| ArgInterpFun f -> f +| ArgInterpWit wit -> + (fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen (glbwit wit) x)) +| ArgInterpLegacy f -> + (fun ist v -> Ftactic.enter (fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject tag v in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) + )) + +let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = + let wit = Genarg.create_arg name in + let () = Genintern.register_intern0 wit (intern_fun name arg) in + let () = Genintern.register_subst0 wit (subst_fun arg) in + let tag = match arg.arg_tag with + | None -> + let () = register_val0 wit None in + val_tag (topwit wit) + | Some tag -> + let () = register_val0 wit (Some tag) in + tag + in + let () = register_interp0 wit (interp_fun name arg tag) in + let entry = match arg.arg_parsing with + | Vernacentries.Arg_alias e -> + let () = Pcoq.register_grammar wit e in + e + | Vernacentries.Arg_rules rules -> + let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in + let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + e + in + let (rpr, gpr, tpr) = arg.arg_printer in + let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in + let () = create_ltac_quotation name + (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v)) + (entry, None) + in + (wit, entry) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 0b2b426018..5b4bedb50a 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -70,6 +70,8 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +(** {5 TACTIC EXTEND} *) + type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig @@ -79,3 +81,60 @@ type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml val tactic_extend : string -> string -> level:Int.t -> ?deprecation:deprecation -> ty_ml list -> unit + +(** {5 ARGUMENT EXTEND} *) + +(** + + This is the main entry point for the ARGUMENT EXTEND macro that allows to + easily create user-made Ltac arguments. + + + Each argument has three type parameters. See {!Genarg} for more details. + There are two kinds of Ltac arguments, uniform and non-uniform. The former + have the same type at each level (raw, glob, top) while the latter may vary. + + When declaring an argument one must provide the following data: + - Internalization : raw -> glob + - Substitution : glob -> glob + - Interpretation : glob -> Ltac dynamic value + - Printing for every level + - An optional toplevel tag of type top (with the proviso that the + interpretation function only produces values with this tag) + + This data can be either given explicitly with the [Fun] constructors, or it + can be inherited from another argument with the [Wit] constructors. + +*) + +type ('a, 'b, 'c) argument_printer = + 'a Pptactic.raw_extra_genarg_printer * + 'b Pptactic.glob_extra_genarg_printer * + 'c Pptactic.extra_genarg_printer + +type ('a, 'b) argument_intern = +| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern +| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern + +type 'b argument_subst = +| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst +| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst + +type ('b, 'c) argument_interp = +| ArgInterpRet : ('c, 'c) argument_interp +| ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp +| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp +| ArgInterpLegacy : + (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + +type ('a, 'b, 'c) tactic_argument = { + arg_parsing : 'a Vernacentries.argument_rule; + arg_tag : 'c Geninterp.Val.tag option; + arg_intern : ('a, 'b) argument_intern; + arg_subst : 'b argument_subst; + arg_interp : ('b, 'c) argument_interp; + arg_printer : ('a, 'b, 'c) argument_printer; +} + +val argument_extend : name:string -> ('a, 'b, 'c) tactic_argument -> + ('a, 'b, 'c) Genarg.genarg_type * 'a Pcoq.Entry.t diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.mlg index 4ea0b30bd7..3ddea7eb30 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Pp open Util @@ -20,15 +22,19 @@ open Tacarg open Pcoq.Constr open Pltac +} + DECLARE PLUGIN "newring_plugin" TACTIC EXTEND protect_fv - [ "protect_fv" string(map) "in" ident(id) ] -> - [ protect_tac_in map id ] +| [ "protect_fv" string(map) "in" ident(id) ] -> + { protect_tac_in map id } | [ "protect_fv" string(map) ] -> - [ protect_tac map ] + { protect_tac map } END +{ + open Pptactic open Ppconstr @@ -46,35 +52,41 @@ let pr_ring_mod = function | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t +} + VERNAC ARGUMENT EXTEND ring_mod - PRINTED BY pr_ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] - | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] - | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] - | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] - | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] - | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] - | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] - | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] + PRINTED BY { pr_ring_mod } + | [ "decidable" constr(eq_test) ] -> { Ring_kind(Computational eq_test) } + | [ "abstract" ] -> { Ring_kind Abstract } + | [ "morphism" constr(morph) ] -> { Ring_kind(Morphism morph) } + | [ "constants" "[" tactic(cst_tac) "]" ] -> { Const_tac(CstTac cst_tac) } + | [ "closed" "[" ne_global_list(l) "]" ] -> { Const_tac(Closed l) } + | [ "preprocess" "[" tactic(pre) "]" ] -> { Pre_tac pre } + | [ "postprocess" "[" tactic(post) "]" ] -> { Post_tac post } + | [ "setoid" constr(sth) constr(ext) ] -> { Setoid(sth,ext) } + | [ "sign" constr(sign_spec) ] -> { Sign_spec sign_spec } | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> - [ Pow_spec (Closed l, pow_spec) ] + { Pow_spec (Closed l, pow_spec) } | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> - [ Pow_spec (CstTac cst_tac, pow_spec) ] - | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] + { Pow_spec (CstTac cst_tac, pow_spec) } + | [ "div" constr(div_spec) ] -> { Div_spec div_spec } END +{ + let pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l) +} + VERNAC ARGUMENT EXTEND ring_mods - PRINTED BY pr_ring_mods - | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ] + PRINTED BY { pr_ring_mods } + | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods } END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> - [ let l = match l with None -> [] | Some l -> l in add_theory id t l] - | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ + { let l = match l with None -> [] | Some l -> l in add_theory id t l } + | [ "Print" "Rings" ] => {Vernac_classifier.classify_as_query} -> { Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> let sigma, env = Pfedit.get_current_context () in @@ -82,35 +94,43 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name ] + ) !from_name } END TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ] + { let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t } END +{ + let pr_field_mod = function | Ring_mod m -> pr_ring_mod m | Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj +} + VERNAC ARGUMENT EXTEND field_mod - PRINTED BY pr_field_mod - | [ ring_mod(m) ] -> [ Ring_mod m ] - | [ "completeness" constr(inj) ] -> [ Inject inj ] + PRINTED BY { pr_field_mod } + | [ ring_mod(m) ] -> { Ring_mod m } + | [ "completeness" constr(inj) ] -> { Inject inj } END +{ + let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l) +} + VERNAC ARGUMENT EXTEND field_mods - PRINTED BY pr_field_mods - | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ] + PRINTED BY { pr_field_mods } + | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods } END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> - [ let l = match l with None -> [] | Some l -> l in add_field_theory id t l ] -| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ + { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } +| [ "Print" "Fields" ] => {Vernac_classifier.classify_as_query} -> { Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> let sigma, env = Pfedit.get_current_context () in @@ -118,10 +138,10 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name ] + ) !field_from_name } END TACTIC EXTEND field_lookup | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] + { let (t,l) = List.sep_last lt in field_lookup f lH l t } END diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.mlg index e4a0910673..8699b62c39 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.mlg @@ -10,12 +10,13 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +{ + let _vmcast = Constr.VMcast open Names open Pp open Pcoq open Ltac_plugin -open Genarg open Stdarg open Tacarg open Libnames @@ -61,7 +62,12 @@ let is_ssr_loaded () = (if CLexer.is_keyword "SsrSyntax_is_Imported" then ssr_loaded:=true; !ssr_loaded) +} + DECLARE PLUGIN "ssreflect_plugin" + +{ + (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; @@ -69,21 +75,31 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let tacltop = (5,Notation_gram.E) let pr_ssrtacarg _ _ prt = prt tacltop -ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg -| [ "YouShouldNotTypeThis" ] -> [ CErrors.anomaly (Pp.str "Grammar placeholder match") ] + +} + +ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg } +| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; - ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> tac ]]; + ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]]; END +{ + (* Lexically closed tactic for tacticals. *) let pr_ssrtclarg _ _ prt tac = prt tacltop tac + +} + ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg - PRINTED BY pr_ssrtclarg -| [ ssrtacarg(tac) ] -> [ tac ] + PRINTED BY { pr_ssrtclarg } +| [ ssrtacarg(tac) ] -> { tac } END +{ + open Genarg (** Adding a new uninterpreted generic argument type *) @@ -139,12 +155,15 @@ let intern_hyp ist (SsrHyp (loc, id) as hyp) = open Pcoq.Prim -ARGUMENT EXTEND ssrhyp TYPED AS ssrhyprep PRINTED BY pr_ssrhyp - INTERPRETED BY interp_hyp - GLOBALIZED BY intern_hyp - | [ ident(id) ] -> [ SsrHyp (Loc.tag ~loc id) ] +} + +ARGUMENT EXTEND ssrhyp TYPED AS ssrhyprep PRINTED BY { pr_ssrhyp } + INTERPRETED BY { interp_hyp } + GLOBALIZED BY { intern_hyp } + | [ ident(id) ] -> { SsrHyp (Loc.tag ~loc id) } END +{ let pr_hoi = hoik pr_hyp let pr_ssrhoi _ _ _ = pr_hoi @@ -163,27 +182,33 @@ let interp_ssrhoi ist gl = function let s, id' = interp_wit wit_ident ist gl id in s, Id (SsrHyp (loc, id')) -ARGUMENT EXTEND ssrhoi_hyp TYPED AS ssrhoirep PRINTED BY pr_ssrhoi - INTERPRETED BY interp_ssrhoi - GLOBALIZED BY intern_ssrhoi - | [ ident(id) ] -> [ Hyp (SsrHyp(Loc.tag ~loc id)) ] +} + +ARGUMENT EXTEND ssrhoi_hyp TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi } + INTERPRETED BY { interp_ssrhoi } + GLOBALIZED BY { intern_ssrhoi } + | [ ident(id) ] -> { Hyp (SsrHyp(Loc.tag ~loc id)) } END -ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY pr_ssrhoi - INTERPRETED BY interp_ssrhoi - GLOBALIZED BY intern_ssrhoi - | [ ident(id) ] -> [ Id (SsrHyp(Loc.tag ~loc id)) ] +ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi } + INTERPRETED BY { interp_ssrhoi } + GLOBALIZED BY { intern_ssrhoi } + | [ ident(id) ] -> { Id (SsrHyp(Loc.tag ~loc id)) } END +{ let pr_ssrhyps _ _ _ = pr_hyps -ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY pr_ssrhyps - INTERPRETED BY interp_hyps - | [ ssrhyp_list(hyps) ] -> [ check_hyps_uniq [] hyps; hyps ] +} + +ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY { pr_ssrhyps } + INTERPRETED BY { interp_hyps } + | [ ssrhyp_list(hyps) ] -> { check_hyps_uniq [] hyps; hyps } END (** Rewriting direction *) +{ let pr_rwdir = function L2R -> mt() | R2L -> str "-" @@ -254,43 +279,46 @@ let test_ssrslashnum11 = let test_ssrslashnum01 = Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 +} -ARGUMENT EXTEND ssrsimpl_ne TYPED AS ssrsimplrep PRINTED BY pr_ssrsimpl -| [ "//=" ] -> [ SimplCut (~-1,~-1) ] -| [ "/=" ] -> [ Simpl ~-1 ] +ARGUMENT EXTEND ssrsimpl_ne TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl } +| [ "//=" ] -> { SimplCut (~-1,~-1) } +| [ "/=" ] -> { Simpl ~-1 } END -Pcoq.(Prim.( -GEXTEND Gram +(* Pcoq.Prim. *) +GRAMMAR EXTEND Gram GLOBAL: ssrsimpl_ne; ssrsimpl_ne: [ - [ test_ssrslashnum11; "/"; n = natural; "/"; m = natural; "=" -> SimplCut(n,m) - | test_ssrslashnum10; "/"; n = natural; "/" -> Cut n - | test_ssrslashnum10; "/"; n = natural; "=" -> Simpl n - | test_ssrslashnum10; "/"; n = natural; "/=" -> SimplCut (n,~-1) - | test_ssrslashnum10; "/"; n = natural; "/"; "=" -> SimplCut (n,~-1) - | test_ssrslashnum01; "//"; m = natural; "=" -> SimplCut (~-1,m) - | test_ssrslashnum00; "//" -> Cut ~-1 + [ test_ssrslashnum11; "/"; n = natural; "/"; m = natural; "=" -> { SimplCut(n,m) } + | test_ssrslashnum10; "/"; n = natural; "/" -> { Cut n } + | test_ssrslashnum10; "/"; n = natural; "=" -> { Simpl n } + | test_ssrslashnum10; "/"; n = natural; "/=" -> { SimplCut (n,~-1) } + | test_ssrslashnum10; "/"; n = natural; "/"; "=" -> { SimplCut (n,~-1) } + | test_ssrslashnum01; "//"; m = natural; "=" -> { SimplCut (~-1,m) } + | test_ssrslashnum00; "//" -> { Cut ~-1 } ]]; END -)) -ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY pr_ssrsimpl -| [ ssrsimpl_ne(sim) ] -> [ sim ] -| [ ] -> [ Nop ] +ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl } +| [ ssrsimpl_ne(sim) ] -> { sim } +| [ ] -> { Nop } END +{ let pr_ssrclear _ _ _ = pr_clear mt -ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyps PRINTED BY pr_ssrclear -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ check_hyps_uniq [] clr; clr ] +} + +ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyps PRINTED BY { pr_ssrclear } +| [ "{" ne_ssrhyp_list(clr) "}" ] -> { check_hyps_uniq [] clr; clr } END -ARGUMENT EXTEND ssrclear TYPED AS ssrclear_ne PRINTED BY pr_ssrclear -| [ ssrclear_ne(clr) ] -> [ clr ] -| [ ] -> [ [] ] +ARGUMENT EXTEND ssrclear TYPED AS ssrclear_ne PRINTED BY { pr_ssrclear } +| [ ssrclear_ne(clr) ] -> { clr } +| [ ] -> { [] } END (** Indexes *) @@ -301,6 +329,7 @@ END (* positive values, and allows the use of constr numerals, so that *) (* e.g., "let n := eval compute in (1 + 3) in (do n!clear)" works. *) +{ let pr_index = function | ArgVar {CAst.v=id} -> pr_id id @@ -342,9 +371,11 @@ let interp_index ist gl idx = open Pltac -ARGUMENT EXTEND ssrindex PRINTED BY pr_ssrindex - INTERPRETED BY interp_index -| [ int_or_var(i) ] -> [ mk_index ~loc i ] +} + +ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex } + INTERPRETED BY { interp_index } +| [ int_or_var(i) ] -> { mk_index ~loc i } END @@ -360,49 +391,61 @@ END (* default, but "{-}" prevents the implicit clear, and can be used to *) (* force dependent elimination -- see ndefectelimtac below. *) +{ let pr_ssrocc _ _ _ = pr_occ open Pcoq.Prim -ARGUMENT EXTEND ssrocc TYPED AS (bool * int list) option PRINTED BY pr_ssrocc -| [ natural(n) natural_list(occ) ] -> [ - Some (false, List.map (check_index ~loc) (n::occ)) ] -| [ "-" natural_list(occ) ] -> [ Some (true, occ) ] -| [ "+" natural_list(occ) ] -> [ Some (false, occ) ] +} + +ARGUMENT EXTEND ssrocc TYPED AS (bool * int list) option PRINTED BY { pr_ssrocc } +| [ natural(n) natural_list(occ) ] -> { + Some (false, List.map (check_index ~loc) (n::occ)) } +| [ "-" natural_list(occ) ] -> { Some (true, occ) } +| [ "+" natural_list(occ) ] -> { Some (false, occ) } END (* modality *) +{ let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt () let wit_ssrmmod = add_genarg "ssrmmod" pr_mmod let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);; -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: ssrmmod; - ssrmmod: [[ "!" -> Must | LEFTQMARK -> May | "?" -> May]]; + ssrmmod: [[ "!" -> { Must } | LEFTQMARK -> { May } | "?" -> { May } ]]; END (** Rewrite multiplier: !n ?n *) +{ + let pr_mult (n, m) = if n > 0 && m <> Once then int n ++ pr_mmod m else pr_mmod m let pr_ssrmult _ _ _ = pr_mult -ARGUMENT EXTEND ssrmult_ne TYPED AS int * ssrmmod PRINTED BY pr_ssrmult - | [ natural(n) ssrmmod(m) ] -> [ check_index ~loc n, m ] - | [ ssrmmod(m) ] -> [ notimes, m ] +} + +ARGUMENT EXTEND ssrmult_ne TYPED AS (int * ssrmmod) PRINTED BY { pr_ssrmult } + | [ natural(n) ssrmmod(m) ] -> { check_index ~loc n, m } + | [ ssrmmod(m) ] -> { notimes, m } END -ARGUMENT EXTEND ssrmult TYPED AS ssrmult_ne PRINTED BY pr_ssrmult - | [ ssrmult_ne(m) ] -> [ m ] - | [ ] -> [ nomult ] +ARGUMENT EXTEND ssrmult TYPED AS ssrmult_ne PRINTED BY { pr_ssrmult } + | [ ssrmult_ne(m) ] -> { m } + | [ ] -> { nomult } END +{ + (** Discharge occ switch (combined occurrence / clear switch *) let pr_docc = function @@ -411,11 +454,15 @@ let pr_docc = function let pr_ssrdocc _ _ _ = pr_docc -ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc -| [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] -| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] +} + +ARGUMENT EXTEND ssrdocc TYPED AS (ssrclear option * ssrocc) PRINTED BY { pr_ssrdocc } +| [ "{" ssrocc(occ) "}" ] -> { mkocc occ } +| [ "{" ssrhyp_list(clr) "}" ] -> { mkclr clr } END +{ + (* Old kinds of terms *) let input_ssrtermkind strm = match Util.stream_nth 0 strm with @@ -458,90 +505,99 @@ let interp_ssrterm _ gl t = Tacmach.project gl, t open Pcoq.Constr +} + ARGUMENT EXTEND ssrterm - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_ssrterm SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "YouShouldNotTypeThis" constr(c) ] -> [ mk_lterm c ] + PRINTED BY { pr_ssrterm } + INTERPRETED BY { interp_ssrterm } + GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm } + RAW_PRINTED BY { pr_ssrterm } + GLOB_PRINTED BY { pr_ssrterm } +| [ "YouShouldNotTypeThis" constr(c) ] -> { mk_lterm c } END - -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssrterm; - ssrterm: [[ k = ssrtermkind; c = Pcoq.Constr.constr -> mk_term k c ]]; + ssrterm: [[ k = ssrtermkind; c = Pcoq.Constr.constr -> { mk_term k c } ]]; END (* New terms *) +{ + let pp_ast_closure_term _ _ _ = pr_ast_closure_term +} + ARGUMENT EXTEND ast_closure_term - PRINTED BY pp_ast_closure_term - INTERPRETED BY interp_ast_closure_term - GLOBALIZED BY glob_ast_closure_term - SUBSTITUTED BY subst_ast_closure_term - RAW_PRINTED BY pp_ast_closure_term - GLOB_PRINTED BY pp_ast_closure_term - | [ term_annotation(a) constr(c) ] -> [ mk_ast_closure_term a c ] + PRINTED BY { pp_ast_closure_term } + INTERPRETED BY { interp_ast_closure_term } + GLOBALIZED BY { glob_ast_closure_term } + SUBSTITUTED BY { subst_ast_closure_term } + RAW_PRINTED BY { pp_ast_closure_term } + GLOB_PRINTED BY { pp_ast_closure_term } + | [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c } END ARGUMENT EXTEND ast_closure_lterm - PRINTED BY pp_ast_closure_term - INTERPRETED BY interp_ast_closure_term - GLOBALIZED BY glob_ast_closure_term - SUBSTITUTED BY subst_ast_closure_term - RAW_PRINTED BY pp_ast_closure_term - GLOB_PRINTED BY pp_ast_closure_term - | [ term_annotation(a) lconstr(c) ] -> [ mk_ast_closure_term a c ] + PRINTED BY { pp_ast_closure_term } + INTERPRETED BY { interp_ast_closure_term } + GLOBALIZED BY { glob_ast_closure_term } + SUBSTITUTED BY { subst_ast_closure_term } + RAW_PRINTED BY { pp_ast_closure_term } + GLOB_PRINTED BY { pp_ast_closure_term } + | [ term_annotation(a) lconstr(c) ] -> { mk_ast_closure_term a c } END (* Old Views *) +{ + let pr_view = pr_list mt (fun c -> str "/" ++ pr_term c) let pr_ssrbwdview _ _ _ = pr_view +} + ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list - PRINTED BY pr_ssrbwdview -| [ "YouShouldNotTypeThis" ] -> [ [] ] + PRINTED BY { pr_ssrbwdview } +| [ "YouShouldNotTypeThis" ] -> { [] } END -Pcoq.( -GEXTEND Gram +(* Pcoq *) +GRAMMAR EXTEND Gram GLOBAL: ssrbwdview; ssrbwdview: [ - [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> [mk_term xNoFlag c] - | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview -> - (mk_term xNoFlag c) :: w ]]; + [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term xNoFlag c] } + | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview -> { + (mk_term xNoFlag c) :: w } ]]; END -) (* New Views *) +{ let pr_ssrfwdview _ _ _ = pr_view2 +} + ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list - PRINTED BY pr_ssrfwdview -| [ "YouShouldNotTypeThis" ] -> [ [] ] + PRINTED BY { pr_ssrfwdview } +| [ "YouShouldNotTypeThis" ] -> { [] } END -Pcoq.( -GEXTEND Gram +(* Pcoq *) +GRAMMAR EXTEND Gram GLOBAL: ssrfwdview; ssrfwdview: [ [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> - [mk_ast_closure_term `None c] + { [mk_ast_closure_term `None c] } | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview -> - (mk_ast_closure_term `None c) :: w ]]; + { (mk_ast_closure_term `None c) :: w } ]]; END -) -(* }}} *) - (* ipats *) +{ let remove_loc x = x.CAst.v @@ -663,75 +719,79 @@ let pushIPatNoop = function | pats :: orpat -> (IPatNoop :: pats) :: orpat | [] -> [] -ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats - INTERPRETED BY interp_ipats - GLOBALIZED BY intern_ipats - | [ "_" ] -> [ [IPatAnon Drop] ] - | [ "*" ] -> [ [IPatAnon All] ] +} + +ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } + INTERPRETED BY { interp_ipats } + GLOBALIZED BY { intern_ipats } + | [ "_" ] -> { [IPatAnon Drop] } + | [ "*" ] -> { [IPatAnon All] } (* - | [ "^" "*" ] -> [ [IPatFastMode] ] - | [ "^" "_" ] -> [ [IPatSeed `Wild] ] - | [ "^_" ] -> [ [IPatSeed `Wild] ] - | [ "^" "?" ] -> [ [IPatSeed `Anon] ] - | [ "^?" ] -> [ [IPatSeed `Anon] ] - | [ "^" ident(id) ] -> [ [IPatSeed (`Id(id,`Pre))] ] - | [ "^" "~" ident(id) ] -> [ [IPatSeed (`Id(id,`Post))] ] - | [ "^~" ident(id) ] -> [ [IPatSeed (`Id(id,`Post))] ] + | [ "^" "*" ] -> { [IPatFastMode] } + | [ "^" "_" ] -> { [IPatSeed `Wild] } + | [ "^_" ] -> { [IPatSeed `Wild] } + | [ "^" "?" ] -> { [IPatSeed `Anon] } + | [ "^?" ] -> { [IPatSeed `Anon] } + | [ "^" ident(id) ] -> { [IPatSeed (`Id(id,`Pre))] } + | [ "^" "~" ident(id) ] -> { [IPatSeed (`Id(id,`Post))] } + | [ "^~" ident(id) ] -> { [IPatSeed (`Id(id,`Post))] } *) - | [ ident(id) ] -> [ [IPatId id] ] - | [ "?" ] -> [ [IPatAnon One] ] + | [ ident(id) ] -> { [IPatId id] } + | [ "?" ] -> { [IPatAnon One] } (* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) - | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ] - | [ ssrdocc(occ) "->" ] -> [ match occ with + | [ ssrsimpl_ne(sim) ] -> { [IPatSimpl sim] } + | [ ssrdocc(occ) "->" ] -> { match occ with | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, L2R)] - | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]] - | [ ssrdocc(occ) "<-" ] -> [ match occ with + | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)] } + | [ ssrdocc(occ) "<-" ] -> { match occ with | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] - | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]] - | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with + | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] } + | [ ssrdocc(occ) ssrfwdview(v) ] -> { match occ with | Some [], _ -> [IPatView (true,v)] | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] - | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ] - | [ ssrdocc(occ) ] -> [ match occ with + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } + | [ ssrdocc(occ) ] -> { match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] - | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")] - | [ "->" ] -> [ [IPatRewrite (allocc, L2R)] ] - | [ "<-" ] -> [ [IPatRewrite (allocc, R2L)] ] - | [ "-" ] -> [ [IPatNoop] ] - | [ "-/" "=" ] -> [ [IPatNoop;IPatSimpl(Simpl ~-1)] ] - | [ "-/=" ] -> [ [IPatNoop;IPatSimpl(Simpl ~-1)] ] - | [ "-/" "/" ] -> [ [IPatNoop;IPatSimpl(Cut ~-1)] ] - | [ "-//" ] -> [ [IPatNoop;IPatSimpl(Cut ~-1)] ] - | [ "-/" integer(n) "/" ] -> [ [IPatNoop;IPatSimpl(Cut n)] ] - | [ "-/" "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] ] - | [ "-//" "=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] ] - | [ "-//=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] ] - | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ] + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } + | [ "->" ] -> { [IPatRewrite (allocc, L2R)] } + | [ "<-" ] -> { [IPatRewrite (allocc, R2L)] } + | [ "-" ] -> { [IPatNoop] } + | [ "-/" "=" ] -> { [IPatNoop;IPatSimpl(Simpl ~-1)] } + | [ "-/=" ] -> { [IPatNoop;IPatSimpl(Simpl ~-1)] } + | [ "-/" "/" ] -> { [IPatNoop;IPatSimpl(Cut ~-1)] } + | [ "-//" ] -> { [IPatNoop;IPatSimpl(Cut ~-1)] } + | [ "-/" integer(n) "/" ] -> { [IPatNoop;IPatSimpl(Cut n)] } + | [ "-/" "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] } + | [ "-//" "=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] } + | [ "-//=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] } + | [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] } | [ "-/" integer(n) "/" integer (m) "=" ] -> - [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ] - | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ] - | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] - | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] + { [IPatNoop;IPatSimpl(SimplCut(n,m))] } + | [ ssrfwdview(v) ] -> { [IPatView (false,v)] } + | [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } + | [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } END -ARGUMENT EXTEND ssripats TYPED AS ssripat PRINTED BY pr_ssripats - | [ ssripat(i) ssripats(tl) ] -> [ i @ tl ] - | [ ] -> [ [] ] +ARGUMENT EXTEND ssripats TYPED AS ssripat PRINTED BY { pr_ssripats } + | [ ssripat(i) ssripats(tl) ] -> { i @ tl } + | [ ] -> { [] } END -ARGUMENT EXTEND ssriorpat TYPED AS ssripat list PRINTED BY pr_ssriorpat -| [ ssripats(pats) "|" ssriorpat(orpat) ] -> [ pats :: orpat ] -| [ ssripats(pats) "|-" ">" ssriorpat(orpat) ] -> [ pats :: pushIPatRewrite orpat ] -| [ ssripats(pats) "|-" ssriorpat(orpat) ] -> [ pats :: pushIPatNoop orpat ] -| [ ssripats(pats) "|->" ssriorpat(orpat) ] -> [ pats :: pushIPatRewrite orpat ] -| [ ssripats(pats) "||" ssriorpat(orpat) ] -> [ pats :: [] :: orpat ] -| [ ssripats(pats) "|||" ssriorpat(orpat) ] -> [ pats :: [] :: [] :: orpat ] -| [ ssripats(pats) "||||" ssriorpat(orpat) ] -> [ [pats; []; []; []] @ orpat ] -| [ ssripats(pats) ] -> [ [pats] ] +ARGUMENT EXTEND ssriorpat TYPED AS ssripat list PRINTED BY { pr_ssriorpat } +| [ ssripats(pats) "|" ssriorpat(orpat) ] -> { pats :: orpat } +| [ ssripats(pats) "|-" ">" ssriorpat(orpat) ] -> { pats :: pushIPatRewrite orpat } +| [ ssripats(pats) "|-" ssriorpat(orpat) ] -> { pats :: pushIPatNoop orpat } +| [ ssripats(pats) "|->" ssriorpat(orpat) ] -> { pats :: pushIPatRewrite orpat } +| [ ssripats(pats) "||" ssriorpat(orpat) ] -> { pats :: [] :: orpat } +| [ ssripats(pats) "|||" ssriorpat(orpat) ] -> { pats :: [] :: [] :: orpat } +| [ ssripats(pats) "||||" ssriorpat(orpat) ] -> { [pats; []; []; []] @ orpat } +| [ ssripats(pats) ] -> { [pats] } END +{ + let reject_ssrhid strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "[" -> @@ -742,43 +802,44 @@ let reject_ssrhid strm = let test_nohidden = Pcoq.Gram.Entry.of_parser "test_ssrhid" reject_ssrhid -ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY pr_ssripat - | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> [ IPatCase(x) ] +} + +ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat } + | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(x) } END -Pcoq.( -GEXTEND Gram +(* Pcoq *) +GRAMMAR EXTEND Gram GLOBAL: ssrcpat; ssrcpat: [ - [ test_nohidden; "["; iorpat = ssriorpat; "]" -> + [ test_nohidden; "["; iorpat = ssriorpat; "]" -> { (* check_no_inner_seed !@loc false iorpat; IPatCase (understand_case_type iorpat) *) - IPatCase iorpat + IPatCase iorpat } (* | test_nohidden; "("; iorpat = ssriorpat; ")" -> (* check_no_inner_seed !@loc false iorpat; IPatCase (understand_case_type iorpat) *) IPatDispatch iorpat *) - | test_nohidden; "[="; iorpat = ssriorpat; "]" -> + | test_nohidden; "[="; iorpat = ssriorpat; "]" -> { (* check_no_inner_seed !@loc false iorpat; *) - IPatInj iorpat ]]; + IPatInj iorpat } ]]; END -);; -Pcoq.( -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssripat; - ssripat: [[ pat = ssrcpat -> [pat] ]]; + ssripat: [[ pat = ssrcpat -> { [pat] } ]]; END -) -ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY pr_ssripats - | [ ssripat(i) ssripats(tl) ] -> [ i @ tl ] +ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY { pr_ssripats } + | [ ssripat(i) ssripats(tl) ] -> { i @ tl } END (* subsets of patterns *) +{ + (* TODO: review what this function does, it looks suspicious *) let check_ssrhpats loc w_binders ipats = let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in @@ -816,80 +877,97 @@ let pr_hpats (((clr, ipat), binders), simpl) = let pr_ssrhpats _ _ _ = pr_hpats let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x -ARGUMENT EXTEND ssrhpats TYPED AS ((ssrclear * ssripat) * ssripat) * ssripat -PRINTED BY pr_ssrhpats - | [ ssripats(i) ] -> [ check_ssrhpats loc true i ] +} + +ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear * ssripat) * ssripat) * ssripat) +PRINTED BY { pr_ssrhpats } + | [ ssripats(i) ] -> { check_ssrhpats loc true i } END ARGUMENT EXTEND ssrhpats_wtransp - TYPED AS bool * (((ssrclear * ssripats) * ssripats) * ssripats) - PRINTED BY pr_ssrhpats_wtransp - | [ ssripats(i) ] -> [ false,check_ssrhpats loc true i ] - | [ ssripats(i) "@" ssripats(j) ] -> [ true,check_ssrhpats loc true (i @ j) ] + TYPED AS (bool * (((ssrclear * ssripats) * ssripats) * ssripats)) + PRINTED BY { pr_ssrhpats_wtransp } + | [ ssripats(i) ] -> { false,check_ssrhpats loc true i } + | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) } END ARGUMENT EXTEND ssrhpats_nobs -TYPED AS ((ssrclear * ssripats) * ssripats) * ssripats PRINTED BY pr_ssrhpats - | [ ssripats(i) ] -> [ check_ssrhpats loc false i ] +TYPED AS (((ssrclear * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } + | [ ssripats(i) ] -> { check_ssrhpats loc false i } END -ARGUMENT EXTEND ssrrpat TYPED AS ssripatrep PRINTED BY pr_ssripat - | [ "->" ] -> [ IPatRewrite (allocc, L2R) ] - | [ "<-" ] -> [ IPatRewrite (allocc, R2L) ] +ARGUMENT EXTEND ssrrpat TYPED AS ssripatrep PRINTED BY { pr_ssripat } + | [ "->" ] -> { IPatRewrite (allocc, L2R) } + | [ "<-" ] -> { IPatRewrite (allocc, R2L) } END +{ + let pr_intros sep intrs = if intrs = [] then mt() else sep () ++ str "=>" ++ pr_ipats intrs let pr_ssrintros _ _ _ = pr_intros mt +} + ARGUMENT EXTEND ssrintros_ne TYPED AS ssripat - PRINTED BY pr_ssrintros - | [ "=>" ssripats_ne(pats) ] -> [ pats ] -(* TODO | [ "=>" ">" ssripats_ne(pats) ] -> [ IPatFastMode :: pats ] + PRINTED BY { pr_ssrintros } + | [ "=>" ssripats_ne(pats) ] -> { pats } +(* TODO | [ "=>" ">" ssripats_ne(pats) ] -> { IPatFastMode :: pats } | [ "=>>" ssripats_ne(pats) ] -> [ IPatFastMode :: pats ] *) END -ARGUMENT EXTEND ssrintros TYPED AS ssrintros_ne PRINTED BY pr_ssrintros - | [ ssrintros_ne(intrs) ] -> [ intrs ] - | [ ] -> [ [] ] +ARGUMENT EXTEND ssrintros TYPED AS ssrintros_ne PRINTED BY { pr_ssrintros } + | [ ssrintros_ne(intrs) ] -> { intrs } + | [ ] -> { [] } END +{ + let pr_ssrintrosarg _ _ prt (tac, ipats) = prt tacltop tac ++ pr_intros spc ipats -ARGUMENT EXTEND ssrintrosarg TYPED AS tactic * ssrintros - PRINTED BY pr_ssrintrosarg -| [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> [ arg, ipats ] +} + +ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) + PRINTED BY { pr_ssrintrosarg } +| [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } END TACTIC EXTEND ssrtclintros | [ "YouShouldNotTypeThis" ssrintrosarg(arg) ] -> - [ let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros ] + { let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros } END +{ + (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id let pr_ssrfwdidx _ _ _ = pr_ssrfwdid +} + (* We use a primitive parser for the head identifier of forward *) (* tactis to avoid syntactic conflicts with basic Coq tactics. *) -ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY pr_ssrfwdidx - | [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] +ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx } + | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END +{ + let accept_ssrfwdid strm = match stream_nth 0 strm with | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm | _ -> raise Stream.Failure - let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: ssrfwdid; - ssrfwdid: [[ test_ssrfwdid; id = Prim.ident -> id ]]; + ssrfwdid: [[ test_ssrfwdid; id = Prim.ident -> { id } ]]; END @@ -900,6 +978,7 @@ GEXTEND Gram (* The latter two are used in forward-chaining tactics (have, suffice, wlog) *) (* and subgoal reordering tacticals (; first & ; last), respectively. *) +{ let pr_ortacs prt = let rec pr_rec = function @@ -914,14 +993,18 @@ let pr_ortacs prt = | [] -> mt() let pr_ssrortacs _ _ = pr_ortacs -ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY pr_ssrortacs -| [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> [ Some tac :: tacs ] -| [ ssrtacarg(tac) "|" ] -> [ [Some tac; None] ] -| [ ssrtacarg(tac) ] -> [ [Some tac] ] -| [ "|" ssrortacs(tacs) ] -> [ None :: tacs ] -| [ "|" ] -> [ [None; None] ] +} + +ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs } +| [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> { Some tac :: tacs } +| [ ssrtacarg(tac) "|" ] -> { [Some tac; None] } +| [ ssrtacarg(tac) ] -> { [Some tac] } +| [ "|" ssrortacs(tacs) ] -> { None :: tacs } +| [ "|" ] -> { [None; None] } END +{ + let pr_hintarg prt = function | true, tacs -> hv 0 (str "[ " ++ pr_ortacs prt tacs ++ str " ]") | false, [Some tac] -> prt tacltop tac @@ -929,26 +1012,30 @@ let pr_hintarg prt = function let pr_ssrhintarg _ _ = pr_hintarg +} -ARGUMENT EXTEND ssrhintarg TYPED AS bool * ssrortacs PRINTED BY pr_ssrhintarg -| [ "[" "]" ] -> [ nullhint ] -| [ "[" ssrortacs(tacs) "]" ] -> [ mk_orhint tacs ] -| [ ssrtacarg(arg) ] -> [ mk_hint arg ] +ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg } +| [ "[" "]" ] -> { nullhint } +| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } +| [ ssrtacarg(arg) ] -> { mk_hint arg } END -ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY pr_ssrhintarg -| [ "[" ssrortacs(tacs) "]" ] -> [ mk_orhint tacs ] +ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg } +| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } END +{ let pr_hint prt arg = if arg = nohint then mt() else str "by " ++ pr_hintarg prt arg let pr_ssrhint _ _ = pr_hint -ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint -| [ ] -> [ nohint ] +} + +ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint } +| [ ] -> { nohint } END -(** The "in" pseudo-tactical *)(* {{{ **********************************************) +(** The "in" pseudo-tactical *) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) @@ -961,6 +1048,8 @@ END (* assumptions. This is especially difficult for discharged "let"s, which *) (* the default simpl and unfold tactics would erase blindly. *) +{ + open Ssrmatching_plugin.Ssrmatching open Ssrmatching_plugin.G_ssrmatching @@ -972,22 +1061,26 @@ let pr_wgen = function | (clr, None) -> spc () ++ pr_clear mt clr let pr_ssrwgen _ _ _ = pr_wgen +} + (* no globwith for char *) ARGUMENT EXTEND ssrwgen - TYPED AS ssrclear * ((ssrhoi_hyp * string) * cpattern option) option - PRINTED BY pr_ssrwgen -| [ ssrclear_ne(clr) ] -> [ clr, None ] -| [ ssrhoi_hyp(hyp) ] -> [ [], Some((hyp, " "), None) ] -| [ "@" ssrhoi_hyp(hyp) ] -> [ [], Some((hyp, "@"), None) ] + TYPED AS (ssrclear * ((ssrhoi_hyp * string) * cpattern option) option) + PRINTED BY { pr_ssrwgen } +| [ ssrclear_ne(clr) ] -> { clr, None } +| [ ssrhoi_hyp(hyp) ] -> { [], Some((hyp, " "), None) } +| [ "@" ssrhoi_hyp(hyp) ] -> { [], Some((hyp, "@"), None) } | [ "(" ssrhoi_id(id) ":=" lcpattern(p) ")" ] -> - [ [], Some ((id," "),Some p) ] -| [ "(" ssrhoi_id(id) ")" ] -> [ [], Some ((id,"("), None) ] + { [], Some ((id," "),Some p) } +| [ "(" ssrhoi_id(id) ")" ] -> { [], Some ((id,"("), None) } | [ "(@" ssrhoi_id(id) ":=" lcpattern(p) ")" ] -> - [ [], Some ((id,"@"),Some p) ] + { [], Some ((id,"@"),Some p) } | [ "(" "@" ssrhoi_id(id) ":=" lcpattern(p) ")" ] -> - [ [], Some ((id,"@"),Some p) ] + { [], Some ((id,"@"),Some p) } END +{ + let pr_clseq = function | InGoal | InHyps -> mt () | InSeqGoal -> str "|- *" @@ -1001,13 +1094,17 @@ let wit_ssrclseq = add_genarg "ssrclseq" pr_clseq let pr_clausehyps = pr_list pr_spc pr_wgen let pr_ssrclausehyps _ _ _ = pr_clausehyps +} + ARGUMENT EXTEND ssrclausehyps -TYPED AS ssrwgen list PRINTED BY pr_ssrclausehyps -| [ ssrwgen(hyp) "," ssrclausehyps(hyps) ] -> [ hyp :: hyps ] -| [ ssrwgen(hyp) ssrclausehyps(hyps) ] -> [ hyp :: hyps ] -| [ ssrwgen(hyp) ] -> [ [hyp] ] +TYPED AS ssrwgen list PRINTED BY { pr_ssrclausehyps } +| [ ssrwgen(hyp) "," ssrclausehyps(hyps) ] -> { hyp :: hyps } +| [ ssrwgen(hyp) ssrclausehyps(hyps) ] -> { hyp :: hyps } +| [ ssrwgen(hyp) ] -> { [hyp] } END +{ + (* type ssrclauses = ssrahyps * ssrclseq *) let pr_clauses (hyps, clseq) = @@ -1015,20 +1112,22 @@ let pr_clauses (hyps, clseq) = else str "in " ++ pr_clausehyps hyps ++ pr_clseq clseq let pr_ssrclauses _ _ _ = pr_clauses -ARGUMENT EXTEND ssrclauses TYPED AS ssrwgen list * ssrclseq - PRINTED BY pr_ssrclauses - | [ "in" ssrclausehyps(hyps) "|-" "*" ] -> [ hyps, InHypsSeqGoal ] - | [ "in" ssrclausehyps(hyps) "|-" ] -> [ hyps, InHypsSeq ] - | [ "in" ssrclausehyps(hyps) "*" ] -> [ hyps, InHypsGoal ] - | [ "in" ssrclausehyps(hyps) ] -> [ hyps, InHyps ] - | [ "in" "|-" "*" ] -> [ [], InSeqGoal ] - | [ "in" "*" ] -> [ [], InAll ] - | [ "in" "*" "|-" ] -> [ [], InAllHyps ] - | [ ] -> [ [], InGoal ] -END +} +ARGUMENT EXTEND ssrclauses TYPED AS (ssrwgen list * ssrclseq) + PRINTED BY { pr_ssrclauses } + | [ "in" ssrclausehyps(hyps) "|-" "*" ] -> { hyps, InHypsSeqGoal } + | [ "in" ssrclausehyps(hyps) "|-" ] -> { hyps, InHypsSeq } + | [ "in" ssrclausehyps(hyps) "*" ] -> { hyps, InHypsGoal } + | [ "in" ssrclausehyps(hyps) ] -> { hyps, InHyps } + | [ "in" "|-" "*" ] -> { [], InSeqGoal } + | [ "in" "*" ] -> { [], InAll } + | [ "in" "*" "|-" ] -> { [], InAllHyps } + | [ ] -> { [], InGoal } +END +{ (** Definition value formatting *) @@ -1142,10 +1241,12 @@ let pr_unguarded prc prlc = prlc let pr_fwd = pr_fwd_guarded pr_unguarded pr_unguarded let pr_ssrfwd _ _ _ = pr_fwd - -ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ast_closure_lterm) PRINTED BY pr_ssrfwd - | [ ":=" ast_closure_lterm(c) ] -> [ mkFwdVal FwdPose c ] - | [ ":" ast_closure_lterm (t) ":=" ast_closure_lterm(c) ] -> [ mkFwdCast FwdPose ~loc t ~c ] + +} + +ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ast_closure_lterm) PRINTED BY { pr_ssrfwd } + | [ ":=" ast_closure_lterm(c) ] -> { mkFwdVal FwdPose c } + | [ ":" ast_closure_lterm (t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdPose ~loc t ~c } END (** Independent parsing for binders *) @@ -1153,13 +1254,19 @@ END (* The pose, pose fix, and pose cofix tactics use these internally to *) (* parse argument fragments. *) +{ + let pr_ssrbvar prc _ _ v = prc v -ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar -| [ ident(id) ] -> [ mkCVar ~loc id ] -| [ "_" ] -> [ mkCHole (Some loc) ] +} + +ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar } +| [ ident(id) ] -> { mkCVar ~loc id } +| [ "_" ] -> { mkCHole (Some loc) } END +{ + let bvar_lname = let open CAst in function | { v = CRef (qid, _) } when qualid_is_ident qid -> CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) @@ -1167,40 +1274,43 @@ let bvar_lname = let open CAst in function let pr_ssrbinder prc _ _ (_, c) = prc c -ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder +} + +ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder } | [ ssrbvar(bv) ] -> - [ let { CAst.loc=xloc } as x = bvar_lname bv in + { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ")" ] -> - [ let { CAst.loc=xloc } as x = bvar_lname bv in + { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> - [ let x = bvar_lname bv in + { let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> - [ let xs = List.map bvar_lname (bv :: bvs) in + { let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> - [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) ] + { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> - [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, None, mkCHole (Some loc)) ] + { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, None, mkCHole (Some loc)) } END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssrbinder; ssrbinder: [ - [ ["of" | "&"]; c = operconstr LEVEL "99" -> - let loc = !@loc in + [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ] ]; END +{ + let rec binders_fmts = function | ((_, h), _) :: bs -> h @ binders_fmts bs | _ -> [] @@ -1233,24 +1343,32 @@ let pr_ssrstruct _ _ _ = function | Some id -> str "{struct " ++ pr_id id ++ str "}" | None -> mt () -ARGUMENT EXTEND ssrstruct TYPED AS ident option PRINTED BY pr_ssrstruct -| [ "{" "struct" ident(id) "}" ] -> [ Some id ] -| [ ] -> [ None ] +} + +ARGUMENT EXTEND ssrstruct TYPED AS ident option PRINTED BY { pr_ssrstruct } +| [ "{" "struct" ident(id) "}" ] -> { Some id } +| [ ] -> { None } END (** The "pose" tactic *) (* The plain pose form. *) +{ + let bind_fwd bs ((fk, h), c) = (fk,binders_fmts bs @ h), { c with body = push_binders c.body bs } -ARGUMENT EXTEND ssrposefwd TYPED AS ssrfwd PRINTED BY pr_ssrfwd - | [ ssrbinder_list(bs) ssrfwd(fwd) ] -> [ bind_fwd bs fwd ] +} + +ARGUMENT EXTEND ssrposefwd TYPED AS ssrfwd PRINTED BY { pr_ssrfwd } + | [ ssrbinder_list(bs) ssrfwd(fwd) ] -> { bind_fwd bs fwd } END (* The pose fix form. *) +{ + let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function @@ -1258,10 +1376,11 @@ let bvar_locid = function CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") +} -ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd +ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd } | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] -> - [ let { CAst.v=id } as lid = bvar_locid bv in + { let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), ac = fwd in let c = ac.body in let has_cast, t', c' = match format_constr_expr h c with @@ -1279,17 +1398,21 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd loop (names_of_local_assums lb) in let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in - id, ((fk, h'), { ac with body = fix }) ] + id, ((fk, h'), { ac with body = fix }) } END (* The pose cofix form. *) +{ + let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd -ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd +} + +ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY { pr_ssrcofixfwd } | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] -> - [ let { CAst.v=id } as lid = bvar_locid bv in + { let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), ac = fwd in let c = ac.body in let has_cast, t', c' = match format_constr_expr h c with @@ -1298,36 +1421,45 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd let h' = BFrec (false, has_cast) :: binders_fmts bs in let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, fix_binders bs, t', c']) in id, ((fk, h'), { ac with body = cofix }) - ] + } END +{ + (* This does not print the type, it should be fixed... *) let pr_ssrsetfwd _ _ _ (((fk,_),(t,_)), docc) = pr_gen_fwd (fun _ _ -> pr_cpattern) (fun _ -> mt()) (fun _ -> mt()) fk ([Bcast ()],t) +} + ARGUMENT EXTEND ssrsetfwd -TYPED AS (ssrfwdfmt * (lcpattern * ast_closure_lterm option)) * ssrdocc -PRINTED BY pr_ssrsetfwd +TYPED AS ((ssrfwdfmt * (lcpattern * ast_closure_lterm option)) * ssrdocc) +PRINTED BY { pr_ssrsetfwd } | [ ":" ast_closure_lterm(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] -> - [ mkssrFwdCast FwdPose loc t c, mkocc occ ] + { mkssrFwdCast FwdPose loc t c, mkocc occ } | [ ":" ast_closure_lterm(t) ":=" lcpattern(c) ] -> - [ mkssrFwdCast FwdPose loc t c, nodocc ] + { mkssrFwdCast FwdPose loc t c, nodocc } | [ ":=" "{" ssrocc(occ) "}" cpattern(c) ] -> - [ mkssrFwdVal FwdPose c, mkocc occ ] -| [ ":=" lcpattern(c) ] -> [ mkssrFwdVal FwdPose c, nodocc ] + { mkssrFwdVal FwdPose c, mkocc occ } +| [ ":=" lcpattern(c) ] -> { mkssrFwdVal FwdPose c, nodocc } END +{ let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint -ARGUMENT EXTEND ssrhavefwd TYPED AS ssrfwd * ssrhint PRINTED BY pr_ssrhavefwd -| [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> [ mkFwdHint ":" t, hint ] -| [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> [ mkFwdCast FwdHave ~loc t ~c, nohint ] -| [ ":" ast_closure_lterm(t) ":=" ] -> [ mkFwdHintNoTC ":" t, nohint ] -| [ ":=" ast_closure_lterm(c) ] -> [ mkFwdVal FwdHave c, nohint ] +} + +ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd } +| [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> { mkFwdHint ":" t, hint } +| [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdHave ~loc t ~c, nohint } +| [ ":" ast_closure_lterm(t) ":=" ] -> { mkFwdHintNoTC ":" t, nohint } +| [ ":=" ast_closure_lterm(c) ] -> { mkFwdVal FwdHave c, nohint } END +{ + let intro_id_to_binder = List.map (function | IPatId id -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in @@ -1347,28 +1479,35 @@ let binder_to_intro_id = CAst.(List.map (function let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) = pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint +} + ARGUMENT EXTEND ssrhavefwdwbinders - TYPED AS bool * (ssrhpats * (ssrfwd * ssrhint)) - PRINTED BY pr_ssrhavefwdwbinders + TYPED AS (bool * (ssrhpats * (ssrfwd * ssrhint))) + PRINTED BY { pr_ssrhavefwdwbinders } | [ ssrhpats_wtransp(trpats) ssrbinder_list(bs) ssrhavefwd(fwd) ] -> - [ let tr, pats = trpats in + { let tr, pats = trpats in let ((clr, pats), binders), simpl = pats in let allbs = intro_id_to_binder binders @ bs in let allbinders = binders @ List.flatten (binder_to_intro_id bs) in let hint = bind_fwd allbs (fst fwd), snd fwd in - tr, ((((clr, pats), allbinders), simpl), hint) ] + tr, ((((clr, pats), allbinders), simpl), hint) } END +{ let pr_ssrdoarg prc _ prt (((n, m), tac), clauses) = pr_index n ++ pr_mmod m ++ pr_hintarg prt tac ++ pr_clauses clauses +} + ARGUMENT EXTEND ssrdoarg - TYPED AS ((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses - PRINTED BY pr_ssrdoarg -| [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] + TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses) + PRINTED BY { pr_ssrdoarg } +| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END +{ + (* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *) let pr_seqtacarg prt = function @@ -1381,13 +1520,17 @@ let pr_ssrseqarg _ _ prt = function | ArgArg 0, tac -> pr_seqtacarg prt tac | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg prt tac +} + (* We must parse the index separately to resolve the conflict with *) (* an unindexed tactic. *) -ARGUMENT EXTEND ssrseqarg TYPED AS ssrindex * (ssrhintarg * tactic option) - PRINTED BY pr_ssrseqarg -| [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] +ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option)) + PRINTED BY { pr_ssrseqarg } +| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END +{ + let sq_brace_tacnames = ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"] (* "by" is a keyword *) @@ -1409,35 +1552,45 @@ let check_seqtacarg dir arg = match snd arg, dir with | _, _ -> arg let ssrorelse = Entry.create "ssrorelse" -GEXTEND Gram + +} + +GRAMMAR EXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ - [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id) - | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n) + [ test_ssrseqvar; id = Prim.ident -> { ArgVar (CAst.make ~loc id) } + | n = Prim.natural -> { ArgArg (check_index ~loc n) } ] ]; - ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]]; - ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> tac ]]; + ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]]; + ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]]; ssrseqarg: [ - [ arg = ssrswap -> noindex, swaptacarg arg - | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> i, (tac, def) - | i = ssrseqidx; arg = ssrswap -> i, swaptacarg arg - | tac = tactic_expr LEVEL "3" -> noindex, (mk_hint tac, None) + [ arg = ssrswap -> { noindex, swaptacarg arg } + | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) } + | i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg } + | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } ] ]; END +{ + let tactic_expr = Pltac.tactic_expr +} + (** 1. Utilities *) (** Tactic-level diagnosis *) (* debug *) +{ + (* Let's play with the new proof engine API *) let old_tac = V82.tactic +} -(** Name generation *)(* {{{ *******************************************************) +(** Name generation *) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) @@ -1448,6 +1601,8 @@ let old_tac = V82.tactic (* when the ssreflect Module is present this is normally an error, *) (* but we provide a compatibility flag to reduce this to a warning. *) +{ + let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true let _ = @@ -1475,21 +1630,23 @@ let ssr_id_of_string loc s = let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) -let (!@) = Pcoq.to_coqloc +} -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: Prim.ident; - Prim.ident: [[ s = IDENT; ssr_null_entry -> ssr_id_of_string !@loc s ]]; + Prim.ident: [[ s = IDENT; ssr_null_entry -> { ssr_id_of_string loc s } ]]; END +{ + let perm_tag = "_perm_Hyp_" let _ = add_internal_name (is_tagged perm_tag) - -(* }}} *) + +} (* We must not anonymize context names discharged by the "in" tactical. *) -(** Tactical extensions. *)(* {{{ **************************************************) +(** Tactical extensions. *) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) @@ -1499,6 +1656,8 @@ let _ = add_internal_name (is_tagged perm_tag) (* don't start with a token, then redefine the grammar and *) (* printer using GEXTEND and set_pr_ssrtac, respectively. *) +{ + type ssrargfmt = ArgSsr of string | ArgSep of string let ssrtac_name name = { @@ -1525,15 +1684,15 @@ let tclintros_expr ?loc tac ipats = let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in ssrtac_expr ?loc "tclintros" args -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: tactic_expr; tactic_expr: LEVEL "1" [ RIGHTA - [ tac = tactic_expr; intros = ssrintros_ne -> tclintros_expr ~loc:!@loc tac intros + [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } ] ]; END -(* }}} *) - (** Bracketing tactical *) @@ -1543,10 +1702,10 @@ END (* expressions so that the pretty-print always reflects the input. *) (* (Removing user-specified parentheses is dubious anyway). *) -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: tactic_expr; - ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> Loc.tag ~loc:!@loc (Tacexp tac) ]]; - tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> TacArg arg ]]; + ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { Loc.tag ~loc (Tacexp tac) } ]]; + tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; END (** The internal "done" and "ssrautoprop" tactics. *) @@ -1558,6 +1717,8 @@ END (* to allow for user extensions. "ssrautoprop" defaults to *) (* trivial. *) +{ + let ssrautoprop gl = try let tacname = @@ -1584,17 +1745,18 @@ let tclBY tac = Tacticals.tclTHEN tac (donetac ~-1) open Ssrfwd +} + TACTIC EXTEND ssrtclby -| [ "by" ssrhintarg(tac) ] -> [ V82.tactic (hinttac ist true tac) ] +| [ "by" ssrhintarg(tac) ] -> { V82.tactic (hinttac ist true tac) } END -(* }}} *) (* We can't parse "by" in ARGUMENT EXTEND because it will only be made *) (* into a keyword in ssreflect.v; so we anticipate this in GEXTEND. *) -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssrhint simple_tactic; - ssrhint: [[ "by"; arg = ssrhintarg -> arg ]]; + ssrhint: [[ "by"; arg = ssrhintarg -> { arg } ]]; END (** The "do" tactical. ********************************************************) @@ -1603,32 +1765,37 @@ END type ssrdoarg = ((ssrindex * ssrmmod) * ssrhint) * ssrclauses *) TACTIC EXTEND ssrtcldo -| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> [ V82.tactic (ssrdotac ist arg) ] +| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> { V82.tactic (ssrdotac ist arg) } END -set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] + +{ + +let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr ?loc n m tac clauses = let arg = ((n, m), tac), clauses in ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)] -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: tactic_expr; ssrdotac: [ - [ tac = tactic_expr LEVEL "3" -> mk_hint tac - | tacs = ssrortacarg -> tacs + [ tac = tactic_expr LEVEL "3" -> { mk_hint tac } + | tacs = ssrortacarg -> { tacs } ] ]; tactic_expr: LEVEL "3" [ RIGHTA [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> - ssrdotac_expr ~loc:!@loc noindex m tac clauses + { ssrdotac_expr ~loc noindex m tac clauses } | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses -> - ssrdotac_expr ~loc:!@loc noindex Once tac clauses + { ssrdotac_expr ~loc noindex Once tac clauses } | IDENT "do"; n = int_or_var; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> - ssrdotac_expr ~loc:!@loc (mk_index ~loc:!@loc n) m tac clauses + { ssrdotac_expr ~loc (mk_index ~loc n) m tac clauses } ] ]; END -(* }}} *) +{ (* We can't actually parse the direction separately because this *) (* would introduce conflicts with the basic ltac syntax. *) @@ -1636,15 +1803,20 @@ let pr_ssrseqdir _ _ _ = function | L2R -> str ";" ++ spc () ++ str "first " | R2L -> str ";" ++ spc () ++ str "last " -ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY pr_ssrseqdir -| [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] +} + +ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } +| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END TACTIC EXTEND ssrtclseq | [ "YouShouldNotTypeThis" ssrtclarg(tac) ssrseqdir(dir) ssrseqarg(arg) ] -> - [ V82.tactic (tclSEQAT ist tac dir arg) ] + { V82.tactic (tclSEQAT ist tac dir arg) } END -set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] + +{ + +let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] let tclseq_expr ?loc tac dir arg = let arg1 = in_gen (rawwit wit_ssrtclarg) tac in @@ -1652,25 +1824,26 @@ let tclseq_expr ?loc tac dir arg = let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3]) -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: tactic_expr; ssr_first: [ - [ tac = ssr_first; ipats = ssrintros_ne -> tclintros_expr ~loc:!@loc tac ipats - | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> TacFirst tacl + [ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats } + | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl } ] ]; ssr_first_else: [ - [ tac1 = ssr_first; tac2 = ssrorelse -> TacOrelse (tac1, tac2) - | tac = ssr_first -> tac ]]; + [ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) } + | tac = ssr_first -> { tac } ]]; tactic_expr: LEVEL "4" [ LEFTA [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> - TacThen (tac1, tac2) + { TacThen (tac1, tac2) } | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg -> - tclseq_expr ~loc:!@loc tac L2R arg + { tclseq_expr ~loc tac L2R arg } | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg -> - tclseq_expr ~loc:!@loc tac R2L arg + { tclseq_expr ~loc tac R2L arg } ] ]; END -(* }}} *) (** 5. Bookkeeping tactics (clear, move, case, elim) *) @@ -1680,18 +1853,24 @@ END (* type ssrgen = ssrdocc * ssrterm *) +{ + let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen -ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen -| [ ssrdocc(docc) cpattern(dt) ] -> [ +} + +ARGUMENT EXTEND ssrgen TYPED AS (ssrdocc * cpattern) PRINTED BY { pr_ssrgen } +| [ ssrdocc(docc) cpattern(dt) ] -> { match docc with | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here") - | _ -> docc, dt ] -| [ cpattern(dt) ] -> [ nodocc, dt ] + | _ -> docc, dt } +| [ cpattern(dt) ] -> { nodocc, dt } END +{ + let has_occ ((_, occ), _) = occ <> None (** Generalization (discharge) sequence *) @@ -1727,39 +1906,47 @@ let cons_dep (gensl, clr) = if List.length gensl = 1 then ([] :: gensl, clr) else CErrors.user_err (Pp.str "multiple dependents switches '/'") -ARGUMENT EXTEND ssrdgens_tl TYPED AS ssrgen list list * ssrclear - PRINTED BY pr_ssrdgens +} + +ARGUMENT EXTEND ssrdgens_tl TYPED AS (ssrgen list list * ssrclear) + PRINTED BY { pr_ssrdgens } | [ "{" ne_ssrhyp_list(clr) "}" cpattern(dt) ssrdgens_tl(dgens) ] -> - [ cons_gen (mkclr clr, dt) dgens ] + { cons_gen (mkclr clr, dt) dgens } | [ "{" ne_ssrhyp_list(clr) "}" ] -> - [ [[]], clr ] + { [[]], clr } | [ "{" ssrocc(occ) "}" cpattern(dt) ssrdgens_tl(dgens) ] -> - [ cons_gen (mkocc occ, dt) dgens ] + { cons_gen (mkocc occ, dt) dgens } | [ "/" ssrdgens_tl(dgens) ] -> - [ cons_dep dgens ] + { cons_dep dgens } | [ cpattern(dt) ssrdgens_tl(dgens) ] -> - [ cons_gen (nodocc, dt) dgens ] + { cons_gen (nodocc, dt) dgens } | [ ] -> - [ [[]], [] ] + { [[]], [] } END -ARGUMENT EXTEND ssrdgens TYPED AS ssrdgens_tl PRINTED BY pr_ssrdgens -| [ ":" ssrgen(gen) ssrdgens_tl(dgens) ] -> [ cons_gen gen dgens ] +ARGUMENT EXTEND ssrdgens TYPED AS ssrdgens_tl PRINTED BY { pr_ssrdgens } +| [ ":" ssrgen(gen) ssrdgens_tl(dgens) ] -> { cons_gen gen dgens } END (** Equations *) (* argument *) +{ + let pr_eqid = function Some pat -> str " " ++ pr_ipat pat | None -> mt () let pr_ssreqid _ _ _ = pr_eqid +} + (* We must use primitive parsing here to avoid conflicts with the *) (* basic move, case, and elim tactics. *) -ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY pr_ssreqid -| [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] +ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY { pr_ssreqid } +| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END +{ + let accept_ssreqid strm = match Util.stream_nth 0 strm with | Tok.IDENT _ -> accept_before_syms [":"] strm @@ -1770,24 +1957,26 @@ let accept_ssreqid strm = let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: ssreqid; ssreqpat: [ - [ id = Prim.ident -> IPatId id - | "_" -> IPatAnon Drop - | "?" -> IPatAnon One - | occ = ssrdocc; "->" -> (match occ with + [ id = Prim.ident -> { IPatId id } + | "_" -> { IPatAnon Drop } + | "?" -> { IPatAnon One } + | occ = ssrdocc; "->" -> { match occ with | None, occ -> IPatRewrite (occ, L2R) - | _ -> CErrors.user_err ~loc:!@loc (str"Only occurrences are allowed here")) - | occ = ssrdocc; "<-" -> (match occ with + | _ -> CErrors.user_err ~loc (str"Only occurrences are allowed here") } + | occ = ssrdocc; "<-" -> { match occ with | None, occ -> IPatRewrite (occ, R2L) - | _ -> CErrors.user_err ~loc:!@loc (str "Only occurrences are allowed here")) - | "->" -> IPatRewrite (allocc, L2R) - | "<-" -> IPatRewrite (allocc, R2L) + | _ -> CErrors.user_err ~loc (str "Only occurrences are allowed here") } + | "->" -> { IPatRewrite (allocc, L2R) } + | "<-" -> { IPatRewrite (allocc, R2L) } ]]; ssreqid: [ - [ test_ssreqid; pat = ssreqpat -> Some pat - | test_ssreqid -> None + [ test_ssreqid; pat = ssreqpat -> { Some pat } + | test_ssreqid -> { None } ]]; END @@ -1800,22 +1989,26 @@ END (* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) +{ + let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) = let pri = pr_intros (gens_sep dgens) in pr_view2 view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats -ARGUMENT EXTEND ssrarg TYPED AS ssrfwdview * (ssreqid * (ssrdgens * ssrintros)) - PRINTED BY pr_ssrarg +} + +ARGUMENT EXTEND ssrarg TYPED AS (ssrfwdview * (ssreqid * (ssrdgens * ssrintros))) + PRINTED BY { pr_ssrarg } | [ ssrfwdview(view) ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] -> - [ view, (eqid, (dgens, ipats)) ] + { view, (eqid, (dgens, ipats)) } | [ ssrfwdview(view) ssrclear(clr) ssrintros(ipats) ] -> - [ view, (None, (([], clr), ipats)) ] + { view, (None, (([], clr), ipats)) } | [ ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] -> - [ [], (eqid, (dgens, ipats)) ] + { [], (eqid, (dgens, ipats)) } | [ ssrclear_ne(clr) ssrintros(ipats) ] -> - [ [], (None, (([], clr), ipats)) ] + { [], (None, (([], clr), ipats)) } | [ ssrintros_ne(ipats) ] -> - [ [], (None, (([], []), ipats)) ] + { [], (None, (([], []), ipats)) } END (** The "clear" tactic *) @@ -1823,11 +2016,13 @@ END (* We just add a numeric version that clears the n top assumptions. *) TACTIC EXTEND ssrclear - | [ "clear" natural(n) ] -> [ tclIPAT (List.init n (fun _ -> IPatAnon Drop)) ] + | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IPatAnon Drop)) } END (** The "move" tactic *) +{ + (* TODO: review this, in particular the => _ and => [] cases *) let rec improper_intros = function | IPatSimpl _ :: ipats -> improper_intros ipats @@ -1845,149 +2040,179 @@ let check_movearg = function CErrors.user_err (Pp.str "no proper intro pattern for equation in move tactic") | arg -> arg -ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg -| [ ssrarg(arg) ] -> [ check_movearg arg ] +} + +ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY { pr_ssrarg } +| [ ssrarg(arg) ] -> { check_movearg arg } END +{ + let movearg_of_parsed_movearg (v,(eq,(dg,ip))) = (v,(eq,(ssrdgens_of_parsed_dgens dg,ip))) +} + TACTIC EXTEND ssrmove | [ "move" ssrmovearg(arg) ssrrpat(pat) ] -> - [ ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] ] + { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] } | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] -> - [ tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses ] -| [ "move" ssrrpat(pat) ] -> [ tclIPAT [pat] ] -| [ "move" ] -> [ ssrsmovetac ] + { tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses } +| [ "move" ssrrpat(pat) ] -> { tclIPAT [pat] } +| [ "move" ] -> { ssrsmovetac } END +{ + let check_casearg = function | view, (_, (([_; gen :: _], _), _)) when view <> [] && has_occ gen -> CErrors.user_err (Pp.str "incompatible view and occurrence switch in dependent case tactic") | arg -> arg -ARGUMENT EXTEND ssrcasearg TYPED AS ssrarg PRINTED BY pr_ssrarg -| [ ssrarg(arg) ] -> [ check_casearg arg ] +} + +ARGUMENT EXTEND ssrcasearg TYPED AS ssrarg PRINTED BY { pr_ssrarg } +| [ ssrarg(arg) ] -> { check_casearg arg } END TACTIC EXTEND ssrcase | [ "case" ssrcasearg(arg) ssrclauses(clauses) ] -> - [ tclCLAUSES (ssrcasetac (movearg_of_parsed_movearg arg)) clauses ] -| [ "case" ] -> [ ssrscasetoptac ] + { tclCLAUSES (ssrcasetac (movearg_of_parsed_movearg arg)) clauses } +| [ "case" ] -> { ssrscasetoptac } END (** The "elim" tactic *) TACTIC EXTEND ssrelim | [ "elim" ssrarg(arg) ssrclauses(clauses) ] -> - [ tclCLAUSES (ssrelimtac (movearg_of_parsed_movearg arg)) clauses ] -| [ "elim" ] -> [ ssrselimtoptac ] + { tclCLAUSES (ssrelimtac (movearg_of_parsed_movearg arg)) clauses } +| [ "elim" ] -> { ssrselimtoptac } END (** 6. Backward chaining tactics: apply, exact, congr. *) (** The "apply" tactic *) +{ + let pr_agen (docc, dt) = pr_docc docc ++ pr_term dt let pr_ssragen _ _ _ = pr_agen let pr_ssragens _ _ _ = pr_dgens pr_agen -ARGUMENT EXTEND ssragen TYPED AS ssrdocc * ssrterm PRINTED BY pr_ssragen -| [ "{" ne_ssrhyp_list(clr) "}" ssrterm(dt) ] -> [ mkclr clr, dt ] -| [ ssrterm(dt) ] -> [ nodocc, dt ] +} + +ARGUMENT EXTEND ssragen TYPED AS (ssrdocc * ssrterm) PRINTED BY { pr_ssragen } +| [ "{" ne_ssrhyp_list(clr) "}" ssrterm(dt) ] -> { mkclr clr, dt } +| [ ssrterm(dt) ] -> { nodocc, dt } END -ARGUMENT EXTEND ssragens TYPED AS ssragen list list * ssrclear -PRINTED BY pr_ssragens +ARGUMENT EXTEND ssragens TYPED AS (ssragen list list * ssrclear) +PRINTED BY { pr_ssragens } | [ "{" ne_ssrhyp_list(clr) "}" ssrterm(dt) ssragens(agens) ] -> - [ cons_gen (mkclr clr, dt) agens ] -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ [[]], clr] + { cons_gen (mkclr clr, dt) agens } +| [ "{" ne_ssrhyp_list(clr) "}" ] -> { [[]], clr} | [ ssrterm(dt) ssragens(agens) ] -> - [ cons_gen (nodocc, dt) agens ] -| [ ] -> [ [[]], [] ] + { cons_gen (nodocc, dt) agens } +| [ ] -> { [[]], [] } END +{ + let mk_applyarg views agens intros = views, (agens, intros) let pr_ssraarg _ _ _ (view, (dgens, ipats)) = let pri = pr_intros (gens_sep dgens) in pr_view view ++ pr_dgens pr_agen dgens ++ pri ipats +} + ARGUMENT EXTEND ssrapplyarg -TYPED AS ssrbwdview * (ssragens * ssrintros) -PRINTED BY pr_ssraarg +TYPED AS (ssrbwdview * (ssragens * ssrintros)) +PRINTED BY { pr_ssraarg } | [ ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] -> - [ mk_applyarg [] (cons_gen gen dgens) intros ] + { mk_applyarg [] (cons_gen gen dgens) intros } | [ ssrclear_ne(clr) ssrintros(intros) ] -> - [ mk_applyarg [] ([], clr) intros ] + { mk_applyarg [] ([], clr) intros } | [ ssrintros_ne(intros) ] -> - [ mk_applyarg [] ([], []) intros ] + { mk_applyarg [] ([], []) intros } | [ ssrbwdview(view) ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] -> - [ mk_applyarg view (cons_gen gen dgens) intros ] + { mk_applyarg view (cons_gen gen dgens) intros } | [ ssrbwdview(view) ssrclear(clr) ssrintros(intros) ] -> - [ mk_applyarg view ([], clr) intros ] + { mk_applyarg view ([], clr) intros } END TACTIC EXTEND ssrapply -| [ "apply" ssrapplyarg(arg) ] -> [ +| [ "apply" ssrapplyarg(arg) ] -> { let views, (gens_clr, intros) = arg in - inner_ssrapplytac views gens_clr ist <*> tclIPATssr intros ] -| [ "apply" ] -> [ apply_top_tac ] + inner_ssrapplytac views gens_clr ist <*> tclIPATssr intros } +| [ "apply" ] -> { apply_top_tac } END (** The "exact" tactic *) +{ + let mk_exactarg views dgens = mk_applyarg views dgens [] -ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg +} + +ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY { pr_ssraarg } | [ ":" ssragen(gen) ssragens(dgens) ] -> - [ mk_exactarg [] (cons_gen gen dgens) ] + { mk_exactarg [] (cons_gen gen dgens) } | [ ssrbwdview(view) ssrclear(clr) ] -> - [ mk_exactarg view ([], clr) ] + { mk_exactarg view ([], clr) } | [ ssrclear_ne(clr) ] -> - [ mk_exactarg [] ([], clr) ] + { mk_exactarg [] ([], clr) } END +{ + let vmexacttac pf = Goal.enter begin fun gl -> exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end +} + TACTIC EXTEND ssrexact -| [ "exact" ssrexactarg(arg) ] -> [ +| [ "exact" ssrexactarg(arg) ] -> { let views, (gens_clr, _) = arg in - V82.tactic (tclBY (V82.of_tactic (inner_ssrapplytac views gens_clr ist))) ] -| [ "exact" ] -> [ - V82.tactic (Tacticals.tclORELSE (donetac ~-1) (tclBY (V82.of_tactic apply_top_tac))) ] -| [ "exact" "<:" lconstr(pf) ] -> [ vmexacttac pf ] + V82.tactic (tclBY (V82.of_tactic (inner_ssrapplytac views gens_clr ist))) } +| [ "exact" ] -> { + V82.tactic (Tacticals.tclORELSE (donetac ~-1) (tclBY (V82.of_tactic apply_top_tac))) } +| [ "exact" "<:" lconstr(pf) ] -> { vmexacttac pf } END (** The "congr" tactic *) (* type ssrcongrarg = open_constr * (int * constr) *) +{ + let pr_ssrcongrarg _ _ _ ((n, f), dgens) = (if n <= 0 then mt () else str " " ++ int n) ++ str " " ++ pr_term f ++ pr_dgens pr_gen dgens -ARGUMENT EXTEND ssrcongrarg TYPED AS (int * ssrterm) * ssrdgens - PRINTED BY pr_ssrcongrarg -| [ natural(n) constr(c) ssrdgens(dgens) ] -> [ (n, mk_term xNoFlag c), dgens ] -| [ natural(n) constr(c) ] -> [ (n, mk_term xNoFlag c),([[]],[]) ] -| [ constr(c) ssrdgens(dgens) ] -> [ (0, mk_term xNoFlag c), dgens ] -| [ constr(c) ] -> [ (0, mk_term xNoFlag c), ([[]],[]) ] +} + +ARGUMENT EXTEND ssrcongrarg TYPED AS ((int * ssrterm) * ssrdgens) + PRINTED BY { pr_ssrcongrarg } +| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term xNoFlag c), dgens } +| [ natural(n) constr(c) ] -> { (n, mk_term xNoFlag c),([[]],[]) } +| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term xNoFlag c), dgens } +| [ constr(c) ] -> { (0, mk_term xNoFlag c), ([[]],[]) } END TACTIC EXTEND ssrcongr | [ "congr" ssrcongrarg(arg) ] -> -[ let arg, dgens = arg in +{ let arg, dgens = arg in V82.tactic begin match dgens with | [gens], clr -> Tacticals.tclTHEN (genstac (gens,clr)) (newssrcongrtac arg ist) | _ -> errorstrm (str"Dependent family abstractions not allowed in congr") - end] + end } END (** 7. Rewriting tactics (rewrite, unlock) *) @@ -1996,6 +2221,8 @@ END (** Rewrite clear/occ switches *) +{ + let pr_rwocc = function | None, None -> mt () | None, occ -> pr_occ occ @@ -2003,14 +2230,18 @@ let pr_rwocc = function let pr_ssrrwocc _ _ _ = pr_rwocc -ARGUMENT EXTEND ssrrwocc TYPED AS ssrdocc PRINTED BY pr_ssrrwocc -| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] -| [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] -| [ ] -> [ noclr ] +} + +ARGUMENT EXTEND ssrrwocc TYPED AS ssrdocc PRINTED BY { pr_ssrrwocc } +| [ "{" ssrhyp_list(clr) "}" ] -> { mkclr clr } +| [ "{" ssrocc(occ) "}" ] -> { mkocc occ } +| [ ] -> { noclr } END (** Rewrite rules *) +{ + let pr_rwkind = function | RWred s -> pr_simpl s | RWdef -> str "/" @@ -2027,29 +2258,33 @@ let pr_ssrrule _ _ _ = pr_rule let noruleterm loc = mk_term xNoFlag (mkCProp loc) -ARGUMENT EXTEND ssrrule_ne TYPED AS ssrrwkind * ssrterm PRINTED BY pr_ssrrule - | [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] +} + +ARGUMENT EXTEND ssrrule_ne TYPED AS (ssrrwkind * ssrterm) PRINTED BY { pr_ssrrule } + | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssrrule_ne; ssrrule_ne : [ [ test_not_ssrslashnum; x = - [ "/"; t = ssrterm -> RWdef, t - | t = ssrterm -> RWeq, t - | s = ssrsimpl_ne -> RWred s, noruleterm (Some !@loc) - ] -> x - | s = ssrsimpl_ne -> RWred s, noruleterm (Some !@loc) + [ "/"; t = ssrterm -> { RWdef, t } + | t = ssrterm -> { RWeq, t } + | s = ssrsimpl_ne -> { RWred s, noruleterm (Some loc) } + ] -> { x } + | s = ssrsimpl_ne -> { RWred s, noruleterm (Some loc) } ]]; END -ARGUMENT EXTEND ssrrule TYPED AS ssrrule_ne PRINTED BY pr_ssrrule - | [ ssrrule_ne(r) ] -> [ r ] - | [ ] -> [ RWred Nop, noruleterm (Some loc) ] +ARGUMENT EXTEND ssrrule TYPED AS ssrrule_ne PRINTED BY { pr_ssrrule } + | [ ssrrule_ne(r) ] -> { r } + | [ ] -> { RWred Nop, noruleterm (Some loc) } END (** Rewrite arguments *) +{ + let pr_option f = function None -> mt() | Some x -> f x let pr_pattern_squarep= pr_option (fun r -> str "[" ++ pr_rpattern r ++ str "]") let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep @@ -2058,58 +2293,66 @@ let pr_rwarg ((d, m), ((docc, rx), r)) = let pr_ssrrwarg _ _ _ = pr_rwarg +} + ARGUMENT EXTEND ssrpattern_squarep -TYPED AS rpattern option PRINTED BY pr_ssrpattern_squarep - | [ "[" rpattern(rdx) "]" ] -> [ Some rdx ] - | [ ] -> [ None ] +TYPED AS rpattern option PRINTED BY { pr_ssrpattern_squarep } + | [ "[" rpattern(rdx) "]" ] -> { Some rdx } + | [ ] -> { None } END ARGUMENT EXTEND ssrpattern_ne_squarep -TYPED AS rpattern option PRINTED BY pr_ssrpattern_squarep - | [ "[" rpattern(rdx) "]" ] -> [ Some rdx ] +TYPED AS rpattern option PRINTED BY { pr_ssrpattern_squarep } + | [ "[" rpattern(rdx) "]" ] -> { Some rdx } END ARGUMENT EXTEND ssrrwarg - TYPED AS (ssrdir * ssrmult) * ((ssrdocc * rpattern option) * ssrrule) - PRINTED BY pr_ssrrwarg + TYPED AS ((ssrdir * ssrmult) * ((ssrdocc * rpattern option) * ssrrule)) + PRINTED BY { pr_ssrrwarg } | [ "-" ssrmult(m) ssrrwocc(docc) ssrpattern_squarep(rx) ssrrule_ne(r) ] -> - [ mk_rwarg (R2L, m) (docc, rx) r ] + { mk_rwarg (R2L, m) (docc, rx) r } | [ "-/" ssrterm(t) ] -> (* just in case '-/' should become a token *) - [ mk_rwarg (R2L, nomult) norwocc (RWdef, t) ] + { mk_rwarg (R2L, nomult) norwocc (RWdef, t) } | [ ssrmult_ne(m) ssrrwocc(docc) ssrpattern_squarep(rx) ssrrule_ne(r) ] -> - [ mk_rwarg (L2R, m) (docc, rx) r ] + { mk_rwarg (L2R, m) (docc, rx) r } | [ "{" ne_ssrhyp_list(clr) "}" ssrpattern_ne_squarep(rx) ssrrule_ne(r) ] -> - [ mk_rwarg norwmult (mkclr clr, rx) r ] + { mk_rwarg norwmult (mkclr clr, rx) r } | [ "{" ne_ssrhyp_list(clr) "}" ssrrule(r) ] -> - [ mk_rwarg norwmult (mkclr clr, None) r ] + { mk_rwarg norwmult (mkclr clr, None) r } | [ "{" ssrocc(occ) "}" ssrpattern_squarep(rx) ssrrule_ne(r) ] -> - [ mk_rwarg norwmult (mkocc occ, rx) r ] + { mk_rwarg norwmult (mkocc occ, rx) r } | [ "{" "}" ssrpattern_squarep(rx) ssrrule_ne(r) ] -> - [ mk_rwarg norwmult (nodocc, rx) r ] + { mk_rwarg norwmult (nodocc, rx) r } | [ ssrpattern_ne_squarep(rx) ssrrule_ne(r) ] -> - [ mk_rwarg norwmult (noclr, rx) r ] + { mk_rwarg norwmult (noclr, rx) r } | [ ssrrule_ne(r) ] -> - [ mk_rwarg norwmult norwocc r ] + { mk_rwarg norwmult norwocc r } END TACTIC EXTEND ssrinstofruleL2R -| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ V82.tactic (ssrinstancesofrule ist L2R arg) ] +| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> { V82.tactic (ssrinstancesofrule ist L2R arg) } END TACTIC EXTEND ssrinstofruleR2L -| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ V82.tactic (ssrinstancesofrule ist R2L arg) ] +| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> { V82.tactic (ssrinstancesofrule ist R2L arg) } END (** Rewrite argument sequence *) (* type ssrrwargs = ssrrwarg list *) +{ + let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs -ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY pr_ssrrwargs - | [ "YouShouldNotTypeThis" ] -> [ anomaly "Grammar placeholder match" ] +} + +ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs } + | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END +{ + let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true let _ = @@ -2120,57 +2363,70 @@ let _ = Goptions.optdepr = false; Goptions.optwrite = (fun b -> ssr_rw_syntax := b) } +let lbrace = Char.chr 123 +(** Workaround to a limitation of coqpp *) + let test_ssr_rw_syntax = let test strm = if not !ssr_rw_syntax then raise Stream.Failure else if is_ssr_loaded () then () else match Util.stream_nth 0 strm with - | Tok.KEYWORD key when List.mem key.[0] ['{'; '['; '/'] -> () + | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> () | _ -> raise Stream.Failure in Gram.Entry.of_parser "test_ssr_rw_syntax" test -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: ssrrwargs; - ssrrwargs: [[ test_ssr_rw_syntax; a = LIST1 ssrrwarg -> a ]]; + ssrrwargs: [[ test_ssr_rw_syntax; a = LIST1 ssrrwarg -> { a } ]]; END (** The "rewrite" tactic *) TACTIC EXTEND ssrrewrite | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] -> - [ tclCLAUSES (old_tac (ssrrewritetac ist args)) clauses ] + { tclCLAUSES (old_tac (ssrrewritetac ist args)) clauses } END (** The "unlock" tactic *) +{ + let pr_unlockarg (occ, t) = pr_occ occ ++ pr_term t let pr_ssrunlockarg _ _ _ = pr_unlockarg -ARGUMENT EXTEND ssrunlockarg TYPED AS ssrocc * ssrterm - PRINTED BY pr_ssrunlockarg - | [ "{" ssrocc(occ) "}" ssrterm(t) ] -> [ occ, t ] - | [ ssrterm(t) ] -> [ None, t ] +} + +ARGUMENT EXTEND ssrunlockarg TYPED AS (ssrocc * ssrterm) + PRINTED BY { pr_ssrunlockarg } + | [ "{" ssrocc(occ) "}" ssrterm(t) ] -> { occ, t } + | [ ssrterm(t) ] -> { None, t } END +{ + let pr_ssrunlockargs _ _ _ args = pr_list spc pr_unlockarg args +} + ARGUMENT EXTEND ssrunlockargs TYPED AS ssrunlockarg list - PRINTED BY pr_ssrunlockargs - | [ ssrunlockarg_list(args) ] -> [ args ] + PRINTED BY { pr_ssrunlockargs } + | [ ssrunlockarg_list(args) ] -> { args } END TACTIC EXTEND ssrunlock | [ "unlock" ssrunlockargs(args) ssrclauses(clauses) ] -> - [ tclCLAUSES (old_tac (unlocktac ist args)) clauses ] + { tclCLAUSES (old_tac (unlocktac ist args)) clauses } END (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) TACTIC EXTEND ssrpose -| [ "pose" ssrfixfwd(ffwd) ] -> [ V82.tactic (ssrposetac ffwd) ] -| [ "pose" ssrcofixfwd(ffwd) ] -> [ V82.tactic (ssrposetac ffwd) ] -| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> [ V82.tactic (ssrposetac (id, fwd)) ] +| [ "pose" ssrfixfwd(ffwd) ] -> { V82.tactic (ssrposetac ffwd) } +| [ "pose" ssrcofixfwd(ffwd) ] -> { V82.tactic (ssrposetac ffwd) } +| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> { V82.tactic (ssrposetac (id, fwd)) } END (** The "set" tactic *) @@ -2179,7 +2435,7 @@ END TACTIC EXTEND ssrset | [ "set" ssrfwdid(id) ssrsetfwd(fwd) ssrclauses(clauses) ] -> - [ tclCLAUSES (old_tac (ssrsettac id fwd)) clauses ] + { tclCLAUSES (old_tac (ssrsettac id fwd)) clauses } END (** The "have" tactic *) @@ -2190,124 +2446,138 @@ END (* Pltac. *) (* The standard TACTIC EXTEND does not work for abstract *) -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: tactic_expr; tactic_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> - ssrtac_expr ~loc:!@loc "abstract" - [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] ]]; + { ssrtac_expr ~loc "abstract" + [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; END TACTIC EXTEND ssrabstract -| [ "abstract" ssrdgens(gens) ] -> [ +| [ "abstract" ssrdgens(gens) ] -> { if List.length (fst gens) <> 1 then errorstrm (str"dependents switches '/' not allowed here"); - Ssripats.ssrabstract (ssrdgens_of_parsed_dgens gens) ] + Ssripats.ssrabstract (ssrdgens_of_parsed_dgens gens) } END TACTIC EXTEND ssrhave | [ "have" ssrhavefwdwbinders(fwd) ] -> - [ V82.tactic (havetac ist fwd false false) ] + { V82.tactic (havetac ist fwd false false) } END TACTIC EXTEND ssrhavesuff | [ "have" "suff" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - [ V82.tactic (havetac ist (false,(pats,fwd)) true false) ] + { V82.tactic (havetac ist (false,(pats,fwd)) true false) } END TACTIC EXTEND ssrhavesuffices | [ "have" "suffices" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - [ V82.tactic (havetac ist (false,(pats,fwd)) true false) ] + { V82.tactic (havetac ist (false,(pats,fwd)) true false) } END TACTIC EXTEND ssrsuffhave | [ "suff" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - [ V82.tactic (havetac ist (false,(pats,fwd)) true true) ] + { V82.tactic (havetac ist (false,(pats,fwd)) true true) } END TACTIC EXTEND ssrsufficeshave | [ "suffices" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] -> - [ V82.tactic (havetac ist (false,(pats,fwd)) true true) ] + { V82.tactic (havetac ist (false,(pats,fwd)) true true) } END (** The "suffice" tactic *) +{ + let pr_ssrsufffwdwbinders _ _ prt (hpats, (fwd, hint)) = pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint +} + ARGUMENT EXTEND ssrsufffwd - TYPED AS ssrhpats * (ssrfwd * ssrhint) PRINTED BY pr_ssrsufffwdwbinders + TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders } | [ ssrhpats(pats) ssrbinder_list(bs) ":" ast_closure_lterm(t) ssrhint(hint) ] -> - [ let ((clr, pats), binders), simpl = pats in + { let ((clr, pats), binders), simpl = pats in let allbs = intro_id_to_binder binders @ bs in let allbinders = binders @ List.flatten (binder_to_intro_id bs) in let fwd = mkFwdHint ":" t in - (((clr, pats), allbinders), simpl), (bind_fwd allbs fwd, hint) ] + (((clr, pats), allbinders), simpl), (bind_fwd allbs fwd, hint) } END TACTIC EXTEND ssrsuff -| [ "suff" ssrsufffwd(fwd) ] -> [ V82.tactic (sufftac ist fwd) ] +| [ "suff" ssrsufffwd(fwd) ] -> { V82.tactic (sufftac ist fwd) } END TACTIC EXTEND ssrsuffices -| [ "suffices" ssrsufffwd(fwd) ] -> [ V82.tactic (sufftac ist fwd) ] +| [ "suffices" ssrsufffwd(fwd) ] -> { V82.tactic (sufftac ist fwd) } END (** The "wlog" (Without Loss Of Generality) tactic *) (* type ssrwlogfwd = ssrwgen list * ssrfwd *) +{ + let pr_ssrwlogfwd _ _ _ (gens, t) = str ":" ++ pr_list mt pr_wgen gens ++ spc() ++ pr_fwd t -ARGUMENT EXTEND ssrwlogfwd TYPED AS ssrwgen list * ssrfwd - PRINTED BY pr_ssrwlogfwd -| [ ":" ssrwgen_list(gens) "/" ast_closure_lterm(t) ] -> [ gens, mkFwdHint "/" t] +} + +ARGUMENT EXTEND ssrwlogfwd TYPED AS (ssrwgen list * ssrfwd) + PRINTED BY { pr_ssrwlogfwd } +| [ ":" ssrwgen_list(gens) "/" ast_closure_lterm(t) ] -> { gens, mkFwdHint "/" t} END TACTIC EXTEND ssrwlog | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - [ V82.tactic (wlogtac ist pats fwd hint false `NoGen) ] + { V82.tactic (wlogtac ist pats fwd hint false `NoGen) } END TACTIC EXTEND ssrwlogs | [ "wlog" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ] + { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } END TACTIC EXTEND ssrwlogss | [ "wlog" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> - [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ] + { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } END TACTIC EXTEND ssrwithoutloss | [ "without" "loss" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - [ V82.tactic (wlogtac ist pats fwd hint false `NoGen) ] + { V82.tactic (wlogtac ist pats fwd hint false `NoGen) } END TACTIC EXTEND ssrwithoutlosss | [ "without" "loss" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ] + { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } END TACTIC EXTEND ssrwithoutlossss | [ "without" "loss" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> - [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ] + { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } END +{ + (* Generally have *) let pr_idcomma _ _ _ = function | None -> mt() | Some None -> str"_, " | Some (Some id) -> pr_id id ++ str", " -ARGUMENT EXTEND ssr_idcomma TYPED AS ident option option PRINTED BY pr_idcomma - | [ ] -> [ None ] +} + +ARGUMENT EXTEND ssr_idcomma TYPED AS ident option option PRINTED BY { pr_idcomma } + | [ ] -> { None } END +{ + let accept_idcomma strm = match stream_nth 0 strm with | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm @@ -2315,35 +2585,44 @@ let accept_idcomma strm = let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: ssr_idcomma; ssr_idcomma: [ [ test_idcomma; - ip = [ id = IDENT -> Some (Id.of_string id) | "_" -> None ]; "," -> - Some ip + ip = [ id = IDENT -> { Some (Id.of_string id) } | "_" -> { None } ]; "," -> + { Some ip } ] ]; END +{ + let augment_preclr clr1 (((clr0, x),y),z) = (((clr1 @ clr0, x),y),z) +} + TACTIC EXTEND ssrgenhave | [ "gen" "have" ssrclear(clr) ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - [ let pats = augment_preclr clr pats in - V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) ] + { let pats = augment_preclr clr pats in + V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) } END TACTIC EXTEND ssrgenhave2 | [ "generally" "have" ssrclear(clr) ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> - [ let pats = augment_preclr clr pats in - V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) ] + { let pats = augment_preclr clr pats in + V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) } END +{ + (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) let () = CLexer.set_keyword_state frozen_lexer ;; +} (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.mlg index 989a6c5bf1..876751911b 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.mlg @@ -10,6 +10,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +{ + open Names module CoqConstr = Constr open CoqConstr @@ -25,7 +27,6 @@ open Notation_ops open Notation_term open Glob_term open Stdarg -open Genarg open Decl_kinds open Pp open Ppconstr @@ -36,9 +37,12 @@ open Evar_kinds open Ssrprinters open Ssrcommon open Ssrparser + +} + DECLARE PLUGIN "ssreflect_plugin" -let (!@) = Pcoq.to_coqloc +{ (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) @@ -46,7 +50,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************) +(** Alternative notations for "match" and anonymous arguments. *)(* ************) (* Syntax: *) (* if <term> is <pattern> then ... else ... *) @@ -71,60 +75,62 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* as this can't be done from an ML extension file, the new *) (* syntax will only work when ssreflect.v is imported. *) -let no_ct = None, None and no_rt = None in +let no_ct = None, None and no_rt = None let aliasvar = function | [[{ CAst.v = CPatAlias (_, na); loc }]] -> Some na - | _ -> None in -let mk_cnotype mp = aliasvar mp, None in -let mk_ctype mp t = aliasvar mp, Some t in -let mk_rtype t = Some t in -let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt in + | _ -> None +let mk_cnotype mp = aliasvar mp, None +let mk_ctype mp t = aliasvar mp, Some t +let mk_rtype t = Some t +let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt let mk_let ?loc rt ct mp c1 = - CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) in -let mk_pat c (na, t) = (c, na, t) in -GEXTEND Gram + CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) +let mk_pat c (na, t) = (c, na, t) + +} + +GRAMMAR EXTEND Gram GLOBAL: binder_constr; - ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [[p]] ]]; + ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]]; + ssr_mpat: [[ p = pattern -> { [[p]] } ]]; ssr_dpat: [ - [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt - | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt - | mp = ssr_mpat -> mp, no_ct, no_rt + [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } + | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt } + | mp = ssr_mpat -> { mp, no_ct, no_rt } ] ]; - ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; - ssr_else: [[ mp = ssr_elsepat; c = lconstr -> CAst.make ~loc:!@loc (mp, c) ]]; + ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]]; + ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; + ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> - let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) + { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> - let b1, ct, rt = db1 in + { let b1, ct, rt = db1 in let b1, b2 = let open CAst in let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) in - CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) + CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> - mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1 + { mk_let ~loc no_rt [mk_pat c no_ct] mp c1 } | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; rt = ssr_rtype; "in"; c1 = lconstr -> - mk_let ~loc:!@loc rt [mk_pat c (mk_cnotype mp)] mp c1 + { mk_let ~loc rt [mk_pat c (mk_cnotype mp)] mp c1 } | "let"; ":"; mp = ssr_mpat; "in"; t = pattern; ":="; c = lconstr; rt = ssr_rtype; "in"; c1 = lconstr -> - mk_let ~loc:!@loc rt [mk_pat c (mk_ctype mp t)] mp c1 + { mk_let ~loc rt [mk_pat c (mk_ctype mp t)] mp c1 } ] ]; END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: closed_binder; closed_binder: [ - [ ["of" | "&"]; c = operconstr LEVEL "99" -> - [CLocalAssum ([CAst.make ~loc:!@loc Anonymous], Default Explicit, c)] + [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> + { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] } ] ]; END -(* }}} *) -(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************) +(** Vernacular commands: Prenex Implicits and Search *)(***********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -138,6 +144,8 @@ END (* Prenex Implicits for all the visible constants that had been *) (* declared as Prenex Implicits. *) +{ + let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f @@ -159,23 +167,24 @@ let declare_one_prenex_implicit locality f = | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] -VERNAC COMMAND FUNCTIONAL EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF +} + +VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF | [ "Prenex" "Implicits" ne_global_list(fl) ] - -> [ fun ~atts ~st -> + -> { let open Vernacinterp in let locality = Locality.make_section_locality atts.locality in List.iter (declare_one_prenex_implicit locality) fl; - st - ] + } END (* Vernac grammar visibility patch *) -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) + { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) } ] ] ; END @@ -184,6 +193,8 @@ END (* Main prefilter *) +{ + type raw_glob_search_about_item = | RGlobSearchSubPattern of constr_expr | RGlobSearchString of Loc.t * string * string option @@ -303,24 +314,32 @@ let interp_search_notation ?loc tag okey = let _, npat = Patternops.pattern_of_glob_constr (sub () body) in Search.GlobSearchSubPattern npat +} + ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem - PRINTED BY pr_ssr_search_item - | [ string(s) ] -> [ RGlobSearchString (loc,s,None) ] - | [ string(s) "%" preident(key) ] -> [ RGlobSearchString (loc,s,Some key) ] - | [ constr_pattern(p) ] -> [ RGlobSearchSubPattern p ] + PRINTED BY { pr_ssr_search_item } + | [ string(s) ] -> { RGlobSearchString (loc,s,None) } + | [ string(s) "%" preident(key) ] -> { RGlobSearchString (loc,s,Some key) } + | [ constr_pattern(p) ] -> { RGlobSearchSubPattern p } END +{ + let pr_ssr_search_arg _ _ _ = let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item p in pr_list spc pr_item +} + ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list - PRINTED BY pr_ssr_search_arg - | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> [ (false, p) :: a ] - | [ ssr_search_item(p) ssr_search_arg(a) ] -> [ (true, p) :: a ] - | [ ] -> [ [] ] + PRINTED BY { pr_ssr_search_arg } + | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> { (false, p) :: a } + | [ ssr_search_item(p) ssr_search_arg(a) ] -> { (true, p) :: a } + | [ ] -> { [] } END +{ + (* Main type conclusion pattern filter *) let rec splay_search_pattern na = function @@ -419,16 +438,20 @@ let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc let pr_ssr_modlocs _ _ _ ml = if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml -ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY pr_ssr_modlocs - | [ ] -> [ [] ] +} + +ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY { pr_ssr_modlocs } + | [ ] -> { [] } END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: ssr_modlocs; - modloc: [[ "-"; m = global -> true, m | m = global -> false, m]]; - ssr_modlocs: [[ "in"; ml = LIST1 modloc -> ml ]]; + modloc: [[ "-"; m = global -> { true, m } | m = global -> { false, m } ]]; + ssr_modlocs: [[ "in"; ml = LIST1 modloc -> { ml } ]]; END +{ + let interp_modloc mr = let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> @@ -446,20 +469,20 @@ let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in Feedback.msg_info (hov 2 pr_res ++ fnl ()) +} + VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> - [ let hpat = interp_search_arg a in + { let hpat = interp_search_arg a in let in_mod = interp_modloc mr in let post_filter gr env typ = in_mod gr env typ && hpat gr env typ in let display gr env typ = if post_filter gr env typ then ssrdisplaysearch gr env typ in - Search.generic_search None display ] + Search.generic_search None display } END -(* }}} *) - -(** View hint database and View application. *)(* {{{ ******************************) +(** View hint database and View application. *)(* ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) @@ -467,6 +490,8 @@ END (* View hints *) +{ + let pr_raw_ssrhintref prc _ _ = let open CAst in function | { v = CAppExpl ((None, r,x), args) } when isCHoles args -> prc (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args) @@ -490,14 +515,19 @@ let mkhintref ?loc c n = match c.CAst.v with | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((None, r, x), mkCHoles ?loc n) | _ -> mkAppC (c, mkCHoles ?loc n) +} + ARGUMENT EXTEND ssrhintref - PRINTED BY pr_ssrhintref - RAW_TYPED AS constr RAW_PRINTED BY pr_raw_ssrhintref - GLOB_TYPED AS constr GLOB_PRINTED BY pr_glob_ssrhintref - | [ constr(c) ] -> [ c ] - | [ constr(c) "|" natural(n) ] -> [ mkhintref ~loc c n ] + TYPED AS constr + PRINTED BY { pr_ssrhintref } + RAW_PRINTED BY { pr_raw_ssrhintref } + GLOB_PRINTED BY { pr_glob_ssrhintref } + | [ constr(c) ] -> { c } + | [ constr(c) "|" natural(n) ] -> { mkhintref ~loc c n } END +{ + (* View purpose *) let pr_viewpos = function @@ -508,70 +538,82 @@ let pr_viewpos = function let pr_ssrviewpos _ _ _ = pr_viewpos -ARGUMENT EXTEND ssrviewpos PRINTED BY pr_ssrviewpos - | [ "for" "move" "/" ] -> [ Some Ssrview.AdaptorDb.Forward ] - | [ "for" "apply" "/" ] -> [ Some Ssrview.AdaptorDb.Backward ] - | [ "for" "apply" "/" "/" ] -> [ Some Ssrview.AdaptorDb.Equivalence ] - | [ "for" "apply" "//" ] -> [ Some Ssrview.AdaptorDb.Equivalence ] - | [ ] -> [ None ] +} + +ARGUMENT EXTEND ssrviewpos PRINTED BY { pr_ssrviewpos } + | [ "for" "move" "/" ] -> { Some Ssrview.AdaptorDb.Forward } + | [ "for" "apply" "/" ] -> { Some Ssrview.AdaptorDb.Backward } + | [ "for" "apply" "/" "/" ] -> { Some Ssrview.AdaptorDb.Equivalence } + | [ "for" "apply" "//" ] -> { Some Ssrview.AdaptorDb.Equivalence } + | [ ] -> { None } END +{ + let pr_ssrviewposspc _ _ _ i = pr_viewpos i ++ spc () -ARGUMENT EXTEND ssrviewposspc TYPED AS ssrviewpos PRINTED BY pr_ssrviewposspc - | [ ssrviewpos(i) ] -> [ i ] +} + +ARGUMENT EXTEND ssrviewposspc TYPED AS ssrviewpos PRINTED BY { pr_ssrviewposspc } + | [ ssrviewpos(i) ] -> { i } END +{ + let print_view_hints kind l = let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in let pp_hints = pr_list spc pr_rawhintref l in Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) +} + VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY | [ "Print" "Hint" "View" ssrviewpos(i) ] -> - [ match i with + { match i with | Some k -> print_view_hints k (Ssrview.AdaptorDb.get k) | None -> List.iter (fun k -> print_view_hints k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; Ssrview.AdaptorDb.Equivalence ] - ] + } END +{ + let glob_view_hints lvh = List.map (Constrintern.intern_constr (Global.env ()) (Evd.from_env (Global.env ()))) lvh +} + VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF | [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] -> - [ let hints = glob_view_hints lvh in + { let hints = glob_view_hints lvh in match n with | None -> Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Forward hints; Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Backward hints | Some k -> - Ssrview.AdaptorDb.declare k hints ] + Ssrview.AdaptorDb.declare k hints } END -(* }}} *) - (** Canonical Structure alias *) -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: gallina_ext; gallina_ext: (* Canonical structure *) [[ IDENT "Canonical"; qid = Constr.global -> - Vernacexpr.VernacCanonical (CAst.make @@ AN qid) + { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) } | IDENT "Canonical"; ntn = Prim.by_notation -> - Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) + { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) } | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> - let s = coerce_reference_to_id qid in + { let s = coerce_reference_to_id qid in Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((CAst.make (Name s)),None), d) + ((CAst.make (Name s)),None), d) } ]]; END @@ -589,30 +631,34 @@ END (* Coq v8.3 defines "by" as a keyword, some hacks are not needed any *) (* longer and thus comment out. Such comments are marked with v8.3 *) +{ + open Pltac -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: hypident; hypident: [ - [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, Locus.InHypTypeOnly - | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, Locus.InHypValueOnly + [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypTypeOnly } + | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypValueOnly } ] ]; END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: hloc; hloc: [ [ "in"; "("; "Type"; "of"; id = ident; ")" -> - Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly) + { Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly) } | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> - Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly) + { Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly) } ] ]; END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: constr_eval; constr_eval: [ - [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ] + [ IDENT "type"; "of"; c = Constr.constr -> { Genredexpr.ConstrTypeOf c }] ]; END @@ -620,6 +666,10 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) +{ + let () = CLexer.set_keyword_state frozen_lexer ;; +} + (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.mlg index 746c368aa9..3f0794fdd4 100644 --- a/plugins/ssrmatching/g_ssrmatching.ml4 +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -8,8 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin -open Genarg open Pcoq open Pcoq.Constr open Ssrmatching @@ -19,83 +20,101 @@ open Ssrmatching.Internal * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; +} + DECLARE PLUGIN "ssrmatching_plugin" +{ + let pr_rpattern _ _ _ = pr_rpattern +} + ARGUMENT EXTEND rpattern TYPED AS rpatternty - PRINTED BY pr_rpattern - INTERPRETED BY interp_rpattern - GLOBALIZED BY glob_rpattern - SUBSTITUTED BY subst_rpattern - | [ lconstr(c) ] -> [ mk_rpattern (T (mk_lterm c None)) ] - | [ "in" lconstr(c) ] -> [ mk_rpattern (In_T (mk_lterm c None)) ] + PRINTED BY { pr_rpattern } + INTERPRETED BY { interp_rpattern } + GLOBALIZED BY { glob_rpattern } + SUBSTITUTED BY { subst_rpattern } + | [ lconstr(c) ] -> { mk_rpattern (T (mk_lterm c None)) } + | [ "in" lconstr(c) ] -> { mk_rpattern (In_T (mk_lterm c None)) } | [ lconstr(x) "in" lconstr(c) ] -> - [ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) ] + { mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) } | [ "in" lconstr(x) "in" lconstr(c) ] -> - [ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) ] + { mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) } | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> - [ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ] + { mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) } | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> - [ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ] + { mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) } END +{ + let pr_ssrterm _ _ _ = pr_ssrterm +} + ARGUMENT EXTEND cpattern - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "Qed" constr(c) ] -> [ mk_lterm c None ] + PRINTED BY { pr_ssrterm } + INTERPRETED BY { interp_ssrterm } + GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm } + RAW_PRINTED BY { pr_ssrterm } + GLOB_PRINTED BY { pr_ssrterm } +| [ "Qed" constr(c) ] -> { mk_lterm c None } END +{ + let input_ssrtermkind strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: cpattern; - cpattern: [[ k = ssrtermkind; c = constr -> + cpattern: [[ k = ssrtermkind; c = constr -> { let pattern = mk_term k c None in - if loc_of_cpattern pattern <> Some !@loc && k = '(' + if loc_of_cpattern pattern <> Some loc && k = '(' then mk_term 'x' c None - else pattern ]]; + else pattern } ]]; END ARGUMENT EXTEND lcpattern TYPED AS cpattern - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ] + PRINTED BY { pr_ssrterm } + INTERPRETED BY { interp_ssrterm } + GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm } + RAW_PRINTED BY { pr_ssrterm } + GLOB_PRINTED BY { pr_ssrterm } +| [ "Qed" lconstr(c) ] -> { mk_lterm c None } END -GEXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: lcpattern; - lcpattern: [[ k = ssrtermkind; c = lconstr -> + lcpattern: [[ k = ssrtermkind; c = lconstr -> { let pattern = mk_term k c None in - if loc_of_cpattern pattern <> Some !@loc && k = '(' + if loc_of_cpattern pattern <> Some loc && k = '(' then mk_term 'x' c None - else pattern ]]; + else pattern } ]]; END -ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern -| [ rpattern(pat) ] -> [ pat ] +ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern } +| [ rpattern(pat) ] -> { pat } END TACTIC EXTEND ssrinstoftpat -| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ] +| [ "ssrinstancesoftpat" cpattern(arg) ] -> { Proofview.V82.tactic (ssrinstancesof arg) } END +{ + (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) let () = CLexer.set_keyword_state frozen_lexer ;; + +} diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.mlg index 55f61a58f9..5dbc9eea7a 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.mlg @@ -10,6 +10,8 @@ DECLARE PLUGIN "numeral_notation_plugin" +{ + open Notation open Numeral open Pp @@ -24,15 +26,17 @@ let pr_numnot_option _ _ _ = function | Warning n -> str "(warning after " ++ str n ++ str ")" | Abstract n -> str "(abstract after " ++ str n ++ str ")" +} + ARGUMENT EXTEND numnotoption - PRINTED BY pr_numnot_option -| [ ] -> [ Nop ] -| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ] -| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ] + PRINTED BY { pr_numnot_option } +| [ ] -> { Nop } +| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } +| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n } END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ] + { vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o } END |
