aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml429
-rw-r--r--parsing/cLexer.mli2
-rw-r--r--parsing/g_constr.ml410
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--parsing/pcoq.ml11
-rw-r--r--parsing/pcoq.mli3
6 files changed, 39 insertions, 24 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 636027f9b..9c9189ffe 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -10,8 +10,19 @@ open Pp
open Util
open Tok
+(** Location utilities *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
+let coq_file_of_ploc_file s =
+ if s = "" then Loc.ToplevelInput else Loc.InFile s
+
+let from_coqloc fname line_nb bol_pos bp ep =
+ Ploc.make_loc (ploc_file_of_coq_file fname) line_nb bol_pos (bp, ep) ""
+
let to_coqloc loc =
- { Loc.fname = Ploc.file_name loc;
+ { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
Loc.line_nb = Ploc.line_nb loc;
Loc.bol_pos = Ploc.bol_pos loc;
Loc.bp = Ploc.first_pos loc;
@@ -118,14 +129,6 @@ let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str)
let bad_token str = raise (Error.E (Bad_token str))
-(** Location utilities *)
-let file_loc_of_file = function
-| None -> ""
-| Some f -> f
-
-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)
@@ -369,7 +372,7 @@ let rec string loc ~comm_level bp len = parser
err loc Unterminated_string
(* To associate locations to a file name *)
-let current_file = ref None
+let current_file = ref Loc.ToplevelInput
(* Utilities for comments in beautify *)
let comment_begin = ref None
@@ -392,7 +395,7 @@ let rec split_comments comacc acc pos = function
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 * string option
+type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source
let init_lexer_state f = (None,"",true,[],f)
let set_lexer_state (o,s,b,c,f) =
@@ -404,7 +407,7 @@ let set_lexer_state (o,s,b,c,f) =
let release_lexer_state () =
(!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
let drop_lexer_state () =
- set_lexer_state (init_lexer_state None)
+ set_lexer_state (init_lexer_state Loc.ToplevelInput)
let real_push_char c = Buffer.add_char current_comment c
@@ -672,7 +675,7 @@ let token_text = function
let func cs =
let loct = loct_create () in
- let cur_loc = ref (make_loc !current_file 1 0 0 0) in
+ let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in
let ts =
Stream.from
(fun i ->
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 77d652b18..d3ef19873 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -49,7 +49,7 @@ end
(* Mainly for comments state, etc... *)
type lexer_state
-val init_lexer_state : string option -> lexer_state
+val init_lexer_state : Loc.source -> lexer_state
val set_lexer_state : lexer_state -> unit
val release_lexer_state : unit -> lexer_state
val drop_lexer_state : unit -> unit
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f637e9746..7d0728458 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -123,8 +123,8 @@ let name_colon =
let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None
GEXTEND Gram
- GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
- constr_pattern lconstr_pattern Constr.ident
+ GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
+ global constr_pattern lconstr_pattern Constr.ident
closed_binder open_binders binder binders binders_fixannot
record_declaration typeclass_constraint pattern appl_arg;
Constr.ident:
@@ -149,6 +149,12 @@ GEXTEND Gram
| "Type"; "@{"; u = universe; "}" -> GType u
] ]
;
+ sort_family:
+ [ [ "Set" -> Sorts.InSet
+ | "Prop" -> Sorts.InProp
+ | "Type" -> Sorts.InType
+ ] ]
+ ;
universe:
[ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
| id = name -> [id]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7a7746cc9..de98415cd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -340,13 +340,13 @@ GEXTEND Gram
;
scheme_kind:
[ [ IDENT "Induction"; "for"; ind = smart_global;
- IDENT "Sort"; s = sort-> InductionScheme(true,ind,s)
+ IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s)
| IDENT "Minimality"; "for"; ind = smart_global;
- IDENT "Sort"; s = sort-> InductionScheme(false,ind,s)
+ IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s)
| IDENT "Elimination"; "for"; ind = smart_global;
- IDENT "Sort"; s = sort-> CaseScheme(true,ind,s)
+ IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s)
| IDENT "Case"; "for"; ind = smart_global;
- IDENT "Sort"; s = sort-> CaseScheme(false,ind,s)
+ IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s)
| IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ]
;
(* Various Binders *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 81f02bf95..40c5da7a5 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -15,8 +15,11 @@ let curry f x y = f (x, y)
let uncurry f (x,y) = f x y
(** Location Utils *)
+let coq_file_of_ploc_file s =
+ if s = "" then Loc.ToplevelInput else Loc.InFile s
+
let to_coqloc loc =
- { Loc.fname = Ploc.file_name loc;
+ { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
Loc.line_nb = Ploc.line_nb loc;
Loc.bol_pos = Ploc.bol_pos loc;
Loc.bp = Ploc.first_pos loc;
@@ -80,7 +83,7 @@ module type S =
Gramext.position option * single_extend_statment list
type coq_parsable
- val parsable : ?file:string -> char Stream.t -> coq_parsable
+ val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -104,7 +107,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
Gramext.position option * single_extend_statment list
type coq_parsable = parsable * CLexer.lexer_state ref
- let parsable ?file c =
+ let parsable ?(file=Loc.ToplevelInput) c =
let state = ref (CLexer.init_lexer_state file) in
CLexer.set_lexer_state !state;
let a = parsable c in
@@ -471,6 +474,7 @@ module Constr =
let global = make_gen_entry uconstr "global"
let universe_level = make_gen_entry uconstr "universe_level"
let sort = make_gen_entry uconstr "sort"
+ let sort_family = make_gen_entry uconstr "sort_family"
let pattern = Gram.entry_create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
@@ -631,6 +635,7 @@ let () =
Grammar.register0 wit_ident (Prim.ident);
Grammar.register0 wit_var (Prim.var);
Grammar.register0 wit_ref (Prim.reference);
+ Grammar.register0 wit_sort_family (Constr.sort_family);
Grammar.register0 wit_constr (Constr.constr);
Grammar.register0 wit_red_expr (Vernac_.red_expr);
()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 445818e13..4e6bff20a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -73,7 +73,7 @@ module type S =
type coq_parsable
- val parsable : ?file:string -> char Stream.t -> coq_parsable
+ val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -225,6 +225,7 @@ module Constr :
val global : reference Gram.entry
val universe_level : glob_level Gram.entry
val sort : glob_sort Gram.entry
+ val sort_family : Sorts.family Gram.entry
val pattern : cases_pattern_expr Gram.entry
val constr_pattern : constr_expr Gram.entry
val lconstr_pattern : constr_expr Gram.entry
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 09:32:51 +0000