diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml | 63 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 25 | ||||
| -rw-r--r-- | parsing/extend.ml | 50 | ||||
| -rw-r--r-- | parsing/notation_gram.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 104 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/tok.ml | 117 | ||||
| -rw-r--r-- | parsing/tok.mli | 30 |
8 files changed, 215 insertions, 178 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index 33890545da..b81d89edf9 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -790,20 +790,25 @@ let loct_add loct i loc = Hashtbl.add loct i loc we unfreeze the state of the lexer. This restores the behaviour of the lexer. B.B. *) -type te = Tok.t - (** Names of tokens, for this lexer, used in Grammar error messages *) -let token_text = function - | ("", 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 token_text : type c. c Tok.p -> string = function + | PKEYWORD t -> "'" ^ t ^ "'" + | PIDENT None -> "identifier" + | PIDENT (Some t) -> "'" ^ t ^ "'" + | PINT None -> "integer" + | PINT (Some s) -> "'" ^ s ^ "'" + | PSTRING None -> "string" + | PSTRING (Some s) -> "STRING \"" ^ s ^ "\"" + | PLEFTQMARK -> "LEFTQMARK" + | PEOI -> "end of input" + | PPATTERNIDENT None -> "PATTERNIDENT" + | PPATTERNIDENT (Some s) -> "PATTERNIDENT \"" ^ s ^ "\"" + | PFIELD None -> "FIELD" + | PFIELD (Some s) -> "FIELD \"" ^ s ^ "\"" + | PBULLET None -> "BULLET" + | PBULLET (Some s) -> "BULLET \"" ^ s ^ "\"" + | PQUOTATION lbl -> "QUOTATION \"" ^ lbl ^ "\"" let func next_token ?loc cs = let loct = loct_create () in @@ -817,18 +822,24 @@ let func next_token ?loc cs = in (ts, loct_func loct) -let make_lexer ~diff_mode = { - Plexing.tok_func = func (next_token ~diff_mode); - Plexing.tok_using = - (fun pat -> match Tok.is_keyword pat with - | Some (false,s) -> add_keyword ~quotation:NoQuotation s - | Some (true,s) -> add_keyword ~quotation:Quotation s - | None -> ()); - Plexing.tok_removing = (fun _ -> ()); - Plexing.tok_match = Tok.match_pattern; - Plexing.tok_text = token_text } +module MakeLexer (Diff : sig val mode : bool end) = struct + type te = Tok.t + type 'c pattern = 'c Tok.p + let tok_pattern_eq = Tok.equal_p + let tok_pattern_strings = Tok.pattern_strings + let tok_func = func (next_token ~diff_mode:Diff.mode) + let tok_using : type c. c pattern -> unit = function + | PKEYWORD s -> add_keyword ~quotation:NoQuotation s + | PQUOTATION s -> add_keyword ~quotation:Quotation s + | _ -> () + let tok_removing = (fun _ -> ()) + let tok_match = Tok.match_pattern + let tok_text = token_text +end + +module Lexer = MakeLexer (struct let mode = false end) -let lexer = make_lexer ~diff_mode:false +module LexerDiff = MakeLexer (struct let mode = true end) (** Terminal symbols interpretation *) @@ -863,6 +874,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", Some s - else if is_number s then "INT", Some s - else "", Some s + if is_ident_not_keyword s then PIDENT (Some s) + else if is_number s then PINT (Some s) + else PKEYWORD s diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 6d5a621877..9df3e45f49 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -45,26 +45,14 @@ 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.pattern -(** The lexer of Coq: *) - -(* modtype Grammar.GLexerType: sig - type te val - lexer : te Plexing.lexer - end +(** When string is neither an ident nor an int, returns a keyword. *) +val terminal : string -> string Tok.p -where +(** The lexer of Coq: *) - type lexer 'te = - { tok_func : lexer_func 'te; - tok_using : pattern -> unit; - tok_removing : pattern -> unit; - tok_match : pattern -> 'te -> string; - tok_text : pattern -> string; - tok_comm : mutable option (list location) } - *) -include Gramlib.Grammar.GLexerType with type te = Tok.t +module Lexer : + Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p module Error : sig type t @@ -90,4 +78,5 @@ 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 *) -val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer +module LexerDiff : + Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p diff --git a/parsing/extend.ml b/parsing/extend.ml index ff879dd1c2..dd7c301dfb 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -10,7 +10,7 @@ (** Entry keys for constr notations *) -type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e +type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.e type side = Left | Right @@ -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.pattern list +type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p 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.pattern list (* Parsed as non-empty list of constr *) + | ETProdConstrList of (production_level * production_position) * string Tok.p 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} *) @@ -79,30 +79,34 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) -type ('self, 'a) 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 -| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol -| Aself : ('self, 'self) symbol -| Anext : ('self, 'self) symbol -| Aentry : 'a entry -> ('self, 'a) symbol -| Aentryl : 'a entry * string -> ('self, 'a) symbol -| Arules : 'a rules list -> ('self, 'a) symbol - -and ('self, _, 'r) rule = -| Stop : ('self, 'r, 'r) rule -| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - -and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } +type norec = NoRec (* just two *) +type mayrec = MayRec (* incompatible types *) + +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 : ('act, Loc.t -> 'a) norec_rule * 'act -> '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 +| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule type 'a single_extend_statement = string option * diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index a50f8d69e3..6df0d6f21a 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.pattern + | GramConstrTerminal of string Tok.p | 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 f2f5d17da3..8f38e437b4 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -17,7 +17,7 @@ open Gramlib (** The parser of Coq *) module G : sig - include Grammar.S with type te = Tok.t + include Grammar.S with type te = Tok.t and type 'c pattern = 'c Tok.p (* where Grammar.S @@ -67,7 +67,7 @@ module type S = end with type 'a Entry.e = 'a Extend.entry = struct - include Grammar.GMake(CLexer) + include Grammar.GMake(CLexer.Lexer) type coq_parsable = parsable * CLexer.lexer_state ref @@ -107,7 +107,7 @@ end module Entry = struct - type 'a t = 'a Grammar.GMake(CLexer).Entry.e + type 'a t = 'a Grammar.GMake(CLexer.Lexer).Entry.e let create = G.Entry.create let parse = G.entry_parse @@ -118,15 +118,6 @@ struct end -module Symbols : sig - 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 slist0sep x y = G.s_list0sep x y false - let slist1sep x y = G.s_list1sep x y false -end - (** Grammar extensions *) (** NB: [extend_statement = @@ -140,43 +131,73 @@ end (** Binding general entry keys to symbol *) -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 -> G.s_token t -| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s) +type ('s, 'trec, 'a, 'r) casted_rule = +| CastedRNo : ('s, G.ty_norec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, norec, 'a, 'r) casted_rule +| CastedRMay : ('s, G.ty_mayrec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, mayrec, 'a, 'r) casted_rule + +type ('s, 'trec, 'a) casted_symbol = +| CastedSNo : ('s, G.ty_norec, 'a) G.ty_symbol -> ('s, norec, 'a) casted_symbol +| CastedSMay : ('s, G.ty_mayrec, 'a) G.ty_symbol -> ('s, mayrec, 'a) casted_symbol + +let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) casted_symbol = +function +| Atoken t -> CastedSNo (G.s_token t) +| Alist1 s -> + begin match symbol_of_prod_entry_key s with + | CastedSNo s -> CastedSNo (G.s_list1 s) + | CastedSMay s -> CastedSMay (G.s_list1 s) end | Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) -| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s) + let CastedSNo sep = symbol_of_prod_entry_key sep in + begin match symbol_of_prod_entry_key s with + | CastedSNo s -> CastedSNo (G.s_list1sep s sep false) + | CastedSMay s -> CastedSMay (G.s_list1sep s sep false) end +| Alist0 s -> + begin match symbol_of_prod_entry_key s with + | CastedSNo s -> CastedSNo (G.s_list0 s) + | CastedSMay s -> CastedSMay (G.s_list0 s) end | Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) -| Aopt s -> G.s_opt (symbol_of_prod_entry_key s) -| Aself -> G.s_self -| Anext -> G.s_next -| Aentry e -> G.s_nterm e -| Aentryl (e, n) -> G.s_nterml e n + let CastedSNo sep = symbol_of_prod_entry_key sep in + begin match symbol_of_prod_entry_key s with + | CastedSNo s -> CastedSNo (G.s_list0sep s sep false) + | CastedSMay s -> CastedSMay (G.s_list0sep s sep false) end +| Aopt s -> + begin match symbol_of_prod_entry_key s with + | CastedSNo s -> CastedSNo (G.s_opt s) + | CastedSMay s -> CastedSMay (G.s_opt s) end +| Aself -> CastedSMay G.s_self +| Anext -> CastedSMay G.s_next +| Aentry e -> CastedSNo (G.s_nterm e) +| Aentryl (e, n) -> CastedSNo (G.s_nterml e n) | Arules rs -> let warning msg = Feedback.msg_warning Pp.(str msg) in - G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) + CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)) -and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function -| Stop -> Casted (G.r_stop, fun act loc -> act loc) +and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) casted_rule = function +| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc) | Next (r, s) -> - let Casted (r, cast) = symbol_of_rule r in - Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x))) - -and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function + begin match symbol_of_rule r, symbol_of_prod_entry_key s with + | CastedRNo (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) + | CastedRNo (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) + | CastedRMay (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) + | CastedRMay (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) end +| NextNoRec (r, s) -> + let CastedRNo (r, cast) = symbol_of_rule r in + let CastedSNo s = symbol_of_prod_entry_key s in + CastedRNo (G.r_next_norec r s, (fun act x -> cast (act x))) + +and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function | Rules (r, act) -> - let Casted (symb, cast) = symbol_of_rule r.norec_rule in - G.production (symb, cast act) + let CastedRNo (symb, cast) = symbol_of_rule r in + G.rules (symb, cast act) (** FIXME: This is a hack around a deficient camlp5 API *) -type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production +type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> - let Casted (symb, cast) = symbol_of_rule toks in - AnyProduction (symb, cast act) + match symbol_of_rule toks with + | CastedRNo (symb, cast) -> AnyProduction (symb, cast act) + | CastedRMay (symb, cast) -> AnyProduction (symb, cast act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, assoc, List.map of_coq_production_rule rule) @@ -288,7 +309,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)) (G.s_token Tok.pattern_for_EOI) in + let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (G.s_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 (symbs, act)]); @@ -425,8 +446,11 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end -let epsilon_value f e = - let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in +let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = + let r = + match symbol_of_prod_entry_key e with + | CastedSNo s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) + | CastedSMay s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0418249e42..e361f0d00f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -203,7 +203,7 @@ module Module : val module_type : module_ast Entry.t end -val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option +val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) diff --git a/parsing/tok.ml b/parsing/tok.ml index f0846dcf90..186d0502fc 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -12,6 +12,31 @@ let string_equal (s1 : string) s2 = s1 = s2 +type 'c p = + | PKEYWORD : string -> string p + | PPATTERNIDENT : string option -> string p + | PIDENT : string option -> string p + | PFIELD : string option -> string p + | PINT : string option -> string p + | PSTRING : string option -> string p + | PLEFTQMARK : unit p + | PBULLET : string option -> string p + | PQUOTATION : string -> string p + | PEOI : unit p + +let pattern_strings : type c. c p -> string * string option = + function + | PKEYWORD s -> "", Some s + | PPATTERNIDENT s -> "PATTERNIDENT", s + | PIDENT s -> "IDENT", s + | PFIELD s -> "FIELD", s + | PINT s -> "INT", s + | PSTRING s -> "STRING", s + | PLEFTQMARK -> "LEFTQMARK", None + | PBULLET s -> "BULLET", s + | PQUOTATION lbl -> "QUOTATION", Some lbl + | PEOI -> "EOI", None + type t = | KEYWORD of string | PATTERNIDENT of string @@ -24,6 +49,22 @@ type t = | QUOTATION of string * string | EOI +let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option = + let streq s1 s2 = match s1, s2 with None, None -> true + | Some s1, Some s2 -> string_equal s1 s2 | _ -> false in + match t1, t2 with + | PKEYWORD s1, PKEYWORD s2 when string_equal s1 s2 -> Some Util.Refl + | PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl + | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl + | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl + | PINT s1, PINT s2 when streq s1 s2 -> Some Util.Refl + | PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl + | PLEFTQMARK, PLEFTQMARK -> Some Util.Refl + | PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl + | PQUOTATION s1, PQUOTATION s2 when string_equal s1 s2 -> Some Util.Refl + | PEOI, PEOI -> Some Util.Refl + | _ -> None + let equal t1 t2 = match t1, t2 with | IDENT s1, KEYWORD s2 -> string_equal s1 s2 | KEYWORD s1, KEYWORD s2 -> string_equal s1 s2 @@ -63,22 +104,6 @@ let extract_string diff_mode = function | QUOTATION(_,s) -> s | EOI -> "" -let to_string = function - | KEYWORD s -> Format.sprintf "%S" s - | IDENT s -> Format.sprintf "IDENT %S" s - | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s - | FIELD s -> Format.sprintf "FIELD %S" s - | INT s -> Format.sprintf "INT %s" s - | STRING s -> Format.sprintf "STRING %S" s - | LEFTQMARK -> "LEFTQMARK" - | BULLET s -> Format.sprintf "BULLET %S" s - | QUOTATION(lbl,s) -> lbl ^ s - | EOI -> "EOI" - -let match_keyword kwd = function - | KEYWORD kwd' when kwd = kwd' -> true - | _ -> false - (* Invariant, txt is "ident" or a well parenthesized "{{....}}" *) let trim_quotation txt = let len = String.length txt in @@ -93,45 +118,23 @@ let trim_quotation txt = aux 0 else None, txt -(* Needed to fix Camlp5 signature. - Cannot use Pp because of silly Tox -> Compat -> Pp dependency *) -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] *) - -type pattern = string * string option - -let is_keyword = function - | "", Some s -> Some (false,s) - | "QUOTATION", Some s -> Some (true,s) - | _ -> None - -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 match_pattern (type c) (p : c p) : t -> c = let err () = raise Stream.Failure in - let cond x = - match value with - | None -> x - | Some value -> if string_equal value x then x else err () in - match key with - | "" -> (function KEYWORD s -> cond s | _ -> err ()) - | "IDENT" when value <> None -> (function (IDENT s | KEYWORD s) -> cond s | _ -> err ()) - | "IDENT" -> (function IDENT s -> cond s | _ -> err ()) - | "PATTERNIDENT" -> (function PATTERNIDENT s -> cond s | _ -> err ()) - | "FIELD" -> (function FIELD s -> cond s | _ -> err ()) - | "INT" -> (function INT s -> cond s | _ -> err ()) - | "STRING" -> (function STRING s -> cond s | _ -> err ()) - | "LEFTQMARK" -> (function LEFTQMARK -> cond "" | _ -> err ()) - | "BULLET" -> (function BULLET s -> cond s | _ -> err ()) - | "QUOTATION" -> (function - | QUOTATION(lbl,s) -> - begin match value with - | None -> assert false - | Some lbl1 -> if string_equal lbl1 lbl then s else err () end - | _ -> err ()) - | "EOI" -> (function EOI -> cond "" | _ -> err ()) - | p -> CErrors.anomaly Pp.(str "Tok: unknown pattern " ++ str p) + let seq = string_equal in + match p with + | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | _ -> err ()) + | PIDENT None -> (function IDENT s' -> s' | _ -> err ()) + | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ()) + | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ()) + | PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ()) + | PFIELD None -> (function FIELD s -> s | _ -> err ()) + | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ()) + | PINT None -> (function INT s -> s | _ -> err ()) + | PINT (Some s) -> (function INT s' when seq s s' -> s' | _ -> err ()) + | PSTRING None -> (function STRING s -> s | _ -> err ()) + | PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ()) + | PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ()) + | PBULLET None -> (function BULLET s -> s | _ -> err ()) + | PBULLET (Some s) -> (function BULLET s' when seq s s' -> s' | _ -> err ()) + | PQUOTATION lbl -> (function QUOTATION(lbl',s') when string_equal lbl lbl' -> s' | _ -> err ()) + | PEOI -> (function EOI -> () | _ -> err ()) diff --git a/parsing/tok.mli b/parsing/tok.mli index 8a255be06f..678877720d 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -10,6 +10,20 @@ (** The type of token for the Coq lexer and parser *) +type 'c p = + | PKEYWORD : string -> string p + | PPATTERNIDENT : string option -> string p + | PIDENT : string option -> string p + | PFIELD : string option -> string p + | PINT : string option -> string p + | PSTRING : string option -> string p + | PLEFTQMARK : unit p + | PBULLET : string option -> string p + | PQUOTATION : string -> string p + | PEOI : unit p + +val pattern_strings : 'c p -> string * string option + type t = | KEYWORD of string | PATTERNIDENT of string @@ -22,13 +36,11 @@ type t = | QUOTATION of string * string | EOI +val equal_p : 'a p -> 'b p -> ('a, 'b) Util.eq option + val equal : t -> t -> bool (* pass true for diff_mode *) val extract_string : bool -> t -> string -val to_string : t -> string -(* Needed to fit Camlp5 signature *) -val print : Format.formatter -> t -> unit -val match_keyword : string -> t -> bool (** Utility function for the test returned by a QUOTATION token: It returns the delimiter parenthesis, if any, and the text @@ -37,12 +49,6 @@ val trim_quotation : string -> char option * string (** for camlp5, eg GRAMMAR EXTEND ..... [ IDENT "x" -> .... END - is a pattern ("IDENT", Some "x") + is a pattern (PIDENT (Some "x")) *) -type pattern = string * string option (* = Plexing.pattern *) - -val is_keyword : pattern -> (bool * 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 +val match_pattern : 'c p -> t -> 'c |