Moved Compat to parsing. This permits to break the dependency of the

kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

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

4 files changed, 68 insertions, 261 deletions

diff --git a/lib/compat.ml4 b/lib/compat.ml4
deleted file mode 100644
index 3c26285bf6..0000000000
--- a/lib/compat.ml4
+++ /dev/null
@@ -1,243 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** 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
-
-module PcamlSig = struct end
-module Token = Token
-
-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
-
-
-(** 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
-    val to_string : t -> string
-  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
-
-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 : Format.formatter -> '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
-IFDEF CAMLP5_6_02_1 THEN
-  let entry_print ft x = Entry.print ft x
-ELSE
-  let entry_print _ x = Entry.print x
-END
-  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 : Format.formatter -> '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 ft x = Entry.print ft 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
-
-(** Compatibility with camlp5 strict mode *)
-IFDEF CAMLP5 THEN
-  IFDEF STRICT THEN
-    let vala x = Ploc.VaVal x
-  ELSE
-    let vala x = x
-  END
-ELSE
-  let vala x = x
-END
-
-(** Fix a quotation difference in [str_item] *)
-
-let declare_str_items loc l =
-IFDEF CAMLP5 THEN
-  MLast.StDcl (loc, vala 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< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-IFDEF CAMLP5 THEN
-
-let make_fun loc cl =
-  let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc, vala 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/lib.mllib b/lib/lib.mllib
index a7d56c666a..f557bd7d73 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
 Xml_lexer
 Xml_parser
-Compat
 Loc
 Errors
 Bigint
diff --git a/lib/loc.ml b/lib/loc.ml
index 58a328823f..57c928bbcb 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -6,24 +6,62 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
+(* Locations management *)
 
-include Compat.Loc
 
-(* Locations management *)
+type t = {
+  fname : string; (** filename *)
+  line_nb : int; (** start line number *)
+  bol_pos : int; (** position of the beginning of start line *)
+  line_nb_last : int; (** end line number *)
+  bol_pos_last : int; (** position of the beginning of end line *)
+  bp : int; (** start position *)
+  ep : int; (** end position *)
+}
+
+exception Exc_located of t * exn
+
+let create fname line_nb bol_pos (bp, ep) = {
+  fname = fname; line_nb = line_nb; bol_pos = bol_pos;
+  line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
+
+let make_loc (bp, ep) = {
+  fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  bp = bp; ep = ep; }
+
+let ghost = {
+  fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  bp = 0; ep = 0; }
 
-let dummy_loc = Compat.Loc.ghost
-let join_loc = Compat.Loc.merge
-let make_loc = Compat.make_loc
-let unloc = Compat.unloc
+let merge loc1 loc2 =
+  if loc1.bp < loc2.bp then
+    if loc1.ep < loc2.ep then {
+      fname = loc1.fname;
+      line_nb = loc1.line_nb;
+      bol_pos = loc1.bol_pos;
+      line_nb_last = loc2.line_nb_last;
+      bol_pos_last = loc2.bol_pos_last;
+      bp = loc1.bp; ep = loc2.ep; }
+    else loc1
+  else if loc2.ep < loc1.ep then {
+    fname = loc2.fname;
+    line_nb = loc2.line_nb;
+    bol_pos = loc2.bol_pos;
+    line_nb_last = loc1.line_nb_last;
+    bol_pos_last = loc1.bol_pos_last;
+    bp = loc2.bp; ep = loc1.ep; }
+  else loc2
+
+let unloc loc = (loc.bp, loc.ep)
+
+let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep)
+
+let raise loc e = raise (Exc_located (loc, e))
+
+let dummy_loc = ghost
+let join_loc = merge
 
 type 'a located = t * 'a
 let located_fold_left f x (_,a) = f x a
 let located_iter2 f (_,a) (_,b) = f a b
 let down_located f (_,a) = f a
-
-let pr_located pr (loc, x) =
-  if Flags.do_beautify () && loc <> dummy_loc then
-    let (b, e) = unloc loc in
-    Pp.comment b ++ pr x ++ Pp.comment e
-  else pr x
diff --git a/lib/loc.mli b/lib/loc.mli
index c1cbdb64d1..0b6ba544d1 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,21 +8,37 @@
 
 (** {5 Basic types} *)
 
-type t = Compat.Loc.t
+type t
 
 exception Exc_located of t * exn
 
 type 'a located = t * 'a
+(** Embed a location in a type *)
 
 (** {5 Location manipulation} *)
 
 (** This is inherited from CAMPL4/5. *)
 
+val create : string -> int -> int -> (int * int) -> t
+(** Create a location from a filename, a line number, a position of the
+    beginning of the line and a pair of start and end position *)
+
 val unloc : t -> int * int
+(** Return the start and end position of a location *)
+
 val make_loc : int * int -> t
+(** Make a location out of its start and end position *)
+
 val ghost : t
+(** Dummy location *)
+
 val merge : t -> t -> t
+
 val raise : t -> exn -> 'a
+(** Raise a located exception *)
+
+val represent : t -> (string * int * int * int * int)
+(** Return the arguments given in [create] *)
 
 (** {5 Location utilities} *)
 
@@ -32,9 +48,6 @@ val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 val down_located : ('a -> 'b) -> 'a located -> 'b
 (** Projects out a located object *)
 
-val pr_located : ('a -> Pp.std_ppcmds) -> 'a located -> Pp.std_ppcmds
-(** Prints an object surrounded by its commented location *)
-
 (** {5 Backward compatibility} *)
 
 val dummy_loc : t