diff options
Diffstat (limited to 'parsing/compat.ml4')
| -rw-r--r-- | parsing/compat.ml4 | 421 |
1 files changed, 0 insertions, 421 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 deleted file mode 100644 index befa0d01..00000000 --- a/parsing/compat.ml4 +++ /dev/null @@ -1,421 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \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 *) - -let file_loc_of_file = function -| None -> "" -| Some f -> f - -IFDEF CAMLP5 THEN - -module CompatLoc = struct - include Ploc - let ghost = dummy - let merge = encl -end - -exception Exc_located = Ploc.Exc - -let to_coqloc loc = - { Loc.fname = Ploc.file_name loc; - Loc.line_nb = Ploc.line_nb loc; - Loc.bol_pos = Ploc.bol_pos loc; - Loc.bp = Ploc.first_pos loc; - Loc.ep = Ploc.last_pos loc; - Loc.line_nb_last = Ploc.line_nb_last loc; - Loc.bol_pos_last = Ploc.bol_pos_last loc; } - -let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) "" - -(* Update a loc without allocating an intermediate pair *) -let set_loc_pos loc bp ep = - Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp) - -(* Increase line number by 1 and update position of beginning of line *) -let bump_loc_line loc bol_pos = - Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos - (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) - -(* Same as [bump_loc_line], but for the last line in location *) -(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop, - so we have to resort to a hack merging two locations. *) -(* Warning: [bump_loc_line_last] changes the end position. You may need to call - [set_loc_pos] to fix it. *) -let bump_loc_line_last loc bol_pos = - let loc' = - Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos - (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc) - in - Ploc.encl loc loc' - -let set_loc_file loc fname = - Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc) - (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) - -(* For some reason, the [Ploc.after] function of Camlp5 does not update line - numbers, so we define our own function that does it. *) -let after loc = - let line_nb = Ploc.line_nb_last loc in - let bol_pos = Ploc.bol_pos_last loc in - Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos - (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc) - -ELSE - -module CompatLoc = Camlp4.PreCast.Loc - -exception Exc_located = CompatLoc.Exc_located - -let to_coqloc loc = - { Loc.fname = CompatLoc.file_name loc; - Loc.line_nb = CompatLoc.start_line loc; - Loc.bol_pos = CompatLoc.start_bol loc; - Loc.bp = CompatLoc.start_off loc; - Loc.ep = CompatLoc.stop_off loc; - Loc.line_nb_last = CompatLoc.stop_line loc; - Loc.bol_pos_last = CompatLoc.stop_bol loc; } - -let make_loc fname line_nb bol_pos start stop = - CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false) - -open CompatLoc - -let set_loc_pos loc bp ep = - of_tuple (file_name loc, start_line loc, start_bol loc, bp, - stop_line loc, stop_bol loc, ep, is_ghost loc) - -let bump_loc_line loc bol_pos = - of_tuple (file_name loc, start_line loc + 1, bol_pos, start_off loc, - start_line loc + 1, bol_pos, stop_off loc, is_ghost loc) - -let bump_loc_line_last loc bol_pos = - of_tuple (file_name loc, start_line loc, start_bol loc, start_off loc, - stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc) - -let set_loc_file loc fname = - of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc, - stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) - -let after loc = - of_tuple (file_name loc, stop_line loc, stop_bol loc, stop_off loc, - stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) - -END - -let (!@) = to_coqloc - -(** Misc module emulation *) - -IFDEF CAMLP5 THEN - -module PcamlSig = struct end -module Token = Token -module CompatGramext = struct include Gramext type assoc = g_assoc 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 -module CompatGramext = Camlp4.Sig.Grammar - -END - -(** Signature of CLexer *) - -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 - type lexer_state - val init_lexer_state : string option -> lexer_state - val set_lexer_state : lexer_state -> unit - val release_lexer_state : unit -> lexer_state - val drop_lexer_state : unit -> unit -end - -ELSE - -module type LexerSig = sig - include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t - type lexer_state - val init_lexer_state : string option -> lexer_state - val set_lexer_state : lexer_state -> unit - val release_lexer_state : unit -> lexer_state - val drop_lexer_state : unit -> unit -end - -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 * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list - type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable - val action : 'a -> action - val entry_create : string -> 'a entry - val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit - val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b - 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 * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list - type coq_parsable = parsable * L.lexer_state ref - let parsable ?file c = - let state = ref (L.init_lexer_state file) in - L.set_lexer_state !state; - let a = parsable c in - state := L.release_lexer_state (); - (a,state) - let action = Gramext.action - let entry_create = Entry.create - let entry_parse e (p,state) = - L.set_lexer_state !state; - try - let c = Entry.parse e p in - state := L.release_lexer_state (); - c - with Exc_located (loc,e) -> - L.drop_lexer_state (); - let loc' = Loc.get_loc (Exninfo.info e) in - let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in - Loc.raise loc e - let with_parsable (p,state) f x = - L.set_lexer_state !state; - try - let a = f x in - state := L.release_lexer_state (); - a - with e -> - L.drop_lexer_state (); - raise e - - let entry_print ft x = Entry.print ft x - 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 = CompatLoc and type Token.t = Tok.t - type 'a entry = 'a Entry.t - type action = Action.t - type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable - val action : 'a -> action - val entry_create : string -> 'a entry - val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit - val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b - val srules' : production_rule list -> symbol -end - -module GrammarMake (L:LexerSig) : GrammarSig = struct - (* We need to refer to Coq's module Loc before it is hidden by include *) - let raise_coq_loc loc e = Loc.raise (to_coqloc loc) e - include Camlp4.Struct.Grammar.Static.Make (L) - type 'a entry = 'a Entry.t - type action = Action.t - type coq_parsable = char Stream.t * L.lexer_state ref - let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state) - let action = Action.mk - let entry_create = Entry.mk - let entry_parse e (s,state) = - L.set_lexer_state !state; - try - let c = parse e (*FIXME*)CompatLoc.ghost s in - state := L.release_lexer_state (); - c - with Exc_located (loc,e) -> - L.drop_lexer_state (); - raise_coq_loc loc e;; - let with_parsable (p,state) f x = - L.set_lexer_state !state; - try - let a = f x in - state := L.release_lexer_state (); - a - with e -> - L.drop_lexer_state (); - Pervasives.raise e;; - let entry_print ft x = Entry.print ft x - let srules' = srules (entry_create "dummy") -end - -END - -(** Some definitions are grammar-specific in Camlp4, so we use a functor to - depend on it while taking a dummy argument in Camlp5. *) - -module GramextMake (G : GrammarSig) : -sig - val stoken : Tok.t -> G.symbol - val sself : G.symbol - val snext : G.symbol - val slist0 : G.symbol -> G.symbol - val slist0sep : G.symbol * G.symbol -> G.symbol - val slist1 : G.symbol -> G.symbol - val slist1sep : G.symbol * G.symbol -> G.symbol - val sopt : G.symbol -> G.symbol - val snterml : G.internal_entry * string -> G.symbol - val snterm : G.internal_entry -> G.symbol - val snterml_level : G.symbol -> string -end = -struct - -IFDEF CAMLP5 THEN - let stoken tok = - let pattern = match tok with - | Tok.KEYWORD s -> "", s - | Tok.IDENT s -> "IDENT", s - | Tok.PATTERNIDENT s -> "PATTERNIDENT", s - | Tok.FIELD s -> "FIELD", s - | Tok.INT s -> "INT", s - | Tok.STRING s -> "STRING", s - | Tok.LEFTQMARK -> "LEFTQMARK", "" - | Tok.BULLET s -> "BULLET", s - | Tok.EOI -> "EOI", "" - in - Gramext.Stoken pattern -ELSE - module Gramext = G - let stoken tok = match tok with - | Tok.KEYWORD s -> Gramext.Skeyword s - | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok) -END - - IFDEF CAMLP5 THEN - let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) - let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) - ELSE - let slist0sep (x, y) = Gramext.Slist0sep (x, y) - let slist1sep (x, y) = Gramext.Slist1sep (x, y) - END - - let snterml (x, y) = Gramext.Snterml (x, y) - let snterm x = Gramext.Snterm x - let sself = Gramext.Sself - let snext = Gramext.Snext - let slist0 x = Gramext.Slist0 x - let slist1 x = Gramext.Slist1 x - let sopt x = Gramext.Sopt x - - let snterml_level = function - | Gramext.Snterml (_, l) -> l - | _ -> failwith "snterml_level" - -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 - -IFDEF CAMLP5 THEN -let warning_verbose = Gramext.warning_verbose -ELSE -(* TODO: this is a workaround, since there isn't such - [warning_verbose] in new camlp4. *) -let warning_verbose = ref true -END |