From b0a2e7dd8c9d26fc239e941b6445823c49a7d535 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 23 Nov 2023 15:51:15 +0100 Subject: [PATCH] Put parts of ltac2_plugin which depend on ltac1 in a separate plugin This requires a new `ltac2_ltac1_common_plugin` for things used by both (profile_ltac, goal selectors and the "use_default" `...` syntax). We could also put that stuff in vernac/. For now we still load the split off parts in Ltac2.Init. It could also make sense to load it in Ltac2.Ltac1 (and require that in Ltac2.Notations as a few notations use `ltac1:()`). --- doc/Makefile.docgram | 3 +- lib/core_plugins_findlib_compat.ml | 2 + plugins/ltac/dune | 2 +- plugins/ltac/g_ltac.mlg | 60 +--- plugins/ltac/g_ltac.mli | 12 - plugins/ltac/pptactic.ml | 14 + plugins/ltac/pptactic.mli | 1 + plugins/ltac/profile_ltac_tactics.mlg | 2 +- plugins/ltac/tacinterp.ml | 16 +- plugins/ltac2/dune | 2 +- plugins/ltac2/g_ltac2.mlg | 48 +-- plugins/ltac2/g_ltac2.mli | 4 +- plugins/ltac2/tac2bt.ml | 2 +- plugins/ltac2/tac2core.ml | 300 +--------------- plugins/ltac2/tac2core.mli | 3 + plugins/ltac2/tac2quote.ml | 2 - plugins/ltac2/tac2quote.mli | 6 - plugins/ltac2_ltac1/dune | 7 + plugins/ltac2_ltac1/g_ltac2_ltac1.mlg | 41 +++ plugins/ltac2_ltac1/g_ltac2_ltac1.mli | 9 + plugins/ltac2_ltac1/ltac2_ltac1_plugin.mllib | 0 plugins/ltac2_ltac1/tac2core_ltac1.ml | 329 ++++++++++++++++++ plugins/ltac2_ltac1/tac2core_ltac1.mli | 9 + plugins/ltac2_ltac1/tac2quote_ltac1.ml | 4 + plugins/ltac2_ltac1/tac2quote_ltac1.mli | 18 + plugins/ltac2_ltac1_common/dune | 7 + .../g_ltac2_ltac1_common.mlg | 71 ++++ .../g_ltac2_ltac1_common.mli | 21 ++ .../ltac2_ltac1_common_plugin.mllib | 0 .../profile_ltac.ml | 21 -- .../profile_ltac.mli | 5 - test-suite/bugs/bug_3612.v | 1 + test-suite/bugs/bug_3649.v | 1 + test-suite/stm/classify_set_proof_mode_9093.v | 1 + test-suite/success/Discriminate_HoTT.v | 1 + theories/Init/Ltac.v | 1 + user-contrib/Ltac2/Init.v | 1 + user-contrib/Ltac2/Ltac1.v | 20 +- 38 files changed, 593 insertions(+), 454 deletions(-) create mode 100644 plugins/ltac2_ltac1/dune create mode 100644 plugins/ltac2_ltac1/g_ltac2_ltac1.mlg create mode 100644 plugins/ltac2_ltac1/g_ltac2_ltac1.mli create mode 100644 plugins/ltac2_ltac1/ltac2_ltac1_plugin.mllib create mode 100644 plugins/ltac2_ltac1/tac2core_ltac1.ml create mode 100644 plugins/ltac2_ltac1/tac2core_ltac1.mli create mode 100644 plugins/ltac2_ltac1/tac2quote_ltac1.ml create mode 100644 plugins/ltac2_ltac1/tac2quote_ltac1.mli create mode 100644 plugins/ltac2_ltac1_common/dune create mode 100644 plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mlg create mode 100644 plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mli create mode 100644 plugins/ltac2_ltac1_common/ltac2_ltac1_common_plugin.mllib rename plugins/{ltac => ltac2_ltac1_common}/profile_ltac.ml (95%) rename plugins/{ltac => ltac2_ltac1_common}/profile_ltac.mli (97%) diff --git a/doc/Makefile.docgram b/doc/Makefile.docgram index b82046fcc433b..b667471bf255a 100644 --- a/doc/Makefile.docgram +++ b/doc/Makefile.docgram @@ -30,7 +30,8 @@ DOC_MLGS := \ plugins/ring/g_ring.mlg \ plugins/rtauto/g_rtauto.mlg \ plugins/syntax/g_number_string.mlg \ - plugins/ltac2/g_ltac2.mlg + plugins/ltac2/g_ltac2.mlg plugins/ltac2_ltac1/g_ltac2_ltac1.mlg \ + plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mlg DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst) diff --git a/lib/core_plugins_findlib_compat.ml b/lib/core_plugins_findlib_compat.ml index 9201fc1ed7e76..4421a6ccd4589 100644 --- a/lib/core_plugins_findlib_compat.ml +++ b/lib/core_plugins_findlib_compat.ml @@ -21,6 +21,8 @@ let legacy_to_findlib = [ ("extraction_plugin", ["plugins";"extraction"]) ; ("funind_plugin", ["plugins";"funind"]) ; ("ltac2_plugin", ["plugins";"ltac2"]) ; + ("ltac2_ltac1_plugin", ["plugins";"ltac2_ltac1"]) ; + ("ltac2_ltac1_common_plugin", ["plugins";"ltac2_ltac1_common"]) ; ("nsatz_plugin", ["plugins";"nsatz"]) ; ("rtauto_plugin", ["plugins";"rtauto"]) ; ("ssrmatching_plugin", ["plugins";"ssrmatching"]) ; diff --git a/plugins/ltac/dune b/plugins/ltac/dune index f86ce761b3d34..7d9768b310972 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -3,7 +3,7 @@ (public_name coq-core.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) - (libraries coq-core.vernac)) + (libraries ltac2_ltac1_common_plugin)) (library (name tauto_plugin) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 4f044c31a4efc..a1dc3398e9d15 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -27,6 +27,8 @@ open Pcoq.Constr open Pvernac.Vernac_ open Pltac +open Ltac2_ltac1_common_plugin.G_ltac2_ltac1_common + let fail_default_value = Locus.ArgArg 0 let arg_of_expr = function @@ -48,19 +50,11 @@ let reference_to_id qid = let tactic_mode = Entry.make "tactic_command" -let toplevel_selector = Entry.make "toplevel_selector" let tacdef_body = Entry.make "tacdef_body" (* Registers [tactic_mode] as a parser for proof editing *) let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - let open Pcoq.Lookahead in - to_entry "test_bracket_ident" begin - lk_kw "[" >> lk_ident - end - (* Tactics grammar rules *) let hint = G_proofs.hint @@ -71,7 +65,7 @@ let for_extraargs = () GRAMMAR EXTEND Gram GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint - tactic_mode constr_may_eval constr_eval toplevel_selector + tactic_mode constr_may_eval constr_eval term; tactic_then_last: @@ -119,7 +113,7 @@ GRAMMAR EXTEND Gram | IDENT "abstract"; tc = NEXT -> { CAst.make ~loc (TacAbstract (tc,None)) } | IDENT "abstract"; tc = NEXT; "using"; s = ident -> { CAst.make ~loc (TacAbstract (tc,Some s)) } - | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { CAst.make ~loc (TacSelect (sel, ta)) } ] + | IDENT "only"; sel = goal_selector; ":"; ta = ltac_expr -> { CAst.make ~loc (TacSelect (sel, ta)) } ] (*End of To do*) | "2" RIGHTA [ ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { CAst.make ~loc (TacOr (ta0,ta1)) } @@ -293,30 +287,6 @@ GRAMMAR EXTEND Gram [ [ tac = ltac_expr -> { tac } ] ] ; - range_selector: - [ [ 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) } - | 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 } ] ] - ; - selector: - [ [ l = range_selector_or_nth -> { l } - | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] - ; - toplevel_selector: - [ [ sel = selector; ":" -> { sel } - | "!"; ":" -> { Goal_select.SelectAlreadyFocused } - | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] - ; tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { Vernacexpr.VernacSynPure (tac g) } | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSynPure (Vernacexpr.VernacSubproof g) } ] ] @@ -348,16 +318,6 @@ open Tacarg open Vernacextend open Libnames -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 } -END - -{ - let pr_ltac_info n = str "Info" ++ spc () ++ int n } @@ -368,18 +328,6 @@ 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 } -END - -{ - let rm_abstract tac = let (loc, tac2) = CAst.(tac.loc, tac.v) in match tac2 with diff --git a/plugins/ltac/g_ltac.mli b/plugins/ltac/g_ltac.mli index 8012378a84201..62418a111975d 100644 --- a/plugins/ltac/g_ltac.mli +++ b/plugins/ltac/g_ltac.mli @@ -25,28 +25,16 @@ val in_tac : val tactic_mode : Vernacexpr.vernac_expr Pcoq.Entry.t -val toplevel_selector : Goal_select.t Pcoq.Entry.t - val tacdef_body : Tacexpr.tacdef_body Pcoq.Entry.t val classic_proof_mode : Pvernac.proof_mode -val test_bracket_ident : unit Pcoq.Entry.t - val hint : Vernacexpr.hints_expr Pcoq.Entry.t -val wit_ltac_selector : (Goal_select.t, unit, unit) Genarg.genarg_type - -val ltac_selector : Goal_select.t Pcoq.Entry.t - val wit_ltac_info : (int, unit, unit) Genarg.genarg_type val ltac_info : int Pcoq.Entry.t -val wit_ltac_use_default : (bool, unit, unit) Genarg.genarg_type - -val ltac_use_default : bool Pcoq.Entry.t - val wit_ltac_tactic_level : (int, unit, unit) Genarg.genarg_type val ltac_tactic_level : int Pcoq.Entry.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 801294e7578c8..79ee854ed63e1 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1179,6 +1179,20 @@ let pr_goal_selector ~toplevel s = let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c +let pp_ltac_call_kind = function + | LtacNotationCall s -> pr_alias_key s + | LtacNameCall cst -> pr_ltac_constant cst + (* todo: don't want the KerName instead? *) + | LtacVarCall (_, id, t) -> Names.Id.print id + | LtacAtomCall te -> + pr_glob_tactic (Global.env ()) + (CAst.make (TacAtom te)) + | LtacConstrInterp (env, sigma, c, _) -> + pr_glob_constr_env env sigma c + | LtacMLCall te -> + (pr_glob_tactic (Global.env ()) + te) + let declare_extra_genarg_pprule wit (f : 'a raw_extra_genarg_printer) (g : 'b glob_extra_genarg_printer) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 77931a3681971..581daa546d3a7 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -156,6 +156,7 @@ val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> val pr_value : entry_relative_level -> Val.t -> Pp.t +val pp_ltac_call_kind : ltac_call_kind -> Pp.t val ltop : entry_relative_level diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index 203f51366c6cc..a3605ee53106c 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -12,7 +12,7 @@ (** Ltac profiling entrypoints *) -open Profile_ltac +open Ltac2_ltac1_common_plugin.Profile_ltac open Stdarg } diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 7a64d21d60cbd..8e2817f521582 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -42,6 +42,12 @@ open Proofview.Notations open Context.Named.Declaration open Ltac_pretype +let do_profile trace ?count_call tac = + Ltac2_ltac1_common_plugin.Profile_ltac.do_profile_gen (function + | (_, c) :: _ -> Some (Pptactic.pp_ltac_call_kind c) + | [] -> None) + trace ?count_call tac + let ltac_trace_info = Tactic_debug.ltac_trace_info let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> @@ -1109,7 +1115,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = | TacAtom t -> let call = LtacAtomCall t in let (stack, _) = push_trace(loc,call) ist in - Profile_ltac.do_profile stack + do_profile stack (catch_error_tac_loc loc stack (interp_atomic ist t)) | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) @@ -1142,7 +1148,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = | TacAbstract (t,ido) -> let call = LtacMLCall tac in let (stack,_) = push_trace(None,call) ist in - Profile_ltac.do_profile stack + do_profile stack (catch_error_tac stack begin Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) @@ -1264,7 +1270,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = already in another global reference *) let ist = ensure_loc loc ist in let (stack, _) = trace in - Profile_ltac.do_profile stack ~count_call:false + do_profile stack ~count_call:false (catch_error_tac_loc (* loc for interpretation *) loc stack (val_interp ~appl ist (Tacenv.interp_ltac r))) @@ -1339,7 +1345,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace trace } in let (stack, _) = trace in - Profile_ltac.do_profile stack ~count_call:false + do_profile stack ~count_call:false (catch_error_tac_loc loc stack (val_interp (ensure_loc loc ist) body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end @@ -1392,7 +1398,7 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace (if !Flags.profile_ltac then ([],[]) else trace); } in let tac = name_if_glob appl (eval_tactic_ist ist t) in let (stack, _) = trace in - Profile_ltac.do_profile stack (catch_error_tac_loc loc stack tac) + do_profile stack (catch_error_tac_loc loc stack tac) | VFun (appl,(stack,_),loc,vmap,vars,_) -> let tactic_nm = match appl with diff --git a/plugins/ltac2/dune b/plugins/ltac2/dune index 233257cda7c83..1387895aeb343 100644 --- a/plugins/ltac2/dune +++ b/plugins/ltac2/dune @@ -3,6 +3,6 @@ (public_name coq-core.plugins.ltac2) (synopsis "Ltac2 plugin") (modules_without_implementation tac2expr tac2qexpr tac2types) - (libraries coq-core.plugins.ltac)) + (libraries ltac2_ltac1_common_plugin)) (coq.pp (modules g_ltac2)) diff --git a/plugins/ltac2/g_ltac2.mlg b/plugins/ltac2/g_ltac2.mlg index 5dbce598423ce..2743418d090e2 100644 --- a/plugins/ltac2/g_ltac2.mlg +++ b/plugins/ltac2/g_ltac2.mlg @@ -16,11 +16,11 @@ open Pp open Util open Names open Pcoq +open Pcoq.Prim open Attributes open Constrexpr open Tac2expr open Tac2qexpr -open Ltac_plugin let lk_ident_or_anti = Pcoq.Lookahead.(lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space)) @@ -110,16 +110,14 @@ let tac2def_ext = Entry.make "tac2def_ext" let tac2def_syn = Entry.make "tac2def_syn" let tac2def_mut = Entry.make "tac2def_mut" let tac2mode = Entry.make "ltac2_command" +let tactic_atom = Entry.make "tactic_atom" -let ltac_expr = Pltac.ltac_expr let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x) let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c -let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e -let inj_ltac1val loc e = inj_wit Tac2quote.wit_ltac1val loc e let pattern_of_qualid qid = if Tac2env.is_constructor qid then CAst.make ?loc:qid.CAst.loc @@ CPatRef (RelId qid, []) @@ -142,7 +140,7 @@ let opt_fun ?loc args ty e = GRAMMAR EXTEND Gram GLOBAL: ltac2_expr ltac2_type tac2def_val tac2def_typ tac2def_ext tac2def_syn - tac2def_mut tac2expr_in_env; + tac2def_mut tac2expr_in_env tactic_atom; tac2pat: [ "1" LEFTA [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> { @@ -157,7 +155,7 @@ GRAMMAR EXTEND Gram | p = tac2pat; "|"; pl = LIST1 tac2pat SEP "|" -> { let pl = p :: pl in CAst.make ~loc @@ CPatOr pl } - | p = tac2pat; "as"; id = lident -> { CAst.make ~loc @@ CPatAs (p,id) } + | p = tac2pat; "as"; id = identref -> { CAst.make ~loc @@ CPatAs (p,id) } ] | "0" [ "_" -> { CAst.make ~loc @@ CPatVar Anonymous } @@ -270,25 +268,18 @@ GRAMMAR EXTEND Gram else CAst.make ~loc @@ CTacRef (RelId qid) } | "@"; id = Prim.ident -> { Tac2quote.of_ident (CAst.make ~loc id) } - | "&"; id = lident -> { Tac2quote.of_hyp ~loc id } + | "&"; id = identref -> { Tac2quote.of_hyp ~loc id } | "'"; c = Constr.constr -> { inj_open_constr loc c } | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c } | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c } | IDENT "preterm"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_preterm c } - | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c } + | IDENT "ident"; ":"; "("; c = identref; ")" -> { Tac2quote.of_ident c } | IDENT "pat"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c } | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c } - | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid } - | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid } - ] ] - ; - ltac1_expr_in_env: - [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac_expr -> { ids, e } - | e = ltac_expr -> { [], e } ] ] ; tac2expr_in_env : - [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac2_expr -> + [ [ test_ltac1_env; ids = LIST0 identref; "|-"; e = ltac2_expr -> { let check { CAst.v = id; CAst.loc = loc } = if Tac2env.is_constructor (Libnames.qualid_of_ident ?loc id) then CErrors.user_err ?loc Pp.(str "Invalid bound Ltac2 identifier " ++ Id.print id) @@ -341,9 +332,6 @@ GRAMMAR EXTEND Gram | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) } ] ]; - locident: - [ [ id = Prim.ident -> { CAst.make ~loc id } ] ] - ; binder: [ [ "_" -> { CAst.make ~loc Anonymous } | l = Prim.ident -> { CAst.make ~loc (Name l) } ] ] @@ -362,7 +350,7 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_mut: - [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = ltac2_expr -> { StrMut (qid, old, e) } ] ] + [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = identref -> { id } ]; ":="; e = ltac2_expr -> { StrMut (qid, old, e) } ] ] ; tac2typ_knd: [ [ t = ltac2_type -> { CTydDef (Some t) } @@ -444,7 +432,7 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_ext: - [ [ "@"; IDENT "external"; id = locident; ":"; t = ltac2_type LEVEL "5"; ":="; + [ [ "@"; IDENT "external"; id = identref; ":"; t = ltac2_type LEVEL "5"; ":="; plugin = Prim.string; name = Prim.string -> { let ml = { mltac_plugin = plugin; mltac_tactic = name } in StrPrm (id, t, ml) } @@ -474,9 +462,6 @@ GRAMMAR EXTEND Gram { (toks, n, e) } ] ] ; - lident: - [ [ id = Prim.ident -> { CAst.make ~loc id } ] ] - ; globref: [ [ "&"; id = Prim.ident -> { CAst.make ~loc (QHypothesis id) } | qid = Prim.qualid -> { CAst.make ~loc @@ QReference qid } @@ -501,13 +486,10 @@ GRAMMAR EXTEND Gram [ [ "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) } ] ] ; ident_or_anti: - [ [ id = lident -> { QExpr id } + [ [ id = identref -> { QExpr id } | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) } ] ] ; - lident: - [ [ id = Prim.ident -> { CAst.make ~loc id } ] ] - ; lnatural: [ [ n = Prim.natural -> { CAst.make ~loc n } ] ] ; @@ -517,7 +499,7 @@ GRAMMAR EXTEND Gram qhyp: [ [ x = anti -> { x } | n = lnatural -> { QExpr (CAst.make ~loc @@ QAnonHyp n) } - | id = lident -> { QExpr (CAst.make ~loc @@ QNamedHyp id) } + | id = identref -> { QExpr (CAst.make ~loc @@ QNamedHyp id) } ] ] ; simple_binding: @@ -572,9 +554,9 @@ GRAMMAR EXTEND Gram | test_leftsquarebracket_equal; "["; "="; tc = intropatterns; "]" -> { CAst.make ~loc @@ QIntroInjection tc } ] ] ; naming_intropattern: - [ [ LEFTQMARK; id = lident -> + [ [ LEFTQMARK; id = identref -> { CAst.make ~loc @@ QIntroFresh (QExpr id) } - | "?$"; id = lident -> + | "?$"; id = identref -> { CAst.make ~loc @@ QIntroFresh (QAnti id) } | "?" -> { CAst.make ~loc @@ QIntroAnonymous } @@ -629,7 +611,7 @@ GRAMMAR EXTEND Gram ; destruction_arg: [ [ n = lnatural -> { CAst.make ~loc @@ QElimOnAnonHyp n } - | id = lident -> { CAst.make ~loc @@ QElimOnIdent id } + | id = identref -> { CAst.make ~loc @@ QElimOnIdent id } | c = constr_with_bindings -> { CAst.make ~loc @@ QElimOnConstr c } ] ] ; @@ -1035,8 +1017,8 @@ END let _ = Pvernac.register_proof_mode "Ltac2" tac2mode -open G_ltac open Vernacextend +open Ltac2_ltac1_common_plugin.G_ltac2_ltac1_common } diff --git a/plugins/ltac2/g_ltac2.mli b/plugins/ltac2/g_ltac2.mli index dbe3c65839a4b..17aa24402209d 100644 --- a/plugins/ltac2/g_ltac2.mli +++ b/plugins/ltac2/g_ltac2.mli @@ -47,8 +47,6 @@ val tac2def_mut : Tac2expr.strexpr Pcoq.Entry.t val tac2mode : Vernacexpr.vernac_expr Pcoq.Entry.t -val ltac_expr : Ltac_plugin.Tacexpr.raw_tactic_expr Pcoq.Entry.t - val tac2expr_in_env : (Names.Id.t CAst.t list * Tac2expr.raw_tacexpr) Pcoq.Entry.t @@ -71,3 +69,5 @@ val wit_ltac2_expr : (Tac2expr.raw_tacexpr, unit, unit) Genarg.genarg_type val ltac2_expr : Tac2expr.raw_tacexpr Pcoq.Entry.t + +val tactic_atom : Tac2expr.raw_tacexpr Pcoq.Entry.t diff --git a/plugins/ltac2/tac2bt.ml b/plugins/ltac2/tac2bt.ml index 596ecfa279479..59d95d29a7f76 100644 --- a/plugins/ltac2/tac2bt.ml +++ b/plugins/ltac2/tac2bt.ml @@ -68,5 +68,5 @@ let with_frame frame tac = in if !ltac2_in_ltac1_profiling then let pr_frame f = Some (Hook.get pr_frame f) in - Ltac_plugin.Profile_ltac.do_profile_gen pr_frame frame ~count_call:true tac + Ltac2_ltac1_common_plugin.Profile_ltac.do_profile_gen pr_frame frame ~count_call:true tac else tac diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 4548412a6f45c..c775b33a145cd 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -77,15 +77,16 @@ let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n)) let std_core n = core_prefix Tac2env.std_prefix n let coq_core n = core_prefix Tac2env.coq_prefix n -let ltac1_core n = core_prefix Tac2env.ltac1_prefix n module Core = struct +let t_unit = coq_core "unit" +let v_unit = Tac2ffi.of_unit () + let t_int = coq_core "int" let t_string = coq_core "string" let t_array = coq_core "array" -let t_unit = coq_core "unit" let t_list = coq_core "list" let t_constr = coq_core "constr" let t_preterm = coq_core "preterm" @@ -94,7 +95,6 @@ let t_ident = coq_core "ident" let t_option = coq_core "option" let t_exn = coq_core "exn" let t_reference = std_core "reference" -let t_ltac1 = ltac1_core "t" let c_nil = coq_core "[]" let c_cons = coq_core "::" @@ -109,7 +109,6 @@ end open Core -let v_unit = Tac2ffi.of_unit () let v_blk = Valexpr.make_block let of_relevance = function @@ -1267,75 +1266,6 @@ let () = define "projection_to_constant" (projection @-> ret (option constant)) @@ fun p -> Some (Projection.constant p) -(** Ltac1 in Ltac2 *) - -let ltac1 = Tac2ffi.repr_ext Tac2ffi.val_ltac1 -let of_ltac1 v = Tac2ffi.of_ext Tac2ffi.val_ltac1 v - -let () = - define "ltac1_ref" (list ident @-> ret ltac1) @@ fun ids -> - let open Ltac_plugin in - let r = - match ids with - | [] -> raise Not_found - | _ :: _ as ids -> - let (id, path) = List.sep_last ids in - let path = DirPath.make (List.rev path) in - let fp = Libnames.make_path path id in - if Tacenv.exists_tactic fp then - List.hd (Tacenv.locate_extended_all_tactic (Libnames.qualid_of_path fp)) - else raise Not_found - in - Tacinterp.Value.of_closure (Tacinterp.default_ist ()) (Tacenv.interp_ltac r) - -let () = - define "ltac1_run" (ltac1 @-> tac unit) @@ fun v -> - let open Ltac_plugin in - Tacinterp.tactic_of_value (Tacinterp.default_ist ()) v - -let () = - define "ltac1_apply" (ltac1 @-> list ltac1 @-> closure @-> tac unit) @@ fun f args k -> - let open Ltac_plugin in - let open Tacexpr in - let open Locus in - let k ret = - Proofview.tclIGNORE (Tac2ffi.apply k [Tac2ffi.of_ext val_ltac1 ret]) - in - let fold arg (i, vars, lfun) = - let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar CAst.(make id)) in - (succ i, x :: vars, Id.Map.add id arg lfun) - in - let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in - let lfun = Id.Map.add (Id.of_string "F") f lfun in - let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in - let tac = CAst.make @@ TacArg (TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in - Tacinterp.val_interp ist tac k - -let () = - define "ltac1_of_constr" (constr @-> ret ltac1) - Ltac_plugin.Tacinterp.Value.of_constr - -let () = - define "ltac1_to_constr" (ltac1 @-> ret (option constr)) - Ltac_plugin.Tacinterp.Value.to_constr - -let () = - define "ltac1_of_ident" (ident @-> ret ltac1) - Ltac_plugin.Taccoerce.Value.of_ident - -let () = - define "ltac1_to_ident" (ltac1 @-> ret (option ident)) - Ltac_plugin.Taccoerce.Value.to_ident - -let () = - define "ltac1_of_list" (list ltac1 @-> ret ltac1) @@ fun l -> - Geninterp.Val.(inject (Base typ_list) l) - -let () = - define "ltac1_to_list" (ltac1 @-> ret (option (list ltac1))) - Ltac_plugin.Tacinterp.Value.to_list - module MapTagDyn = Dyn.Make() type ('a,'set,'map) map_tag = ('a * 'set * 'map) MapTagDyn.tag @@ -1770,121 +1700,6 @@ let () = } in define_ml_object Tac2quote.wit_reference obj -let () = - let intern self ist (ids, tac) = - let map { CAst.v = id } = id in - let ids = List.map map ids in - (* Prevent inner calls to Ltac2 values *) - let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in - let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in - let ist = { ist with Genintern.extra; ltacvars } in - let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in - let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in - let ty = List.fold_left fold (gtypref t_unit) ids in - GlbVal (ids, tac), ty - in - let interp _ (ids, tac) = - let clos args = - let add lfun id v = - let v = Tac2ffi.to_ext val_ltac1 v in - Id.Map.add id v lfun - in - let lfun = List.fold_left2 add Id.Map.empty ids args in - let ist = { env_ist = Id.Map.empty } in - let lfun = Tac2interp.set_env ist lfun in - let ist = Ltac_plugin.Tacinterp.default_ist () in - let ist = { ist with Geninterp.lfun = lfun } in - let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in - tac >>= fun () -> - return v_unit - in - let len = List.length ids in - if Int.equal len 0 then - clos [] - else - return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) - in - let subst s (ids, tac) = (ids, Gensubst.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in - let print env sigma (ids, tac) = - let ids = - if List.is_empty ids then mt () - else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc () - in - str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" - in - let raw_print env sigma (ids, tac) = - let ids = - if List.is_empty ids then mt () - else pr_sequence (fun id -> Id.print id.CAst.v) ids ++ spc () ++ str "|-" ++ spc () - in - str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_raw_tactic env sigma tac ++ str ")" - in - let obj = { - ml_intern = intern; - ml_subst = subst; - ml_interp = interp; - ml_print = print; - ml_raw_print = raw_print; - } in - define_ml_object Tac2quote.wit_ltac1 obj - -let () = - let open Ltac_plugin in - let intern self ist (ids, tac) = - let map { CAst.v = id } = id in - let ids = List.map map ids in - (* Prevent inner calls to Ltac2 values *) - let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in - let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in - let ist = { ist with Genintern.extra; ltacvars } in - let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in - let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in - let ty = List.fold_left fold (gtypref t_ltac1) ids in - GlbVal (ids, tac), ty - in - let interp _ (ids, tac) = - let clos args = - let add lfun id v = - let v = Tac2ffi.to_ext val_ltac1 v in - Id.Map.add id v lfun - in - let lfun = List.fold_left2 add Id.Map.empty ids args in - let ist = { env_ist = Id.Map.empty } in - let lfun = Tac2interp.set_env ist lfun in - let ist = Ltac_plugin.Tacinterp.default_ist () in - let ist = { ist with Geninterp.lfun = lfun } in - return (Tac2ffi.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac)) - in - let len = List.length ids in - if Int.equal len 0 then - clos [] - else - return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) - in - let subst s (ids, tac) = (ids, Gensubst.substitute Tacarg.wit_tactic s tac) in - let print env sigma (ids, tac) = - let ids = - if List.is_empty ids then mt () - else pr_sequence Id.print ids ++ str " |- " - in - str "ltac1val:(" ++ ids++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" - in - let raw_print env sigma (ids, tac) = - let ids = - if List.is_empty ids then mt () - else pr_sequence (fun id -> Id.print id.CAst.v) ids ++ spc () ++ str "|-" ++ spc () - in - str "ltac1val:(" ++ ids ++ Ltac_plugin.Pptactic.pr_raw_tactic env sigma tac ++ str ")" - in - let obj = { - ml_intern = intern; - ml_subst = subst; - ml_interp = interp; - ml_print = print; - ml_raw_print = raw_print; - } in - define_ml_object Tac2quote.wit_ltac1val obj - (** Ltac2 in terms *) let () = @@ -2023,115 +1838,6 @@ let () = in Genintern.register_ntn_subst0 wit_ltac2_constr subs -(** Ltac2 in Ltac1 *) - -let () = - let create name wit = - let e = Tac2entries.Pltac.tac2expr_in_env in - let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some name, in_gen (rawwit wit) v) in - Ltac_plugin.Tacentries.create_ltac_quotation ~plugin:ltac2_plugin name inject (e, None) - in - let () = create "ltac2" wit_ltac2in1 in - let () = create "ltac2val" wit_ltac2in1_val in - () - -(* Ltac1 runtime representation of Ltac2 closures. *) -let typ_ltac2 : valexpr Geninterp.Val.typ = - Geninterp.Val.create "ltac2:ltac2_eval" - -let () = Genprint.register_val_print0 typ_ltac2 (fun v -> - TopPrinterBasic (fun () -> Pp.str "")) - -let cast_typ (type a) (tag : a Geninterp.Val.typ) (v : Geninterp.Val.t) : a = - let Geninterp.Val.Dyn (tag', v) = v in - match Geninterp.Val.eq tag tag' with - | None -> assert false - | Some Refl -> v - -let () = - let open Ltac_plugin in - (* This is a hack similar to Tacentries.ml_val_tactic_extend *) - let intern_fun _ e = Empty.abort e in - let subst_fun s v = v in - let () = Genintern.register_intern0 wit_ltac2_val intern_fun in - let () = Gensubst.register_subst0 wit_ltac2_val subst_fun in - (* These are bound names and not relevant *) - let tac_id = Id.of_string "F" in - let arg_id = Id.of_string "X" in - let interp_fun ist () = - let tac = cast_typ typ_ltac2 @@ Id.Map.get tac_id ist.Tacinterp.lfun in - let arg = Id.Map.get arg_id ist.Tacinterp.lfun in - let tac = Tac2ffi.to_closure tac in - Tac2ffi.apply tac [of_ltac1 arg] >>= fun ans -> - let ans = Tac2ffi.to_ext val_ltac1 ans in - Ftactic.return ans - in - let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in - define "ltac1_lambda" (valexpr @-> ret ltac1) @@ fun f -> - let body = Tacexpr.TacGeneric (Some ltac2_plugin, in_gen (glbwit wit_ltac2_val) ()) in - let clos = CAst.make (Tacexpr.TacFun ([Name arg_id], CAst.make (Tacexpr.TacArg body))) in - let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in - let lfun = Id.Map.singleton tac_id f in - let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in - Tacinterp.Value.of_closure ist clos - -let ltac2_eval = - let open Ltac_plugin in - let ml_name = { - Tacexpr.mltac_plugin = ltac2_plugin; - mltac_tactic = "ltac2_eval"; - } in - let eval_fun args ist = match args with - | [] -> assert false - | tac :: args -> - (* By convention the first argument is the tactic being applied, the rest - being the arguments it should be fed with *) - let tac = cast_typ typ_ltac2 tac in - let tac = Tac2ffi.to_closure tac in - let args = List.map (fun arg -> Tac2ffi.of_ext val_ltac1 arg) args in - Proofview.tclIGNORE (Tac2ffi.apply tac args) - in - let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in - { Tacexpr.mltac_name = ml_name; mltac_index = 0 } - -let () = - let open Ltac_plugin in - let open Tacinterp in - let interp ist (ids, tac) = match ids with - | [] -> - (* Evaluate the Ltac2 quotation eagerly *) - let idtac = Value.of_closure { ist with lfun = Id.Map.empty } - (CAst.make (Tacexpr.TacId [])) in - let ist = { env_ist = Id.Map.empty } in - Tac2interp.interp ist tac >>= fun v -> - let v = idtac in - Ftactic.return v - | _ :: _ -> - (* Return a closure [@f := {blob} |- fun ids => ltac2_eval(f, ids) ] *) - (* This name cannot clash with Ltac2 variables which are all lowercase *) - let self_id = Id.of_string "F" in - let nas = List.map (fun id -> Name id) ids in - let mk_arg id = Tacexpr.Reference (Locus.ArgVar (CAst.make id)) in - let args = List.map mk_arg ids in - let clos = CAst.make (Tacexpr.TacFun - (nas, CAst.make (Tacexpr.TacML (ltac2_eval, mk_arg self_id :: args)))) in - let self = GTacFun (List.map (fun id -> Name id) ids, tac) in - let self = Tac2interp.interp_value { env_ist = Id.Map.empty } self in - let self = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) self in - let ist = { ist with lfun = Id.Map.singleton self_id self } in - Ftactic.return (Value.of_closure ist clos) - in - Geninterp.register_interp0 wit_ltac2in1 interp - -let () = - let interp ist tac = - let ist = { env_ist = Id.Map.empty } in - Tac2interp.interp ist tac >>= fun v -> - let v = repr_to ltac1 v in - Ftactic.return v - in - Geninterp.register_interp0 wit_ltac2in1_val interp - let () = let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> assert false) in let pr_glb (ids, e) = diff --git a/plugins/ltac2/tac2core.mli b/plugins/ltac2/tac2core.mli index 3f4dede6dc5cf..797946cb54960 100644 --- a/plugins/ltac2/tac2core.mli +++ b/plugins/ltac2/tac2core.mli @@ -16,6 +16,9 @@ open Tac2expr module Core : sig +val t_unit : type_constant +val v_unit : Tac2ffi.valexpr + val t_list : type_constant val c_nil : ltac_constructor val c_cons : ltac_constructor diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml index cd6e6e4925252..c8c8b07deee23 100644 --- a/plugins/ltac2/tac2quote.ml +++ b/plugins/ltac2/tac2quote.ml @@ -24,8 +24,6 @@ let wit_ident = Arg.create "ident" let wit_constr = Arg.create "constr" let wit_open_constr = Arg.create "open_constr" let wit_preterm = Arg.create "preterm" -let wit_ltac1 = Arg.create "ltac1" -let wit_ltac1val = Arg.create "ltac1val" (** Syntactic quoting of expressions. *) diff --git a/plugins/ltac2/tac2quote.mli b/plugins/ltac2/tac2quote.mli index a24bcb7eecf08..b928170f13674 100644 --- a/plugins/ltac2/tac2quote.mli +++ b/plugins/ltac2/tac2quote.mli @@ -106,9 +106,3 @@ val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag val wit_preterm : (Constrexpr.constr_expr, Id.Set.t * Glob_term.glob_constr) Arg.tag - -val wit_ltac1 : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag -(** Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2. *) - -val wit_ltac1val : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag -(** Ltac1 AST quotation, seen as a value-returning expression, with type Ltac1.t. *) diff --git a/plugins/ltac2_ltac1/dune b/plugins/ltac2_ltac1/dune new file mode 100644 index 0000000000000..abd2ddf0748b1 --- /dev/null +++ b/plugins/ltac2_ltac1/dune @@ -0,0 +1,7 @@ +(library + (name ltac2_ltac1_plugin) + (public_name coq-core.plugins.ltac2_ltac1) + (synopsis "Ltac2 and Ltac1 interoperability plugin") + (libraries ltac_plugin ltac2_plugin)) + +(coq.pp (modules g_ltac2_ltac1)) diff --git a/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg b/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg new file mode 100644 index 0000000000000..0e08dcaaada57 --- /dev/null +++ b/plugins/ltac2_ltac1/g_ltac2_ltac1.mlg @@ -0,0 +1,41 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* { inj_ltac1 loc qid } + | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid } ] ] + ; + ltac1_expr_in_env: + [ [ test_ltac1_env; ids = LIST0 identref; "|-"; e = ltac_expr -> { ids, e } + | e = ltac_expr -> { [], e } + ] ] + ; +END diff --git a/plugins/ltac2_ltac1/g_ltac2_ltac1.mli b/plugins/ltac2_ltac1/g_ltac2_ltac1.mli new file mode 100644 index 0000000000000..b72d544151179 --- /dev/null +++ b/plugins/ltac2_ltac1/g_ltac2_ltac1.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* ret ltac1) @@ fun ids -> + let open Ltac_plugin in + let r = + match ids with + | [] -> raise Not_found + | _ :: _ as ids -> + let (id, path) = List.sep_last ids in + let path = DirPath.make (List.rev path) in + let fp = Libnames.make_path path id in + if Tacenv.exists_tactic fp then + List.hd (Tacenv.locate_extended_all_tactic (Libnames.qualid_of_path fp)) + else raise Not_found + in + Tacinterp.Value.of_closure (Tacinterp.default_ist ()) (Tacenv.interp_ltac r) + +let () = + define "ltac1_run" (ltac1 @-> tac unit) @@ fun v -> + let open Ltac_plugin in + Tacinterp.tactic_of_value (Tacinterp.default_ist ()) v + +let () = + define "ltac1_apply" (ltac1 @-> list ltac1 @-> closure @-> tac unit) @@ fun f args k -> + let open Ltac_plugin in + let open Tacexpr in + let open Locus in + let k ret = + Proofview.tclIGNORE (Tac2ffi.apply k [Tac2ffi.of_ext val_ltac1 ret]) + in + let fold arg (i, vars, lfun) = + let id = Id.of_string ("x" ^ string_of_int i) in + let x = Reference (ArgVar CAst.(make id)) in + (succ i, x :: vars, Id.Map.add id arg lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let lfun = Id.Map.add (Id.of_string "F") f lfun in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + let tac = CAst.make @@ TacArg (TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + Tacinterp.val_interp ist tac k + +let () = + define "ltac1_of_constr" (constr @-> ret ltac1) + Ltac_plugin.Tacinterp.Value.of_constr + +let () = + define "ltac1_to_constr" (ltac1 @-> ret (option constr)) + Ltac_plugin.Tacinterp.Value.to_constr + +let () = + define "ltac1_of_ident" (ident @-> ret ltac1) + Ltac_plugin.Taccoerce.Value.of_ident + +let () = + define "ltac1_to_ident" (ltac1 @-> ret (option ident)) + Ltac_plugin.Taccoerce.Value.to_ident + +let () = + define "ltac1_of_list" (list ltac1 @-> ret ltac1) @@ fun l -> + Geninterp.Val.(inject (Base typ_list) l) + +let () = + define "ltac1_to_list" (ltac1 @-> ret (option (list ltac1))) + Ltac_plugin.Tacinterp.Value.to_list + +let gtypref kn = GTypRef (Other kn, []) + +open Tac2core.Core + +let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n)) +let ltac1_core n = core_prefix Tac2env.ltac1_prefix n +let t_ltac1 = ltac1_core "t" + +let () = + let intern self ist (ids, tac) = + let map { CAst.v = id } = id in + let ids = List.map map ids in + (* Prevent inner calls to Ltac2 values *) + let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in + let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in + let ist = { ist with Genintern.extra; ltacvars } in + let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in + let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in + let ty = List.fold_left fold (gtypref t_unit) ids in + GlbVal (ids, tac), ty + in + let interp _ (ids, tac) = + let clos args = + let add lfun id v = + let v = Tac2ffi.to_ext val_ltac1 v in + Id.Map.add id v lfun + in + let lfun = List.fold_left2 add Id.Map.empty ids args in + let ist = { env_ist = Id.Map.empty } in + let lfun = Tac2interp.set_env ist lfun in + let ist = Ltac_plugin.Tacinterp.default_ist () in + let ist = { ist with Geninterp.lfun = lfun } in + let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in + tac >>= fun () -> + return v_unit + in + let len = List.length ids in + if Int.equal len 0 then + clos [] + else + return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) + in + let subst s (ids, tac) = (ids, Gensubst.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in + let print env sigma (ids, tac) = + let ids = + if List.is_empty ids then mt () + else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc () + in + str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" + in + let raw_print env sigma (ids, tac) = + let ids = + if List.is_empty ids then mt () + else pr_sequence (fun id -> Id.print id.CAst.v) ids ++ spc () ++ str "|-" ++ spc () + in + str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_raw_tactic env sigma tac ++ str ")" + in + let obj = { + ml_intern = intern; + ml_subst = subst; + ml_interp = interp; + ml_print = print; + ml_raw_print = raw_print; + } in + define_ml_object Tac2quote_ltac1.wit_ltac1 obj + +let () = + let open Ltac_plugin in + let intern self ist (ids, tac) = + let map { CAst.v = id } = id in + let ids = List.map map ids in + (* Prevent inner calls to Ltac2 values *) + let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in + let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in + let ist = { ist with Genintern.extra; ltacvars } in + let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in + let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in + let ty = List.fold_left fold (gtypref t_ltac1) ids in + GlbVal (ids, tac), ty + in + let interp _ (ids, tac) = + let clos args = + let add lfun id v = + let v = Tac2ffi.to_ext val_ltac1 v in + Id.Map.add id v lfun + in + let lfun = List.fold_left2 add Id.Map.empty ids args in + let ist = { env_ist = Id.Map.empty } in + let lfun = Tac2interp.set_env ist lfun in + let ist = Ltac_plugin.Tacinterp.default_ist () in + let ist = { ist with Geninterp.lfun = lfun } in + return (Tac2ffi.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac)) + in + let len = List.length ids in + if Int.equal len 0 then + clos [] + else + return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) + in + let subst s (ids, tac) = (ids, Gensubst.substitute Tacarg.wit_tactic s tac) in + let print env sigma (ids, tac) = + let ids = + if List.is_empty ids then mt () + else pr_sequence Id.print ids ++ str " |- " + in + str "ltac1val:(" ++ ids++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" + in + let raw_print env sigma (ids, tac) = + let ids = + if List.is_empty ids then mt () + else pr_sequence (fun id -> Id.print id.CAst.v) ids ++ spc () ++ str "|-" ++ spc () + in + str "ltac1val:(" ++ ids ++ Ltac_plugin.Pptactic.pr_raw_tactic env sigma tac ++ str ")" + in + let obj = { + ml_intern = intern; + ml_subst = subst; + ml_interp = interp; + ml_print = print; + ml_raw_print = raw_print; + } in + define_ml_object Tac2quote_ltac1.wit_ltac1val obj + +(** Ltac2 in Ltac1 *) + +let () = + let create name wit = + let e = Tac2entries.Pltac.tac2expr_in_env in + let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some name, in_gen (rawwit wit) v) in + Ltac_plugin.Tacentries.create_ltac_quotation ~plugin:ltac2_ltac1_plugin name inject (e, None) + in + let () = create "ltac2" wit_ltac2in1 in + let () = create "ltac2val" wit_ltac2in1_val in + () + +(* Ltac1 runtime representation of Ltac2 closures. *) +let typ_ltac2 : valexpr Geninterp.Val.typ = + Geninterp.Val.create "ltac2:ltac2_eval" + +let () = Genprint.register_val_print0 typ_ltac2 (fun v -> + TopPrinterBasic (fun () -> Pp.str "")) + +let cast_typ (type a) (tag : a Geninterp.Val.typ) (v : Geninterp.Val.t) : a = + let Geninterp.Val.Dyn (tag', v) = v in + match Geninterp.Val.eq tag tag' with + | None -> assert false + | Some Refl -> v + +let () = + let open Ltac_plugin in + (* This is a hack similar to Tacentries.ml_val_tactic_extend *) + let intern_fun _ e = Empty.abort e in + let subst_fun s v = v in + let () = Genintern.register_intern0 wit_ltac2_val intern_fun in + let () = Gensubst.register_subst0 wit_ltac2_val subst_fun in + (* These are bound names and not relevant *) + let tac_id = Id.of_string "F" in + let arg_id = Id.of_string "X" in + let interp_fun ist () = + let tac = cast_typ typ_ltac2 @@ Id.Map.get tac_id ist.Tacinterp.lfun in + let arg = Id.Map.get arg_id ist.Tacinterp.lfun in + let tac = Tac2ffi.to_closure tac in + Tac2ffi.apply tac [of_ltac1 arg] >>= fun ans -> + let ans = Tac2ffi.to_ext val_ltac1 ans in + Ftactic.return ans + in + let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in + define "ltac1_lambda" (valexpr @-> ret ltac1) @@ fun f -> + let body = Tacexpr.TacGeneric (Some ltac2_ltac1_plugin, in_gen (glbwit wit_ltac2_val) ()) in + let clos = CAst.make (Tacexpr.TacFun ([Name arg_id], CAst.make (Tacexpr.TacArg body))) in + let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in + let lfun = Id.Map.singleton tac_id f in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in + Tacinterp.Value.of_closure ist clos + +let ltac2_eval = + let open Ltac_plugin in + let ml_name = { + Tacexpr.mltac_plugin = ltac2_ltac1_plugin; + mltac_tactic = "ltac2_eval"; + } in + let eval_fun args ist = match args with + | [] -> assert false + | tac :: args -> + (* By convention the first argument is the tactic being applied, the rest + being the arguments it should be fed with *) + let tac = cast_typ typ_ltac2 tac in + let tac = Tac2ffi.to_closure tac in + let args = List.map (fun arg -> Tac2ffi.of_ext val_ltac1 arg) args in + Proofview.tclIGNORE (Tac2ffi.apply tac args) + in + let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in + { Tacexpr.mltac_name = ml_name; mltac_index = 0 } + +let () = + let open Ltac_plugin in + let open Tacinterp in + let interp ist (ids, tac) = match ids with + | [] -> + (* Evaluate the Ltac2 quotation eagerly *) + let idtac = Value.of_closure { ist with lfun = Id.Map.empty } + (CAst.make (Tacexpr.TacId [])) in + let ist = { env_ist = Id.Map.empty } in + Tac2interp.interp ist tac >>= fun v -> + let v = idtac in + Ftactic.return v + | _ :: _ -> + (* Return a closure [@f := {blob} |- fun ids => ltac2_eval(f, ids) ] *) + (* This name cannot clash with Ltac2 variables which are all lowercase *) + let self_id = Id.of_string "F" in + let nas = List.map (fun id -> Name id) ids in + let mk_arg id = Tacexpr.Reference (Locus.ArgVar (CAst.make id)) in + let args = List.map mk_arg ids in + let clos = CAst.make (Tacexpr.TacFun + (nas, CAst.make (Tacexpr.TacML (ltac2_eval, mk_arg self_id :: args)))) in + let self = GTacFun (List.map (fun id -> Name id) ids, tac) in + let self = Tac2interp.interp_value { env_ist = Id.Map.empty } self in + let self = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) self in + let ist = { ist with lfun = Id.Map.singleton self_id self } in + Ftactic.return (Value.of_closure ist clos) + in + Geninterp.register_interp0 wit_ltac2in1 interp + +let () = + let interp ist tac = + let ist = { env_ist = Id.Map.empty } in + Tac2interp.interp ist tac >>= fun v -> + let v = repr_to ltac1 v in + Ftactic.return v + in + Geninterp.register_interp0 wit_ltac2in1_val interp diff --git a/plugins/ltac2_ltac1/tac2core_ltac1.mli b/plugins/ltac2_ltac1/tac2core_ltac1.mli new file mode 100644 index 0000000000000..b72d544151179 --- /dev/null +++ b/plugins/ltac2_ltac1/tac2core_ltac1.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* > lk_ident + end + +let pr_ltac_use_default b = + let open Pp in + if b then (* Bug: a space is inserted before "..." *) str ".." else mt () + +} + +GRAMMAR EXTEND Gram + GLOBAL: toplevel_selector goal_selector; + range_selector: + [ [ 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) } + | 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 } ] ] + ; + goal_selector: + [ [ l = range_selector_or_nth -> { l } + | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] + ; + toplevel_selector: + [ [ sel = goal_selector; ":" -> { sel } + | "!"; ":" -> { Goal_select.SelectAlreadyFocused } + | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] + ; +END + +VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector } +| [ toplevel_selector(s) ] -> { s } +END + +VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default } +| [ "." ] -> { false } +| [ "..." ] -> { true } +END diff --git a/plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mli b/plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mli new file mode 100644 index 0000000000000..c59363da9228a --- /dev/null +++ b/plugins/ltac2_ltac1_common/g_ltac2_ltac1_common.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Pptactic.pr_alias_key s - | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - (* todo: don't want the KerName instead? *) - | Tacexpr.LtacVarCall (_, id, t) -> Names.Id.print id - | Tacexpr.LtacAtomCall te -> - Pptactic.pr_glob_tactic (Global.env ()) - (CAst.make (Tacexpr.TacAtom te)) - | Tacexpr.LtacConstrInterp (env, sigma, c, _) -> - pr_glob_constr_env env sigma c - | Tacexpr.LtacMLCall te -> - (Pptactic.pr_glob_tactic (Global.env ()) - te) - let string_of_call ck = let s = string_of_ppcmds ck in let s = String.map (fun c -> if c = '\n' then ' ' else c) s in @@ -370,12 +355,6 @@ let do_profile_gen pp_call call_trace ?(count_call=true) tac = exit_tactic ~count_call start_time name))) | None -> Proofview.tclUNIT ()) -let do_profile trace ?count_call tac = - do_profile_gen (function - | (_, c) :: _ -> Some (pp_ltac_call_kind c) - | [] -> None) - trace ?count_call tac - (* ************** Accumulation of data from workers ************************* *) let get_local_profiling_results () = List.hd !stack diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac2_ltac1_common/profile_ltac.mli similarity index 97% rename from plugins/ltac/profile_ltac.mli rename to plugins/ltac2_ltac1_common/profile_ltac.mli index 1f4339f7620b2..60e462783331f 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac2_ltac1_common/profile_ltac.mli @@ -41,11 +41,6 @@ count and tactic running time goes in the second tree. Alas, I suspect that fixing this requires a redesign of how the profiler hooks into the tactic engine. *) -val do_profile : - ('a * Tacexpr.ltac_call_kind) list -> - ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic - - val do_profile_gen : ('a -> Pp.t option) -> 'a -> ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic diff --git a/test-suite/bugs/bug_3612.v b/test-suite/bugs/bug_3612.v index 3c852aa090409..ca3d844ff1683 100644 --- a/test-suite/bugs/bug_3612.v +++ b/test-suite/bugs/bug_3612.v @@ -38,6 +38,7 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. +Declare ML Module "coq-core.plugins.ltac2_ltac1_common". Declare ML Module "coq-core.plugins.ltac". Set Default Proof Mode "Classic". diff --git a/test-suite/bugs/bug_3649.v b/test-suite/bugs/bug_3649.v index f219ea5244245..a0f84e9a3343d 100644 --- a/test-suite/bugs/bug_3649.v +++ b/test-suite/bugs/bug_3649.v @@ -2,6 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) +Declare ML Module "coq-core.plugins.ltac2_ltac1_common". Declare ML Module "coq-core.plugins.ltac". Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). diff --git a/test-suite/stm/classify_set_proof_mode_9093.v b/test-suite/stm/classify_set_proof_mode_9093.v index bd051ffc0afbe..cb0633ee72717 100644 --- a/test-suite/stm/classify_set_proof_mode_9093.v +++ b/test-suite/stm/classify_set_proof_mode_9093.v @@ -1,5 +1,6 @@ (* -*- coq-prog-args: ("-async-proofs" "on" "-noinit"); -*- *) +Declare ML Module "coq-core.plugins.ltac2_ltac1_common". Declare ML Module "coq-core.plugins.ltac". Set Default Proof Mode "Classic". diff --git a/test-suite/success/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v index 0feba189cc31b..4c442c42e3421 100644 --- a/test-suite/success/Discriminate_HoTT.v +++ b/test-suite/success/Discriminate_HoTT.v @@ -9,6 +9,7 @@ Unset Elimination Schemes. Set Universe Polymorphism. +Declare ML Module "coq-core.plugins.ltac2_ltac1_common". Declare ML Module "coq-core.plugins.ltac". Global Set Default Proof Mode "Classic". diff --git a/theories/Init/Ltac.v b/theories/Init/Ltac.v index 319776da5fe72..8c88e5dccd87d 100644 --- a/theories/Init/Ltac.v +++ b/theories/Init/Ltac.v @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Declare ML Module "ltac2_ltac1_common_plugin:coq-core.plugins.ltac2_ltac1_common". Declare ML Module "ltac_plugin:coq-core.plugins.ltac". #[export] Set Default Proof Mode "Classic". diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 55b4cf65212d7..9b891333bbda2 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -9,6 +9,7 @@ (************************************************************************) Declare ML Module "ltac2_plugin:coq-core.plugins.ltac2". +Declare ML Module "ltac2_ltac1_plugin:coq-core.plugins.ltac2_ltac1". #[export] Set Default Proof Mode "Ltac2". diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index 88bfbbbc79d20..cf550b84b299f 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/user-contrib/Ltac2/Ltac1.v @@ -18,30 +18,30 @@ Require Import Ltac2.Init. Ltac2 Type t. (** Dynamically-typed Ltac1 values. *) -Ltac2 @ external ref : ident list -> t := "coq-core.plugins.ltac2" "ltac1_ref". +Ltac2 @ external ref : ident list -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_ref". (** Returns the Ltac1 definition with the given absolute name. *) -Ltac2 @ external run : t -> unit := "coq-core.plugins.ltac2" "ltac1_run". +Ltac2 @ external run : t -> unit := "coq-core.plugins.ltac2_ltac1" "ltac1_run". (** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning anything. *) -Ltac2 @ external lambda : (t -> t) -> t := "coq-core.plugins.ltac2" "ltac1_lambda". +Ltac2 @ external lambda : (t -> t) -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_lambda". (** Embed an Ltac2 function into Ltac1 values. Contrarily to the ltac1:(...) quotation, this function allows both to capture an Ltac2 context inside the closure and to return an Ltac1 value. Returning values in Ltac1 is a intrepid endeavour prone to weird runtime semantics. *) -Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "coq-core.plugins.ltac2" "ltac1_apply". +Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "coq-core.plugins.ltac2_ltac1" "ltac1_apply". (** Applies an Ltac1 value to a list of arguments, and provides the result in CPS style. It does **not** run the returned value. *) (** Conversion functions *) -Ltac2 @ external of_constr : constr -> t := "coq-core.plugins.ltac2" "ltac1_of_constr". -Ltac2 @ external to_constr : t -> constr option := "coq-core.plugins.ltac2" "ltac1_to_constr". +Ltac2 @ external of_constr : constr -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_constr". +Ltac2 @ external to_constr : t -> constr option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_constr". -Ltac2 @ external of_ident : ident -> t := "coq-core.plugins.ltac2" "ltac1_of_ident". -Ltac2 @ external to_ident : t -> ident option := "coq-core.plugins.ltac2" "ltac1_to_ident". +Ltac2 @ external of_ident : ident -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_ident". +Ltac2 @ external to_ident : t -> ident option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_ident". -Ltac2 @ external of_list : t list -> t := "coq-core.plugins.ltac2" "ltac1_of_list". -Ltac2 @ external to_list : t -> t list option := "coq-core.plugins.ltac2" "ltac1_to_list". +Ltac2 @ external of_list : t list -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_list". +Ltac2 @ external to_list : t -> t list option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_list".