From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- grammar/tacextend.mlp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'grammar') diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 1dd8da12a..b14fba975 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -129,7 +129,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let gl = mlexpr_of_clause clause in let level = mlexpr_of_int level in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in declare_str_items loc [ <:str_item< do { Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); -- cgit v1.2.3 From cd3971e53b76cb62e14822eb3e275d3968a4f215 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 15 May 2017 22:30:09 +0200 Subject: Adding support for using grammar entries returning no value in EXTEND. --- dev/top_printers.ml | 4 ++-- grammar/argextend.mlp | 12 ++++++++---- grammar/q_util.mli | 2 +- grammar/q_util.mlp | 2 +- grammar/tacextend.mlp | 17 ++++++++++------- grammar/vernacextend.mlp | 16 ++++++++++------ parsing/egramml.ml | 4 ++-- parsing/egramml.mli | 2 +- plugins/ltac/g_ltac.ml4 | 8 ++++++-- plugins/ltac/pptactic.ml | 7 ++++--- plugins/ltac/pptactic.mli | 2 +- plugins/ltac/tacentries.ml | 14 +++++++------- plugins/ltac/tacentries.mli | 2 +- 13 files changed, 54 insertions(+), 38 deletions(-) (limited to 'grammar') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f8498c402..ce6d5dff0 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -510,7 +510,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)] let _ = try @@ -526,7 +526,7 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] + (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)] (* Setting printer of unbound global reference *) open Names diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index d00ee4e5d..5cfcc6fd2 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -40,7 +40,8 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >> + | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) @@ -63,7 +64,7 @@ let is_ident x = function | _ -> false let make_extend loc s cl wit = match cl with -| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act -> +| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act -> (** Special handling of identity arguments by not redeclaring an entry *) <:str_item< value $lid:s$ = @@ -246,10 +247,13 @@ EXTEND genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> ExtTerminal s ] ] ; diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 5b3eb3202..0b3def058 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -23,7 +23,7 @@ type user_symbol = type extend_token = | ExtTerminal of string -| ExtNonTerminal of user_symbol * string +| ExtNonTerminal of user_symbol * string option val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 8b930cf36..87262e1c8 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -25,7 +25,7 @@ type user_symbol = type extend_token = | ExtTerminal of string -| ExtNonTerminal of user_symbol * string +| ExtNonTerminal of user_symbol * string option let mlexpr_of_list f l = List.fold_right diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index b14fba975..3057ee58c 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -31,19 +31,19 @@ let mlexpr_of_ident id = let rec make_patt = function | [] -> <:patt< [] >> - | ExtNonTerminal (_, p) :: l -> + | ExtNonTerminal (_, Some p) :: l -> <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, p) :: l -> + | ExtNonTerminal (g, Some p) :: l -> let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let raw e l in let v = if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in + else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l @@ -75,7 +75,7 @@ let rec mlexpr_of_symbol = function let make_prod_item = function | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> + <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_option mlexpr_of_ident id$ >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl @@ -87,7 +87,7 @@ let is_constr_gram = function | _ -> false let make_var = function - | ExtNonTerminal (_, p) -> Some p + | ExtNonTerminal (_, p) -> p | _ -> assert false let declare_tactic loc tacname ~level classification clause = match clause with @@ -158,10 +158,13 @@ EXTEND tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> let () = if s = "" then failwith "Empty terminal." in ExtTerminal s diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 436a7f0d9..7c99b52e8 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -27,7 +27,7 @@ type rule = { let rec make_let e = function | [] -> e - | ExtNonTerminal (g, p) :: l -> + | ExtNonTerminal (g, Some p) :: l -> let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let e l in @@ -42,7 +42,7 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = let fold accu = function - | ExtNonTerminal (_, p) -> p :: accu + | ExtNonTerminal (_, Some p) -> p :: accu | _ -> accu in let names = List.fold_left fold [] pt in @@ -101,10 +101,11 @@ let make_fun_classifiers loc s c l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | ExtNonTerminal (g, id) -> + | ExtNonTerminal (g, ido) -> let nt = type_of_user_symbol g in let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in - <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ + let typ = match ido with None -> None | Some _ -> Some nt in + <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_option (make_rawwit loc) typ$ $mlexpr_of_prod_entry_key base g$ >> let mlexpr_of_clause cl = @@ -178,10 +179,13 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (e, s) + ExtNonTerminal (e, Some s) + | e = LIDENT -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, None) | s = STRING -> ExtTerminal s ] ] diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 97a3e89a5..984957589 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -17,7 +17,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item + Loc.t * 'a raw_abstract_argument_type option * ('s, 'a) symbol -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) @@ -38,7 +38,7 @@ let rec ty_rule_of_gram = function AnyTyRule r | GramNonTerminal (_, t, tok) :: rem -> let AnyTyRule rem = ty_rule_of_gram rem in - let inj = Some (fun obj -> Genarg.in_gen t obj) in + let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in let r = TyNext (rem, tok, inj) in AnyTyRule r diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 1ad947200..29baaf052 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -15,7 +15,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string - | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type * + | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type option * ('s, 'a) Extend.symbol -> 's grammar_prod_item val extend_vernac_command_grammar : diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ca5d198c2..d717ed0a5 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -460,7 +460,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, sep), id) -> +| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg +| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false +| Tacentries.TacNonTerm (_, (arg, sep), Some id) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -470,7 +472,9 @@ let pr_ltac_production_item = function 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, (Names.Id.to_string nt, sep), p) ] + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b73b66e56..a61957559 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -264,8 +264,9 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (loc, symb, id) :: prods, arg :: args -> - TacNonTerm (loc, (symb, arg), id) :: pack prods args + | TacNonTerm (_, _, None) :: prods, args -> pack prods args + | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args -> + TacNonTerm (loc, (symb, arg), ido) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 729338fb9..433f342c4 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -21,7 +21,7 @@ open Ppextend type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 32750383b..91262f6fd 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -21,7 +21,7 @@ open Nameops type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state = in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, _) -> + | TacNonTerm (loc, s, ido) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (loc, typ, e) + GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s - | TacNonTerm (loc, (nt, sep), id) -> + | TacNonTerm (loc, (nt, sep), ido) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> @@ -220,7 +220,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, id) + TacNonTerm (loc, symbol, ido) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, _, id) -> Some id +| TacNonTerm (_, _, ido) -> ido let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, _, id) -> Some id + | TacNonTerm (_, _, ido) -> ido in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 069504473..dac62dad3 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type raw_argument = string * string option (** An argument type as provided in Tactic notations, i.e. a string like -- cgit v1.2.3