Removing dead code in Compat.

3 files changed, 24 insertions, 73 deletions

diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 310a44149..2b67693d2 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
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6dcf76da8..8c8272589 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -19,6 +19,18 @@ module G = GrammarMake (CLexer)
 
 let warning_verbose = Compat.warning_verbose
 
+let of_coq_assoc = function
+| Extend.RightA -> CompatGramext.RightA
+| Extend.LeftA -> CompatGramext.LeftA
+| Extend.NonA -> CompatGramext.NonA
+
+let of_coq_position = function
+| Extend.First -> CompatGramext.First
+| Extend.Last -> CompatGramext.Last
+| Extend.Before s -> CompatGramext.Before s
+| Extend.After s -> CompatGramext.After s
+| Extend.Level s -> CompatGramext.Level s
+
 module Symbols = GramextMake(G)
 
 let gram_token_of_token = Symbols.stoken
@@ -86,8 +98,10 @@ let grammar_delete e reinit (pos,rls) =
     (List.rev rls);
   match reinit with
   | Some (a,ext) ->
-    let lev = match Option.map Compat.to_coq_position pos with
-    | Some (Level n) -> n
+    let a = of_coq_assoc a in
+    let ext = of_coq_position ext in
+    let lev = match pos with
+    | Some (CompatGramext.Level n) -> n
     | _ -> assert false
     in
     maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
@@ -135,8 +149,7 @@ let rec remove_grammars n =
     (match !camlp4_state with
        | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove")
        | ByGrammar(g,reinit,ext)::t ->
-           let f (a,b) = (of_coq_assoc a, of_coq_position b) in
-           grammar_delete g (Option.map f reinit) ext;
+           grammar_delete g reinit ext;
            camlp4_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d32052001..8c3c299ad 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -288,3 +288,8 @@ val register_empty_levels : bool -> int list ->
 val remove_levels : int -> unit
 
 val level_of_snterml : Gram.symbol -> int
+
+(** TODO: remove me *)
+
+val of_coq_position :  Extend.gram_position -> Compat.CompatGramext.position
+val of_coq_assoc :  Extend.gram_assoc -> Compat.CompatGramext.assoc