From ccfa2585dbe9a482040f2b2d405fdb4451d19e39 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 17:10:43 +0100 Subject: Move most of Gramext into Grammar. This module was defining unsafe functions and datatypes only relevant to the grammar engine. We hide them under the API so as to be able to later clean it up. --- gramlib/gramext.ml | 451 +-------------------------------------------------- gramlib/gramext.mli | 55 +------ gramlib/grammar.ml | 457 +++++++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 454 insertions(+), 509 deletions(-) diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 46c2688f05..c396bbab34 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -2,51 +2,6 @@ (* gramext.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -open Printf - -type 'a parser_t = 'a Stream.t -> Obj.t - -type 'te grammar = - { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - glexer : 'te Plexing.lexer } - -type 'te g_entry = - { egram : 'te grammar; - ename : string; - elocal : bool; - mutable estart : int -> 'te parser_t; - mutable econtinue : int -> int -> Obj.t -> 'te parser_t; - mutable edesc : 'te g_desc } -and 'te g_desc = - Dlevels of 'te g_level list - | Dparser of 'te parser_t -and 'te g_level = - { assoc : g_assoc; - lname : string option; - lsuffix : 'te g_tree; - lprefix : 'te g_tree } -and g_assoc = NonA | RightA | LeftA -and 'te g_symbol = - | Snterm of 'te g_entry - | Snterml of 'te g_entry * string - | Slist0 of 'te g_symbol - | Slist0sep of 'te g_symbol * 'te g_symbol * bool - | Slist1 of 'te g_symbol - | Slist1sep of 'te g_symbol * 'te g_symbol * bool - | Sopt of 'te g_symbol - | Sself - | Snext - | Stoken of Plexing.pattern - | Stree of 'te g_tree -and g_action = Obj.t -and 'te g_tree = - Node of 'te g_node - | LocAct of g_action * g_action list - | DeadEnd -and 'te g_node = - { node : 'te g_symbol; son : 'te g_tree; brother : 'te g_tree } -and err_fun = unit -> string - type position = First | Last @@ -54,408 +9,4 @@ type position = | After of string | Level of string -let rec derive_eps = - function - Slist0 _ -> true - | Slist0sep (_, _, _) -> true - | Sopt _ -> true - | Stree t -> tree_derive_eps t - | Slist1 _ | Slist1sep (_, _, _) | Snterm _ | - Snterml (_, _) | Snext | Sself | Stoken _ -> - false -and tree_derive_eps = - function - LocAct (_, _) -> true - | Node {node = s; brother = bro; son = son} -> - derive_eps s && tree_derive_eps son || tree_derive_eps bro - | DeadEnd -> false - -let rec eq_symbol s1 s2 = - match s1, s2 with - Snterm e1, Snterm e2 -> e1 == e2 - | Snterml (e1, l1), Snterml (e2, l2) -> e1 == e2 && l1 = l2 - | Slist0 s1, Slist0 s2 -> eq_symbol s1 s2 - | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> - eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 - | Slist1 s1, Slist1 s2 -> eq_symbol s1 s2 - | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> - eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 - | Sopt s1, Sopt s2 -> eq_symbol s1 s2 - | Stree _, Stree _ -> false - | _ -> s1 = s2 - -let is_before s1 s2 = - match s1, s2 with - Stoken ("ANY", _), _ -> false - | _, Stoken ("ANY", _) -> true - | Stoken (_, s), Stoken (_, "") when s <> "" -> true - | Stoken _, Stoken _ -> false - | Stoken _, _ -> true - | _ -> false - -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 - | [] -> - match tree with - Node {node = s; son = son; brother = bro} -> - Node {node = s; son = son; brother = insert [] bro} - | LocAct (old_action, action_list) -> - begin match warning with - | None -> () - | Some warn_fn -> - let msg = - " 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 - Some t -> t - | None -> Node {node = s; son = insert sl DeadEnd; brother = tree} - and try_insert s sl tree = - match tree with - Node {node = s1; son = son; brother = bro} -> - if eq_symbol s s1 then - let t = Node {node = s1; son = insert sl son; brother = bro} in - Some t - else if is_before s1 s || derive_eps s && not (derive_eps s1) then - let bro = - match try_insert s sl bro with - Some bro -> bro - | None -> Node {node = s; son = insert sl DeadEnd; brother = bro} - in - let t = Node {node = s1; son = son; brother = bro} in Some t - else - begin match try_insert s sl bro with - Some bro -> - let t = Node {node = s1; son = son; brother = bro} in Some t - | None -> None - end - | LocAct (_, _) | DeadEnd -> None - in - insert gsymbols tree - -let srules ~warning rl = - let t = - List.fold_left - (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) - DeadEnd rl - in - Stree t - -let is_level_labelled n lev = - match lev.lname with - Some n1 -> n = n1 - | None -> false - -let insert_level ~warning entry_name e1 symbols action slev = - match e1 with - true -> - {assoc = slev.assoc; lname = slev.lname; - 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 ~warning entry_name symbols action slev.lprefix} - -let empty_lev lname assoc = - let assoc = - match assoc with - Some a -> a - | None -> LeftA - in - {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} - -let change_lev ~warning lev n lname assoc = - let a = - match assoc with - None -> lev.assoc - | Some a -> - if a <> lev.assoc then - begin - match warning with - | None -> () - | Some warn_fn -> - warn_fn (" Changing associativity of level \""^n^"\"") - end; - a - in - begin match lname with - Some n -> - if lname <> lev.lname then - begin match warning with - | None -> () - | Some warn_fn -> - warn_fn (" Level label \""^n^"\" ignored") - end; - | None -> () - end; - {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} - -let get_level ~warning entry position levs = - match position with - Some First -> [], empty_lev, levs - | Some Last -> levs, empty_lev, [] - | Some (Level n) -> - let rec get = - function - [] -> - eprintf "No level labelled \"%s\" in entry \"%s\"\n" n - entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: 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 - get levs - | Some (Before n) -> - let rec get = - function - [] -> - eprintf "No level labelled \"%s\" in entry \"%s\"\n" n - entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: levs -> - if is_level_labelled n lev then [], empty_lev, lev :: levs - else - let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 - in - get levs - | Some (After n) -> - let rec get = - function - [] -> - eprintf "No level labelled \"%s\" in entry \"%s\"\n" n - entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: levs -> - if is_level_labelled n lev then [lev], empty_lev, 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 "", levs - | [] -> [], empty_lev, [] - -let change_to_self entry = - function - Snterm e when e == entry -> Sself - | x -> x - -let get_initial entry = - function - Sself :: symbols -> true, symbols - | symbols -> false, symbols - -let insert_tokens gram symbols = - let rec insert = - function - | Slist0 s -> insert s - | Slist1 s -> insert s - | Slist0sep (s, t, _) -> insert s; insert t - | Slist1sep (s, t, _) -> insert s; insert t - | Sopt s -> insert s - | Stree t -> tinsert t - | Stoken ("ANY", _) -> () - | Stoken tok -> - gram.glexer.Plexing.tok_using tok; - let r = - try Hashtbl.find gram.gtokens tok with - Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r - in - incr r - | Snterm _ | Snterml (_, _) | Snext | Sself -> () - and tinsert = - function - Node {node = s; brother = bro; son = son} -> - insert s; tinsert bro; tinsert son - | LocAct (_, _) | DeadEnd -> () - in - List.iter insert symbols - -let levels_of_rules ~warning entry position rules = - let elev = - match entry.edesc with - Dlevels elev -> elev - | Dparser _ -> - eprintf "Error: entry not extensible: \"%s\"\n" entry.ename; - flush stderr; - failwith "Grammar.extend" - in - if rules = [] then elev - else - let (levs1, make_lev, levs2) = get_level ~warning entry position elev in - let (levs, _) = - List.fold_left - (fun (levs, make_lev) (lname, assoc, level) -> - let lev = make_lev lname assoc in - let lev = - List.fold_left - (fun lev (symbols, action) -> - let symbols = List.map (change_to_self entry) symbols in - let (e1, symbols) = get_initial entry symbols in - insert_tokens entry.egram symbols; - insert_level ~warning entry.ename e1 symbols action lev) - lev level - in - lev :: levs, empty_lev) - ([], make_lev) rules - in - levs1 @ List.rev levs @ levs2 - -let logically_eq_symbols entry = - let rec eq_symbols s1 s2 = - match s1, s2 with - Snterm e1, Snterm e2 -> e1.ename = e2.ename - | Snterm e1, Sself -> e1.ename = entry.ename - | Sself, Snterm e2 -> entry.ename = e2.ename - | Snterml (e1, l1), Snterml (e2, l2) -> e1.ename = e2.ename && l1 = l2 - | Slist0 s1, Slist0 s2 -> eq_symbols s1 s2 - | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> - eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 - | Slist1 s1, Slist1 s2 -> eq_symbols s1 s2 - | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> - eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 - | Sopt s1, Sopt s2 -> eq_symbols s1 s2 - | Stree t1, Stree t2 -> eq_trees t1 t2 - | _ -> s1 = s2 - and eq_trees t1 t2 = - match t1, t2 with - Node n1, Node n2 -> - eq_symbols n1.node n2.node && eq_trees n1.son n2.son && - eq_trees n1.brother n2.brother - | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true - | _ -> false - in - eq_symbols - -(* [delete_rule_in_tree] returns - [Some (dsl, t)] if success - [dsl] = - Some (list of deleted nodes) if branch deleted - None if action replaced by previous version of action - [t] = remaining tree - [None] if failure *) - -let delete_rule_in_tree entry = - let rec delete_in_tree symbols tree = - match symbols, tree with - s :: sl, Node n -> - if logically_eq_symbols entry s n.node then delete_son sl n - else - begin match delete_in_tree symbols n.brother with - Some (dsl, t) -> - Some (dsl, Node {node = n.node; son = n.son; brother = t}) - | None -> None - end - | s :: sl, _ -> None - | [], Node n -> - begin match delete_in_tree [] n.brother with - Some (dsl, t) -> - Some (dsl, Node {node = n.node; son = n.son; brother = t}) - | None -> None - end - | [], DeadEnd -> None - | [], LocAct (_, []) -> Some (Some [], DeadEnd) - | [], LocAct (_, action :: list) -> Some (None, LocAct (action, list)) - and delete_son sl n = - match delete_in_tree sl n.son with - Some (Some dsl, DeadEnd) -> Some (Some (n.node :: dsl), n.brother) - | Some (Some dsl, t) -> - let t = Node {node = n.node; son = t; brother = n.brother} in - Some (Some (n.node :: dsl), t) - | Some (None, t) -> - let t = Node {node = n.node; son = t; brother = n.brother} in - Some (None, t) - | None -> None - in - delete_in_tree - -let rec decr_keyw_use gram = - function - Stoken tok -> - let r = Hashtbl.find gram.gtokens tok in - decr r; - if !r == 0 then - begin - Hashtbl.remove gram.gtokens tok; - gram.glexer.Plexing.tok_removing tok - end - | Slist0 s -> decr_keyw_use gram s - | Slist1 s -> decr_keyw_use gram s - | Slist0sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 - | Slist1sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 - | Sopt s -> decr_keyw_use gram s - | Stree t -> decr_keyw_use_in_tree gram t - | Sself | Snext | Snterm _ | Snterml (_, _) -> () -and decr_keyw_use_in_tree gram = - function - DeadEnd | LocAct (_, _) -> () - | Node n -> - decr_keyw_use gram n.node; - decr_keyw_use_in_tree gram n.son; - decr_keyw_use_in_tree gram n.brother - -let rec delete_rule_in_suffix entry symbols = - function - lev :: levs -> - begin match delete_rule_in_tree entry symbols lev.lsuffix with - Some (dsl, t) -> - begin match dsl with - Some dsl -> List.iter (decr_keyw_use entry.egram) dsl - | None -> () - end; - begin match t with - DeadEnd when lev.lprefix == DeadEnd -> levs - | _ -> - let lev = - {assoc = lev.assoc; lname = lev.lname; lsuffix = t; - lprefix = lev.lprefix} - in - lev :: levs - end - | None -> - let levs = delete_rule_in_suffix entry symbols levs in lev :: levs - end - | [] -> raise Not_found - -let rec delete_rule_in_prefix entry symbols = - function - lev :: levs -> - begin match delete_rule_in_tree entry symbols lev.lprefix with - Some (dsl, t) -> - begin match dsl with - Some dsl -> List.iter (decr_keyw_use entry.egram) dsl - | None -> () - end; - begin match t with - DeadEnd when lev.lsuffix == DeadEnd -> levs - | _ -> - let lev = - {assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix; - lprefix = t} - in - lev :: levs - end - | None -> - let levs = delete_rule_in_prefix entry symbols levs in lev :: levs - end - | [] -> raise Not_found - -let delete_rule_in_level_list entry symbols levs = - match symbols with - Sself :: symbols -> delete_rule_in_suffix entry symbols levs - | Snterm e :: symbols when e == entry -> - delete_rule_in_suffix entry symbols levs - | _ -> delete_rule_in_prefix entry symbols levs +type g_assoc = NonA | RightA | LeftA diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index f1e294fb4c..f9daf5bf10 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -2,49 +2,6 @@ (* gramext.mli,v *) (* Copyright (c) INRIA 2007-2017 *) -type 'a parser_t = 'a Stream.t -> Obj.t - -type 'te grammar = - { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - glexer : 'te Plexing.lexer } - -type 'te g_entry = - { egram : 'te grammar; - ename : string; - elocal : bool; - mutable estart : int -> 'te parser_t; - mutable econtinue : int -> int -> Obj.t -> 'te parser_t; - mutable edesc : 'te g_desc } -and 'te g_desc = - Dlevels of 'te g_level list - | Dparser of 'te parser_t -and 'te g_level = - { assoc : g_assoc; - lname : string option; - lsuffix : 'te g_tree; - lprefix : 'te g_tree } -and g_assoc = NonA | RightA | LeftA -and 'te g_symbol = - | Snterm of 'te g_entry - | Snterml of 'te g_entry * string - | Slist0 of 'te g_symbol - | Slist0sep of 'te g_symbol * 'te g_symbol * bool - | Slist1 of 'te g_symbol - | Slist1sep of 'te g_symbol * 'te g_symbol * bool - | Sopt of 'te g_symbol - | Sself - | Snext - | Stoken of Plexing.pattern - | Stree of 'te g_tree -and g_action = Obj.t -and 'te g_tree = - Node of 'te g_node - | LocAct of g_action * g_action list - | DeadEnd -and 'te g_node = - { node : 'te g_symbol; son : 'te g_tree; brother : 'te g_tree } -and err_fun = unit -> string - type position = First | Last @@ -52,14 +9,4 @@ type position = | After of string | Level of string -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 : 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 +type g_assoc = NonA | RightA | LeftA diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index e959e9b9e6..1562a275db 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -5,6 +5,453 @@ open Gramext open Format +type 'a parser_t = 'a Stream.t -> Obj.t + +type 'te grammar = + { gtokens : (Plexing.pattern, int ref) Hashtbl.t; + glexer : 'te Plexing.lexer } + +type 'te g_entry = + { egram : 'te grammar; + ename : string; + elocal : bool; + mutable estart : int -> 'te parser_t; + mutable econtinue : int -> int -> Obj.t -> 'te parser_t; + mutable edesc : 'te g_desc } +and 'te g_desc = + Dlevels of 'te g_level list + | Dparser of 'te parser_t +and 'te g_level = + { assoc : g_assoc; + lname : string option; + lsuffix : 'te g_tree; + lprefix : 'te g_tree } +and 'te g_symbol = + | Snterm of 'te g_entry + | Snterml of 'te g_entry * string + | Slist0 of 'te g_symbol + | Slist0sep of 'te g_symbol * 'te g_symbol * bool + | Slist1 of 'te g_symbol + | Slist1sep of 'te g_symbol * 'te g_symbol * bool + | Sopt of 'te g_symbol + | Sself + | Snext + | Stoken of Plexing.pattern + | Stree of 'te g_tree +and g_action = Obj.t +and 'te g_tree = + Node of 'te g_node + | LocAct of g_action * g_action list + | DeadEnd +and 'te g_node = + { node : 'te g_symbol; son : 'te g_tree; brother : 'te g_tree } + +let rec derive_eps = + function + Slist0 _ -> true + | Slist0sep (_, _, _) -> true + | Sopt _ -> true + | Stree t -> tree_derive_eps t + | Slist1 _ | Slist1sep (_, _, _) | Snterm _ | + Snterml (_, _) | Snext | Sself | Stoken _ -> + false +and tree_derive_eps = + function + LocAct (_, _) -> true + | Node {node = s; brother = bro; son = son} -> + derive_eps s && tree_derive_eps son || tree_derive_eps bro + | DeadEnd -> false + +let rec eq_symbol s1 s2 = + match s1, s2 with + Snterm e1, Snterm e2 -> e1 == e2 + | Snterml (e1, l1), Snterml (e2, l2) -> e1 == e2 && l1 = l2 + | Slist0 s1, Slist0 s2 -> eq_symbol s1 s2 + | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> + eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 + | Slist1 s1, Slist1 s2 -> eq_symbol s1 s2 + | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> + eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 + | Sopt s1, Sopt s2 -> eq_symbol s1 s2 + | Stree _, Stree _ -> false + | _ -> s1 = s2 + +let is_before s1 s2 = + match s1, s2 with + Stoken ("ANY", _), _ -> false + | _, Stoken ("ANY", _) -> true + | Stoken (_, s), Stoken (_, "") when s <> "" -> true + | Stoken _, Stoken _ -> false + | Stoken _, _ -> true + | _ -> false + +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 + | [] -> + match tree with + Node {node = s; son = son; brother = bro} -> + Node {node = s; son = son; brother = insert [] bro} + | LocAct (old_action, action_list) -> + begin match warning with + | None -> () + | Some warn_fn -> + let msg = + " 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 + Some t -> t + | None -> Node {node = s; son = insert sl DeadEnd; brother = tree} + and try_insert s sl tree = + match tree with + Node {node = s1; son = son; brother = bro} -> + if eq_symbol s s1 then + let t = Node {node = s1; son = insert sl son; brother = bro} in + Some t + else if is_before s1 s || derive_eps s && not (derive_eps s1) then + let bro = + match try_insert s sl bro with + Some bro -> bro + | None -> Node {node = s; son = insert sl DeadEnd; brother = bro} + in + let t = Node {node = s1; son = son; brother = bro} in Some t + else + begin match try_insert s sl bro with + Some bro -> + let t = Node {node = s1; son = son; brother = bro} in Some t + | None -> None + end + | LocAct (_, _) | DeadEnd -> None + in + insert gsymbols tree + +let srules ~warning rl = + let t = + List.fold_left + (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) + DeadEnd rl + in + Stree t + +let is_level_labelled n lev = + match lev.lname with + Some n1 -> n = n1 + | None -> false + +let insert_level ~warning entry_name e1 symbols action slev = + match e1 with + true -> + {assoc = slev.assoc; lname = slev.lname; + 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 ~warning entry_name symbols action slev.lprefix} + +let empty_lev lname assoc = + let assoc = + match assoc with + Some a -> a + | None -> LeftA + in + {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} + +let change_lev ~warning lev n lname assoc = + let a = + match assoc with + None -> lev.assoc + | Some a -> + if a <> lev.assoc then + begin + match warning with + | None -> () + | Some warn_fn -> + warn_fn (" Changing associativity of level \""^n^"\"") + end; + a + in + begin match lname with + Some n -> + if lname <> lev.lname then + begin match warning with + | None -> () + | Some warn_fn -> + warn_fn (" Level label \""^n^"\" ignored") + end; + | None -> () + end; + {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} + +let get_level ~warning entry position levs = + match position with + Some First -> [], empty_lev, levs + | Some Last -> levs, empty_lev, [] + | Some (Level n) -> + let rec get = + function + [] -> + eprintf "No level labelled \"%s\" in entry \"%s\"\n" n + entry.ename; + flush stderr; + failwith "Grammar.extend" + | lev :: 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 + get levs + | Some (Before n) -> + let rec get = + function + [] -> + eprintf "No level labelled \"%s\" in entry \"%s\"\n" n + entry.ename; + flush stderr; + failwith "Grammar.extend" + | lev :: levs -> + if is_level_labelled n lev then [], empty_lev, lev :: levs + else + let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 + in + get levs + | Some (After n) -> + let rec get = + function + [] -> + eprintf "No level labelled \"%s\" in entry \"%s\"\n" n + entry.ename; + flush stderr; + failwith "Grammar.extend" + | lev :: levs -> + if is_level_labelled n lev then [lev], empty_lev, 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 "", levs + | [] -> [], empty_lev, [] + +let change_to_self entry = + function + Snterm e when e == entry -> Sself + | x -> x + +let get_initial entry = + function + Sself :: symbols -> true, symbols + | symbols -> false, symbols + +let insert_tokens gram symbols = + let rec insert = + function + | Slist0 s -> insert s + | Slist1 s -> insert s + | Slist0sep (s, t, _) -> insert s; insert t + | Slist1sep (s, t, _) -> insert s; insert t + | Sopt s -> insert s + | Stree t -> tinsert t + | Stoken ("ANY", _) -> () + | Stoken tok -> + gram.glexer.Plexing.tok_using tok; + let r = + try Hashtbl.find gram.gtokens tok with + Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r + in + incr r + | Snterm _ | Snterml (_, _) | Snext | Sself -> () + and tinsert = + function + Node {node = s; brother = bro; son = son} -> + insert s; tinsert bro; tinsert son + | LocAct (_, _) | DeadEnd -> () + in + List.iter insert symbols + +let levels_of_rules ~warning entry position rules = + let elev = + match entry.edesc with + Dlevels elev -> elev + | Dparser _ -> + eprintf "Error: entry not extensible: \"%s\"\n" entry.ename; + flush stderr; + failwith "Grammar.extend" + in + if rules = [] then elev + else + let (levs1, make_lev, levs2) = get_level ~warning entry position elev in + let (levs, _) = + List.fold_left + (fun (levs, make_lev) (lname, assoc, level) -> + let lev = make_lev lname assoc in + let lev = + List.fold_left + (fun lev (symbols, action) -> + let symbols = List.map (change_to_self entry) symbols in + let (e1, symbols) = get_initial entry symbols in + insert_tokens entry.egram symbols; + insert_level ~warning entry.ename e1 symbols action lev) + lev level + in + lev :: levs, empty_lev) + ([], make_lev) rules + in + levs1 @ List.rev levs @ levs2 + +let logically_eq_symbols entry = + let rec eq_symbols s1 s2 = + match s1, s2 with + Snterm e1, Snterm e2 -> e1.ename = e2.ename + | Snterm e1, Sself -> e1.ename = entry.ename + | Sself, Snterm e2 -> entry.ename = e2.ename + | Snterml (e1, l1), Snterml (e2, l2) -> e1.ename = e2.ename && l1 = l2 + | Slist0 s1, Slist0 s2 -> eq_symbols s1 s2 + | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> + eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 + | Slist1 s1, Slist1 s2 -> eq_symbols s1 s2 + | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> + eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 + | Sopt s1, Sopt s2 -> eq_symbols s1 s2 + | Stree t1, Stree t2 -> eq_trees t1 t2 + | _ -> s1 = s2 + and eq_trees t1 t2 = + match t1, t2 with + Node n1, Node n2 -> + eq_symbols n1.node n2.node && eq_trees n1.son n2.son && + eq_trees n1.brother n2.brother + | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true + | _ -> false + in + eq_symbols + +(* [delete_rule_in_tree] returns + [Some (dsl, t)] if success + [dsl] = + Some (list of deleted nodes) if branch deleted + None if action replaced by previous version of action + [t] = remaining tree + [None] if failure *) + +let delete_rule_in_tree entry = + let rec delete_in_tree symbols tree = + match symbols, tree with + s :: sl, Node n -> + if logically_eq_symbols entry s n.node then delete_son sl n + else + begin match delete_in_tree symbols n.brother with + Some (dsl, t) -> + Some (dsl, Node {node = n.node; son = n.son; brother = t}) + | None -> None + end + | s :: sl, _ -> None + | [], Node n -> + begin match delete_in_tree [] n.brother with + Some (dsl, t) -> + Some (dsl, Node {node = n.node; son = n.son; brother = t}) + | None -> None + end + | [], DeadEnd -> None + | [], LocAct (_, []) -> Some (Some [], DeadEnd) + | [], LocAct (_, action :: list) -> Some (None, LocAct (action, list)) + and delete_son sl n = + match delete_in_tree sl n.son with + Some (Some dsl, DeadEnd) -> Some (Some (n.node :: dsl), n.brother) + | Some (Some dsl, t) -> + let t = Node {node = n.node; son = t; brother = n.brother} in + Some (Some (n.node :: dsl), t) + | Some (None, t) -> + let t = Node {node = n.node; son = t; brother = n.brother} in + Some (None, t) + | None -> None + in + delete_in_tree + +let rec decr_keyw_use gram = + function + Stoken tok -> + let r = Hashtbl.find gram.gtokens tok in + decr r; + if !r == 0 then + begin + Hashtbl.remove gram.gtokens tok; + gram.glexer.Plexing.tok_removing tok + end + | Slist0 s -> decr_keyw_use gram s + | Slist1 s -> decr_keyw_use gram s + | Slist0sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 + | Slist1sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 + | Sopt s -> decr_keyw_use gram s + | Stree t -> decr_keyw_use_in_tree gram t + | Sself | Snext | Snterm _ | Snterml (_, _) -> () +and decr_keyw_use_in_tree gram = + function + DeadEnd | LocAct (_, _) -> () + | Node n -> + decr_keyw_use gram n.node; + decr_keyw_use_in_tree gram n.son; + decr_keyw_use_in_tree gram n.brother + +let rec delete_rule_in_suffix entry symbols = + function + lev :: levs -> + begin match delete_rule_in_tree entry symbols lev.lsuffix with + Some (dsl, t) -> + begin match dsl with + Some dsl -> List.iter (decr_keyw_use entry.egram) dsl + | None -> () + end; + begin match t with + DeadEnd when lev.lprefix == DeadEnd -> levs + | _ -> + let lev = + {assoc = lev.assoc; lname = lev.lname; lsuffix = t; + lprefix = lev.lprefix} + in + lev :: levs + end + | None -> + let levs = delete_rule_in_suffix entry symbols levs in lev :: levs + end + | [] -> raise Not_found + +let rec delete_rule_in_prefix entry symbols = + function + lev :: levs -> + begin match delete_rule_in_tree entry symbols lev.lprefix with + Some (dsl, t) -> + begin match dsl with + Some dsl -> List.iter (decr_keyw_use entry.egram) dsl + | None -> () + end; + begin match t with + DeadEnd when lev.lsuffix == DeadEnd -> levs + | _ -> + let lev = + {assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix; + lprefix = t} + in + lev :: levs + end + | None -> + let levs = delete_rule_in_prefix entry symbols levs in lev :: levs + end + | [] -> raise Not_found + +let delete_rule_in_level_list entry symbols levs = + match symbols with + Sself :: symbols -> delete_rule_in_suffix entry symbols levs + | Snterm e :: symbols when e == entry -> + delete_rule_in_suffix entry symbols levs + | _ -> delete_rule_in_prefix entry symbols levs + external gramext_action : 'a -> g_action = "%identity" let rec flatten_tree = @@ -671,7 +1118,7 @@ let extend_entry ~warning entry position rules = let delete_rule entry sl = match entry.edesc with Dlevels levs -> - let levs = Gramext.delete_rule_in_level_list entry sl levs in + let levs = delete_rule_in_level_list entry sl levs in entry.edesc <- Dlevels levs; entry.estart <- (fun lev strm -> @@ -813,7 +1260,7 @@ module GMake (L : GLexerType) = econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} - external obj : 'a e -> te Gramext.g_entry = "%identity" + external obj : 'a e -> te g_entry = "%identity" let parse (e : 'a e) p : 'a = Obj.magic (parse_parsable e p : Obj.t) let parse_token_stream (e : 'a e) ts : 'a = @@ -827,9 +1274,9 @@ module GMake (L : GLexerType) = edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)} let print ppf e = fprintf ppf "%a@." print_entry (obj e) end - type ('self, 'a) ty_symbol = te Gramext.g_symbol + type ('self, 'a) ty_symbol = te g_symbol type ('self, 'f, 'r) ty_rule = ('self, Obj.t) ty_symbol list - type 'a ty_production = ('a, Obj.t, Obj.t) ty_rule * Gramext.g_action + type 'a ty_production = ('a, Obj.t, Obj.t) ty_rule * g_action let s_nterm e = Snterm e let s_nterml e l = Snterml (e, l) let s_list0 s = Slist0 s @@ -840,7 +1287,7 @@ module GMake (L : GLexerType) = let s_self = Sself let s_next = Snext let s_token tok = Stoken tok - let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t) + let s_rules ~warning (t : Obj.t ty_production list) = srules ~warning (Obj.magic t) let r_stop = [] let r_next r s = r @ [s] let production -- cgit v1.2.3 From fba77d134e27c086a982e61de5741038bf92bb8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 17:28:05 +0100 Subject: Make Grammar truly functorial. The old implementation was simply hiding the fact that the functor relied on a generic data type. If we want to implement the grammar engine in a truly type-safe way, we need to make the ancilliary datatypes depend on the type parameters. --- gramlib/grammar.ml | 120 +++++++++++++++++++++++++++-------------------------- 1 file changed, 62 insertions(+), 58 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 1562a275db..8710dc7bb0 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -5,6 +5,66 @@ open Gramext open Format +(* Functorial interface *) + +module type GLexerType = sig type te val lexer : te Plexing.lexer end + +module type S = + sig + type te + type parsable + val parsable : char Stream.t -> parsable + val tokens : string -> (string * int) list + module Entry : + sig + type 'a e + val create : string -> 'a e + val parse : 'a e -> parsable -> 'a + val name : 'a e -> string + 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 + end + type ('self, 'a) ty_symbol + type ('self, 'f, 'r) ty_rule + type 'a ty_production + val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol + val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol + val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + val s_list0sep : + ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> + ('self, 'a list) ty_symbol + val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + val s_list1sep : + ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> + ('self, 'a list) ty_symbol + val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol + 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 : 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, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production + module Unsafe : + sig + val clear_entry : 'a Entry.e -> unit + end + 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 safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit + end + +(* Implementation *) + +module GMake (L : GLexerType) = +struct + type 'a parser_t = 'a Stream.t -> Obj.t type 'te grammar = @@ -1188,63 +1248,6 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () -(* Functorial interface *) - -module type GLexerType = sig type te val lexer : te Plexing.lexer end - -module type S = - sig - type te - type parsable - val parsable : char Stream.t -> parsable - val tokens : string -> (string * int) list - module Entry : - sig - type 'a e - val create : string -> 'a e - val parse : 'a e -> parsable -> 'a - val name : 'a e -> string - 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 - end - type ('self, 'a) ty_symbol - type ('self, 'f, 'r) ty_rule - type 'a ty_production - val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol - val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol - val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol - val s_list0sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol - val s_list1sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol - 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 : 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, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production - module Unsafe : - sig - val clear_entry : 'a Entry.e -> unit - end - 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 safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit - end - -module GMake (L : GLexerType) = - struct type te = L.te type parsable = te gen_parsable let gram = gcreate L.lexer @@ -1303,4 +1306,5 @@ module GMake (L : GLexerType) = list) = extend_entry ~warning e pos (Obj.magic r) let safe_delete_rule e r = delete_rule (Entry.obj e) r - end + +end -- cgit v1.2.3 From 81c6a0873d90bfa3909c2046054c21096f80eb07 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 17:35:01 +0100 Subject: Specialize the intermediate types of the Grammar functor. Now that we depend on a module argument, we do not have to quantify over the arguments anymore. --- gramlib/grammar.ml | 68 +++++++++++++++++++++++++++--------------------------- 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 8710dc7bb0..5082f8ef5d 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -65,46 +65,48 @@ module type S = module GMake (L : GLexerType) = struct -type 'a parser_t = 'a Stream.t -> Obj.t +type te = L.te -type 'te grammar = +type parser_t = L.te Stream.t -> Obj.t + +type grammar = { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - glexer : 'te Plexing.lexer } + glexer : L.te Plexing.lexer } -type 'te g_entry = - { egram : 'te grammar; +type g_entry = + { egram : grammar; ename : string; elocal : bool; - mutable estart : int -> 'te parser_t; - mutable econtinue : int -> int -> Obj.t -> 'te parser_t; - mutable edesc : 'te g_desc } -and 'te g_desc = - Dlevels of 'te g_level list - | Dparser of 'te parser_t -and 'te g_level = + mutable estart : int -> parser_t; + mutable econtinue : int -> int -> Obj.t -> parser_t; + mutable edesc : g_desc } +and g_desc = + Dlevels of g_level list + | Dparser of parser_t +and g_level = { assoc : g_assoc; lname : string option; - lsuffix : 'te g_tree; - lprefix : 'te g_tree } -and 'te g_symbol = - | Snterm of 'te g_entry - | Snterml of 'te g_entry * string - | Slist0 of 'te g_symbol - | Slist0sep of 'te g_symbol * 'te g_symbol * bool - | Slist1 of 'te g_symbol - | Slist1sep of 'te g_symbol * 'te g_symbol * bool - | Sopt of 'te g_symbol + lsuffix : g_tree; + lprefix : g_tree } +and g_symbol = + | Snterm of g_entry + | Snterml of g_entry * string + | Slist0 of g_symbol + | Slist0sep of g_symbol * g_symbol * bool + | Slist1 of g_symbol + | Slist1sep of g_symbol * g_symbol * bool + | Sopt of g_symbol | Sself | Snext | Stoken of Plexing.pattern - | Stree of 'te g_tree + | Stree of g_tree and g_action = Obj.t -and 'te g_tree = - Node of 'te g_node +and g_tree = + Node of g_node | LocAct of g_action * g_action list | DeadEnd -and 'te g_node = - { node : 'te g_symbol; son : 'te g_tree; brother : 'te g_tree } +and g_node = + { node : g_symbol; son : g_tree; brother : g_tree } let rec derive_eps = function @@ -1203,9 +1205,9 @@ let tokens g con = g.gtokens; !list -type 'te gen_parsable = +type parsable = { pa_chr_strm : char Stream.t; - pa_tok_strm : 'te Stream.t; + pa_tok_strm : L.te Stream.t; pa_loc_func : Plexing.location_function } let parse_parsable entry p = @@ -1248,8 +1250,6 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () - type te = L.te - type parsable = te gen_parsable let gram = gcreate L.lexer let parsable cs = let (ts, lf) = L.lexer.Plexing.tok_func cs in @@ -1257,13 +1257,13 @@ let clear_entry e = let tokens = tokens gram module Entry = struct - type 'a e = te g_entry + type 'a e = g_entry let create n = {egram = gram; ename = n; elocal = false; estart = empty_entry n; econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} - external obj : 'a e -> te g_entry = "%identity" + external obj : 'a e -> g_entry = "%identity" let parse (e : 'a e) p : 'a = Obj.magic (parse_parsable e p : Obj.t) let parse_token_stream (e : 'a e) ts : 'a = @@ -1277,7 +1277,7 @@ let clear_entry e = edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)} let print ppf e = fprintf ppf "%a@." print_entry (obj e) end - type ('self, 'a) ty_symbol = te g_symbol + type ('self, 'a) ty_symbol = g_symbol type ('self, 'f, 'r) ty_rule = ('self, Obj.t) ty_symbol list type 'a ty_production = ('a, Obj.t, Obj.t) ty_rule * g_action let s_nterm e = Snterm e -- cgit v1.2.3 From 5c41d4feb28f181aa6a6a7c9624341eac5eda9d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 17:43:36 +0100 Subject: Centralizing the calls to the global mutable grammar in Grammar. --- gramlib/grammar.ml | 53 ++++++++++++++++++++++++----------------------------- 1 file changed, 24 insertions(+), 29 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 5082f8ef5d..50b3379c51 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -73,10 +73,18 @@ type grammar = { gtokens : (Plexing.pattern, int ref) Hashtbl.t; glexer : L.te Plexing.lexer } +let egram = + {gtokens = Hashtbl.create 301; glexer = L.lexer } + +let tokens con = + let list = ref [] in + Hashtbl.iter + (fun (p_con, p_prm) c -> if p_con = con then list := (p_prm, !c) :: !list) + egram.gtokens; + !list + type g_entry = - { egram : grammar; - ename : string; - elocal : bool; + { ename : string; mutable estart : int -> parser_t; mutable econtinue : int -> int -> Obj.t -> parser_t; mutable edesc : g_desc } @@ -359,7 +367,7 @@ let levels_of_rules ~warning entry position rules = (fun lev (symbols, action) -> let symbols = List.map (change_to_self entry) symbols in let (e1, symbols) = get_initial entry symbols in - insert_tokens entry.egram symbols; + insert_tokens egram symbols; insert_level ~warning entry.ename e1 symbols action lev) lev level in @@ -467,7 +475,7 @@ let rec delete_rule_in_suffix entry symbols = begin match delete_rule_in_tree entry symbols lev.lsuffix with Some (dsl, t) -> begin match dsl with - Some dsl -> List.iter (decr_keyw_use entry.egram) dsl + Some dsl -> List.iter (decr_keyw_use egram) dsl | None -> () end; begin match t with @@ -490,7 +498,7 @@ let rec delete_rule_in_prefix entry symbols = begin match delete_rule_in_tree entry symbols lev.lprefix with Some (dsl, t) -> begin match dsl with - Some dsl -> List.iter (decr_keyw_use entry.egram) dsl + Some dsl -> List.iter (decr_keyw_use egram) dsl | None -> () end; begin match t with @@ -564,13 +572,13 @@ let rec print_symbol ppf = | Stoken (con, prm) when con <> "" && prm <> "" -> fprintf ppf "%s@ %a" con print_str prm | Snterml (e, l) -> - fprintf ppf "%s%s@ LEVEL@ %a" e.ename (if e.elocal then "*" else "") + fprintf ppf "%s%s@ LEVEL@ %a" e.ename "" print_str l | Snterm _ | Snext | Sself | Stoken _ | Stree _ as s -> print_symbol1 ppf s and print_symbol1 ppf = function - | Snterm e -> fprintf ppf "%s%s" e.ename (if e.elocal then "*" else "") + | Snterm e -> fprintf ppf "%s%s" e.ename "" | Sself -> pp_print_string ppf "SELF" | Snext -> pp_print_string ppf "NEXT" | Stoken ("", s) -> print_str ppf s @@ -646,7 +654,7 @@ let name_of_symbol entry = Snterm e -> "[" ^ e.ename ^ "]" | Snterml (e, l) -> "[" ^ e.ename ^ " level " ^ l ^ "]" | Sself | Snext -> "[" ^ entry.ename ^ "]" - | Stoken tok -> entry.egram.glexer.Plexing.tok_text tok + | Stoken tok -> egram.glexer.Plexing.tok_text tok | _ -> "???" let rec get_token_list entry rev_tokl last_tok tree = @@ -690,7 +698,7 @@ and name_of_tree_failed entry = List.fold_left (fun s tok -> (if s = "" then "" else s ^ " ") ^ - entry.egram.glexer.Plexing.tok_text tok) + egram.glexer.Plexing.tok_text tok) "" (List.rev (last_tok :: rev_tokl)) end | DeadEnd | LocAct (_, _) -> "???" @@ -903,7 +911,7 @@ and parser_cont p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) = and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = let plast = let n = List.length rev_tokl + 1 in - let tematch = token_ematch entry.egram last_tok in + let tematch = token_ematch egram last_tok in let ps strm = match peek_nth n strm with Some tok -> @@ -921,7 +929,7 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = match List.rev rev_tokl with [] -> (fun (strm__ : _ Stream.t) -> plast strm__) | tok :: tokl -> - let tematch = token_ematch entry.egram tok in + let tematch = token_ematch egram tok in let ps strm = match peek_nth 1 strm with Some tok -> tematch tok @@ -932,7 +940,7 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = function [] -> plast | tok :: tokl -> - let tematch = token_ematch entry.egram tok in + let tematch = token_ematch egram tok in let ps strm = match peek_nth n strm with Some tok -> tematch tok @@ -1068,7 +1076,7 @@ and parser_of_symbol entry nlevn = | Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__) | Stoken tok -> parser_of_token entry tok and parser_of_token entry tok = - let f = entry.egram.glexer.Plexing.tok_match tok in + let f = egram.glexer.Plexing.tok_match tok in fun strm -> match Stream.peek strm with Some tok -> let r = f tok in Stream.junk strm; Obj.repr r @@ -1194,17 +1202,6 @@ let delete_rule entry sl = (* Normal interface *) -let create_toktab () = Hashtbl.create 301 -let gcreate glexer = - {gtokens = create_toktab (); glexer = glexer } - -let tokens g con = - let list = ref [] in - Hashtbl.iter - (fun (p_con, p_prm) c -> if p_con = con then list := (p_prm, !c) :: !list) - g.gtokens; - !list - type parsable = { pa_chr_strm : char Stream.t; pa_tok_strm : L.te Stream.t; @@ -1250,16 +1247,14 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () - let gram = gcreate L.lexer let parsable cs = 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 module Entry = struct type 'a e = g_entry let create n = - {egram = gram; ename = n; elocal = false; estart = empty_entry n; + { ename = n; estart = empty_entry n; econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} @@ -1270,7 +1265,7 @@ let clear_entry e = Obj.magic (e.estart 0 ts : Obj.t) let name e = e.ename let of_parser n (p : te Stream.t -> 'a) : 'a e = - {egram = gram; ename = n; elocal = false; + { ename = n; estart = (fun _ -> (Obj.magic p : te Stream.t -> Obj.t)); econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); -- cgit v1.2.3 From 8c3bf38e574b576dfd5389ff012c7dbc969fc2ab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 17:50:30 +0100 Subject: Introduce a GADT of well-typed grammar entries in Grammar. Not fully used yet, we rely on erasure casts for now. --- gramlib/grammar.ml | 99 +++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 68 insertions(+), 31 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 50b3379c51..b7a38fa5f9 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -116,6 +116,53 @@ and g_tree = and g_node = { node : g_symbol; son : g_tree; brother : g_tree } +external gramext_action : 'a -> g_action = "%identity" +external app : Obj.t -> 'a = "%identity" + +type ('self, 'a) ty_symbol = +| Ttoken : Plexing.pattern -> ('self, string) ty_symbol +| Tlist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol +| Tlist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol +| Tlist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol +| Tlist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol +| Topt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol +| Tself : ('self, 'self) ty_symbol +| Tnext : ('self, 'self) ty_symbol +| Tnterm : g_entry -> ('self, 'a) ty_symbol +| Tnterml : g_entry * string -> ('self, 'a) ty_symbol +| Ttree : g_tree -> ('self, 'a) ty_symbol + +and ('self, _, 'r) ty_rule = +| TStop : ('self, 'r, 'r) ty_rule +| TNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule + +type 'a ty_production = +| TProd : ('a, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production + +let rec u_symbol : type s a. (s, a) ty_symbol -> g_symbol = function +| Ttoken t -> Stoken t +| Tlist1 t -> Slist1 (u_symbol t) +| Tlist1sep (t, s, b) -> Slist1sep (u_symbol t, u_symbol s, b) +| Tlist0 t -> Slist0 (u_symbol t) +| Tlist0sep (t, s, b) -> Slist0sep (u_symbol t, u_symbol s, b) +| Topt t -> Sopt (u_symbol t) +| Tself -> Sself +| Tnext -> Snext +| Tnterm e -> Snterm e +| Tnterml (e, n) -> Snterml (e, n) +| Ttree t -> Stree t + +let rec u_rule : type s a r. (s, a, r) ty_rule -> g_symbol list -> g_symbol list = fun r accu -> match r with +| TStop -> accu +| TNext (r, t) -> u_rule r (u_symbol t :: accu) + +let u_production = function +| TProd (r, act) -> (u_rule r [], gramext_action act) + +let u_extend rl = + let map (lvl, assoc, prods) = (lvl, assoc, List.map u_production prods) in + List.map map rl + let rec derive_eps = function Slist0 _ -> true @@ -206,9 +253,9 @@ let srules ~warning rl = let t = List.fold_left (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) - DeadEnd rl + DeadEnd (List.map u_production rl) in - Stree t + Ttree t let is_level_labelled n lev = match lev.lname with @@ -522,8 +569,6 @@ let delete_rule_in_level_list entry symbols levs = delete_rule_in_suffix entry symbols levs | _ -> delete_rule_in_prefix entry symbols levs -external gramext_action : 'a -> g_action = "%identity" - let rec flatten_tree = function DeadEnd -> [] @@ -740,8 +785,6 @@ let symb_failed entry prev_symb_result prev_symb symb = let tree = Node {node = symb; brother = DeadEnd; son = DeadEnd} in tree_failed entry prev_symb_result prev_symb tree -external app : Obj.t -> 'a = "%identity" - let is_level_labelled n lev = match lev.lname with Some n1 -> n = n1 @@ -1258,7 +1301,6 @@ let clear_entry e = econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} - external obj : 'a e -> g_entry = "%identity" let parse (e : 'a e) p : 'a = Obj.magic (parse_parsable e p : Obj.t) let parse_token_stream (e : 'a e) ts : 'a = @@ -1270,36 +1312,31 @@ let clear_entry e = econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)} - let print ppf e = fprintf ppf "%a@." print_entry (obj e) + let print ppf e = fprintf ppf "%a@." print_entry e end - type ('self, 'a) ty_symbol = g_symbol - type ('self, 'f, 'r) ty_rule = ('self, Obj.t) ty_symbol list - type 'a ty_production = ('a, Obj.t, Obj.t) ty_rule * g_action - let s_nterm e = Snterm e - let s_nterml e l = Snterml (e, l) - let s_list0 s = Slist0 s - let s_list0sep s sep b = Slist0sep (s, sep, b) - let s_list1 s = Slist1 s - let s_list1sep s sep b = Slist1sep (s, sep, b) - let s_opt s = Sopt s - let s_self = Sself - let s_next = Snext - let s_token tok = Stoken tok - let s_rules ~warning (t : Obj.t ty_production list) = srules ~warning (Obj.magic t) - let r_stop = [] - let r_next r s = r @ [s] - let production - (p : ('a, 'f, Loc.t -> 'a) ty_rule * 'f) : 'a ty_production = - Obj.magic p + let s_nterm e = Tnterm e + let s_nterml e l = Tnterml (e, l) + let s_list0 s = Tlist0 s + let s_list0sep s sep b = Tlist0sep (s, sep, b) + let s_list1 s = Tlist1 s + let s_list1sep s sep b = Tlist1sep (s, sep, b) + let s_opt s = Topt s + let s_self = Tself + let s_next = Tnext + let s_token tok = Ttoken tok + let s_rules ~warning (t : 'a ty_production list) = srules ~warning t + let r_stop = TStop + let r_next r s = TNext (r, s) + let production (p, act) = TProd (p, act) module Unsafe = struct let clear_entry = clear_entry end - let safe_extend ~warning e pos + let safe_extend ~warning (e : 'a Entry.e) pos (r : - (string option * Gramext.g_assoc option * Obj.t ty_production list) + (string option * Gramext.g_assoc option * 'a ty_production list) list) = - extend_entry ~warning e pos (Obj.magic r) - let safe_delete_rule e r = delete_rule (Entry.obj e) r + extend_entry ~warning e pos (u_extend r) + let safe_delete_rule e r = delete_rule e (u_rule r []) end -- cgit v1.2.3 From 287ec1199df6962e9b399a697322fc4fee904996 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 19:01:20 +0100 Subject: Further propagation of well-typedness in Grammar. --- gramlib/grammar.ml | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index b7a38fa5f9..782fbcfc58 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -156,13 +156,6 @@ let rec u_rule : type s a r. (s, a, r) ty_rule -> g_symbol list -> g_symbol list | TStop -> accu | TNext (r, t) -> u_rule r (u_symbol t :: accu) -let u_production = function -| TProd (r, act) -> (u_rule r [], gramext_action act) - -let u_extend rl = - let map (lvl, assoc, prods) = (lvl, assoc, List.map u_production prods) in - List.map map rl - let rec derive_eps = function Slist0 _ -> true @@ -220,8 +213,8 @@ let insert_tree ~warning entry_name gsymbols action tree = "some rule has been masked" in warn_fn msg end; - LocAct (action, old_action :: action_list) - | DeadEnd -> LocAct (action, []) + LocAct (gramext_action action, old_action :: action_list) + | DeadEnd -> LocAct (gramext_action action, []) and insert_in_tree s sl tree = match try_insert s sl tree with Some t -> t @@ -252,8 +245,8 @@ let insert_tree ~warning entry_name gsymbols action tree = let srules ~warning rl = let t = List.fold_left - (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) - DeadEnd (List.map u_production rl) + (fun tree (TProd (symbols, action)) -> insert_tree ~warning "" (u_rule symbols []) action tree) + DeadEnd rl in Ttree t @@ -357,10 +350,15 @@ let get_level ~warning entry position levs = lev :: levs -> [], change_lev ~warning lev "", levs | [] -> [], empty_lev, [] -let change_to_self entry = +(** FIXME *) +let change_to_self0 (entry : g_entry) (type s) (type a) : (s, a) ty_symbol -> (s, a) ty_symbol = function - Snterm e when e == entry -> Sself - | x -> x + Tnterm e when e == entry -> (Obj.magic Tself) + | x -> (Obj.magic x) + +let rec change_to_self : type s a r. g_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with +| TStop -> TStop +| TNext (r, t) -> TNext (change_to_self e r, change_to_self0 e t) let get_initial entry = function @@ -402,8 +400,9 @@ let levels_of_rules ~warning entry position rules = flush stderr; failwith "Grammar.extend" in - if rules = [] then elev - else + match rules with + | [] -> elev + | _ -> let (levs1, make_lev, levs2) = get_level ~warning entry position elev in let (levs, _) = List.fold_left @@ -411,8 +410,9 @@ let levels_of_rules ~warning entry position rules = let lev = make_lev lname assoc in let lev = List.fold_left - (fun lev (symbols, action) -> - let symbols = List.map (change_to_self entry) symbols in + (fun lev (TProd (symbols, action)) -> + let symbols = change_to_self entry symbols in + let symbols = u_rule symbols [] in let (e1, symbols) = get_initial entry symbols in insert_tokens egram symbols; insert_level ~warning entry.ename e1 symbols action lev) @@ -1223,7 +1223,7 @@ let init_entry_functions entry = entry.econtinue <- f; f lev bp a strm) let extend_entry ~warning entry position rules = - let elev = Gramext.levels_of_rules ~warning entry position rules in + let elev = levels_of_rules ~warning entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry (* Deleting a rule *) @@ -1336,7 +1336,7 @@ let clear_entry e = (r : (string option * Gramext.g_assoc option * 'a ty_production list) list) = - extend_entry ~warning e pos (u_extend r) + extend_entry ~warning e pos r let safe_delete_rule e r = delete_rule e (u_rule r []) end -- cgit v1.2.3 From 9da757b47984837ed5d6b88e72325b45d2122c17 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Feb 2019 20:11:43 +0100 Subject: Almost fully type-safe implementation of camlp5. There are still minute uses of type-unsafe primitives. Most of them can be removed if I had a little higher dan in GADTs (or weeks to spare thinking about how non-interactive proofs can be performed) but one, which is really a potential source of unsoundness. The latter is not problematic as all uses in Coq are protected about the unsoundness proof, but the API is clearly deficient and needs to be fixed at some point. --- gramlib/grammar.ml | 613 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 360 insertions(+), 253 deletions(-) diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 782fbcfc58..e313f2e648 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -5,6 +5,8 @@ open Gramext open Format +type ('a, 'b) eq = Refl : ('a, 'a) eq + (* Functorial interface *) module type GLexerType = sig type te val lexer : te Plexing.lexer end @@ -67,7 +69,7 @@ struct type te = L.te -type parser_t = L.te Stream.t -> Obj.t +type 'a parser_t = L.te Stream.t -> 'a type grammar = { gtokens : (Plexing.pattern, int ref) Hashtbl.t; @@ -83,110 +85,113 @@ let tokens con = egram.gtokens; !list -type g_entry = - { ename : string; - mutable estart : int -> parser_t; - mutable econtinue : int -> int -> Obj.t -> parser_t; - mutable edesc : g_desc } -and g_desc = - Dlevels of g_level list - | Dparser of parser_t -and g_level = - { assoc : g_assoc; - lname : string option; - lsuffix : g_tree; - lprefix : g_tree } -and g_symbol = - | Snterm of g_entry - | Snterml of g_entry * string - | Slist0 of g_symbol - | Slist0sep of g_symbol * g_symbol * bool - | Slist1 of g_symbol - | Slist1sep of g_symbol * g_symbol * bool - | Sopt of g_symbol - | Sself - | Snext - | Stoken of Plexing.pattern - | Stree of g_tree -and g_action = Obj.t -and g_tree = - Node of g_node - | LocAct of g_action * g_action list - | DeadEnd -and g_node = - { node : g_symbol; son : g_tree; brother : g_tree } - -external gramext_action : 'a -> g_action = "%identity" -external app : Obj.t -> 'a = "%identity" - -type ('self, 'a) ty_symbol = -| Ttoken : Plexing.pattern -> ('self, string) ty_symbol -| Tlist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol -| Tlist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol -| Tlist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol -| Tlist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol -| Topt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol -| Tself : ('self, 'self) ty_symbol -| Tnext : ('self, 'self) ty_symbol -| Tnterm : g_entry -> ('self, 'a) ty_symbol -| Tnterml : g_entry * string -> ('self, 'a) ty_symbol -| Ttree : g_tree -> ('self, 'a) ty_symbol +type 'a ty_entry = { + ename : string; + mutable estart : int -> 'a parser_t; + mutable econtinue : int -> int -> 'a -> 'a parser_t; + mutable edesc : 'a ty_desc; +} + +and 'a ty_desc = +| Dlevels of 'a ty_level list +| Dparser of 'a parser_t + +and 'a ty_level = { + assoc : g_assoc; + lname : string option; + lsuffix : ('a, 'a -> Loc.t -> 'a) ty_tree; + lprefix : ('a, Loc.t -> 'a) ty_tree; +} + +and ('self, 'a) ty_symbol = +| Stoken : Plexing.pattern -> ('self, string) ty_symbol +| Slist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol +| Slist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol +| Slist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol +| Slist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol +| Sopt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol +| Sself : ('self, 'self) ty_symbol +| Snext : ('self, 'self) ty_symbol +| Snterm : 'a ty_entry -> ('self, 'a) ty_symbol +| Snterml : 'a ty_entry * string -> ('self, 'a) ty_symbol +| Stree : ('self, Loc.t -> 'a) ty_tree -> ('self, 'a) ty_symbol and ('self, _, 'r) ty_rule = | TStop : ('self, 'r, 'r) ty_rule | TNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule +and ('self, 'a) ty_tree = +| Node : ('self, 'b, 'a) ty_node -> ('self, 'a) ty_tree +| LocAct : 'k * 'k list -> ('self, 'k) ty_tree +| DeadEnd : ('self, 'k) ty_tree + +and ('self, 'a, 'r) ty_node = { + node : ('self, 'a) ty_symbol; + son : ('self, 'a -> 'r) ty_tree; + brother : ('self, 'r) ty_tree; +} + type 'a ty_production = | TProd : ('a, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production -let rec u_symbol : type s a. (s, a) ty_symbol -> g_symbol = function -| Ttoken t -> Stoken t -| Tlist1 t -> Slist1 (u_symbol t) -| Tlist1sep (t, s, b) -> Slist1sep (u_symbol t, u_symbol s, b) -| Tlist0 t -> Slist0 (u_symbol t) -| Tlist0sep (t, s, b) -> Slist0sep (u_symbol t, u_symbol s, b) -| Topt t -> Sopt (u_symbol t) -| Tself -> Sself -| Tnext -> Snext -| Tnterm e -> Snterm e -| Tnterml (e, n) -> Snterml (e, n) -| Ttree t -> Stree t - -let rec u_rule : type s a r. (s, a, r) ty_rule -> g_symbol list -> g_symbol list = fun r accu -> match r with -| TStop -> accu -| TNext (r, t) -> u_rule r (u_symbol t :: accu) - -let rec derive_eps = +let rec derive_eps : type s a. (s, a) ty_symbol -> bool = function Slist0 _ -> true | Slist0sep (_, _, _) -> true | Sopt _ -> true | Stree t -> tree_derive_eps t - | Slist1 _ | Slist1sep (_, _, _) | Snterm _ | - Snterml (_, _) | Snext | Sself | Stoken _ -> - false -and tree_derive_eps = + | Slist1 _ -> false + | Slist1sep (_, _, _) -> false + | Snterm _ | Snterml (_, _) -> false + | Snext -> false + | Sself -> false + | Stoken _ -> false +and tree_derive_eps : type s a. (s, a) ty_tree -> bool = function LocAct (_, _) -> true | Node {node = s; brother = bro; son = son} -> derive_eps s && tree_derive_eps son || tree_derive_eps bro | DeadEnd -> false -let rec eq_symbol s1 s2 = +(** FIXME: find a way to do that type-safely *) +let eq_entry : type a1 a2. a1 ty_entry -> a2 ty_entry -> (a1, a2) eq option = fun e1 e2 -> + if (Obj.magic e1) == (Obj.magic e2) then Some (Obj.magic Refl) + else None + +let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 -> match s1, s2 with - Snterm e1, Snterm e2 -> e1 == e2 - | Snterml (e1, l1), Snterml (e2, l2) -> e1 == e2 && l1 = l2 - | Slist0 s1, Slist0 s2 -> eq_symbol s1 s2 + Snterm e1, Snterm e2 -> eq_entry e1 e2 + | Snterml (e1, l1), Snterml (e2, l2) -> + if String.equal l1 l2 then eq_entry e1 e2 else None + | Slist0 s1, Slist0 s2 -> + begin match eq_symbol s1 s2 with None -> None | Some Refl -> Some Refl end | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> - eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 - | Slist1 s1, Slist1 s2 -> eq_symbol s1 s2 + if b1 = b2 then match eq_symbol s1 s2 with + | None -> None + | Some Refl -> + match eq_symbol sep1 sep2 with + | None -> None + | Some Refl -> Some Refl + else None + | Slist1 s1, Slist1 s2 -> + begin match eq_symbol s1 s2 with None -> None | Some Refl -> Some Refl end | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> - eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 - | Sopt s1, Sopt s2 -> eq_symbol s1 s2 - | Stree _, Stree _ -> false - | _ -> s1 = s2 - -let is_before s1 s2 = + if b1 = b2 then match eq_symbol s1 s2 with + | None -> None + | Some Refl -> + match eq_symbol sep1 sep2 with + | None -> None + | Some Refl -> Some Refl + else None + | Sopt s1, Sopt s2 -> + begin match eq_symbol s1 s2 with None -> None | Some Refl -> Some Refl end + | Stree _, Stree _ -> None + | Sself, Sself -> Some Refl + | Snext, Snext -> Some Refl + | Stoken p1, Stoken p2 -> if p1 = p2 then Some Refl else None + | _ -> None + +let is_before : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 -> match s1, s2 with Stoken ("ANY", _), _ -> false | _, Stoken ("ANY", _) -> true @@ -195,14 +200,46 @@ let is_before s1 s2 = | Stoken _, _ -> true | _ -> false -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 - | [] -> +(** Ancilliary datatypes *) + +type ('self, _) ty_symbols = +| TNil : ('self, unit) ty_symbols +| TCns : ('self, 'a) ty_symbol * ('self, 'b) ty_symbols -> ('self, 'a * 'b) ty_symbols + +(** ('i, 'p, 'f, 'r) rel_prod0 ~ + ∃ α₁ ... αₙ. + p ≡ αₙ * ... α₁ * 'i ∧ + f ≡ α₁ -> ... -> αₙ -> 'r +*) +type ('i, _, 'f, _) rel_prod0 = +| Rel0 : ('i, 'i, 'f, 'f) rel_prod0 +| RelS : ('i, 'p, 'f, 'a -> 'r) rel_prod0 -> ('i, 'a * 'p, 'f, 'r) rel_prod0 + +type ('p, 'k, 'r) rel_prod = (unit, 'p, 'k, 'r) rel_prod0 + +type ('s, 'i, 'k, 'r) any_symbols = +| AnyS : ('s, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'i, 'k, 'r) any_symbols + +(** FIXME *) +let rec symbols : type s p k r. (s, p) ty_symbols -> (s, k, r) ty_rule -> (s, unit, k, r) any_symbols = + fun accu r -> match r with + | TStop -> AnyS (Obj.magic accu, Rel0) + | TNext (r, s) -> + let AnyS (r, pf) = symbols (TCns (s, accu)) r in + AnyS (Obj.magic r, RelS (Obj.magic pf)) + +let get_symbols : type s k r. (s, k, r) ty_rule -> (s, unit, k, r) any_symbols = + fun r -> symbols TNil r + +let insert_tree (type s p k a) ~warning entry_name (gsymbols : (s, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, a) ty_tree) = + let rec insert : type p f k. (s, p) ty_symbols -> (p, k, f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree = + fun symbols pf tree action -> + match symbols, pf with + TCns (s, sl), RelS pf -> insert_in_tree s sl pf tree action + | TNil, Rel0 -> match tree with Node {node = s; son = son; brother = bro} -> - Node {node = s; son = son; brother = insert [] bro} + Node {node = s; son = son; brother = insert TNil Rel0 bro action} | LocAct (old_action, action_list) -> begin match warning with | None -> () @@ -213,57 +250,66 @@ let insert_tree ~warning entry_name gsymbols action tree = "some rule has been masked" in warn_fn msg end; - LocAct (gramext_action action, old_action :: action_list) - | DeadEnd -> LocAct (gramext_action action, []) - and insert_in_tree s sl tree = - match try_insert s sl tree with + LocAct (action, old_action :: action_list) + | DeadEnd -> LocAct (action, []) + and insert_in_tree : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree = + fun s sl pf tree action -> + match try_insert s sl pf tree action with Some t -> t - | None -> Node {node = s; son = insert sl DeadEnd; brother = tree} - and try_insert s sl tree = + | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = tree} + and try_insert : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree option = + fun s sl pf tree action -> match tree with Node {node = s1; son = son; brother = bro} -> - if eq_symbol s s1 then - let t = Node {node = s1; son = insert sl son; brother = bro} in + begin match eq_symbol s s1 with + | Some Refl -> + let t = Node {node = s1; son = insert sl pf son action; brother = bro} in Some t - else if is_before s1 s || derive_eps s && not (derive_eps s1) then + | None -> + if is_before s1 s || derive_eps s && not (derive_eps s1) then let bro = - match try_insert s sl bro with + match try_insert s sl pf bro action with Some bro -> bro - | None -> Node {node = s; son = insert sl DeadEnd; brother = bro} + | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = bro} in let t = Node {node = s1; son = son; brother = bro} in Some t else - begin match try_insert s sl bro with + begin match try_insert s sl pf bro action with Some bro -> let t = Node {node = s1; son = son; brother = bro} in Some t | None -> None end + end | LocAct (_, _) | DeadEnd -> None in - insert gsymbols tree + insert gsymbols pf tree action -let srules ~warning rl = +let srules (type self a) ~warning (rl : a ty_production list) = let t = List.fold_left - (fun tree (TProd (symbols, action)) -> insert_tree ~warning "" (u_rule symbols []) action tree) + (fun tree (TProd (symbols, action)) -> + let AnyS (symbols, pf) = get_symbols symbols in + insert_tree ~warning "" symbols pf action tree) DeadEnd rl in - Ttree t + (* FIXME: use an universal self type to ensure well-typedness *) + (Obj.magic (Stree t) : (self, a) ty_symbol) let is_level_labelled n lev = match lev.lname with Some n1 -> n = n1 | None -> false -let insert_level ~warning entry_name e1 symbols action slev = - match e1 with - true -> +let insert_level (type s p k) ~warning entry_name (symbols : (s, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = + match symbols with + | TCns (Sself, symbols) -> + let RelS pf = pf in {assoc = slev.assoc; lname = slev.lname; - lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix; + lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix; lprefix = slev.lprefix} - | false -> + | _ -> {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; - lprefix = insert_tree ~warning entry_name symbols action slev.lprefix} + lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix} let empty_lev lname assoc = let assoc = @@ -350,23 +396,21 @@ let get_level ~warning entry position levs = lev :: levs -> [], change_lev ~warning lev "", levs | [] -> [], empty_lev, [] -(** FIXME *) -let change_to_self0 (entry : g_entry) (type s) (type a) : (s, a) ty_symbol -> (s, a) ty_symbol = +let change_to_self0 (type s) (type a) (entry : s ty_entry) : (s, a) ty_symbol -> (s, a) ty_symbol = function - Tnterm e when e == entry -> (Obj.magic Tself) - | x -> (Obj.magic x) + | Snterm e -> + begin match eq_entry e entry with + | None -> Snterm e + | Some Refl -> Sself + end + | x -> x -let rec change_to_self : type s a r. g_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with +let rec change_to_self : type s a r. s ty_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with | TStop -> TStop | TNext (r, t) -> TNext (change_to_self e r, change_to_self0 e t) -let get_initial entry = - function - Sself :: symbols -> true, symbols - | symbols -> false, symbols - let insert_tokens gram symbols = - let rec insert = + let rec insert : type s a. (s, a) ty_symbol -> unit = function | Slist0 s -> insert s | Slist1 s -> insert s @@ -382,14 +426,19 @@ let insert_tokens gram symbols = Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r in incr r - | Snterm _ | Snterml (_, _) | Snext | Sself -> () - and tinsert = + | Snterm _ | Snterml (_, _) -> () + | Snext -> () + | Sself -> () + and tinsert : type s a. (s, a) ty_tree -> unit = function Node {node = s; brother = bro; son = son} -> insert s; tinsert bro; tinsert son | LocAct (_, _) | DeadEnd -> () + and linsert : type s p. (s, p) ty_symbols -> unit = function + | TNil -> () + | TCns (s, r) -> insert s; linsert r in - List.iter insert symbols + linsert symbols let levels_of_rules ~warning entry position rules = let elev = @@ -412,10 +461,9 @@ let levels_of_rules ~warning entry position rules = List.fold_left (fun lev (TProd (symbols, action)) -> let symbols = change_to_self entry symbols in - let symbols = u_rule symbols [] in - let (e1, symbols) = get_initial entry symbols in + let AnyS (symbols, pf) = get_symbols symbols in insert_tokens egram symbols; - insert_level ~warning entry.ename e1 symbols action lev) + insert_level ~warning entry.ename symbols pf action lev) lev level in lev :: levs, empty_lev) @@ -424,7 +472,7 @@ let levels_of_rules ~warning entry position rules = levs1 @ List.rev levs @ levs2 let logically_eq_symbols entry = - let rec eq_symbols s1 s2 = + let rec eq_symbols : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 -> match s1, s2 with Snterm e1, Snterm e2 -> e1.ename = e2.ename | Snterm e1, Sself -> e1.ename = entry.ename @@ -438,8 +486,11 @@ let logically_eq_symbols entry = eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 | Sopt s1, Sopt s2 -> eq_symbols s1 s2 | Stree t1, Stree t2 -> eq_trees t1 t2 - | _ -> s1 = s2 - and eq_trees t1 t2 = + | Stoken p1, Stoken p2 -> p1 = p2 + | Sself, Sself -> true + | Snext, Snext -> true + | _ -> false + and eq_trees : type s1 s2 a1 a2. (s1, a1) ty_tree -> (s2, a2) ty_tree -> bool = fun t1 t2 -> match t1, t2 with Node n1, Node n2 -> eq_symbols n1.node n2.node && eq_trees n1.son n2.son && @@ -457,10 +508,15 @@ let logically_eq_symbols entry = [t] = remaining tree [None] if failure *) +type 's ex_symbols = +| ExS : ('s, 'p) ty_symbols -> 's ex_symbols + let delete_rule_in_tree entry = - let rec delete_in_tree symbols tree = + let rec delete_in_tree : + type s p r. (s, p) ty_symbols -> (s, r) ty_tree -> (s ex_symbols option * (s, r) ty_tree) option = + fun symbols tree -> match symbols, tree with - s :: sl, Node n -> + | TCns (s, sl), Node n -> if logically_eq_symbols entry s n.node then delete_son sl n else begin match delete_in_tree symbols n.brother with @@ -468,22 +524,24 @@ let delete_rule_in_tree entry = Some (dsl, Node {node = n.node; son = n.son; brother = t}) | None -> None end - | s :: sl, _ -> None - | [], Node n -> - begin match delete_in_tree [] n.brother with + | TCns (s, sl), _ -> None + | TNil, Node n -> + begin match delete_in_tree TNil n.brother with Some (dsl, t) -> Some (dsl, Node {node = n.node; son = n.son; brother = t}) | None -> None end - | [], DeadEnd -> None - | [], LocAct (_, []) -> Some (Some [], DeadEnd) - | [], LocAct (_, action :: list) -> Some (None, LocAct (action, list)) - and delete_son sl n = + | TNil, DeadEnd -> None + | TNil, LocAct (_, []) -> Some (Some (ExS TNil), DeadEnd) + | TNil, LocAct (_, action :: list) -> Some (None, LocAct (action, list)) + and delete_son : + type s p a r. (s, p) ty_symbols -> (s, a, r) ty_node -> (s ex_symbols option * (s, r) ty_tree) option = + fun sl n -> match delete_in_tree sl n.son with - Some (Some dsl, DeadEnd) -> Some (Some (n.node :: dsl), n.brother) - | Some (Some dsl, t) -> + Some (Some (ExS dsl), DeadEnd) -> Some (Some (ExS (TCns (n.node, dsl))), n.brother) + | Some (Some (ExS dsl), t) -> let t = Node {node = n.node; son = t; brother = n.brother} in - Some (Some (n.node :: dsl), t) + Some (Some (ExS (TCns (n.node, dsl))), t) | Some (None, t) -> let t = Node {node = n.node; son = t; brother = n.brother} in Some (None, t) @@ -491,7 +549,7 @@ let delete_rule_in_tree entry = in delete_in_tree -let rec decr_keyw_use gram = +let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram -> function Stoken tok -> let r = Hashtbl.find gram.gtokens tok in @@ -507,14 +565,20 @@ let rec decr_keyw_use gram = | Slist1sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 | Sopt s -> decr_keyw_use gram s | Stree t -> decr_keyw_use_in_tree gram t - | Sself | Snext | Snterm _ | Snterml (_, _) -> () -and decr_keyw_use_in_tree gram = + | Sself -> () + | Snext -> () + | Snterm _ | Snterml (_, _) -> () +and decr_keyw_use_in_tree : type s a. _ -> (s, a) ty_tree -> unit = fun gram -> function DeadEnd | LocAct (_, _) -> () | Node n -> decr_keyw_use gram n.node; decr_keyw_use_in_tree gram n.son; decr_keyw_use_in_tree gram n.brother +and decr_keyw_use_in_list : type s p. _ -> (s, p) ty_symbols -> unit = fun gram -> + function + | TNil -> () + | TCns (s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l let rec delete_rule_in_suffix entry symbols = function @@ -522,7 +586,7 @@ let rec delete_rule_in_suffix entry symbols = begin match delete_rule_in_tree entry symbols lev.lsuffix with Some (dsl, t) -> begin match dsl with - Some dsl -> List.iter (decr_keyw_use egram) dsl + Some (ExS dsl) -> decr_keyw_use_in_list egram dsl | None -> () end; begin match t with @@ -545,7 +609,7 @@ let rec delete_rule_in_prefix entry symbols = begin match delete_rule_in_tree entry symbols lev.lprefix with Some (dsl, t) -> begin match dsl with - Some dsl -> List.iter (decr_keyw_use egram) dsl + Some (ExS dsl) -> decr_keyw_use_in_list egram dsl | None -> () end; begin match t with @@ -562,19 +626,23 @@ let rec delete_rule_in_prefix entry symbols = end | [] -> raise Not_found -let delete_rule_in_level_list entry symbols levs = +let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p) ty_symbols) levs = match symbols with - Sself :: symbols -> delete_rule_in_suffix entry symbols levs - | Snterm e :: symbols when e == entry -> - delete_rule_in_suffix entry symbols levs + TCns (Sself, symbols) -> delete_rule_in_suffix entry symbols levs + | TCns (Snterm e, symbols') -> + begin match eq_entry e entry with + | None -> delete_rule_in_prefix entry symbols levs + | Some Refl -> + delete_rule_in_suffix entry symbols' levs + end | _ -> delete_rule_in_prefix entry symbols levs -let rec flatten_tree = +let rec flatten_tree : type s a. (s, a) ty_tree -> s ex_symbols list = function DeadEnd -> [] - | LocAct (_, _) -> [[]] + | LocAct (_, _) -> [ExS TNil] | Node {node = n; brother = b; son = s} -> - List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b + List.map (fun (ExS l) -> ExS (TCns (n, l))) (flatten_tree s) @ flatten_tree b let utf8_print = ref true @@ -603,7 +671,8 @@ let string_escaped s = let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s) -let rec print_symbol ppf = +let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit = + fun ppf -> function | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s | Slist0sep (s, t, osep) -> @@ -619,9 +688,9 @@ let rec print_symbol ppf = | Snterml (e, l) -> fprintf ppf "%s%s@ LEVEL@ %a" e.ename "" print_str l - | Snterm _ | Snext | Sself | Stoken _ | Stree _ as s -> - print_symbol1 ppf s -and print_symbol1 ppf = + | s -> print_symbol1 ppf s +and print_symbol1 : type s r. formatter -> (s, r) ty_symbol -> unit = + fun ppf -> function | Snterm e -> fprintf ppf "%s%s" e.ename "" | Sself -> pp_print_string ppf "SELF" @@ -629,24 +698,26 @@ and print_symbol1 ppf = | Stoken ("", s) -> print_str ppf s | Stoken (con, "") -> pp_print_string ppf con | Stree t -> print_level ppf pp_print_space (flatten_tree t) - | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) | - Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ as s -> + | s -> fprintf ppf "(%a)" print_symbol s -and print_rule ppf symbols = +and print_rule : type s p. formatter -> (s, p) ty_symbols -> unit = + fun ppf symbols -> fprintf ppf "@["; - let _ = - List.fold_left - (fun sep symbol -> - fprintf ppf "%t%a" sep print_symbol symbol; - fun ppf -> fprintf ppf ";@ ") - (fun ppf -> ()) symbols + let rec fold : type s p. _ -> (s, p) ty_symbols -> unit = + fun sep symbols -> match symbols with + | TNil -> () + | TCns (symbol, symbols) -> + fprintf ppf "%t%a" sep print_symbol symbol; + fold (fun ppf -> fprintf ppf ";@ ") symbols in + let () = fold (fun ppf -> ()) symbols in fprintf ppf "@]" -and print_level ppf pp_print_space rules = +and print_level : type s. _ -> _ -> s ex_symbols list -> _ = + fun ppf pp_print_space rules -> fprintf ppf "@[[ "; let _ = List.fold_left - (fun sep rule -> + (fun sep (ExS rule) -> fprintf ppf "%t%a" sep print_rule rule; fun ppf -> fprintf ppf "%a| " pp_print_space ()) (fun ppf -> ()) rules @@ -658,7 +729,7 @@ let print_levels ppf elev = List.fold_left (fun sep lev -> let rules = - List.map (fun t -> Sself :: t) (flatten_tree lev.lsuffix) @ + List.map (fun (ExS t) -> ExS (TCns (Sself, t))) (flatten_tree lev.lsuffix) @ flatten_tree lev.lprefix in fprintf ppf "%t@[" sep; @@ -694,21 +765,32 @@ let loc_of_token_interval bp ep = else let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2 -let name_of_symbol entry = +let name_of_symbol : type s a. s ty_entry -> (s, a) ty_symbol -> string = + fun entry -> function Snterm e -> "[" ^ e.ename ^ "]" | Snterml (e, l) -> "[" ^ e.ename ^ " level " ^ l ^ "]" - | Sself | Snext -> "[" ^ entry.ename ^ "]" + | Sself -> "[" ^ entry.ename ^ "]" + | Snext -> "[" ^ entry.ename ^ "]" | Stoken tok -> egram.glexer.Plexing.tok_text tok | _ -> "???" -let rec get_token_list entry rev_tokl last_tok tree = +type ('r, 'f) tok_list = +| TokNil : ('f, 'f) tok_list +| TokCns : ('r, 'f) tok_list -> (string -> 'r, 'f) tok_list + +type ('s, 'f) tok_tree = TokTree : ('s, string -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree + +let rec get_token_list : type s r f. + s ty_entry -> _ -> _ -> _ -> (r, f) tok_list -> (s, string -> r) ty_tree -> (_ * _ * _ * (s, f) tok_tree) option = + fun entry first_tok rev_tokl last_tok pf tree -> match tree with Node {node = Stoken tok; son = son; brother = DeadEnd} -> - get_token_list entry (last_tok :: rev_tokl) tok son - | _ -> if rev_tokl = [] then None else Some (rev_tokl, last_tok, tree) + get_token_list entry first_tok (last_tok :: rev_tokl) tok (TokCns pf) son + | _ -> if rev_tokl = [] then None else Some (first_tok, rev_tokl, last_tok, TokTree (tree, pf)) -let rec name_of_symbol_failed entry = +let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ = + fun entry -> function | Slist0 s -> name_of_symbol_failed entry s | Slist0sep (s, _, _) -> name_of_symbol_failed entry s @@ -717,12 +799,13 @@ let rec name_of_symbol_failed entry = | Sopt s -> name_of_symbol_failed entry s | Stree t -> name_of_tree_failed entry t | s -> name_of_symbol entry s -and name_of_tree_failed entry = +and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ = + fun entry -> function Node {node = s; brother = bro; son = son} -> let tokl = match s with - Stoken tok -> get_token_list entry [] tok son + Stoken tok -> get_token_list entry tok [] tok TokNil son | _ -> None in begin match tokl with @@ -739,7 +822,7 @@ and name_of_tree_failed entry = | Node _ -> txt ^ " or " ^ name_of_tree_failed entry bro in txt - | Some (rev_tokl, last_tok, son) -> + | Some (_, rev_tokl, last_tok, _) -> List.fold_left (fun s tok -> (if s = "" then "" else s ^ " ") ^ @@ -748,7 +831,7 @@ and name_of_tree_failed entry = end | DeadEnd | LocAct (_, _) -> "???" -let tree_failed entry prev_symb_result prev_symb tree = +let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, a) ty_symbol) tree = let txt = name_of_tree_failed entry tree in let txt = match prev_symb with @@ -759,7 +842,7 @@ let tree_failed entry prev_symb_result prev_symb tree = let txt1 = name_of_symbol_failed entry s in txt1 ^ " or " ^ txt ^ " expected" | Slist0sep (s, sep, _) -> - begin match Obj.magic prev_symb_result with + begin match prev_symb_result with [] -> let txt1 = name_of_symbol_failed entry s in txt1 ^ " or " ^ txt ^ " expected" @@ -768,7 +851,7 @@ let tree_failed entry prev_symb_result prev_symb tree = txt1 ^ " or " ^ txt ^ " expected" end | Slist1sep (s, sep, _) -> - begin match Obj.magic prev_symb_result with + begin match prev_symb_result with [] -> let txt1 = name_of_symbol_failed entry s in txt1 ^ " or " ^ txt ^ " expected" @@ -776,7 +859,8 @@ let tree_failed entry prev_symb_result prev_symb tree = let txt1 = name_of_symbol_failed entry sep in txt1 ^ " or " ^ txt ^ " expected" end - | Sopt _ | Stree _ -> txt ^ " expected" + | Sopt _ -> txt ^ " expected" + | Stree _ -> txt ^ " expected" | _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb in txt ^ " (in [" ^ entry.ename ^ "])" @@ -801,28 +885,33 @@ let level_number entry lab = Dlevels elev -> lookup 0 elev | Dparser _ -> raise Not_found -let rec top_symb entry = +let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol = + fun entry -> function - Sself | Snext -> Snterm entry + Sself -> Snterm entry + | Snext -> Snterm entry | Snterml (e, _) -> Snterm e | Slist1sep (s, sep, b) -> Slist1sep (top_symb entry s, sep, b) | _ -> raise Stream.Failure -let entry_of_symb entry = +let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry = + fun entry -> function - Sself | Snext -> entry + Sself -> entry + | Snext -> entry | Snterm e -> e | Snterml (e, _) -> e | _ -> raise Stream.Failure -let top_tree entry = +let top_tree : type s a. s ty_entry -> (s, a) ty_tree -> (s, a) ty_tree = + fun entry -> function Node {node = s; brother = bro; son = son} -> Node {node = top_symb entry s; brother = bro; son = son} | 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 fun a -> p strm else raise Stream.Failure let continue entry bp a s son p1 (strm__ : _ Stream.t) = @@ -831,7 +920,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) + fun _ -> act a let do_recover parser_of_tree entry nlevn alevn bp a s son (strm__ : _ Stream.t) = @@ -869,27 +958,28 @@ let call_and_push ps al strm = let token_ematch gram tok = let tematch = gram.glexer.Plexing.tok_match tok in - fun tok -> Obj.repr (tematch tok : string) + fun tok -> tematch tok -let rec parser_of_tree entry nlevn alevn = +let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> r parser_t = + fun entry nlevn alevn -> function DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure) | LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act) | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} -> (fun (strm__ : _ Stream.t) -> - let a = entry.estart alevn strm__ in app act a) + let a = entry.estart alevn strm__ in act a) | Node {node = Sself; son = LocAct (act, _); brother = bro} -> let p2 = parser_of_tree entry nlevn alevn bro in (fun (strm__ : _ Stream.t) -> match try Some (entry.estart alevn strm__) with Stream.Failure -> None with - Some a -> app act a + Some a -> act a | _ -> p2 strm__) | Node {node = s; son = son; brother = DeadEnd} -> let tokl = match s with - Stoken tok -> get_token_list entry [] tok son + Stoken tok -> get_token_list entry tok [] tok TokNil son | _ -> None in begin match tokl with @@ -905,19 +995,20 @@ let rec parser_of_tree entry nlevn alevn = Stream.Failure -> raise (Stream.Error (tree_failed entry a s son)) in - app act a) - | Some (rev_tokl, last_tok, son) -> + act a) + | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) -> + let s = Stoken first_tok in let lt = Stoken last_tok in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn lt son in - parser_of_token_list entry s son p1 + parser_of_token_list entry s son pf p1 (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl last_tok end | Node {node = s; son = son; brother = bro} -> let tokl = match s with - Stoken tok -> get_token_list entry [] tok son + Stoken tok -> get_token_list entry tok [] tok TokNil son | _ -> None in match tokl with @@ -933,45 +1024,50 @@ let rec parser_of_tree entry nlevn alevn = begin match (try Some (p1 bp a strm) with Stream.Failure -> None) with - Some act -> app act a + Some act -> act a | None -> raise (Stream.Error (tree_failed entry a s son)) end | None -> p2 strm) - | Some (rev_tokl, last_tok, son) -> + | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) -> let lt = Stoken last_tok in let p2 = parser_of_tree entry nlevn alevn bro in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn lt son in let p1 = - parser_of_token_list entry lt son p1 p2 rev_tokl last_tok + parser_of_token_list entry lt son pf p1 p2 rev_tokl last_tok in fun (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> p2 strm__ -and parser_cont p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) = +and parser_cont : type s a r. + (a -> r) parser_t -> s ty_entry -> int -> int -> (s, a) ty_symbol -> (s, a -> r) ty_tree -> int -> a -> (a -> r) parser_t = + fun p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> recover parser_of_tree entry nlevn alevn bp a s son strm__ -and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = - let plast = +and parser_of_token_list : type s r f. + s ty_entry -> (s, string) ty_symbol -> (s, string -> r) ty_tree -> + (r, f) tok_list -> (int -> string -> (string -> r) parser_t) -> f parser_t -> _ -> _ -> f parser_t = + fun entry s son pf p1 p2 rev_tokl last_tok -> + let plast : r parser_t = let n = List.length rev_tokl + 1 in let tematch = token_ematch egram last_tok in let ps strm = match peek_nth n strm with Some tok -> let r = tematch tok in - for _i = 1 to n do Stream.junk strm done; Obj.repr r + for _i = 1 to n do Stream.junk strm done; r | None -> raise Stream.Failure in fun (strm : _ Stream.t) -> let bp = Stream.count strm in let a = ps strm in match try Some (p1 bp a strm) with Stream.Failure -> None with - Some act -> app act a + Some act -> act a | None -> raise (Stream.Error (tree_failed entry a s son)) in - match List.rev rev_tokl with - [] -> (fun (strm__ : _ Stream.t) -> plast strm__) - | tok :: tokl -> + match List.rev rev_tokl, pf with + [], TokNil -> (fun (strm__ : _ Stream.t) -> plast strm__) + | tok :: tokl, TokCns pf -> let tematch = token_ematch egram tok in let ps strm = match peek_nth 1 strm with @@ -979,25 +1075,30 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = | None -> raise Stream.Failure in let p1 = - let rec loop n = - function - [] -> plast - | tok :: tokl -> + let rec loop : type s f. _ -> _ -> (s, f) tok_list -> (string -> s) parser_t -> (string -> f) parser_t = + fun n tokl pf plast -> + match tokl, pf with + [], TokNil -> plast + | tok :: tokl, TokCns pf -> let tematch = token_ematch egram tok in let ps strm = match peek_nth n strm with Some tok -> tematch tok | None -> raise Stream.Failure in - let p1 = loop (n + 1) tokl in + let p1 = loop (n + 1) tokl pf (Obj.magic plast) in (* FIXME *) fun (strm__ : _ Stream.t) -> - let a = ps strm__ in let act = p1 strm__ in app act a + let a = ps strm__ in let act = p1 strm__ in (Obj.magic act a) (* FIXME *) + | _ -> assert false in - loop 2 tokl + loop 2 tokl pf plast in fun (strm__ : _ Stream.t) -> - let a = ps strm__ in let act = p1 strm__ in app act a -and parser_of_symbol entry nlevn = + let a = ps strm__ in let act = p1 strm__ in act a + | _ -> assert false +and parser_of_symbol : type s a. + s ty_entry -> int -> (s, a) ty_symbol -> a parser_t = + fun entry nlevn -> function | Slist0 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in @@ -1007,7 +1108,7 @@ and parser_of_symbol entry nlevn = | _ -> al in (fun (strm__ : _ Stream.t) -> - let a = loop [] strm__ in Obj.repr (List.rev a)) + let a = loop [] strm__ in List.rev a) | Slist0sep (symb, sep, false) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -1024,8 +1125,8 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> match try Some (ps [] strm__) with Stream.Failure -> None with - Some al -> let a = kont al strm__ in Obj.repr (List.rev a) - | _ -> Obj.repr []) + Some al -> let a = kont al strm__ in List.rev a + | _ -> []) | Slist0sep (symb, sep, true) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -1042,8 +1143,8 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> match try Some (ps [] strm__) with Stream.Failure -> None with - Some al -> let a = kont al strm__ in Obj.repr (List.rev a) - | _ -> Obj.repr []) + Some al -> let a = kont al strm__ in List.rev a + | _ -> []) | Slist1 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in let rec loop al (strm__ : _ Stream.t) = @@ -1053,7 +1154,7 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> let al = ps [] strm__ in - let a = loop al strm__ in Obj.repr (List.rev a)) + let a = loop al strm__ in List.rev a) | Slist1sep (symb, sep, false) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -1075,7 +1176,7 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> let al = ps [] strm__ in - let a = kont al strm__ in Obj.repr (List.rev a)) + let a = kont al strm__ in List.rev a) | Slist1sep (symb, sep, true) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -1098,33 +1199,37 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> let al = ps [] strm__ in - let a = kont al strm__ in Obj.repr (List.rev a)) + let a = kont al strm__ in List.rev a) | Sopt s -> let ps = parser_of_symbol entry nlevn s in (fun (strm__ : _ Stream.t) -> match try Some (ps strm__) with Stream.Failure -> None with - Some a -> Obj.repr (Some a) - | _ -> Obj.repr None) + Some a -> Some a + | _ -> None) | Stree t -> let pt = parser_of_tree entry 1 0 t in (fun (strm__ : _ Stream.t) -> let bp = Stream.count strm__ in let a = pt strm__ in let ep = Stream.count strm__ in - let loc = loc_of_token_interval bp ep in app a loc) + let loc = loc_of_token_interval bp ep in a loc) | Snterm e -> (fun (strm__ : _ Stream.t) -> e.estart 0 strm__) | Snterml (e, l) -> (fun (strm__ : _ Stream.t) -> e.estart (level_number e l) strm__) | Sself -> (fun (strm__ : _ Stream.t) -> entry.estart 0 strm__) | Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__) | Stoken tok -> parser_of_token entry tok -and parser_of_token entry tok = +and parser_of_token : type s. + s ty_entry -> Plexing.pattern -> string parser_t = + fun entry tok -> let f = egram.glexer.Plexing.tok_match tok in fun strm -> match Stream.peek strm with - Some tok -> let r = f tok in Stream.junk strm; Obj.repr r + Some tok -> let r = f tok in Stream.junk strm; r | None -> raise Stream.Failure -and parse_top_symb entry symb = parser_of_symbol entry 0 (top_symb entry symb) +and parse_top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a parser_t = + fun entry symb -> + parser_of_symbol entry 0 (top_symb entry symb) let rec start_parser_of_levels entry clevn = function @@ -1154,7 +1259,7 @@ let rec start_parser_of_levels entry clevn = let bp = Stream.count strm__ in let act = p2 strm__ in let ep = Stream.count strm__ in - let a = app act (loc_of_token_interval bp ep) in + let a = act (loc_of_token_interval bp ep) in entry.econtinue levn bp a strm) | _ -> fun levn strm -> @@ -1165,7 +1270,7 @@ let rec start_parser_of_levels entry clevn = match try Some (p2 strm__) with Stream.Failure -> None with Some act -> let ep = Stream.count strm__ in - let a = app act (loc_of_token_interval bp ep) in + let a = act (loc_of_token_interval bp ep) in entry.econtinue levn bp a strm | _ -> p1 levn strm__ @@ -1191,7 +1296,7 @@ let rec continue_parser_of_levels entry clevn = Stream.Failure -> let act = p2 strm__ in let ep = Stream.count strm__ in - let a = app act a (loc_of_token_interval bp ep) in + let a = act a (loc_of_token_interval bp ep) in entry.econtinue levn bp a strm let continue_parser_of_entry entry = @@ -1295,35 +1400,35 @@ let clear_entry e = {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf} module Entry = struct - type 'a e = g_entry + type 'a e = 'a ty_entry let create n = { ename = n; estart = empty_entry n; econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} let parse (e : 'a e) p : 'a = - Obj.magic (parse_parsable e p : Obj.t) + parse_parsable e p let parse_token_stream (e : 'a e) ts : 'a = - Obj.magic (e.estart 0 ts : Obj.t) + e.estart 0 ts let name e = e.ename let of_parser n (p : te Stream.t -> 'a) : 'a e = { ename = n; - estart = (fun _ -> (Obj.magic p : te Stream.t -> Obj.t)); + estart = (fun _ -> p); econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); - edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)} + edesc = Dparser p} let print ppf e = fprintf ppf "%a@." print_entry e end - let s_nterm e = Tnterm e - let s_nterml e l = Tnterml (e, l) - let s_list0 s = Tlist0 s - let s_list0sep s sep b = Tlist0sep (s, sep, b) - let s_list1 s = Tlist1 s - let s_list1sep s sep b = Tlist1sep (s, sep, b) - let s_opt s = Topt s - let s_self = Tself - let s_next = Tnext - let s_token tok = Ttoken tok + let s_nterm e = Snterm e + let s_nterml e l = Snterml (e, l) + let s_list0 s = Slist0 s + let s_list0sep s sep b = Slist0sep (s, sep, b) + let s_list1 s = Slist1 s + let s_list1sep s sep b = Slist1sep (s, sep, b) + let s_opt s = Sopt s + let s_self = Sself + let s_next = Snext + let s_token tok = Stoken tok let s_rules ~warning (t : 'a ty_production list) = srules ~warning t let r_stop = TStop let r_next r s = TNext (r, s) @@ -1337,6 +1442,8 @@ let clear_entry e = (string option * Gramext.g_assoc option * 'a ty_production list) list) = extend_entry ~warning e pos r - let safe_delete_rule e r = delete_rule e (u_rule r []) + let safe_delete_rule e r = + let AnyS (symbols, _) = get_symbols r in + delete_rule e symbols end -- cgit v1.2.3