Thorough rewriting of the Pcoq API towards safety and static invariants.

Amongst other things:

1. No more unsafe grammar extensions, except when going through the CAMLPX-based
Pcoq.Gram module. This is mostly safe because CAMLPX adds casts to ensure that
parsing rules are well-typed. In particular, constr notation is now based on
GADTs ensuring well-typedness.

2. Less reliance on unsafe coq inside Pcoq, and exposing a self-contained API.
The Entry module was also removed as it now results useless.

3. Purely functional API for synchronized grammar extension. This gets rid of
quite buggy code maintaining a table of empty entries to work around CAMLPX bugs.
The state modification is now explicit and grammar extensions synchronized with
the summary must provide the rules they want to perform instead of doing so
imperatively.

1 files changed, 10 insertions, 21 deletions

diff --git a/intf/extend.mli b/intf/extend.mli
index 381d47dd18..7ba332f709 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -8,6 +8,8 @@
 
 (** Entry keys for constr notations *)
 
+type 'a entry = 'a Compat.GrammarMake(CLexer).entry
+
 type side = Left | Right
 
 type gram_assoc = NonA | RightA | LeftA
@@ -64,40 +66,27 @@ type 'a user_symbol =
 
 (** {5 Type-safe grammar extension} *)
 
-(** (a, b, r) adj => [a = x₁ -> ... xₙ -> r] & [b = x₁ * (... (xₙ * unit))]. *)
-type (_, _, _) adj =
-| Adj0 : ('r, unit, 'r) adj
-| AdjS : ('s, 'b, 'r) adj -> ('a -> 's, 'a * 'b, 'r) adj
-
-type _ index =
-| I0 : 'a -> ('a * 'r) index
-| IS : 'a index -> ('b * 'a) index
-
-(** This type should be marshallable, this is why we use a convoluted
-    representation in the [Arules] constructor instead of putting a function. *)
 type ('self, 'a) symbol =
 | Atoken : Tok.t -> ('self, string) symbol
 | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
-| Alist1sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol
+| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
 | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
-| Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol
+| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
 | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
 | Aself : ('self, 'self) symbol
 | Anext : ('self, 'self) symbol
-| Aentry : 'a Entry.t -> ('self, 'a) symbol
-| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol
-| Arules : 'a rules -> ('self, 'a index) symbol
+| Aentry : 'a entry -> ('self, 'a) symbol
+| Aentryl : 'a entry * int -> ('self, 'a) symbol
+| Arules : 'a rules list -> ('self, 'a) symbol
 
 and ('self, _, 'r) rule =
 | Stop : ('self, 'r, 'r) rule
 | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
 
+and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule }
+
 and 'a rules =
-| Rule0 : unit rules
-| RuleS :
-  ('any, 'act, Loc.t -> Loc.t * 'a) rule *
-  ('act, 'a, Loc.t -> Loc.t * 'a) adj *
-  'b rules -> ((Loc.t * 'a) * 'b) rules
+| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
 
 type 'a production_rule =
 | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule