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, 2 insertions, 69 deletions

diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 310a44149a..2b67693d28 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -21,17 +21,11 @@ end
 exception Exc_located = Ploc.Exc
 
 IFDEF CAMLP5_6_00 THEN
-let ploc_make_loc fname lnb pos bpep = Ploc.make_loc fname lnb pos bpep ""
 let ploc_file_name = Ploc.file_name
 ELSE
-let ploc_make_loc fname lnb pos bpep = Ploc.make lnb pos bpep
 let ploc_file_name _ = ""
 END
 
-let of_coqloc loc =
-  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
-  ploc_make_loc fname lnb pos (bp,ep)
-
 let to_coqloc loc =
   Loc.create (ploc_file_name loc) (Ploc.line_nb loc)
     (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc)
@@ -44,10 +38,6 @@ module CompatLoc = Camlp4.PreCast.Loc
 
 exception Exc_located = CompatLoc.Exc_located
 
-let of_coqloc loc =
-  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
-  CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false)
-
 let to_coqloc loc =
   Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc)
     (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc)
@@ -65,6 +55,7 @@ IFDEF CAMLP5 THEN
 
 module PcamlSig = struct end
 module Token = Token
+module CompatGramext = struct include Gramext type assoc = g_assoc end
 
 ELSE
 
@@ -73,68 +64,10 @@ module Ast = Camlp4.PreCast.Ast
 module Pcaml = Camlp4.PreCast.Syntax
 module MLast = Ast
 module Token = struct exception Error of string end
+module CompatGramext = Camlp4.Sig.Grammar
 
 END
 
-
-(** Grammar auxiliary types *)
-
-IFDEF CAMLP5 THEN
-
-let to_coq_assoc = function
-| Gramext.RightA -> Extend.RightA
-| Gramext.LeftA -> Extend.LeftA
-| Gramext.NonA -> Extend.NonA
-
-let of_coq_assoc = function
-| Extend.RightA -> Gramext.RightA
-| Extend.LeftA -> Gramext.LeftA
-| Extend.NonA -> Gramext.NonA
-
-let of_coq_position = function
-| Extend.First -> Gramext.First
-| Extend.Last -> Gramext.Last
-| Extend.Before s -> Gramext.Before s
-| Extend.After s -> Gramext.After s
-| Extend.Level s -> Gramext.Level s
-
-let to_coq_position = function
-| Gramext.First -> Extend.First
-| Gramext.Last -> Extend.Last
-| Gramext.Before s -> Extend.Before s
-| Gramext.After s -> Extend.After s
-| Gramext.Level s -> Extend.Level s
-| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *)
-
-ELSE
-
-let to_coq_assoc = function
-| PcamlSig.Grammar.RightA -> Extend.RightA
-| PcamlSig.Grammar.LeftA -> Extend.LeftA
-| PcamlSig.Grammar.NonA -> Extend.NonA
-
-let of_coq_assoc = function
-| Extend.RightA -> PcamlSig.Grammar.RightA
-| Extend.LeftA -> PcamlSig.Grammar.LeftA
-| Extend.NonA -> PcamlSig.Grammar.NonA
-
-let of_coq_position = function
-| Extend.First -> PcamlSig.Grammar.First
-| Extend.Last -> PcamlSig.Grammar.Last
-| Extend.Before s -> PcamlSig.Grammar.Before s
-| Extend.After s -> PcamlSig.Grammar.After s
-| Extend.Level s -> PcamlSig.Grammar.Level s
-
-let to_coq_position = function
-| PcamlSig.Grammar.First -> Extend.First
-| PcamlSig.Grammar.Last -> Extend.Last
-| PcamlSig.Grammar.Before s -> Extend.Before s
-| PcamlSig.Grammar.After s -> Extend.After s
-| PcamlSig.Grammar.Level s -> Extend.Level s
-
-END
-
-
 (** Signature of CLexer *)
 
 IFDEF CAMLP5 THEN