Multiple payload types in tokens

Instead of just string (and empty strings for tokens without payload)

4 files changed, 502 insertions, 353 deletions

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 9eebe7a1e2..c452c7b307 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -4,16 +4,16 @@
 
 open Gramext
 open Format
-
-type ('a, 'b) eq = Refl : ('a, 'a) eq
+open Util
 
 (* Functorial interface *)
 
-module type GLexerType = sig type te val lexer : te Plexing.lexer end
+module type GLexerType = Plexing.Lexer
 
 module type S =
   sig
     type te
+    type 'c pattern
     type parsable
     val parsable : ?loc:Loc.t -> char Stream.t -> parsable
     val tokens : string -> (string option * int) list
@@ -27,29 +27,36 @@ module type S =
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
       end
-    type ('self, 'a) ty_symbol
-    type ('self, 'f, 'r) ty_rule
+    type ty_norec = TyNoRec
+    type ty_mayrec = TyMayRec
+    type ('self, 'trec, 'a) ty_symbol
+    type ('self, 'trec, 'f, 'r) ty_rule
+    type 'a ty_rules
     type 'a ty_production
-    val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
-    val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
-    val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+    val s_nterm : 'a Entry.e -> ('self, ty_norec, 'a) ty_symbol
+    val s_nterml : 'a Entry.e -> string -> ('self, ty_norec, 'a) ty_symbol
+    val s_list0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
     val s_list0sep :
-      ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
-        ('self, 'a list) ty_symbol
-    val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+      ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+        ('self, 'trec, 'a list) ty_symbol
+    val s_list1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
     val s_list1sep :
-      ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
-        ('self, 'a list) ty_symbol
-    val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
-    val s_self : ('self, 'self) ty_symbol
-    val s_next : ('self, 'self) ty_symbol
-    val s_token : Plexing.pattern -> ('self, string) ty_symbol
-    val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
-    val r_stop : ('self, 'r, 'r) ty_rule
+      ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+        ('self, 'trec, 'a list) ty_symbol
+    val s_opt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol
+    val s_self : ('self, ty_mayrec, 'self) ty_symbol
+    val s_next : ('self, ty_mayrec, 'self) ty_symbol
+    val s_token : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+    val s_rules : warning:(string -> unit) option -> 'a ty_rules list -> ('self, ty_norec, 'a) ty_symbol
+    val r_stop : ('self, ty_norec, 'r, 'r) ty_rule
     val r_next :
-      ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
-        ('self, 'b -> 'a, 'r) ty_rule
-    val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
+      ('self, _, 'a, 'r) ty_rule -> ('self, _, 'b) ty_symbol ->
+        ('self, ty_mayrec, 'b -> 'a, 'r) ty_rule
+    val r_next_norec :
+      ('self, ty_norec, 'a, 'r) ty_rule -> ('self, ty_norec, 'b) ty_symbol ->
+        ('self, ty_norec, 'b -> 'a, 'r) ty_rule
+    val rules : (_, ty_norec, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_rules
+    val production : ('a, _, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
     module Unsafe :
       sig
         val clear_entry : 'a Entry.e -> unit
@@ -59,7 +66,7 @@ module type S =
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
         unit
-    val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit
+    val safe_delete_rule : 'a Entry.e -> ('a, _, 'r, 'f) ty_rule -> unit
   end
 
 (* Implementation *)
@@ -68,15 +75,15 @@ module GMake (L : GLexerType) =
 struct
 
 type te = L.te
+type 'c pattern = 'c L.pattern
 
 type 'a parser_t = L.te Stream.t -> 'a
 
 type grammar =
-  { gtokens : (Plexing.pattern, int ref) Hashtbl.t;
-    glexer : L.te Plexing.lexer }
+  { gtokens : (string * string option, int ref) Hashtbl.t }
 
 let egram =
-  {gtokens = Hashtbl.create 301; glexer = L.lexer }
+  {gtokens = Hashtbl.create 301 }
 
 let tokens con =
   let list = ref [] in
@@ -85,6 +92,17 @@ let tokens con =
     egram.gtokens;
   !list
 
+type ty_norec = TyNoRec
+type ty_mayrec = TyMayRec
+
+type ('a, 'b, 'c) ty_and_rec =
+| NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec
+| MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec
+
+type ('a, 'b, 'c, 'd) ty_and_rec3 =
+| NoRec3 : (ty_norec, ty_norec, ty_norec, ty_norec) ty_and_rec3
+| MayRec3 : ('a, 'b, 'c, ty_mayrec) ty_and_rec3
+
 type 'a ty_entry = {
   ename : string;
   mutable estart : int -> 'a parser_t;
@@ -96,45 +114,50 @@ and 'a ty_desc =
 | Dlevels of 'a ty_level list
 | Dparser of 'a parser_t
 
-and 'a ty_level = {
+and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level
+
+and ('trecs, 'trecp, 'a) ty_rec_level = {
   assoc : g_assoc;
   lname : string option;
-  lsuffix : ('a, 'a -> Loc.t -> 'a) ty_tree;
-  lprefix : ('a, Loc.t -> 'a) ty_tree;
+  lsuffix : ('a, 'trecs, 'a -> Loc.t -> 'a) ty_tree;
+  lprefix : ('a, 'trecp, Loc.t -> 'a) ty_tree;
 }
 
-and ('self, 'a) ty_symbol =
-| Stoken : Plexing.pattern -> ('self, string) ty_symbol
-| Slist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
-| Slist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol
-| Slist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
-| Slist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol
-| Sopt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
-| Sself : ('self, 'self) ty_symbol
-| Snext : ('self, 'self) ty_symbol
-| Snterm : 'a ty_entry -> ('self, 'a) ty_symbol
-| Snterml : 'a ty_entry * string -> ('self, 'a) ty_symbol
-| Stree : ('self, Loc.t -> 'a) ty_tree -> ('self, 'a) ty_symbol
-
-and ('self, _, 'r) ty_rule =
-| TStop : ('self, 'r, 'r) ty_rule
-| TNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule
-
-and ('self, 'a) ty_tree =
-| Node : ('self, 'b, 'a) ty_node -> ('self, 'a) ty_tree
-| LocAct : 'k * 'k list -> ('self, 'k) ty_tree
-| DeadEnd : ('self, 'k) ty_tree
-
-and ('self, 'a, 'r) ty_node = {
-  node : ('self, 'a) ty_symbol;
-  son : ('self, 'a -> 'r) ty_tree;
-  brother : ('self, 'r) ty_tree;
+and ('self, 'trec, 'a) ty_symbol =
+| Stoken : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+| Slist1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
+| Slist1sep : ('self, 'trec, 'a) ty_symbol * ('self, ty_norec, _) ty_symbol * bool -> ('self, 'trec, 'a list) ty_symbol
+| Slist0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
+| Slist0sep : ('self, 'trec, 'a) ty_symbol * ('self, ty_norec, _) ty_symbol * bool -> ('self, 'trec, 'a list) ty_symbol
+| Sopt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol
+| Sself : ('self, ty_mayrec, 'self) ty_symbol
+| Snext : ('self, ty_mayrec, 'self) ty_symbol
+| Snterm : 'a ty_entry -> ('self, ty_norec, 'a) ty_symbol
+| Snterml : 'a ty_entry * string -> ('self, ty_norec, 'a) ty_symbol
+| Stree : ('self, 'trec, Loc.t -> 'a) ty_tree -> ('self, 'trec, 'a) ty_symbol
+
+and ('self, _, _, 'r) ty_rule =
+| TStop : ('self, ty_norec, 'r, 'r) ty_rule
+| TNext : ('trr, 'trs, 'tr) ty_and_rec * ('self, 'trr, 'a, 'r) ty_rule * ('self, 'trs, 'b) ty_symbol -> ('self, 'tr, 'b -> 'a, 'r) ty_rule
+
+and ('self, 'trec, 'a) ty_tree =
+| Node : ('trn, 'trs, 'trb, 'tr) ty_and_rec3 * ('self, 'trn, 'trs, 'trb, 'b, 'a) ty_node -> ('self, 'tr, 'a) ty_tree
+| LocAct : 'k * 'k list -> ('self, ty_norec, 'k) ty_tree
+| DeadEnd : ('self, ty_norec, 'k) ty_tree
+
+and ('self, 'trec, 'trecs, 'trecb, 'a, 'r) ty_node = {
+  node : ('self, 'trec, 'a) ty_symbol;
+  son : ('self, 'trecs, 'a -> 'r) ty_tree;
+  brother : ('self, 'trecb, 'r) ty_tree;
 }
 
+type 'a ty_rules =
+| TRules : (_, ty_norec, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_rules
+
 type 'a ty_production =
-| TProd : ('a, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production
+| TProd : ('a, _, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production
 
-let rec derive_eps : type s a. (s, a) ty_symbol -> bool =
+let rec derive_eps : type s r a. (s, r, a) ty_symbol -> bool =
   function
     Slist0 _ -> true
   | Slist0sep (_, _, _) -> true
@@ -142,14 +165,14 @@ let rec derive_eps : type s a. (s, a) ty_symbol -> bool =
   | Stree t -> tree_derive_eps t
   | Slist1 _ -> false
   | Slist1sep (_, _, _) -> false
-  | Snterm _ | Snterml (_, _) -> false
+  | Snterm _ -> false | Snterml (_, _) -> false
   | Snext -> false
   | Sself -> false
   | Stoken _ -> false
-and tree_derive_eps : type s a. (s, a) ty_tree -> bool =
+and tree_derive_eps : type s tr a. (s, tr, a) ty_tree -> bool =
   function
     LocAct (_, _) -> true
-  | Node {node = s; brother = bro; son = son} ->
+  | Node (_, {node = s; brother = bro; son = son}) ->
       derive_eps s && tree_derive_eps son || tree_derive_eps bro
   | DeadEnd -> false
 
@@ -158,7 +181,7 @@ let eq_entry : type a1 a2. a1 ty_entry -> a2 ty_entry -> (a1, a2) eq option = fu
   if (Obj.magic e1) == (Obj.magic e2) then Some (Obj.magic Refl)
   else None
 
-let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 ->
+let rec eq_symbol : type s r1 r2 a1 a2. (s, r1, a1) ty_symbol -> (s, r2, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 ->
   match s1, s2 with
     Snterm e1, Snterm e2 -> eq_entry e1 e2
   | Snterml (e1, l1), Snterml (e2, l2) ->
@@ -188,23 +211,42 @@ let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1,
   | Stree _, Stree _ -> None
   | Sself, Sself -> Some Refl
   | Snext, Snext -> Some Refl
-  | Stoken p1, Stoken p2 -> if p1 = p2 then Some Refl else None
+  | Stoken p1, Stoken p2 -> L.tok_pattern_eq p1 p2
   | _ -> None
 
-let is_before : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 ->
+let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) ty_symbol -> bool = fun s1 s2 ->
   match s1, s2 with
-    Stoken ("ANY", _), _ -> false
-  | _, Stoken ("ANY", _) -> true
-  | Stoken (_, Some _), Stoken (_, None) -> true
-  | Stoken _, Stoken _ -> false
+  | Stoken p1, Stoken p2 ->
+     snd (L.tok_pattern_strings p1) <> None
+     && snd (L.tok_pattern_strings p2) = None
   | Stoken _, _ -> true
   | _ -> false
 
 (** Ancilliary datatypes *)
 
-type ('self, _) ty_symbols =
-| TNil : ('self, unit) ty_symbols
-| TCns : ('self, 'a) ty_symbol * ('self, 'b) ty_symbols -> ('self, 'a * 'b) ty_symbols
+type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec
+
+type ('a, 'b, 'c) ty_and_ex =
+| NR00 : (ty_mayrec, ty_mayrec, ty_mayrec) ty_and_ex
+| NR01 : (ty_mayrec, ty_norec, ty_mayrec) ty_and_ex
+| NR10 : (ty_norec, ty_mayrec, ty_mayrec) ty_and_ex
+| NR11 : (ty_norec, ty_norec, ty_norec) ty_and_ex
+
+type ('a, 'b) ty_mayrec_and_ex =
+| MayRecNR : ('a, 'b, _) ty_and_ex -> ('a, 'b) ty_mayrec_and_ex
+
+type ('s, 'a) ty_mayrec_symbol =
+| MayRecSymbol : ('s, _, 'a) ty_symbol -> ('s, 'a) ty_mayrec_symbol
+
+type ('s, 'a) ty_mayrec_tree =
+| MayRecTree : ('s, 'tr, 'a) ty_tree -> ('s, 'a) ty_mayrec_tree
+
+type ('s, 'a, 'r) ty_mayrec_rule =
+| MayRecRule : ('s, _, 'a, 'r) ty_rule -> ('s, 'a, 'r) ty_mayrec_rule
+
+type ('self, 'trec, _) ty_symbols =
+| TNil : ('self, ty_norec, unit) ty_symbols
+| TCns : ('trh, 'trt, 'tr) ty_and_rec * ('self, 'trh, 'a) ty_symbol * ('self, 'trt, 'b) ty_symbols -> ('self, 'tr, 'a * 'b) ty_symbols
 
 (** ('i, 'p, 'f, 'r) rel_prod0 ~
   ∃ α₁ ... αₙ.
@@ -217,99 +259,196 @@ type ('i, _, 'f, _) rel_prod0 =
 
 type ('p, 'k, 'r) rel_prod = (unit, 'p, 'k, 'r) rel_prod0
 
-type ('s, 'i, 'k, 'r) any_symbols =
-| AnyS : ('s, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'i, 'k, 'r) any_symbols
-
-(** FIXME *)
-let rec symbols : type s p k r. (s, p) ty_symbols -> (s, k, r) ty_rule -> (s, unit, k, r) any_symbols =
-  fun accu r -> match r with
-  | TStop -> AnyS (Obj.magic accu, Rel0)
-  | TNext (r, s) ->
-    let AnyS (r, pf) = symbols (TCns (s, accu)) r in
-    AnyS (Obj.magic r, RelS (Obj.magic pf))
-
-let get_symbols : type s k r. (s, k, r) ty_rule -> (s, unit, k, r) any_symbols =
-  fun r -> symbols TNil r
-
-let insert_tree (type s p k a) ~warning entry_name (gsymbols : (s, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, a) ty_tree) =
-  let rec insert : type p f k. (s, p) ty_symbols -> (p, k, f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree  =
-    fun symbols pf tree action ->
+type ('s, 'tr, 'i, 'k, 'r) any_symbols =
+| AnyS : ('s, 'tr, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'tr, 'i, 'k, 'r) any_symbols
+
+type ('s, 'tr, 'k, 'r) ty_belast_rule =
+| Belast : ('trr, 'trs, 'tr) ty_and_rec * ('s, 'trr, 'k, 'a -> 'r) ty_rule * ('s, 'trs, 'a) ty_symbol -> ('s, 'tr, 'k, 'r) ty_belast_rule
+
+(* unfortunately, this is quadratic, but ty_rules aren't too long
+ * (99% of the time of length less or equal 10 and maximum is 22
+ * when compiling Coq and its standard library) *)
+let rec get_symbols : type s trec k r. (s, trec, k, r) ty_rule -> (s, trec, unit, k, r) any_symbols =
+  let rec belast_rule : type s trr trs tr a k r. (trr, trs, tr) ty_and_rec -> (s, trr, k, r) ty_rule -> (s, trs, a) ty_symbol -> (s, tr, a -> k, r) ty_belast_rule =
+    fun ar r s -> match ar, r with
+    | NoRec2, TStop -> Belast (NoRec2, TStop, s)
+    | MayRec2, TStop -> Belast (MayRec2, TStop, s)
+    | NoRec2, TNext (NoRec2, r, s') ->
+       let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in
+       Belast (NoRec2, TNext (NoRec2, r, s), s')
+    | MayRec2, TNext (_, r, s') ->
+       let Belast (_, r, s') = belast_rule MayRec2 r s' in
+       Belast (MayRec2, TNext (MayRec2, r, s), s') in
+  function
+  | TStop -> AnyS (TNil, Rel0)
+  | TNext (MayRec2, r, s) ->
+     let Belast (MayRec2, r, s) = belast_rule MayRec2 r s in
+     let AnyS (r, pf) = get_symbols r in
+     AnyS (TCns (MayRec2, s, r), RelS pf)
+  | TNext (NoRec2, r, s) ->
+     let Belast (NoRec2, r, s) = belast_rule NoRec2 r s in
+     let AnyS (r, pf) = get_symbols r in
+     AnyS (TCns (NoRec2, s, r), RelS pf)
+
+let get_rec_symbols (type s tr p) (s : (s, tr, p) ty_symbols) : tr ty_rec =
+  match s with TCns (MayRec2, _, _) -> MayRec
+  | TCns (NoRec2, _, _) -> NoRec | TNil -> NoRec
+
+let get_rec_tree (type s tr f) (s : (s, tr, f) ty_tree) : tr ty_rec =
+  match s with Node (MayRec3, _) -> MayRec
+  | Node (NoRec3, _) -> NoRec | LocAct _ -> NoRec | DeadEnd -> NoRec
+
+let and_symbols_tree (type s trs trt p f) (s : (s, trs, p) ty_symbols) (t : (s, trt, f) ty_tree) : (trs, trt) ty_mayrec_and_ex =
+  match get_rec_symbols s, get_rec_tree t with
+  | MayRec, MayRec -> MayRecNR NR00 | MayRec, NoRec -> MayRecNR NR01
+  | NoRec, MayRec -> MayRecNR NR10 | NoRec, NoRec -> MayRecNR NR11
+
+let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_rec) (arn : (trn, trs, trb, trt) ty_and_rec3) (t : (s, trb, f) ty_tree) : (tr', trb, tr) ty_and_rec =
+  match ar, arn, get_rec_tree t with
+  | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2
+  | NoRec2, NoRec3, NoRec -> NoRec2
+
+let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree =
+  let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree  =
+    fun ar symbols pf tree action ->
     match symbols, pf with
-      TCns (s, sl), RelS pf -> insert_in_tree s sl pf tree action
+      TCns (ars, s, sl), RelS pf -> insert_in_tree ar ars s sl pf tree action
     | TNil, Rel0 ->
-        match tree with
-          Node {node = s; son = son; brother = bro} ->
-            Node {node = s; son = son; brother = insert TNil Rel0 bro action}
-        | LocAct (old_action, action_list) ->
+        let node (type tb) ({node = s; son = son; brother = bro} : (_, _, _, tb, _, _) ty_node) =
+          let ar : (ty_norec, tb, tb) ty_and_ex =
+            match get_rec_tree bro with MayRec -> NR10 | NoRec -> NR11 in
+          {node = s; son = son; brother = insert ar TNil Rel0 bro action} in
+        match ar, tree with
+        | NR10, Node (_, n) -> Node (MayRec3, node n)
+        | NR11, Node (NoRec3, n) -> Node (NoRec3, node n)
+        | NR11, LocAct (old_action, action_list) ->
           begin match warning with
             | None -> ()
             | Some warn_fn ->
               let msg =
                 "<W> Grammar extension: " ^
-                (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^
+                (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^
                 "some rule has been masked" in
               warn_fn msg
           end;
           LocAct (action, old_action :: action_list)
-        | DeadEnd -> LocAct (action, [])
-  and insert_in_tree : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree =
-    fun s sl pf tree action ->
-    match try_insert s sl pf tree action with
+        | NR11, DeadEnd -> LocAct (action, [])
+  and insert_in_tree : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_ex -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree =
+    fun ar ars s sl pf tree action ->
+    let ar : (trs'', trt, tr) ty_and_rec = match ar with NR11 -> NoRec2
+      | NR00 -> MayRec2 | NR01 -> MayRec2 | NR10 -> MayRec2 in
+    match try_insert ar ars s sl pf tree action with
       Some t -> t
-    | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = tree}
-  and try_insert : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree option =
-    fun s sl pf tree action ->
+    | None ->
+       let node ar =
+         {node = s; son = insert ar sl pf DeadEnd action; brother = tree} in
+       match ar, ars, get_rec_symbols sl with
+       | MayRec2, MayRec2, MayRec -> Node (MayRec3, node NR01)
+       | MayRec2, _, NoRec -> Node (MayRec3, node NR11)
+       | NoRec2, NoRec2, NoRec -> Node (NoRec3, node NR11)
+  and try_insert : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_rec -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree option =
+    fun ar ars s sl pf tree action ->
     match tree with
-      Node {node = s1; son = son; brother = bro} ->
+      Node (arn, {node = s1; son = son; brother = bro}) ->
         begin match eq_symbol s s1 with
         | Some Refl ->
-          let t = Node {node = s1; son = insert sl pf son action; brother = bro} in
-          Some t
+          let MayRecNR arss = and_symbols_tree sl son in
+          let son = insert arss sl pf son action in
+          let node = {node = s1; son = son; brother = bro} in
+          begin match ar, ars, arn, arss with
+          | MayRec2, _, _, _ -> Some (Node (MayRec3, node))
+          | NoRec2, NoRec2, NoRec3, NR11 -> Some (Node (NoRec3, node)) end
         | None ->
+        let ar' = and_and_tree ar arn bro in
         if is_before s1 s || derive_eps s && not (derive_eps s1) then
           let bro =
-            match try_insert s sl pf bro action with
+            match try_insert ar' ars s sl pf bro action with
               Some bro -> bro
-            | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = bro}
+            | None ->
+                let MayRecNR arss = and_symbols_tree sl DeadEnd in
+                let son = insert arss sl pf DeadEnd action in
+                let node = {node = s; son = son; brother = bro} in
+                match ar, ars, arn, arss with
+                | MayRec2, _, _, _ -> Node (MayRec3, node)
+                | NoRec2, NoRec2, NoRec3, NR11 -> Node (NoRec3, node)
           in
-          let t = Node {node = s1; son = son; brother = bro} in Some t
+          let node = {node = s1; son = son; brother = bro} in
+          match ar, arn with
+            | MayRec2, _ -> Some (Node (MayRec3, node))
+            | NoRec2, NoRec3 -> Some (Node (NoRec3, node))
         else
-          begin match try_insert s sl pf bro action with
+          match try_insert ar' ars s sl pf bro action with
             Some bro ->
-              let t = Node {node = s1; son = son; brother = bro} in Some t
+              let node = {node = s1; son = son; brother = bro} in
+              begin match ar, arn with
+                | MayRec2, _ -> Some (Node (MayRec3, node))
+                | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) end
           | None -> None
-          end
         end
-    | LocAct (_, _) | DeadEnd -> None
+    | LocAct (_, _) -> None | DeadEnd -> None
   in
-  insert gsymbols pf tree action
+  insert ar gsymbols pf tree action
 
-let srules (type self a) ~warning (rl : a ty_production list) =
+let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, ty_norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, ty_norec, a) ty_tree) : (s, ty_norec, a) ty_tree =
+  insert_tree ~warning entry_name NR11 gsymbols pf action tree
+
+let insert_tree (type s trs trt p k a) ~warning entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree =
+  let MayRecNR ar = and_symbols_tree gsymbols tree in
+  MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree)
+
+let srules (type self a) ~warning (rl : a ty_rules list) : (self, ty_norec, a) ty_symbol =
+  let rec retype_tree : type s a. (s, ty_norec, a) ty_tree -> (self, ty_norec, a) ty_tree =
+    function
+    | Node (NoRec3, {node = s; son = son; brother = bro}) ->
+      Node (NoRec3, {node = retype_symbol s; son = retype_tree son; brother = retype_tree bro})
+    | LocAct (k, kl) -> LocAct (k, kl)
+    | DeadEnd -> DeadEnd
+  and retype_symbol : type s a. (s, ty_norec, a) ty_symbol -> (self, ty_norec, a) ty_symbol =
+    function
+    | Stoken p -> Stoken p
+    | Slist1 s -> Slist1 (retype_symbol s)
+    | Slist1sep (s, sep, b) -> Slist1sep (retype_symbol s, retype_symbol sep, b)
+    | Slist0 s -> Slist0 (retype_symbol s)
+    | Slist0sep (s, sep, b) -> Slist0sep (retype_symbol s, retype_symbol sep, b)
+    | Sopt s -> Sopt (retype_symbol s)
+    | Snterm e -> Snterm e
+    | Snterml (e, l) -> Snterml (e, l)
+    | Stree t -> Stree (retype_tree t) in
+  let rec retype_rule : type s k r. (s, ty_norec, k, r) ty_rule -> (self, ty_norec, k, r) ty_rule =
+    function
+    | TStop -> TStop
+    | TNext (NoRec2, r, s) -> TNext (NoRec2, retype_rule r, retype_symbol s) in
   let t =
     List.fold_left
-      (fun tree (TProd (symbols, action)) ->
+      (fun tree (TRules (symbols, action)) ->
+        let symbols = retype_rule symbols in
         let AnyS (symbols, pf) = get_symbols symbols in
-        insert_tree ~warning "" symbols pf action tree)
+        insert_tree_norec ~warning "" symbols pf action tree)
       DeadEnd rl
   in
-  (* FIXME: use an universal self type to ensure well-typedness *)
-  (Obj.magic (Stree t) : (self, a) ty_symbol)
+  Stree t
 
-let is_level_labelled n lev =
+let is_level_labelled n (Level lev) =
   match lev.lname with
     Some n1 -> n = n1
   | None -> false
 
-let insert_level (type s p k) ~warning entry_name (symbols : (s, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
+let insert_level (type s tr p k) ~warning entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
   match symbols with
-  | TCns (Sself, symbols) ->
+  | TCns (_, Sself, symbols) ->
+      let Level slev = slev in
       let RelS pf = pf in
+      let MayRecTree lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix in
+      Level
       {assoc = slev.assoc; lname = slev.lname;
-       lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix;
+       lsuffix = lsuffix;
        lprefix = slev.lprefix}
   | _ ->
+      let Level slev = slev in
+      let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in
+      Level
       {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix;
-       lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix}
+       lprefix = lprefix}
 
 let empty_lev lname assoc =
   let assoc =
@@ -317,9 +456,10 @@ let empty_lev lname assoc =
       Some a -> a
     | None -> LeftA
   in
+  Level
   {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd}
 
-let change_lev ~warning lev n lname assoc =
+let change_lev ~warning (Level lev) n lname assoc =
   let a =
     match assoc with
       None -> lev.assoc
@@ -343,6 +483,7 @@ let change_lev ~warning lev n lname assoc =
         end;
   | None -> ()
   end;
+  Level
   {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
 
 let get_level ~warning entry position levs =
@@ -396,21 +537,24 @@ let get_level ~warning entry position levs =
         lev :: levs -> [], change_lev ~warning lev "<top>", levs
       | [] -> [], empty_lev, []
 
-let change_to_self0 (type s) (type a) (entry : s ty_entry) : (s, a) ty_symbol -> (s, a) ty_symbol =
+let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol =
   function
   | Snterm e ->
       begin match eq_entry e entry with
-      | None -> Snterm e
-      | Some Refl -> Sself
+      | None -> MayRecSymbol (Snterm e)
+      | Some Refl -> MayRecSymbol (Sself)
       end
-  | x -> x
+  | x -> MayRecSymbol x
 
-let rec change_to_self : type s a r. s ty_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with
-| TStop -> TStop
-| TNext (r, t) -> TNext (change_to_self e r, change_to_self0 e t)
+let rec change_to_self : type s trec a r. s ty_entry -> (s, trec, a, r) ty_rule -> (s, a, r) ty_mayrec_rule = fun e r -> match r with
+| TStop -> MayRecRule TStop
+| TNext (_, r, t) ->
+  let MayRecRule r = change_to_self e r in
+  let MayRecSymbol t = change_to_self0 e t in
+  MayRecRule (TNext (MayRec2, r, t))
 
 let insert_tokens gram symbols =
-  let rec insert : type s a. (s, a) ty_symbol -> unit =
+  let rec insert : type s trec a. (s, trec, a) ty_symbol -> unit =
     function
     | Slist0 s -> insert s
     | Slist1 s -> insert s
@@ -418,25 +562,25 @@ let insert_tokens gram symbols =
     | Slist1sep (s, t, _) -> insert s; insert t
     | Sopt s -> insert s
     | Stree t -> tinsert t
-    | Stoken ("ANY", _) -> ()
     | Stoken tok ->
-        gram.glexer.Plexing.tok_using tok;
+        L.tok_using tok;
         let r =
+          let tok = L.tok_pattern_strings tok in
           try Hashtbl.find gram.gtokens tok with
             Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r
         in
         incr r
-    | Snterm _ | Snterml (_, _) -> ()
+    | Snterm _ -> () | Snterml (_, _) -> ()
     | Snext -> ()
     | Sself -> ()
-  and tinsert : type s a. (s, a) ty_tree -> unit =
+  and tinsert : type s tr a. (s, tr, a) ty_tree -> unit =
     function
-      Node {node = s; brother = bro; son = son} ->
+      Node (_, {node = s; brother = bro; son = son}) ->
         insert s; tinsert bro; tinsert son
-    | LocAct (_, _) | DeadEnd -> ()
-  and linsert : type s p. (s, p) ty_symbols -> unit = function
+    | LocAct (_, _) -> () | DeadEnd -> ()
+  and linsert : type s tr p. (s, tr, p) ty_symbols -> unit = function
   | TNil -> ()
-  | TCns (s, r) -> insert s; linsert r
+  | TCns (_, s, r) -> insert s; linsert r
   in
   linsert symbols
 
@@ -460,7 +604,7 @@ let levels_of_rules ~warning entry position rules =
            let lev =
              List.fold_left
                (fun lev (TProd (symbols, action)) ->
-                  let symbols = change_to_self entry symbols in
+                  let MayRecRule symbols = change_to_self entry symbols in
                   let AnyS (symbols, pf) = get_symbols symbols in
                   insert_tokens egram symbols;
                   insert_level ~warning entry.ename symbols pf action lev)
@@ -472,7 +616,7 @@ let levels_of_rules ~warning entry position rules =
     levs1 @ List.rev levs @ levs2
 
 let logically_eq_symbols entry =
-  let rec eq_symbols : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 ->
+  let rec eq_symbols : type s1 s2 trec1 trec2 a1 a2. (s1, trec1, a1) ty_symbol -> (s2, trec2, a2) ty_symbol -> bool = fun s1 s2 ->
     match s1, s2 with
       Snterm e1, Snterm e2 -> e1.ename = e2.ename
     | Snterm e1, Sself -> e1.ename = entry.ename
@@ -486,16 +630,19 @@ let logically_eq_symbols entry =
         eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2
     | Sopt s1, Sopt s2 -> eq_symbols s1 s2
     | Stree t1, Stree t2 -> eq_trees t1 t2
-    | Stoken p1, Stoken p2 -> p1 = p2
+    | Stoken p1, Stoken p2 -> L.tok_pattern_eq p1 p2 <> None
     | Sself, Sself -> true
     | Snext, Snext -> true
     | _ -> false
-  and eq_trees : type s1 s2 a1 a2. (s1, a1) ty_tree -> (s2, a2) ty_tree -> bool = fun t1 t2 ->
+  and eq_trees : type s1 s2 tr1 tr2 a1 a2. (s1, tr1, a1) ty_tree -> (s2, tr2, a2) ty_tree -> bool = fun t1 t2 ->
     match t1, t2 with
-      Node n1, Node n2 ->
+      Node (_, n1), Node (_, n2) ->
         eq_symbols n1.node n2.node && eq_trees n1.son n2.son &&
         eq_trees n1.brother n2.brother
-    | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true
+    | LocAct _, LocAct _ -> true
+    | LocAct _, DeadEnd -> true
+    | DeadEnd, LocAct _ -> true
+    | DeadEnd, DeadEnd -> true
     | _ -> false
   in
   eq_symbols
@@ -509,55 +656,56 @@ let logically_eq_symbols entry =
      [None] if failure *)
 
 type 's ex_symbols =
-| ExS : ('s, 'p) ty_symbols -> 's ex_symbols
+| ExS : ('s, 'tr, 'p) ty_symbols -> 's ex_symbols
 
 let delete_rule_in_tree entry =
   let rec delete_in_tree :
-    type s p r. (s, p) ty_symbols -> (s, r) ty_tree -> (s ex_symbols option * (s, r) ty_tree) option =
+    type s tr tr' p r. (s, tr, p) ty_symbols -> (s, tr', r) ty_tree -> (s ex_symbols option * (s, r) ty_mayrec_tree) option =
     fun symbols tree ->
     match symbols, tree with
-    | TCns (s, sl), Node n ->
+    | TCns (_, s, sl), Node (_, n) ->
         if logically_eq_symbols entry s n.node then delete_son sl n
         else
           begin match delete_in_tree symbols n.brother with
-            Some (dsl, t) ->
-              Some (dsl, Node {node = n.node; son = n.son; brother = t})
+            Some (dsl, MayRecTree t) ->
+              Some (dsl, MayRecTree (Node (MayRec3, {node = n.node; son = n.son; brother = t})))
           | None -> None
           end
-    | TCns (s, sl), _ -> None
-    | TNil, Node n ->
+    | TCns (_, s, sl), _ -> None
+    | TNil, Node (_, n) ->
         begin match delete_in_tree TNil n.brother with
-          Some (dsl, t) ->
-            Some (dsl, Node {node = n.node; son = n.son; brother = t})
+          Some (dsl, MayRecTree t) ->
+            Some (dsl, MayRecTree (Node (MayRec3, {node = n.node; son = n.son; brother = t})))
         | None -> None
         end
     | TNil, DeadEnd -> None
-    | TNil, LocAct (_, []) -> Some (Some (ExS TNil), DeadEnd)
-    | TNil, LocAct (_, action :: list) -> Some (None, LocAct (action, list))
+    | TNil, LocAct (_, []) -> Some (Some (ExS TNil), MayRecTree DeadEnd)
+    | TNil, LocAct (_, action :: list) -> Some (None, MayRecTree (LocAct (action, list)))
   and delete_son :
-    type s p a r. (s, p) ty_symbols -> (s, a, r) ty_node -> (s ex_symbols option * (s, r) ty_tree) option =
+    type s p tr trn trs trb a r. (s, tr, p) ty_symbols -> (s, trn, trs, trb, a, r) ty_node -> (s ex_symbols option * (s, r) ty_mayrec_tree) option =
     fun sl n ->
     match delete_in_tree sl n.son with
-      Some (Some (ExS dsl), DeadEnd) -> Some (Some (ExS (TCns (n.node, dsl))), n.brother)
-    | Some (Some (ExS dsl), t) ->
-        let t = Node {node = n.node; son = t; brother = n.brother} in
-        Some (Some (ExS (TCns (n.node, dsl))), t)
-    | Some (None, t) ->
-        let t = Node {node = n.node; son = t; brother = n.brother} in
-        Some (None, t)
+      Some (Some (ExS dsl), MayRecTree DeadEnd) -> Some (Some (ExS (TCns (MayRec2, n.node, dsl))), MayRecTree n.brother)
+    | Some (Some (ExS dsl), MayRecTree t) ->
+        let t = Node (MayRec3, {node = n.node; son = t; brother = n.brother}) in
+        Some (Some (ExS (TCns (MayRec2, n.node, dsl))), MayRecTree t)
+    | Some (None, MayRecTree t) ->
+        let t = Node (MayRec3, {node = n.node; son = t; brother = n.brother}) in
+        Some (None, MayRecTree t)
     | None -> None
   in
   delete_in_tree
 
-let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram ->
+let rec decr_keyw_use : type s tr a. _ -> (s, tr, a) ty_symbol -> unit = fun gram ->
   function
     Stoken tok ->
-      let r = Hashtbl.find gram.gtokens tok in
+      let tok' = L.tok_pattern_strings tok in
+      let r = Hashtbl.find gram.gtokens tok' in
       decr r;
       if !r == 0 then
         begin
-          Hashtbl.remove gram.gtokens tok;
-          gram.glexer.Plexing.tok_removing tok
+          Hashtbl.remove gram.gtokens tok';
+          L.tok_removing tok
         end
   | Slist0 s -> decr_keyw_use gram s
   | Slist1 s -> decr_keyw_use gram s
@@ -567,69 +715,71 @@ let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram ->
   | Stree t -> decr_keyw_use_in_tree gram t
   | Sself -> ()
   | Snext -> ()
-  | Snterm _ | Snterml (_, _) -> ()
-and decr_keyw_use_in_tree : type s a. _ -> (s, a) ty_tree -> unit = fun gram ->
+  | Snterm _ -> () | Snterml (_, _) -> ()
+and decr_keyw_use_in_tree : type s tr a. _ -> (s, tr, a) ty_tree -> unit = fun gram ->
   function
-    DeadEnd | LocAct (_, _) -> ()
-  | Node n ->
+    DeadEnd -> () | LocAct (_, _) -> ()
+  | Node (_, n) ->
       decr_keyw_use gram n.node;
       decr_keyw_use_in_tree gram n.son;
       decr_keyw_use_in_tree gram n.brother
-and decr_keyw_use_in_list : type s p. _ -> (s, p) ty_symbols -> unit = fun gram ->
+and decr_keyw_use_in_list : type s tr p. _ -> (s, tr, p) ty_symbols -> unit = fun gram ->
   function
   | TNil -> ()
-  | TCns (s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l
+  | TCns (_, s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l
 
 let rec delete_rule_in_suffix entry symbols =
   function
-    lev :: levs ->
+    Level lev :: levs ->
       begin match delete_rule_in_tree entry symbols lev.lsuffix with
-        Some (dsl, t) ->
+        Some (dsl, MayRecTree t) ->
           begin match dsl with
             Some (ExS dsl) -> decr_keyw_use_in_list egram dsl
           | None -> ()
           end;
-          begin match t with
-            DeadEnd when lev.lprefix == DeadEnd -> levs
+          begin match t, lev.lprefix with
+            DeadEnd, DeadEnd -> levs
           | _ ->
               let lev =
                 {assoc = lev.assoc; lname = lev.lname; lsuffix = t;
                  lprefix = lev.lprefix}
               in
-              lev :: levs
+              Level lev :: levs
           end
       | None ->
-          let levs = delete_rule_in_suffix entry symbols levs in lev :: levs
+          let levs = delete_rule_in_suffix entry symbols levs in
+          Level lev :: levs
       end
   | [] -> raise Not_found
 
 let rec delete_rule_in_prefix entry symbols =
   function
-    lev :: levs ->
+    Level lev :: levs ->
       begin match delete_rule_in_tree entry symbols lev.lprefix with
-        Some (dsl, t) ->
+        Some (dsl, MayRecTree t) ->
           begin match dsl with
             Some (ExS dsl) -> decr_keyw_use_in_list egram dsl
           | None -> ()
           end;
-          begin match t with
-            DeadEnd when lev.lsuffix == DeadEnd -> levs
+          begin match t, lev.lsuffix with
+            DeadEnd, DeadEnd -> levs
           | _ ->
               let lev =
                 {assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix;
                  lprefix = t}
               in
-              lev :: levs
+              Level lev :: levs
           end
       | None ->
-          let levs = delete_rule_in_prefix entry symbols levs in lev :: levs
+          let levs = delete_rule_in_prefix entry symbols levs in
+          Level lev :: levs
       end
   | [] -> raise Not_found
 
-let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p) ty_symbols) levs =
+let delete_rule_in_level_list (type s tr p) (entry : s ty_entry) (symbols : (s, tr, p) ty_symbols) levs =
   match symbols with
-    TCns (Sself, symbols) -> delete_rule_in_suffix entry symbols levs
-  | TCns (Snterm e, symbols') ->
+    TCns (_, Sself, symbols) -> delete_rule_in_suffix entry symbols levs
+  | TCns (_, Snterm e, symbols') ->
     begin match eq_entry e entry with
     | None -> delete_rule_in_prefix entry symbols levs
     | Some Refl ->
@@ -637,12 +787,12 @@ let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p)
     end
   | _ -> delete_rule_in_prefix entry symbols levs
 
-let rec flatten_tree : type s a. (s, a) ty_tree -> s ex_symbols list =
+let rec flatten_tree : type s tr a. (s, tr, a) ty_tree -> s ex_symbols list =
   function
     DeadEnd -> []
   | LocAct (_, _) -> [ExS TNil]
-  | Node {node = n; brother = b; son = s} ->
-      List.map (fun (ExS l) -> ExS (TCns (n, l))) (flatten_tree s) @ flatten_tree b
+  | Node (_, {node = n; brother = b; son = s}) ->
+      List.map (fun (ExS l) -> ExS (TCns (MayRec2, n, l))) (flatten_tree s) @ flatten_tree b
 
 let utf8_print = ref true
 
@@ -671,7 +821,7 @@ let string_escaped s =
 
 let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s)
 
-let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit =
+let rec print_symbol : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit =
   fun ppf ->
   function
   | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s
@@ -683,30 +833,36 @@ let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit =
       fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t
         (if osep then " OPT_SEP" else "")
   | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s
-  | Stoken (con, Some prm) when con <> "" ->
-      fprintf ppf "%s@ %a" con print_str prm
+  | Stoken p when L.tok_pattern_strings p <> ("", None) ->
+     begin match L.tok_pattern_strings p with
+     | con, Some prm -> fprintf ppf "%s@ %a" con print_str prm
+     | con, None -> fprintf ppf "%s" con end
   | Snterml (e, l) ->
       fprintf ppf "%s%s@ LEVEL@ %a" e.ename ""
         print_str l
   | s -> print_symbol1 ppf s
-and print_symbol1 : type s r. formatter -> (s, r) ty_symbol -> unit =
+and print_symbol1 : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit =
   fun ppf ->
   function
   | Snterm e -> fprintf ppf "%s%s" e.ename ""
   | Sself -> pp_print_string ppf "SELF"
   | Snext -> pp_print_string ppf "NEXT"
-  | Stoken ("", Some s) -> print_str ppf s
-  | Stoken (con, None) -> pp_print_string ppf con
+  | Stoken p ->
+     begin match L.tok_pattern_strings p with
+     | "", Some s -> print_str ppf s
+     | con, None -> pp_print_string ppf con
+     | con, Some prm -> fprintf ppf "(%s@ %a)" con print_str prm end
   | Stree t -> print_level ppf pp_print_space (flatten_tree t)
   | s ->
       fprintf ppf "(%a)" print_symbol s
-and print_rule : type s p. formatter -> (s, p) ty_symbols -> unit =
+and print_rule : type s tr p. formatter -> (s, tr, p) ty_symbols -> unit =
   fun ppf symbols ->
   fprintf ppf "@[<hov 0>";
-  let rec fold : type s p. _ -> (s, p) ty_symbols -> unit =
-    fun sep symbols -> match symbols with
+  let rec fold : type s tr p. _ -> (s, tr, p) ty_symbols -> unit =
+    fun sep symbols ->
+    match symbols with
     | TNil -> ()
-    | TCns (symbol, symbols) ->
+    | TCns (_, symbol, symbols) ->
       fprintf ppf "%t%a" sep print_symbol symbol;
       fold (fun ppf -> fprintf ppf ";@ ") symbols
   in
@@ -727,9 +883,9 @@ and print_level : type s. _ -> _ -> s ex_symbols list -> _ =
 let print_levels ppf elev =
   let _ =
     List.fold_left
-      (fun sep lev ->
+      (fun sep (Level lev) ->
          let rules =
-           List.map (fun (ExS t) -> ExS (TCns (Sself, t))) (flatten_tree lev.lsuffix) @
+           List.map (fun (ExS t) -> ExS (TCns (MayRec2, Sself, t))) (flatten_tree lev.lsuffix) @
            flatten_tree lev.lprefix
          in
          fprintf ppf "%t@[<hov 2>" sep;
@@ -765,31 +921,39 @@ let loc_of_token_interval bp ep =
   else
     let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2
 
-let name_of_symbol : type s a. s ty_entry -> (s, a) ty_symbol -> string =
+let name_of_symbol : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> string =
   fun entry ->
   function
     Snterm e -> "[" ^ e.ename ^ "]"
   | Snterml (e, l) -> "[" ^ e.ename ^ " level " ^ l ^ "]"
   | Sself -> "[" ^ entry.ename ^ "]"
   | Snext -> "[" ^ entry.ename ^ "]"
-  | Stoken tok -> egram.glexer.Plexing.tok_text tok
+  | Stoken tok -> L.tok_text tok
   | _ -> "???"
 
 type ('r, 'f) tok_list =
 | TokNil : ('f, 'f) tok_list
-| TokCns : ('r, 'f) tok_list -> (string -> 'r, 'f) tok_list
+| TokCns : 'a pattern * ('r, 'f) tok_list -> ('a -> 'r, 'f) tok_list
+
+type ('s, 'f) tok_tree = TokTree : 'a pattern * ('s, _, 'a -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree
 
-type ('s, 'f) tok_tree = TokTree : ('s, string -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree
+let rec tok_list_length : type a b. (a, b) tok_list -> int =
+  function
+  | TokNil -> 0
+  | TokCns (_, t) -> 1 + tok_list_length t
 
-let rec get_token_list : type s r f.
-  s ty_entry -> _ -> _ -> _ -> (r, f) tok_list -> (s, string -> r) ty_tree -> (_ * _ * _ * (s, f) tok_tree) option =
-  fun entry first_tok rev_tokl last_tok pf tree ->
+let rec get_token_list : type s tr a r f.
+  s ty_entry -> a pattern -> (r, f) tok_list -> (s, tr, a -> r) ty_tree -> (s, f) tok_tree option =
+  fun entry last_tok rev_tokl tree ->
   match tree with
-    Node {node = Stoken tok; son = son; brother = DeadEnd} ->
-      get_token_list entry first_tok (last_tok :: rev_tokl) tok (TokCns pf) son
-  | _ -> if rev_tokl = [] then None else Some (first_tok, rev_tokl, last_tok, TokTree (tree, pf))
+    Node (_, {node = Stoken tok; son = son; brother = DeadEnd}) ->
+      get_token_list entry tok (TokCns (last_tok, rev_tokl)) son
+  | _ ->
+     match rev_tokl with
+     | TokNil -> None
+     | _ -> Some (TokTree (last_tok, tree, rev_tokl))
 
-let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ =
+let rec name_of_symbol_failed : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> _ =
   fun entry ->
   function
   | Slist0 s -> name_of_symbol_failed entry s
@@ -799,13 +963,13 @@ let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ =
   | Sopt s -> name_of_symbol_failed entry s
   | Stree t -> name_of_tree_failed entry t
   | s -> name_of_symbol entry s
-and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ =
+and name_of_tree_failed : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> _ =
   fun entry ->
   function
-    Node {node = s; brother = bro; son = son} ->
+    Node (_, {node = s; brother = bro; son = son}) ->
       let tokl =
         match s with
-          Stoken tok -> get_token_list entry tok [] tok TokNil son
+          Stoken tok -> get_token_list entry tok TokNil son
         | _ -> None
       in
       begin match tokl with
@@ -818,20 +982,20 @@ and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ =
           in
           let txt =
             match bro with
-              DeadEnd | LocAct (_, _) -> txt
+              DeadEnd -> txt | LocAct (_, _) -> txt
             | Node _ -> txt ^ " or " ^ name_of_tree_failed entry bro
           in
           txt
-      | Some (_, rev_tokl, last_tok, _) ->
-          List.fold_left
-            (fun s tok ->
-               (if s = "" then "" else s ^ " ") ^
-               egram.glexer.Plexing.tok_text tok)
-            "" (List.rev (last_tok :: rev_tokl))
+      | Some (TokTree (last_tok, _, rev_tokl)) ->
+         let rec build_str : type a b. string -> (a, b) tok_list -> string =
+           fun s -> function
+           | TokNil -> s
+           | TokCns (tok, t) -> build_str (L.tok_text tok ^ " " ^ s) t in
+         build_str (L.tok_text last_tok) rev_tokl
       end
-  | DeadEnd | LocAct (_, _) -> "???"
+  | DeadEnd -> "???" | LocAct (_, _) -> "???"
 
-let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, a) ty_symbol) tree =
+let tree_failed (type s tr a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, tr, a) ty_symbol) tree =
   let txt = name_of_tree_failed entry tree in
   let txt =
     match prev_symb with
@@ -866,14 +1030,9 @@ let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_sym
   txt ^ " (in [" ^ entry.ename ^ "])"
 
 let symb_failed entry prev_symb_result prev_symb symb =
-  let tree = Node {node = symb; brother = DeadEnd; son = DeadEnd} in
+  let tree = Node (MayRec3, {node = symb; brother = DeadEnd; son = DeadEnd}) in
   tree_failed entry prev_symb_result prev_symb tree
 
-let is_level_labelled n lev =
-  match lev.lname with
-    Some n1 -> n = n1
-  | None -> false
-
 let level_number entry lab =
   let rec lookup levn =
     function
@@ -885,7 +1044,7 @@ let level_number entry lab =
     Dlevels elev -> lookup 0 elev
   | Dparser _ -> raise Not_found
 
-let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol =
+let rec top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> (s, ty_norec, a) ty_symbol =
   fun entry ->
   function
     Sself -> Snterm entry
@@ -894,7 +1053,7 @@ let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol
   | Slist1sep (s, sep, b) -> Slist1sep (top_symb entry s, sep, b)
   | _ -> raise Stream.Failure
 
-let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry =
+let entry_of_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a ty_entry =
   fun entry ->
   function
     Sself -> entry
@@ -903,12 +1062,14 @@ let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry =
   | Snterml (e, _) -> e
   | _ -> raise Stream.Failure
 
-let top_tree : type s a. s ty_entry -> (s, a) ty_tree -> (s, a) ty_tree =
+let top_tree : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> (s, tr, a) ty_tree =
   fun entry ->
   function
-    Node {node = s; brother = bro; son = son} ->
-      Node {node = top_symb entry s; brother = bro; son = son}
-  | LocAct (_, _) | DeadEnd -> raise Stream.Failure
+    Node (MayRec3, {node = s; brother = bro; son = son}) ->
+      Node (MayRec3, {node = top_symb entry s; brother = bro; son = son})
+  | Node (NoRec3, {node = s; brother = bro; son = son}) ->
+      Node (NoRec3, {node = top_symb entry s; brother = bro; son = son})
+  | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
 
 let skip_if_empty bp p strm =
   if Stream.count strm == bp then fun a -> p strm
@@ -957,18 +1118,18 @@ let call_and_push ps al strm =
   let al = if !item_skipped then al else a :: al in item_skipped := false; al
 
 let token_ematch gram tok =
-  let tematch = gram.glexer.Plexing.tok_match tok in
+  let tematch = L.tok_match tok in
   fun tok -> tematch tok
 
-let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> r parser_t =
+let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_tree -> r parser_t =
   fun entry nlevn alevn ->
   function
     DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure)
   | LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act)
-  | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} ->
+  | Node (_, {node = Sself; son = LocAct (act, _); brother = DeadEnd}) ->
       (fun (strm__ : _ Stream.t) ->
          let a = entry.estart alevn strm__ in act a)
-  | Node {node = Sself; son = LocAct (act, _); brother = bro} ->
+  | Node (_, {node = Sself; son = LocAct (act, _); brother = bro}) ->
       let p2 = parser_of_tree entry nlevn alevn bro in
       (fun (strm__ : _ Stream.t) ->
          match
@@ -976,10 +1137,10 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree ->
          with
            Some a -> act a
          | _ -> p2 strm__)
-  | Node {node = s; son = son; brother = DeadEnd} ->
+  | Node (_, {node = s; son = son; brother = DeadEnd}) ->
       let tokl =
         match s with
-          Stoken tok -> get_token_list entry tok [] tok TokNil son
+          Stoken tok -> get_token_list entry tok TokNil son
         | _ -> None
       in
       begin match tokl with
@@ -996,19 +1157,16 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree ->
                    raise (Stream.Error (tree_failed entry a s son))
              in
              act a)
-      | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) ->
-          let s = Stoken first_tok in
+      | Some (TokTree (last_tok, son, rev_tokl)) ->
           let lt = Stoken last_tok in
           let p1 = parser_of_tree entry nlevn alevn son in
           let p1 = parser_cont p1 entry nlevn alevn lt son in
-          parser_of_token_list entry s son pf p1
-            (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl
-            last_tok
+          parser_of_token_list entry son p1 rev_tokl last_tok
       end
-  | Node {node = s; son = son; brother = bro} ->
+  | Node (_, {node = s; son = son; brother = bro}) ->
       let tokl =
         match s with
-          Stoken tok -> get_token_list entry tok [] tok TokNil son
+          Stoken tok -> get_token_list entry tok TokNil son
         | _ -> None
       in
       match tokl with
@@ -1028,28 +1186,28 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree ->
                  | None -> raise (Stream.Error (tree_failed entry a s son))
                  end
              | None -> p2 strm)
-      | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) ->
+      | Some (TokTree (last_tok, son, rev_tokl)) ->
           let lt = Stoken last_tok in
           let p2 = parser_of_tree entry nlevn alevn bro in
           let p1 = parser_of_tree entry nlevn alevn son in
           let p1 = parser_cont p1 entry nlevn alevn lt son in
           let p1 =
-            parser_of_token_list entry lt son pf p1 p2 rev_tokl last_tok
+            parser_of_token_list entry son p1 rev_tokl last_tok
           in
           fun (strm__ : _ Stream.t) ->
             try p1 strm__ with Stream.Failure -> p2 strm__
-and parser_cont : type s a r.
-  (a -> r) parser_t -> s ty_entry -> int -> int -> (s, a) ty_symbol -> (s, a -> r) ty_tree -> int -> a -> (a -> r) parser_t =
+and parser_cont : type s tr tr' a r.
+  (a -> r) parser_t -> s ty_entry -> int -> int -> (s, tr, a) ty_symbol -> (s, tr', a -> r) ty_tree -> int -> a -> (a -> r) parser_t =
   fun p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) ->
   try p1 strm__ with
     Stream.Failure ->
       recover parser_of_tree entry nlevn alevn bp a s son strm__
-and parser_of_token_list : type s r f.
-  s ty_entry -> (s, string) ty_symbol -> (s, string -> r) ty_tree ->
-    (r, f) tok_list -> (int -> string -> (string -> r) parser_t) -> f parser_t -> _ -> _ -> f parser_t =
-  fun entry s son pf p1 p2 rev_tokl last_tok ->
+and parser_of_token_list : type s tr lt r f.
+  s ty_entry -> (s, tr, lt -> r) ty_tree ->
+    (int -> lt -> (lt -> r) parser_t) -> (r, f) tok_list -> lt pattern -> f parser_t =
+  fun entry son p1 rev_tokl last_tok ->
+  let n = tok_list_length rev_tokl + 1 in
   let plast : r parser_t =
-    let n = List.length rev_tokl + 1 in
     let tematch = token_ematch egram last_tok in
     let ps strm =
       match peek_nth n strm with
@@ -1063,41 +1221,24 @@ and parser_of_token_list : type s r f.
       let a = ps strm in
       match try Some (p1 bp a strm) with Stream.Failure -> None with
         Some act -> act a
-      | None -> raise (Stream.Error (tree_failed entry a s son))
+      | None -> raise (Stream.Error (tree_failed entry a (Stoken last_tok) son))
   in
-  match List.rev rev_tokl, pf with
-    [], TokNil -> (fun (strm__ : _ Stream.t) -> plast strm__)
-  | tok :: tokl, TokCns pf ->
-      let tematch = token_ematch egram tok in
-      let ps strm =
-        match peek_nth 1 strm with
-          Some tok -> tematch tok
-        | None -> raise Stream.Failure
-      in
-      let p1 =
-        let rec loop : type s f. _ -> _ -> (s, f) tok_list -> (string -> s) parser_t -> (string -> f) parser_t =
-          fun n tokl pf plast ->
-          match tokl, pf with
-            [], TokNil -> plast
-          | tok :: tokl, TokCns pf ->
-              let tematch = token_ematch egram tok in
-              let ps strm =
-                match peek_nth n strm with
-                  Some tok -> tematch tok
-                | None -> raise Stream.Failure
-              in
-              let p1 = loop (n + 1) tokl pf (Obj.magic plast) in (* FIXME *)
-              fun (strm__ : _ Stream.t) ->
-                let a = ps strm__ in let act = p1 strm__ in (Obj.magic act a) (* FIXME *)
-          | _ -> assert false
-        in
-        loop 2 tokl pf plast
-      in
-      fun (strm__ : _ Stream.t) ->
-        let a = ps strm__ in let act = p1 strm__ in act a
-  | _ -> assert false
-and parser_of_symbol : type s a.
-  s ty_entry -> int -> (s, a) ty_symbol -> a parser_t =
+  let rec loop : type s f. _ -> (s, f) tok_list -> s parser_t -> f parser_t =
+    fun n tokl plast -> match tokl with
+    | TokNil -> plast
+    | TokCns (tok, tokl) ->
+       let tematch = token_ematch egram tok in
+       let ps strm =
+         match peek_nth n strm with
+           Some tok -> tematch tok
+         | None -> raise Stream.Failure
+       in
+       let plast = fun (strm : _ Stream.t) ->
+         let a = ps strm in let act = plast strm in act a in
+       loop (n - 1) tokl plast in
+  loop (n - 1) rev_tokl plast
+and parser_of_symbol : type s tr a.
+  s ty_entry -> int -> (s, tr, a) ty_symbol -> a parser_t =
   fun entry nlevn ->
   function
   | Slist0 s ->
@@ -1219,22 +1360,22 @@ and parser_of_symbol : type s a.
   | Sself -> (fun (strm__ : _ Stream.t) -> entry.estart 0 strm__)
   | Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__)
   | Stoken tok -> parser_of_token entry tok
-and parser_of_token : type s.
-  s ty_entry -> Plexing.pattern -> string parser_t =
+and parser_of_token : type s a.
+  s ty_entry -> a pattern -> a parser_t =
   fun entry tok ->
-  let f = egram.glexer.Plexing.tok_match tok in
+  let f = L.tok_match tok in
   fun strm ->
     match Stream.peek strm with
       Some tok -> let r = f tok in Stream.junk strm; r
     | None -> raise Stream.Failure
-and parse_top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a parser_t =
+and parse_top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a parser_t =
   fun entry symb ->
   parser_of_symbol entry 0 (top_symb entry symb)
 
 let rec start_parser_of_levels entry clevn =
   function
     [] -> (fun levn (strm__ : _ Stream.t) -> raise Stream.Failure)
-  | lev :: levs ->
+  | Level lev :: levs ->
       let p1 = start_parser_of_levels entry (succ clevn) levs in
       match lev.lprefix with
         DeadEnd -> p1
@@ -1277,7 +1418,7 @@ let rec start_parser_of_levels entry clevn =
 let rec continue_parser_of_levels entry clevn =
   function
     [] -> (fun levn bp a (strm__ : _ Stream.t) -> raise Stream.Failure)
-  | lev :: levs ->
+  | Level lev :: levs ->
       let p1 = continue_parser_of_levels entry (succ clevn) levs in
       match lev.lsuffix with
         DeadEnd -> p1
@@ -1399,7 +1540,7 @@ let clear_entry e =
   | Dparser _ -> ()
 
     let parsable ?loc cs =
-      let (ts, lf) = L.lexer.Plexing.tok_func ?loc cs in
+      let (ts, lf) = L.tok_func ?loc cs in
       {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
     module Entry =
       struct
@@ -1432,9 +1573,11 @@ let clear_entry e =
     let s_self = Sself
     let s_next = Snext
     let s_token tok = Stoken tok
-    let s_rules ~warning (t : 'a ty_production list) = srules ~warning t
+    let s_rules ~warning (t : 'a ty_rules list) = srules ~warning t
     let r_stop = TStop
-    let r_next r s = TNext (r, s)
+    let r_next r s = TNext (MayRec2, r, s)
+    let r_next_norec r s = TNext (NoRec2, r, s)
+    let rules (p, act) = TRules (p, act)
     let production (p, act) = TProd (p, act)
     module Unsafe =
       struct
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 453ec85187..ec4ec62409 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -15,13 +15,14 @@
        rule "an entry cannot call an entry of another grammar" by
        normal OCaml typing. *)
 
-module type GLexerType = sig type te val lexer : te Plexing.lexer end
+module type GLexerType = Plexing.Lexer
    (** The input signature for the functor [Grammar.GMake]: [te] is the
        type of the tokens. *)
 
 module type S =
   sig
     type te
+    type 'c pattern
     type parsable
     val parsable : ?loc:Loc.t -> char Stream.t -> parsable
     val tokens : string -> (string option * int) list
@@ -35,29 +36,37 @@ module type S =
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
       end
-    type ('self, 'a) ty_symbol
-    type ('self, 'f, 'r) ty_rule
+    type ty_norec = TyNoRec
+    type ty_mayrec = TyMayRec
+    type ('self, 'trec, 'a) ty_symbol
+    type ('self, 'trec, 'f, 'r) ty_rule
+    type 'a ty_rules
     type 'a ty_production
-    val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
-    val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
-    val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+    val s_nterm : 'a Entry.e -> ('self, ty_norec, 'a) ty_symbol
+    val s_nterml : 'a Entry.e -> string -> ('self, ty_norec, 'a) ty_symbol
+    val s_list0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
     val s_list0sep :
-      ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
-        ('self, 'a list) ty_symbol
-    val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+      ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+        ('self, 'trec, 'a list) ty_symbol
+    val s_list1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
     val s_list1sep :
-      ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
-        ('self, 'a list) ty_symbol
-    val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
-    val s_self : ('self, 'self) ty_symbol
-    val s_next : ('self, 'self) ty_symbol
-    val s_token : Plexing.pattern -> ('self, string) ty_symbol
-    val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
-    val r_stop : ('self, 'r, 'r) ty_rule
+      ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+        ('self, 'trec, 'a list) ty_symbol
+    val s_opt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol
+    val s_self : ('self, ty_mayrec, 'self) ty_symbol
+    val s_next : ('self, ty_mayrec, 'self) ty_symbol
+    val s_token : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+    val s_rules : warning:(string -> unit) option -> 'a ty_rules list -> ('self, ty_norec, 'a) ty_symbol
+
+    val r_stop : ('self, ty_norec, 'r, 'r) ty_rule
     val r_next :
-      ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
-        ('self, 'b -> 'a, 'r) ty_rule
-    val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
+      ('self, _, 'a, 'r) ty_rule -> ('self, _, 'b) ty_symbol ->
+        ('self, ty_mayrec, 'b -> 'a, 'r) ty_rule
+    val r_next_norec :
+      ('self, ty_norec, 'a, 'r) ty_rule -> ('self, ty_norec, 'b) ty_symbol ->
+        ('self, ty_norec, 'b -> 'a, 'r) ty_rule
+    val rules : (_, ty_norec, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_rules
+    val production : ('a, _, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
 
     module Unsafe :
       sig
@@ -68,7 +77,7 @@ module type S =
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
         unit
-    val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit
+    val safe_delete_rule : 'a Entry.e -> ('a, _, 'f, 'r) ty_rule -> unit
   end
    (** Signature type of the functor [Grammar.GMake]. The types and
        functions are almost the same than in generic interface, but:
@@ -80,4 +89,5 @@ module type S =
          type (instead of (string * string)); the module parameter
          must specify a way to show them as (string * string) *)
 
-module GMake (L : GLexerType) : S with type te = L.te
+module GMake (L : GLexerType) :
+  S with type te = L.te and type 'c pattern = 'c L.pattern
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 6da06f147f..e881ab3350 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -2,15 +2,17 @@
 (* plexing.ml,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-type pattern = string * string option
-
 type location_function = int -> Loc.t
 type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
 
-type 'te lexer =
-  { tok_func : 'te lexer_func;
-    tok_using : pattern -> unit;
-    tok_removing : pattern -> unit;
-    tok_match : pattern -> 'te -> string;
-    tok_text : pattern -> string;
-  }
+module type Lexer = sig
+  type te
+  type 'c pattern
+  val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option
+  val tok_pattern_strings : 'c pattern -> string * string option
+  val tok_func : te lexer_func
+  val tok_using : 'c pattern -> unit
+  val tok_removing : 'c pattern -> unit
+  val tok_match : 'c pattern -> te -> 'c
+  val tok_text : 'c pattern -> string
+end
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 26443df026..521eba7446 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -8,27 +8,21 @@
    grammars (see module [Grammar]). It also provides some useful functions
    to create lexers. *)
 
-type pattern = string * string option
-    (* Type for values used by the generated code of the EXTEND
-       statement to represent terminals in entry rules.
--      The first string is the constructor name (must start with
-       an uppercase character). When it is empty, the second string
-       is supposed to be a keyword.
--      The second component is the constructor parameter. None if it
-       has no parameter (corresponding to the 'wildcard' pattern).
--      The way tokens patterns are interpreted to parse tokens is done
-       by the lexer, function [tok_match] below. *)
-
 (** Lexer type *)
 
-type 'te lexer =
-  { tok_func : 'te lexer_func;
-    tok_using : pattern -> unit;
-    tok_removing : pattern -> unit;
-    tok_match : pattern -> 'te -> string;
-    tok_text : pattern -> string;
-  }
-and 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
+type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
 and location_function = int -> Loc.t
   (** The type of a function giving the location of a token in the
       source from the token number in the stream (starting from zero). *)
+
+module type Lexer = sig
+  type te
+  type 'c pattern
+  val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option
+  val tok_pattern_strings : 'c pattern -> string * string option
+  val tok_func : te lexer_func
+  val tok_using : 'c pattern -> unit
+  val tok_removing : 'c pattern -> unit
+  val tok_match : 'c pattern -> te -> 'c
+  val tok_text : 'c pattern -> string
+end