From f77d6a239ff70a8aaa10d256f545fc21b2c7ecc0 Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Tue, 30 Mar 2021 22:21:26 +0200 Subject: Fix printing of ssr do intros and seq tactics --- plugins/ssr/ssrparser.mlg | 126 ++++++++++++++++++++++++++-------------- test-suite/output/bug_13240.out | 3 + test-suite/output/bug_13240.v | 10 ++++ 3 files changed, 95 insertions(+), 44 deletions(-) create mode 100644 test-suite/output/bug_13240.out create mode 100644 test-suite/output/bug_13240.v diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 935cef58b9..ad85f68b03 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -46,6 +46,7 @@ open Ssrtacticals open Ssrbwd open Ssrequality open Ssripats +open Libobject (** Ssreflect load check. *) @@ -79,8 +80,39 @@ let ssrtac_entry name = { mltac_index = 0; } -let register_ssrtac name f = - Tacenv.register_ml_tactic (ssrtac_name name) [|f|] +let cache_tactic_notation (_, (key, body, parule)) = + Tacenv.register_alias key body; + Pptactic.declare_notation_tactic_pprule key parule + +type tactic_grammar_obj = KerName.t * Tacenv.alias_tactic * Pptactic.pp_tactic + +let inSsrGrammar : tactic_grammar_obj -> obj = + declare_object {(default_object "SsrGrammar") with + load_function = (fun _ -> cache_tactic_notation); + cache_function = cache_tactic_notation; + classify_function = (fun x -> Keep x)} + +let path = MPfile (DirPath.make @@ List.map Id.of_string ["ssreflect"; "ssr"; "Coq"]) + +let register_ssrtac name f prods = + let open Pptactic in + Tacenv.register_ml_tactic (ssrtac_name name) [|f|]; + let map id = Reference (Locus.ArgVar (CAst.make id)) in + let get_id = function + | TacTerm s -> None + | TacNonTerm (_, (_, ido)) -> ido in + let ids = List.map_filter get_id prods in + let tac = TacML (CAst.make (ssrtac_entry name, List.map map ids)) in + let key = KerName.make path (Label.make ("ssrparser_" ^ name)) in + let body = Tacenv.{ alias_args = ids; alias_body = tac; alias_deprecation = None } in + let parule = { + pptac_level = 0; + pptac_prods = prods + } in + let obj () = + Lib.add_anonymous_leaf (inSsrGrammar (key, body, parule)) in + Mltop.declare_cache_obj obj __coq_plugin_name; + key let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v @@ -933,7 +965,7 @@ END { let pr_intros sep intrs = - if intrs = [] then mt() else sep () ++ str "=>" ++ pr_ipats intrs + if intrs = [] then mt() else sep () ++ str "=>" ++ sep () ++ pr_ipats intrs let pr_ssrintros _ _ _ = pr_intros mt } @@ -963,15 +995,6 @@ END { -let () = register_ssrtac "tclintros" begin fun args ist -> match args with -| [arg] -> - let arg = cast_arg wit_ssrintrosarg arg in - let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros -| _ -> assert false -end - - (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id @@ -1672,20 +1695,28 @@ let _ = add_internal_name (is_tagged perm_tag) { -type ssrargfmt = ArgSsr of string | ArgSep of string + let ssrtac_expr ?loc key args = + TacAlias (CAst.make ?loc (key, (List.map (fun x -> Tacexpr.TacGeneric (None, x)) args))) -let set_pr_ssrtac name prec afmt = (* FIXME *) () (* - let fmt = List.map (function - | ArgSep s -> Egramml.GramTerminal s - | ArgSsr s -> Egramml.GramTerminal s - | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in - let tacname = ssrtac_name name in () *) +let mk_non_term wit id = + let open Pptactic in + TacNonTerm (None, (Extend.Uentry (Genarg.ArgT.Any (Genarg.get_arg_tag wit)), Some id)) -let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) +let tclintroskey = + let prods = + [ mk_non_term wit_ssrintrosarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [arg] -> + let arg = cast_arg wit_ssrintrosarg arg in + let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros + | _ -> assert false + end in + register_ssrtac "tclintros" tac prods let tclintros_expr ?loc tac ipats = - let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in - ssrtac_expr ?loc "tclintros" args + let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in + ssrtac_expr ?loc tclintroskey args } @@ -1768,18 +1799,20 @@ END { -let () = register_ssrtac "tcldo" begin fun args ist -> match args with -| [arg] -> - let arg = cast_arg wit_ssrdoarg arg in - ssrdotac ist arg -| _ -> assert false -end - -let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] +let tcldokey = + let open Pptactic in + let prods = [ TacTerm "do"; mk_non_term wit_ssrdoarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [arg] -> + let arg = cast_arg wit_ssrdoarg arg in + ssrdotac ist arg + | _ -> assert false + end in + register_ssrtac "tcldo" tac prods let ssrdotac_expr ?loc n m tac clauses = let arg = ((n, m), tac), clauses in - ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)] + ssrtac_expr ?loc tcldokey [in_gen (rawwit wit_ssrdoarg) arg] } @@ -1815,22 +1848,26 @@ END { -let () = register_ssrtac "tclseq" begin fun args ist -> match args with -| [tac; dir; arg] -> - let tac = cast_arg wit_ssrtclarg tac in - let dir = cast_arg wit_ssrseqdir dir in - let arg = cast_arg wit_ssrseqarg arg in - tclSEQAT ist tac dir arg -| _ -> assert false -end - -let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] +let tclseqkey = + let prods = + [ mk_non_term wit_ssrtclarg (Names.Id.of_string "tac") + ; mk_non_term wit_ssrseqdir (Names.Id.of_string "dir") + ; mk_non_term wit_ssrseqarg (Names.Id.of_string "arg") ] in + let tac = begin fun args ist -> match args with + | [tac; dir; arg] -> + let tac = cast_arg wit_ssrtclarg tac in + let dir = cast_arg wit_ssrseqdir dir in + let arg = cast_arg wit_ssrseqarg arg in + tclSEQAT ist tac dir arg + | _ -> assert false + end in + register_ssrtac "tclseq" tac prods let tclseq_expr ?loc tac dir arg = let arg1 = in_gen (rawwit wit_ssrtclarg) tac in let arg2 = in_gen (rawwit wit_ssrseqdir) dir in let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in - ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3]) + ssrtac_expr ?loc tclseqkey [arg1; arg2; arg3] } @@ -2453,8 +2490,9 @@ GRAMMAR EXTEND Gram GLOBAL: ltac_expr; ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> - { ssrtac_expr ~loc "abstract" - [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; + { TacML (CAst.make ~loc ( + ssrtac_entry "abstract", [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)])) + } ]]; END TACTIC EXTEND ssrabstract | [ "abstract" ssrdgens(gens) ] -> { diff --git a/test-suite/output/bug_13240.out b/test-suite/output/bug_13240.out new file mode 100644 index 0000000000..5fccef5cfe --- /dev/null +++ b/test-suite/output/bug_13240.out @@ -0,0 +1,3 @@ +Ltac t1 a b := a ; last b +Ltac t2 := do !idtac +Ltac t3 := idtac => True diff --git a/test-suite/output/bug_13240.v b/test-suite/output/bug_13240.v new file mode 100644 index 0000000000..a999450cd2 --- /dev/null +++ b/test-suite/output/bug_13240.v @@ -0,0 +1,10 @@ +Require Import ssreflect. + +Ltac t1 a b := a; last b. +Print t1. + +Ltac t2 := do !idtac. +Print t2. + +Ltac t3 := idtac => True. +Print t3. -- cgit v1.2.3