aboutsummaryrefslogtreecommitdiff
path: root/gramlib
diff options
context:
space:
mode:
Diffstat (limited to 'gramlib')
-rw-r--r--gramlib/dune3
-rw-r--r--gramlib/gramext.ml72
-rw-r--r--gramlib/gramext.mli3
-rw-r--r--gramlib/grammar.ml107
-rw-r--r--gramlib/grammar.mli3
-rw-r--r--gramlib/plexing.ml7
-rw-r--r--gramlib/plexing.mli6
-rw-r--r--gramlib/ploc.ml45
-rw-r--r--gramlib/ploc.mli66
9 files changed, 30 insertions, 282 deletions
diff --git a/gramlib/dune b/gramlib/dune
index 6a9e622b4c..8ca6aff25a 100644
--- a/gramlib/dune
+++ b/gramlib/dune
@@ -1,3 +1,4 @@
(library
(name gramlib)
- (public_name coq.gramlib))
+ (public_name coq.gramlib)
+ (libraries coq.lib))
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index c35c4bd18e..46c2688f05 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -8,7 +8,7 @@ type 'a parser_t = 'a Stream.t -> Obj.t
type 'te grammar =
{ gtokens : (Plexing.pattern, int ref) Hashtbl.t;
- mutable glexer : 'te Plexing.lexer }
+ glexer : 'te Plexing.lexer }
type 'te g_entry =
{ egram : 'te grammar;
@@ -52,7 +52,6 @@ type position =
| Last
| Before of string
| After of string
- | Like of string
| Level of string
let rec derive_eps =
@@ -154,27 +153,6 @@ let is_level_labelled n lev =
Some n1 -> n = n1
| None -> false
-let rec token_exists_in_level f lev =
- token_exists_in_tree f lev.lprefix || token_exists_in_tree f lev.lsuffix
-and token_exists_in_tree f =
- function
- Node n ->
- token_exists_in_symbol f n.node || token_exists_in_tree f n.brother ||
- token_exists_in_tree f n.son
- | LocAct (_, _) | DeadEnd -> false
-and token_exists_in_symbol f =
- function
- | Slist0 sy -> token_exists_in_symbol f sy
- | Slist0sep (sy, sep, _) ->
- token_exists_in_symbol f sy || token_exists_in_symbol f sep
- | Slist1 sy -> token_exists_in_symbol f sy
- | Slist1sep (sy, sep, _) ->
- token_exists_in_symbol f sy || token_exists_in_symbol f sep
- | Sopt sy -> token_exists_in_symbol f sy
- | Stoken tok -> f tok
- | Stree t -> token_exists_in_tree f t
- | Snterm _ | Snterml (_, _) | Snext | Sself -> false
-
let insert_level ~warning entry_name e1 symbols action slev =
match e1 with
true ->
@@ -265,58 +243,11 @@ let get_level ~warning entry position levs =
let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
in
get levs
- | Some (Like n) ->
- let f (tok, prm) = n = tok || n = prm in
- let rec get =
- function
- [] ->
- eprintf "No level with \"%s\" in entry \"%s\"\n" n entry.ename;
- flush stderr;
- failwith "Grammar.extend"
- | lev :: levs ->
- if token_exists_in_level f lev then [], change_lev ~warning lev n, levs
- else
- let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
- in
- get levs
| None ->
match levs with
lev :: levs -> [], change_lev ~warning lev "<top>", levs
| [] -> [], empty_lev, []
-let rec check_gram entry =
- function
- Snterm e ->
- if e.egram != entry.egram then
- begin
- eprintf "\
-Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
- entry.ename e.ename;
- flush stderr;
- failwith "Grammar.extend error"
- end
- | Snterml (e, _) ->
- if e.egram != entry.egram then
- begin
- eprintf "\
-Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
- entry.ename e.ename;
- flush stderr;
- failwith "Grammar.extend error"
- end
- | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s
- | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s
- | Slist0 s -> check_gram entry s
- | Slist1 s -> check_gram entry s
- | Sopt s -> check_gram entry s
- | Stree t -> tree_check_gram entry t
- | Snext | Sself | Stoken _ -> ()
-and tree_check_gram entry =
- function
- Node {node = n; brother = bro; son = son} ->
- check_gram entry n; tree_check_gram entry bro; tree_check_gram entry son
- | LocAct (_, _) | DeadEnd -> ()
-
let change_to_self entry =
function
Snterm e when e == entry -> Sself
@@ -373,7 +304,6 @@ let levels_of_rules ~warning entry position rules =
List.fold_left
(fun lev (symbols, action) ->
let symbols = List.map (change_to_self entry) symbols in
- List.iter (check_gram entry) symbols;
let (e1, symbols) = get_initial entry symbols in
insert_tokens entry.egram symbols;
insert_level ~warning entry.ename e1 symbols action lev)
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index ecb95ec61b..f1e294fb4c 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -6,7 +6,7 @@ type 'a parser_t = 'a Stream.t -> Obj.t
type 'te grammar =
{ gtokens : (Plexing.pattern, int ref) Hashtbl.t;
- mutable glexer : 'te Plexing.lexer }
+ glexer : 'te Plexing.lexer }
type 'te g_entry =
{ egram : 'te grammar;
@@ -50,7 +50,6 @@ type position =
| Last
| Before of string
| After of string
- | Like of string
| Level of string
val levels_of_rules : warning:(string -> unit) option ->
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 285c14ec62..0ad11d075f 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -130,7 +130,7 @@ let loc_of_token_interval bp ep =
if bp == ep then
if bp == 0 then Ploc.dummy else Ploc.after (!floc (bp - 1)) 0 1
else
- let loc1 = !floc bp in let loc2 = !floc (pred ep) in Ploc.encl loc1 loc2
+ let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2
let name_of_symbol entry =
function
@@ -186,84 +186,6 @@ and name_of_tree_failed entry =
end
| DeadEnd | LocAct (_, _) -> "???"
-let search_tree_in_entry prev_symb tree =
- function
- Dlevels levels ->
- let rec search_levels =
- function
- [] -> tree
- | level :: levels ->
- match search_level level with
- Some tree -> tree
- | None -> search_levels levels
- and search_level level =
- match search_tree level.lsuffix with
- Some t -> Some (Node {node = Sself; son = t; brother = DeadEnd})
- | None -> search_tree level.lprefix
- and search_tree t =
- if tree <> DeadEnd && t == tree then Some t
- else
- match t with
- Node n ->
- begin match search_symbol n.node with
- Some symb ->
- Some (Node {node = symb; son = n.son; brother = DeadEnd})
- | None ->
- match search_tree n.son with
- Some t ->
- Some (Node {node = n.node; son = t; brother = DeadEnd})
- | None -> search_tree n.brother
- end
- | LocAct (_, _) | DeadEnd -> None
- and search_symbol symb =
- match symb with
- Snterm _ | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) |
- Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ | Stree _
- when symb == prev_symb ->
- Some symb
- | Slist0 symb ->
- begin match search_symbol symb with
- Some symb -> Some (Slist0 symb)
- | None -> None
- end
- | Slist0sep (symb, sep, b) ->
- begin match search_symbol symb with
- Some symb -> Some (Slist0sep (symb, sep, b))
- | None ->
- match search_symbol sep with
- Some sep -> Some (Slist0sep (symb, sep, b))
- | None -> None
- end
- | Slist1 symb ->
- begin match search_symbol symb with
- Some symb -> Some (Slist1 symb)
- | None -> None
- end
- | Slist1sep (symb, sep, b) ->
- begin match search_symbol symb with
- Some symb -> Some (Slist1sep (symb, sep, b))
- | None ->
- match search_symbol sep with
- Some sep -> Some (Slist1sep (symb, sep, b))
- | None -> None
- end
- | Sopt symb ->
- begin match search_symbol symb with
- Some symb -> Some (Sopt symb)
- | None -> None
- end
- | Stree t ->
- begin match search_tree t with
- Some t -> Some (Stree t)
- | None -> None
- end
- | _ -> None
- in
- search_levels levels
- | Dparser _ -> tree
-
-let error_verbose = ref false
-
let tree_failed entry prev_symb_result prev_symb tree =
let txt = name_of_tree_failed entry tree in
let txt =
@@ -295,18 +217,6 @@ let tree_failed entry prev_symb_result prev_symb tree =
| Sopt _ | Stree _ -> txt ^ " expected"
| _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb
in
- if !error_verbose then
- begin let tree = search_tree_in_entry prev_symb tree entry.edesc in
- let ppf = err_formatter in
- fprintf ppf "@[<v 0>@,";
- fprintf ppf "----------------------------------@,";
- fprintf ppf "Parse error in entry [%s], rule:@;<0 2>" entry.ename;
- fprintf ppf "@[";
- print_level ppf pp_force_newline (flatten_tree tree);
- fprintf ppf "@]@,";
- fprintf ppf "----------------------------------@,";
- fprintf ppf "@]@."
- end;
txt ^ " (in [" ^ entry.ename ^ "])"
let symb_failed entry prev_symb_result prev_symb symb =
@@ -374,11 +284,8 @@ let do_recover parser_of_tree entry nlevn alevn bp a s son
continue entry bp a s son (parser_of_tree entry nlevn alevn son)
strm__
-let strict_parsing = ref false
-
let recover parser_of_tree entry nlevn alevn bp a s son strm =
- if !strict_parsing then raise (Stream.Error (tree_failed entry a s son))
- else do_recover parser_of_tree entry nlevn alevn bp a s son strm
+ do_recover parser_of_tree entry nlevn alevn bp a s son strm
let token_count = ref 0
@@ -794,8 +701,6 @@ let tokens g con =
g.gtokens;
!list
-let glexer g = g.glexer
-
type 'te gen_parsable =
{ pa_chr_strm : char Stream.t;
pa_tok_strm : 'te Stream.t;
@@ -816,7 +721,7 @@ let parse_parsable entry p =
let cnt = Stream.count ts in
let loc = fun_loc cnt in
if !token_count - 1 <= cnt then loc
- else Ploc.encl loc (fun_loc (!token_count - 1))
+ else Loc.merge loc (fun_loc (!token_count - 1))
with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1)
in
floc := fun_loc;
@@ -851,7 +756,6 @@ module type S =
type parsable
val parsable : char Stream.t -> parsable
val tokens : string -> (string * int) list
- val glexer : te Plexing.lexer
module Entry :
sig
type 'a e
@@ -884,7 +788,7 @@ module type S =
val r_next :
('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
('self, 'b -> 'a, 'r) ty_rule
- val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
+ val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
module Unsafe :
sig
val clear_entry : 'a Entry.e -> unit
@@ -906,7 +810,6 @@ module GMake (L : GLexerType) =
let (ts, lf) = L.lexer.Plexing.tok_func cs in
{pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
let tokens = tokens gram
- let glexer = glexer gram
module Entry =
struct
type 'a e = te g_entry
@@ -946,7 +849,7 @@ module GMake (L : GLexerType) =
let r_stop = []
let r_next r s = r @ [s]
let production
- (p : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f) : 'a ty_production =
+ (p : ('a, 'f, Loc.t -> 'a) ty_rule * 'f) : 'a ty_production =
Obj.magic p
module Unsafe =
struct
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 0c585a7c0d..bde07ddc48 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -25,7 +25,6 @@ module type S =
type parsable
val parsable : char Stream.t -> parsable
val tokens : string -> (string * int) list
- val glexer : te Plexing.lexer
module Entry :
sig
type 'a e
@@ -58,7 +57,7 @@ module type S =
val r_next :
('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
('self, 'b -> 'a, 'r) ty_rule
- val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
+ val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
module Unsafe :
sig
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 986363ec1f..f99a3c2480 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -6,14 +6,13 @@ type pattern = string * string
exception Error of string
-type location = Ploc.t
-type location_function = int -> location
+type location_function = int -> Loc.t
type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
type 'te lexer =
{ tok_func : 'te lexer_func;
tok_using : pattern -> unit;
tok_removing : pattern -> unit;
- mutable tok_match : pattern -> 'te -> string;
+ tok_match : pattern -> 'te -> string;
tok_text : pattern -> string;
- mutable tok_comm : location list option }
+ }
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 96b432a8ad..eed4082e00 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -28,10 +28,10 @@ type 'te lexer =
{ tok_func : 'te lexer_func;
tok_using : pattern -> unit;
tok_removing : pattern -> unit;
- mutable tok_match : pattern -> 'te -> string;
+ tok_match : pattern -> 'te -> string;
tok_text : pattern -> string;
- mutable tok_comm : Ploc.t list option }
+ }
and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
-and location_function = int -> Ploc.t
+and location_function = int -> Loc.t
(** The type of a function giving the location of a token in the
source from the token number in the stream (starting from zero). *)
diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index 082686db01..9342fc6c1d 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -2,60 +2,23 @@
(* ploc.ml,v *)
(* Copyright (c) INRIA 2007-2017 *)
-type t =
- { fname : string;
- line_nb : int;
- bol_pos : int;
- line_nb_last : int;
- bol_pos_last : int;
- bp : int;
- ep : int;
- comm : string;
- ecomm : string }
-
-let make_loc fname line_nb bol_pos (bp, ep) comm =
- {fname = fname; line_nb = line_nb; bol_pos = bol_pos;
- line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep;
- comm = comm; ecomm = ""}
+open Loc
let make_unlined (bp, ep) =
- {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+ {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
bp = bp; ep = ep; comm = ""; ecomm = ""}
let dummy =
- {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+ {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
bp = 0; ep = 0; comm = ""; ecomm = ""}
-let file_name loc = loc.fname
-let first_pos loc = loc.bp
-let last_pos loc = loc.ep
-let line_nb loc = loc.line_nb
-let bol_pos loc = loc.bol_pos
-let line_nb_last loc = loc.line_nb_last
-let bol_pos_last loc = loc.bol_pos_last
-let comment loc = loc.comm
-let comment_last loc = loc.ecomm
-
(* *)
-let encl loc1 loc2 =
- if loc1.bp < loc2.bp then
- if loc1.ep < loc2.ep then
- {fname = loc1.fname; line_nb = loc1.line_nb; bol_pos = loc1.bol_pos;
- line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last;
- bp = loc1.bp; ep = loc2.ep; comm = loc1.comm; ecomm = loc2.comm}
- else loc1
- else if loc2.ep < loc1.ep then
- {fname = loc2.fname; line_nb = loc2.line_nb; bol_pos = loc2.bol_pos;
- line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last;
- bp = loc2.bp; ep = loc1.ep; comm = loc2.comm; ecomm = loc1.comm}
- else loc2
-let shift sh loc = {loc with bp = sh + loc.bp; ep = sh + loc.ep}
let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}
let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}
let with_comment loc comm = {loc with comm = comm}
-exception Exc of t * exn
+exception Exc of Loc.t * exn
let raise loc exc =
match exc with
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 2ce6382183..100fbc7271 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -2,85 +2,39 @@
(* ploc.mli,v *)
(* Copyright (c) INRIA 2007-2017 *)
-(** Locations and some pervasive type and value. *)
-
-type t
-
(* located exceptions *)
-exception Exc of t * exn
+exception Exc of Loc.t * exn
(** [Ploc.Exc loc e] is an encapsulation of the exception [e] with
the input location [loc]. To be used to specify a location
for an error. This exception must not be raised by [raise] but
rather by [Ploc.raise] (see below), to prevent the risk of several
encapsulations of [Ploc.Exc]. *)
-val raise : t -> exn -> 'a
+
+val raise : Loc.t -> exn -> 'a
(** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc],
re-raise it (ignoring the new location [loc]), else raise the
exception [Ploc.Exc loc e]. *)
-(* making locations *)
-
-val make_loc : string -> int -> int -> int * int -> string -> t
- (** [Ploc.make_loc fname line_nb bol_pos (bp, ep) comm] creates a location
- starting at line number [line_nb], where the position of the beginning
- of the line is [bol_pos] and between the positions [bp] (included) and
- [ep] excluded. And [comm] is the comment before the location. The
- positions are in number of characters since the begin of the stream. *)
-val make_unlined : int * int -> t
+val make_unlined : int * int -> Loc.t
(** [Ploc.make_unlined] is like [Ploc.make] except that the line number
is not provided (to be used e.g. when the line number is unknown. *)
-val dummy : t
+val dummy : Loc.t
(** [Ploc.dummy] is a dummy location, used in situations when location
has no meaning. *)
-(* getting location info *)
-
-val file_name : t -> string
- (** [Ploc.file_name loc] returns the file name of the location. *)
-val first_pos : t -> int
- (** [Ploc.first_pos loc] returns the position of the begin of the location
- in number of characters since the beginning of the stream. *)
-val last_pos : t -> int
- (** [Ploc.last_pos loc] returns the position of the first character not
- in the location in number of characters since the beginning of the
- stream. *)
-val line_nb : t -> int
- (** [Ploc.line_nb loc] returns the line number of the location or [-1] if
- the location does not contain a line number (i.e. built with
- [Ploc.make_unlined]. *)
-val bol_pos : t -> int
- (** [Ploc.bol_pos loc] returns the position of the beginning of the line
- of the location in number of characters since the beginning of
- the stream, or [0] if the location does not contain a line number
- (i.e. built with [Ploc.make_unlined]. *)
-val line_nb_last : t -> int
-val bol_pos_last : t -> int
- (** Return the line number and the position of the beginning of the line
- of the last position. *)
-val comment : t -> string
- (** [Ploc.comment loc] returns the comment before the location. *)
-val comment_last : t -> string
- (** [Ploc.comment loc] returns the last comment of the location. *)
-
(* combining locations *)
-val encl : t -> t -> t
- (** [Ploc.encl loc1 loc2] returns the location starting at the
- smallest start of [loc1] and [loc2] and ending at the greatest end
- of them. In other words, it is the location enclosing [loc1] and
- [loc2]. *)
-val shift : int -> t -> t
- (** [Ploc.shift sh loc] returns the location [loc] shifted with [sh]
- characters. The line number is not recomputed. *)
-val sub : t -> int -> int -> t
+val sub : Loc.t -> int -> int -> Loc.t
(** [Ploc.sub loc sh len] is the location [loc] shifted with [sh]
characters and with length [len]. The previous ending position
of the location is lost. *)
-val after : t -> int -> int -> t
+
+val after : Loc.t -> int -> int -> Loc.t
(** [Ploc.after loc sh len] is the location just after loc (starting at
the end position of [loc]) shifted with [sh] characters and of length
[len]. *)
-val with_comment : t -> string -> t
+
+val with_comment : Loc.t -> string -> Loc.t
(** Change the comment part of the given location *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:03:17 +0000