From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- parsing/argextend.ml4 | 6 +++--- parsing/egrammar.mli | 6 +++--- parsing/g_vernac.ml4 | 6 ++++-- parsing/g_xml.ml4 | 2 +- parsing/pcoq.ml4 | 29 +++++++++++++++++++++++++++-- parsing/pcoq.mli | 10 +++++----- parsing/ppconstr.ml | 10 +++++----- parsing/ppvernac.ml | 11 ++++++++--- parsing/q_coqast.ml4 | 13 +++++++++---- parsing/q_util.ml4 | 8 ++++---- parsing/tacextend.ml4 | 4 ++-- parsing/vernacextend.ml4 | 4 ++-- 12 files changed, 73 insertions(+), 36 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 12c0ea1d..2731fc90 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: argextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) +(* $Id: argextend.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) open Genarg open Q_util open Q_coqast -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) +let join_loc = Util.join_loc let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> @@ -226,7 +226,7 @@ EXTEND let t, g = interp_entry_name loc e sep in (g, Some (s,t)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then - Pcoq.lexer.Token.using ("", s); + Compat.using Pcoq.lexer ("", s); (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None) ] ] ; diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 5dda69ba..4216899b 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: egrammar.mli 9147 2006-09-15 21:49:56Z herbelin $ i*) +(*i $Id: egrammar.mli 10185 2007-10-06 18:05:13Z herbelin $ i*) (*i*) open Util @@ -45,7 +45,7 @@ val extend_grammar : all_grammar_command -> unit type grammar_tactic_production = | TacTerm of string | TacNonTerm of - loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option + loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option val extend_tactic_grammar : string -> grammar_tactic_production list list -> unit @@ -61,7 +61,7 @@ val get_extend_vernac_grammars : (* val reset_extend_grammars_v8 : unit -> unit *) -val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol +val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol val recover_notation_grammar : notation -> (precedence * tolerability list) -> notation_grammar diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6a9388b2..cdd484e7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_vernac.ml4 9977 2007-07-12 12:18:46Z msozeau $ *) +(* $Id: g_vernac.ml4 10067 2007-08-09 17:13:16Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -143,7 +143,9 @@ GEXTEND Gram VernacFixpoint (recs,Options.boxed_definitions()) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint (corecs,false) - | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] + | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l + | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; + l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] ; gallina_ext: [ [ b = record_token; oc = opt_coercion; name = identref; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 2f31c0b6..ce284454 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_xml.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: g_xml.ml4 10090 2007-08-24 10:53:53Z herbelin $ *) open Pp open Util diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f7adfdd8..bf3cb084 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.ml4 9333 2006-11-02 13:59:14Z barras $ i*) +(*i $Id: pcoq.ml4 10185 2007-10-06 18:05:13Z herbelin $ i*) open Pp open Util @@ -29,6 +29,29 @@ open Ppextend we unfreeze the state of the lexer. This restores the behaviour of the lexer. B.B. *) +IFDEF CAMLP5 THEN + +let lexer = { + Token.tok_func = Lexer.func; + Token.tok_using = Lexer.add_token; + Token.tok_removing = (fun _ -> ()); + Token.tok_match = Token.default_match; + (* Token.parse = Lexer.tparse; *) + Token.tok_comm = None; + Token.tok_text = Lexer.token_text } + +module L = + struct + type te = string * string + let lexer = lexer + end + +(* The parser of Coq *) + +module G = Grammar.GMake(L) + +ELSE + let lexer = { Token.func = Lexer.func; Token.using = Lexer.add_token; @@ -45,6 +68,8 @@ module L = module G = Grammar.Make(L) +END + let grammar_delete e rls = List.iter (fun (_,_,lev) -> @@ -95,7 +120,7 @@ type ext_kind = | ByGrammar of grammar_object G.Entry.e * Gramext.position option * (string option * Gramext.g_assoc option * - (Token.t Gramext.g_symbol list * Gramext.g_action) list) list + (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list | ByGEXTEND of (unit -> unit) * (unit -> unit) let camlp4_state = ref [] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1fe8c122..681a6b2c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*) +(*i $Id: pcoq.mli 10185 2007-10-06 18:05:13Z herbelin $ i*) open Util open Names @@ -20,9 +20,9 @@ open Libnames (* The lexer and parser of Coq. *) -val lexer : Token.lexer +val lexer : Compat.lexer -module Gram : Grammar.S with type te = Token.t +module Gram : Grammar.S with type te = Compat.token (* The superclass of all grammar entries *) type grammar_object @@ -42,7 +42,7 @@ val get_constr_entry : val grammar_extend : grammar_object Gram.Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * - (Token.t Gramext.g_symbol list * Gramext.g_action) list) list + (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list -> unit val remove_grammars : int -> unit @@ -210,7 +210,7 @@ module Vernac_ : (* Binding entry names to campl4 entries *) val symbol_of_production : Gramext.g_assoc option -> constr_entry -> - bool -> constr_production_entry -> Token.t Gramext.g_symbol + bool -> constr_production_entry -> Compat.token Gramext.g_symbol (* Registering/resetting the level of an entry *) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 275e179e..92c6715e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: ppconstr.ml 10087 2007-08-24 10:39:30Z herbelin $ *) (*i*) open Util @@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value let pr_delimiters key strm = strm ++ str ("%"^key) -let pr_located pr ((b,e),x) = - if Options.do_translate() && (b,e)<>dummy_loc then - let (b,e) = unloc (b,e) in +let pr_located pr (loc,x) = + if Options.do_translate() && loc<>dummy_loc then + let (b,e) = unloc loc in comment b ++ pr x ++ comment e else pr x @@ -142,7 +142,7 @@ let pr_opt_type_spc pr = function | CHole _ -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t -let pr_lident (b,_ as loc,id) = +let pr_lident (loc,id) = if loc <> dummy_loc then let (b,_) = unloc loc in pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f9b8c425..77f0d5cb 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 9562 2007-01-31 09:00:36Z msozeau $ *) +(* $Id: ppvernac.ml 10087 2007-08-24 10:39:30Z herbelin $ *) open Pp open Names @@ -28,7 +28,7 @@ open Tacinterp let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr -let pr_lident (b,_ as loc,id) = +let pr_lident (loc,id) = if loc <> dummy_loc then let (b,_) = unloc loc in pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) @@ -39,7 +39,7 @@ let string_of_fqid fqid = let pr_fqid fqid = str (string_of_fqid fqid) -let pr_lfqid (_,_ as loc,fqid) = +let pr_lfqid (loc,fqid) = if loc <> dummy_loc then let (b,_) = unloc loc in pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) @@ -602,6 +602,11 @@ let rec pr_vernac = function | VernacScheme l -> hov 2 (str"Scheme" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) + | VernacCombinedScheme (id, l) -> + hov 2 (str"Combined Scheme" ++ spc() ++ + pr_lident id ++ spc() ++ str"from" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) + (* Gallina extensions *) | VernacRecord (b,(oc,name),ps,s,c,fs) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 23787f4c..9f828c96 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_coqast.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *) +(* $Id: q_coqast.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) open Util open Names @@ -19,13 +19,18 @@ let purge_str s = if String.length s == 0 || s.[0] <> '$' then s else String.sub s 1 (String.length s - 1) +IFDEF OCAML308 THEN DEFINE NOP END +IFDEF OCAML309 THEN DEFINE NOP END +IFDEF CAMLP5 THEN DEFINE NOP END + let anti loc x = let e = let loc = - ifdef OCAML_308 then + IFDEF NOP THEN loc - else - (1, snd loc - fst loc) + ELSE + (1, snd loc - fst loc) + END in <:expr< $lid:purge_str x$ >> in <:expr< $anti:e$ >> diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 2ef56907..552c144a 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_util.ml4 9333 2006-11-02 13:59:14Z barras $ *) +(* $Id: q_util.ml4 10087 2007-08-24 10:39:30Z herbelin $ *) (* This file defines standard combinators to build ml expressions *) @@ -37,18 +37,18 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) l (let loc = dummy_loc in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in - let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in <:expr< ($e1$, $e2$, $e3$) >> (* We don't give location for tactic quotation! *) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 73d41465..2dfe489e 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) +(* $Id: tacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *) +open Util open Genarg open Q_util open Q_coqast open Argextend -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 7cf542fe..4847f385 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) +(* $Id: vernacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *) +open Util open Genarg open Q_util open Q_coqast open Argextend -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> -- cgit v1.2.3