[parsing] Remove extend AST in favor of gramlib constructors

We remove Coq's wrapper over gramlib's grammar constructors.

2 files changed, 49 insertions, 255 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8f7d6d1966..e10e4bb8dd 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -10,7 +10,6 @@
 
 open CErrors
 open Util
-open Extend
 open Genarg
 open Gramlib
 
@@ -19,47 +18,16 @@ open Gramlib
 type norec = Gramlib.Grammar.norec
 type mayrec = Gramlib.Grammar.mayrec
 
-type ('self, 'trec, 'a) symbol =
-| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
-| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
-| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
-              -> ('self, 'trec, 'a list) symbol
-| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
-| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
-              -> ('self, 'trec, 'a list) symbol
-| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol
-| Aself : ('self, mayrec, 'self) symbol
-| Anext : ('self, mayrec, 'self) symbol
-| Aentry : 'a entry -> ('self, norec, 'a) symbol
-| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol
-| Arules : 'a rules list -> ('self, norec, 'a) symbol
-
-and ('self, 'trec, _, 'r) rule =
-| Stop : ('self, norec, 'r, 'r) rule
-| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule
-| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule
-
-and 'a rules =
-| Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules
-
-type 'a production_rule =
-| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-
 module G : sig
 
   include Grammar.S
     with type te = Tok.t
      and type 'c pattern = 'c Tok.p
-     and type 'a pattern = 'a Tok.p
-     and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol
-     and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule
-     and type 'a Rules.t = 'a rules
-     and type 'a Production.t = 'a production_rule
 
   val comment_state : Parsable.t -> ((int * int) * string) list
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
-  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
-  val mk_rule : 'a Tok.p list -> string rules
+  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+  val mk_rule : 'a Tok.p list -> string Rules.t
 
 end with type 'a Entry.t = 'a Extend.entry = struct
 
@@ -88,6 +56,12 @@ end with type 'a Entry.t = 'a Extend.entry = struct
 
   let tokens = G_.tokens
 
+  type 'a single_extend_statement = 'a G_.single_extend_statement
+  type 'a extend_statement = 'a G_.extend_statement =
+    { pos : Gramlib.Gramext.position option
+    ; data : 'a single_extend_statement list
+    }
+
   module Entry = struct
     include G_.Entry
 
@@ -105,164 +79,17 @@ end with type 'a Entry.t = 'a Extend.entry = struct
 
   end
 
-  module Symbol = struct
-    type ('self, 'trec, 'a) t = ('self, 'trec, 'a) symbol
-    let token tok = Atoken tok
-    let list0 e = Alist0 e
-    let list0sep e s _ = Alist0sep (e,s)
-    let list1 e = Alist1 e
-    let list1sep e s _ = Alist1sep (e,s)
-    let opt e = Aopt e
-    let self = Aself
-    let next = Anext
-    let nterm e = Aentry e
-    let nterml e s = Aentryl (e,s)
-    let rules ~warning:_ r = Arules r
-  end
-
-  module Rule = struct
-    type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) rule
-    let stop = Stop
-    let next a b = Next (a,b)
-    let next_norec a b = NextNoRec (a,b)
-  end
-
-  module Rules = struct
-    type 'a t = 'a rules
-    let make a f = Rules(a,f)
-  end
-
-  module Production = struct
-    type 'a t = 'a production_rule
-    let make a f = Rule(a,f)
-  end
-
-  module Unsafe = struct
-    let clear_entry = G_.Unsafe.clear_entry
-  end
-
-  (** FIXME: This is a hack around a deficient camlp5 API *)
-  type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G_.Rule.t * 'f -> 'a any_production
-
-  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_.Symbol.token t
-    | Alist1 s ->
-      let s = symbol_of_prod_entry_key s in
-      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_.Symbol.list1sep s sep false
-    | Alist0 s ->
-      let s = symbol_of_prod_entry_key s in
-      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_.Symbol.list0sep s sep false
-    | Aopt s ->
-      let s = symbol_of_prod_entry_key s in
-      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_.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs)
-
-  and symbol_of_rule : type s tr a r. (s, tr, a, r) rule -> (s, tr, a, r) G_.Rule.t = function
-    | Stop ->
-      G_.Rule.stop
-    | Next (r, s) ->
-      let r = symbol_of_rule r in
-      let s = symbol_of_prod_entry_key s in
-      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_.Rule.next_norec r s
-
-  and symbol_of_rules : type a. a rules -> a G_.Rules.t = function
-    | Rules (r, act) ->
-      let symb = symbol_of_rule r in
-      G_.Rules.make symb act
-
-  let of_coq_production_rule : type a. a production_rule -> a any_production = function
-    | Rule (toks, act) ->
-      AnyProduction (symbol_of_rule toks, act)
-
-  let of_coq_single_extend_statement (lvl, assoc, rule) =
-    (lvl, assoc, List.map of_coq_production_rule rule)
-
-  let of_coq_extend_statement (pos, st) =
-    (pos, List.map of_coq_single_extend_statement st)
-
-  let fix_extend_statement (pos, st) =
-    let fix_single_extend_statement (lvl, assoc, rules) =
-      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)
-
-  let safe_extend ~warning e pos ext =
-    let pos, ext = of_coq_extend_statement (pos,ext) in
-    let pos, ext = fix_extend_statement (pos, ext) in
-    G_.safe_extend ~warning e pos ext
-
-  let safe_delete_rule e r =
-    let r = symbol_of_rule r in
-    G_.safe_delete_rule e r
-
-  let level_of_nonterm = function
-    | Aentryl (_,l) -> Some l
-    | _ -> None
-
-  exception SelfSymbol
-  let rec generalize_symbol :
-    type a tr s. (s, tr, a) symbol -> (s, norec, a) symbol =
-    function
-    | Atoken tok ->
-      Atoken tok
-    | Alist1 e ->
-      Alist1 (generalize_symbol e)
-    | Alist1sep (e, sep) ->
-      let e = generalize_symbol e in
-      let sep = generalize_symbol sep in
-      Alist1sep (e, sep)
-    | Alist0 e ->
-      Alist0 (generalize_symbol e)
-    | Alist0sep (e, sep) ->
-      let e = generalize_symbol e in
-      let sep = generalize_symbol sep in
-      Alist0sep (e, sep)
-    | Aopt e ->
-      Aopt (generalize_symbol e)
-    | Aself ->
-      raise SelfSymbol
-    | Anext ->
-      raise SelfSymbol
-    | Aentry e ->
-      Aentry e
-    | Aentryl (e, l) ->
-      Aentryl (e, l)
-    | Arules r ->
-      Arules r
-
-  let generalize_symbol s =
-    try Some (generalize_symbol s)
-    with SelfSymbol -> None
-
-  let rec mk_rule tok =
-    match tok with
-    | [] ->
-      let stop_e = Stop in
-      Rules (stop_e, fun _ -> (* dropped anyway: *) "")
-    | tkn :: rem ->
-      let Rules (r, f) = mk_rule rem in
-      let r = Rule.next_norec r (Symbol.token tkn) in
-      Rules (r, fun _ -> f)
+  module Symbol = G_.Symbol
+  module Rule = G_.Rule
+  module Rules = G_.Rules
+  module Production = G_.Production
+  module Unsafe = G_.Unsafe
+
+  let safe_extend = G_.safe_extend
+  let safe_delete_rule = G_.safe_delete_rule
+  let level_of_nonterm = G_.level_of_nonterm
+  let generalize_symbol = G_.generalize_symbol
+  let mk_rule = G_.mk_rule
 end
 
 module Parsable = struct
@@ -349,21 +176,9 @@ end
 (** Type of reinitialization data *)
 type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 
-type 'a single_extend_statement =
-  string option *
-  (* Level *)
-  Gramlib.Gramext.g_assoc option *
-  (* Associativity *)
-  'a production_rule list
-  (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
-  Gramlib.Gramext.position option *
-  'a single_extend_statement list
-
 type extend_rule =
-| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
+| ExtendRule : 'a G.Entry.t * 'a G.extend_statement -> extend_rule
+| ExtendRuleReinit : 'a G.Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
 
 module EntryCommand = Dyn.Make ()
 module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end
@@ -382,39 +197,38 @@ let camlp5_entries = ref EntryDataMap.empty
 
 (** Deletion *)
 
-let grammar_delete e (pos,rls) =
+let grammar_delete e { G.pos; data } =
   List.iter
     (fun (n,ass,lev) ->
-      List.iter (fun (Rule(pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
-    (List.rev rls)
+      List.iter (fun pil -> G.safe_delete_rule e pil) (List.rev lev))
+    (List.rev data)
 
-let grammar_delete_reinit e reinit (pos, rls) =
-  grammar_delete e (pos, rls);
+let grammar_delete_reinit e reinit ({ G.pos; data } as d)=
+  grammar_delete e d;
   let a, ext = reinit in
   let lev = match pos with
     | Some (Gramext.Level n) -> n
     | _ -> assert false
   in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
-  (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
+  let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in
+  G.safe_extend ~warning:(Some warning) e ext
 
 (** Extension *)
 
-let grammar_extend e (pos,ext) =
-  let undo () = grammar_delete e (pos,ext) in
-  let redo () = G.safe_extend ~warning:None e pos ext in
+let grammar_extend e ext =
+  let undo () = grammar_delete e ext in
+  let redo () = G.safe_extend ~warning:None e ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e ext =
   camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
-  let pos, ext = ext in
-  G.safe_extend ~warning:None e pos ext
+  G.safe_extend ~warning:None e ext
 
 let grammar_extend_sync_reinit e reinit ext =
   camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
-  let pos, ext = ext in
-  G.safe_extend ~warning:None e pos ext
+  G.safe_extend ~warning:None e ext
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -467,7 +281,8 @@ let eoi_entry en =
   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.make symbs act]);
+  let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
+  Gram.safe_extend ~warning:(Some warning) e ext;
   e
 
 let map_entry f en =
@@ -475,7 +290,8 @@ let map_entry f en =
   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.make symbs act]);
+  let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
+  Gram.safe_extend ~warning:(Some warning) e ext;
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -620,12 +436,12 @@ module Module =
     let module_type = Entry.create "module_type"
   end
 
-let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) =
+let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) =
   let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in
-  let ext = [None, None, [r]] in
   let entry = G.Entry.make "epsilon" in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
-  let () = G.safe_extend ~warning:(Some warning) entry None ext in
+  let ext = { G.pos = None; data = [None, None, [r]] } in
+  let () = G.safe_extend ~warning:(Some warning) entry ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e7e3e9442b..f83109d39a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -223,51 +223,26 @@ module Module :
 
 (** {5 Type-safe grammar extension} *)
 
-type ('self, 'trec, 'a) symbol
-type ('self, 'trec, _, 'r) rule
-
 type norec = Gramlib.Grammar.norec
 type mayrec = Gramlib.Grammar.mayrec
 
-type 'a rules
-type 'a production_rule
-
 module G : sig
 
   include Gramlib.Grammar.S
 
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
-  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
-  val mk_rule : 'a Tok.p list -> string rules
+  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+  val mk_rule : 'a Tok.p list -> string Rules.t
 
 end with type 'a Entry.t = 'a Entry.t
      and type te = Tok.t
      and type 'a pattern = 'a Tok.p
-     and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol
-     and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule
-     and type 'a Rules.t = 'a rules
-     and type 'a Production.t = 'a production_rule
 
-val epsilon_value : ('a -> 'self) -> ('self, _, 'a) symbol -> 'self option
+val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option
 
 (** {5 Extending the parser without synchronization} *)
 
-type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
-(** Type of reinitialization data *)
-
-type 'a single_extend_statement =
-  string option *
-  (* Level *)
-  Gramlib.Gramext.g_assoc option *
-  (* Associativity *)
-  'a production_rule list
-  (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
-  Gramlib.Gramext.position option *
-  'a single_extend_statement list
-
-val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a G.extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
@@ -283,9 +258,12 @@ type 'a grammar_command
 (** Type of synchronized parsing extensions. The ['a] type should be
     marshallable. *)
 
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
+(** Type of reinitialization data *)
+
 type extend_rule =
-| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a G.extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,