From 13929f39f8560cfcb3aacf20c84c6dcb5295cec5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 19 Aug 2019 02:35:56 +0200 Subject: [parsing] Make grammar extension type private. After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's. --- plugins/ltac/tacentries.ml | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4af5699317..53b5386375 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -44,11 +44,11 @@ let coincide s pat off = !break let atactic n = - if n = 5 then Aentry Pltac.binder_tactic - else Aentryl (Pltac.tactic_expr, string_of_int n) + if n = 5 then Pcoq.G.Symbol.nterm Pltac.binder_tactic + else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n) type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name + 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.symbol -> entry_name (** Quite ad-hoc *) let get_tacentry n m = @@ -57,8 +57,8 @@ let get_tacentry n m = && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) in - if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself) - else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext) + if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.self) + else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.next) else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function @@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with let rec prod_item_of_symbol lev = function | Extend.Ulist1 s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1 e) + EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1 e) | Extend.Ulist0 s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0 e) + EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0 e) | Extend.Ulist1sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep))) + EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false) | Extend.Ulist0sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep))) + EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false) | Extend.Uopt s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (OptArg typ), Aopt e) + EntryName (Rawwit (OptArg typ), Pcoq.G.Symbol.opt e) | Extend.Uentry arg -> let ArgT.Any tag = arg in let wit = ExtraArg tag in - EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit)) + EntryName (Rawwit wit, Pcoq.G.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in assert (coincide (ArgT.repr tag) "tactic" 0); @@ -399,19 +399,19 @@ let create_ltac_quotation name cast (e, l) = in let () = ltac_quotations := String.Set.add name !ltac_quotations in let entry = match l with - | None -> Aentry e - | Some l -> Aentryl (e, string_of_int l) + | None -> Pcoq.G.Symbol.nterm e + | Some l -> Pcoq.G.Symbol.nterml e (string_of_int l) in (* let level = Some "1" in *) let level = None in let assoc = None in let rule = Next (Next (Next (Next (Next (Stop, - Atoken (CLexer.terminal name)), - Atoken (CLexer.terminal ":")), - Atoken (CLexer.terminal "(")), + Pcoq.G.Symbol.token (CLexer.terminal name)), + Pcoq.G.Symbol.token (CLexer.terminal ":")), + Pcoq.G.Symbol.token (CLexer.terminal "(")), entry), - Atoken (CLexer.terminal ")")) + Pcoq.G.Symbol.token (CLexer.terminal ")")) in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in -- cgit v1.2.3 From 767ecfec49543b70a605d20b1dae8252e1faabfe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 19 Aug 2019 03:17:25 +0200 Subject: [parsing] Make grammar rules private. After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's. --- plugins/ltac/tacentries.ml | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 53b5386375..6b83590b1d 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -406,15 +406,21 @@ let create_ltac_quotation name cast (e, l) = let level = None in let assoc = None in let rule = - Next (Next (Next (Next (Next (Stop, - Pcoq.G.Symbol.token (CLexer.terminal name)), - Pcoq.G.Symbol.token (CLexer.terminal ":")), - Pcoq.G.Symbol.token (CLexer.terminal "(")), - entry), - Pcoq.G.Symbol.token (CLexer.terminal ")")) + Pcoq.G.( + Rule.next + (Rule.next + (Rule.next + (Rule.next + (Rule.next + Rule.stop + (Symbol.token (CLexer.terminal name))) + (Symbol.token (CLexer.terminal ":"))) + (Symbol.token (CLexer.terminal "("))) + entry) + (Symbol.token (CLexer.terminal ")"))) in let action _ v _ _ _ loc = cast (Some loc, v) in - let gram = (level, assoc, [Rule (rule, action)]) in + let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in Pcoq.grammar_extend Pltac.tactic_arg (None, [gram]) (** Command *) -- cgit v1.2.3 From d5dcb490f4f08dc1f5ae4158a26d264e03f808cc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 19 Aug 2019 04:02:09 +0200 Subject: [parsing] Remove extend AST in favor of gramlib constructors We remove Coq's wrapper over gramlib's grammar constructors. --- plugins/ltac/tacentries.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 6b83590b1d..eed7f07b2e 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -48,7 +48,7 @@ let atactic n = else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n) type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.symbol -> entry_name + 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.G.Symbol.t -> entry_name (** Quite ad-hoc *) let get_tacentry n m = @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in + let r = ExtendRule (entry, { G.pos; data=[(None, None, [rules])]}) in ([r], state) let tactic_grammar = @@ -421,7 +421,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in - Pcoq.grammar_extend Pltac.tactic_arg (None, [gram]) + Pcoq.grammar_extend Pltac.tactic_arg {G.pos=None; data=[gram]} (** Command *) @@ -765,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = e | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e {G.pos=None; data=[(None, None, rules)]} in e in let (rpr, gpr, tpr) = arg.arg_printer in -- cgit v1.2.3 From af7628468d638c77fb3f55a9eb315b687b76a21d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 21 Feb 2020 12:20:00 -0500 Subject: [parsing] Remove redundant interfaces from Pcoq There is not need to re-export Gramlib's API in a non-structured way anymore. We thus expose the core Gramlib interface to users and remove redundant functions. A question about whether to move more parts of the API to `Gramlib` is still open, as well as on naming. --- plugins/ltac/g_tactic.mlg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 5a26ac8827..bec83411c1 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -62,7 +62,7 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = - Pcoq.Entry.of_parser "lpar_id_colon" + Pcoq.G.Entry.of_parser "lpar_id_colon" (fun _ strm -> let rec skip_to_rpar p n = match List.last (Stream.npeek n strm) with -- cgit v1.2.3 From f759aaf9de94a11aa34a31c869829d60243d273d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Mar 2020 07:17:57 -0400 Subject: [pcoq] Inline the exported Gramlib interface instead of exposing it as G --- plugins/ltac/g_tactic.mlg | 2 +- plugins/ltac/tacentries.ml | 36 ++++++++++++++++++------------------ 2 files changed, 19 insertions(+), 19 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index bec83411c1..5a26ac8827 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -62,7 +62,7 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = - Pcoq.G.Entry.of_parser "lpar_id_colon" + Pcoq.Entry.of_parser "lpar_id_colon" (fun _ strm -> let rec skip_to_rpar p n = match List.last (Stream.npeek n strm) with diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index eed7f07b2e..4127d28bae 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -44,11 +44,11 @@ let coincide s pat off = !break let atactic n = - if n = 5 then Pcoq.G.Symbol.nterm Pltac.binder_tactic - else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n) + if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic + else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.G.Symbol.t -> entry_name + 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name (** Quite ad-hoc *) let get_tacentry n m = @@ -57,8 +57,8 @@ let get_tacentry n m = && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) in - if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.self) - else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.G.Symbol.next) + if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self) + else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next) else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function @@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with let rec prod_item_of_symbol lev = function | Extend.Ulist1 s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1 e) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e) | Extend.Ulist0 s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0 e) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e) | Extend.Ulist1sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list1sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false) | Extend.Ulist0sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Pcoq.G.Symbol.list0sep e (Pcoq.G.Symbol.token (CLexer.terminal sep)) false) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false) | Extend.Uopt s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (OptArg typ), Pcoq.G.Symbol.opt e) + EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e) | Extend.Uentry arg -> let ArgT.Any tag = arg in let wit = ExtraArg tag in - EntryName (Rawwit wit, Pcoq.G.Symbol.nterm (genarg_grammar wit)) + EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in assert (coincide (ArgT.repr tag) "tactic" 0); @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - let r = ExtendRule (entry, { G.pos; data=[(None, None, [rules])]}) in + let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in ([r], state) let tactic_grammar = @@ -399,14 +399,14 @@ let create_ltac_quotation name cast (e, l) = in let () = ltac_quotations := String.Set.add name !ltac_quotations in let entry = match l with - | None -> Pcoq.G.Symbol.nterm e - | Some l -> Pcoq.G.Symbol.nterml e (string_of_int l) + | None -> Pcoq.Symbol.nterm e + | Some l -> Pcoq.Symbol.nterml e (string_of_int l) in (* let level = Some "1" in *) let level = None in let assoc = None in let rule = - Pcoq.G.( + Pcoq.( Rule.next (Rule.next (Rule.next @@ -420,8 +420,8 @@ let create_ltac_quotation name cast (e, l) = (Symbol.token (CLexer.terminal ")"))) in let action _ v _ _ _ loc = cast (Some loc, v) in - let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in - Pcoq.grammar_extend Pltac.tactic_arg {G.pos=None; data=[gram]} + let gram = (level, assoc, [Pcoq.Production.make rule action]) in + Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]} (** Command *) @@ -765,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = e | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e {G.pos=None; data=[(None, None, rules)]} in + let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in e in let (rpr, gpr, tpr) = arg.arg_printer in -- cgit v1.2.3