From eadb00648127c9a535b533d51189dce41ef16db7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 17 Feb 2019 10:10:22 +0100 Subject: Multiple payload types in tokens Instead of just string (and empty strings for tokens without payload) --- coqpp/coqpp_main.ml | 26 +- gramlib/grammar.ml | 749 +++++++++++++++++++++++++++------------------ gramlib/grammar.mli | 54 ++-- gramlib/plexing.ml | 20 +- gramlib/plexing.mli | 32 +- parsing/cLexer.ml | 63 ++-- parsing/cLexer.mli | 25 +- parsing/extend.ml | 50 +-- parsing/notation_gram.ml | 2 +- parsing/pcoq.ml | 104 ++++--- parsing/pcoq.mli | 2 +- parsing/tok.ml | 117 +++---- parsing/tok.mli | 30 +- plugins/ltac/tacentries.ml | 2 +- printing/proof_diffs.ml | 3 +- vernac/egramcoq.ml | 85 +++-- vernac/egramml.ml | 16 +- vernac/egramml.mli | 2 +- vernac/metasyntax.ml | 8 +- vernac/pvernac.ml | 2 +- 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 = " 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 "", 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 "@["; - 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@[" 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)) -- cgit v1.2.3 From ef6c99e0e2e55b9fe316cc14663df161ebf4a21e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Mar 2019 22:06:44 +0100 Subject: Improve coqpp error message for SELF in anonymous entry Something like "("; [ s = SELF -> { s } ]; ")" in a GRAMMAR EXTEND in a mlg file was causing an error message such as OCAMLOPT f.ml File "f.mlg", line 179, characters 55-67: # not in a semantic rule so line doesn't match anything in the mlg file Error: This expression has type ('a, Extend.mayrec, 'a) Extend.symbol but an expression was expected of type ('a, Extend.norec, 'b) Extend.symbol Type Extend.mayrec is not compatible with type Extend.norec It is now COQPP f.mlg Error: 'SELF' or 'NEXT' illegal in anonymous entry level --- coqpp/coqpp_main.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 8657d315f5..baa6c2d64e 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -161,29 +161,33 @@ let is_token s = match string_split s with | [s] -> is_uident s | _ -> false -let rec parse_tokens = function +let rec parse_tokens ?(in_anon=false) = +let err_anon () = + if in_anon then + fatal (Printf.sprintf "'SELF' or 'NEXT' illegal in anonymous entry level") in +function | [GSymbString s] -> SymbToken ("", Some s) | [GSymbQualid ("QUOTATION", None); GSymbString s] -> SymbToken ("QUOTATION", Some s) -| [GSymbQualid ("SELF", None)] -> SymbSelf -| [GSymbQualid ("NEXT", None)] -> SymbNext +| [GSymbQualid ("SELF", None)] -> err_anon (); SymbSelf +| [GSymbQualid ("NEXT", None)] -> err_anon (); SymbNext | [GSymbQualid ("LIST0", None); tkn] -> - SymbList0 (parse_token tkn, None) + SymbList0 (parse_token ~in_anon tkn, None) | [GSymbQualid ("LIST1", None); tkn] -> - SymbList1 (parse_token tkn, None) + SymbList1 (parse_token ~in_anon tkn, None) | [GSymbQualid ("LIST0", None); tkn; GSymbQualid ("SEP", None); tkn'] -> - SymbList0 (parse_token tkn, Some (parse_token tkn')) + SymbList0 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn')) | [GSymbQualid ("LIST1", None); tkn; GSymbQualid ("SEP", None); tkn'] -> - SymbList1 (parse_token tkn, Some (parse_token tkn')) + SymbList1 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn')) | [GSymbQualid ("OPT", None); tkn] -> - SymbOpt (parse_token tkn) + SymbOpt (parse_token ~in_anon tkn) | [GSymbQualid (e, None)] when is_token e -> SymbToken (e, None) | [GSymbQualid (e, None); GSymbString s] when is_token e -> SymbToken (e, Some s) | [GSymbQualid (e, lvl)] when not (is_token e) -> SymbEntry (e, lvl) -| [GSymbParen tkns] -> parse_tokens tkns +| [GSymbParen tkns] -> parse_tokens ~in_anon tkns | [GSymbProd prds] -> let map p = - let map (pat, tkns) = (pat, parse_tokens tkns) in + let map (pat, tkns) = (pat, parse_tokens ~in_anon:true tkns) in (List.map map p.gprod_symbs, p.gprod_body) in SymbRules (List.map map prds) @@ -199,7 +203,7 @@ let rec parse_tokens = function in fatal (Printf.sprintf "Invalid token: %s" (db_tokens t)) -and parse_token tkn = parse_tokens [tkn] +and parse_token ~in_anon tkn = parse_tokens ~in_anon [tkn] let print_fun fmt (vars, body) = let vars = List.rev vars in -- cgit v1.2.3 From d8d3b7a8251b874c436ac11b881cf4fb5f991784 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 24 Mar 2019 22:59:34 +0100 Subject: Add overlay --- dev/ci/user-overlays/09815-token-type.sh | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 dev/ci/user-overlays/09815-token-type.sh diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh new file mode 100644 index 0000000000..4b49011de3 --- /dev/null +++ b/dev/ci/user-overlays/09815-token-type.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then + ltac2_CI_REF=token-type + ltac2_CI_GITURL=https://github.com/proux01/ltac2 +fi -- cgit v1.2.3