Add (almost) compatibility with camlp4, without breaking support for camlp5

The choice between camlp4/5 is done during configure with flags
 -usecamlp5 (default for the moment) vs. -usecamlp4.

 Currently, to have a full camlp4 compatibility, you need to change
 all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
 into "`EOI" in grammar entries. I've a sed script that does that
 (actually the converse), but I prefer to re-think it and check a few
 things before branching this sed into the build mechanism.

 lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
 and try to propose a common interface (cf LexerSig / GrammarSig).
 A few incompatible quotations have been turned into underlying code
 manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
 parsable by both camlp4 and 5. See in particular the fate of
 <:str_item< declare ... end >>

 Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
 This forces to use camlp5 > 5.01.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 225 insertions, 20 deletions

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index c377581527..aba2720456 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -8,19 +8,221 @@
 
 (** Compatibility file depending on ocaml/camlp4 version *)
 
+(** Locations *)
+
+IFDEF CAMLP5 THEN
+
+module Loc = struct
+  include Ploc
+  exception Exc_located = Exc
+  let ghost = dummy
+  let merge = encl
+end
+
+let make_loc = Loc.make_unlined
+let unloc loc = (Loc.first_pos loc, Loc.last_pos loc)
+
+ELSE
+
+module Loc = Camlp4.PreCast.Loc
+
+let make_loc (start,stop) =
+  Loc.of_tuple ("", 0, 0, start, 0, 0, stop, false)
+let unloc loc = (Loc.start_off loc, Loc.stop_off loc)
+
+END
+
+(** Misc module emulation *)
+
 IFDEF CAMLP5 THEN
 
-type loc = Stdpp.location
-let dummy_loc = Stdpp.dummy_loc
-let make_loc = Stdpp.make_loc
-let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else Stdpp.encl_loc loc1 loc2
-type lexer = Tok.t Token.glexer
+module PcamlSig = struct end
+
+ELSE
+
+module PcamlSig = Camlp4.Sig
+module Ast = Camlp4.PreCast.Ast
+module Pcaml = Camlp4.PreCast.Syntax
+module MLast = Ast
+module Token = struct exception Error of string end
+
+END
+
 
-ELSE (* official camlp4 of ocaml >= 3.10 *)
+(** Grammar auxiliary types *)
+
+IFDEF CAMLP5 THEN
+type gram_assoc = Gramext.g_assoc = NonA | RightA | LeftA
+type gram_position = Gramext.position =
+  | First
+  | Last
+  | Before of string
+  | After of string
+  | Like of string (** dont use it, not in camlp4 *)
+  | Level of string
+ELSE
+type gram_assoc = PcamlSig.Grammar.assoc = NonA | RightA | LeftA
+type gram_position = PcamlSig.Grammar.position =
+  | First
+  | Last
+  | Before of string
+  | After of string
+  | Level of string
+END
+
+
+(** Signature of Lexer *)
+
+IFDEF CAMLP5 THEN
+
+module type LexerSig = sig
+  include Grammar.GLexerType with type te = Tok.t
+  module Error : sig
+    type t
+    exception E of t
+  end
+end
+
+ELSE
+
+module type LexerSig =
+  Camlp4.Sig.Lexer with module Loc = Loc and type Token.t = Tok.t
+
+END
+
+(** Signature and implementation of grammars *)
+
+IFDEF CAMLP5 THEN
 
-TODO
+module type GrammarSig = sig
+  include Grammar.S with type te = Tok.t
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * gram_assoc option * production_rule list
+  type extend_statment =
+      gram_position option * single_extend_statment list
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_print : 'a entry -> unit
+  val srules' : production_rule list -> symbol
+  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
+end
 
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+  include Grammar.GMake (L)
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * gram_assoc option * production_rule list
+  type extend_statment =
+      gram_position option * single_extend_statment list
+  let action = Gramext.action
+  let entry_create = Entry.create
+  let entry_parse = Entry.parse
+  let entry_print = Entry.print
+  let srules' = Gramext.srules
+  let parse_tokens_after_filter = Entry.parse_token
+end
+
+ELSE
+
+module type GrammarSig = sig
+  include Camlp4.Sig.Grammar.Static
+    with module Loc = Loc and type Token.t = Tok.t
+  type 'a entry = 'a Entry.t
+  type action = Action.t
+  type parsable
+  val parsable : char Stream.t -> parsable
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_print : 'a entry -> unit
+  val srules' : production_rule list -> symbol
+end
+
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+  include Camlp4.Struct.Grammar.Static.Make (L)
+  type 'a entry = 'a Entry.t
+  type action = Action.t
+  type parsable = char Stream.t
+  let parsable s = s
+  let action = Action.mk
+  let entry_create = Entry.mk
+  let entry_parse e s = parse e (*FIXME*)Loc.ghost s
+  let entry_print x = Entry.print Format.std_formatter x
+  let srules' = srules (entry_create "dummy")
+end
+
+END
+
+
+(** Misc functional adjustments *)
+
+(** - The lexer produces streams made of pairs in camlp4 *)
+
+let get_tok = IFDEF CAMLP5 THEN fun x -> x ELSE fst END
+
+(** - Gram.extend is more currified in camlp5 than in camlp4 *)
+
+IFDEF CAMLP5 THEN
+let maybe_curry f x y = f (x,y)
+let maybe_uncurry f (x,y) = f x y
+ELSE
+let maybe_curry f = f
+let maybe_uncurry f = f
+END
+
+
+(** Fix a quotation difference in [str_item] *)
+
+let declare_str_items loc l =
+  let l' = <:str_item< open Pcoq >> :: <:str_item< open Extrawit >> :: l in
+IFDEF CAMLP5 THEN
+  MLast.StDcl (loc,l') (* correspond to <:str_item< declare $list:l'$ end >> *)
+ELSE
+  Ast.stSem_of_list l'
+END
+
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+  (<:patt< _ >>, None, <:expr< failwith "Extension: cannot occur" >>)
+
+IFDEF CAMLP5 THEN
+
+let make_fun loc cl =
+  let l = cl @ [default_patt loc] in
+  MLast.ExFun (loc,l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
+
+ELSE
+
+let make_fun loc cl =
+  let mk_when = function
+    | Some w -> w
+    | None -> Ast.ExNil loc
+  in
+  let mk_clause (patt,optwhen,expr) =
+    (* correspond to <:match_case< ... when ... -> ... >> *)
+    Ast.McArr (loc, patt, mk_when optwhen, expr) in
+  let init = mk_clause (default_patt loc) in
+  let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
+  let l = List.fold_right add_clause cl init in
+  Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
+
+END
+
+(** Explicit antiquotation $anti:... $ *)
+
+IFDEF CAMLP5 THEN
+let expl_anti loc e = <:expr< $anti:e$ >>
+ELSE
+let expl_anti _loc e = e (* FIXME: understand someday if we can do better *)
 END
diff --git a/lib/util.ml b/lib/util.ml
index d08727d27e..af5f2e33c4 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 open Pp
+open Compat
 
 (* Errors *)
 
@@ -27,17 +28,17 @@ let todo s = prerr_string ("TODO: "^s^"\n")
 
 exception Timeout
 
-type loc = Compat.loc
-let dummy_loc = Compat.dummy_loc
-let unloc = Compat.unloc
-let make_loc = Compat.make_loc
-let join_loc = Compat.join_loc
+type loc = Loc.t
+let dummy_loc = Loc.ghost
+let join_loc = Loc.merge
+let make_loc = make_loc
+let unloc = unloc
 
 (* raising located exceptions *)
 type 'a located = loc * 'a
-let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
-let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
-let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
+let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm))
+let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
+let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 
 let located_fold_left f x (_,a) = f x a
 let located_iter2 f (_,a) (_,b) = f a b
diff --git a/lib/util.mli b/lib/util.mli
index 9cef982fb3..98d2b6cf9d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -7,6 +7,7 @@
   **********************************************************************)
 
 open Pp
+open Compat
 
 (** This module contains numerous utility functions on strings, lists,
    arrays, etc. *)
@@ -36,17 +37,18 @@ val todo : string -> unit
 
 exception Timeout
 
-type loc = Compat.loc
+type loc = Loc.t
 
 type 'a located = loc * 'a
 
 val unloc : loc -> int * int
 val make_loc : int * int -> loc
 val dummy_loc : loc
+val join_loc : loc -> loc -> loc
+
 val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a
-val join_loc : loc -> loc -> loc
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit