[gramlib] Refactor gramlib interface.

This is in preparation for making the Gramlib interface the canonical
one; see #11647 .

I tried to implement some of the ideas that were floated around in a
chat with Pierre-Marie, suggestions / comments are welcome.

4 files changed, 381 insertions, 283 deletions

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index e1b9c6b7cb..0024d70466 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -10,70 +10,88 @@ open Util
 
 module type GLexerType = Plexing.Lexer
 
-type ty_norec = TyNoRec
-type ty_mayrec = TyMayRec
+type norec
+type mayrec
 
-module type S =
+module type S = sig
+  type te
+  type 'c pattern
+
+  module Parsable : sig
+    type t
+    val make : ?loc:Loc.t -> char Stream.t -> t
+  end
+
+  val tokens : string -> (string option * int) list
+
+  module Entry : sig
+    type 'a t
+    val make : string -> 'a t
+    val parse : 'a t -> Parsable.t -> 'a
+    val name : 'a t -> string
+    val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t
+    val parse_token_stream : 'a t -> te Stream.t -> 'a
+    val print : Format.formatter -> 'a t -> unit
+  end
+
+  module rec Symbol : sig
+
+    type ('self, 'trec, 'a) t
+    val nterm : 'a Entry.t -> ('self, norec, 'a) t
+    val nterml : 'a Entry.t -> string -> ('self, norec, 'a) t
+    val list0 : ('self, 'trec, 'a) t -> ('self, 'trec, 'a list) t
+    val list0sep :
+      ('self, 'trec, 'a) t -> ('self, norec, 'b) t -> bool ->
+      ('self, 'trec, 'a list) t
+    val list1 : ('self, 'trec, 'a) t -> ('self, 'trec, 'a list) t
+    val list1sep :
+      ('self, 'trec, 'a) t -> ('self, norec, 'b) t -> bool ->
+      ('self, 'trec, 'a list) t
+    val opt : ('self, 'trec, 'a) t -> ('self, 'trec, 'a option) t
+    val self : ('self, mayrec, 'self) t
+    val next : ('self, mayrec, 'self) t
+    val token : 'c pattern -> ('self, norec, 'c) t
+    val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+
+  end and Rule : sig
+
+    type ('self, 'trec, 'f, 'r) t
+
+    val stop : ('self, norec, 'r, 'r) t
+    val next :
+      ('self, _, 'a, 'r) t -> ('self, _, 'b) Symbol.t ->
+      ('self, mayrec, 'b -> 'a, 'r) t
+    val next_norec :
+      ('self, norec, 'a, 'r) Rule.t -> ('self, norec, 'b) Symbol.t ->
+      ('self, norec, 'b -> 'a, 'r) t
+
+  end and Rules : sig
+
+    type 'a t
+    val make : (_, norec, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
+
+  end
+
+  module Production : sig
+    type 'a t
+    val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
+  end
+
+  module Unsafe :
   sig
-    type te
-    type 'c pattern
-    type parsable
-    val parsable : ?loc:Loc.t -> char Stream.t -> parsable
-    val tokens : string -> (string option * int) list
-    module Entry :
-      sig
-        type 'a e
-        val create : string -> 'a e
-        val parse : 'a e -> parsable -> 'a
-        val name : 'a e -> string
-        val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a e
-        val parse_token_stream : 'a e -> te Stream.t -> 'a
-        val print : Format.formatter -> 'a e -> unit
-      end
-    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, 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, '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, '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, 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
-      end
-    val safe_extend : warning:(string -> unit) option ->
-      'a Entry.e -> Gramext.position option ->
-        (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 clear_entry : 'a Entry.t -> unit
   end
+  val safe_extend : warning:(string -> unit) option ->
+    'a Entry.t -> Gramext.position option ->
+    (string option * Gramext.g_assoc option * 'a Production.t list)
+      list ->
+    unit
+  val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit
+end
 
 (* Implementation *)
 
-module GMake (L : GLexerType) =
-struct
+module GMake (L : GLexerType) = struct
 
 type te = L.te
 type 'c pattern = 'c L.pattern
@@ -84,7 +102,7 @@ type grammar =
   { gtokens : (string * string option, int ref) Hashtbl.t }
 
 let egram =
-  {gtokens = Hashtbl.create 301 }
+  { gtokens = Hashtbl.create 301 }
 
 let tokens con =
   let list = ref [] in
@@ -94,12 +112,12 @@ let tokens con =
   !list
 
 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
+| NoRec2 : (norec, norec, norec) ty_and_rec
+| MayRec2 : ('a, 'b, 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
+| NoRec3 : (norec, norec, norec, norec) ty_and_rec3
+| MayRec3 : ('a, 'b, 'c, mayrec) ty_and_rec3
 
 type 'a ty_entry = {
   ename : string;
@@ -122,26 +140,26 @@ and ('trecs, 'trecp, 'a) ty_rec_level = {
 }
 
 and ('self, 'trec, 'a) ty_symbol =
-| Stoken : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+| Stoken : 'c pattern -> ('self, 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
+| Slist1sep : ('self, 'trec, 'a) ty_symbol * ('self, 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
+| Slist0sep : ('self, 'trec, 'a) ty_symbol * ('self, 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
+| Sself : ('self, mayrec, 'self) ty_symbol
+| Snext : ('self, mayrec, 'self) ty_symbol
+| Snterm : 'a ty_entry -> ('self, norec, 'a) ty_symbol
+| Snterml : 'a ty_entry * string -> ('self, 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
+| TStop : ('self, 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
+| LocAct : 'k * 'k list -> ('self, norec, 'k) ty_tree
+| DeadEnd : ('self, norec, 'k) ty_tree
 
 and ('self, 'trec, 'trecs, 'trecb, 'a, 'r) ty_node = {
   node : ('self, 'trec, 'a) ty_symbol;
@@ -150,7 +168,7 @@ and ('self, 'trec, 'trecs, 'trecb, 'a, 'r) ty_node = {
 }
 
 type 'a ty_rules =
-| TRules : (_, ty_norec, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_rules
+| TRules : (_, 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
@@ -222,13 +240,13 @@ let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) t
 
 (** Ancillary datatypes *)
 
-type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec
+type 'a ty_rec = MayRec : mayrec ty_rec | NoRec : 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
+| NR00 : (mayrec, mayrec, mayrec) ty_and_ex
+| NR01 : (mayrec, norec, mayrec) ty_and_ex
+| NR10 : (norec, mayrec, mayrec) ty_and_ex
+| NR11 : (norec, norec, norec) ty_and_ex
 
 type ('a, 'b) ty_mayrec_and_ex =
 | MayRecNR : ('a, 'b, _) ty_and_ex -> ('a, 'b) ty_mayrec_and_ex
@@ -243,7 +261,7 @@ 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
+| TNil : ('self, 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 ~
@@ -313,7 +331,7 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t
       TCns (ars, s, sl), RelS pf -> insert_in_tree ar ars s sl pf tree action
     | TNil, Rel0 ->
         let node (type tb) ({node = s; son = son; brother = bro} : (_, _, _, tb, _, _) ty_node) =
-          let ar : (ty_norec, tb, tb) ty_and_ex =
+          let ar : (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
@@ -387,21 +405,21 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t
   in
   insert ar gsymbols pf tree action
 
-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 =
+let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, 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 =
+let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_symbol =
+  let rec retype_tree : type s a. (s, norec, a) ty_tree -> (self, 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 =
+  and retype_symbol : type s a. (s, norec, a) ty_symbol -> (self, norec, a) ty_symbol =
     function
     | Stoken p -> Stoken p
     | Slist1 s -> Slist1 (retype_symbol s)
@@ -412,7 +430,7 @@ let srules (type self a) ~warning (rl : a ty_rules list) : (self, ty_norec, a) t
     | 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 =
+  let rec retype_rule : type s k r. (s, norec, k, r) ty_rule -> (self, norec, k, r) ty_rule =
     function
     | TStop -> TStop
     | TNext (NoRec2, r, s) -> TNext (NoRec2, retype_rule r, retype_symbol s) in
@@ -1037,7 +1055,7 @@ let level_number entry lab =
     Dlevels elev -> lookup 0 elev
   | Dparser _ -> raise Not_found
 
-let rec top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> (s, ty_norec, a) ty_symbol =
+let rec top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> (s, norec, a) ty_symbol =
   fun entry ->
   function
     Sself -> Snterm entry
@@ -1484,105 +1502,168 @@ let delete_rule entry sl =
 
 (* Normal interface *)
 
-type parsable =
-  { pa_chr_strm : char Stream.t;
-    pa_tok_strm : L.te Stream.t;
-    pa_loc_func : Plexing.location_function }
-
-let parse_parsable entry p =
-  let efun = entry.estart 0 in
-  let ts = p.pa_tok_strm in
-  let cs = p.pa_chr_strm in
-  let fun_loc = p.pa_loc_func in
-  let restore =
-    let old_floc = !floc in
-    let old_tc = !token_count in
-    fun () -> floc := old_floc; token_count := old_tc
-  in
-  let get_loc () =
-    try
-      let cnt = Stream.count ts in
-      (* Ensure that the token at location cnt has been peeked so that
-         the location function knows about it *)
-      let _ = Stream.peek ts in
-      let loc = fun_loc cnt in
-      if !token_count - 1 <= cnt then loc
-      else Loc.merge loc (fun_loc (!token_count - 1))
-    with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1)
-  in
-  floc := fun_loc;
-  token_count := 0;
-  try let r = efun ts in restore (); r with
-    Stream.Failure ->
+module Parsable = struct
+
+  type t =
+    { pa_chr_strm : char Stream.t
+    ; pa_tok_strm : L.te Stream.t
+    ; pa_loc_func : Plexing.location_function
+    }
+
+  let parse_parsable entry p =
+    let efun = entry.estart 0 in
+    let ts = p.pa_tok_strm in
+    let cs = p.pa_chr_strm in
+    let fun_loc = p.pa_loc_func in
+    let restore =
+      let old_floc = !floc in
+      let old_tc = !token_count in
+      fun () -> floc := old_floc; token_count := old_tc
+    in
+    let get_loc () =
+      try
+        let cnt = Stream.count ts in
+        (* Ensure that the token at location cnt has been peeked so that
+           the location function knows about it *)
+        let _ = Stream.peek ts in
+        let loc = fun_loc cnt in
+        if !token_count - 1 <= cnt then loc
+        else Loc.merge loc (fun_loc (!token_count - 1))
+      with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1)
+    in
+    floc := fun_loc;
+    token_count := 0;
+    try let r = efun ts in restore (); r with
+      Stream.Failure ->
       let loc = get_loc () in
       restore ();
       Ploc.raise loc (Stream.Error ("illegal begin of " ^ entry.ename))
-  | Stream.Error _ as exc ->
+    | Stream.Error _ as exc ->
       let loc = get_loc () in restore (); Ploc.raise loc exc
-  | exc ->
+    | exc ->
       let loc = Stream.count cs, Stream.count cs + 1 in
       restore (); Ploc.raise (Ploc.make_unlined loc) exc
 
-(* Unsafe *)
+  let make ?loc cs =
+    let (ts, lf) = L.tok_func ?loc cs in
+    {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
 
-let clear_entry e =
-  e.estart <- (fun _ (strm__ : _ Stream.t) -> raise Stream.Failure);
-  e.econtinue <- (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
-  match e.edesc with
-    Dlevels _ -> e.edesc <- Dlevels []
-  | Dparser _ -> ()
+end
 
-    let parsable ?loc cs =
-      let (ts, lf) = L.tok_func ?loc cs in
-      {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
-    module Entry =
-      struct
-        type 'a e = 'a ty_entry
-        let create n =
-          { ename = n; estart = empty_entry n;
-           econtinue =
-             (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
-           edesc = Dlevels []}
-        let parse (e : 'a e) p : 'a =
-          parse_parsable e p
-        let parse_token_stream (e : 'a e) ts : 'a =
-          e.estart 0 ts
-        let name e = e.ename
-        let of_parser n (p : Plexing.location_function -> te Stream.t -> 'a) : 'a e =
-          { ename = n;
-           estart = (fun _ -> p !floc);
-           econtinue =
-             (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
-           edesc = Dparser p}
-        let print ppf e = fprintf ppf "%a@." print_entry e
-      end
-    let s_nterm e = Snterm e
-    let s_nterml e l = Snterml (e, l)
-    let s_list0 s = Slist0 s
-    let s_list0sep s sep b = Slist0sep (s, sep, b)
-    let s_list1 s = Slist1 s
-    let s_list1sep s sep b = Slist1sep (s, sep, b)
-    let s_opt s = Sopt s
-    let s_self = Sself
-    let s_next = Snext
-    let s_token tok = Stoken tok
-    let s_rules ~warning (t : 'a ty_rules list) = srules ~warning t
-    let r_stop = TStop
-    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
-        let clear_entry = clear_entry
-      end
-    let safe_extend ~warning (e : 'a Entry.e) pos
-        (r :
-         (string option * Gramext.g_assoc option * 'a ty_production list)
-           list) =
-      extend_entry ~warning e pos r
-    let safe_delete_rule e r =
-      let AnyS (symbols, _) = get_symbols r in
-      delete_rule e symbols
+module Entry = struct
+  type 'a t = 'a ty_entry
+  let make n =
+    { ename = n; estart = empty_entry n;
+      econtinue =
+        (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
+      edesc = Dlevels []}
+  let parse (e : 'a t) p : 'a =
+    Parsable.parse_parsable e p
+  let parse_token_stream (e : 'a t) ts : 'a =
+    e.estart 0 ts
+  let name e = e.ename
+  let of_parser n (p : Plexing.location_function -> te Stream.t -> 'a) : 'a t =
+    { ename = n;
+      estart = (fun _ -> p !floc);
+      econtinue =
+        (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
+      edesc = Dparser p}
+  let print ppf e = fprintf ppf "%a@." print_entry e
+end
+
+module rec Symbol : sig
+
+  type ('self, 'trec, 'a) t = ('self, 'trec, 'a) ty_symbol
+
+  val nterm : 'a Entry.t -> ('self, norec, 'a) t
+  val nterml : 'a Entry.t -> string -> ('self, norec, 'a) t
+  val list0 : ('self, 'trec, 'a) t -> ('self, 'trec, 'a list) t
+  val list0sep :
+    ('self, 'trec, 'a) t -> ('self, norec, 'b) t -> bool ->
+    ('self, 'trec, 'a list) t
+  val list1 : ('self, 'trec, 'a) t -> ('self, 'trec, 'a list) t
+  val list1sep :
+    ('self, 'trec, 'a) t -> ('self, norec, 'b) t -> bool ->
+    ('self, 'trec, 'a list) t
+  val opt : ('self, 'trec, 'a) t -> ('self, 'trec, 'a option) t
+  val self : ('self, mayrec, 'self) t
+  val next : ('self, mayrec, 'self) t
+  val token : 'c pattern -> ('self, norec, 'c) t
+  val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+
+end = struct
+
+  type ('self, 'trec, 'a) t = ('self, 'trec, 'a) ty_symbol
+  let nterm e = Snterm e
+  let nterml e l = Snterml (e, l)
+  let list0 s = Slist0 s
+  let list0sep s sep b = Slist0sep (s, sep, b)
+  let list1 s = Slist1 s
+  let list1sep s sep b = Slist1sep (s, sep, b)
+  let opt s = Sopt s
+  let self = Sself
+  let next = Snext
+  let token tok = Stoken tok
+  let rules ~warning (t : 'a Rules.t list) = srules ~warning t
+
+end and Rule : sig
+
+  type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) ty_rule
+
+  val stop : ('self, norec, 'r, 'r) t
+  val next :
+    ('self, _, 'a, 'r) t -> ('self, _, 'b) Symbol.t ->
+    ('self, mayrec, 'b -> 'a, 'r) t
+  val next_norec :
+    ('self, norec, 'a, 'r) Rule.t -> ('self, norec, 'b) Symbol.t ->
+    ('self, norec, 'b -> 'a, 'r) t
+
+end = struct
+
+  type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) ty_rule
+
+  let stop = TStop
+  let next r s = TNext (MayRec2, r, s)
+  let next_norec r s = TNext (NoRec2, r, s)
+
+end and Rules : sig
+
+  type 'a t = 'a ty_rules
+  val make : (_, norec, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
+
+end = struct
+
+  type 'a t = 'a ty_rules
+  let make p act = TRules (p, act)
+
+end
+
+module Production = struct
+
+  type 'a t = 'a ty_production
+  let make p act = TProd (p, act)
+
+end
+
+module Unsafe = struct
+
+  let clear_entry e =
+    e.estart <- (fun _ (strm__ : _ Stream.t) -> raise Stream.Failure);
+    e.econtinue <- (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
+    match e.edesc with
+      Dlevels _ -> e.edesc <- Dlevels []
+    | Dparser _ -> ()
+
+end
+
+let safe_extend ~warning (e : 'a Entry.t) pos
+    (r :
+       (string option * Gramext.g_assoc option * 'a ty_production list)
+         list) =
+  extend_entry ~warning e pos r
+
+let safe_delete_rule e r =
+  let AnyS (symbols, _) = get_symbols r in
+  delete_rule e symbols
 
 end
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 9e48460206..f0423a92af 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -19,76 +19,93 @@ module type GLexerType = Plexing.Lexer
    (** The input signature for the functor [Grammar.GMake]: [te] is the
        type of the tokens. *)
 
-type ty_norec = TyNoRec
-type ty_mayrec = TyMayRec
+type norec
+type mayrec
 
-module type S =
+module type S = sig
+  type te
+  type 'c pattern
+
+  module Parsable : sig
+    type t
+    val make : ?loc:Loc.t -> char Stream.t -> t
+  end
+
+  val tokens : string -> (string option * int) list
+
+  module Entry : sig
+    type 'a t
+    val make : string -> 'a t
+    val parse : 'a t -> Parsable.t -> 'a
+    val name : 'a t -> string
+    val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t
+    val parse_token_stream : 'a t -> te Stream.t -> 'a
+    val print : Format.formatter -> 'a t -> unit
+  end
+
+  module rec Symbol : sig
+
+    type ('self, 'trec, 'a) t
+    val nterm : 'a Entry.t -> ('self, norec, 'a) t
+    val nterml : 'a Entry.t -> string -> ('self, norec, 'a) t
+    val list0 : ('self, 'trec, 'a) t -> ('self, 'trec, 'a list) t
+    val list0sep :
+      ('self, 'trec, 'a) t -> ('self, norec, 'b) t -> bool ->
+      ('self, 'trec, 'a list) t
+    val list1 : ('self, 'trec, 'a) t -> ('self, 'trec, 'a list) t
+    val list1sep :
+      ('self, 'trec, 'a) t -> ('self, norec, 'b) t -> bool ->
+      ('self, 'trec, 'a list) t
+    val opt : ('self, 'trec, 'a) t -> ('self, 'trec, 'a option) t
+    val self : ('self, mayrec, 'self) t
+    val next : ('self, mayrec, 'self) t
+    val token : 'c pattern -> ('self, norec, 'c) t
+    val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+
+  end and Rule : sig
+
+    type ('self, 'trec, 'f, 'r) t
+
+    val stop : ('self, norec, 'r, 'r) t
+    val next :
+      ('self, _, 'a, 'r) t -> ('self, _, 'b) Symbol.t ->
+      ('self, mayrec, 'b -> 'a, 'r) t
+    val next_norec :
+      ('self, norec, 'a, 'r) Rule.t -> ('self, norec, 'b) Symbol.t ->
+      ('self, norec, 'b -> 'a, 'r) t
+
+  end and Rules : sig
+
+    type 'a t
+    val make : (_, norec, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
+
+  end
+
+  module Production : sig
+    type 'a t
+    val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
+  end
+
+  module Unsafe :
   sig
-    type te
-    type 'c pattern
-    type parsable
-    val parsable : ?loc:Loc.t -> char Stream.t -> parsable
-    val tokens : string -> (string option * int) list
-    module Entry :
-      sig
-        type 'a e
-        val create : string -> 'a e
-        val parse : 'a e -> parsable -> 'a
-        val name : 'a e -> string
-        val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a e
-        val parse_token_stream : 'a e -> te Stream.t -> 'a
-        val print : Format.formatter -> 'a e -> unit
-      end
-    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, 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, '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, '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, 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
-      end
-    val safe_extend : warning:(string -> unit) option ->
-      'a Entry.e -> Gramext.position option ->
-        (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 clear_entry : 'a Entry.t -> unit
   end
-   (** Signature type of the functor [Grammar.GMake]. The types and
-       functions are almost the same than in generic interface, but:
--      Grammars are not values. Functions holding a grammar as parameter
-         do not have this parameter yet.
--      The type [parsable] is used in function [parse] instead of
-         the char stream, avoiding the possible loss of tokens.
--      The type of tokens (expressions and patterns) can be any
-         type (instead of (string * string)); the module parameter
-         must specify a way to show them as (string * string) *)
+  val safe_extend : warning:(string -> unit) option ->
+    'a Entry.t -> Gramext.position option ->
+    (string option * Gramext.g_assoc option * 'a Production.t list)
+      list ->
+    unit
+  val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit
+end
+(** Signature type of the functor [Grammar.GMake]. The types and
+    functions are almost the same than in generic interface, but:
+    -      Grammars are not values. Functions holding a grammar as parameter
+      do not have this parameter yet.
+    -      The type [parsable] is used in function [parse] instead of
+      the char stream, avoiding the possible loss of tokens.
+    -      The type of tokens (expressions and patterns) can be any
+      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 and type 'c pattern = 'c L.pattern
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 848861238a..c53c3f02a8 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.Lexer).Entry.e
+type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.t
 
 type side = Left | Right
 
@@ -82,8 +82,8 @@ type ('a,'b,'c) ty_user_symbol =
 
 (* Should be merged with gramlib's implementation *)
 
-type norec = Gramlib.Grammar.ty_norec
-type mayrec = Gramlib.Grammar.ty_mayrec
+type norec = Gramlib.Grammar.norec
+type mayrec = Gramlib.Grammar.mayrec
 
 type ('self, 'trec, 'a) symbol =
 | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 92c3b7c6e8..63181bc0bc 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -65,20 +65,20 @@ module type S =
 
   val comment_state : coq_parsable -> ((int * int) * string) list
 
-end with type 'a Entry.e = 'a Extend.entry = struct
+end with type 'a Entry.t = 'a Extend.entry = struct
 
   include Grammar.GMake(CLexer.Lexer)
 
-  type coq_parsable = parsable * CLexer.lexer_state ref
+  type coq_parsable = Parsable.t * CLexer.lexer_state ref
 
   let coq_parsable ?loc c =
     let state = ref (CLexer.init_lexer_state ()) in
     CLexer.set_lexer_state !state;
-    let a = parsable ?loc c in
+    let a = Parsable.make ?loc c in
     state := CLexer.get_lexer_state ();
     (a,state)
 
-  let entry_create = Entry.create
+  let entry_create = Entry.make
 
   let entry_parse e (p,state) =
     CLexer.set_lexer_state !state;
@@ -107,9 +107,9 @@ end
 module Entry =
 struct
 
-  type 'a t = 'a Grammar.GMake(CLexer.Lexer).Entry.e
+  type 'a t = 'a Grammar.GMake(CLexer.Lexer).Entry.t
 
-  let create = G.Entry.create
+  let create = G.Entry.make
   let parse = G.entry_parse
   let print = G.Entry.print
   let of_parser = G.Entry.of_parser
@@ -131,53 +131,53 @@ end
 
 (** Binding general entry keys to symbol *)
 
-let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.ty_symbol =
+let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.Symbol.t =
 function
-| Atoken t -> G.s_token t
+| Atoken t -> G.Symbol.token t
 | Alist1 s ->
   let s = symbol_of_prod_entry_key s in
-  G.s_list1 s
+  G.Symbol.list1 s
 | Alist1sep (s,sep) ->
   let s = symbol_of_prod_entry_key s in
   let sep = symbol_of_prod_entry_key sep in
-  G.s_list1sep s sep false
+  G.Symbol.list1sep s sep false
 | Alist0 s ->
   let s = symbol_of_prod_entry_key s in
-  G.s_list0 s
+  G.Symbol.list0 s
 | Alist0sep (s,sep) ->
   let s = symbol_of_prod_entry_key s in
   let sep = symbol_of_prod_entry_key sep in
-  G.s_list0sep s sep false
+  G.Symbol.list0sep s sep false
 | Aopt s ->
   let s = symbol_of_prod_entry_key s in
-  G.s_opt s
-| Aself -> G.s_self
-| Anext -> G.s_next
-| Aentry e -> G.s_nterm e
-| Aentryl (e, n) -> G.s_nterml e n
+  G.Symbol.opt s
+| Aself -> G.Symbol.self
+| Anext -> G.Symbol.next
+| Aentry e -> G.Symbol.nterm e
+| Aentryl (e, n) -> G.Symbol.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)
+  G.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs)
 
-and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.ty_rule = function
+and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.Rule.t = function
 | Stop ->
-  G.r_stop
+  G.Rule.stop
 | Next (r, s) ->
   let r = symbol_of_rule r in
   let s = symbol_of_prod_entry_key s in
-  G.r_next r s
+  G.Rule.next r s
 | NextNoRec (r, s) ->
   let r = symbol_of_rule r in
   let s = symbol_of_prod_entry_key s in
-  G.r_next_norec r s
+  G.Rule.next_norec r s
 
-and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function
+and symbol_of_rules : type a. a Extend.rules -> a G.Rules.t = function
 | Rules (r, act) ->
   let symb = symbol_of_rule r in
-  G.rules (symb,act)
+  G.Rules.make symb act
 
 (** FIXME: This is a hack around a deficient camlp5 API *)
-type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production
+type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.Rule.t * 'f -> 'a any_production
 
 let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
 | Rule (toks, act) ->
@@ -191,7 +191,7 @@ let of_coq_extend_statement (pos, st) =
 
 let fix_extend_statement (pos, st) =
   let fix_single_extend_statement (lvl, assoc, rules) =
-    let fix_production_rule (AnyProduction (s, act)) = G.production (s, act) in
+    let fix_production_rule (AnyProduction (s, act)) = G.Production.make s act in
     (lvl, assoc, List.map fix_production_rule rules)
   in
   (pos, List.map fix_single_extend_statement st)
@@ -216,13 +216,13 @@ type extend_rule =
 | ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
 
 module EntryCommand = Dyn.Make ()
-module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end
+module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end
 module EntryDataMap = EntryCommand.Map(EntryData)
 
 type ext_kind =
   | ByGrammar of extend_rule
   | ByEXTEND of (unit -> unit) * (unit -> unit)
-  | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind
+  | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.t -> ext_kind
 
 (** The list of extensions *)
 
@@ -316,18 +316,18 @@ 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.PEOI) in
+  let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.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)]);
+  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]);
   e
 
 let map_entry f en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
-  let symbs = G.r_next G.r_stop (G.s_nterm en) in
+  let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in
   let act = fun x loc -> f 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)]);
+  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -473,7 +473,7 @@ module Module =
 
 let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) =
   let s = symbol_of_prod_entry_key e in
-  let r = G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in
+  let r = G.Production.make (G.Rule.next G.Rule.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
@@ -535,7 +535,7 @@ let extend_grammar_command tag g =
   let nb = List.length rules in
   grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
 
-let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list =
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.t list =
   let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
   let grammar_state = match !grammar_stack with
   | [] -> GramState.empty
@@ -568,7 +568,7 @@ let extend_dyn_grammar (e, _) = match e with
 
 (** Registering extra grammar *)
 
-type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry
+type any_entry = AnyEntry : 'a Gram.Entry.t -> any_entry
 
 let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty