From 5b6582f8d47975f6f4f394cf44a1c65c799d43ff Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 4 Oct 2012 11:53:07 +0000 Subject: 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 --- lib/compat.ml4 | 243 --------------------------------------------------------- lib/lib.mllib | 1 - lib/loc.ml | 64 ++++++++++++--- lib/loc.mli | 21 ++++- 4 files changed, 68 insertions(+), 261 deletions(-) delete mode 100644 lib/compat.ml4 (limited to 'lib') 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 *) -(* 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 -- cgit v1.2.3