aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml422
-rw-r--r--parsing/cLexer.mli15
-rw-r--r--parsing/egramcoq.ml10
-rw-r--r--parsing/egramcoq.mli10
-rw-r--r--parsing/egramml.ml10
-rw-r--r--parsing/egramml.mli10
-rw-r--r--parsing/g_constr.ml410
-rw-r--r--parsing/g_prim.ml410
-rw-r--r--parsing/g_proofs.ml410
-rw-r--r--parsing/g_vernac.ml422
-rw-r--r--parsing/pcoq.ml27
-rw-r--r--parsing/pcoq.mli15
-rw-r--r--parsing/tok.ml10
-rw-r--r--parsing/tok.mli10
14 files changed, 103 insertions, 88 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 52a6fe16c..d65b35c46 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
@@ -384,16 +386,6 @@ let comments = ref []
let current_comment = Buffer.create 8192
let between_commands = ref true
-let rec split_comments comacc acc pos = function
- [] -> comments := List.rev acc; comacc
- | ((b,e),c as com)::coms ->
- (* Take all comments that terminates before pos, or begin exactly
- at pos (used to print comments attached after an expression) *)
- if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
- else split_comments comacc (com::acc) pos coms
-
-let extract_comments pos = split_comments [] [] pos !comments
-
(* The state of the lexer visible from outside *)
type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source
@@ -410,6 +402,8 @@ let release_lexer_state = get_lexer_state
let drop_lexer_state () =
set_lexer_state (init_lexer_state Loc.ToplevelInput)
+let get_comment_state (_,_,_,c,_) = c
+
let real_push_char c = Buffer.add_char current_comment c
(* Add a char if it is between two commands, if it is a newline or
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 5f4e10f14..a14f08d91 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** This should be functional but it is not due to the interface *)
@@ -55,7 +57,4 @@ val get_lexer_state : unit -> lexer_state
val release_lexer_state : unit -> lexer_state
[@@ocaml.deprecated "Use get_lexer_state"]
val drop_lexer_state : unit -> unit
-
-(* Retrieve the comments lexed at a given location of the stream
- currently being processeed *)
-val extract_comments : int -> string list
+val get_comment_state : lexer_state -> ((int * int) * string) list
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index cad837d08..c0ead3a0a 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open CErrors
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 1e3869818..e15add10f 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Mapping of grammar productions to camlp5 actions *)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index cf9485b73..90cd7d10b 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 74dd95a20..31aa1a989 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Vernacexpr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8a1e6d121..b4f09ee6a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 0b7efe739..a1d36b822 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 44f46578c..e393c2bbf 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Constrexpr
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 93e534e0b..feaef3161 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1,19 +1,21 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open CErrors
open Util
open Names
+open Vernacexpr
open Constrexpr
open Constrexpr_ops
open Extend
-open Vernacexpr
open Decl_kinds
open Declarations
open Misctypes
@@ -56,9 +58,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
| "8.8" -> Current
| "8.7" -> V8_7
| "8.6" -> V8_6
- | "8.5" -> V8_5
- | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
- if allow_old then VOld else
+ | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
CErrors.user_err ~hdr:"get_compat_version"
Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
| s ->
@@ -142,7 +142,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
(* Gallina declarations *)
GEXTEND Gram
GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
- record_field decl_notation rec_definition ident_decl;
+ record_field decl_notation rec_definition ident_decl univ_decl;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
@@ -557,8 +557,8 @@ GEXTEND Gram
[ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
- [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
- CWith_Definition (fqid,c)
+ [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
+ CWith_Definition (fqid,udecl,c)
| IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
CWith_Module (fqid,qid)
] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 7a51908d9..258c4bb11 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open CErrors
@@ -88,7 +90,9 @@ module type S =
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 comment_state : coq_parsable -> ((int * int) * string) list
+
val srules' : production_rule list -> symbol
val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
@@ -105,6 +109,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
string option * Gramext.g_assoc option * production_rule list
type extend_statment =
Gramext.position option * single_extend_statment list
+
type coq_parsable = parsable * CLexer.lexer_state ref
let parsable ?(file=Loc.ToplevelInput) c =
@@ -129,15 +134,8 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
Loc.raise ~loc e
- let with_parsable (p,state) f x =
- CLexer.set_lexer_state !state;
- try
- let a = f x in
- state := CLexer.get_lexer_state ();
- a
- with e ->
- CLexer.drop_lexer_state ();
- raise e
+ let comment_state (p,state) =
+ CLexer.get_comment_state !state
let entry_print ft x = Entry.print ft x
@@ -444,6 +442,7 @@ module Prim =
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
+ let univ_decl = Gram.entry_create "Prim.univ_decl"
let ident_decl = Gram.entry_create "Prim.ident_decl"
let pattern_ident = Gram.entry_create "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f36250176..e66aa4ade 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Loc
@@ -78,7 +80,9 @@ module type S =
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
+
+ (* Get comment parsing information from the Lexer *)
+ val comment_state : coq_parsable -> ((int * int) * string) list
(* Apparently not used *)
val srules' : production_rule list -> symbol
@@ -194,6 +198,7 @@ module Prim :
val ident : Id.t Gram.entry
val name : lname Gram.entry
val identref : lident Gram.entry
+ val univ_decl : universe_decl_expr Gram.entry
val ident_decl : ident_decl Gram.entry
val pattern_ident : Id.t Gram.entry
val pattern_identref : lident Gram.entry
diff --git a/parsing/tok.ml b/parsing/tok.ml
index fafad2779..91b4f25ba 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** The type of token for the Coq lexer and parser *)
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 162310e2a..9b8c00855 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** The type of token for the Coq lexer and parser *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 07:53:42 +0000