aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml125
-rw-r--r--parsing/cLexer.mli13
-rw-r--r--parsing/dune1
-rw-r--r--parsing/extend.ml23
-rw-r--r--parsing/g_constr.mlg6
-rw-r--r--parsing/g_prim.mlg1
-rw-r--r--parsing/notation_gram.ml2
-rw-r--r--parsing/pcoq.ml242
-rw-r--r--parsing/pcoq.mli27
-rw-r--r--parsing/tok.ml19
-rw-r--r--parsing/tok.mli4
11 files changed, 194 insertions, 269 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 619718f723..49d6cf01d9 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -11,28 +11,7 @@
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 = 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;
- 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 (!@) = to_coqloc
+open Gramlib
(* Dictionaries: trees annotated with string options, each node being a map
from chars to dictionaries (the subtrees). A trie, in other words. *)
@@ -127,18 +106,22 @@ module Error = struct
end
open Error
-let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str)
+let err loc str = Loc.raise ~loc (Error.E str)
let bad_token str = raise (Error.E (Bad_token str))
(* 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)
+ Ploc.sub loc (bp - loc.Loc.bp) (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)
+ Loc.{ loc with
+ line_nb = loc.line_nb + 1;
+ line_nb_last = loc.line_nb + 1;
+ bol_pos;
+ bol_pos_last = bol_pos;
+ }
(* 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,
@@ -146,19 +129,25 @@ let bump_loc_line loc bol_pos =
(* 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 open Loc in
+ let loc' = { loc with
+ line_nb = loc.line_nb_last + 1;
+ line_nb_last = loc.line_nb_last + 1;
+ bol_pos;
+ bol_pos_last = bol_pos;
+ bp = loc.bp + 1;
+ ep = loc.ep + 1;
+ } in
+ Loc.merge loc 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)
+ Loc.{ loc with
+ line_nb = loc.line_nb_last;
+ bol_pos = loc.bol_pos_last;
+ bp = loc.ep;
+ }
(** Lexer conventions on tokens *)
@@ -323,7 +312,7 @@ let rec ident_tail loc len s = match Stream.peek s with
| Utf8Token (st, n) when Unicode.is_unknown st ->
let id = get_buff len in
let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
- warn_unrecognized_unicode ~loc:!@loc (u,id); len
+ warn_unrecognized_unicode ~loc (u,id); len
| _ -> len
let rec number len s = match Stream.peek s with
@@ -367,7 +356,7 @@ let rec string loc ~comm_level bp len s = match Stream.peek s with
Stream.junk s;
let () = match comm_level with
| Some 0 ->
- warn_comment_terminator_in_string ~loc:!@loc ()
+ warn_comment_terminator_in_string ~loc ()
| _ -> ()
in
let comm_level = Option.map pred comm_level in
@@ -559,20 +548,27 @@ let process_sequence loc bp c cs =
aux 1 cs
(* Must be a special token *)
-let process_chars loc bp c cs =
+let process_chars ~diff_mode loc bp c cs =
let t = progress_from_byte loc None (-1) !token_tree cs c in
let ep = Stream.count cs in
match t with
| Some t -> (KEYWORD t, set_loc_pos loc bp ep)
| None ->
let ep' = bp + utf8_char_size loc cs c in
- njunk (ep' - ep) cs;
- let loc = set_loc_pos loc bp ep' in
- err loc Undefined_token
+ if diff_mode then begin
+ let len = ep' - bp in
+ ignore (store 0 c);
+ ignore (nstore (len - 1) 1 cs);
+ IDENT (get_buff len), set_loc_pos loc bp ep
+ end else begin
+ njunk (ep' - ep) cs;
+ let loc = set_loc_pos loc bp ep' in
+ err loc Undefined_token
+ end
(* Parse what follows a dot *)
-let parse_after_dot loc c bp s = match Stream.peek s with
+let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with
| Some ('a'..'z' | 'A'..'Z' | '_' as d) ->
Stream.junk s;
let len =
@@ -587,11 +583,11 @@ let parse_after_dot loc c bp s = match Stream.peek s with
let len = ident_tail loc (nstore n 0 s) s in
let field = get_buff len in
(try find_keyword loc ("."^field) s with Not_found -> FIELD field)
- | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s)
+ | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s)
(* Parse what follows a question mark *)
-let parse_after_qmark loc bp s =
+let parse_after_qmark ~diff_mode loc bp s =
match Stream.peek s with
| Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK
| None -> KEYWORD "?"
@@ -599,7 +595,7 @@ let parse_after_qmark loc bp s =
match lookup_utf8 loc s with
| Utf8Token (st, _) when Unicode.is_valid_ident_initial st -> LEFTQMARK
| AsciiChar | Utf8Token _ | EmptyStream ->
- fst (process_chars loc bp '?' s)
+ fst (process_chars ~diff_mode loc bp '?' s)
let blank_or_eof cs =
match Stream.peek cs with
@@ -609,20 +605,20 @@ let blank_or_eof cs =
(* Parse a token in a char stream *)
-let rec next_token loc s =
+let rec next_token ~diff_mode loc s =
let bp = Stream.count s in
match Stream.peek s with
| Some ('\n' as c) ->
Stream.junk s;
let ep = Stream.count s in
- comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s
+ comm_loc bp; push_char c; next_token ~diff_mode (bump_loc_line loc ep) s
| Some (' ' | '\t' | '\r' as c) ->
Stream.junk s;
- comm_loc bp; push_char c; next_token loc s
+ comm_loc bp; push_char c; next_token ~diff_mode loc s
| Some ('.' as c) ->
Stream.junk s;
let t =
- try parse_after_dot loc c bp s with
+ try parse_after_dot ~diff_mode loc c bp s with
Stream.Failure -> raise (Stream.Error "")
in
let ep = Stream.count s in
@@ -641,13 +637,13 @@ let rec next_token loc s =
Stream.junk s;
let t,new_between_commands =
if !between_commands then process_sequence loc bp c s, true
- else process_chars loc bp c s,false
+ else process_chars ~diff_mode loc bp c s,false
in
comment_stop bp; between_commands := new_between_commands; t
| Some '?' ->
Stream.junk s;
let ep = Stream.count s in
- let t = parse_after_qmark loc bp s in
+ let t = parse_after_qmark ~diff_mode loc bp s in
comment_stop bp; (t, set_loc_pos loc bp ep)
| Some ('a'..'z' | 'A'..'Z' | '_' as c) ->
Stream.junk s;
@@ -681,12 +677,16 @@ let rec next_token loc s =
Stream.junk s;
begin try
match Stream.peek s with
+ | Some '*' when diff_mode ->
+ Stream.junk s;
+ let ep = Stream.count s in
+ (IDENT "(*", set_loc_pos loc bp ep)
| Some '*' ->
Stream.junk s;
comm_loc bp;
push_string "(*";
- let loc = comment loc bp s in next_token loc s
- | _ -> let t = process_chars loc bp c s in comment_stop bp; t
+ let loc = comment loc bp s in next_token ~diff_mode loc s
+ | _ -> let t = process_chars ~diff_mode loc bp c s in comment_stop bp; t
with Stream.Failure -> raise (Stream.Error "")
end
| Some ('{' | '}' as c) ->
@@ -694,7 +694,7 @@ let rec next_token loc s =
let ep = Stream.count s in
let t,new_between_commands =
if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true
- else process_chars loc bp c s, false
+ else process_chars ~diff_mode loc bp c s, false
in
comment_stop bp; between_commands := new_between_commands; t
| _ ->
@@ -706,14 +706,14 @@ let rec next_token loc s =
comment_stop bp;
(try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
| AsciiChar | Utf8Token _ ->
- let t = process_chars loc bp (Stream.next s) s in
+ let t = process_chars ~diff_mode loc bp (Stream.next s) s in
comment_stop bp; t
| EmptyStream ->
comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
(* (* Debug: uncomment this for tracing tokens seen by coq...*)
-let next_token loc s =
- let (t,loc as r) = next_token loc s in
+let next_token ~diff_mode loc s =
+ let (t,loc as r) = next_token ~diff_mode loc s in
Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t);
r *)
@@ -754,9 +754,9 @@ let token_text = function
| (con, "") -> con
| (con, prm) -> con ^ " \"" ^ prm ^ "\""
-let func cs =
+let func next_token cs =
let loct = loct_create () in
- let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in
+ let cur_loc = ref (Loc.create !current_file 1 0 0 0) in
let ts =
Stream.from
(fun i ->
@@ -766,17 +766,18 @@ let func cs =
in
(ts, loct_func loct)
-let lexer = {
- Plexing.tok_func = func;
+let make_lexer ~diff_mode = {
+ Plexing.tok_func = func (next_token ~diff_mode);
Plexing.tok_using =
(fun pat -> match Tok.of_pattern pat with
| KEYWORD s -> add_keyword s
| _ -> ());
Plexing.tok_removing = (fun _ -> ());
Plexing.tok_match = Tok.match_pattern;
- Plexing.tok_comm = None;
Plexing.tok_text = token_text }
+let lexer = make_lexer ~diff_mode:false
+
(** Terminal symbols interpretation *)
let is_ident_not_keyword s =
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index e4aa8debc1..af3fd7f318 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -40,7 +40,7 @@ where
tok_text : pattern -> string;
tok_comm : mutable option (list location) }
*)
-include Grammar.GLexerType with type te = Tok.t
+include Gramlib.Grammar.GLexerType with type te = Tok.t
module Error : sig
type t
@@ -56,3 +56,14 @@ val set_lexer_state : lexer_state -> unit
val get_lexer_state : unit -> lexer_state
val drop_lexer_state : unit -> unit
val get_comment_state : lexer_state -> ((int * int) * string) list
+
+(** Create a lexer. true enables alternate handling for computing diffs.
+It ensures that, ignoring white space, the concatenated tokens equal the input
+string. Specifically:
+- for strings, return the enclosing quotes as tokens and treat the quoted value
+as if it was unquoted, possibly becoming multiple tokens
+- for comments, return the "(*" as a token and treat the contents of the comment as if
+it was not in a comment, possibly becoming multiple tokens
+- return any unrecognized Ascii or UTF-8 character as a string
+*)
+val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer
diff --git a/parsing/dune b/parsing/dune
index 0669e3a3c2..e91740650f 100644
--- a/parsing/dune
+++ b/parsing/dune
@@ -2,7 +2,6 @@
(name parsing)
(public_name coq.parsing)
(wrapped false)
- (flags :standard -open Gramlib)
(libraries coq.gramlib proofs))
(rule
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6fe2956643..9b5537d7f6 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -10,21 +10,12 @@
(** Entry keys for constr notations *)
-type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
+type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e
type side = Left | Right
-type gram_assoc = NonA | RightA | LeftA
-
-type gram_position =
- | First
- | Last
- | Before of string
- | After of string
- | Level of string
-
type production_position =
- | BorderProd of side * gram_assoc option
+ | BorderProd of side * Gramlib.Gramext.g_assoc option
| InternalProd
type production_level =
@@ -115,12 +106,12 @@ type 'a production_rule =
type 'a single_extend_statement =
string option *
- (** Level *)
- gram_assoc option *
- (** Associativity *)
+ (* Level *)
+ Gramlib.Gramext.g_assoc option *
+ (* Associativity *)
'a production_rule list
- (** Symbol list with the interpretation function *)
+ (* Symbol list with the interpretation function *)
type 'a extend_statement =
- gram_position option *
+ Gramlib.Gramext.position option *
'a single_extend_statement list
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index e25f7aa54f..b3ae24e941 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -81,7 +81,7 @@ let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
let lpar_id_coloneq =
- Gram.Entry.of_parser "test_lpar_id_coloneq"
+ Pcoq.Entry.of_parser "test_lpar_id_coloneq"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
@@ -96,7 +96,7 @@ let lpar_id_coloneq =
| _ -> err ())
let impl_ident_head =
- Gram.Entry.of_parser "impl_ident_head"
+ Pcoq.Entry.of_parser "impl_ident_head"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD "{" ->
@@ -109,7 +109,7 @@ let impl_ident_head =
| _ -> err ())
let name_colon =
- Gram.Entry.of_parser "name_colon"
+ Pcoq.Entry.of_parser "name_colon"
(fun strm ->
match stream_nth 0 strm with
| IDENT s ->
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index dfb788907e..6247a12640 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -13,7 +13,6 @@
open Names
open Libnames
-open Pcoq
open Pcoq.Prim
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index d8c08803b6..fc5feba58b 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -32,7 +32,7 @@ type grammar_constr_prod_item =
type one_notation_grammar = {
notgram_level : level;
- notgram_assoc : Extend.gram_assoc option;
+ notgram_assoc : Gramlib.Gramext.g_assoc option;
notgram_notation : Constrexpr.notation;
notgram_prods : grammar_constr_prod_item list list;
}
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index eb3e633892..19ae97da77 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -12,32 +12,7 @@ open CErrors
open Util
open Extend
open Genarg
-
-let curry f x y = f (x, y)
-let uncurry f (x,y) = f x y
-
-(** Location Utils *)
-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 of_coqloc loc =
- let open Loc in
- Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
-
-let to_coqloc 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;
- 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 (!@) = to_coqloc
+open Gramlib
(** The parser of Coq *)
module G : sig
@@ -59,7 +34,7 @@ module type S =
type e 'a = 'y;
value create : string -> e 'a;
value parse : e 'a -> parsable -> 'a;
- value parse_token : e 'a -> Stream.t te -> 'a;
+ value parse_token_stream : e 'a -> Stream.t te -> 'a;
value name : e 'a -> string;
value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
value print : Format.formatter -> e 'a -> unit;
@@ -82,28 +57,18 @@ module type S =
end
*)
- 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 coq_parsable
val coq_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
val comment_state : coq_parsable -> ((int * int) * string) list
-end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
+end with type 'a Entry.e = 'a Extend.entry = struct
include Grammar.GMake(CLexer)
- 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 coq_parsable = parsable * CLexer.lexer_state ref
let coq_parsable ?(file=Loc.ToplevelInput) c =
@@ -113,7 +78,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
state := CLexer.get_lexer_state ();
(a,state)
- let action = Gramext.action
let entry_create = Entry.create
let entry_parse e (p,state) =
@@ -125,7 +89,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
with Ploc.Exc (loc,e) ->
CLexer.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
+ let loc = match loc' with None -> loc | Some loc -> loc in
Loc.raise ~loc e
let comment_state (p,state) =
@@ -148,34 +112,16 @@ struct
let create = G.Entry.create
let parse = G.entry_parse
let print = G.Entry.print
+ let of_parser = G.Entry.of_parser
+ let name = G.Entry.name
+ let parse_token_stream = G.Entry.parse_token_stream
end
-let warning_verbose = Gramext.warning_verbose
-
-let of_coq_assoc = function
-| Extend.RightA -> Gramext.RightA
-| Extend.LeftA -> Gramext.LeftA
-| Extend.NonA -> Gramext.NonA
-
-let of_coq_position = function
-| Extend.First -> Gramext.First
-| Extend.Last -> Gramext.Last
-| Extend.Before s -> Gramext.Before s
-| Extend.After s -> Gramext.After s
-| Extend.Level s -> Gramext.Level s
-
module Symbols : 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 stoken : Tok.t -> ('s, string) G.ty_symbol
+ val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
+ val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
end = struct
let stoken tok =
@@ -190,27 +136,12 @@ end = struct
| Tok.BULLET s -> "BULLET", s
| Tok.EOI -> "EOI", ""
in
- Gramext.Stoken pattern
-
- let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
- let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
-
- 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
+ G.s_token pattern
+ let slist0sep x y = G.s_list0sep x y false
+ let slist1sep x y = G.s_list1sep x y false
end
-let camlp5_verbosity silent f x =
- let a = !warning_verbose in
- warning_verbose := silent;
- f x;
- warning_verbose := a
-
(** Grammar extensions *)
(** NB: [extend_statement =
@@ -224,61 +155,71 @@ let camlp5_verbosity silent f x =
(** Binding general entry keys to symbol *)
-let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function
-| Stop -> fun f -> G.action (fun loc -> f (!@ loc))
-| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x))
-
-let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
- | Atoken t -> Symbols.stoken t
- | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
- | Alist1sep (s,sep) ->
- Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
- | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
- | Alist0sep (s,sep) ->
- Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
- | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
- | Aself -> Symbols.sself
- | Anext -> Symbols.snext
- | Aentry e ->
- Symbols.snterm (G.Entry.obj e)
- | Aentryl (e, n) ->
- Symbols.snterml (G.Entry.obj e, n)
- | Arules rs ->
- Gramext.srules (List.map symbol_of_rules rs)
-
-and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
-| Stop -> fun accu -> accu
-| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
-
-and symbol_of_rules : type a. a Extend.rules -> _ = function
+type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function
+| Atoken t -> Symbols.stoken t
+| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s)
+| Alist1sep (s,sep) ->
+ Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
+| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s)
+| Alist0sep (s,sep) ->
+ Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
+| Aopt s -> G.s_opt (symbol_of_prod_entry_key s)
+| Aself -> G.s_self
+| Anext -> G.s_next
+| Aentry e -> G.s_nterm e
+| Aentryl (e, n) -> G.s_nterml e n
+| Arules rs ->
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)
+
+and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function
+| Stop -> Casted (G.r_stop, fun act loc -> act loc)
+| Next (r, s) ->
+ let Casted (r, cast) = symbol_of_rule r in
+ Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x)))
+
+and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function
| Rules (r, act) ->
- let symb = symbol_of_rule r.norec_rule [] in
- let act = of_coq_action r.norec_rule act in
- (symb, act)
+ let Casted (symb, cast) = symbol_of_rule r.norec_rule in
+ G.production (symb, cast act)
+
+(** FIXME: This is a hack around a deficient camlp5 API *)
+type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production
-let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
-| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
+let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
+| Rule (toks, act) ->
+ let Casted (symb, cast) = symbol_of_rule toks in
+ AnyProduction (symb, cast act)
let of_coq_single_extend_statement (lvl, assoc, rule) =
- (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+ (lvl, assoc, List.map of_coq_production_rule rule)
let of_coq_extend_statement (pos, st) =
- (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+ (pos, List.map of_coq_single_extend_statement st)
+
+let fix_extend_statement (pos, st) =
+ let fix_single_extend_statement (lvl, assoc, rules) =
+ let fix_production_rule (AnyProduction (s, act)) = G.production (s, act) in
+ (lvl, assoc, List.map fix_production_rule rules)
+ in
+ (pos, List.map fix_single_extend_statement st)
(** Type of reinitialization data *)
-type gram_reinit = gram_assoc * gram_position
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
type extend_rule =
-| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
module EntryCommand = Dyn.Make ()
-module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end
+module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end
module EntryDataMap = EntryCommand.Map(EntryData)
type ext_kind =
| ByGrammar of extend_rule
| ByEXTEND of (unit -> unit) * (unit -> unit)
- | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind
+ | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind
(** The list of extensions *)
@@ -291,17 +232,16 @@ let camlp5_entries = ref EntryDataMap.empty
let grammar_delete e reinit (pos,rls) =
List.iter
(fun (n,ass,lev) ->
- List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+ List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
(List.rev rls);
match reinit with
| Some (a,ext) ->
- let a = of_coq_assoc a in
- let ext = of_coq_position ext in
let lev = match pos with
| Some (Gramext.Level n) -> n
| _ -> assert false
in
- (G.extend e) (Some ext) [Some lev,Some a,[]]
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
| None -> ()
(** Extension *)
@@ -309,13 +249,15 @@ let grammar_delete e reinit (pos,rls) =
let grammar_extend e reinit ext =
let ext = of_coq_extend_statement ext in
let undo () = grammar_delete e reinit ext in
- let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in
+ let pos, ext = fix_extend_statement ext in
+ let redo () = G.safe_extend ~warning:None e pos ext in
camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
redo ()
let grammar_extend_sync e reinit ext =
camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
- camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
+ let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
+ G.safe_extend ~warning:None e pos ext
(** The apparent parser of Coq; encapsulate G to keep track
of the extensions. *)
@@ -323,25 +265,6 @@ let grammar_extend_sync e reinit ext =
module Gram =
struct
include G
- let extend e =
- curry
- (fun ext ->
- camlp5_state :=
- (ByEXTEND ((fun () -> grammar_delete e None ext),
- (fun () -> uncurry (G.extend e) ext)))
- :: !camlp5_state;
- uncurry (G.extend e) ext)
- let delete_rule e pil =
- (* spiwack: if you use load an ML module which contains GDELETE_RULE
- in a section, God kills a kitty. As it would corrupt remove_grammars.
- There does not seem to be a good way to undo a delete rule. As deleting
- takes fewer arguments than extending. The production rule isn't returned
- by delete_rule. If we could retrieve the necessary information, then
- ByEXTEND provides just the framework we need to allow this in section.
- I'm not entirely sure it makes sense, but at least it would be more correct.
- *)
- G.delete_rule e pil
- let gram_extend e ext = grammar_extend e None ext
end
(** Remove extensions
@@ -380,16 +303,18 @@ let make_rule r = [None, None, r]
let eoi_entry en =
let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
- let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
- let act = Gram.action (fun _ x loc -> x) in
- uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+ let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in
+ let act = fun _ x loc -> x in
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]);
e
let map_entry f en =
let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
- let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
- let act = Gram.action (fun x loc -> f x) in
- uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+ let symbs = G.r_next G.r_stop (G.s_nterm en) in
+ let act = fun x loc -> f x in
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]);
e
(* Parse a string, does NOT check if the entire string was read
@@ -516,10 +441,11 @@ module Module =
end
let epsilon_value f e =
- let r = Rule (Next (Stop, e), fun x _ -> f x) in
- let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+ let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
+ let ext = [None, None, [r]] in
let entry = Gram.entry_create "epsilon" in
- let () = uncurry (G.extend entry) ext in
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ let () = G.safe_extend ~warning:(Some warning) entry None ext in
try Some (parse_string entry "") with _ -> None
(** Synchronized grammar extensions *)
@@ -572,7 +498,7 @@ let extend_grammar_command tag g =
let nb = List.length rules in
grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
-let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list =
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list =
let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
let grammar_state = match !grammar_stack with
| [] -> GramState.empty
@@ -604,7 +530,7 @@ let extend_dyn_grammar (e, _) = match e with
(** Registering extra grammar *)
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry
let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
@@ -627,7 +553,7 @@ type frozen_t =
(grammar_entry * GramState.t) list *
CLexer.keyword_state
-let freeze _ : frozen_t =
+let freeze ~marshallable : frozen_t =
(!grammar_stack, CLexer.get_keyword_state ())
(* We compare the current state of the grammar and the state to unfreeze,
@@ -660,7 +586,7 @@ let parser_summary_tag =
Summary.init_function = Summary.nop }
let with_grammar_rule_protection f x =
- let fs = freeze false in
+ let fs = freeze ~marshallable:false in
try let a = f x in unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c05229d576..352857d4cd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -16,17 +16,6 @@ open Libnames
(** The parser of Coq *)
-(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE.
- We only have it here to work with Camlp5. Handwritten grammar extensions
- should use the safe [Pcoq.grammar_extend] function below. *)
-module Gram : sig
-
- include Grammar.S with type te = Tok.t
-
- val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit
-
-end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
-
module Parsable :
sig
type t
@@ -36,10 +25,13 @@ sig
end
module Entry : sig
- type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+ type 'a t = 'a Extend.entry
val create : string -> 'a t
val parse : 'a t -> Parsable.t -> 'a
val print : Format.formatter -> 'a t -> unit
+ val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t
+ val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
+ val name : 'a t -> string
end
(** The parser of Coq is built from three kinds of rule declarations:
@@ -117,10 +109,6 @@ end
*)
-(** Temporarily activate camlp5 verbosity *)
-
-val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
-
(** Parse a string *)
val parse_string : 'a Entry.t -> string -> 'a
@@ -209,7 +197,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** {5 Extending the parser without synchronization} *)
-type gram_reinit = gram_assoc * gram_position
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
(** Type of reinitialization data *)
val grammar_extend : 'a Entry.t -> gram_reinit option ->
@@ -272,11 +260,6 @@ val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-(** Location Utils *)
-val of_coqloc : Loc.t -> Ploc.t
-val to_coqloc : Ploc.t -> Loc.t
-val (!@) : Ploc.t -> Loc.t
-
type frozen_t
val parser_summary_tag : frozen_t Summary.Dyn.tag
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 91b4f25ba3..03825e350f 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -36,12 +36,25 @@ let equal t1 t2 = match t1, t2 with
| EOI, EOI -> true
| _ -> false
-let extract_string = function
+let extract_string diff_mode = function
| KEYWORD s -> s
| IDENT s -> s
- | STRING s -> s
+ | STRING s ->
+ if diff_mode then
+ let escape_quotes s =
+ let len = String.length s in
+ let buf = Buffer.create len in
+ for i = 0 to len-1 do
+ let ch = String.get s i in
+ Buffer.add_char buf ch;
+ if ch = '"' then Buffer.add_char buf '"' else ()
+ done;
+ Buffer.contents buf
+ in
+ "\"" ^ (escape_quotes s) ^ "\""
+ else s
| PATTERNIDENT s -> s
- | FIELD s -> s
+ | FIELD s -> if diff_mode then "." ^ s else s
| INT s -> s
| LEFTQMARK -> "?"
| BULLET s -> s
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 9b8c008555..5750096a28 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -22,11 +22,13 @@ type t =
| EOI
val equal : t -> t -> bool
-val extract_string : t -> string
+(* pass true for diff_mode *)
+val extract_string : bool -> t -> string
val to_string : t -> string
(* Needed to fit Camlp5 signature *)
val print : Format.formatter -> t -> unit
val match_keyword : string -> t -> bool
+
(** for camlp5 *)
val of_pattern : string*string -> t
val to_pattern : t -> string*string
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:42:30 +0000