aboutsummaryrefslogtreecommitdiff
path: root/gramlib
diff options
context:
space:
mode:
Diffstat (limited to 'gramlib')
-rw-r--r--gramlib/dune3
-rw-r--r--gramlib/gramext.ml140
-rw-r--r--gramlib/gramext.mli11
-rw-r--r--gramlib/gramlib.mllib4
-rw-r--r--gramlib/grammar.ml156
-rw-r--r--gramlib/grammar.mli17
-rw-r--r--gramlib/plexing.ml7
-rw-r--r--gramlib/plexing.mli6
-rw-r--r--gramlib/ploc.ml45
-rw-r--r--gramlib/ploc.mli66
10 files changed, 87 insertions, 368 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 72468b540e..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,11 +52,8 @@ type position =
| Last
| Before of string
| After of string
- | Like of string
| Level of string
-let warning_verbose = ref true
-
let rec derive_eps =
function
Slist0 _ -> true
@@ -96,7 +93,7 @@ let is_before s1 s2 =
| Stoken _, _ -> true
| _ -> false
-let insert_tree entry_name gsymbols action tree =
+let insert_tree ~warning entry_name gsymbols action tree =
let rec insert symbols tree =
match symbols with
s :: sl -> insert_in_tree s sl tree
@@ -105,14 +102,16 @@ let insert_tree entry_name gsymbols action tree =
Node {node = s; son = son; brother = bro} ->
Node {node = s; son = son; brother = insert [] bro}
| LocAct (old_action, action_list) ->
- if !warning_verbose then
- begin
- eprintf "<W> Grammar extension: ";
- if entry_name <> "" then eprintf "in [%s], " entry_name;
- eprintf "some rule has been masked\n";
- flush stderr
- end;
- LocAct (action, old_action :: action_list)
+ begin match warning with
+ | None -> ()
+ | Some warn_fn ->
+ let msg =
+ "<W> Grammar extension: " ^
+ (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^
+ "some rule has been masked" in
+ warn_fn msg
+ end;
+ LocAct (action, old_action :: action_list)
| DeadEnd -> LocAct (action, [])
and insert_in_tree s sl tree =
match try_insert s sl tree with
@@ -141,51 +140,28 @@ let insert_tree entry_name gsymbols action tree =
in
insert gsymbols tree
-let srules rl =
+let srules ~warning rl =
let t =
List.fold_left
- (fun tree (symbols, action) -> insert_tree "" symbols action tree)
+ (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree)
DeadEnd rl
in
Stree t
-external action : 'a -> g_action = "%identity"
-
let is_level_labelled n lev =
match lev.lname with
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 entry_name e1 symbols action slev =
+let insert_level ~warning entry_name e1 symbols action slev =
match e1 with
true ->
{assoc = slev.assoc; lname = slev.lname;
- lsuffix = insert_tree entry_name symbols action slev.lsuffix;
+ lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix;
lprefix = slev.lprefix}
| false ->
{assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix;
- lprefix = insert_tree entry_name symbols action slev.lprefix}
+ lprefix = insert_tree ~warning entry_name symbols action slev.lprefix}
let empty_lev lname assoc =
let assoc =
@@ -195,27 +171,33 @@ let empty_lev lname assoc =
in
{assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd}
-let change_lev lev n lname assoc =
+let change_lev ~warning lev n lname assoc =
let a =
match assoc with
None -> lev.assoc
| Some a ->
- if a <> lev.assoc && !warning_verbose then
- begin
- eprintf "<W> Changing associativity of level \"%s\"\n" n;
- flush stderr
- end;
+ if a <> lev.assoc then
+ begin
+ match warning with
+ | None -> ()
+ | Some warn_fn ->
+ warn_fn ("<W> Changing associativity of level \""^n^"\"")
+ end;
a
in
begin match lname with
Some n ->
- if lname <> lev.lname && !warning_verbose then
- begin eprintf "<W> Level label \"%s\" ignored\n" n; flush stderr end
+ if lname <> lev.lname then
+ begin match warning with
+ | None -> ()
+ | Some warn_fn ->
+ warn_fn ("<W> Level label \""^n^"\" ignored")
+ end;
| None -> ()
end;
{assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
-let get_level entry position levs =
+let get_level ~warning entry position levs =
match position with
Some First -> [], empty_lev, levs
| Some Last -> levs, empty_lev, []
@@ -228,7 +210,7 @@ let get_level entry position levs =
flush stderr;
failwith "Grammar.extend"
| lev :: levs ->
- if is_level_labelled n lev then [], change_lev lev n, levs
+ if is_level_labelled n lev then [], change_lev ~warning lev n, levs
else
let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
in
@@ -261,58 +243,11 @@ let get_level 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 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 lev "<top>", levs
+ 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
@@ -349,7 +284,7 @@ let insert_tokens gram symbols =
in
List.iter insert symbols
-let levels_of_rules entry position rules =
+let levels_of_rules ~warning entry position rules =
let elev =
match entry.edesc with
Dlevels elev -> elev
@@ -360,7 +295,7 @@ let levels_of_rules entry position rules =
in
if rules = [] then elev
else
- let (levs1, make_lev, levs2) = get_level entry position elev in
+ let (levs1, make_lev, levs2) = get_level ~warning entry position elev in
let (levs, _) =
List.fold_left
(fun (levs, make_lev) (lname, assoc, level) ->
@@ -369,10 +304,9 @@ let levels_of_rules 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 entry.ename e1 symbols action lev)
+ insert_level ~warning entry.ename e1 symbols action lev)
lev level
in
lev :: levs, empty_lev)
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index e888508277..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,19 +50,16 @@ type position =
| Last
| Before of string
| After of string
- | Like of string
| Level of string
-val levels_of_rules :
+val levels_of_rules : warning:(string -> unit) option ->
'te g_entry -> position option ->
(string option * g_assoc option * ('te g_symbol list * g_action) list)
list ->
'te g_level list
-val srules : ('te g_symbol list * g_action) list -> 'te g_symbol
-external action : 'a -> g_action = "%identity"
+
+val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol
val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool
val delete_rule_in_level_list :
'te g_entry -> 'te g_symbol list -> 'te g_level list -> 'te g_level list
-
-val warning_verbose : bool ref
diff --git a/gramlib/gramlib.mllib b/gramlib/gramlib.mllib
new file mode 100644
index 0000000000..4c915b2b05
--- /dev/null
+++ b/gramlib/gramlib.mllib
@@ -0,0 +1,4 @@
+Ploc
+Plexing
+Gramext
+Grammar
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 760410894a..0ad11d075f 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -5,6 +5,8 @@
open Gramext
open Format
+external gramext_action : 'a -> g_action = "%identity"
+
let rec flatten_tree =
function
DeadEnd -> []
@@ -128,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
@@ -184,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 =
@@ -293,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 =
@@ -350,7 +262,7 @@ let top_tree entry =
| LocAct (_, _) | DeadEnd -> raise Stream.Failure
let skip_if_empty bp p strm =
- if Stream.count strm == bp then Gramext.action (fun a -> p strm)
+ if Stream.count strm == bp then gramext_action (fun a -> p strm)
else raise Stream.Failure
let continue entry bp a s son p1 (strm__ : _ Stream.t) =
@@ -359,7 +271,7 @@ let continue entry bp a s son p1 (strm__ : _ Stream.t) =
try p1 strm__ with
Stream.Failure -> raise (Stream.Error (tree_failed entry a s son))
in
- Gramext.action (fun _ -> app act a)
+ gramext_action (fun _ -> app act a)
let do_recover parser_of_tree entry nlevn alevn bp a s son
(strm__ : _ Stream.t) =
@@ -372,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
@@ -753,9 +662,9 @@ let init_entry_functions entry =
let f = continue_parser_of_entry entry in
entry.econtinue <- f; f lev bp a strm)
-let extend_entry entry position rules =
+let extend_entry ~warning entry position rules =
try
- let elev = Gramext.levels_of_rules entry position rules in
+ let elev = Gramext.levels_of_rules ~warning entry position rules in
entry.edesc <- Dlevels elev; init_entry_functions entry
with Plexing.Error s ->
Printf.eprintf "Lexer initialization error:\n- %s\n" s;
@@ -792,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;
@@ -814,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;
@@ -839,8 +746,6 @@ let clear_entry e =
Dlevels _ -> e.edesc <- Dlevels []
| Dparser _ -> ()
-let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer
-
(* Functorial interface *)
module type GLexerType = sig type te val lexer : te Plexing.lexer end
@@ -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
@@ -861,8 +765,6 @@ module type S =
val of_parser : string -> (te Stream.t -> 'a) -> 'a e
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
- external obj : 'a e -> te Gramext.g_entry = "%identity"
- val parse_token : 'a e -> te Stream.t -> 'a
end
type ('self, 'a) ty_symbol
type ('self, 'f, 'r) ty_rule
@@ -881,29 +783,21 @@ module type S =
val s_self : ('self, 'self) ty_symbol
val s_next : ('self, 'self) ty_symbol
val s_token : Plexing.pattern -> ('self, string) ty_symbol
- val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
+ val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
val r_stop : ('self, 'r, 'r) ty_rule
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 gram_reinit : te Plexing.lexer -> unit
val clear_entry : 'a Entry.e -> unit
end
- val extend :
- 'a Entry.e -> Gramext.position option ->
- (string option * Gramext.g_assoc option *
- (te Gramext.g_symbol list * Gramext.g_action) list)
- list ->
- unit
- val safe_extend :
+ val safe_extend : warning:(string -> unit) option ->
'a Entry.e -> Gramext.position option ->
(string option * Gramext.g_assoc option * 'a ty_production list)
list ->
unit
- val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit
val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit
end
@@ -916,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
@@ -930,18 +823,6 @@ module GMake (L : GLexerType) =
Obj.magic (parse_parsable e p : Obj.t)
let parse_token_stream (e : 'a e) ts : 'a =
Obj.magic (e.estart 0 ts : Obj.t)
- let _warned_using_parse_token = ref false
- let parse_token (entry : 'a e) ts : 'a =
- (* commented: too often warned in Coq...
- if not warned_using_parse_token.val then do {
- eprintf "<W> use of Entry.parse_token ";
- eprintf "deprecated since 2017-06-16\n%!";
- eprintf "use Entry.parse_token_stream instead\n%! ";
- warned_using_parse_token.val := True
- }
- else ();
- *)
- parse_token_stream entry ts
let name e = e.ename
let of_parser n (p : te Stream.t -> 'a) : 'a e =
{egram = gram; ename = n; elocal = false;
@@ -964,23 +845,20 @@ module GMake (L : GLexerType) =
let s_self = Sself
let s_next = Snext
let s_token tok = Stoken tok
- let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t)
+ let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t)
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
- let gram_reinit = gram_reinit gram
let clear_entry = clear_entry
end
- let extend = extend_entry
- let safe_extend e pos
+ let safe_extend ~warning e pos
(r :
(string option * Gramext.g_assoc option * Obj.t ty_production list)
list) =
- extend e pos (Obj.magic r)
- let delete_rule e r = delete_rule (Entry.obj e) r
- let safe_delete_rule = delete_rule
+ extend_entry ~warning e pos (Obj.magic r)
+ let safe_delete_rule e r = delete_rule (Entry.obj e) r
end
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 244ab710dc..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
@@ -35,8 +34,6 @@ module type S =
val of_parser : string -> (te Stream.t -> 'a) -> 'a e
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
- external obj : 'a e -> te Gramext.g_entry = "%identity"
- val parse_token : 'a e -> te Stream.t -> 'a
end
type ('self, 'a) ty_symbol
type ('self, 'f, 'r) ty_rule
@@ -55,30 +52,22 @@ module type S =
val s_self : ('self, 'self) ty_symbol
val s_next : ('self, 'self) ty_symbol
val s_token : Plexing.pattern -> ('self, string) ty_symbol
- val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
+ val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
val r_stop : ('self, 'r, 'r) ty_rule
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 gram_reinit : te Plexing.lexer -> unit
val clear_entry : 'a Entry.e -> unit
end
- val extend :
- 'a Entry.e -> Gramext.position option ->
- (string option * Gramext.g_assoc option *
- (te Gramext.g_symbol list * Gramext.g_action) list)
- list ->
- unit
- val safe_extend :
+ val safe_extend : warning:(string -> unit) option ->
'a Entry.e -> Gramext.position option ->
(string option * Gramext.g_assoc option * 'a ty_production list)
list ->
unit
- val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit
val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit
end
(** Signature type of the functor [Grammar.GMake]. The types and
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-04-28 17:37:53 +0000