diff options
| -rw-r--r-- | coqpp/coqpp_main.ml | 26 | ||||
| -rw-r--r-- | gramlib/grammar.ml | 749 | ||||
| -rw-r--r-- | gramlib/grammar.mli | 54 | ||||
| -rw-r--r-- | gramlib/plexing.ml | 20 | ||||
| -rw-r--r-- | gramlib/plexing.mli | 32 | ||||
| -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 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 3 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 85 | ||||
| -rw-r--r-- | vernac/egramml.ml | 16 | ||||
| -rw-r--r-- | vernac/egramml.mli | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 8 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 2 |
21 files changed, 807 insertions, 587 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index f4c819eeb6..8657d315f5 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -214,9 +214,20 @@ let print_fun fmt (vars, body) = (** Meta-program instead of calling Tok.of_pattern here because otherwise violates value restriction *) -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 print_tok fmt = +let print_pat fmt = print_opt fmt print_string in +function +| "", Some s -> fprintf fmt "Tok.PKEYWORD (%a)" print_string s +| "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s +| "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s +| "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s +| "INT", s -> fprintf fmt "Tok.PINT (%a)" print_pat s +| "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s +| "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK" +| "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s +| "QUOTATION", Some s -> fprintf fmt "Tok.PQUOTATION %a" print_string s +| "EOI", None -> fprintf fmt "Tok.PEOI" +| _ -> failwith "Tok.of_pattern: not a constructor" let rec print_prod fmt p = let (vars, tkns) = List.split p.gprod_symbs in @@ -225,12 +236,13 @@ 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 tkn print_fun (vars, body) + fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body) -and print_symbols fmt = function +and print_symbols ~norec fmt = function | [] -> fprintf fmt "Extend.Stop" | tkn :: tkns -> - fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn + let c = if norec then "Extend.NextNoRec" else "Extend.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) -> @@ -257,7 +269,7 @@ and print_symbol fmt tkn = match tkn with let pr fmt (r, body) = let (vars, tkn) = List.split r in let tkn = List.rev tkn in - fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) + fprintf fmt "Extend.Rules @[(%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) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 9eebe7a1e2..c452c7b307 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -4,16 +4,16 @@ open Gramext open Format - -type ('a, 'b) eq = Refl : ('a, 'a) eq +open Util (* Functorial interface *) -module type GLexerType = sig type te val lexer : te Plexing.lexer end +module type GLexerType = Plexing.Lexer module type S = sig type te + type 'c pattern type parsable val parsable : ?loc:Loc.t -> char Stream.t -> parsable val tokens : string -> (string option * int) list @@ -27,29 +27,36 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ('self, 'a) ty_symbol - type ('self, 'f, 'r) ty_rule + type ty_norec = TyNoRec + type ty_mayrec = TyMayRec + type ('self, 'trec, 'a) ty_symbol + type ('self, 'trec, 'f, 'r) ty_rule + type 'a ty_rules type 'a ty_production - val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol - val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol - val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + val s_nterm : 'a Entry.e -> ('self, ty_norec, 'a) ty_symbol + val s_nterml : 'a Entry.e -> string -> ('self, ty_norec, 'a) ty_symbol + val s_list0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol val s_list0sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool -> + ('self, 'trec, 'a list) ty_symbol + val s_list1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol val s_list1sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol - val s_self : ('self, 'self) ty_symbol - val s_next : ('self, 'self) ty_symbol - val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol - val r_stop : ('self, 'r, 'r) ty_rule + ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool -> + ('self, 'trec, 'a list) ty_symbol + val s_opt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol + val s_self : ('self, ty_mayrec, 'self) ty_symbol + val s_next : ('self, ty_mayrec, 'self) ty_symbol + val s_token : 'c pattern -> ('self, ty_norec, 'c) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_rules list -> ('self, ty_norec, 'a) ty_symbol + val r_stop : ('self, ty_norec, 'r, 'r) ty_rule val r_next : - ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> - ('self, 'b -> 'a, 'r) ty_rule - val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production + ('self, _, 'a, 'r) ty_rule -> ('self, _, 'b) ty_symbol -> + ('self, ty_mayrec, 'b -> 'a, 'r) ty_rule + val r_next_norec : + ('self, ty_norec, 'a, 'r) ty_rule -> ('self, ty_norec, 'b) ty_symbol -> + ('self, ty_norec, 'b -> 'a, 'r) ty_rule + val rules : (_, ty_norec, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_rules + val production : ('a, _, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig val clear_entry : 'a Entry.e -> unit @@ -59,7 +66,7 @@ module type S = (string option * Gramext.g_assoc option * 'a ty_production list) list -> unit - val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit + val safe_delete_rule : 'a Entry.e -> ('a, _, 'r, 'f) ty_rule -> unit end (* Implementation *) @@ -68,15 +75,15 @@ module GMake (L : GLexerType) = struct type te = L.te +type 'c pattern = 'c L.pattern type 'a parser_t = L.te Stream.t -> 'a type grammar = - { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - glexer : L.te Plexing.lexer } + { gtokens : (string * string option, int ref) Hashtbl.t } let egram = - {gtokens = Hashtbl.create 301; glexer = L.lexer } + {gtokens = Hashtbl.create 301 } let tokens con = let list = ref [] in @@ -85,6 +92,17 @@ let tokens con = egram.gtokens; !list +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + +type ('a, 'b, 'c) ty_and_rec = +| NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec +| MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec + +type ('a, 'b, 'c, 'd) ty_and_rec3 = +| NoRec3 : (ty_norec, ty_norec, ty_norec, ty_norec) ty_and_rec3 +| MayRec3 : ('a, 'b, 'c, ty_mayrec) ty_and_rec3 + type 'a ty_entry = { ename : string; mutable estart : int -> 'a parser_t; @@ -96,45 +114,50 @@ and 'a ty_desc = | Dlevels of 'a ty_level list | Dparser of 'a parser_t -and 'a ty_level = { +and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level + +and ('trecs, 'trecp, 'a) ty_rec_level = { assoc : g_assoc; lname : string option; - lsuffix : ('a, 'a -> Loc.t -> 'a) ty_tree; - lprefix : ('a, Loc.t -> 'a) ty_tree; + lsuffix : ('a, 'trecs, 'a -> Loc.t -> 'a) ty_tree; + lprefix : ('a, 'trecp, Loc.t -> 'a) ty_tree; } -and ('self, 'a) ty_symbol = -| Stoken : Plexing.pattern -> ('self, string) ty_symbol -| Slist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol -| Slist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol -| Slist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol -| Slist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol -| Sopt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol -| Sself : ('self, 'self) ty_symbol -| Snext : ('self, 'self) ty_symbol -| Snterm : 'a ty_entry -> ('self, 'a) ty_symbol -| Snterml : 'a ty_entry * string -> ('self, 'a) ty_symbol -| Stree : ('self, Loc.t -> 'a) ty_tree -> ('self, 'a) ty_symbol - -and ('self, _, 'r) ty_rule = -| TStop : ('self, 'r, 'r) ty_rule -| TNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule - -and ('self, 'a) ty_tree = -| Node : ('self, 'b, 'a) ty_node -> ('self, 'a) ty_tree -| LocAct : 'k * 'k list -> ('self, 'k) ty_tree -| DeadEnd : ('self, 'k) ty_tree - -and ('self, 'a, 'r) ty_node = { - node : ('self, 'a) ty_symbol; - son : ('self, 'a -> 'r) ty_tree; - brother : ('self, 'r) ty_tree; +and ('self, 'trec, 'a) ty_symbol = +| Stoken : 'c pattern -> ('self, ty_norec, 'c) ty_symbol +| Slist1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol +| Slist1sep : ('self, 'trec, 'a) ty_symbol * ('self, ty_norec, _) ty_symbol * bool -> ('self, 'trec, 'a list) ty_symbol +| Slist0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol +| Slist0sep : ('self, 'trec, 'a) ty_symbol * ('self, ty_norec, _) ty_symbol * bool -> ('self, 'trec, 'a list) ty_symbol +| Sopt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol +| Sself : ('self, ty_mayrec, 'self) ty_symbol +| Snext : ('self, ty_mayrec, 'self) ty_symbol +| Snterm : 'a ty_entry -> ('self, ty_norec, 'a) ty_symbol +| Snterml : 'a ty_entry * string -> ('self, ty_norec, 'a) ty_symbol +| Stree : ('self, 'trec, Loc.t -> 'a) ty_tree -> ('self, 'trec, 'a) ty_symbol + +and ('self, _, _, 'r) ty_rule = +| TStop : ('self, ty_norec, 'r, 'r) ty_rule +| TNext : ('trr, 'trs, 'tr) ty_and_rec * ('self, 'trr, 'a, 'r) ty_rule * ('self, 'trs, 'b) ty_symbol -> ('self, 'tr, 'b -> 'a, 'r) ty_rule + +and ('self, 'trec, 'a) ty_tree = +| Node : ('trn, 'trs, 'trb, 'tr) ty_and_rec3 * ('self, 'trn, 'trs, 'trb, 'b, 'a) ty_node -> ('self, 'tr, 'a) ty_tree +| LocAct : 'k * 'k list -> ('self, ty_norec, 'k) ty_tree +| DeadEnd : ('self, ty_norec, 'k) ty_tree + +and ('self, 'trec, 'trecs, 'trecb, 'a, 'r) ty_node = { + node : ('self, 'trec, 'a) ty_symbol; + son : ('self, 'trecs, 'a -> 'r) ty_tree; + brother : ('self, 'trecb, 'r) ty_tree; } +type 'a ty_rules = +| TRules : (_, ty_norec, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_rules + type 'a ty_production = -| TProd : ('a, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production +| TProd : ('a, _, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production -let rec derive_eps : type s a. (s, a) ty_symbol -> bool = +let rec derive_eps : type s r a. (s, r, a) ty_symbol -> bool = function Slist0 _ -> true | Slist0sep (_, _, _) -> true @@ -142,14 +165,14 @@ let rec derive_eps : type s a. (s, a) ty_symbol -> bool = | Stree t -> tree_derive_eps t | Slist1 _ -> false | Slist1sep (_, _, _) -> false - | Snterm _ | Snterml (_, _) -> false + | Snterm _ -> false | Snterml (_, _) -> false | Snext -> false | Sself -> false | Stoken _ -> false -and tree_derive_eps : type s a. (s, a) ty_tree -> bool = +and tree_derive_eps : type s tr a. (s, tr, a) ty_tree -> bool = function LocAct (_, _) -> true - | Node {node = s; brother = bro; son = son} -> + | Node (_, {node = s; brother = bro; son = son}) -> derive_eps s && tree_derive_eps son || tree_derive_eps bro | DeadEnd -> false @@ -158,7 +181,7 @@ let eq_entry : type a1 a2. a1 ty_entry -> a2 ty_entry -> (a1, a2) eq option = fu if (Obj.magic e1) == (Obj.magic e2) then Some (Obj.magic Refl) else None -let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 -> +let rec eq_symbol : type s r1 r2 a1 a2. (s, r1, a1) ty_symbol -> (s, r2, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 -> match s1, s2 with Snterm e1, Snterm e2 -> eq_entry e1 e2 | Snterml (e1, l1), Snterml (e2, l2) -> @@ -188,23 +211,42 @@ let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1, | Stree _, Stree _ -> None | Sself, Sself -> Some Refl | Snext, Snext -> Some Refl - | Stoken p1, Stoken p2 -> if p1 = p2 then Some Refl else None + | Stoken p1, Stoken p2 -> L.tok_pattern_eq p1 p2 | _ -> None -let is_before : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 -> +let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) ty_symbol -> bool = fun s1 s2 -> match s1, s2 with - Stoken ("ANY", _), _ -> false - | _, Stoken ("ANY", _) -> true - | Stoken (_, Some _), Stoken (_, None) -> true - | Stoken _, Stoken _ -> false + | Stoken p1, Stoken p2 -> + snd (L.tok_pattern_strings p1) <> None + && snd (L.tok_pattern_strings p2) = None | Stoken _, _ -> true | _ -> false (** Ancilliary datatypes *) -type ('self, _) ty_symbols = -| TNil : ('self, unit) ty_symbols -| TCns : ('self, 'a) ty_symbol * ('self, 'b) ty_symbols -> ('self, 'a * 'b) ty_symbols +type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec + +type ('a, 'b, 'c) ty_and_ex = +| NR00 : (ty_mayrec, ty_mayrec, ty_mayrec) ty_and_ex +| NR01 : (ty_mayrec, ty_norec, ty_mayrec) ty_and_ex +| NR10 : (ty_norec, ty_mayrec, ty_mayrec) ty_and_ex +| NR11 : (ty_norec, ty_norec, ty_norec) ty_and_ex + +type ('a, 'b) ty_mayrec_and_ex = +| MayRecNR : ('a, 'b, _) ty_and_ex -> ('a, 'b) ty_mayrec_and_ex + +type ('s, 'a) ty_mayrec_symbol = +| MayRecSymbol : ('s, _, 'a) ty_symbol -> ('s, 'a) ty_mayrec_symbol + +type ('s, 'a) ty_mayrec_tree = +| MayRecTree : ('s, 'tr, 'a) ty_tree -> ('s, 'a) ty_mayrec_tree + +type ('s, 'a, 'r) ty_mayrec_rule = +| MayRecRule : ('s, _, 'a, 'r) ty_rule -> ('s, 'a, 'r) ty_mayrec_rule + +type ('self, 'trec, _) ty_symbols = +| TNil : ('self, ty_norec, unit) ty_symbols +| TCns : ('trh, 'trt, 'tr) ty_and_rec * ('self, 'trh, 'a) ty_symbol * ('self, 'trt, 'b) ty_symbols -> ('self, 'tr, 'a * 'b) ty_symbols (** ('i, 'p, 'f, 'r) rel_prod0 ~ ∃ α₁ ... αₙ. @@ -217,99 +259,196 @@ type ('i, _, 'f, _) rel_prod0 = type ('p, 'k, 'r) rel_prod = (unit, 'p, 'k, 'r) rel_prod0 -type ('s, 'i, 'k, 'r) any_symbols = -| AnyS : ('s, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'i, 'k, 'r) any_symbols - -(** FIXME *) -let rec symbols : type s p k r. (s, p) ty_symbols -> (s, k, r) ty_rule -> (s, unit, k, r) any_symbols = - fun accu r -> match r with - | TStop -> AnyS (Obj.magic accu, Rel0) - | TNext (r, s) -> - let AnyS (r, pf) = symbols (TCns (s, accu)) r in - AnyS (Obj.magic r, RelS (Obj.magic pf)) - -let get_symbols : type s k r. (s, k, r) ty_rule -> (s, unit, k, r) any_symbols = - fun r -> symbols TNil r - -let insert_tree (type s p k a) ~warning entry_name (gsymbols : (s, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, a) ty_tree) = - let rec insert : type p f k. (s, p) ty_symbols -> (p, k, f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree = - fun symbols pf tree action -> +type ('s, 'tr, 'i, 'k, 'r) any_symbols = +| AnyS : ('s, 'tr, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'tr, 'i, 'k, 'r) any_symbols + +type ('s, 'tr, 'k, 'r) ty_belast_rule = +| Belast : ('trr, 'trs, 'tr) ty_and_rec * ('s, 'trr, 'k, 'a -> 'r) ty_rule * ('s, 'trs, 'a) ty_symbol -> ('s, 'tr, 'k, 'r) ty_belast_rule + +(* unfortunately, this is quadratic, but ty_rules aren't too long + * (99% of the time of length less or equal 10 and maximum is 22 + * when compiling Coq and its standard library) *) +let rec get_symbols : type s trec k r. (s, trec, k, r) ty_rule -> (s, trec, unit, k, r) any_symbols = + let rec belast_rule : type s trr trs tr a k r. (trr, trs, tr) ty_and_rec -> (s, trr, k, r) ty_rule -> (s, trs, a) ty_symbol -> (s, tr, a -> k, r) ty_belast_rule = + fun ar r s -> match ar, r with + | NoRec2, TStop -> Belast (NoRec2, TStop, s) + | MayRec2, TStop -> Belast (MayRec2, TStop, s) + | NoRec2, TNext (NoRec2, r, s') -> + let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in + Belast (NoRec2, TNext (NoRec2, r, s), s') + | MayRec2, TNext (_, r, s') -> + let Belast (_, r, s') = belast_rule MayRec2 r s' in + Belast (MayRec2, TNext (MayRec2, r, s), s') in + function + | TStop -> AnyS (TNil, Rel0) + | TNext (MayRec2, r, s) -> + let Belast (MayRec2, r, s) = belast_rule MayRec2 r s in + let AnyS (r, pf) = get_symbols r in + AnyS (TCns (MayRec2, s, r), RelS pf) + | TNext (NoRec2, r, s) -> + let Belast (NoRec2, r, s) = belast_rule NoRec2 r s in + let AnyS (r, pf) = get_symbols r in + AnyS (TCns (NoRec2, s, r), RelS pf) + +let get_rec_symbols (type s tr p) (s : (s, tr, p) ty_symbols) : tr ty_rec = + match s with TCns (MayRec2, _, _) -> MayRec + | TCns (NoRec2, _, _) -> NoRec | TNil -> NoRec + +let get_rec_tree (type s tr f) (s : (s, tr, f) ty_tree) : tr ty_rec = + match s with Node (MayRec3, _) -> MayRec + | Node (NoRec3, _) -> NoRec | LocAct _ -> NoRec | DeadEnd -> NoRec + +let and_symbols_tree (type s trs trt p f) (s : (s, trs, p) ty_symbols) (t : (s, trt, f) ty_tree) : (trs, trt) ty_mayrec_and_ex = + match get_rec_symbols s, get_rec_tree t with + | MayRec, MayRec -> MayRecNR NR00 | MayRec, NoRec -> MayRecNR NR01 + | NoRec, MayRec -> MayRecNR NR10 | NoRec, NoRec -> MayRecNR NR11 + +let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_rec) (arn : (trn, trs, trb, trt) ty_and_rec3) (t : (s, trb, f) ty_tree) : (tr', trb, tr) ty_and_rec = + match ar, arn, get_rec_tree t with + | 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 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 - TCns (s, sl), RelS pf -> insert_in_tree s sl pf tree action + TCns (ars, s, sl), RelS pf -> insert_in_tree ar ars s sl pf tree action | TNil, Rel0 -> - match tree with - Node {node = s; son = son; brother = bro} -> - Node {node = s; son = son; brother = insert TNil Rel0 bro action} - | LocAct (old_action, action_list) -> + let node (type tb) ({node = s; son = son; brother = bro} : (_, _, _, tb, _, _) ty_node) = + let ar : (ty_norec, tb, tb) ty_and_ex = + match get_rec_tree bro with MayRec -> NR10 | NoRec -> NR11 in + {node = s; son = son; brother = insert ar TNil Rel0 bro action} in + match ar, tree with + | 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 -> let msg = "<W> Grammar extension: " ^ - (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^ + (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^ "some rule has been masked" in warn_fn msg end; LocAct (action, old_action :: action_list) - | DeadEnd -> LocAct (action, []) - and insert_in_tree : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree = - fun s sl pf tree action -> - match try_insert s sl pf tree action with + | 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 = + fun ar ars s sl pf tree action -> + let ar : (trs'', trt, tr) ty_and_rec = match ar with NR11 -> NoRec2 + | NR00 -> MayRec2 | NR01 -> MayRec2 | NR10 -> MayRec2 in + match try_insert ar ars s sl pf tree action with Some t -> t - | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = tree} - and try_insert : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree option = - fun s sl pf tree action -> + | None -> + let node ar = + {node = s; son = insert ar sl pf DeadEnd action; brother = tree} in + match ar, ars, get_rec_symbols sl with + | MayRec2, MayRec2, MayRec -> Node (MayRec3, node NR01) + | MayRec2, _, NoRec -> Node (MayRec3, node NR11) + | NoRec2, NoRec2, NoRec -> Node (NoRec3, node NR11) + and try_insert : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_rec -> (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 option = + fun ar ars s sl pf tree action -> match tree with - Node {node = s1; son = son; brother = bro} -> + Node (arn, {node = s1; son = son; brother = bro}) -> begin match eq_symbol s s1 with | Some Refl -> - let t = Node {node = s1; son = insert sl pf son action; brother = bro} in - Some t + let MayRecNR arss = and_symbols_tree sl son in + let son = insert arss sl pf son action in + let node = {node = s1; son = son; brother = bro} in + begin match ar, ars, arn, arss with + | MayRec2, _, _, _ -> Some (Node (MayRec3, node)) + | NoRec2, NoRec2, NoRec3, NR11 -> Some (Node (NoRec3, node)) end | None -> + let ar' = and_and_tree ar arn bro in if is_before s1 s || derive_eps s && not (derive_eps s1) then let bro = - match try_insert s sl pf bro action with + match try_insert ar' ars s sl pf bro action with Some bro -> bro - | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = bro} + | None -> + let MayRecNR arss = and_symbols_tree sl DeadEnd in + let son = insert arss sl pf DeadEnd action in + let node = {node = s; son = son; brother = bro} in + match ar, ars, arn, arss with + | MayRec2, _, _, _ -> Node (MayRec3, node) + | NoRec2, NoRec2, NoRec3, NR11 -> Node (NoRec3, node) in - let t = Node {node = s1; son = son; brother = bro} in Some t + let node = {node = s1; son = son; brother = bro} in + match ar, arn with + | MayRec2, _ -> Some (Node (MayRec3, node)) + | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) else - begin match try_insert s sl pf bro action with + match try_insert ar' ars s sl pf bro action with Some bro -> - let t = Node {node = s1; son = son; brother = bro} in Some t + let node = {node = s1; son = son; brother = bro} in + begin match ar, arn with + | MayRec2, _ -> Some (Node (MayRec3, node)) + | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) end | None -> None - end end - | LocAct (_, _) | DeadEnd -> None + | LocAct (_, _) -> None | DeadEnd -> None in - insert gsymbols pf tree action + insert ar gsymbols pf tree action -let srules (type self a) ~warning (rl : a ty_production list) = +let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, ty_norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, ty_norec, a) ty_tree) : (s, ty_norec, a) ty_tree = + insert_tree ~warning 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 MayRecNR ar = and_symbols_tree gsymbols tree in + MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree) + +let srules (type self a) ~warning (rl : a ty_rules list) : (self, ty_norec, a) ty_symbol = + let rec retype_tree : type s a. (s, ty_norec, a) ty_tree -> (self, ty_norec, a) ty_tree = + function + | Node (NoRec3, {node = s; son = son; brother = bro}) -> + Node (NoRec3, {node = retype_symbol s; son = retype_tree son; brother = retype_tree bro}) + | LocAct (k, kl) -> LocAct (k, kl) + | DeadEnd -> DeadEnd + and retype_symbol : type s a. (s, ty_norec, a) ty_symbol -> (self, ty_norec, a) ty_symbol = + function + | Stoken p -> Stoken p + | Slist1 s -> Slist1 (retype_symbol s) + | Slist1sep (s, sep, b) -> Slist1sep (retype_symbol s, retype_symbol sep, b) + | Slist0 s -> Slist0 (retype_symbol s) + | Slist0sep (s, sep, b) -> Slist0sep (retype_symbol s, retype_symbol sep, b) + | Sopt s -> Sopt (retype_symbol s) + | Snterm e -> Snterm e + | Snterml (e, l) -> Snterml (e, l) + | Stree t -> Stree (retype_tree t) in + let rec retype_rule : type s k r. (s, ty_norec, k, r) ty_rule -> (self, ty_norec, k, r) ty_rule = + function + | TStop -> TStop + | TNext (NoRec2, r, s) -> TNext (NoRec2, retype_rule r, retype_symbol s) in let t = List.fold_left - (fun tree (TProd (symbols, action)) -> + (fun tree (TRules (symbols, action)) -> + let symbols = retype_rule symbols in let AnyS (symbols, pf) = get_symbols symbols in - insert_tree ~warning "" symbols pf action tree) + insert_tree_norec ~warning "" symbols pf action tree) DeadEnd rl in - (* FIXME: use an universal self type to ensure well-typedness *) - (Obj.magic (Stree t) : (self, a) ty_symbol) + Stree t -let is_level_labelled n lev = +let is_level_labelled n (Level lev) = match lev.lname with Some n1 -> n = n1 | None -> false -let insert_level (type s p k) ~warning entry_name (symbols : (s, 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) ~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 = match symbols with - | TCns (Sself, symbols) -> + | 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 + Level {assoc = slev.assoc; lname = slev.lname; - lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix; + lsuffix = lsuffix; lprefix = slev.lprefix} | _ -> + let Level slev = slev in + let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in + Level {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; - lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix} + lprefix = lprefix} let empty_lev lname assoc = let assoc = @@ -317,9 +456,10 @@ let empty_lev lname assoc = Some a -> a | None -> LeftA in + Level {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} -let change_lev ~warning lev n lname assoc = +let change_lev ~warning (Level lev) n lname assoc = let a = match assoc with None -> lev.assoc @@ -343,6 +483,7 @@ let change_lev ~warning lev n lname assoc = end; | None -> () end; + Level {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} let get_level ~warning entry position levs = @@ -396,21 +537,24 @@ let get_level ~warning entry position levs = lev :: levs -> [], change_lev ~warning lev "<top>", levs | [] -> [], empty_lev, [] -let change_to_self0 (type s) (type a) (entry : s ty_entry) : (s, a) ty_symbol -> (s, a) ty_symbol = +let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol = function | Snterm e -> begin match eq_entry e entry with - | None -> Snterm e - | Some Refl -> Sself + | None -> MayRecSymbol (Snterm e) + | Some Refl -> MayRecSymbol (Sself) end - | x -> x + | x -> MayRecSymbol x -let rec change_to_self : type s a r. s ty_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with -| TStop -> TStop -| TNext (r, t) -> TNext (change_to_self e r, change_to_self0 e t) +let rec change_to_self : type s trec a r. s ty_entry -> (s, trec, a, r) ty_rule -> (s, a, r) ty_mayrec_rule = fun e r -> match r with +| TStop -> MayRecRule TStop +| TNext (_, r, t) -> + let MayRecRule r = change_to_self e r in + let MayRecSymbol t = change_to_self0 e t in + MayRecRule (TNext (MayRec2, r, t)) let insert_tokens gram symbols = - let rec insert : type s a. (s, a) ty_symbol -> unit = + let rec insert : type s trec a. (s, trec, a) ty_symbol -> unit = function | Slist0 s -> insert s | Slist1 s -> insert s @@ -418,25 +562,25 @@ let insert_tokens gram symbols = | Slist1sep (s, t, _) -> insert s; insert t | Sopt s -> insert s | Stree t -> tinsert t - | Stoken ("ANY", _) -> () | Stoken tok -> - gram.glexer.Plexing.tok_using tok; + L.tok_using tok; let r = + let tok = L.tok_pattern_strings tok in try Hashtbl.find gram.gtokens tok with Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r in incr r - | Snterm _ | Snterml (_, _) -> () + | Snterm _ -> () | Snterml (_, _) -> () | Snext -> () | Sself -> () - and tinsert : type s a. (s, a) ty_tree -> unit = + and tinsert : type s tr a. (s, tr, a) ty_tree -> unit = function - Node {node = s; brother = bro; son = son} -> + Node (_, {node = s; brother = bro; son = son}) -> insert s; tinsert bro; tinsert son - | LocAct (_, _) | DeadEnd -> () - and linsert : type s p. (s, p) ty_symbols -> unit = function + | LocAct (_, _) -> () | DeadEnd -> () + and linsert : type s tr p. (s, tr, p) ty_symbols -> unit = function | TNil -> () - | TCns (s, r) -> insert s; linsert r + | TCns (_, s, r) -> insert s; linsert r in linsert symbols @@ -460,7 +604,7 @@ let levels_of_rules ~warning entry position rules = let lev = List.fold_left (fun lev (TProd (symbols, action)) -> - let symbols = change_to_self entry symbols in + 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) @@ -472,7 +616,7 @@ let levels_of_rules ~warning entry position rules = levs1 @ List.rev levs @ levs2 let logically_eq_symbols entry = - let rec eq_symbols : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 -> + let rec eq_symbols : type s1 s2 trec1 trec2 a1 a2. (s1, trec1, a1) ty_symbol -> (s2, trec2, a2) ty_symbol -> bool = fun s1 s2 -> match s1, s2 with Snterm e1, Snterm e2 -> e1.ename = e2.ename | Snterm e1, Sself -> e1.ename = entry.ename @@ -486,16 +630,19 @@ let logically_eq_symbols entry = eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 | Sopt s1, Sopt s2 -> eq_symbols s1 s2 | Stree t1, Stree t2 -> eq_trees t1 t2 - | Stoken p1, Stoken p2 -> p1 = p2 + | Stoken p1, Stoken p2 -> L.tok_pattern_eq p1 p2 <> None | Sself, Sself -> true | Snext, Snext -> true | _ -> false - and eq_trees : type s1 s2 a1 a2. (s1, a1) ty_tree -> (s2, a2) ty_tree -> bool = fun t1 t2 -> + and eq_trees : type s1 s2 tr1 tr2 a1 a2. (s1, tr1, a1) ty_tree -> (s2, tr2, a2) ty_tree -> bool = fun t1 t2 -> match t1, t2 with - Node n1, Node n2 -> + Node (_, n1), Node (_, n2) -> eq_symbols n1.node n2.node && eq_trees n1.son n2.son && eq_trees n1.brother n2.brother - | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true + | LocAct _, LocAct _ -> true + | LocAct _, DeadEnd -> true + | DeadEnd, LocAct _ -> true + | DeadEnd, DeadEnd -> true | _ -> false in eq_symbols @@ -509,55 +656,56 @@ let logically_eq_symbols entry = [None] if failure *) type 's ex_symbols = -| ExS : ('s, 'p) ty_symbols -> 's ex_symbols +| ExS : ('s, 'tr, 'p) ty_symbols -> 's ex_symbols let delete_rule_in_tree entry = let rec delete_in_tree : - type s p r. (s, p) ty_symbols -> (s, r) ty_tree -> (s ex_symbols option * (s, r) ty_tree) option = + type s tr tr' p r. (s, tr, p) ty_symbols -> (s, tr', r) ty_tree -> (s ex_symbols option * (s, r) ty_mayrec_tree) option = fun symbols tree -> match symbols, tree with - | TCns (s, sl), Node n -> + | TCns (_, s, sl), Node (_, n) -> if logically_eq_symbols entry s n.node then delete_son sl n else begin match delete_in_tree symbols n.brother with - Some (dsl, t) -> - Some (dsl, Node {node = n.node; son = n.son; brother = t}) + Some (dsl, MayRecTree t) -> + Some (dsl, MayRecTree (Node (MayRec3, {node = n.node; son = n.son; brother = t}))) | None -> None end - | TCns (s, sl), _ -> None - | TNil, Node n -> + | TCns (_, s, sl), _ -> None + | TNil, Node (_, n) -> begin match delete_in_tree TNil n.brother with - Some (dsl, t) -> - Some (dsl, Node {node = n.node; son = n.son; brother = t}) + Some (dsl, MayRecTree t) -> + Some (dsl, MayRecTree (Node (MayRec3, {node = n.node; son = n.son; brother = t}))) | None -> None end | TNil, DeadEnd -> None - | TNil, LocAct (_, []) -> Some (Some (ExS TNil), DeadEnd) - | TNil, LocAct (_, action :: list) -> Some (None, LocAct (action, list)) + | TNil, LocAct (_, []) -> Some (Some (ExS TNil), MayRecTree DeadEnd) + | TNil, LocAct (_, action :: list) -> Some (None, MayRecTree (LocAct (action, list))) and delete_son : - type s p a r. (s, p) ty_symbols -> (s, a, r) ty_node -> (s ex_symbols option * (s, r) ty_tree) option = + type s p tr trn trs trb a r. (s, tr, p) ty_symbols -> (s, trn, trs, trb, a, r) ty_node -> (s ex_symbols option * (s, r) ty_mayrec_tree) option = fun sl n -> match delete_in_tree sl n.son with - Some (Some (ExS dsl), DeadEnd) -> Some (Some (ExS (TCns (n.node, dsl))), n.brother) - | Some (Some (ExS dsl), t) -> - let t = Node {node = n.node; son = t; brother = n.brother} in - Some (Some (ExS (TCns (n.node, dsl))), t) - | Some (None, t) -> - let t = Node {node = n.node; son = t; brother = n.brother} in - Some (None, t) + Some (Some (ExS dsl), MayRecTree DeadEnd) -> Some (Some (ExS (TCns (MayRec2, n.node, dsl))), MayRecTree n.brother) + | Some (Some (ExS dsl), MayRecTree t) -> + let t = Node (MayRec3, {node = n.node; son = t; brother = n.brother}) in + Some (Some (ExS (TCns (MayRec2, n.node, dsl))), MayRecTree t) + | Some (None, MayRecTree t) -> + let t = Node (MayRec3, {node = n.node; son = t; brother = n.brother}) in + Some (None, MayRecTree t) | None -> None in delete_in_tree -let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram -> +let rec decr_keyw_use : type s tr a. _ -> (s, tr, a) ty_symbol -> unit = fun gram -> function Stoken tok -> - let r = Hashtbl.find gram.gtokens tok in + let tok' = L.tok_pattern_strings tok in + let r = Hashtbl.find gram.gtokens tok' in decr r; if !r == 0 then begin - Hashtbl.remove gram.gtokens tok; - gram.glexer.Plexing.tok_removing tok + Hashtbl.remove gram.gtokens tok'; + L.tok_removing tok end | Slist0 s -> decr_keyw_use gram s | Slist1 s -> decr_keyw_use gram s @@ -567,69 +715,71 @@ let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram -> | Stree t -> decr_keyw_use_in_tree gram t | Sself -> () | Snext -> () - | Snterm _ | Snterml (_, _) -> () -and decr_keyw_use_in_tree : type s a. _ -> (s, a) ty_tree -> unit = fun gram -> + | Snterm _ -> () | Snterml (_, _) -> () +and decr_keyw_use_in_tree : type s tr a. _ -> (s, tr, a) ty_tree -> unit = fun gram -> function - DeadEnd | LocAct (_, _) -> () - | Node n -> + DeadEnd -> () | LocAct (_, _) -> () + | Node (_, n) -> decr_keyw_use gram n.node; decr_keyw_use_in_tree gram n.son; decr_keyw_use_in_tree gram n.brother -and decr_keyw_use_in_list : type s p. _ -> (s, p) ty_symbols -> unit = fun gram -> +and decr_keyw_use_in_list : type s tr p. _ -> (s, tr, p) ty_symbols -> unit = fun gram -> function | TNil -> () - | TCns (s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l + | TCns (_, s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l let rec delete_rule_in_suffix entry symbols = function - lev :: levs -> + Level lev :: levs -> begin match delete_rule_in_tree entry symbols lev.lsuffix with - Some (dsl, t) -> + Some (dsl, MayRecTree t) -> begin match dsl with Some (ExS dsl) -> decr_keyw_use_in_list egram dsl | None -> () end; - begin match t with - DeadEnd when lev.lprefix == DeadEnd -> levs + begin match t, lev.lprefix with + DeadEnd, DeadEnd -> levs | _ -> let lev = {assoc = lev.assoc; lname = lev.lname; lsuffix = t; lprefix = lev.lprefix} in - lev :: levs + Level lev :: levs end | None -> - let levs = delete_rule_in_suffix entry symbols levs in lev :: levs + let levs = delete_rule_in_suffix entry symbols levs in + Level lev :: levs end | [] -> raise Not_found let rec delete_rule_in_prefix entry symbols = function - lev :: levs -> + Level lev :: levs -> begin match delete_rule_in_tree entry symbols lev.lprefix with - Some (dsl, t) -> + Some (dsl, MayRecTree t) -> begin match dsl with Some (ExS dsl) -> decr_keyw_use_in_list egram dsl | None -> () end; - begin match t with - DeadEnd when lev.lsuffix == DeadEnd -> levs + begin match t, lev.lsuffix with + DeadEnd, DeadEnd -> levs | _ -> let lev = {assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = t} in - lev :: levs + Level lev :: levs end | None -> - let levs = delete_rule_in_prefix entry symbols levs in lev :: levs + let levs = delete_rule_in_prefix entry symbols levs in + Level lev :: levs end | [] -> raise Not_found -let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p) ty_symbols) levs = +let delete_rule_in_level_list (type s tr p) (entry : s ty_entry) (symbols : (s, tr, p) ty_symbols) levs = match symbols with - TCns (Sself, symbols) -> delete_rule_in_suffix entry symbols levs - | TCns (Snterm e, symbols') -> + TCns (_, Sself, symbols) -> delete_rule_in_suffix entry symbols levs + | TCns (_, Snterm e, symbols') -> begin match eq_entry e entry with | None -> delete_rule_in_prefix entry symbols levs | Some Refl -> @@ -637,12 +787,12 @@ let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p) end | _ -> delete_rule_in_prefix entry symbols levs -let rec flatten_tree : type s a. (s, a) ty_tree -> s ex_symbols list = +let rec flatten_tree : type s tr a. (s, tr, a) ty_tree -> s ex_symbols list = function DeadEnd -> [] | LocAct (_, _) -> [ExS TNil] - | Node {node = n; brother = b; son = s} -> - List.map (fun (ExS l) -> ExS (TCns (n, l))) (flatten_tree s) @ flatten_tree b + | Node (_, {node = n; brother = b; son = s}) -> + List.map (fun (ExS l) -> ExS (TCns (MayRec2, n, l))) (flatten_tree s) @ flatten_tree b let utf8_print = ref true @@ -671,7 +821,7 @@ let string_escaped s = let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s) -let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit = +let rec print_symbol : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit = fun ppf -> function | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s @@ -683,30 +833,36 @@ 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, Some prm) when con <> "" -> - fprintf ppf "%s@ %a" con print_str prm + | Stoken p when L.tok_pattern_strings p <> ("", None) -> + begin match L.tok_pattern_strings p with + | con, Some prm -> fprintf ppf "%s@ %a" con print_str prm + | con, None -> fprintf ppf "%s" con end | Snterml (e, l) -> fprintf ppf "%s%s@ LEVEL@ %a" e.ename "" print_str l | s -> print_symbol1 ppf s -and print_symbol1 : type s r. formatter -> (s, r) ty_symbol -> unit = +and print_symbol1 : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit = fun ppf -> function | Snterm e -> fprintf ppf "%s%s" e.ename "" | Sself -> pp_print_string ppf "SELF" | Snext -> pp_print_string ppf "NEXT" - | Stoken ("", Some s) -> print_str ppf s - | Stoken (con, None) -> pp_print_string ppf con + | Stoken p -> + begin match L.tok_pattern_strings p with + | "", Some s -> print_str ppf s + | con, None -> pp_print_string ppf con + | con, Some prm -> fprintf ppf "(%s@ %a)" con print_str prm end | Stree t -> print_level ppf pp_print_space (flatten_tree t) | s -> fprintf ppf "(%a)" print_symbol s -and print_rule : type s p. formatter -> (s, p) ty_symbols -> unit = +and print_rule : type s tr p. formatter -> (s, tr, p) ty_symbols -> unit = fun ppf symbols -> fprintf ppf "@[<hov 0>"; - let rec fold : type s p. _ -> (s, p) ty_symbols -> unit = - fun sep symbols -> match symbols with + let rec fold : type s tr p. _ -> (s, tr, p) ty_symbols -> unit = + fun sep symbols -> + match symbols with | TNil -> () - | TCns (symbol, symbols) -> + | TCns (_, symbol, symbols) -> fprintf ppf "%t%a" sep print_symbol symbol; fold (fun ppf -> fprintf ppf ";@ ") symbols in @@ -727,9 +883,9 @@ and print_level : type s. _ -> _ -> s ex_symbols list -> _ = let print_levels ppf elev = let _ = List.fold_left - (fun sep lev -> + (fun sep (Level lev) -> let rules = - List.map (fun (ExS t) -> ExS (TCns (Sself, t))) (flatten_tree lev.lsuffix) @ + List.map (fun (ExS t) -> ExS (TCns (MayRec2, Sself, t))) (flatten_tree lev.lsuffix) @ flatten_tree lev.lprefix in fprintf ppf "%t@[<hov 2>" sep; @@ -765,31 +921,39 @@ let loc_of_token_interval bp ep = else let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2 -let name_of_symbol : type s a. s ty_entry -> (s, a) ty_symbol -> string = +let name_of_symbol : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> string = fun entry -> function Snterm e -> "[" ^ e.ename ^ "]" | Snterml (e, l) -> "[" ^ e.ename ^ " level " ^ l ^ "]" | Sself -> "[" ^ entry.ename ^ "]" | Snext -> "[" ^ entry.ename ^ "]" - | Stoken tok -> egram.glexer.Plexing.tok_text tok + | Stoken tok -> L.tok_text tok | _ -> "???" type ('r, 'f) tok_list = | TokNil : ('f, 'f) tok_list -| TokCns : ('r, 'f) tok_list -> (string -> 'r, 'f) tok_list +| TokCns : 'a pattern * ('r, 'f) tok_list -> ('a -> 'r, 'f) tok_list + +type ('s, 'f) tok_tree = TokTree : 'a pattern * ('s, _, 'a -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree -type ('s, 'f) tok_tree = TokTree : ('s, string -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree +let rec tok_list_length : type a b. (a, b) tok_list -> int = + function + | TokNil -> 0 + | TokCns (_, t) -> 1 + tok_list_length t -let rec get_token_list : type s r f. - s ty_entry -> _ -> _ -> _ -> (r, f) tok_list -> (s, string -> r) ty_tree -> (_ * _ * _ * (s, f) tok_tree) option = - fun entry first_tok rev_tokl last_tok pf tree -> +let rec get_token_list : type s tr a r f. + s ty_entry -> a pattern -> (r, f) tok_list -> (s, tr, a -> r) ty_tree -> (s, f) tok_tree option = + fun entry last_tok rev_tokl tree -> match tree with - Node {node = Stoken tok; son = son; brother = DeadEnd} -> - get_token_list entry first_tok (last_tok :: rev_tokl) tok (TokCns pf) son - | _ -> if rev_tokl = [] then None else Some (first_tok, rev_tokl, last_tok, TokTree (tree, pf)) + Node (_, {node = Stoken tok; son = son; brother = DeadEnd}) -> + get_token_list entry tok (TokCns (last_tok, rev_tokl)) son + | _ -> + match rev_tokl with + | TokNil -> None + | _ -> Some (TokTree (last_tok, tree, rev_tokl)) -let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ = +let rec name_of_symbol_failed : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> _ = fun entry -> function | Slist0 s -> name_of_symbol_failed entry s @@ -799,13 +963,13 @@ let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ = | Sopt s -> name_of_symbol_failed entry s | Stree t -> name_of_tree_failed entry t | s -> name_of_symbol entry s -and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ = +and name_of_tree_failed : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> _ = fun entry -> function - Node {node = s; brother = bro; son = son} -> + Node (_, {node = s; brother = bro; son = son}) -> let tokl = match s with - Stoken tok -> get_token_list entry tok [] tok TokNil son + Stoken tok -> get_token_list entry tok TokNil son | _ -> None in begin match tokl with @@ -818,20 +982,20 @@ and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ = in let txt = match bro with - DeadEnd | LocAct (_, _) -> txt + DeadEnd -> txt | LocAct (_, _) -> txt | Node _ -> txt ^ " or " ^ name_of_tree_failed entry bro in txt - | Some (_, rev_tokl, last_tok, _) -> - List.fold_left - (fun s tok -> - (if s = "" then "" else s ^ " ") ^ - egram.glexer.Plexing.tok_text tok) - "" (List.rev (last_tok :: rev_tokl)) + | Some (TokTree (last_tok, _, rev_tokl)) -> + let rec build_str : type a b. string -> (a, b) tok_list -> string = + fun s -> function + | TokNil -> s + | TokCns (tok, t) -> build_str (L.tok_text tok ^ " " ^ s) t in + build_str (L.tok_text last_tok) rev_tokl end - | DeadEnd | LocAct (_, _) -> "???" + | DeadEnd -> "???" | LocAct (_, _) -> "???" -let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, a) ty_symbol) tree = +let tree_failed (type s tr a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, tr, a) ty_symbol) tree = let txt = name_of_tree_failed entry tree in let txt = match prev_symb with @@ -866,14 +1030,9 @@ let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_sym txt ^ " (in [" ^ entry.ename ^ "])" let symb_failed entry prev_symb_result prev_symb symb = - let tree = Node {node = symb; brother = DeadEnd; son = DeadEnd} in + let tree = Node (MayRec3, {node = symb; brother = DeadEnd; son = DeadEnd}) in tree_failed entry prev_symb_result prev_symb tree -let is_level_labelled n lev = - match lev.lname with - Some n1 -> n = n1 - | None -> false - let level_number entry lab = let rec lookup levn = function @@ -885,7 +1044,7 @@ let level_number entry lab = Dlevels elev -> lookup 0 elev | Dparser _ -> raise Not_found -let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol = +let rec top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> (s, ty_norec, a) ty_symbol = fun entry -> function Sself -> Snterm entry @@ -894,7 +1053,7 @@ let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol | Slist1sep (s, sep, b) -> Slist1sep (top_symb entry s, sep, b) | _ -> raise Stream.Failure -let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry = +let entry_of_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a ty_entry = fun entry -> function Sself -> entry @@ -903,12 +1062,14 @@ let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry = | Snterml (e, _) -> e | _ -> raise Stream.Failure -let top_tree : type s a. s ty_entry -> (s, a) ty_tree -> (s, a) ty_tree = +let top_tree : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> (s, tr, a) ty_tree = fun entry -> function - Node {node = s; brother = bro; son = son} -> - Node {node = top_symb entry s; brother = bro; son = son} - | LocAct (_, _) | DeadEnd -> raise Stream.Failure + Node (MayRec3, {node = s; brother = bro; son = son}) -> + Node (MayRec3, {node = top_symb entry s; brother = bro; son = son}) + | Node (NoRec3, {node = s; brother = bro; son = son}) -> + Node (NoRec3, {node = top_symb entry s; brother = bro; son = son}) + | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure let skip_if_empty bp p strm = if Stream.count strm == bp then fun a -> p strm @@ -957,18 +1118,18 @@ let call_and_push ps al strm = let al = if !item_skipped then al else a :: al in item_skipped := false; al let token_ematch gram tok = - let tematch = gram.glexer.Plexing.tok_match tok in + let tematch = L.tok_match tok in fun tok -> tematch tok -let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> r parser_t = +let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_tree -> r parser_t = fun entry nlevn alevn -> function DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure) | LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act) - | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} -> + | Node (_, {node = Sself; son = LocAct (act, _); brother = DeadEnd}) -> (fun (strm__ : _ Stream.t) -> let a = entry.estart alevn strm__ in act a) - | Node {node = Sself; son = LocAct (act, _); brother = bro} -> + | Node (_, {node = Sself; son = LocAct (act, _); brother = bro}) -> let p2 = parser_of_tree entry nlevn alevn bro in (fun (strm__ : _ Stream.t) -> match @@ -976,10 +1137,10 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> with Some a -> act a | _ -> p2 strm__) - | Node {node = s; son = son; brother = DeadEnd} -> + | Node (_, {node = s; son = son; brother = DeadEnd}) -> let tokl = match s with - Stoken tok -> get_token_list entry tok [] tok TokNil son + Stoken tok -> get_token_list entry tok TokNil son | _ -> None in begin match tokl with @@ -996,19 +1157,16 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> raise (Stream.Error (tree_failed entry a s son)) in act a) - | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) -> - let s = Stoken first_tok in + | Some (TokTree (last_tok, son, rev_tokl)) -> let lt = Stoken last_tok in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn lt son in - parser_of_token_list entry s son pf p1 - (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl - last_tok + parser_of_token_list entry son p1 rev_tokl last_tok end - | Node {node = s; son = son; brother = bro} -> + | Node (_, {node = s; son = son; brother = bro}) -> let tokl = match s with - Stoken tok -> get_token_list entry tok [] tok TokNil son + Stoken tok -> get_token_list entry tok TokNil son | _ -> None in match tokl with @@ -1028,28 +1186,28 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> | None -> raise (Stream.Error (tree_failed entry a s son)) end | None -> p2 strm) - | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) -> + | Some (TokTree (last_tok, son, rev_tokl)) -> let lt = Stoken last_tok in let p2 = parser_of_tree entry nlevn alevn bro in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn lt son in let p1 = - parser_of_token_list entry lt son pf p1 p2 rev_tokl last_tok + parser_of_token_list entry son p1 rev_tokl last_tok in fun (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> p2 strm__ -and parser_cont : type s a r. - (a -> r) parser_t -> s ty_entry -> int -> int -> (s, a) ty_symbol -> (s, a -> r) ty_tree -> int -> a -> (a -> r) parser_t = +and parser_cont : type s tr tr' a r. + (a -> r) parser_t -> s ty_entry -> int -> int -> (s, tr, a) ty_symbol -> (s, tr', a -> r) ty_tree -> int -> a -> (a -> r) parser_t = fun p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> recover parser_of_tree entry nlevn alevn bp a s son strm__ -and parser_of_token_list : type s r f. - s ty_entry -> (s, string) ty_symbol -> (s, string -> r) ty_tree -> - (r, f) tok_list -> (int -> string -> (string -> r) parser_t) -> f parser_t -> _ -> _ -> f parser_t = - fun entry s son pf p1 p2 rev_tokl last_tok -> +and parser_of_token_list : type s tr lt r f. + s ty_entry -> (s, tr, lt -> r) ty_tree -> + (int -> lt -> (lt -> r) parser_t) -> (r, f) tok_list -> lt pattern -> f parser_t = + fun entry son p1 rev_tokl last_tok -> + let n = tok_list_length rev_tokl + 1 in let plast : r parser_t = - let n = List.length rev_tokl + 1 in let tematch = token_ematch egram last_tok in let ps strm = match peek_nth n strm with @@ -1063,41 +1221,24 @@ and parser_of_token_list : type s r f. let a = ps strm in match try Some (p1 bp a strm) with Stream.Failure -> None with Some act -> act a - | None -> raise (Stream.Error (tree_failed entry a s son)) + | None -> raise (Stream.Error (tree_failed entry a (Stoken last_tok) son)) in - match List.rev rev_tokl, pf with - [], TokNil -> (fun (strm__ : _ Stream.t) -> plast strm__) - | tok :: tokl, TokCns pf -> - let tematch = token_ematch egram tok in - let ps strm = - match peek_nth 1 strm with - Some tok -> tematch tok - | None -> raise Stream.Failure - in - let p1 = - let rec loop : type s f. _ -> _ -> (s, f) tok_list -> (string -> s) parser_t -> (string -> f) parser_t = - fun n tokl pf plast -> - match tokl, pf with - [], TokNil -> plast - | tok :: tokl, TokCns pf -> - let tematch = token_ematch egram tok in - let ps strm = - match peek_nth n strm with - Some tok -> tematch tok - | None -> raise Stream.Failure - in - let p1 = loop (n + 1) tokl pf (Obj.magic plast) in (* FIXME *) - fun (strm__ : _ Stream.t) -> - let a = ps strm__ in let act = p1 strm__ in (Obj.magic act a) (* FIXME *) - | _ -> assert false - in - loop 2 tokl pf plast - in - fun (strm__ : _ Stream.t) -> - let a = ps strm__ in let act = p1 strm__ in act a - | _ -> assert false -and parser_of_symbol : type s a. - s ty_entry -> int -> (s, a) ty_symbol -> a parser_t = + let rec loop : type s f. _ -> (s, f) tok_list -> s parser_t -> f parser_t = + fun n tokl plast -> match tokl with + | TokNil -> plast + | TokCns (tok, tokl) -> + let tematch = token_ematch egram tok in + let ps strm = + match peek_nth n strm with + Some tok -> tematch tok + | None -> raise Stream.Failure + in + let plast = fun (strm : _ Stream.t) -> + let a = ps strm in let act = plast strm in act a in + loop (n - 1) tokl plast in + loop (n - 1) rev_tokl plast +and parser_of_symbol : type s tr a. + s ty_entry -> int -> (s, tr, a) ty_symbol -> a parser_t = fun entry nlevn -> function | Slist0 s -> @@ -1219,22 +1360,22 @@ and parser_of_symbol : type s a. | Sself -> (fun (strm__ : _ Stream.t) -> entry.estart 0 strm__) | Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__) | Stoken tok -> parser_of_token entry tok -and parser_of_token : type s. - s ty_entry -> Plexing.pattern -> string parser_t = +and parser_of_token : type s a. + s ty_entry -> a pattern -> a parser_t = fun entry tok -> - let f = egram.glexer.Plexing.tok_match tok in + let f = L.tok_match tok in fun strm -> match Stream.peek strm with Some tok -> let r = f tok in Stream.junk strm; r | None -> raise Stream.Failure -and parse_top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a parser_t = +and parse_top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a parser_t = fun entry symb -> parser_of_symbol entry 0 (top_symb entry symb) let rec start_parser_of_levels entry clevn = function [] -> (fun levn (strm__ : _ Stream.t) -> raise Stream.Failure) - | lev :: levs -> + | Level lev :: levs -> let p1 = start_parser_of_levels entry (succ clevn) levs in match lev.lprefix with DeadEnd -> p1 @@ -1277,7 +1418,7 @@ let rec start_parser_of_levels entry clevn = let rec continue_parser_of_levels entry clevn = function [] -> (fun levn bp a (strm__ : _ Stream.t) -> raise Stream.Failure) - | lev :: levs -> + | Level lev :: levs -> let p1 = continue_parser_of_levels entry (succ clevn) levs in match lev.lsuffix with DeadEnd -> p1 @@ -1399,7 +1540,7 @@ let clear_entry e = | Dparser _ -> () let parsable ?loc cs = - let (ts, lf) = L.lexer.Plexing.tok_func ?loc cs in + let (ts, lf) = L.tok_func ?loc cs in {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf} module Entry = struct @@ -1432,9 +1573,11 @@ let clear_entry e = let s_self = Sself let s_next = Snext let s_token tok = Stoken tok - let s_rules ~warning (t : 'a ty_production list) = srules ~warning t + let s_rules ~warning (t : 'a ty_rules list) = srules ~warning t let r_stop = TStop - let r_next r s = TNext (r, s) + let r_next r s = TNext (MayRec2, r, s) + let r_next_norec r s = TNext (NoRec2, r, s) + let rules (p, act) = TRules (p, act) let production (p, act) = TProd (p, act) module Unsafe = struct diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 453ec85187..ec4ec62409 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -15,13 +15,14 @@ rule "an entry cannot call an entry of another grammar" by normal OCaml typing. *) -module type GLexerType = sig type te val lexer : te Plexing.lexer end +module type GLexerType = Plexing.Lexer (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) module type S = sig type te + type 'c pattern type parsable val parsable : ?loc:Loc.t -> char Stream.t -> parsable val tokens : string -> (string option * int) list @@ -35,29 +36,37 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ('self, 'a) ty_symbol - type ('self, 'f, 'r) ty_rule + type ty_norec = TyNoRec + type ty_mayrec = TyMayRec + type ('self, 'trec, 'a) ty_symbol + type ('self, 'trec, 'f, 'r) ty_rule + type 'a ty_rules type 'a ty_production - val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol - val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol - val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + val s_nterm : 'a Entry.e -> ('self, ty_norec, 'a) ty_symbol + val s_nterml : 'a Entry.e -> string -> ('self, ty_norec, 'a) ty_symbol + val s_list0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol val s_list0sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool -> + ('self, 'trec, 'a list) ty_symbol + val s_list1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol val s_list1sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol - val s_self : ('self, 'self) ty_symbol - val s_next : ('self, 'self) ty_symbol - val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol - val r_stop : ('self, 'r, 'r) ty_rule + ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool -> + ('self, 'trec, 'a list) ty_symbol + val s_opt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol + val s_self : ('self, ty_mayrec, 'self) ty_symbol + val s_next : ('self, ty_mayrec, 'self) ty_symbol + val s_token : 'c pattern -> ('self, ty_norec, 'c) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_rules list -> ('self, ty_norec, 'a) ty_symbol + + val r_stop : ('self, ty_norec, 'r, 'r) ty_rule val r_next : - ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> - ('self, 'b -> 'a, 'r) ty_rule - val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production + ('self, _, 'a, 'r) ty_rule -> ('self, _, 'b) ty_symbol -> + ('self, ty_mayrec, 'b -> 'a, 'r) ty_rule + val r_next_norec : + ('self, ty_norec, 'a, 'r) ty_rule -> ('self, ty_norec, 'b) ty_symbol -> + ('self, ty_norec, 'b -> 'a, 'r) ty_rule + val rules : (_, ty_norec, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_rules + val production : ('a, _, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig @@ -68,7 +77,7 @@ module type S = (string option * Gramext.g_assoc option * 'a ty_production list) list -> unit - val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit + val safe_delete_rule : 'a Entry.e -> ('a, _, 'f, 'r) ty_rule -> unit end (** Signature type of the functor [Grammar.GMake]. The types and functions are almost the same than in generic interface, but: @@ -80,4 +89,5 @@ module type S = 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 +module GMake (L : GLexerType) : + S with type te = L.te and type 'c pattern = 'c L.pattern diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index 6da06f147f..e881ab3350 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -2,15 +2,17 @@ (* plexing.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -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 -type 'te lexer = - { tok_func : 'te lexer_func; - tok_using : pattern -> unit; - tok_removing : pattern -> unit; - tok_match : pattern -> 'te -> string; - tok_text : pattern -> string; - } +module type Lexer = sig + type te + type 'c pattern + val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option + val tok_pattern_strings : 'c pattern -> string * string option + val tok_func : te lexer_func + val tok_using : 'c pattern -> unit + val tok_removing : 'c pattern -> unit + val tok_match : 'c pattern -> te -> 'c + val tok_text : 'c pattern -> string +end diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 26443df026..521eba7446 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -8,27 +8,21 @@ grammars (see module [Grammar]). It also provides some useful functions to create lexers. *) -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 - an uppercase character). When it is empty, the second string - is supposed to be a keyword. -- The second component is the constructor parameter. None if it - has no parameter (corresponding to the 'wildcard' pattern). -- The way tokens patterns are interpreted to parse tokens is done - by the lexer, function [tok_match] below. *) - (** Lexer type *) -type 'te lexer = - { tok_func : 'te lexer_func; - tok_using : pattern -> unit; - tok_removing : pattern -> unit; - tok_match : pattern -> 'te -> string; - tok_text : pattern -> string; - } -and 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function +type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function 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 + type te + type 'c pattern + val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option + val tok_pattern_strings : 'c pattern -> string * string option + val tok_func : te lexer_func + val tok_using : 'c pattern -> unit + val tok_removing : 'c pattern -> unit + val tok_match : 'c pattern -> te -> 'c + val tok_text : 'c pattern -> string +end 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 diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index b770b97384..814be64f81 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -48,7 +48,7 @@ let atactic n = else Aentryl (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) Extend.symbol -> entry_name (** Quite ad-hoc *) let get_tacentry n m = diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index ab4501fe75..d042a1d650 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -102,8 +102,7 @@ let tokenize_string s = let st = CLexer.get_lexer_state () in try let istr = Stream.of_string s in - let lexer = CLexer.make_lexer ~diff_mode:true in - let lex = lexer.Gramlib.Plexing.tok_func istr in + let lex = CLexer.LexerDiff.tok_func istr in let toks = stream_tok [] (fst lex) in CLexer.set_lexer_state st; toks diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index f96b567f1b..f1a08cc9b3 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.pattern list * 'r target -> ('r, 'r list) entry +| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry | TTOpenBinderList : ('self, local_binder_expr list) entry -| TTClosedBinderList : Tok.pattern list -> ('self, local_binder_expr list list) entry +| TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry @@ -319,41 +319,49 @@ let is_binder_level from e = match e with let make_sep_rules = function | [tk] -> Atoken tk | tkl -> - let rec mkrule : Tok.pattern list -> string rules = function - | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "") + let rec mkrule : 'a Tok.p list -> 'a rules = function + | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "") | tkn :: rem -> - let Rules ({ norec_rule = r }, f) = mkrule rem in - let r = { norec_rule = Next (r, Atoken tkn) } in + 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 symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat -> - if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200") - else if is_self from p then Aself +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 custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200")) + else if is_self from p then MayRecMay Aself else let g = target_entry custom forpat in let lev = adjust_level assoc from p in begin match lev with - | None -> Aentry g - | Some None -> Anext - | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev) + | None -> MayRecNo (Aentry g) + | Some None -> MayRecMay Anext + | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev)) end -let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with +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 (typ', [], forpat) -> - Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat) + begin match symbol_of_target InConstrEntry typ' assoc from forpat with + | MayRecNo s -> MayRecNo (Alist1 s) + | MayRecMay s -> MayRecMay (Alist1 s) end | TTConstrList (typ', tkl, forpat) -> - Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl) -| TTPattern p -> Aentryl (Constr.pattern, string_of_int p) -| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) -| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) -| TTName -> Aentry Prim.name -| TTOpenBinderList -> Aentry Constr.open_binders -| TTBigint -> Aentry Prim.bigint -| TTReference -> Aentry Constr.global + begin match symbol_of_target InConstrEntry 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.bigint) +| TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName @@ -406,8 +414,8 @@ match e with | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } type (_, _) ty_symbol = -| TyTerm : Tok.pattern -> ('s, string) ty_symbol -| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol +| TyTerm : string Tok.p -> ('s, string) ty_symbol +| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) mayrec_symbol * bool -> ('s, 'a) ty_symbol type ('self, _, 'r) ty_rule = | TyStop : ('self, 'r, 'r) ty_rule @@ -444,11 +452,23 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> in ty_eval rem f { env with constrs; constrlists; } -let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function -| TyStop -> Stop +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 + +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) -> Next (ty_erase rem, Atoken tok) -| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) +| 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 +| 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 type ('self, 'r) any_ty_rule = | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule @@ -485,7 +505,7 @@ let rec pure_sublevels' custom assoc from forpat level = function let rem = pure_sublevels' custom assoc from forpat level rem in let push where p rem = match symbol_of_target custom p assoc from forpat with - | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem + | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem | _ -> rem in (match e with | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem @@ -507,7 +527,6 @@ let extend_constr state forpat ng = let (entry, level) = interp_constr_entry_key custom forpat n in let fold (accu, state) pt = let AnyTyRule r = make_ty_rule assoc n forpat pt in - let symbs = ty_erase r in let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in let isforpat = target_to_bool forpat in let needed_levels, state = register_empty_levels state isforpat pure_sublevels in @@ -515,7 +534,11 @@ let extend_constr state forpat ng = let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in - let rule = (name, p4assoc, [Rule (symbs, act)]) in + let rule = + let r = match ty_erase r with + | MayRecRNo symbs -> Rule (symbs, act) + | MayRecRMay symbs -> Rule (symbs, act) in + name, p4assoc, [r] in let r = ExtendRule (entry, reinit, (pos, [rule])) in (accu @ empty_rules @ [r], state) in diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 89caff847f..bc58993a2e 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -19,17 +19,17 @@ 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) symbol) Loc.located -> 's grammar_prod_item type 'a ty_arg = ('a -> raw_generic_argument) -type ('self, _, 'r) ty_rule = -| TyStop : ('self, 'r, 'r) ty_rule -| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option -> - ('self, 'b -> 'a, 'r) ty_rule +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 type ('self, 'r) any_ty_rule = -| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule +| AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule let rec ty_rule_of_gram = function | [] -> AnyTyRule TyStop @@ -44,13 +44,13 @@ let rec ty_rule_of_gram = function let r = TyNext (rem, tok, inj) in AnyTyRule r -let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function +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) type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r -let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function +let rec ty_eval : type s tr a. (s, tr, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function | TyStop -> fun f loc -> f loc [] | TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f | TyNext (rem, tok, Some inj) -> fun f x -> diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 3689f60383..1cf75a55b1 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) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : extend_name -> vernac_expr Pcoq.Entry.t option -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 781fd404f8..b5e9e1b0d5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -574,20 +574,20 @@ let is_not_small_constr = function | _ -> false let rec define_keywords_aux = function - | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",Some k) :: l + | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(Tok.PIDENT (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(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l + n1 :: GramConstrTerminal(Tok.PKEYWORD 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", Some k)::l -> + | GramConstrTerminal(Tok.PIDENT (Some k))::l -> Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; - GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l + GramConstrTerminal(Tok.PKEYWORD 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 9438b9749f..d474ef8637 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.pattern_for_EOI), act_eoi); + Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in Pcoq.grammar_extend main_entry None (None, [None, None, rule]) diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 4bfe5c66b5..ef06e59316 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -169,7 +169,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_comm | 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, a) Extend.symbol = +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Extend.norec, a) Extend.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)) |