diff options
| -rw-r--r-- | coqpp/coqpp_main.ml | 15 | ||||
| -rw-r--r-- | gramlib/grammar.ml | 10 | ||||
| -rw-r--r-- | gramlib/grammar.mli | 2 | ||||
| -rw-r--r-- | gramlib/plexing.ml | 2 | ||||
| -rw-r--r-- | gramlib/plexing.mli | 2 | ||||
| -rw-r--r-- | parsing/cLexer.ml | 30 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 2 | ||||
| -rw-r--r-- | parsing/extend.ml | 6 | ||||
| -rw-r--r-- | parsing/notation_gram.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 19 | ||||
| -rw-r--r-- | parsing/tok.ml | 60 | ||||
| -rw-r--r-- | parsing/tok.mli | 15 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 8 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 9 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 |
15 files changed, 78 insertions, 106 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 90158c3aa3..c8a87e6cb6 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -212,17 +212,9 @@ let print_fun fmt (vars, body) = (** Meta-program instead of calling Tok.of_pattern here because otherwise violates value restriction *) -let print_tok fmt = function -| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s -| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s -| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s -| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s -| "INT", s -> fprintf fmt "Tok.INT %a" print_string s -| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s -| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK" -| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s -| "EOI", _ -> fprintf fmt "Tok.EOI" -| _ -> failwith "Tok.of_pattern: not a constructor" +let print_tok fmt (k,o) = + let print_pat fmt = print_opt fmt print_string in + fprintf fmt "(%a,%a)" print_string k print_pat o let rec print_prod fmt p = let (vars, tkns) = List.split p.gprod_symbs in @@ -240,7 +232,6 @@ and print_symbols fmt = function and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> - let s = match s with None -> "" | Some s -> s in fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) | SymbEntry (e, None) -> fprintf fmt "(Extend.Aentry %s)" e diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 74350c4f15..9eebe7a1e2 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -16,7 +16,7 @@ module type S = type te type parsable val parsable : ?loc:Loc.t -> char Stream.t -> parsable - val tokens : string -> (string * int) list + val tokens : string -> (string option * int) list module Entry : sig type 'a e @@ -195,7 +195,7 @@ let is_before : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bo match s1, s2 with Stoken ("ANY", _), _ -> false | _, Stoken ("ANY", _) -> true - | Stoken (_, s), Stoken (_, "") when s <> "" -> true + | Stoken (_, Some _), Stoken (_, None) -> true | Stoken _, Stoken _ -> false | Stoken _, _ -> true | _ -> false @@ -683,7 +683,7 @@ let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit = fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t (if osep then " OPT_SEP" else "") | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s - | Stoken (con, prm) when con <> "" && prm <> "" -> + | Stoken (con, Some prm) when con <> "" -> fprintf ppf "%s@ %a" con print_str prm | Snterml (e, l) -> fprintf ppf "%s%s@ LEVEL@ %a" e.ename "" @@ -695,8 +695,8 @@ and print_symbol1 : type s r. formatter -> (s, r) ty_symbol -> unit = | Snterm e -> fprintf ppf "%s%s" e.ename "" | Sself -> pp_print_string ppf "SELF" | Snext -> pp_print_string ppf "NEXT" - | Stoken ("", s) -> print_str ppf s - | Stoken (con, "") -> pp_print_string ppf con + | Stoken ("", Some s) -> print_str ppf s + | Stoken (con, None) -> pp_print_string ppf con | Stree t -> print_level ppf pp_print_space (flatten_tree t) | s -> fprintf ppf "(%a)" print_symbol s diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 7cb7a92f85..453ec85187 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -24,7 +24,7 @@ module type S = type te type parsable val parsable : ?loc:Loc.t -> char Stream.t -> parsable - val tokens : string -> (string * int) list + val tokens : string -> (string option * int) list module Entry : sig type 'a e diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index c294923a85..6da06f147f 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -2,7 +2,7 @@ (* plexing.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -type pattern = string * string +type pattern = string * string option type location_function = int -> Loc.t type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index f6e4d96b80..48722e01be 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -8,7 +8,7 @@ grammars (see module [Grammar]). It also provides some useful functions to create lexers. *) -type pattern = string * string +type pattern = string * string option (* Type for values used by the generated code of the EXTEND statement to represent terminals in entry rules. - The first string is the constructor name (must start with diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index 503cfcdb4f..7345afb307 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -740,15 +740,15 @@ type te = Tok.t (** Names of tokens, for this lexer, used in Grammar error messages *) let token_text = function - | ("", t) -> "'" ^ t ^ "'" - | ("IDENT", "") -> "identifier" - | ("IDENT", t) -> "'" ^ t ^ "'" - | ("INT", "") -> "integer" - | ("INT", s) -> "'" ^ s ^ "'" - | ("STRING", "") -> "string" - | ("EOI", "") -> "end of input" - | (con, "") -> con - | (con, prm) -> con ^ " \"" ^ prm ^ "\"" + | ("", Some t) -> "'" ^ t ^ "'" + | ("IDENT", None) -> "identifier" + | ("IDENT", Some t) -> "'" ^ t ^ "'" + | ("INT", None) -> "integer" + | ("INT", Some s) -> "'" ^ s ^ "'" + | ("STRING", None) -> "string" + | ("EOI", None) -> "end of input" + | (con, None) -> con + | (con, Some prm) -> con ^ " \"" ^ prm ^ "\"" let func next_token ?loc cs = let loct = loct_create () in @@ -765,9 +765,9 @@ let func next_token ?loc cs = let make_lexer ~diff_mode = { Plexing.tok_func = func (next_token ~diff_mode); Plexing.tok_using = - (fun pat -> match Tok.of_pattern pat with - | KEYWORD s -> add_keyword s - | _ -> ()); + (fun pat -> match Tok.is_keyword pat with + | Some s -> add_keyword s + | None -> ()); Plexing.tok_removing = (fun _ -> ()); Plexing.tok_match = Tok.match_pattern; Plexing.tok_text = token_text } @@ -807,6 +807,6 @@ let strip s = let terminal s = let s = strip s in let () = match s with "" -> failwith "empty token." | _ -> () in - if is_ident_not_keyword s then IDENT s - else if is_number s then INT s - else KEYWORD s + if is_ident_not_keyword s then "IDENT", Some s + else if is_number s then "INT", Some s + else "", Some s diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 807f37a1a4..662f6a477d 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -21,7 +21,7 @@ val get_keyword_state : unit -> keyword_state val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit -val terminal : string -> Tok.t +val terminal : string -> Tok.pattern (** The lexer of Coq: *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 9b5537d7f6..ff879dd1c2 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -44,7 +44,7 @@ type simple_constr_prod_entry_key = (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) -type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.pattern list type binder_target = ForBinder | ForTerm @@ -54,7 +54,7 @@ type constr_prod_entry_key = | ETProdBigint (* Parsed as an (unbounded) integer *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) - | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdConstrList of (production_level * production_position) * Tok.pattern list (* Parsed as non-empty list of constr *) | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) (** {5 AST for user-provided entries} *) @@ -80,7 +80,7 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = -| Atoken : Tok.t -> ('self, string) symbol +| Atoken : Tok.pattern -> ('self, string) symbol | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index fc5feba58b..a50f8d69e3 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -21,7 +21,7 @@ type level = Constrexpr.notation_entry * precedence * tolerability list * constr (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t + | GramConstrTerminal of Tok.pattern | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option | GramConstrListMark of int * bool * int (* tells action rule to make a list of the n previous parsed items; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9241205755..f2f5d17da3 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -119,25 +119,10 @@ struct end module Symbols : sig - val stoken : Tok.t -> ('s, string) G.ty_symbol val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol end = struct - let stoken tok = - let pattern = match tok with - | Tok.KEYWORD s -> "", s - | Tok.IDENT s -> "IDENT", s - | Tok.PATTERNIDENT s -> "PATTERNIDENT", s - | Tok.FIELD s -> "FIELD", s - | Tok.INT s -> "INT", s - | Tok.STRING s -> "STRING", s - | Tok.LEFTQMARK -> "LEFTQMARK", "" - | Tok.BULLET s -> "BULLET", s - | Tok.EOI -> "EOI", "" - in - G.s_token pattern - let slist0sep x y = G.s_list0sep x y false let slist1sep x y = G.s_list1sep x y false end @@ -158,7 +143,7 @@ end type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function -| Atoken t -> Symbols.stoken t +| Atoken t -> G.s_token t | Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s) | Alist1sep (s,sep) -> Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) @@ -303,7 +288,7 @@ let make_rule r = [None, None, r] let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in - let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in + let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (G.s_token Tok.pattern_for_EOI) 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 (symbs, act)]); diff --git a/parsing/tok.ml b/parsing/tok.ml index 03825e350f..ba249bd977 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -82,41 +82,31 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok) (** For camlp5, conversion from/to [Plexing.pattern], and a match function analoguous to [Plexing.default_match] *) -let of_pattern = function - | "", s -> KEYWORD s - | "IDENT", s -> IDENT s - | "PATTERNIDENT", s -> PATTERNIDENT s - | "FIELD", s -> FIELD s - | "INT", s -> INT s - | "STRING", s -> STRING s - | "LEFTQMARK", _ -> LEFTQMARK - | "BULLET", s -> BULLET s - | "EOI", _ -> EOI - | _ -> failwith "Tok.of_pattern: not a constructor" +type pattern = string * string option -let to_pattern = function - | KEYWORD s -> "", s - | IDENT s -> "IDENT", s - | PATTERNIDENT s -> "PATTERNIDENT", s - | FIELD s -> "FIELD", s - | INT s -> "INT", s - | STRING s -> "STRING", s - | LEFTQMARK -> "LEFTQMARK", "" - | BULLET s -> "BULLET", s - | EOI -> "EOI", "" +let is_keyword = function + | "", Some s -> Some s + | _ -> None -let match_pattern = +let pattern_for_EOI = ("EOI",None) +let pattern_for_KEYWORD s = ("",Some s) +let pattern_for_IDENT s = ("IDENT",Some s) + +let match_pattern (key, value) = let err () = raise Stream.Failure in - function - | "", "" -> (function KEYWORD s -> s | _ -> err ()) - | "IDENT", "" -> (function IDENT s -> s | _ -> err ()) - | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ()) - | "FIELD", "" -> (function FIELD s -> s | _ -> err ()) - | "INT", "" -> (function INT s -> s | _ -> err ()) - | "STRING", "" -> (function STRING s -> s | _ -> err ()) - | "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ()) - | "BULLET", "" -> (function BULLET s -> s | _ -> err ()) - | "EOI", "" -> (function EOI -> "" | _ -> err ()) - | pat -> - let tok = of_pattern pat in - function tok' -> if equal tok tok' then snd pat else err () + let cond x = + match value with + | None -> x + | Some value -> if string_equal value x then x else err () in + match key with + | "" -> (function { v = KEYWORD s } -> cond s | _ -> err ()) + | "IDENT" when value <> None -> (function { v = (IDENT s | KEYWORD s) } -> cond s | _ -> err ()) + | "IDENT" -> (function { v = IDENT s } -> cond s | _ -> err ()) + | "PATTERNIDENT" -> (function { v = PATTERNIDENT s } -> cond s | _ -> err ()) + | "FIELD" -> (function { v = FIELD s } -> cond s | _ -> err ()) + | "INT" -> (function { v = INT s } -> cond s | _ -> err ()) + | "STRING" -> (function { v = STRING s } -> cond s | _ -> err ()) + | "LEFTQMARK" -> (function { v = LEFTQMARK } -> cond "" | _ -> err ()) + | "BULLET" -> (function { v = BULLET s } -> cond s | _ -> err ()) + | "EOI" -> (function { v = EOI } -> cond "" | _ -> err ()) + | p -> CErrors.anomaly Pp.(str "Tok: unknown pattern " ++ str p) diff --git a/parsing/tok.mli b/parsing/tok.mli index 5750096a28..e32047e6ec 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -29,7 +29,14 @@ val to_string : t -> string val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool -(** for camlp5 *) -val of_pattern : string*string -> t -val to_pattern : t -> string*string -val match_pattern : string*string -> t -> string +(** for camlp5, + eg GRAMMAR EXTEND ..... [ IDENT "x" -> .... END + is a pattern ("IDENT", Some "x") +*) +type pattern = string * string option (* = Plexing.pattern *) + +val is_keyword : pattern -> string option +val pattern_for_EOI : pattern +val pattern_for_KEYWORD : string -> pattern +val pattern_for_IDENT : string -> pattern +val match_pattern : pattern -> t -> string diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 1a07d74a0e..f96b567f1b 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -247,10 +247,10 @@ type (_, _) entry = | TTReference : ('self, qualid) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry -| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry +| TTConstrList : prod_info * Tok.pattern list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry | TTOpenBinderList : ('self, local_binder_expr list) entry -| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry +| TTClosedBinderList : Tok.pattern list -> ('self, local_binder_expr list list) entry type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry @@ -319,7 +319,7 @@ let is_binder_level from e = match e with let make_sep_rules = function | [tk] -> Atoken tk | tkl -> - let rec mkrule : Tok.t list -> string rules = function + let rec mkrule : Tok.pattern list -> string rules = function | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "") | tkn :: rem -> let Rules ({ norec_rule = r }, f) = mkrule rem in @@ -406,7 +406,7 @@ match e with | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } type (_, _) ty_symbol = -| TyTerm : Tok.t -> ('s, string) ty_symbol +| TyTerm : Tok.pattern -> ('s, string) ty_symbol | TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol type ('self, _, 'r) ty_rule = diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 3da12e7714..781fd404f8 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -23,7 +23,6 @@ open Libobject open Constrintern open Vernacexpr open Libnames -open Tok open Notation open Nameops @@ -575,20 +574,20 @@ let is_not_small_constr = function | _ -> false let rec define_keywords_aux = function - | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l + | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",Some k) :: l when is_not_small_constr e -> Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; - n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l + n1 :: GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function - | GramConstrTerminal(IDENT k)::l -> + | GramConstrTerminal("IDENT", Some k)::l -> Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; - GramConstrTerminal(KEYWORD k) :: define_keywords_aux l + GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l let distribute a ll = List.map (fun l -> a @ l) ll diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 994fad85f0..9438b9749f 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -55,7 +55,7 @@ module Vernac_ = let act_vernac v loc = Some CAst.(make ~loc v) in let act_eoi _ loc = None in let rule = [ - Rule (Next (Stop, Atoken Tok.EOI), act_eoi); + Rule (Next (Stop, Atoken Tok.pattern_for_EOI), act_eoi); Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in Pcoq.grammar_extend main_entry None (None, [None, None, rule]) |