From 4a88beff476d2c27eae381bc8a61f777015c0617 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 21:57:46 -0400 Subject: [gitlab] Increase flambda stack size. See https://github.com/ocaml/ocaml/issues/7842 --- .gitlab-ci.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ebeee0d4e4..df71ab3c2f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -103,6 +103,9 @@ before_script: interruptible: true dependencies: [] script: + # flambda can be pretty stack hungry, specially with -O3 + # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244 + - ulimit -s 16384 - set -e - make -f Makefile.dune world - set +e -- cgit v1.2.3 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. --- coqpp/coqpp_main.ml | 32 +-- gramlib/grammar.ml | 11 +- gramlib/grammar.mli | 8 +- parsing/extend.ml | 33 ---- parsing/pcoq.ml | 393 ++++++++++++++++++++++--------------- parsing/pcoq.mli | 36 +++- plugins/ltac/tacentries.ml | 34 ++-- user-contrib/Ltac2/g_ltac2.mlg | 9 +- user-contrib/Ltac2/tac2core.ml | 71 +++---- user-contrib/Ltac2/tac2entries.ml | 14 +- user-contrib/Ltac2/tac2entries.mli | 2 +- vernac/egramcoq.ml | 73 ++++--- vernac/egramml.ml | 16 +- vernac/egramml.mli | 4 +- vernac/pvernac.ml | 5 +- vernac/vernacextend.ml | 18 +- vernac/vernacextend.mli | 2 +- 17 files changed, 420 insertions(+), 341 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index bdffabf0b2..5d1f0a876f 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -217,43 +217,43 @@ let rec print_prod fmt p = and print_extrule fmt (tkn, vars, body) = let tkn = List.rev tkn in - fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body) + fprintf fmt "@[Pcoq.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body) and print_symbols ~norec fmt = function -| [] -> fprintf fmt "Extend.Stop" +| [] -> fprintf fmt "Pcoq.Stop" | tkn :: tkns -> - let c = if norec then "Extend.NextNoRec" else "Extend.Next" in + let c = if norec then "Pcoq.NextNoRec" else "Pcoq.Next" in fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> - fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) + fprintf fmt "(Pcoq.G.Symbol.token (%a))" print_tok (t, s) | SymbEntry (e, None) -> - fprintf fmt "(Extend.Aentry %s)" e + fprintf fmt "(Pcoq.G.Symbol.nterm %s)" e | SymbEntry (e, Some l) -> - fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l + fprintf fmt "(Pcoq.G.Symbol.nterml %s (%a))" e print_string l | SymbSelf -> - fprintf fmt "Extend.Aself" + fprintf fmt "Pcoq.G.Symbol.self" | SymbNext -> - fprintf fmt "Extend.Anext" + fprintf fmt "Pcoq.G.Symbol.next" | SymbList0 (s, None) -> - fprintf fmt "(Extend.Alist0 %a)" print_symbol s + fprintf fmt "(Pcoq.G.Symbol.list0 %a)" print_symbol s | SymbList0 (s, Some sep) -> - fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Pcoq.G.Symbol.list0sep (%a) (%a) false)" print_symbol s print_symbol sep | SymbList1 (s, None) -> - fprintf fmt "(Extend.Alist1 %a)" print_symbol s + fprintf fmt "(Pcoq.G.Symbol.list1 (%a))" print_symbol s | SymbList1 (s, Some sep) -> - fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Pcoq.G.Symbol.list1sep (%a) (%a) false)" print_symbol s print_symbol sep | SymbOpt s -> - fprintf fmt "(Extend.Aopt %a)" print_symbol s + fprintf fmt "(Pcoq.G.Symbol.opt %a)" print_symbol s | SymbRules rules -> let pr fmt (r, body) = let (vars, tkn) = List.split r in let tkn = List.rev tkn in - fprintf fmt "Extend.Rules @[(%a,@ (%a))@]" (print_symbols ~norec:true) tkn print_fun (vars, body) + fprintf fmt "Pcoq.G.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body) in let pr fmt rules = print_list fmt pr rules in - fprintf fmt "(Extend.Arules %a)" pr (List.rev rules) + fprintf fmt "(Pcoq.G.Symbol.rules ~warning:None %a)" pr (List.rev rules) | SymbQuote c -> fprintf fmt "(%s)" c @@ -452,7 +452,7 @@ let terminal s = let p = if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_numeral" else "CLexer.terminal" in - let c = Printf.sprintf "Extend.Atoken (%s \"%s\")" p s in + let c = Printf.sprintf "Pcoq.G.Symbol.token (%s \"%s\")" p s in SymbQuote c let rec parse_symb self = function diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 0024d70466..818608674e 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -77,8 +77,7 @@ module type S = sig val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t end - module Unsafe : - sig + module Unsafe : sig val clear_entry : 'a Entry.t -> unit end val safe_extend : warning:(string -> unit) option -> @@ -87,6 +86,10 @@ module type S = sig list -> unit val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit + + (* Used in custom entries, should tweak? *) + val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option + end (* Implementation *) @@ -1666,4 +1669,8 @@ let safe_delete_rule e r = let AnyS (symbols, _) = get_symbols r in delete_rule e symbols +let level_of_nonterm sym = match sym with + | Snterml (_,l) -> Some l + | _ -> None + end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index f0423a92af..4ac85bd358 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -86,16 +86,20 @@ module type S = sig val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t end - module Unsafe : - sig + module Unsafe : sig val clear_entry : 'a Entry.t -> unit end + val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a Production.t list) list -> unit val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit + + (* Used in custom entries, should tweak? *) + val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option + end (** Signature type of the functor [Grammar.GMake]. The types and functions are almost the same than in generic interface, but: diff --git a/parsing/extend.ml b/parsing/extend.ml index 20297fa156..9c7f5c87c4 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -77,36 +77,3 @@ type ('a,'b,'c) ty_user_symbol = | TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol - -(** {5 Type-safe grammar extension} *) - -(* Should be merged with gramlib's implementation *) - -type norec = Gramlib.Grammar.norec -type mayrec = Gramlib.Grammar.mayrec - -type ('self, 'trec, 'a) symbol = -| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol -| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol -| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol - -> ('self, 'trec, 'a list) symbol -| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol -| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol - -> ('self, 'trec, 'a list) symbol -| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol -| Aself : ('self, mayrec, 'self) symbol -| Anext : ('self, mayrec, 'self) symbol -| Aentry : 'a entry -> ('self, norec, 'a) symbol -| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol -| Arules : 'a rules list -> ('self, norec, 'a) symbol - -and ('self, 'trec, _, 'r) rule = -| Stop : ('self, norec, 'r, 'r) rule -| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule -| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule - -and 'a rules = -| Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules - -type 'a production_rule = -| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b3f997e1b3..5601dcb474 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -15,109 +15,256 @@ open Genarg open Gramlib (** The parser of Coq *) -module G : sig - include Grammar.S with type te = Tok.t and type 'c pattern = 'c Tok.p - -(* where Grammar.S - -module type S = - sig - type te = 'x; - type parsable = 'x; - value parsable : Stream.t char -> parsable; - value tokens : string -> list (string * int); - value glexer : Plexing.lexer te; - value set_algorithm : parse_algorithm -> unit; - module Entry : - sig - type e 'a = 'y; - value create : string -> e 'a; - value parse : e 'a -> parsable -> 'a; - value parse_token_stream : e 'a -> Stream.t te -> 'a; - value name : e 'a -> string; - value of_parser : string -> (Stream.t te -> 'a) -> e 'a; - value print : Format.formatter -> e 'a -> unit; - external obj : e 'a -> Gramext.g_entry te = "%identity"; - end - ; - module Unsafe : - sig - value gram_reinit : Plexing.lexer te -> unit; - value clear_entry : Entry.e 'a -> unit; - end - ; - value extend : - Entry.e 'a -> option Gramext.position -> - list - (option string * option Gramext.g_assoc * - list (list (Gramext.g_symbol te) * Gramext.g_action)) -> - unit; - value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; - end - *) +type norec = Gramlib.Grammar.norec +type mayrec = Gramlib.Grammar.mayrec + +type ('self, 'trec, 'a) symbol = +| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol +| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol +| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol + -> ('self, 'trec, 'a list) symbol +| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol +| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol + -> ('self, 'trec, 'a list) symbol +| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol +| Aself : ('self, mayrec, 'self) symbol +| Anext : ('self, mayrec, 'self) symbol +| Aentry : 'a entry -> ('self, norec, 'a) symbol +| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol +| Arules : 'a rules list -> ('self, norec, 'a) symbol + +and ('self, 'trec, _, 'r) rule = +| Stop : ('self, norec, 'r, 'r) rule +| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule +| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule + +and 'a rules = +| Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules + +type 'a production_rule = +| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - type coq_parsable +module G : sig - val coq_parsable : ?loc:Loc.t -> char Stream.t -> coq_parsable - val entry_create : string -> 'a entry - val entry_parse : 'a entry -> coq_parsable -> 'a + include Grammar.S + with type te = Tok.t + and type 'c pattern = 'c Tok.p + and type 'a pattern = 'a Tok.p + and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol + and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule + and type 'a Rules.t = 'a rules + and type 'a Production.t = 'a production_rule - val comment_state : coq_parsable -> ((int * int) * string) list + val comment_state : Parsable.t -> ((int * int) * string) list + val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option + val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option end with type 'a Entry.t = 'a Extend.entry = struct - include Grammar.GMake(CLexer.Lexer) + module G_ = Grammar.GMake(CLexer.Lexer) - type coq_parsable = Parsable.t * CLexer.lexer_state ref + type te = G_.te + type 'c pattern = 'c G_.pattern + + type coq_parsable = G_.Parsable.t * CLexer.lexer_state ref let coq_parsable ?loc c = let state = ref (CLexer.init_lexer_state ()) in CLexer.set_lexer_state !state; - let a = Parsable.make ?loc c in + let a = G_.Parsable.make ?loc c in state := CLexer.get_lexer_state (); (a,state) - let entry_create = Entry.make - - let entry_parse e (p,state) = - CLexer.set_lexer_state !state; - try - let c = Entry.parse e p in - state := CLexer.get_lexer_state (); - c - with Ploc.Exc (loc,e) -> - CLexer.drop_lexer_state (); - let loc' = Loc.get_loc (Exninfo.info e) in - let loc = match loc' with None -> loc | Some loc -> loc in - Loc.raise ~loc e - let comment_state (p,state) = CLexer.get_comment_state !state -end + module Parsable = struct + type t = coq_parsable + let make = coq_parsable + (* let comment_state = comment_state *) + end -module Parsable = -struct - type t = G.coq_parsable - let make = G.coq_parsable - let comment_state = G.comment_state -end + let tokens = G_.tokens -module Entry = -struct + module Entry = struct + include G_.Entry + + let parse e (p,state) = + CLexer.set_lexer_state !state; + try + let c = G_.Entry.parse e p in + state := CLexer.get_lexer_state (); + c + with Ploc.Exc (loc,e) -> + CLexer.drop_lexer_state (); + let loc' = Loc.get_loc (Exninfo.info e) in + let loc = match loc' with None -> loc | Some loc -> loc in + Loc.raise ~loc e + + end + + module Symbol = struct + type ('self, 'trec, 'a) t = ('self, 'trec, 'a) symbol + let token tok = Atoken tok + let list0 e = Alist0 e + let list0sep e s _ = Alist0sep (e,s) + let list1 e = Alist1 e + let list1sep e s _ = Alist1sep (e,s) + let opt e = Aopt e + let self = Aself + let next = Anext + let nterm e = Aentry e + let nterml e s = Aentryl (e,s) + let rules ~warning:_ r = Arules r + end - type 'a t = 'a Grammar.GMake(CLexer.Lexer).Entry.t + module Rule = struct + type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) rule + let stop = Stop + let next a b = Next (a,b) + let next_norec a b = NextNoRec (a,b) + end - let create = G.Entry.make - let parse = G.entry_parse - let print = G.Entry.print - let of_parser = G.Entry.of_parser - let name = G.Entry.name - let parse_token_stream = G.Entry.parse_token_stream + module Rules = struct + type 'a t = 'a rules + let make a f = Rules(a,f) + end + + module Production = struct + type 'a t = 'a production_rule + let make a f = Rule(a,f) + end + + module Unsafe = struct + let clear_entry = G_.Unsafe.clear_entry + end + + (** FIXME: This is a hack around a deficient camlp5 API *) + type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G_.Rule.t * 'f -> 'a any_production + + let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G_.Symbol.t = + function + | Atoken t -> G_.Symbol.token t + | Alist1 s -> + let s = symbol_of_prod_entry_key s in + G_.Symbol.list1 s + | Alist1sep (s,sep) -> + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G_.Symbol.list1sep s sep false + | Alist0 s -> + let s = symbol_of_prod_entry_key s in + G_.Symbol.list0 s + | Alist0sep (s,sep) -> + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G_.Symbol.list0sep s sep false + | Aopt s -> + let s = symbol_of_prod_entry_key s in + G_.Symbol.opt s + | Aself -> G_.Symbol.self + | Anext -> G_.Symbol.next + | Aentry e -> G_.Symbol.nterm e + | Aentryl (e, n) -> G_.Symbol.nterml e n + | Arules rs -> + let warning msg = Feedback.msg_warning Pp.(str msg) in + G_.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs) + + and symbol_of_rule : type s tr a r. (s, tr, a, r) rule -> (s, tr, a, r) G_.Rule.t = function + | Stop -> + G_.Rule.stop + | Next (r, s) -> + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G_.Rule.next r s + | NextNoRec (r, s) -> + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G_.Rule.next_norec r s + + and symbol_of_rules : type a. a rules -> a G_.Rules.t = function + | Rules (r, act) -> + let symb = symbol_of_rule r in + G_.Rules.make symb act + + let of_coq_production_rule : type a. a production_rule -> a any_production = function + | Rule (toks, act) -> + AnyProduction (symbol_of_rule toks, act) + + let of_coq_single_extend_statement (lvl, assoc, rule) = + (lvl, assoc, List.map of_coq_production_rule rule) + + let of_coq_extend_statement (pos, st) = + (pos, List.map of_coq_single_extend_statement st) + + let fix_extend_statement (pos, st) = + let fix_single_extend_statement (lvl, assoc, rules) = + let fix_production_rule (AnyProduction (s, act)) = G_.Production.make s act in + (lvl, assoc, List.map fix_production_rule rules) + in + (pos, List.map fix_single_extend_statement st) + + let safe_extend ~warning e pos ext = + let pos, ext = of_coq_extend_statement (pos,ext) in + let pos, ext = fix_extend_statement (pos, ext) in + G_.safe_extend ~warning e pos ext + + let safe_delete_rule e r = + let r = symbol_of_rule r in + G_.safe_delete_rule e r + + let level_of_nonterm = function + | Aentryl (_,l) -> Some l + | _ -> None + + exception SelfSymbol + let rec generalize_symbol : + type a tr s. (s, tr, a) symbol -> (s, norec, a) symbol = + function + | Atoken tok -> + Atoken tok + | Alist1 e -> + Alist1 (generalize_symbol e) + | Alist1sep (e, sep) -> + let e = generalize_symbol e in + let sep = generalize_symbol sep in + Alist1sep (e, sep) + | Alist0 e -> + Alist0 (generalize_symbol e) + | Alist0sep (e, sep) -> + let e = generalize_symbol e in + let sep = generalize_symbol sep in + Alist0sep (e, sep) + | Aopt e -> + Aopt (generalize_symbol e) + | Aself -> + raise SelfSymbol + | Anext -> + raise SelfSymbol + | Aentry e -> + Aentry e + | Aentryl (e, l) -> + Aentryl (e, l) + | Arules r -> + Arules r + + let generalize_symbol s = + try Some (generalize_symbol s) + with SelfSymbol -> None end +module Parsable = struct + include G.Parsable + let comment_state = G.comment_state +end + +module Entry = struct + include G.Entry + let create = make +end + module Lookahead = struct @@ -189,71 +336,6 @@ end (** Binding general entry keys to symbol *) -let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.Symbol.t = -function -| Atoken t -> G.Symbol.token t -| Alist1 s -> - let s = symbol_of_prod_entry_key s in - G.Symbol.list1 s -| Alist1sep (s,sep) -> - let s = symbol_of_prod_entry_key s in - let sep = symbol_of_prod_entry_key sep in - G.Symbol.list1sep s sep false -| Alist0 s -> - let s = symbol_of_prod_entry_key s in - G.Symbol.list0 s -| Alist0sep (s,sep) -> - let s = symbol_of_prod_entry_key s in - let sep = symbol_of_prod_entry_key sep in - G.Symbol.list0sep s sep false -| Aopt s -> - let s = symbol_of_prod_entry_key s in - G.Symbol.opt s -| Aself -> G.Symbol.self -| Anext -> G.Symbol.next -| Aentry e -> G.Symbol.nterm e -| Aentryl (e, n) -> G.Symbol.nterml e n -| Arules rs -> - let warning msg = Feedback.msg_warning Pp.(str msg) in - G.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs) - -and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.Rule.t = function -| Stop -> - G.Rule.stop -| Next (r, s) -> - let r = symbol_of_rule r in - let s = symbol_of_prod_entry_key s in - G.Rule.next r s -| NextNoRec (r, s) -> - let r = symbol_of_rule r in - let s = symbol_of_prod_entry_key s in - G.Rule.next_norec r s - -and symbol_of_rules : type a. a Extend.rules -> a G.Rules.t = function -| Rules (r, act) -> - let symb = symbol_of_rule r in - G.Rules.make symb act - -(** FIXME: This is a hack around a deficient camlp5 API *) -type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.Rule.t * 'f -> 'a any_production - -let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function -| Rule (toks, act) -> - AnyProduction (symbol_of_rule toks, act) - -let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, assoc, List.map of_coq_production_rule rule) - -let of_coq_extend_statement (pos, st) = - (pos, List.map of_coq_single_extend_statement st) - -let fix_extend_statement (pos, st) = - let fix_single_extend_statement (lvl, assoc, rules) = - let fix_production_rule (AnyProduction (s, act)) = G.Production.make s act in - (lvl, assoc, List.map fix_production_rule rules) - in - (pos, List.map fix_single_extend_statement st) - (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position @@ -293,7 +375,7 @@ let camlp5_entries = ref EntryDataMap.empty let grammar_delete e (pos,rls) = List.iter (fun (n,ass,lev) -> - List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) + List.iter (fun (Rule(pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) (List.rev rls) let grammar_delete_reinit e reinit (pos, rls) = @@ -308,22 +390,20 @@ let grammar_delete_reinit e reinit (pos, rls) = (** Extension *) -let grammar_extend e ext = - let ext = of_coq_extend_statement ext in - let undo () = grammar_delete e ext in - let pos, ext = fix_extend_statement ext in +let grammar_extend e (pos,ext) = + let undo () = grammar_delete e (pos,ext) in let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e ext = camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; - let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + let pos, ext = ext in G.safe_extend ~warning:None e pos ext let grammar_extend_sync_reinit e reinit ext = camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; - let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + let pos, ext = ext in G.safe_extend ~warning:None e pos ext (** The apparent parser of Coq; encapsulate G to keep track @@ -344,11 +424,11 @@ let rec remove_grammars n = match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t -> - grammar_delete_reinit g reinit (of_coq_extend_statement ext); + grammar_delete_reinit g reinit ext; camlp5_state := t; remove_grammars (n-1) | ByGrammar (ExtendRule (g, ext)) :: t -> - grammar_delete g (of_coq_extend_statement ext); + grammar_delete g ext; camlp5_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -393,7 +473,7 @@ let map_entry f en = let parse_string f ?loc x = let strm = Stream.of_string x in - Gram.entry_parse f (Gram.coq_parsable ?loc strm) + G.Entry.parse f (G.Parsable.make ?loc strm) type gram_universe = string @@ -531,10 +611,9 @@ module Module = end let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = - let s = symbol_of_prod_entry_key e in - let r = G.Production.make (G.Rule.next G.Rule.stop s) (fun x _ -> f x) in + let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in let ext = [None, None, [r]] in - let entry = Gram.entry_create "epsilon" in + let entry = G.Entry.make "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in let () = G.safe_extend ~warning:(Some warning) entry None ext in try Some (parse_string entry "") with _ -> None @@ -601,7 +680,7 @@ let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) | (_, st) :: _ -> st in let (names, st) = modify g grammar_state in - let entries = List.map (fun name -> Gram.entry_create name) names in + let entries = List.map (fun name -> G.Entry.make name) names in let iter name e = camlp5_state := ByEntry (tag, name, e) :: !camlp5_state; let EntryData.Ex old = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 87c7f168ce..63a4c1dd58 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Extend open Genarg open Constrexpr open Libnames @@ -222,7 +221,40 @@ module Module : val module_type : module_ast Entry.t end -val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self option +(** {5 Type-safe grammar extension} *) + +type ('self, 'trec, 'a) symbol + +type norec = Gramlib.Grammar.norec +type mayrec = Gramlib.Grammar.mayrec + +type ('self, 'trec, _, 'r) rule = +| Stop : ('self, norec, 'r, 'r) rule +| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule +| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule + +type 'a rules = + | Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules + +type 'a production_rule = + | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + +module G : sig + + include Gramlib.Grammar.S + + val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option + val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option + +end with type 'a Entry.t = 'a Entry.t + and type te = Tok.t + and type 'a pattern = 'a Tok.p + and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol + and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule + and type 'a Rules.t = 'a rules + and type 'a Production.t = 'a production_rule + +val epsilon_value : ('a -> 'self) -> ('self, _, 'a) symbol -> 'self option (** {5 Extending the parser without synchronization} *) 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 diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 5e04959e9a..52d92d87c0 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -826,12 +826,11 @@ END let () = -let open Extend in let open Tok in let (++) r s = Next (r, s) in let rules = [ Rule ( - Stop ++ Aentry test_dollar_ident ++ Atoken (PKEYWORD "$") ++ Aentry Prim.ident, + Stop ++ Pcoq.G.Symbol.nterm test_dollar_ident ++ Pcoq.G.Symbol.token (PKEYWORD "$") ++ Pcoq.G.Symbol.nterm Prim.ident, begin fun id _ _ loc -> let id = Loc.tag ~loc id in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in @@ -840,7 +839,7 @@ let rules = [ ); Rule ( - Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident, + Stop ++ Pcoq.G.Symbol.nterm test_ampersand_ident ++ Pcoq.G.Symbol.token (PKEYWORD "&") ++ Pcoq.G.Symbol.nterm Prim.ident, begin fun id _ _ loc -> let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in @@ -849,8 +848,8 @@ let rules = [ ); Rule ( - Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++ - Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"), + Stop ++ Pcoq.G.Symbol.token (PIDENT (Some "ltac2")) ++ Pcoq.G.Symbol.token (PKEYWORD ":") ++ + Pcoq.G.Symbol.token (PKEYWORD "(") ++ Pcoq.G.Symbol.nterm tac2expr ++ Pcoq.G.Symbol.token (PKEYWORD ")"), begin fun _ tac _ _ _ loc -> let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 38b05bed6b..2edbcc38f5 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1431,7 +1431,7 @@ let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) let add_generic_scope s entry arg = let parse = function | [] -> - let scope = Extend.Aentry entry in + let scope = Pcoq.G.Symbol.nterm entry in let act x = CAst.make @@ CTacExt (arg, x) in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail s arg @@ -1442,14 +1442,14 @@ open CAst let () = add_scope "keyword" begin function | [SexprStr {loc;v=s}] -> - let scope = Extend.Atoken (Tok.PKEYWORD s) in + let scope = Pcoq.G.Symbol.token (Tok.PKEYWORD s) in Tac2entries.ScopeRule (scope, (fun _ -> q_unit)) | arg -> scope_fail "keyword" arg end let () = add_scope "terminal" begin function | [SexprStr {loc;v=s}] -> - let scope = Extend.Atoken (CLexer.terminal s) in + let scope = Pcoq.G.Symbol.token (CLexer.terminal s) in Tac2entries.ScopeRule (scope, (fun _ -> q_unit)) | arg -> scope_fail "terminal" arg end @@ -1457,13 +1457,13 @@ end let () = add_scope "list0" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let scope = Extend.Alist0 scope in + let scope = Pcoq.G.Symbol.list0 scope in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | [tok; SexprStr {v=str}] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let sep = Extend.Atoken (CLexer.terminal str) in - let scope = Extend.Alist0sep (scope, sep) in + let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in + let scope = Pcoq.G.Symbol.list0sep scope sep false in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "list0" arg @@ -1472,13 +1472,13 @@ end let () = add_scope "list1" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let scope = Extend.Alist1 scope in + let scope = Pcoq.G.Symbol.list1 scope in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | [tok; SexprStr {v=str}] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let sep = Extend.Atoken (CLexer.terminal str) in - let scope = Extend.Alist1sep (scope, sep) in + let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in + let scope = Pcoq.G.Symbol.list1sep scope sep false in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "list1" arg @@ -1487,7 +1487,7 @@ end let () = add_scope "opt" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let scope = Extend.Aopt scope in + let scope = Pcoq.G.Symbol.opt scope in let act opt = match opt with | None -> CAst.make @@ CTacCst (AbsKn (Other Core.c_none)) @@ -1500,7 +1500,7 @@ end let () = add_scope "self" begin function | [] -> - let scope = Extend.Aself in + let scope = Pcoq.G.Symbol.self in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "self" arg @@ -1508,7 +1508,7 @@ end let () = add_scope "next" begin function | [] -> - let scope = Extend.Anext in + let scope = Pcoq.G.Symbol.next in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "next" arg @@ -1517,12 +1517,12 @@ end let () = add_scope "tactic" begin function | [] -> (* Default to level 5 parsing *) - let scope = Extend.Aentryl (tac2expr, "5") in + let scope = Pcoq.G.Symbol.nterml tac2expr "5" in let act tac = tac in Tac2entries.ScopeRule (scope, act) | [SexprInt {loc;v=n}] as arg -> let () = if n < 0 || n > 6 then scope_fail "tactic" arg in - let scope = Extend.Aentryl (tac2expr, string_of_int n) in + let scope = Pcoq.G.Symbol.nterml tac2expr (string_of_int n) in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "tactic" arg @@ -1543,12 +1543,12 @@ let () = add_scope "constr" (fun arg -> arg in let act e = Tac2quote.of_constr ~delimiters e in - Tac2entries.ScopeRule (Extend.Aentry Pcoq.Constr.constr, act) + Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm Pcoq.Constr.constr, act) ) let add_expr_scope name entry f = add_scope name begin function - | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f) + | [] -> Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm entry, f) | arg -> scope_fail name arg end @@ -1578,28 +1578,7 @@ let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern (** seq scope, a bit hairy *) -open Extend -exception SelfSymbol - -let rec generalize_symbol : - type a tr s. (s, tr, a) Extend.symbol -> (s, Extend.norec, a) Extend.symbol = function -| Atoken tok -> Atoken tok -| Alist1 e -> Alist1 (generalize_symbol e) -| Alist1sep (e, sep) -> - let e = generalize_symbol e in - let sep = generalize_symbol sep in - Alist1sep (e, sep) -| Alist0 e -> Alist0 (generalize_symbol e) -| Alist0sep (e, sep) -> - let e = generalize_symbol e in - let sep = generalize_symbol sep in - Alist0sep (e, sep) -| Aopt e -> Aopt (generalize_symbol e) -| Aself -> raise SelfSymbol -| Anext -> raise SelfSymbol -| Aentry e -> Aentry e -| Aentryl (e, l) -> Aentryl (e, l) -| Arules r -> Arules r +open Pcoq type _ converter = | CvNil : (Loc.t -> raw_tacexpr) converter @@ -1611,14 +1590,19 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu) type seqrule = -| Seqrule : (Tac2expr.raw_tacexpr, Extend.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule +| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule let rec make_seq_rule = function | [] -> Seqrule (Stop, CvNil) | tok :: rem -> let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in - let scope = generalize_symbol scope in + let scope = + match Pcoq.G.generalize_symbol scope with + | None -> + CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules") + | Some scope -> scope + in let Seqrule (r, c) = make_seq_rule rem in let r = NextNoRec (r, scope) in let f = match tok with @@ -1629,11 +1613,8 @@ let rec make_seq_rule = function let () = add_scope "seq" begin fun toks -> let scope = - try - let Seqrule (r, c) = make_seq_rule (List.rev toks) in - Arules [Rules (r, apply c [])] - with SelfSymbol -> - CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules") + let Seqrule (r, c) = make_seq_rule (List.rev toks) in + Pcoq.G.Symbol.rules ~warning:None [Rules (r, apply c [])] in Tac2entries.ScopeRule (scope, (fun e -> e)) end diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index e9945794d3..d5d5bad987 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -558,7 +558,7 @@ type 'a token = | TacNonTerm of Name.t * 'a type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule @@ -583,7 +583,7 @@ let parse_scope = function CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id) | SexprStr {v=str} -> let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in - ScopeRule (Extend.Atoken (Tok.PIDENT (Some str)), (fun _ -> v_unit)) + ScopeRule (Pcoq.G.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit)) | tok -> let loc = loc_of_token tok in CErrors.user_err ?loc (str "Invalid parsing token") @@ -611,19 +611,19 @@ type synext = { type krule = | KRule : - (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Extend.rule * + (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.rule * ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule let rec get_rule (tok : scope_rule token list) : krule = match tok with -| [] -> KRule (Extend.Stop, fun k loc -> k loc []) +| [] -> KRule (Pcoq.Stop, fun k loc -> k loc []) | TacNonTerm (na, ScopeRule (scope, inj)) :: tok -> let KRule (rule, act) = get_rule tok in - let rule = Extend.Next (rule, scope) in + let rule = Pcoq.Next (rule, scope) in let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in KRule (rule, act) | TacTerm t :: tok -> let KRule (rule, act) = get_rule tok in - let rule = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in + let rule = Pcoq.Next (rule, Pcoq.G.Symbol.token (CLexer.terminal t)) in let act k _ = act k in KRule (rule, act) @@ -637,7 +637,7 @@ let perform_notation syn st = let bnd = List.map map args in CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp) in - let rule = Extend.Rule (rule, act mk) in + let rule = Pcoq.Rule (rule, act mk) in let lev = match syn.synext_lev with | None -> None | Some lev -> Some (string_of_int lev) diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index fed43a4dd5..4938e96cae 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit (** {5 Notations} *) type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5dae389a62..ba542101c8 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -325,51 +325,56 @@ let is_binder_level custom (custom',from) e = match e with | _ -> false let make_sep_rules = function - | [tk] -> Atoken tk + | [tk] -> + Pcoq.G.Symbol.token tk | tkl -> - let rec mkrule : 'a Tok.p list -> 'a rules = function - | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "") - | tkn :: rem -> - let Rules (r, f) = mkrule rem in - let r = NextNoRec (r, Atoken tkn) in - Rules (r, fun _ -> f) - in - let r = mkrule (List.rev tkl) in - Arules [r] + let rec mkrule : 'a Tok.p list -> 'a rules = function + | [] -> + Rules (Stop, fun _ -> (* dropped anyway: *) "") + | tkn :: rem -> + let Rules (r, f) = mkrule rem in + let r = NextNoRec (r, Pcoq.G.Symbol.token tkn) in + Rules (r, fun _ -> f) + in + let r = mkrule (List.rev tkl) in + Pcoq.G.Symbol.rules ~warning:None [r] type ('s, 'a) mayrec_symbol = | MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol | MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> - if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200")) - else if is_self custom from p then MayRecMay Aself + if is_binder_level custom from p + then + (* Prevent self *) + MayRecNo (Pcoq.G.Symbol.nterml (target_entry custom forpat) "200") + else if is_self custom from p then MayRecMay Pcoq.G.Symbol.self else let g = target_entry custom forpat in let lev = adjust_level custom assoc from p in begin match lev with - | DefaultLevel -> MayRecNo (Aentry g) - | NextLevel -> MayRecMay Anext - | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev)) + | DefaultLevel -> MayRecNo (Pcoq.G.Symbol.nterm g) + | NextLevel -> MayRecMay Pcoq.G.Symbol.next + | NumLevel lev -> MayRecNo (Pcoq.G.Symbol.nterml g (string_of_int lev)) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat | TTConstrList (s, typ', [], forpat) -> begin match symbol_of_target s typ' assoc from forpat with - | MayRecNo s -> MayRecNo (Alist1 s) - | MayRecMay s -> MayRecMay (Alist1 s) end + | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1 s) + | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1 s) end | TTConstrList (s, typ', tkl, forpat) -> begin match symbol_of_target s typ' assoc from forpat with - | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl)) - | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end -| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p)) -| TTClosedBinderList [] -> MayRecNo (Alist1 (Aentry Constr.binder)) -| TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl)) -| TTName -> MayRecNo (Aentry Prim.name) -| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) -| TTBigint -> MayRecNo (Aentry Prim.bignat) -| TTReference -> MayRecNo (Aentry Constr.global) + | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) + | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) end +| TTPattern p -> MayRecNo (Pcoq.G.Symbol.nterml Constr.pattern (string_of_int p)) +| TTClosedBinderList [] -> MayRecNo (Pcoq.G.Symbol.list1 (Pcoq.G.Symbol.nterm Constr.binder)) +| TTClosedBinderList tkl -> MayRecNo (Pcoq.G.Symbol.list1sep (Pcoq.G.Symbol.nterm Constr.binder) (make_sep_rules tkl) false) +| TTName -> MayRecNo (Pcoq.G.Symbol.nterm Prim.name) +| TTOpenBinderList -> MayRecNo (Pcoq.G.Symbol.nterm Constr.open_binders) +| TTBigint -> MayRecNo (Pcoq.G.Symbol.nterm Prim.bignat) +| TTReference -> MayRecNo (Pcoq.G.Symbol.nterm Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName @@ -461,16 +466,16 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> ty_eval rem f { env with constrs; constrlists; } type ('s, 'a, 'r) mayrec_rule = -| MayRecRNo : ('s, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule -| MayRecRMay : ('s, Extend.mayrec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule +| MayRecRNo : ('s, norec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule +| MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function | TyStop -> MayRecRNo Stop | TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> begin match ty_erase rem with - | MayRecRNo rem -> MayRecRMay (Next (rem, Atoken tok)) - | MayRecRMay rem -> MayRecRMay (Next (rem, Atoken tok)) end + | MayRecRNo rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) + | MayRecRMay rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) end | TyNext (rem, TyNonTerm (_, _, s, _)) -> begin match ty_erase rem, s with | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s)) @@ -522,7 +527,13 @@ let rec pure_sublevels' assoc from forpat level = function let rem = pure_sublevels' assoc from forpat level rem in let push where p rem = match symbol_of_target where p assoc from forpat with - | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem + | MayRecNo sym -> + (match Pcoq.G.level_of_nonterm sym with + | None -> rem + | Some i -> + if different_levels (fst from,level) (where,i) then + (where,int_of_string i) :: rem + else rem) | _ -> rem in (match e with | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 793aad6b24..bcd8de1ff4 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -24,9 +24,9 @@ type 's grammar_prod_item = type 'a ty_arg = ('a -> raw_generic_argument) type ('self, 'tr, _, 'r) ty_rule = -| TyStop : ('self, Extend.norec, 'r, 'r) ty_rule -| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Extend.symbol * 'b ty_arg option -> - ('self, Extend.mayrec, 'b -> 'a, 'r) ty_rule +| TyStop : ('self, Pcoq.norec, 'r, 'r) ty_rule +| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.symbol * 'b ty_arg option -> + ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule @@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function | [] -> AnyTyRule TyStop | GramTerminal s :: rem -> let AnyTyRule rem = ty_rule_of_gram rem in - let tok = Atoken (CLexer.terminal s) in + let tok = Pcoq.G.Symbol.token (CLexer.terminal s) in let r = TyNext (rem, tok, None) in AnyTyRule r | GramNonTerminal (_, (t, tok)) :: rem -> @@ -44,9 +44,9 @@ let rec ty_rule_of_gram = function let r = TyNext (rem, tok, inj) in AnyTyRule r -let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Extend.rule = function -| TyStop -> Extend.Stop -| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok) +let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function +| TyStop -> Pcoq.Stop +| TyNext (rem, tok, _) -> Pcoq.Next (ty_erase rem, tok) type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r @@ -62,7 +62,7 @@ let make_rule f prod = let symb = ty_erase ty_rule in let f loc l = f loc (List.rev l) in let act = ty_eval ty_rule f in - Extend.Rule (symb, act) + Pcoq.Rule (symb, act) let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function | TUentry a -> ExtraArg a diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 7f6656b079..e6e4748b59 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -18,7 +18,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * - ('s, _, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item + ('s, _, 'a) Pcoq.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : extend_name -> vernac_expr Pcoq.Entry.t option -> @@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Extend.production_rule + 'a grammar_prod_item list -> 'a Pcoq.production_rule diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 08625b41a6..aebded72f8 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -51,12 +51,11 @@ module Vernac_ = let noedit_mode = gec_vernac "noedit_command" let () = - let open Extend in let act_vernac v loc = Some v in let act_eoi _ loc = None in let rule = [ - Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); - Rule (Next (Stop, Aentry vernac_control), act_vernac); + Rule (Next (Stop, Pcoq.G.Symbol.token Tok.PEOI), act_eoi); + Rule (Next (Stop, Pcoq.G.Symbol.nterm vernac_control), act_vernac); ] in Pcoq.grammar_extend main_entry (None, [None, None, rule]) diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 0e8202da9f..fc6ece27cd 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c | Some Refl -> untype_command ty (f v) args end -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Extend.norec, a) Extend.symbol = +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.symbol = let open Extend in function -| TUlist1 l -> Alist1 (untype_user_symbol l) -| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUlist0 l -> Alist0 (untype_user_symbol l) -| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUopt o -> Aopt (untype_user_symbol o) -| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) -| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) +| TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false +| TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false +| TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o) +| TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a)) +| TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i) let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function | TyNil -> [] @@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext = type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Extend.production_rule list +| Arg_rules of 'a Pcoq.production_rule list type 'a vernac_argument = { arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t; diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 90c00415d4..0acb5f43f9 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -111,7 +111,7 @@ type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t (** This is used because CAMLP5 parser can be dumb about rule factorization, which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Extend.production_rule list +| Arg_rules of 'a Pcoq.production_rule list (** There is a discrepancy here as we use directly extension rules and thus entries instead of ty_user_symbol and thus arguments as roots. *) -- 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. --- coqpp/coqpp_main.ml | 8 ++++---- parsing/pcoq.ml | 10 ++++++++++ parsing/pcoq.mli | 14 ++++---------- plugins/ltac/tacentries.ml | 20 +++++++++++++------- user-contrib/Ltac2/g_ltac2.mlg | 19 +++++++++++-------- user-contrib/Ltac2/tac2core.ml | 6 +++--- user-contrib/Ltac2/tac2entries.ml | 8 ++++---- vernac/egramcoq.ml | 29 +++++++++++------------------ vernac/egramml.ml | 6 +++--- vernac/pvernac.ml | 4 ++-- 10 files changed, 65 insertions(+), 59 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 5d1f0a876f..70e400c29b 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -217,13 +217,13 @@ let rec print_prod fmt p = and print_extrule fmt (tkn, vars, body) = let tkn = List.rev tkn in - fprintf fmt "@[Pcoq.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body) + fprintf fmt "@[Pcoq.G.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body) and print_symbols ~norec fmt = function -| [] -> fprintf fmt "Pcoq.Stop" +| [] -> fprintf fmt "Pcoq.G.Rule.stop" | tkn :: tkns -> - let c = if norec then "Pcoq.NextNoRec" else "Pcoq.Next" in - fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn + let c = if norec then "Pcoq.G.Rule.next_norec" else "Pcoq.G.Rule.next" in + fprintf fmt "%s @[(%a)@ (%a)@]" c (print_symbols ~norec) tkns print_symbol tkn and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 5601dcb474..8f7d6d1966 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -59,6 +59,7 @@ module G : sig val comment_state : Parsable.t -> ((int * int) * string) list val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option + val mk_rule : 'a Tok.p list -> string rules end with type 'a Entry.t = 'a Extend.entry = struct @@ -253,6 +254,15 @@ end with type 'a Entry.t = 'a Extend.entry = struct try Some (generalize_symbol s) with SelfSymbol -> None + let rec mk_rule tok = + match tok with + | [] -> + let stop_e = Stop in + Rules (stop_e, fun _ -> (* dropped anyway: *) "") + | tkn :: rem -> + let Rules (r, f) = mk_rule rem in + let r = Rule.next_norec r (Symbol.token tkn) in + Rules (r, fun _ -> f) end module Parsable = struct diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 63a4c1dd58..e7e3e9442b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -224,20 +224,13 @@ module Module : (** {5 Type-safe grammar extension} *) type ('self, 'trec, 'a) symbol +type ('self, 'trec, _, 'r) rule type norec = Gramlib.Grammar.norec type mayrec = Gramlib.Grammar.mayrec -type ('self, 'trec, _, 'r) rule = -| Stop : ('self, norec, 'r, 'r) rule -| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule -| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule - -type 'a rules = - | Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules - -type 'a production_rule = - | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule +type 'a rules +type 'a production_rule module G : sig @@ -245,6 +238,7 @@ module G : sig val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option + val mk_rule : 'a Tok.p list -> string rules end with type 'a Entry.t = 'a Entry.t and type te = Tok.t 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 *) diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 52d92d87c0..8b3203c8dd 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -827,10 +827,11 @@ END let () = let open Tok in -let (++) r s = Next (r, s) in +let (++) r s = Pcoq.G.Rule.next r s in let rules = [ - Rule ( - Stop ++ Pcoq.G.Symbol.nterm test_dollar_ident ++ Pcoq.G.Symbol.token (PKEYWORD "$") ++ Pcoq.G.Symbol.nterm Prim.ident, + Pcoq.G.( + Production.make + (Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.ident) begin fun id _ _ loc -> let id = Loc.tag ~loc id in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in @@ -838,8 +839,9 @@ let rules = [ end ); - Rule ( - Stop ++ Pcoq.G.Symbol.nterm test_ampersand_ident ++ Pcoq.G.Symbol.token (PKEYWORD "&") ++ Pcoq.G.Symbol.nterm Prim.ident, + Pcoq.G.( + Production.make + (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident) begin fun id _ _ loc -> let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in @@ -847,9 +849,10 @@ let rules = [ end ); - Rule ( - Stop ++ Pcoq.G.Symbol.token (PIDENT (Some "ltac2")) ++ Pcoq.G.Symbol.token (PKEYWORD ":") ++ - Pcoq.G.Symbol.token (PKEYWORD "(") ++ Pcoq.G.Symbol.nterm tac2expr ++ Pcoq.G.Symbol.token (PKEYWORD ")"), + Pcoq.G.( + Production.make + (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++ + Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")")) begin fun _ tac _ _ _ loc -> let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 2edbcc38f5..547ca0c2ed 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1594,7 +1594,7 @@ type seqrule = let rec make_seq_rule = function | [] -> - Seqrule (Stop, CvNil) + Seqrule (Pcoq.G.Rule.stop, CvNil) | tok :: rem -> let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in let scope = @@ -1604,7 +1604,7 @@ let rec make_seq_rule = function | Some scope -> scope in let Seqrule (r, c) = make_seq_rule rem in - let r = NextNoRec (r, scope) in + let r = Pcoq.G.Rule.next_norec r scope in let f = match tok with | SexprStr _ -> None (* Leave out mere strings *) | _ -> Some f @@ -1614,7 +1614,7 @@ let rec make_seq_rule = function let () = add_scope "seq" begin fun toks -> let scope = let Seqrule (r, c) = make_seq_rule (List.rev toks) in - Pcoq.G.Symbol.rules ~warning:None [Rules (r, apply c [])] + Pcoq.G.(Symbol.rules ~warning:None [Rules.make r (apply c [])]) in Tac2entries.ScopeRule (scope, (fun e -> e)) end diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index d5d5bad987..c5f081eab9 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -615,15 +615,15 @@ type krule = ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule let rec get_rule (tok : scope_rule token list) : krule = match tok with -| [] -> KRule (Pcoq.Stop, fun k loc -> k loc []) +| [] -> KRule (Pcoq.G.Rule.stop, fun k loc -> k loc []) | TacNonTerm (na, ScopeRule (scope, inj)) :: tok -> let KRule (rule, act) = get_rule tok in - let rule = Pcoq.Next (rule, scope) in + let rule = Pcoq.G.Rule.next rule scope in let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in KRule (rule, act) | TacTerm t :: tok -> let KRule (rule, act) = get_rule tok in - let rule = Pcoq.Next (rule, Pcoq.G.Symbol.token (CLexer.terminal t)) in + let rule = Pcoq.G.(Rule.next rule (Symbol.token (CLexer.terminal t))) in let act k _ = act k in KRule (rule, act) @@ -637,7 +637,7 @@ let perform_notation syn st = let bnd = List.map map args in CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp) in - let rule = Pcoq.Rule (rule, act mk) in + let rule = Pcoq.G.Production.make rule (act mk) in let lev = match syn.synext_lev with | None -> None | Some lev -> Some (string_of_int lev) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index ba542101c8..43029f4d53 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -328,15 +328,7 @@ let make_sep_rules = function | [tk] -> Pcoq.G.Symbol.token tk | tkl -> - let rec mkrule : 'a Tok.p list -> 'a rules = function - | [] -> - Rules (Stop, fun _ -> (* dropped anyway: *) "") - | tkn :: rem -> - let Rules (r, f) = mkrule rem in - let r = NextNoRec (r, Pcoq.G.Symbol.token tkn) in - Rules (r, fun _ -> f) - in - let r = mkrule (List.rev tkl) in + let r = Pcoq.G.mk_rule (List.rev tkl) in Pcoq.G.Symbol.rules ~warning:None [r] type ('s, 'a) mayrec_symbol = @@ -470,18 +462,18 @@ type ('s, 'a, 'r) mayrec_rule = | MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function -| TyStop -> MayRecRNo Stop +| TyStop -> MayRecRNo G.Rule.stop | TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> begin match ty_erase rem with - | MayRecRNo rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) - | MayRecRMay rem -> MayRecRMay (Next (rem, Pcoq.G.Symbol.token tok)) end + | MayRecRNo rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) + | MayRecRMay rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) end | TyNext (rem, TyNonTerm (_, _, s, _)) -> begin match ty_erase rem, s with - | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s)) - | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s)) - | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s)) - | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end + | MayRecRNo rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s) + | MayRecRNo rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) + | MayRecRMay rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s) + | MayRecRMay rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) end type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule @@ -564,8 +556,9 @@ let extend_constr state forpat ng = let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = let r = match ty_erase r with - | MayRecRNo symbs -> Rule (symbs, act) - | MayRecRMay symbs -> Rule (symbs, act) in + | MayRecRNo symbs -> Pcoq.G.Production.make symbs act + | MayRecRMay symbs -> Pcoq.G.Production.make symbs act + in name, p4assoc, [r] in let r = match reinit with | None -> diff --git a/vernac/egramml.ml b/vernac/egramml.ml index bcd8de1ff4..175217803f 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -45,8 +45,8 @@ let rec ty_rule_of_gram = function AnyTyRule r let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function -| TyStop -> Pcoq.Stop -| TyNext (rem, tok, _) -> Pcoq.Next (ty_erase rem, tok) +| TyStop -> Pcoq.G.Rule.stop +| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r @@ -62,7 +62,7 @@ let make_rule f prod = let symb = ty_erase ty_rule in let f loc l = f loc (List.rev l) in let act = ty_eval ty_rule f in - Pcoq.Rule (symb, act) + Pcoq.G.Production.make symb act let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function | TUentry a -> ExtraArg a diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index aebded72f8..27b8a5bda2 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -54,8 +54,8 @@ module Vernac_ = let act_vernac v loc = Some v in let act_eoi _ loc = None in let rule = [ - Rule (Next (Stop, Pcoq.G.Symbol.token Tok.PEOI), act_eoi); - Rule (Next (Stop, Pcoq.G.Symbol.nterm vernac_control), act_vernac); + Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi); + Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac); ] in Pcoq.grammar_extend main_entry (None, [None, None, rule]) -- 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. --- coqpp/coqpp_main.ml | 2 +- gramlib/grammar.ml | 102 ++++++++++++-- gramlib/grammar.mli | 21 ++- parsing/pcoq.ml | 264 ++++++------------------------------- parsing/pcoq.mli | 40 ++---- plugins/ltac/tacentries.ml | 8 +- user-contrib/Ltac2/g_ltac2.mlg | 2 +- user-contrib/Ltac2/tac2core.ml | 2 +- user-contrib/Ltac2/tac2entries.ml | 6 +- user-contrib/Ltac2/tac2entries.mli | 2 +- vernac/egramcoq.ml | 14 +- vernac/egramml.ml | 8 +- vernac/egramml.mli | 4 +- vernac/pvernac.ml | 2 +- vernac/vernacextend.ml | 6 +- vernac/vernacextend.mli | 2 +- 16 files changed, 182 insertions(+), 303 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 70e400c29b..17f81c555c 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -266,7 +266,7 @@ let print_rule fmt r = let print_entry fmt e = let print_position_opt fmt pos = print_opt fmt print_position pos in let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ " + fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.G.pos=%a; data=%a}@]@]@ in@ " e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules let print_ast fmt ext = diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 818608674e..0eed42f290 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -80,12 +80,21 @@ module type S = sig module Unsafe : sig val clear_entry : 'a Entry.t -> unit end - val safe_extend : warning:(string -> unit) option -> - 'a Entry.t -> Gramext.position option -> - (string option * Gramext.g_assoc option * 'a Production.t list) - list -> - unit - val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit + + type 'a single_extend_statement = + string option * Gramext.g_assoc option * 'a Production.t list + + type 'a extend_statement = + { pos : Gramext.position option + ; data : 'a single_extend_statement list + } + + val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit + val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit + + val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option + + val mk_rule : 'a pattern list -> string Rules.t (* Used in custom entries, should tweak? *) val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option @@ -1659,13 +1668,18 @@ module Unsafe = struct end -let safe_extend ~warning (e : 'a Entry.t) pos - (r : - (string option * Gramext.g_assoc option * 'a ty_production list) - list) = - extend_entry ~warning e pos r +type 'a single_extend_statement = + string option * Gramext.g_assoc option * 'a ty_production list + +type 'a extend_statement = + { pos : Gramext.position option + ; data : 'a single_extend_statement list + } + +let safe_extend ~warning (e : 'a Entry.t) { pos; data } = + extend_entry ~warning e pos data -let safe_delete_rule e r = +let safe_delete_rule e (TProd (r,_act)) = let AnyS (symbols, _) = get_symbols r in delete_rule e symbols @@ -1673,4 +1687,68 @@ let level_of_nonterm sym = match sym with | Snterml (_,l) -> Some l | _ -> None +exception SelfSymbol + +let rec generalize_symbol : + type a tr s. (s, tr, a) Symbol.t -> (s, norec, a) ty_symbol = + function + | Stoken tok -> + Stoken tok + | Slist1 e -> + Slist1 (generalize_symbol e) + | Slist1sep (e, sep, b) -> + let e = generalize_symbol e in + let sep = generalize_symbol sep in + Slist1sep (e, sep, b) + | Slist0 e -> + Slist0 (generalize_symbol e) + | Slist0sep (e, sep, b) -> + let e = generalize_symbol e in + let sep = generalize_symbol sep in + Slist0sep (e, sep, b) + | Sopt e -> + Sopt (generalize_symbol e) + | Sself -> + raise SelfSymbol + | Snext -> + raise SelfSymbol + | Snterm e -> + Snterm e + | Snterml (e, l) -> + Snterml (e, l) + | Stree r -> + Stree (generalize_tree r) +and generalize_tree : type a tr s . + (s, tr, a) ty_tree -> (s, norec, a) ty_tree = fun r -> + match r with + | Node (fi, n) -> + let fi = match fi with + | NoRec3 -> NoRec3 + | MayRec3 -> raise SelfSymbol + in + let n = match n with + | { node; son; brother } -> + let node = generalize_symbol node in + let son = generalize_tree son in + let brother = generalize_tree brother in + { node; son; brother } + in + Node (fi, n) + | LocAct _ as r -> r + | DeadEnd as r -> r + +let generalize_symbol s = + try Some (generalize_symbol s) + with SelfSymbol -> None + +let rec mk_rule tok = + match tok with + | [] -> + let stop_e = Rule.stop in + TRules (stop_e, fun _ -> (* dropped anyway: *) "") + | tkn :: rem -> + let TRules (r, f) = mk_rule rem in + let r = Rule.next_norec r (Symbol.token tkn) in + TRules (r, fun _ -> f) + end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 4ac85bd358..4280181109 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -90,16 +90,23 @@ module type S = sig val clear_entry : 'a Entry.t -> unit end - val safe_extend : warning:(string -> unit) option -> - 'a Entry.t -> Gramext.position option -> - (string option * Gramext.g_assoc option * 'a Production.t list) - list -> - unit - val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit + type 'a single_extend_statement = + string option * Gramext.g_assoc option * 'a Production.t list + + type 'a extend_statement = + { pos : Gramext.position option + ; data : 'a single_extend_statement list + } + + val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit + val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit + + val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option + + val mk_rule : 'a pattern list -> string Rules.t (* Used in custom entries, should tweak? *) val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option - end (** Signature type of the functor [Grammar.GMake]. The types and functions are almost the same than in generic interface, but: diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8f7d6d1966..e10e4bb8dd 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -10,7 +10,6 @@ open CErrors open Util -open Extend open Genarg open Gramlib @@ -19,47 +18,16 @@ open Gramlib type norec = Gramlib.Grammar.norec type mayrec = Gramlib.Grammar.mayrec -type ('self, 'trec, 'a) symbol = -| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol -| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol -| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol - -> ('self, 'trec, 'a list) symbol -| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol -| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol - -> ('self, 'trec, 'a list) symbol -| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol -| Aself : ('self, mayrec, 'self) symbol -| Anext : ('self, mayrec, 'self) symbol -| Aentry : 'a entry -> ('self, norec, 'a) symbol -| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol -| Arules : 'a rules list -> ('self, norec, 'a) symbol - -and ('self, 'trec, _, 'r) rule = -| Stop : ('self, norec, 'r, 'r) rule -| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule -| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule - -and 'a rules = -| Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules - -type 'a production_rule = -| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - module G : sig include Grammar.S with type te = Tok.t and type 'c pattern = 'c Tok.p - and type 'a pattern = 'a Tok.p - and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol - and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule - and type 'a Rules.t = 'a rules - and type 'a Production.t = 'a production_rule val comment_state : Parsable.t -> ((int * int) * string) list val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option - val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option - val mk_rule : 'a Tok.p list -> string rules + val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option + val mk_rule : 'a Tok.p list -> string Rules.t end with type 'a Entry.t = 'a Extend.entry = struct @@ -88,6 +56,12 @@ end with type 'a Entry.t = 'a Extend.entry = struct let tokens = G_.tokens + type 'a single_extend_statement = 'a G_.single_extend_statement + type 'a extend_statement = 'a G_.extend_statement = + { pos : Gramlib.Gramext.position option + ; data : 'a single_extend_statement list + } + module Entry = struct include G_.Entry @@ -105,164 +79,17 @@ end with type 'a Entry.t = 'a Extend.entry = struct end - module Symbol = struct - type ('self, 'trec, 'a) t = ('self, 'trec, 'a) symbol - let token tok = Atoken tok - let list0 e = Alist0 e - let list0sep e s _ = Alist0sep (e,s) - let list1 e = Alist1 e - let list1sep e s _ = Alist1sep (e,s) - let opt e = Aopt e - let self = Aself - let next = Anext - let nterm e = Aentry e - let nterml e s = Aentryl (e,s) - let rules ~warning:_ r = Arules r - end - - module Rule = struct - type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) rule - let stop = Stop - let next a b = Next (a,b) - let next_norec a b = NextNoRec (a,b) - end - - module Rules = struct - type 'a t = 'a rules - let make a f = Rules(a,f) - end - - module Production = struct - type 'a t = 'a production_rule - let make a f = Rule(a,f) - end - - module Unsafe = struct - let clear_entry = G_.Unsafe.clear_entry - end - - (** FIXME: This is a hack around a deficient camlp5 API *) - type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G_.Rule.t * 'f -> 'a any_production - - let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G_.Symbol.t = - function - | Atoken t -> G_.Symbol.token t - | Alist1 s -> - let s = symbol_of_prod_entry_key s in - G_.Symbol.list1 s - | Alist1sep (s,sep) -> - let s = symbol_of_prod_entry_key s in - let sep = symbol_of_prod_entry_key sep in - G_.Symbol.list1sep s sep false - | Alist0 s -> - let s = symbol_of_prod_entry_key s in - G_.Symbol.list0 s - | Alist0sep (s,sep) -> - let s = symbol_of_prod_entry_key s in - let sep = symbol_of_prod_entry_key sep in - G_.Symbol.list0sep s sep false - | Aopt s -> - let s = symbol_of_prod_entry_key s in - G_.Symbol.opt s - | Aself -> G_.Symbol.self - | Anext -> G_.Symbol.next - | Aentry e -> G_.Symbol.nterm e - | Aentryl (e, n) -> G_.Symbol.nterml e n - | Arules rs -> - let warning msg = Feedback.msg_warning Pp.(str msg) in - G_.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs) - - and symbol_of_rule : type s tr a r. (s, tr, a, r) rule -> (s, tr, a, r) G_.Rule.t = function - | Stop -> - G_.Rule.stop - | Next (r, s) -> - let r = symbol_of_rule r in - let s = symbol_of_prod_entry_key s in - G_.Rule.next r s - | NextNoRec (r, s) -> - let r = symbol_of_rule r in - let s = symbol_of_prod_entry_key s in - G_.Rule.next_norec r s - - and symbol_of_rules : type a. a rules -> a G_.Rules.t = function - | Rules (r, act) -> - let symb = symbol_of_rule r in - G_.Rules.make symb act - - let of_coq_production_rule : type a. a production_rule -> a any_production = function - | Rule (toks, act) -> - AnyProduction (symbol_of_rule toks, act) - - let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, assoc, List.map of_coq_production_rule rule) - - let of_coq_extend_statement (pos, st) = - (pos, List.map of_coq_single_extend_statement st) - - let fix_extend_statement (pos, st) = - let fix_single_extend_statement (lvl, assoc, rules) = - let fix_production_rule (AnyProduction (s, act)) = G_.Production.make s act in - (lvl, assoc, List.map fix_production_rule rules) - in - (pos, List.map fix_single_extend_statement st) - - let safe_extend ~warning e pos ext = - let pos, ext = of_coq_extend_statement (pos,ext) in - let pos, ext = fix_extend_statement (pos, ext) in - G_.safe_extend ~warning e pos ext - - let safe_delete_rule e r = - let r = symbol_of_rule r in - G_.safe_delete_rule e r - - let level_of_nonterm = function - | Aentryl (_,l) -> Some l - | _ -> None - - exception SelfSymbol - let rec generalize_symbol : - type a tr s. (s, tr, a) symbol -> (s, norec, a) symbol = - function - | Atoken tok -> - Atoken tok - | Alist1 e -> - Alist1 (generalize_symbol e) - | Alist1sep (e, sep) -> - let e = generalize_symbol e in - let sep = generalize_symbol sep in - Alist1sep (e, sep) - | Alist0 e -> - Alist0 (generalize_symbol e) - | Alist0sep (e, sep) -> - let e = generalize_symbol e in - let sep = generalize_symbol sep in - Alist0sep (e, sep) - | Aopt e -> - Aopt (generalize_symbol e) - | Aself -> - raise SelfSymbol - | Anext -> - raise SelfSymbol - | Aentry e -> - Aentry e - | Aentryl (e, l) -> - Aentryl (e, l) - | Arules r -> - Arules r - - let generalize_symbol s = - try Some (generalize_symbol s) - with SelfSymbol -> None - - let rec mk_rule tok = - match tok with - | [] -> - let stop_e = Stop in - Rules (stop_e, fun _ -> (* dropped anyway: *) "") - | tkn :: rem -> - let Rules (r, f) = mk_rule rem in - let r = Rule.next_norec r (Symbol.token tkn) in - Rules (r, fun _ -> f) + module Symbol = G_.Symbol + module Rule = G_.Rule + module Rules = G_.Rules + module Production = G_.Production + module Unsafe = G_.Unsafe + + let safe_extend = G_.safe_extend + let safe_delete_rule = G_.safe_delete_rule + let level_of_nonterm = G_.level_of_nonterm + let generalize_symbol = G_.generalize_symbol + let mk_rule = G_.mk_rule end module Parsable = struct @@ -349,21 +176,9 @@ end (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position -type 'a single_extend_statement = - string option * - (* Level *) - Gramlib.Gramext.g_assoc option * - (* Associativity *) - 'a production_rule list - (* Symbol list with the interpretation function *) - -type 'a extend_statement = - Gramlib.Gramext.position option * - 'a single_extend_statement list - type extend_rule = -| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule -| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule +| ExtendRule : 'a G.Entry.t * 'a G.extend_statement -> extend_rule +| ExtendRuleReinit : 'a G.Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule module EntryCommand = Dyn.Make () module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end @@ -382,39 +197,38 @@ let camlp5_entries = ref EntryDataMap.empty (** Deletion *) -let grammar_delete e (pos,rls) = +let grammar_delete e { G.pos; data } = List.iter (fun (n,ass,lev) -> - List.iter (fun (Rule(pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) - (List.rev rls) + List.iter (fun pil -> G.safe_delete_rule e pil) (List.rev lev)) + (List.rev data) -let grammar_delete_reinit e reinit (pos, rls) = - grammar_delete e (pos, rls); +let grammar_delete_reinit e reinit ({ G.pos; data } as d)= + grammar_delete e d; let a, ext = reinit in let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false in let warning msg = Feedback.msg_warning Pp.(str msg) in - (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] + let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in + G.safe_extend ~warning:(Some warning) e ext (** Extension *) -let grammar_extend e (pos,ext) = - let undo () = grammar_delete e (pos,ext) in - let redo () = G.safe_extend ~warning:None e pos ext in +let grammar_extend e ext = + let undo () = grammar_delete e ext in + let redo () = G.safe_extend ~warning:None e ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e ext = camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; - let pos, ext = ext in - G.safe_extend ~warning:None e pos ext + G.safe_extend ~warning:None e ext let grammar_extend_sync_reinit e reinit ext = camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; - let pos, ext = ext in - G.safe_extend ~warning:None e pos ext + G.safe_extend ~warning:None e ext (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -467,7 +281,8 @@ let eoi_entry en = let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in let act = fun _ x loc -> x in let warning msg = Feedback.msg_warning Pp.(str msg) in - Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]); + let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in + Gram.safe_extend ~warning:(Some warning) e ext; e let map_entry f en = @@ -475,7 +290,8 @@ let map_entry f en = let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in let act = fun x loc -> f x in let warning msg = Feedback.msg_warning Pp.(str msg) in - Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]); + let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in + Gram.safe_extend ~warning:(Some warning) e ext; e (* Parse a string, does NOT check if the entire string was read @@ -620,12 +436,12 @@ module Module = let module_type = Entry.create "module_type" end -let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = +let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) = let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in - let ext = [None, None, [r]] in let entry = G.Entry.make "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in - let () = G.safe_extend ~warning:(Some warning) entry None ext in + let ext = { G.pos = None; data = [None, None, [r]] } in + let () = G.safe_extend ~warning:(Some warning) entry ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e7e3e9442b..f83109d39a 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -223,51 +223,26 @@ module Module : (** {5 Type-safe grammar extension} *) -type ('self, 'trec, 'a) symbol -type ('self, 'trec, _, 'r) rule - type norec = Gramlib.Grammar.norec type mayrec = Gramlib.Grammar.mayrec -type 'a rules -type 'a production_rule - module G : sig include Gramlib.Grammar.S val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option - val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option - val mk_rule : 'a Tok.p list -> string rules + val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option + val mk_rule : 'a Tok.p list -> string Rules.t end with type 'a Entry.t = 'a Entry.t and type te = Tok.t and type 'a pattern = 'a Tok.p - and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol - and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule - and type 'a Rules.t = 'a rules - and type 'a Production.t = 'a production_rule -val epsilon_value : ('a -> 'self) -> ('self, _, 'a) symbol -> 'self option +val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option (** {5 Extending the parser without synchronization} *) -type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position -(** Type of reinitialization data *) - -type 'a single_extend_statement = - string option * - (* Level *) - Gramlib.Gramext.g_assoc option * - (* Associativity *) - 'a production_rule list - (* Symbol list with the interpretation function *) - -type 'a extend_statement = - Gramlib.Gramext.position option * - 'a single_extend_statement list - -val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit +val grammar_extend : 'a Entry.t -> 'a G.extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -283,9 +258,12 @@ type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position +(** Type of reinitialization data *) + type extend_rule = -| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule -| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a G.extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, 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 diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 8b3203c8dd..477672ebdb 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -861,7 +861,7 @@ let rules = [ ] in Hook.set Tac2entries.register_constr_quotations begin fun () -> - Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)]) + Pcoq.grammar_extend Pcoq.Constr.operconstr {G.pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]} end } diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 547ca0c2ed..0946c88228 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1590,7 +1590,7 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu) type seqrule = -| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule +| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule let rec make_seq_rule = function | [] -> diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index c5f081eab9..7c4971db8c 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -558,7 +558,7 @@ type 'a token = | TacNonTerm of Name.t * 'a type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule @@ -611,7 +611,7 @@ type synext = { type krule = | KRule : - (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.rule * + (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.G.Rule.t * ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule let rec get_rule (tok : scope_rule token list) : krule = match tok with @@ -643,7 +643,7 @@ let perform_notation syn st = | Some lev -> Some (string_of_int lev) in let rule = (lev, None, [rule]) in - ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st) + ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.G.pos=None; data=[rule]})], st) let ltac2_notation = Pcoq.create_grammar_command "ltac2-notation" perform_notation diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index 4938e96cae..1efac697aa 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit (** {5 Notations} *) type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 43029f4d53..88bcf1d477 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -332,8 +332,8 @@ let make_sep_rules = function Pcoq.G.Symbol.rules ~warning:None [r] type ('s, 'a) mayrec_symbol = -| MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol -| MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol +| MayRecNo : ('s, norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol +| MayRecMay : ('s, mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> if is_binder_level custom from p @@ -458,8 +458,8 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> ty_eval rem f { env with constrs; constrlists; } type ('s, 'a, 'r) mayrec_rule = -| MayRecRNo : ('s, norec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule -| MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule +| MayRecRNo : ('s, norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule +| MayRecRMay : ('s, mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function | TyStop -> MayRecRNo G.Rule.stop @@ -501,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function | ForPattern -> true let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = - let empty = (pos, [(name, p4assoc, [])]) in + let empty = { G.pos; data = [(name, p4assoc, [])] } in match reinit with | None -> ExtendRule (target_entry where forpat, empty) @@ -562,9 +562,9 @@ let extend_constr state forpat ng = name, p4assoc, [r] in let r = match reinit with | None -> - ExtendRule (entry, (pos, [rule])) + ExtendRule (entry, { G.pos; data = [rule]}) | Some reinit -> - ExtendRuleReinit (entry, reinit, (pos, [rule])) + ExtendRuleReinit (entry, reinit, { G.pos; data = [rule]}) in (accu @ empty_rules @ [r], state) in diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 175217803f..00a239f56e 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -19,13 +19,13 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - ('a raw_abstract_argument_type * ('s, _, 'a) symbol) Loc.located -> 's grammar_prod_item + ('a raw_abstract_argument_type * ('s, _, 'a) G.Symbol.t) Loc.located -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) type ('self, 'tr, _, 'r) ty_rule = | TyStop : ('self, Pcoq.norec, 'r, 'r) ty_rule -| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.symbol * 'b ty_arg option -> +| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.G.Symbol.t * 'b ty_arg option -> ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule type ('self, 'r) any_ty_rule = @@ -44,7 +44,7 @@ let rec ty_rule_of_gram = function let r = TyNext (rem, tok, inj) in AnyTyRule r -let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function +let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.G.Rule.t = function | TyStop -> Pcoq.G.Rule.stop | TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok @@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl = vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in - grammar_extend nt (None, [None, None, rules]) + grammar_extend nt { G.pos=None; data=[None, None, rules]} diff --git a/vernac/egramml.mli b/vernac/egramml.mli index e6e4748b59..77198452b9 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -18,7 +18,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * - ('s, _, 'a) Pcoq.symbol) Loc.located -> 's grammar_prod_item + ('s, _, 'a) Pcoq.G.Symbol.t) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : extend_name -> vernac_expr Pcoq.Entry.t option -> @@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Pcoq.production_rule + 'a grammar_prod_item list -> 'a Pcoq.G.Production.t diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 27b8a5bda2..9a9c96064d 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -57,7 +57,7 @@ module Vernac_ = Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi); Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac); ] in - Pcoq.grammar_extend main_entry (None, [None, None, rule]) + Pcoq.(grammar_extend main_entry {G.pos=None; data=[None, None, rule]}) let select_tactic_entry spec = match spec with diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index fc6ece27cd..ac4d33c926 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -166,7 +166,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c | Some Refl -> untype_command ty (f v) args end -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.symbol = +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.G.Symbol.t = let open Extend in function | TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l) | TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false @@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext = type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Pcoq.production_rule list +| Arg_rules of 'a Pcoq.G.Production.t list type 'a vernac_argument = { arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t; @@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg = e | 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 {Pcoq.G.pos=None; data=[(None, None, rules)]} in e in let pr = arg.arg_printer in diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 0acb5f43f9..4d9537b6ff 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -111,7 +111,7 @@ type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t (** This is used because CAMLP5 parser can be dumb about rule factorization, which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Pcoq.production_rule list +| Arg_rules of 'a Pcoq.G.Production.t list (** There is a discrepancy here as we use directly extension rules and thus entries instead of ty_user_symbol and thus arguments as roots. *) -- cgit v1.2.3 From f9174f64c56375adb42e53b97df9eeb8b0a9680d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 20 Feb 2020 22:51:46 -0500 Subject: [parsing] Remove unneeded `Extend.entry` type. This is not needed anymore after the unification. --- parsing/extend.ml | 2 -- parsing/pcoq.ml | 2 +- parsing/pcoq.mli | 2 +- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/parsing/extend.ml b/parsing/extend.ml index 9c7f5c87c4..fadfb6c5f4 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -10,8 +10,6 @@ (** Entry keys for constr notations *) -type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.t - type side = Left | Right type production_position = diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index e10e4bb8dd..7d301e75bd 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -29,7 +29,7 @@ module G : sig val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option val mk_rule : 'a Tok.p list -> string Rules.t -end with type 'a Entry.t = 'a Extend.entry = struct +end = struct module G_ = Grammar.GMake(CLexer.Lexer) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f83109d39a..e12a1cc11b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -24,7 +24,7 @@ sig end module Entry : sig - type 'a t = 'a Extend.entry + type 'a t val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit -- 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. --- ide/idetop.ml | 6 ++--- parsing/pcoq.ml | 41 +++++++++-------------------------- parsing/pcoq.mli | 35 +++++++----------------------- plugins/ltac/g_tactic.mlg | 2 +- plugins/ssr/ssrparser.mlg | 22 +++++++++---------- plugins/ssrmatching/g_ssrmatching.mlg | 2 +- stm/stm.mli | 4 ++-- toplevel/coqloop.ml | 10 ++++----- toplevel/coqloop.mli | 2 +- toplevel/vernac.ml | 4 ++-- user-contrib/Ltac2/tac2core.ml | 2 +- vernac/egramcoq.ml | 8 +++---- vernac/egramml.ml | 6 ++--- vernac/metasyntax.ml | 4 ++-- vernac/proof_using.ml | 2 +- vernac/pvernac.ml | 4 ++-- vernac/vernacextend.ml | 18 +++++++-------- vernac/vernacinterp.ml | 4 ++-- vernac/vernacstate.ml | 2 +- vernac/vernacstate.mli | 2 +- 20 files changed, 70 insertions(+), 110 deletions(-) diff --git a/ide/idetop.ml b/ide/idetop.ml index 0ef7fca41f..81e7e4d148 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -91,7 +91,7 @@ let set_doc doc = ide_doc := Some doc let add ((s,eid),(sid,verbose)) = let doc = get_doc () in - let pa = Pcoq.Parsable.make (Stream.of_string s) in + let pa = Pcoq.G.Parsable.make (Stream.of_string s) in match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with | None -> assert false (* s is not an empty string *) | Some ast -> @@ -127,13 +127,13 @@ let edit_at id = * be removed in the next version of the protocol. *) let query (route, (s,id)) = - let pa = Pcoq.Parsable.make (Stream.of_string s) in + let pa = Pcoq.G.Parsable.make (Stream.of_string s) in let doc = get_doc () in Stm.query ~at:id ~doc ~route pa let annotate phrase = let doc = get_doc () in - let pa = Pcoq.Parsable.make (Stream.of_string phrase) in + let pa = Pcoq.G.Parsable.make (Stream.of_string phrase) in match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with | None -> Richpp.richpp_of_pp 78 (Pp.mt ()) | Some ast -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7d301e75bd..8f3c1e029c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -15,9 +15,6 @@ open Gramlib (** The parser of Coq *) -type norec = Gramlib.Grammar.norec -type mayrec = Gramlib.Grammar.mayrec - module G : sig include Grammar.S @@ -25,9 +22,6 @@ module G : sig and type 'c pattern = 'c Tok.p val comment_state : Parsable.t -> ((int * int) * string) list - val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option - val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option - val mk_rule : 'a Tok.p list -> string Rules.t end = struct @@ -92,11 +86,6 @@ end = struct let mk_rule = G_.mk_rule end -module Parsable = struct - include G.Parsable - let comment_state = G.comment_state -end - module Entry = struct include G.Entry let create = make @@ -121,7 +110,7 @@ struct let to_entry s (lk : t) = let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in - Entry.of_parser s run + G.Entry.of_parser s run let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with | None -> None @@ -171,8 +160,6 @@ end In [single_extend_statement], first two parameters are name and assoc iff a level is created *) -(** Binding general entry keys to symbol *) - (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position @@ -230,14 +217,6 @@ let grammar_extend_sync_reinit e reinit ext = camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; G.safe_extend ~warning:None e ext -(** The apparent parser of Coq; encapsulate G to keep track - of the extensions. *) - -module Gram = - struct - include G - end - (** Remove extensions [n] is the number of extended entries (not the number of Grammar commands!) @@ -277,21 +256,21 @@ let make_rule r = [None, None, r] (** An entry that checks we reached the end of the input. *) let eoi_entry en = - let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in + let e = G.Entry.make ((G.Entry.name en) ^ "_eoi") in let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in let act = fun _ x loc -> x in let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - Gram.safe_extend ~warning:(Some warning) e ext; + G.safe_extend ~warning:(Some warning) e ext; e let map_entry f en = - let e = Entry.create ((Gram.Entry.name en) ^ "_map") in + let e = G.Entry.make ((G.Entry.name en) ^ "_map") in let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in let act = fun x loc -> f x in let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - Gram.safe_extend ~warning:(Some warning) e ext; + G.safe_extend ~warning:(Some warning) e ext; e (* Parse a string, does NOT check if the entire string was read @@ -320,14 +299,14 @@ let get_univ u = let new_entry u s = let ename = u ^ ":" ^ s in - let e = Entry.create ename in + let e = G.Entry.make ename in e let make_gen_entry u s = new_entry u s module GrammarObj = struct - type ('r, _, _) obj = 'r Entry.t + type ('r, _, _) obj = 'r G.Entry.t let name = "grammar" let default _ = None end @@ -350,7 +329,7 @@ let genarg_grammar x = check_compatibility x; Grammar.obj x -let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t = +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a G.Entry.t = let e = new_entry u s in let Rawwit t = etyp in let () = Grammar.register0 t e in @@ -499,7 +478,7 @@ let extend_grammar_command tag g = let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.t list = +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b G.Entry.t list = let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty @@ -532,7 +511,7 @@ let extend_dyn_grammar (e, _) = match e with (** Registering extra grammar *) -type any_entry = AnyEntry : 'a Gram.Entry.t -> any_entry +type any_entry = AnyEntry : 'a G.Entry.t -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e12a1cc11b..0352c1d55b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -15,22 +15,18 @@ open Libnames (** The parser of Coq *) -module Parsable : -sig - type t - val make : ?loc:Loc.t -> char Stream.t -> t - (* Get comment parsing information from the Lexer *) - val comment_state : t -> ((int * int) * string) list -end +module G : sig + + include Gramlib.Grammar.S + + val comment_state : Parsable.t -> ((int * int) * string) list + +end with type te = Tok.t and type 'a pattern = 'a Tok.p module Entry : sig - type 'a t + type 'a t = 'a G.Entry.t val create : string -> 'a t - val parse : 'a t -> Parsable.t -> 'a - val print : Format.formatter -> 'a t -> unit val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t - val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a - val name : 'a t -> string end module Lookahead : sig @@ -223,21 +219,6 @@ module Module : (** {5 Type-safe grammar extension} *) -type norec = Gramlib.Grammar.norec -type mayrec = Gramlib.Grammar.mayrec - -module G : sig - - include Gramlib.Grammar.S - - val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option - val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option - val mk_rule : 'a Tok.p list -> string Rules.t - -end with type 'a Entry.t = 'a Entry.t - and type te = Tok.t - and type 'a pattern = 'a Tok.p - val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option (** {5 Extending the parser without synchronization} *) 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 diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 442b40221b..c3396584a4 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -263,16 +263,16 @@ let negate_parser f tok x = | Some _ -> raise Stream.Failure let test_not_ssrslashnum = - Pcoq.Entry.of_parser + Pcoq.G.Entry.of_parser "test_not_ssrslashnum" (negate_parser test_ssrslashnum10) let test_ssrslashnum00 = - Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 + Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 let test_ssrslashnum10 = - Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 + Pcoq.G.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 let test_ssrslashnum11 = - Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 + Pcoq.G.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 let test_ssrslashnum01 = - Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 + Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 } @@ -459,7 +459,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "@" -> xWithAt | _ -> xNoFlag -let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind (* New kinds of terms *) @@ -470,7 +470,7 @@ let input_term_annotation _ strm = | Tok.KEYWORD "@" :: _ -> `At | _ -> `None let term_annotation = - Pcoq.Entry.of_parser "term_annotation" input_term_annotation + Pcoq.G.Entry.of_parser "term_annotation" input_term_annotation (* terms *) @@ -811,7 +811,7 @@ let reject_ssrhid _ strm = | _ -> ()) | _ -> () -let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid +let test_nohidden = Pcoq.G.Entry.of_parser "test_ssrhid" reject_ssrhid let rec reject_binder crossed_paren k tok s = match @@ -825,7 +825,7 @@ let rec reject_binder crossed_paren k tok s = | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure | _ -> if crossed_paren then () else raise Stream.Failure -let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0) +let _test_nobinder = Pcoq.G.Entry.of_parser "test_nobinder" (reject_binder false 0) } @@ -1659,7 +1659,7 @@ let ssr_id_of_string loc s = ^ "Scripts with explicit references to anonymous variables are fragile.")) end; Id.of_string s -let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ()) +let ssr_null_entry = Pcoq.G.Entry.of_parser "ssr_null" (fun _ _ -> ()) } @@ -2382,7 +2382,7 @@ let test_ssr_rw_syntax = match Util.stream_nth 0 strm with | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> () | _ -> raise Stream.Failure in - Pcoq.Entry.of_parser "test_ssr_rw_syntax" test + Pcoq.G.Entry.of_parser "test_ssr_rw_syntax" test } diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 33e523a4a4..59abf80dc5 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -70,7 +70,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind } diff --git a/stm/stm.mli b/stm/stm.mli index 2c27d63b82..88da3c747f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -93,7 +93,7 @@ val new_doc : stm_init_options -> doc * Stateid.t be the case if an error was raised at parsing time). *) val parse_sentence : doc:doc -> Stateid.t -> - entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.G.Parsable.t -> 'a (* Reminder: A parsable [pa] is constructed using [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) @@ -119,7 +119,7 @@ val get_proof : doc:doc -> Stateid.t -> Proof.t option throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : doc:doc -> - at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.G.Parsable.t -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index b8acdd3af1..0d9edb248b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Pcoq.Parsable.t; (* stream of tokens *) + mutable tokens : Pcoq.G.Parsable.t; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); + ibuf.tokens <- Pcoq.G.Parsable.make (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -230,7 +230,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Pcoq.Parsable.make (Stream.of_list []); + tokens = Pcoq.G.Parsable.make (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -247,7 +247,7 @@ let parse_to_dot = | Tok.EOI -> () | _ -> dot tok st in - Pcoq.Entry.of_parser "Coqtoplevel.dot" dot + Pcoq.G.Entry.of_parser "Coqtoplevel.dot" dot (* If an error occurred while parsing, we try to read the input until a dot token is encountered. @@ -255,7 +255,7 @@ let parse_to_dot = let rec discard_to_dot () = try - Pcoq.Entry.parse parse_to_dot top_buffer.tokens + Pcoq.G.Entry.parse parse_to_dot top_buffer.tokens with | CLexer.Error.E _ -> discard_to_dot () | e when CErrors.noncritical e -> () diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 1eafc70530..b07f3e5c57 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -18,7 +18,7 @@ type input_buffer = { mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of beginning of lines *) - mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) + mutable tokens : Pcoq.G.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 955630f40c..ce4b85c75f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -88,7 +88,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in let in_pa = - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file)) + Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile file)) (Stream.of_channel in_chan) in let open State in @@ -100,7 +100,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = with | None -> input_cleanup (); - state, ids, Pcoq.Parsable.comment_state in_pa + state, ids, Pcoq.G.comment_state in_pa | Some ast -> (* Printing of AST for -compile-verbose *) Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo; diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 0946c88228..920be6db5b 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1590,7 +1590,7 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu) type seqrule = -| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule +| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule let rec make_seq_rule = function | [] -> diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 88bcf1d477..7a52f53dc0 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -332,8 +332,8 @@ let make_sep_rules = function Pcoq.G.Symbol.rules ~warning:None [r] type ('s, 'a) mayrec_symbol = -| MayRecNo : ('s, norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol -| MayRecMay : ('s, mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol +| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol +| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> if is_binder_level custom from p @@ -458,8 +458,8 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> ty_eval rem f { env with constrs; constrlists; } type ('s, 'a, 'r) mayrec_rule = -| MayRecRNo : ('s, norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule -| MayRecRMay : ('s, mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule +| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule +| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function | TyStop -> MayRecRNo G.Rule.stop diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 00a239f56e..981de78162 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -24,9 +24,9 @@ type 's grammar_prod_item = type 'a ty_arg = ('a -> raw_generic_argument) type ('self, 'tr, _, 'r) ty_rule = -| TyStop : ('self, Pcoq.norec, 'r, 'r) ty_rule -| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.G.Symbol.t * 'b ty_arg option -> - ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule +| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule +| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) G.Symbol.t * 'b ty_arg option -> + ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 475d5c31f7..38e57a310a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -46,7 +46,7 @@ let entry_buf = Buffer.create 64 let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in - let () = Pcoq.Entry.print ft e in + let () = Pcoq.G.Entry.print ft e in str (Buffer.contents entry_buf) let pr_registered_grammar name = @@ -55,7 +55,7 @@ let pr_registered_grammar name = | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.") | entries -> let pr_one (Pcoq.AnyEntry e) = - str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++ + str "Entry " ++ str (Pcoq.G.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e in prlist pr_one entries diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 2130a398e9..8d0dcbf0fe 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -169,7 +169,7 @@ let suggest_variable env id = let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) +let using_from_string us = Pcoq.G.Entry.parse G_vernac.section_subset_expr (Pcoq.G.Parsable.make (Stream.of_string us)) let proof_using_opt_name = ["Default";"Proof";"Using"] let () = diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 9a9c96064d..26364ed075 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -65,8 +65,8 @@ module Vernac_ = | Some ename -> find_proof_mode ename let command_entry = - Pcoq.Entry.of_parser "command_entry" - (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) + Pcoq.G.Entry.of_parser "command_entry" + (fun _ strm -> Pcoq.G.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) end diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ac4d33c926..4008c3d799 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c | Some Refl -> untype_command ty (f v) args end -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.G.Symbol.t = +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.G.Symbol.t = let open Extend in function -| TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l) -| TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false -| TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l) -| TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false -| TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o) -| TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a)) -| TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i) + | TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l) + | TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false + | TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l) + | TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false + | TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o) + | TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a)) + | TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i) let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function | TyNil -> [] @@ -193,7 +193,7 @@ let vernac_extend ~command ?classifier ?entry ext = | None -> let e = match entry with | None -> "COMMAND" - | Some e -> Pcoq.Entry.name e + | Some e -> Pcoq.G.Entry.name e in let msg = Printf.sprintf "\ Vernac entry \"%s\" misses a classifier. \ diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 15a19c06c2..6b7b2c2691 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -183,12 +183,12 @@ and vernac_load ~verbosely fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = Util.open_utf8_file_in longfname in - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in + Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in (* Parsing loop *) let v_mod = if verbosely then Flags.verbosely else Flags.silently in let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with + match Pcoq.G.Entry.parse (Pvernac.main_entry proof_mode) po with | Some x -> x | None -> raise End_of_input) in let rec load_loop ~stack = diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6846826bfa..49486b889d 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -19,7 +19,7 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; Flags.with_option Flags.we_are_parsing - (fun () -> Pcoq.Entry.parse entry pa) + (fun () -> Pcoq.G.Entry.parse entry pa) () end diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 7607f8373a..ed1b76b618 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -14,7 +14,7 @@ module Parser : sig val init : unit -> state val cur_state : unit -> state - val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a + val parse : state -> 'a Pcoq.Entry.t -> Pcoq.G.Parsable.t -> 'a end -- cgit v1.2.3 From f374c2562b9522bd90330f6f17f0a7e41c723e8b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 21 Feb 2020 12:46:22 -0500 Subject: [parsing] Move `coq_parsable` custom logic to Grammar. Latest refactorings allow us to make the signature Coq parser a standard `Grammar.S` one; the only bit needed is to provide the extra capabilities to the `Lexer` signature w.r.t. to comments state. The handling of Lexer state is still a bit ad-hoc, in particular it is global whereas it should be fully attached to the parsable. This may work ok in batch mode but the current behavior may be buggy in the interactive context. This PR doesn't solve that but it is a step towards a more functional solution. --- gramlib/grammar.ml | 35 +++++++++++++++++++++--- gramlib/grammar.mli | 17 ++++++++++-- parsing/cLexer.ml | 34 ++++++++++++----------- parsing/cLexer.mli | 10 +------ parsing/pcoq.ml | 72 +------------------------------------------------ parsing/pcoq.mli | 9 ++----- printing/proof_diffs.ml | 7 +++-- toplevel/vernac.ml | 2 +- 8 files changed, 73 insertions(+), 113 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 0eed42f290..ac6f752670 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -8,7 +8,18 @@ open Util (* Functorial interface *) -module type GLexerType = Plexing.Lexer +module type GLexerType = sig + include Plexing.Lexer + + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end +end type norec type mayrec @@ -20,6 +31,7 @@ module type S = sig module Parsable : sig type t val make : ?loc:Loc.t -> char Stream.t -> t + val comments : t -> ((int * int) * string) list end val tokens : string -> (string option * int) list @@ -1520,7 +1532,7 @@ module Parsable = struct { pa_chr_strm : char Stream.t ; pa_tok_strm : L.te Stream.t ; pa_loc_func : Plexing.location_function - } + ; lexer_state : L.State.t ref } let parse_parsable entry p = let efun = entry.estart 0 in @@ -1556,9 +1568,26 @@ module Parsable = struct let loc = Stream.count cs, Stream.count cs + 1 in restore (); Ploc.raise (Ploc.make_unlined loc) exc + let parse_parsable e p = + L.State.set !(p.lexer_state); + try + let c = parse_parsable e p in + p.lexer_state := L.State.get (); + c + with Ploc.Exc (loc,e) -> + L.State.drop (); + let loc' = Loc.get_loc (Exninfo.info e) in + let loc = match loc' with None -> loc | Some loc -> loc in + Loc.raise ~loc e + let make ?loc cs = + let lexer_state = ref (L.State.init ()) in + L.State.set !lexer_state; let (ts, lf) = L.tok_func ?loc cs in - {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf} + lexer_state := L.State.get (); + {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf; lexer_state} + + let comments p = L.State.get_comments !(p.lexer_state) end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 4280181109..7738e32cab 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -15,9 +15,21 @@ rule "an entry cannot call an entry of another grammar" by normal OCaml typing. *) -module type GLexerType = Plexing.Lexer - (** The input signature for the functor [Grammar.GMake]: [te] is the +(** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) +module type GLexerType = sig + include Plexing.Lexer + + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end +end + type norec type mayrec @@ -29,6 +41,7 @@ module type S = sig module Parsable : sig type t val make : ?loc:Loc.t -> char Stream.t -> t + val comments : t -> ((int * int) * string) list end val tokens : string -> (string option * int) list diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index a39da96a53..85640cabba 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -392,22 +392,6 @@ let comments = ref [] let current_comment = Buffer.create 8192 let between_commands = ref true -(* The state of the lexer visible from outside *) -type lexer_state = int option * string * bool * ((int * int) * string) list - -let init_lexer_state () = (None,"",true,[]) -let set_lexer_state (o,s,b,c) = - comment_begin := o; - Buffer.clear current_comment; Buffer.add_string current_comment s; - between_commands := b; - comments := c -let get_lexer_state () = - (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) -let drop_lexer_state () = - set_lexer_state (init_lexer_state ()) - -let get_comment_state (_,_,_,c) = c - let real_push_char c = Buffer.add_char current_comment c (* Add a char if it is between two commands, if it is a newline or @@ -851,6 +835,24 @@ module MakeLexer (Diff : sig val mode : bool end) = struct let tok_removing = (fun _ -> ()) let tok_match = Tok.match_pattern let tok_text = token_text + + (* The state of the lexer visible from outside *) + module State = struct + + type t = int option * string * bool * ((int * int) * string) list + + let init () = (None,"",true,[]) + let set (o,s,b,c) = + comment_begin := o; + Buffer.clear current_comment; Buffer.add_string current_comment s; + between_commands := b; + comments := c + let get () = + (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) + let drop () = set (init ()) + let get_comments (_,_,_,c) = c + + end end module Lexer = MakeLexer (struct let mode = false end) diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 2c1284c4db..67b8310bde 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -63,15 +63,6 @@ module Error : sig val to_string : t -> string end -(* Mainly for comments state, etc... *) -type lexer_state - -val init_lexer_state : unit -> lexer_state -val set_lexer_state : lexer_state -> unit -val get_lexer_state : unit -> lexer_state -val drop_lexer_state : unit -> unit -val get_comment_state : lexer_state -> ((int * int) * string) list - (** Create a lexer. true enables alternate handling for computing diffs. It ensures that, ignoring white space, the concatenated tokens equal the input string. Specifically: @@ -81,5 +72,6 @@ as if it was unquoted, possibly becoming multiple tokens it was not in a comment, possibly becoming multiple tokens - return any unrecognized Ascii or UTF-8 character as a string *) + module LexerDiff : Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8f3c1e029c..59f92e7790 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,77 +14,7 @@ open Genarg open Gramlib (** The parser of Coq *) - -module G : sig - - include Grammar.S - with type te = Tok.t - and type 'c pattern = 'c Tok.p - - val comment_state : Parsable.t -> ((int * int) * string) list - -end = struct - - module G_ = Grammar.GMake(CLexer.Lexer) - - type te = G_.te - type 'c pattern = 'c G_.pattern - - type coq_parsable = G_.Parsable.t * CLexer.lexer_state ref - - let coq_parsable ?loc c = - let state = ref (CLexer.init_lexer_state ()) in - CLexer.set_lexer_state !state; - let a = G_.Parsable.make ?loc c in - state := CLexer.get_lexer_state (); - (a,state) - - let comment_state (p,state) = - CLexer.get_comment_state !state - - module Parsable = struct - type t = coq_parsable - let make = coq_parsable - (* let comment_state = comment_state *) - end - - let tokens = G_.tokens - - type 'a single_extend_statement = 'a G_.single_extend_statement - type 'a extend_statement = 'a G_.extend_statement = - { pos : Gramlib.Gramext.position option - ; data : 'a single_extend_statement list - } - - module Entry = struct - include G_.Entry - - let parse e (p,state) = - CLexer.set_lexer_state !state; - try - let c = G_.Entry.parse e p in - state := CLexer.get_lexer_state (); - c - with Ploc.Exc (loc,e) -> - CLexer.drop_lexer_state (); - let loc' = Loc.get_loc (Exninfo.info e) in - let loc = match loc' with None -> loc | Some loc -> loc in - Loc.raise ~loc e - - end - - module Symbol = G_.Symbol - module Rule = G_.Rule - module Rules = G_.Rules - module Production = G_.Production - module Unsafe = G_.Unsafe - - let safe_extend = G_.safe_extend - let safe_delete_rule = G_.safe_delete_rule - let level_of_nonterm = G_.level_of_nonterm - let generalize_symbol = G_.generalize_symbol - let mk_rule = G_.mk_rule -end +module G = Grammar.GMake(CLexer.Lexer) module Entry = struct include G.Entry diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0352c1d55b..5d21b39dee 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -15,14 +15,9 @@ open Libnames (** The parser of Coq *) -module G : sig - - include Gramlib.Grammar.S - - val comment_state : Parsable.t -> ((int * int) * string) list - -end with type te = Tok.t and type 'a pattern = 'a Tok.p +module G : Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p +(** Compatibility module, please avoid *) module Entry : sig type 'a t = 'a G.Entry.t val create : string -> 'a t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index fb91ea7b5c..9d75341795 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -98,18 +98,17 @@ let tokenize_string s = else stream_tok ((Tok.extract_string true e) :: acc) str in - let st = CLexer.get_lexer_state () in + let st = CLexer.Lexer.State.get () in try let istr = Stream.of_string s in let lex = CLexer.LexerDiff.tok_func istr in let toks = stream_tok [] (fst lex) in - CLexer.set_lexer_state st; + CLexer.Lexer.State.set st; toks with exn -> - CLexer.set_lexer_state st; + CLexer.Lexer.State.set st; raise (Diff_Failure "Input string is not lexable");; - type hyp_info = { idents: string list; rhs_pp: Pp.t; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ce4b85c75f..f501e89ed5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -100,7 +100,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = with | None -> input_cleanup (); - state, ids, Pcoq.G.comment_state in_pa + state, ids, Pcoq.G.Parsable.comments in_pa | Some ast -> (* Printing of AST for -compile-verbose *) Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo; -- cgit v1.2.3 From 9847448b5f9dbf32806decf676f415d584a2cddb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 21 Feb 2020 12:59:51 -0500 Subject: [gramlib] Remove warning function parameter in favor of standard mechanism. If we need more fine-tuning we should manage the warnings with the standard Coq mechanism. --- coqpp/coqpp_main.ml | 2 +- gramlib/grammar.ml | 85 +++++++++++++++++++----------------------- gramlib/grammar.mli | 5 +-- parsing/pcoq.ml | 18 ++++----- user-contrib/Ltac2/tac2core.ml | 2 +- vernac/egramcoq.ml | 2 +- 6 files changed, 51 insertions(+), 63 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 17f81c555c..0e0aefaaef 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -253,7 +253,7 @@ and print_symbol fmt tkn = match tkn with fprintf fmt "Pcoq.G.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body) in let pr fmt rules = print_list fmt pr rules in - fprintf fmt "(Pcoq.G.Symbol.rules ~warning:None %a)" pr (List.rev rules) + fprintf fmt "(Pcoq.G.Symbol.rules %a)" pr (List.rev rules) | SymbQuote c -> fprintf fmt "(%s)" c diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index ac6f752670..814844508b 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -63,7 +63,7 @@ module type S = sig val self : ('self, mayrec, 'self) t val next : ('self, mayrec, 'self) t val token : 'c pattern -> ('self, norec, 'c) t - val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t + val rules : 'a Rules.t list -> ('self, norec, 'a) t end and Rule : sig @@ -101,7 +101,7 @@ module type S = sig ; data : 'a single_extend_statement list } - val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit + val safe_extend : 'a Entry.t -> 'a extend_statement -> unit val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option @@ -348,7 +348,7 @@ let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_r | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2 | NoRec2, NoRec3, NoRec -> NoRec2 -let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree = +let insert_tree (type s trs trt tr p k a) entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree = let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree = fun ar symbols pf tree action -> match symbols, pf with @@ -362,15 +362,15 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t | NR10, Node (_, n) -> Node (MayRec3, node n) | NR11, Node (NoRec3, n) -> Node (NoRec3, node n) | NR11, LocAct (old_action, action_list) -> - begin match warning with - | None -> () - | Some warn_fn -> + (* What to do about this warning? For now it is disabled *) + if false then + begin let msg = " Grammar extension: " ^ (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^ "some rule has been masked" in - warn_fn msg - end; + Feedback.msg_warning (Pp.str msg) + end; LocAct (action, old_action :: action_list) | NR11, DeadEnd -> LocAct (action, []) and insert_in_tree : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_ex -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree = @@ -429,14 +429,14 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t in insert ar gsymbols pf tree action -let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree = - insert_tree ~warning entry_name NR11 gsymbols pf action tree +let insert_tree_norec (type s p k a) entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree = + insert_tree entry_name NR11 gsymbols pf action tree -let insert_tree (type s trs trt p k a) ~warning entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree = +let insert_tree (type s trs trt p k a) entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree = let MayRecNR ar = and_symbols_tree gsymbols tree in - MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree) + MayRecTree (insert_tree entry_name ar gsymbols pf action tree) -let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_symbol = +let srules (type self a) (rl : a ty_rules list) : (self, norec, a) ty_symbol = let rec retype_tree : type s a. (s, norec, a) ty_tree -> (self, norec, a) ty_tree = function | Node (NoRec3, {node = s; son = son; brother = bro}) -> @@ -463,7 +463,7 @@ let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_s (fun tree (TRules (symbols, action)) -> let symbols = retype_rule symbols in let AnyS (symbols, pf) = get_symbols symbols in - insert_tree_norec ~warning "" symbols pf action tree) + insert_tree_norec "" symbols pf action tree) DeadEnd rl in Stree t @@ -473,19 +473,19 @@ let is_level_labelled n (Level lev) = Some n1 -> n = n1 | None -> false -let insert_level (type s tr p k) ~warning entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = +let insert_level (type s tr p k) entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = match symbols with | TCns (_, Sself, symbols) -> let Level slev = slev in let RelS pf = pf in - let MayRecTree lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix in + let MayRecTree lsuffix = insert_tree entry_name symbols pf action slev.lsuffix in Level {assoc = slev.assoc; lname = slev.lname; lsuffix = lsuffix; lprefix = slev.lprefix} | _ -> let Level slev = slev in - let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in + let MayRecTree lprefix = insert_tree entry_name symbols pf action slev.lprefix in Level {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; lprefix = lprefix} @@ -499,34 +499,27 @@ let empty_lev lname assoc = Level {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} -let change_lev ~warning (Level lev) n lname assoc = +let change_lev (Level lev) n lname assoc = let a = match assoc with None -> lev.assoc | Some a -> if a <> lev.assoc then - begin - match warning with - | None -> () - | Some warn_fn -> - warn_fn (" Changing associativity of level \""^n^"\"") - end; - a + Feedback.msg_warning (Pp.str (" Changing associativity of level \""^n^"\"")); + a in - begin match lname with - Some n -> - if lname <> lev.lname then - begin match warning with - | None -> () - | Some warn_fn -> - warn_fn (" Level label \""^n^"\" ignored") - end; - | None -> () + begin + match lname with + | Some n -> + (* warning disabled; it was in the past *) + if false && lname <> lev.lname then + Feedback.msg_warning (Pp.str (" Level label \""^n^"\" ignored")) + | None -> () end; Level {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} -let get_level ~warning entry position levs = +let get_level entry position levs = match position with Some First -> [], empty_lev, levs | Some Last -> levs, empty_lev, [] @@ -539,7 +532,7 @@ let get_level ~warning entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if is_level_labelled n lev then [], change_lev ~warning lev n, levs + if is_level_labelled n lev then [], change_lev lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in @@ -574,7 +567,7 @@ let get_level ~warning entry position levs = get levs | None -> match levs with - lev :: levs -> [], change_lev ~warning lev "", levs + lev :: levs -> [], change_lev lev "", levs | [] -> [], empty_lev, [] let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol = @@ -624,7 +617,7 @@ let insert_tokens gram symbols = in linsert symbols -let levels_of_rules ~warning entry position rules = +let levels_of_rules entry position rules = let elev = match entry.edesc with Dlevels elev -> elev @@ -636,7 +629,7 @@ let levels_of_rules ~warning entry position rules = match rules with | [] -> elev | _ -> - let (levs1, make_lev, levs2) = get_level ~warning entry position elev in + let (levs1, make_lev, levs2) = get_level entry position elev in let (levs, _) = List.fold_left (fun (levs, make_lev) (lname, assoc, level) -> @@ -647,7 +640,7 @@ let levels_of_rules ~warning entry position rules = let MayRecRule symbols = change_to_self entry symbols in let AnyS (symbols, pf) = get_symbols symbols in insert_tokens egram symbols; - insert_level ~warning entry.ename symbols pf action lev) + insert_level entry.ename symbols pf action lev) lev level in lev :: levs, empty_lev) @@ -1503,8 +1496,8 @@ let init_entry_functions entry = let f = continue_parser_of_entry entry in entry.econtinue <- f; f lev bp a strm) -let extend_entry ~warning entry position rules = - let elev = levels_of_rules ~warning entry position rules in +let extend_entry entry position rules = + let elev = levels_of_rules entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry (* Deleting a rule *) @@ -1630,7 +1623,7 @@ module rec Symbol : sig val self : ('self, mayrec, 'self) t val next : ('self, mayrec, 'self) t val token : 'c pattern -> ('self, norec, 'c) t - val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t + val rules : 'a Rules.t list -> ('self, norec, 'a) t end = struct @@ -1645,7 +1638,7 @@ end = struct let self = Sself let next = Snext let token tok = Stoken tok - let rules ~warning (t : 'a Rules.t list) = srules ~warning t + let rules (t : 'a Rules.t list) = srules t end and Rule : sig @@ -1705,8 +1698,8 @@ type 'a extend_statement = ; data : 'a single_extend_statement list } -let safe_extend ~warning (e : 'a Entry.t) { pos; data } = - extend_entry ~warning e pos data +let safe_extend (e : 'a Entry.t) { pos; data } = + extend_entry e pos data let safe_delete_rule e (TProd (r,_act)) = let AnyS (symbols, _) = get_symbols r in diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 7738e32cab..16e147de3b 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -30,7 +30,6 @@ module type GLexerType = sig end end - type norec type mayrec @@ -73,7 +72,7 @@ module type S = sig val self : ('self, mayrec, 'self) t val next : ('self, mayrec, 'self) t val token : 'c pattern -> ('self, norec, 'c) t - val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t + val rules : 'a Rules.t list -> ('self, norec, 'a) t end and Rule : sig @@ -111,7 +110,7 @@ module type S = sig ; data : 'a single_extend_statement list } - val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit + val safe_extend : 'a Entry.t -> 'a extend_statement -> unit val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 59f92e7790..fe280c1f69 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -127,25 +127,24 @@ let grammar_delete_reinit e reinit ({ G.pos; data } as d)= | Some (Gramext.Level n) -> n | _ -> assert false in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in - G.safe_extend ~warning:(Some warning) e ext + G.safe_extend e ext (** Extension *) let grammar_extend e ext = let undo () = grammar_delete e ext in - let redo () = G.safe_extend ~warning:None e ext in + let redo () = G.safe_extend e ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e ext = camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; - G.safe_extend ~warning:None e ext + G.safe_extend e ext let grammar_extend_sync_reinit e reinit ext = camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; - G.safe_extend ~warning:None e ext + G.safe_extend e ext (** Remove extensions @@ -189,18 +188,16 @@ let eoi_entry en = let e = G.Entry.make ((G.Entry.name en) ^ "_eoi") in let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in let act = fun _ x loc -> x in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - G.safe_extend ~warning:(Some warning) e ext; + G.safe_extend e ext; e let map_entry f en = let e = G.Entry.make ((G.Entry.name en) ^ "_map") in let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in let act = fun x loc -> f x in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - G.safe_extend ~warning:(Some warning) e ext; + G.safe_extend e ext; e (* Parse a string, does NOT check if the entire string was read @@ -348,9 +345,8 @@ module Module = let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) = let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in let entry = G.Entry.make "epsilon" in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = [None, None, [r]] } in - let () = G.safe_extend ~warning:(Some warning) entry ext in + let () = G.safe_extend entry ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 920be6db5b..ab660b486e 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1614,7 +1614,7 @@ let rec make_seq_rule = function let () = add_scope "seq" begin fun toks -> let scope = let Seqrule (r, c) = make_seq_rule (List.rev toks) in - Pcoq.G.(Symbol.rules ~warning:None [Rules.make r (apply c [])]) + Pcoq.G.(Symbol.rules [Rules.make r (apply c [])]) in Tac2entries.ScopeRule (scope, (fun e -> e)) end diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 7a52f53dc0..c4f15a40ce 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -329,7 +329,7 @@ let make_sep_rules = function Pcoq.G.Symbol.token tk | tkl -> let r = Pcoq.G.mk_rule (List.rev tkl) in - Pcoq.G.Symbol.rules ~warning:None [r] + Pcoq.G.Symbol.rules [r] type ('s, 'a) mayrec_symbol = | MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol -- cgit v1.2.3 From ef3079e22fa7941d3335d7779c840e8d2d2bde39 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 21 Feb 2020 14:18:37 -0500 Subject: [parsing] Move comments lexer extensions to base lexer interface This makes sense as a step towards a more functional handling of the state. --- gramlib/grammar.ml | 15 +-------------- gramlib/grammar.mli | 15 +-------------- gramlib/plexing.ml | 13 ++++++++++++- gramlib/plexing.mli | 13 ++++++++++++- parsing/cLexer.mli | 4 ++-- 5 files changed, 28 insertions(+), 32 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 814844508b..834850082e 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -8,19 +8,6 @@ open Util (* Functorial interface *) -module type GLexerType = sig - include Plexing.Lexer - - module State : sig - type t - val init : unit -> t - val set : t -> unit - val get : unit -> t - val drop : unit -> unit - val get_comments : t -> ((int * int) * string) list - end -end - type norec type mayrec @@ -115,7 +102,7 @@ end (* Implementation *) -module GMake (L : GLexerType) = struct +module GMake (L : Plexing.S) = struct type te = L.te type 'c pattern = 'c L.pattern diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 16e147de3b..0872321da0 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -17,18 +17,6 @@ (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) -module type GLexerType = sig - include Plexing.Lexer - - module State : sig - type t - val init : unit -> t - val set : t -> unit - val get : unit -> t - val drop : unit -> unit - val get_comments : t -> ((int * int) * string) list - end -end type norec type mayrec @@ -130,5 +118,4 @@ end type (instead of (string * string)); the module parameter must specify a way to show them as (string * string) *) -module GMake (L : GLexerType) : - S with type te = L.te and type 'c pattern = 'c L.pattern +module GMake (L : Plexing.S) : S with type te = L.te and type 'c pattern = 'c L.pattern diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index e881ab3350..ce3e38ff08 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -5,7 +5,7 @@ type location_function = int -> Loc.t type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function -module type Lexer = sig +module type S = sig type te type 'c pattern val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option @@ -15,4 +15,15 @@ module type Lexer = sig val tok_removing : 'c pattern -> unit val tok_match : 'c pattern -> te -> 'c val tok_text : 'c pattern -> string + + (* State for the comments, at some point we should make it functional *) + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end + end diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 521eba7446..0c190af635 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -15,7 +15,7 @@ and location_function = int -> Loc.t (** The type of a function giving the location of a token in the source from the token number in the stream (starting from zero). *) -module type Lexer = sig +module type S = sig type te type 'c pattern val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option @@ -25,4 +25,15 @@ module type Lexer = sig val tok_removing : 'c pattern -> unit val tok_match : 'c pattern -> te -> 'c val tok_text : 'c pattern -> string + + (* State for the comments, at some point we should make it functional *) + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end + end diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 67b8310bde..ac2c5bcfe2 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -55,7 +55,7 @@ val terminal_numeral : string -> NumTok.Unsigned.t Tok.p (** The lexer of Coq: *) module Lexer : - Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p + Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p module Error : sig type t @@ -74,4 +74,4 @@ it was not in a comment, possibly becoming multiple tokens *) module LexerDiff : - Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p + Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p -- 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 --- coqpp/coqpp_main.ml | 36 ++++++++--------- gramlib/grammar.ml | 2 + gramlib/grammar.mli | 1 + ide/idetop.ml | 6 +-- parsing/pcoq.ml | 75 ++++++++++++++++------------------- parsing/pcoq.mli | 17 +++----- plugins/ltac/g_tactic.mlg | 2 +- plugins/ltac/tacentries.ml | 36 ++++++++--------- plugins/ssr/ssrparser.mlg | 22 +++++----- plugins/ssrmatching/g_ssrmatching.mlg | 2 +- stm/stm.mli | 4 +- toplevel/coqloop.ml | 10 ++--- toplevel/coqloop.mli | 2 +- toplevel/vernac.ml | 4 +- user-contrib/Ltac2/g_ltac2.mlg | 10 ++--- user-contrib/Ltac2/tac2core.ml | 42 ++++++++++---------- user-contrib/Ltac2/tac2entries.ml | 16 ++++---- user-contrib/Ltac2/tac2entries.mli | 2 +- vernac/egramcoq.ml | 72 ++++++++++++++++----------------- vernac/egramml.ml | 16 ++++---- vernac/egramml.mli | 4 +- vernac/metasyntax.ml | 4 +- vernac/proof_using.ml | 2 +- vernac/pvernac.ml | 10 ++--- vernac/vernacextend.ml | 22 +++++----- vernac/vernacextend.mli | 2 +- vernac/vernacinterp.ml | 4 +- vernac/vernacstate.ml | 2 +- vernac/vernacstate.mli | 2 +- 29 files changed, 210 insertions(+), 219 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 0e0aefaaef..43cd6f1784 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -115,7 +115,7 @@ let print_local fmt ext = match locals with | [] -> () | e :: locals -> - let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in + let mk_e fmt e = fprintf fmt "Pcoq.Entry.make \"%s\"" e in let () = fprintf fmt "@[let %s =@ @[%a@]@]@ " e mk_e e in let iter e = fprintf fmt "@[and %s =@ @[%a@]@]@ " e mk_e e in let () = List.iter iter locals in @@ -217,43 +217,43 @@ let rec print_prod fmt p = and print_extrule fmt (tkn, vars, body) = let tkn = List.rev tkn in - fprintf fmt "@[Pcoq.G.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body) + fprintf fmt "@[Pcoq.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body) and print_symbols ~norec fmt = function -| [] -> fprintf fmt "Pcoq.G.Rule.stop" +| [] -> fprintf fmt "Pcoq.Rule.stop" | tkn :: tkns -> - let c = if norec then "Pcoq.G.Rule.next_norec" else "Pcoq.G.Rule.next" in + let c = if norec then "Pcoq.Rule.next_norec" else "Pcoq.Rule.next" in fprintf fmt "%s @[(%a)@ (%a)@]" c (print_symbols ~norec) tkns print_symbol tkn and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> - fprintf fmt "(Pcoq.G.Symbol.token (%a))" print_tok (t, s) + fprintf fmt "(Pcoq.Symbol.token (%a))" print_tok (t, s) | SymbEntry (e, None) -> - fprintf fmt "(Pcoq.G.Symbol.nterm %s)" e + fprintf fmt "(Pcoq.Symbol.nterm %s)" e | SymbEntry (e, Some l) -> - fprintf fmt "(Pcoq.G.Symbol.nterml %s (%a))" e print_string l + fprintf fmt "(Pcoq.Symbol.nterml %s (%a))" e print_string l | SymbSelf -> - fprintf fmt "Pcoq.G.Symbol.self" + fprintf fmt "Pcoq.Symbol.self" | SymbNext -> - fprintf fmt "Pcoq.G.Symbol.next" + fprintf fmt "Pcoq.Symbol.next" | SymbList0 (s, None) -> - fprintf fmt "(Pcoq.G.Symbol.list0 %a)" print_symbol s + fprintf fmt "(Pcoq.Symbol.list0 %a)" print_symbol s | SymbList0 (s, Some sep) -> - fprintf fmt "(Pcoq.G.Symbol.list0sep (%a) (%a) false)" print_symbol s print_symbol sep + fprintf fmt "(Pcoq.Symbol.list0sep (%a) (%a) false)" print_symbol s print_symbol sep | SymbList1 (s, None) -> - fprintf fmt "(Pcoq.G.Symbol.list1 (%a))" print_symbol s + fprintf fmt "(Pcoq.Symbol.list1 (%a))" print_symbol s | SymbList1 (s, Some sep) -> - fprintf fmt "(Pcoq.G.Symbol.list1sep (%a) (%a) false)" print_symbol s print_symbol sep + fprintf fmt "(Pcoq.Symbol.list1sep (%a) (%a) false)" print_symbol s print_symbol sep | SymbOpt s -> - fprintf fmt "(Pcoq.G.Symbol.opt %a)" print_symbol s + fprintf fmt "(Pcoq.Symbol.opt %a)" print_symbol s | SymbRules rules -> let pr fmt (r, body) = let (vars, tkn) = List.split r in let tkn = List.rev tkn in - fprintf fmt "Pcoq.G.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body) + fprintf fmt "Pcoq.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body) in let pr fmt rules = print_list fmt pr rules in - fprintf fmt "(Pcoq.G.Symbol.rules %a)" pr (List.rev rules) + fprintf fmt "(Pcoq.Symbol.rules %a)" pr (List.rev rules) | SymbQuote c -> fprintf fmt "(%s)" c @@ -266,7 +266,7 @@ let print_rule fmt r = let print_entry fmt e = let print_position_opt fmt pos = print_opt fmt print_position pos in let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.G.pos=%a; data=%a}@]@]@ in@ " + fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.pos=%a; data=%a}@]@]@ in@ " e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules let print_ast fmt ext = @@ -452,7 +452,7 @@ let terminal s = let p = if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_numeral" else "CLexer.terminal" in - let c = Printf.sprintf "Pcoq.G.Symbol.token (%s \"%s\")" p s in + let c = Printf.sprintf "Pcoq.Symbol.token (%s \"%s\")" p s in SymbQuote c let rec parse_symb self = function diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 834850082e..41669b77c9 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -26,6 +26,7 @@ module type S = sig module Entry : sig type 'a t val make : string -> 'a t + val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val name : 'a t -> string val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t @@ -1578,6 +1579,7 @@ module Entry = struct econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} + let create = make let parse (e : 'a t) p : 'a = Parsable.parse_parsable e p let parse_token_stream (e : 'a t) ts : 'a = diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 0872321da0..6f998f7b80 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -36,6 +36,7 @@ module type S = sig module Entry : sig type 'a t val make : string -> 'a t + val create : string -> 'a t (* compat *) val parse : 'a t -> Parsable.t -> 'a val name : 'a t -> string val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t diff --git a/ide/idetop.ml b/ide/idetop.ml index 81e7e4d148..0ef7fca41f 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -91,7 +91,7 @@ let set_doc doc = ide_doc := Some doc let add ((s,eid),(sid,verbose)) = let doc = get_doc () in - let pa = Pcoq.G.Parsable.make (Stream.of_string s) in + let pa = Pcoq.Parsable.make (Stream.of_string s) in match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with | None -> assert false (* s is not an empty string *) | Some ast -> @@ -127,13 +127,13 @@ let edit_at id = * be removed in the next version of the protocol. *) let query (route, (s,id)) = - let pa = Pcoq.G.Parsable.make (Stream.of_string s) in + let pa = Pcoq.Parsable.make (Stream.of_string s) in let doc = get_doc () in Stm.query ~at:id ~doc ~route pa let annotate phrase = let doc = get_doc () in - let pa = Pcoq.G.Parsable.make (Stream.of_string phrase) in + let pa = Pcoq.Parsable.make (Stream.of_string phrase) in match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with | None -> Richpp.richpp_of_pp 78 (Pp.mt ()) | Some ast -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index fe280c1f69..5b0562fb0d 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,12 +14,7 @@ open Genarg open Gramlib (** The parser of Coq *) -module G = Grammar.GMake(CLexer.Lexer) - -module Entry = struct - include G.Entry - let create = make -end +include Grammar.GMake(CLexer.Lexer) module Lookahead = struct @@ -40,7 +35,7 @@ struct let to_entry s (lk : t) = let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in - G.Entry.of_parser s run + Entry.of_parser s run let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with | None -> None @@ -94,17 +89,17 @@ end type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position type extend_rule = -| ExtendRule : 'a G.Entry.t * 'a G.extend_statement -> extend_rule -| ExtendRuleReinit : 'a G.Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule module EntryCommand = Dyn.Make () -module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end +module EntryData = struct type _ t = Ex : 'b Entry.t String.Map.t -> ('a * 'b) t end module EntryDataMap = EntryCommand.Map(EntryData) type ext_kind = | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) - | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.t -> ext_kind + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b Entry.t -> ext_kind (** The list of extensions *) @@ -114,37 +109,37 @@ let camlp5_entries = ref EntryDataMap.empty (** Deletion *) -let grammar_delete e { G.pos; data } = +let grammar_delete e { pos; data } = List.iter (fun (n,ass,lev) -> - List.iter (fun pil -> G.safe_delete_rule e pil) (List.rev lev)) + List.iter (fun pil -> safe_delete_rule e pil) (List.rev lev)) (List.rev data) -let grammar_delete_reinit e reinit ({ G.pos; data } as d)= +let grammar_delete_reinit e reinit ({ pos; data } as d)= grammar_delete e d; let a, ext = reinit in let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false in - let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in - G.safe_extend e ext + let ext = { pos = Some ext; data = [Some lev,Some a,[]] } in + safe_extend e ext (** Extension *) let grammar_extend e ext = let undo () = grammar_delete e ext in - let redo () = G.safe_extend e ext in + let redo () = safe_extend e ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e ext = camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; - G.safe_extend e ext + safe_extend e ext let grammar_extend_sync_reinit e reinit ext = camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; - G.safe_extend e ext + safe_extend e ext (** Remove extensions @@ -170,7 +165,7 @@ let rec remove_grammars n = redo(); camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state | ByEntry (tag, name, e) :: t -> - G.Unsafe.clear_entry e; + Unsafe.clear_entry e; camlp5_state := t; let EntryData.Ex entries = try EntryDataMap.find tag !camlp5_entries @@ -185,19 +180,19 @@ let make_rule r = [None, None, r] (** An entry that checks we reached the end of the input. *) let eoi_entry en = - let e = G.Entry.make ((G.Entry.name en) ^ "_eoi") in - let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in + let e = Entry.make ((Entry.name en) ^ "_eoi") in + let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (Symbol.token Tok.PEOI) in let act = fun _ x loc -> x in - let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - G.safe_extend e ext; + let ext = { pos = None; data = make_rule [Production.make symbs act] } in + safe_extend e ext; e let map_entry f en = - let e = G.Entry.make ((G.Entry.name en) ^ "_map") in - let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in + let e = Entry.make ((Entry.name en) ^ "_map") in + let symbs = Rule.next Rule.stop (Symbol.nterm en) in let act = fun x loc -> f x in - let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - G.safe_extend e ext; + let ext = { pos = None; data = make_rule [Production.make symbs act] } in + safe_extend e ext; e (* Parse a string, does NOT check if the entire string was read @@ -205,7 +200,7 @@ let map_entry f en = let parse_string f ?loc x = let strm = Stream.of_string x in - G.Entry.parse f (G.Parsable.make ?loc strm) + Entry.parse f (Parsable.make ?loc strm) type gram_universe = string @@ -226,14 +221,14 @@ let get_univ u = let new_entry u s = let ename = u ^ ":" ^ s in - let e = G.Entry.make ename in + let e = Entry.make ename in e let make_gen_entry u s = new_entry u s module GrammarObj = struct - type ('r, _, _) obj = 'r G.Entry.t + type ('r, _, _) obj = 'r Entry.t let name = "grammar" let default _ = None end @@ -256,7 +251,7 @@ let genarg_grammar x = check_compatibility x; Grammar.obj x -let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a G.Entry.t = +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t = let e = new_entry u s in let Rawwit t = etyp in let () = Grammar.register0 t e in @@ -342,11 +337,11 @@ module Module = let module_type = Entry.create "module_type" end -let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) = - let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in - let entry = G.Entry.make "epsilon" in - let ext = { G.pos = None; data = [None, None, [r]] } in - let () = G.safe_extend entry ext in +let epsilon_value (type s tr a) f (e : (s, tr, a) Symbol.t) = + let r = Production.make (Rule.next Rule.stop e) (fun x _ -> f x) in + let entry = Entry.make "epsilon" in + let ext = { pos = None; data = [None, None, [r]] } in + let () = safe_extend entry ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -404,14 +399,14 @@ let extend_grammar_command tag g = let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b G.Entry.t list = +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Entry.t list = let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty | (_, st) :: _ -> st in let (names, st) = modify g grammar_state in - let entries = List.map (fun name -> G.Entry.make name) names in + let entries = List.map (fun name -> Entry.make name) names in let iter name e = camlp5_state := ByEntry (tag, name, e) :: !camlp5_state; let EntryData.Ex old = @@ -437,7 +432,7 @@ let extend_dyn_grammar (e, _) = match e with (** Registering extra grammar *) -type any_entry = AnyEntry : 'a G.Entry.t -> any_entry +type any_entry = AnyEntry : 'a Entry.t -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5d21b39dee..90088be307 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -15,14 +15,7 @@ open Libnames (** The parser of Coq *) -module G : Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p - -(** Compatibility module, please avoid *) -module Entry : sig - type 'a t = 'a G.Entry.t - val create : string -> 'a t - val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t -end +include Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p module Lookahead : sig type t @@ -214,11 +207,11 @@ module Module : (** {5 Type-safe grammar extension} *) -val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option +val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Symbol.t -> 'self option (** {5 Extending the parser without synchronization} *) -val grammar_extend : 'a Entry.t -> 'a G.extend_statement -> unit +val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -238,8 +231,8 @@ type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) type extend_rule = -| ExtendRule : 'a Entry.t * 'a G.extend_statement -> extend_rule -| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule +| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule +| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, 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 diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index c3396584a4..442b40221b 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -263,16 +263,16 @@ let negate_parser f tok x = | Some _ -> raise Stream.Failure let test_not_ssrslashnum = - Pcoq.G.Entry.of_parser + Pcoq.Entry.of_parser "test_not_ssrslashnum" (negate_parser test_ssrslashnum10) let test_ssrslashnum00 = - Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 + Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00 let test_ssrslashnum10 = - Pcoq.G.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 + Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10 let test_ssrslashnum11 = - Pcoq.G.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 + Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11 let test_ssrslashnum01 = - Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 + Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01 } @@ -459,7 +459,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "@" -> xWithAt | _ -> xNoFlag -let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind (* New kinds of terms *) @@ -470,7 +470,7 @@ let input_term_annotation _ strm = | Tok.KEYWORD "@" :: _ -> `At | _ -> `None let term_annotation = - Pcoq.G.Entry.of_parser "term_annotation" input_term_annotation + Pcoq.Entry.of_parser "term_annotation" input_term_annotation (* terms *) @@ -811,7 +811,7 @@ let reject_ssrhid _ strm = | _ -> ()) | _ -> () -let test_nohidden = Pcoq.G.Entry.of_parser "test_ssrhid" reject_ssrhid +let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid let rec reject_binder crossed_paren k tok s = match @@ -825,7 +825,7 @@ let rec reject_binder crossed_paren k tok s = | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure | _ -> if crossed_paren then () else raise Stream.Failure -let _test_nobinder = Pcoq.G.Entry.of_parser "test_nobinder" (reject_binder false 0) +let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0) } @@ -1659,7 +1659,7 @@ let ssr_id_of_string loc s = ^ "Scripts with explicit references to anonymous variables are fragile.")) end; Id.of_string s -let ssr_null_entry = Pcoq.G.Entry.of_parser "ssr_null" (fun _ _ -> ()) +let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ()) } @@ -2382,7 +2382,7 @@ let test_ssr_rw_syntax = match Util.stream_nth 0 strm with | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> () | _ -> raise Stream.Failure in - Pcoq.G.Entry.of_parser "test_ssr_rw_syntax" test + Pcoq.Entry.of_parser "test_ssr_rw_syntax" test } diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 59abf80dc5..33e523a4a4 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -70,7 +70,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind } diff --git a/stm/stm.mli b/stm/stm.mli index 88da3c747f..2c27d63b82 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -93,7 +93,7 @@ val new_doc : stm_init_options -> doc * Stateid.t be the case if an error was raised at parsing time). *) val parse_sentence : doc:doc -> Stateid.t -> - entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.G.Parsable.t -> 'a + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a (* Reminder: A parsable [pa] is constructed using [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) @@ -119,7 +119,7 @@ val get_proof : doc:doc -> Stateid.t -> Proof.t option throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : doc:doc -> - at:Stateid.t -> route:Feedback.route_id -> Pcoq.G.Parsable.t -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 0d9edb248b..b8acdd3af1 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Pcoq.G.Parsable.t; (* stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.G.Parsable.make (Stream.from (prompt_char doc ic ibuf)); + ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -230,7 +230,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Pcoq.G.Parsable.make (Stream.of_list []); + tokens = Pcoq.Parsable.make (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -247,7 +247,7 @@ let parse_to_dot = | Tok.EOI -> () | _ -> dot tok st in - Pcoq.G.Entry.of_parser "Coqtoplevel.dot" dot + Pcoq.Entry.of_parser "Coqtoplevel.dot" dot (* If an error occurred while parsing, we try to read the input until a dot token is encountered. @@ -255,7 +255,7 @@ let parse_to_dot = let rec discard_to_dot () = try - Pcoq.G.Entry.parse parse_to_dot top_buffer.tokens + Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | CLexer.Error.E _ -> discard_to_dot () | e when CErrors.noncritical e -> () diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index b07f3e5c57..1eafc70530 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -18,7 +18,7 @@ type input_buffer = { mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of beginning of lines *) - mutable tokens : Pcoq.G.Parsable.t; (** stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f501e89ed5..076796468f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -88,7 +88,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in let in_pa = - Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile file)) + Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file)) (Stream.of_channel in_chan) in let open State in @@ -100,7 +100,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = with | None -> input_cleanup (); - state, ids, Pcoq.G.Parsable.comments in_pa + state, ids, Pcoq.Parsable.comments in_pa | Some ast -> (* Printing of AST for -compile-verbose *) Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo; diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 477672ebdb..57d59fc2ef 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -827,9 +827,9 @@ END let () = let open Tok in -let (++) r s = Pcoq.G.Rule.next r s in +let (++) r s = Pcoq.Rule.next r s in let rules = [ - Pcoq.G.( + Pcoq.( Production.make (Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.ident) begin fun id _ _ loc -> @@ -839,7 +839,7 @@ let rules = [ end ); - Pcoq.G.( + Pcoq.( Production.make (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident) begin fun id _ _ loc -> @@ -849,7 +849,7 @@ let rules = [ end ); - Pcoq.G.( + Pcoq.( Production.make (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++ Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")")) @@ -861,7 +861,7 @@ let rules = [ ] in Hook.set Tac2entries.register_constr_quotations begin fun () -> - Pcoq.grammar_extend Pcoq.Constr.operconstr {G.pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]} + Pcoq.grammar_extend Pcoq.Constr.operconstr {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]} end } diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index ab660b486e..2ed854c9f7 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1431,7 +1431,7 @@ let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) let add_generic_scope s entry arg = let parse = function | [] -> - let scope = Pcoq.G.Symbol.nterm entry in + let scope = Pcoq.Symbol.nterm entry in let act x = CAst.make @@ CTacExt (arg, x) in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail s arg @@ -1442,14 +1442,14 @@ open CAst let () = add_scope "keyword" begin function | [SexprStr {loc;v=s}] -> - let scope = Pcoq.G.Symbol.token (Tok.PKEYWORD s) in + let scope = Pcoq.Symbol.token (Tok.PKEYWORD s) in Tac2entries.ScopeRule (scope, (fun _ -> q_unit)) | arg -> scope_fail "keyword" arg end let () = add_scope "terminal" begin function | [SexprStr {loc;v=s}] -> - let scope = Pcoq.G.Symbol.token (CLexer.terminal s) in + let scope = Pcoq.Symbol.token (CLexer.terminal s) in Tac2entries.ScopeRule (scope, (fun _ -> q_unit)) | arg -> scope_fail "terminal" arg end @@ -1457,13 +1457,13 @@ end let () = add_scope "list0" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let scope = Pcoq.G.Symbol.list0 scope in + let scope = Pcoq.Symbol.list0 scope in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | [tok; SexprStr {v=str}] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in - let scope = Pcoq.G.Symbol.list0sep scope sep false in + let sep = Pcoq.Symbol.token (CLexer.terminal str) in + let scope = Pcoq.Symbol.list0sep scope sep false in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "list0" arg @@ -1472,13 +1472,13 @@ end let () = add_scope "list1" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let scope = Pcoq.G.Symbol.list1 scope in + let scope = Pcoq.Symbol.list1 scope in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | [tok; SexprStr {v=str}] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let sep = Pcoq.G.Symbol.token (CLexer.terminal str) in - let scope = Pcoq.G.Symbol.list1sep scope sep false in + let sep = Pcoq.Symbol.token (CLexer.terminal str) in + let scope = Pcoq.Symbol.list1sep scope sep false in let act l = Tac2quote.of_list act l in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "list1" arg @@ -1487,7 +1487,7 @@ end let () = add_scope "opt" begin function | [tok] -> let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in - let scope = Pcoq.G.Symbol.opt scope in + let scope = Pcoq.Symbol.opt scope in let act opt = match opt with | None -> CAst.make @@ CTacCst (AbsKn (Other Core.c_none)) @@ -1500,7 +1500,7 @@ end let () = add_scope "self" begin function | [] -> - let scope = Pcoq.G.Symbol.self in + let scope = Pcoq.Symbol.self in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "self" arg @@ -1508,7 +1508,7 @@ end let () = add_scope "next" begin function | [] -> - let scope = Pcoq.G.Symbol.next in + let scope = Pcoq.Symbol.next in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "next" arg @@ -1517,12 +1517,12 @@ end let () = add_scope "tactic" begin function | [] -> (* Default to level 5 parsing *) - let scope = Pcoq.G.Symbol.nterml tac2expr "5" in + let scope = Pcoq.Symbol.nterml tac2expr "5" in let act tac = tac in Tac2entries.ScopeRule (scope, act) | [SexprInt {loc;v=n}] as arg -> let () = if n < 0 || n > 6 then scope_fail "tactic" arg in - let scope = Pcoq.G.Symbol.nterml tac2expr (string_of_int n) in + let scope = Pcoq.Symbol.nterml tac2expr (string_of_int n) in let act tac = tac in Tac2entries.ScopeRule (scope, act) | arg -> scope_fail "tactic" arg @@ -1543,12 +1543,12 @@ let () = add_scope "constr" (fun arg -> arg in let act e = Tac2quote.of_constr ~delimiters e in - Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm Pcoq.Constr.constr, act) + Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) ) let add_expr_scope name entry f = add_scope name begin function - | [] -> Tac2entries.ScopeRule (Pcoq.G.Symbol.nterm entry, f) + | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f) | arg -> scope_fail name arg end @@ -1590,21 +1590,21 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu) type seqrule = -| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule +| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) Rule.t * 'act converter -> seqrule let rec make_seq_rule = function | [] -> - Seqrule (Pcoq.G.Rule.stop, CvNil) + Seqrule (Pcoq.Rule.stop, CvNil) | tok :: rem -> let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in let scope = - match Pcoq.G.generalize_symbol scope with + match Pcoq.generalize_symbol scope with | None -> CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules") | Some scope -> scope in let Seqrule (r, c) = make_seq_rule rem in - let r = Pcoq.G.Rule.next_norec r scope in + let r = Pcoq.Rule.next_norec r scope in let f = match tok with | SexprStr _ -> None (* Leave out mere strings *) | _ -> Some f @@ -1614,7 +1614,7 @@ let rec make_seq_rule = function let () = add_scope "seq" begin fun toks -> let scope = let Seqrule (r, c) = make_seq_rule (List.rev toks) in - Pcoq.G.(Symbol.rules [Rules.make r (apply c [])]) + Pcoq.(Symbol.rules [Rules.make r (apply c [])]) in Tac2entries.ScopeRule (scope, (fun e -> e)) end diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 7c4971db8c..ebc63ddd01 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -558,7 +558,7 @@ type 'a token = | TacNonTerm of Name.t * 'a type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule @@ -583,7 +583,7 @@ let parse_scope = function CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id) | SexprStr {v=str} -> let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in - ScopeRule (Pcoq.G.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit)) + ScopeRule (Pcoq.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit)) | tok -> let loc = loc_of_token tok in CErrors.user_err ?loc (str "Invalid parsing token") @@ -611,19 +611,19 @@ type synext = { type krule = | KRule : - (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.G.Rule.t * + (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.Rule.t * ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule let rec get_rule (tok : scope_rule token list) : krule = match tok with -| [] -> KRule (Pcoq.G.Rule.stop, fun k loc -> k loc []) +| [] -> KRule (Pcoq.Rule.stop, fun k loc -> k loc []) | TacNonTerm (na, ScopeRule (scope, inj)) :: tok -> let KRule (rule, act) = get_rule tok in - let rule = Pcoq.G.Rule.next rule scope in + let rule = Pcoq.Rule.next rule scope in let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in KRule (rule, act) | TacTerm t :: tok -> let KRule (rule, act) = get_rule tok in - let rule = Pcoq.G.(Rule.next rule (Symbol.token (CLexer.terminal t))) in + let rule = Pcoq.(Rule.next rule (Symbol.token (CLexer.terminal t))) in let act k _ = act k in KRule (rule, act) @@ -637,13 +637,13 @@ let perform_notation syn st = let bnd = List.map map args in CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp) in - let rule = Pcoq.G.Production.make rule (act mk) in + let rule = Pcoq.Production.make rule (act mk) in let lev = match syn.synext_lev with | None -> None | Some lev -> Some (string_of_int lev) in let rule = (lev, None, [rule]) in - ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.G.pos=None; data=[rule]})], st) + ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.pos=None; data=[rule]})], st) let ltac2_notation = Pcoq.create_grammar_command "ltac2-notation" perform_notation diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index 1efac697aa..edad118dc9 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit (** {5 Notations} *) type scope_rule = -| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule +| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule type scope_interpretation = sexpr list -> scope_rule diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index c4f15a40ce..fdc8b1ba4c 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -326,47 +326,47 @@ let is_binder_level custom (custom',from) e = match e with let make_sep_rules = function | [tk] -> - Pcoq.G.Symbol.token tk + Pcoq.Symbol.token tk | tkl -> - let r = Pcoq.G.mk_rule (List.rev tkl) in - Pcoq.G.Symbol.rules [r] + let r = Pcoq.mk_rule (List.rev tkl) in + Pcoq.Symbol.rules [r] type ('s, 'a) mayrec_symbol = -| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol -| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol +| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol +| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> if is_binder_level custom from p then (* Prevent self *) - MayRecNo (Pcoq.G.Symbol.nterml (target_entry custom forpat) "200") - else if is_self custom from p then MayRecMay Pcoq.G.Symbol.self + MayRecNo (Pcoq.Symbol.nterml (target_entry custom forpat) "200") + else if is_self custom from p then MayRecMay Pcoq.Symbol.self else let g = target_entry custom forpat in let lev = adjust_level custom assoc from p in begin match lev with - | DefaultLevel -> MayRecNo (Pcoq.G.Symbol.nterm g) - | NextLevel -> MayRecMay Pcoq.G.Symbol.next - | NumLevel lev -> MayRecNo (Pcoq.G.Symbol.nterml g (string_of_int lev)) + | DefaultLevel -> MayRecNo (Pcoq.Symbol.nterm g) + | NextLevel -> MayRecMay Pcoq.Symbol.next + | NumLevel lev -> MayRecNo (Pcoq.Symbol.nterml g (string_of_int lev)) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat | TTConstrList (s, typ', [], forpat) -> begin match symbol_of_target s typ' assoc from forpat with - | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1 s) - | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1 s) end + | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s) + | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end | TTConstrList (s, typ', tkl, forpat) -> begin match symbol_of_target s typ' assoc from forpat with - | MayRecNo s -> MayRecNo (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) - | MayRecMay s -> MayRecMay (Pcoq.G.Symbol.list1sep s (make_sep_rules tkl) false) end -| TTPattern p -> MayRecNo (Pcoq.G.Symbol.nterml Constr.pattern (string_of_int p)) -| TTClosedBinderList [] -> MayRecNo (Pcoq.G.Symbol.list1 (Pcoq.G.Symbol.nterm Constr.binder)) -| TTClosedBinderList tkl -> MayRecNo (Pcoq.G.Symbol.list1sep (Pcoq.G.Symbol.nterm Constr.binder) (make_sep_rules tkl) false) -| TTName -> MayRecNo (Pcoq.G.Symbol.nterm Prim.name) -| TTOpenBinderList -> MayRecNo (Pcoq.G.Symbol.nterm Constr.open_binders) -| TTBigint -> MayRecNo (Pcoq.G.Symbol.nterm Prim.bignat) -| TTReference -> MayRecNo (Pcoq.G.Symbol.nterm Constr.global) + | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) + | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end +| TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p)) +| TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder)) +| TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false) +| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name) +| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders) +| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat) +| TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName @@ -458,22 +458,22 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> ty_eval rem f { env with constrs; constrlists; } type ('s, 'a, 'r) mayrec_rule = -| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule -| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule +| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule +| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function -| TyStop -> MayRecRNo G.Rule.stop +| TyStop -> MayRecRNo Rule.stop | TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> begin match ty_erase rem with - | MayRecRNo rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) - | MayRecRMay rem -> MayRecRMay (G.Rule.next rem (G.Symbol.token tok)) end + | MayRecRNo rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) + | MayRecRMay rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) end | TyNext (rem, TyNonTerm (_, _, s, _)) -> begin match ty_erase rem, s with - | MayRecRNo rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s) - | MayRecRNo rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) - | MayRecRMay rem, MayRecNo s -> MayRecRMay (G.Rule.next rem s) - | MayRecRMay rem, MayRecMay s -> MayRecRMay (G.Rule.next rem s) end + | MayRecRNo rem, MayRecNo s -> MayRecRMay (Rule.next rem s) + | MayRecRNo rem, MayRecMay s -> MayRecRMay (Rule.next rem s) + | MayRecRMay rem, MayRecNo s -> MayRecRMay (Rule.next rem s) + | MayRecRMay rem, MayRecMay s -> MayRecRMay (Rule.next rem s) end type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule @@ -501,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function | ForPattern -> true let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = - let empty = { G.pos; data = [(name, p4assoc, [])] } in + let empty = { pos; data = [(name, p4assoc, [])] } in match reinit with | None -> ExtendRule (target_entry where forpat, empty) @@ -520,7 +520,7 @@ let rec pure_sublevels' assoc from forpat level = function let push where p rem = match symbol_of_target where p assoc from forpat with | MayRecNo sym -> - (match Pcoq.G.level_of_nonterm sym with + (match Pcoq.level_of_nonterm sym with | None -> rem | Some i -> if different_levels (fst from,level) (where,i) then @@ -556,15 +556,15 @@ let extend_constr state forpat ng = let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = let r = match ty_erase r with - | MayRecRNo symbs -> Pcoq.G.Production.make symbs act - | MayRecRMay symbs -> Pcoq.G.Production.make symbs act + | MayRecRNo symbs -> Pcoq.Production.make symbs act + | MayRecRMay symbs -> Pcoq.Production.make symbs act in name, p4assoc, [r] in let r = match reinit with | None -> - ExtendRule (entry, { G.pos; data = [rule]}) + ExtendRule (entry, { pos; data = [rule]}) | Some reinit -> - ExtendRuleReinit (entry, reinit, { G.pos; data = [rule]}) + ExtendRuleReinit (entry, reinit, { pos; data = [rule]}) in (accu @ empty_rules @ [r], state) in diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 981de78162..bda1401bc9 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -19,13 +19,13 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - ('a raw_abstract_argument_type * ('s, _, 'a) G.Symbol.t) Loc.located -> 's grammar_prod_item + ('a raw_abstract_argument_type * ('s, _, 'a) Symbol.t) Loc.located -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) type ('self, 'tr, _, 'r) ty_rule = | TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule -| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) G.Symbol.t * 'b ty_arg option -> +| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Symbol.t * 'b ty_arg option -> ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule type ('self, 'r) any_ty_rule = @@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function | [] -> AnyTyRule TyStop | GramTerminal s :: rem -> let AnyTyRule rem = ty_rule_of_gram rem in - let tok = Pcoq.G.Symbol.token (CLexer.terminal s) in + let tok = Pcoq.Symbol.token (CLexer.terminal s) in let r = TyNext (rem, tok, None) in AnyTyRule r | GramNonTerminal (_, (t, tok)) :: rem -> @@ -44,9 +44,9 @@ let rec ty_rule_of_gram = function let r = TyNext (rem, tok, inj) in AnyTyRule r -let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.G.Rule.t = function -| TyStop -> Pcoq.G.Rule.stop -| TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok +let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.Rule.t = function +| TyStop -> Pcoq.Rule.stop +| TyNext (rem, tok, _) -> Pcoq.Rule.next (ty_erase rem) tok type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r @@ -62,7 +62,7 @@ let make_rule f prod = let symb = ty_erase ty_rule in let f loc l = f loc (List.rev l) in let act = ty_eval ty_rule f in - Pcoq.G.Production.make symb act + Pcoq.Production.make symb act let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function | TUentry a -> ExtraArg a @@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl = vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in - grammar_extend nt { G.pos=None; data=[None, None, rules]} + grammar_extend nt { pos=None; data=[None, None, rules]} diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 77198452b9..15f415ca3b 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -18,7 +18,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * - ('s, _, 'a) Pcoq.G.Symbol.t) Loc.located -> 's grammar_prod_item + ('s, _, 'a) Pcoq.Symbol.t) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : extend_name -> vernac_expr Pcoq.Entry.t option -> @@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Pcoq.G.Production.t + 'a grammar_prod_item list -> 'a Pcoq.Production.t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 38e57a310a..475d5c31f7 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -46,7 +46,7 @@ let entry_buf = Buffer.create 64 let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in - let () = Pcoq.G.Entry.print ft e in + let () = Pcoq.Entry.print ft e in str (Buffer.contents entry_buf) let pr_registered_grammar name = @@ -55,7 +55,7 @@ let pr_registered_grammar name = | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.") | entries -> let pr_one (Pcoq.AnyEntry e) = - str "Entry " ++ str (Pcoq.G.Entry.name e) ++ str " is" ++ fnl () ++ + str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e in prlist pr_one entries diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 8d0dcbf0fe..2130a398e9 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -169,7 +169,7 @@ let suggest_variable env id = let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let using_from_string us = Pcoq.G.Entry.parse G_vernac.section_subset_expr (Pcoq.G.Parsable.make (Stream.of_string us)) +let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) let proof_using_opt_name = ["Default";"Proof";"Using"] let () = diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 26364ed075..f4cb1adfe8 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -54,10 +54,10 @@ module Vernac_ = let act_vernac v loc = Some v in let act_eoi _ loc = None in let rule = [ - Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi); - Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac); + Pcoq.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi); + Pcoq.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac); ] in - Pcoq.(grammar_extend main_entry {G.pos=None; data=[None, None, rule]}) + Pcoq.(grammar_extend main_entry {pos=None; data=[None, None, rule]}) let select_tactic_entry spec = match spec with @@ -65,8 +65,8 @@ module Vernac_ = | Some ename -> find_proof_mode ename let command_entry = - Pcoq.G.Entry.of_parser "command_entry" - (fun _ strm -> Pcoq.G.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) + Pcoq.Entry.of_parser "command_entry" + (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) end diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 4008c3d799..1920c276af 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -166,15 +166,15 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c | Some Refl -> untype_command ty (f v) args end -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.G.Symbol.t = +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.Symbol.t = let open Extend in function - | TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l) - | TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false - | TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l) - | TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false - | TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o) - | TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a)) - | TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i) + | TUlist1 l -> Pcoq.Symbol.list1 (untype_user_symbol l) + | TUlist1sep (l, s) -> Pcoq.Symbol.list1sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false + | TUlist0 l -> Pcoq.Symbol.list0 (untype_user_symbol l) + | TUlist0sep (l, s) -> Pcoq.Symbol.list0sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false + | TUopt o -> Pcoq.Symbol.opt (untype_user_symbol o) + | TUentry a -> Pcoq.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a)) + | TUentryl (a, i) -> Pcoq.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i) let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function | TyNil -> [] @@ -193,7 +193,7 @@ let vernac_extend ~command ?classifier ?entry ext = | None -> let e = match entry with | None -> "COMMAND" - | Some e -> Pcoq.G.Entry.name e + | Some e -> Pcoq.Entry.name e in let msg = Printf.sprintf "\ Vernac entry \"%s\" misses a classifier. \ @@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext = type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Pcoq.G.Production.t list +| Arg_rules of 'a Pcoq.Production.t list type 'a vernac_argument = { arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t; @@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg = e | Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e {Pcoq.G.pos=None; data=[(None, None, rules)]} in + let () = Pcoq.grammar_extend e {Pcoq.pos=None; data=[(None, None, rules)]} in e in let pr = arg.arg_printer in diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4d9537b6ff..0d0ebc1086 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -111,7 +111,7 @@ type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t (** This is used because CAMLP5 parser can be dumb about rule factorization, which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Pcoq.G.Production.t list +| Arg_rules of 'a Pcoq.Production.t list (** There is a discrepancy here as we use directly extension rules and thus entries instead of ty_user_symbol and thus arguments as roots. *) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 6b7b2c2691..15a19c06c2 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -183,12 +183,12 @@ and vernac_load ~verbosely fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = Util.open_utf8_file_in longfname in - Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in + Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in (* Parsing loop *) let v_mod = if verbosely then Flags.verbosely else Flags.silently in let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.G.Entry.parse (Pvernac.main_entry proof_mode) po with + match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with | Some x -> x | None -> raise End_of_input) in let rec load_loop ~stack = diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 49486b889d..6846826bfa 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -19,7 +19,7 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; Flags.with_option Flags.we_are_parsing - (fun () -> Pcoq.G.Entry.parse entry pa) + (fun () -> Pcoq.Entry.parse entry pa) () end diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index ed1b76b618..7607f8373a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -14,7 +14,7 @@ module Parser : sig val init : unit -> state val cur_state : unit -> state - val parse : state -> 'a Pcoq.Entry.t -> Pcoq.G.Parsable.t -> 'a + val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a end -- cgit v1.2.3 From 5c9f318f5f1b6e85b03bba9450ac059377be54fc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Mar 2020 07:21:27 -0400 Subject: [gramlib] Don't expose unsafe interfaces to clients I'd say this is more of a temporary measure than a long-term plan; IMO we should make the interfaces safe so `Gramlib.Grammar` does provide only one signature. --- gramlib/grammar.ml | 20 +++++++++++++------- gramlib/grammar.mli | 25 +++++++++++++++++-------- 2 files changed, 30 insertions(+), 15 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 41669b77c9..d6951fff6d 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -77,10 +77,6 @@ module type S = sig val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t end - module Unsafe : sig - val clear_entry : 'a Entry.t -> unit - end - type 'a single_extend_statement = string option * Gramext.g_assoc option * 'a Production.t list @@ -89,9 +85,6 @@ module type S = sig ; data : 'a single_extend_statement list } - val safe_extend : 'a Entry.t -> 'a extend_statement -> unit - val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit - val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option val mk_rule : 'a pattern list -> string Rules.t @@ -101,6 +94,19 @@ module type S = sig end +module type ExtS = sig + + include S + + val safe_extend : 'a Entry.t -> 'a extend_statement -> unit + val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit + + module Unsafe : sig + val clear_entry : 'a Entry.t -> unit + end + +end + (* Implementation *) module GMake (L : Plexing.S) = struct diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 6f998f7b80..33006f6f65 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -87,10 +87,6 @@ module type S = sig val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t end - module Unsafe : sig - val clear_entry : 'a Entry.t -> unit - end - type 'a single_extend_statement = string option * Gramext.g_assoc option * 'a Production.t list @@ -99,16 +95,29 @@ module type S = sig ; data : 'a single_extend_statement list } - val safe_extend : 'a Entry.t -> 'a extend_statement -> unit - val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit - val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option val mk_rule : 'a pattern list -> string Rules.t (* Used in custom entries, should tweak? *) val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option + +end + +(* Interface private to clients *) +module type ExtS = sig + + include S + + val safe_extend : 'a Entry.t -> 'a extend_statement -> unit + val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit + + module Unsafe : sig + val clear_entry : 'a Entry.t -> unit + end + end + (** Signature type of the functor [Grammar.GMake]. The types and functions are almost the same than in generic interface, but: - Grammars are not values. Functions holding a grammar as parameter @@ -119,4 +128,4 @@ end type (instead of (string * string)); the module parameter must specify a way to show them as (string * string) *) -module GMake (L : Plexing.S) : S with type te = L.te and type 'c pattern = 'c L.pattern +module GMake (L : Plexing.S) : ExtS with type te = L.te and type 'c pattern = 'c L.pattern -- cgit v1.2.3