From 38020166be0d3533ca8060be1e09192a5ed3c6e7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Nov 2018 18:32:07 +0100
Subject: Remove Smeta constructor in Gramlib.

This constructor was only used by meta-level macros that are not used and
serve no purpose in the grammar engine.
---
 gramlib/gramext.ml  |  7 +------
 gramlib/gramext.mli |  1 -
 gramlib/grammar.ml  | 33 +--------------------------------
 3 files changed, 2 insertions(+), 39 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 8960d4f257..bd2631f747 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -28,7 +28,6 @@ and 'te g_level =
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
     Sfacto of 'te g_symbol
-  | Smeta of string * 'te g_symbol list * Obj.t
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
@@ -70,7 +69,7 @@ let rec derive_eps =
   | Sfacto s -> derive_eps s
   | Stree t -> tree_derive_eps t
   | Svala (_, s) -> derive_eps s
-  | Smeta (_, _, _) | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
+  | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
     Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
       false
 and tree_derive_eps =
@@ -204,7 +203,6 @@ and token_exists_in_tree f =
 and token_exists_in_symbol f =
   function
     Sfacto sy -> token_exists_in_symbol f sy
-  | Smeta (_, syl, _) -> List.exists (token_exists_in_symbol f) syl
   | Slist0 sy -> token_exists_in_symbol f sy
   | Slist0sep (sy, sep, _) ->
       token_exists_in_symbol f sy || token_exists_in_symbol f sep
@@ -342,7 +340,6 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
           failwith "Grammar.extend error"
         end
   | Sfacto s -> check_gram entry s
-  | Smeta (_, sl, _) -> List.iter (check_gram entry) sl
   | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist0 s -> check_gram entry s
@@ -372,7 +369,6 @@ let insert_tokens gram symbols =
   let rec insert =
     function
       Sfacto s -> insert s
-    | Smeta (_, sl, _) -> List.iter insert sl
     | Slist0 s -> insert s
     | Slist1 s -> insert s
     | Slist0sep (s, t, _) -> insert s; insert t
@@ -508,7 +504,6 @@ let rec decr_keyw_use gram =
           gram.glexer.Plexing.tok_removing tok
         end
   | Sfacto s -> decr_keyw_use gram s
-  | Smeta (_, sl, _) -> List.iter (decr_keyw_use gram) sl
   | 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
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index a76b7da9a2..f012d85bd0 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -26,7 +26,6 @@ and 'te g_level =
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
     Sfacto of 'te g_symbol
-  | Smeta of string * 'te g_symbol list * Obj.t
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 04ec1049ed..b38ce59fad 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -42,7 +42,6 @@ let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s)
 let rec print_symbol ppf =
   function
     Sfacto s -> print_symbol ppf s
-  | Smeta (n, sl, _) -> print_meta ppf n sl
   | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s
   | Slist0sep (s, t, osep) ->
       fprintf ppf "LIST0 %a SEP %a%s" print_symbol1 s print_symbol1 t
@@ -61,20 +60,6 @@ let rec print_symbol ppf =
         print_str l
   | Snterm _ | Snext | Sself | Scut | Stoken _ | Stree _ as s ->
       print_symbol1 ppf s
-and print_meta ppf n sl =
-  let rec loop i =
-    function
-      [] -> ()
-    | s :: sl ->
-        let j =
-          try String.index_from n i ' ' with Not_found -> String.length n
-        in
-        fprintf ppf "%s %a" (String.sub n i (j - i)) print_symbol1 s;
-        if sl = [] then ()
-        else
-          begin fprintf ppf " "; loop (min (j + 1) (String.length n)) sl end
-  in
-  loop 0 sl
 and print_symbol1 ppf =
   function
     Sfacto s -> print_symbol1 ppf s
@@ -85,7 +70,7 @@ 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)
-  | Smeta (_, _, _) | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) |
+  | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) |
     Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Sflag _ | Stoken _ |
     Svala (_, _) as s ->
       fprintf ppf "(%a)" print_symbol s
@@ -178,7 +163,6 @@ let rec name_of_symbol_failed entry =
   | Sflag s -> name_of_symbol_failed entry s
   | Stree t -> name_of_tree_failed entry t
   | Svala (_, s) -> name_of_symbol_failed entry s
-  | Smeta (_, s :: _, _) -> name_of_symbol_failed entry s
   | s -> name_of_symbol entry s
 and name_of_tree_failed entry =
   function
@@ -593,12 +577,6 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok =
 and parser_of_symbol entry nlevn =
   function
     Sfacto s -> parser_of_symbol entry nlevn s
-  | Smeta (_, symbl, act) ->
-      let act = Obj.magic act entry symbl in
-      Obj.magic
-        (List.fold_left
-           (fun act symb -> Obj.magic act (parser_of_symbol entry nlevn symb))
-           act symbl)
   | Slist0 s ->
       let ps = call_and_push (parser_of_symbol entry nlevn s) in
       let rec loop al (strm__ : _ Stream.t) =
@@ -970,7 +948,6 @@ let find_entry e s =
       Sfacto s -> find_symbol s
     | Snterm e -> if e.ename = s then Some e else None
     | Snterml (e, _) -> if e.ename = s then Some e else None
-    | Smeta (_, sl, _) -> find_symbol_list sl
     | Slist0 s -> find_symbol s
     | Slist0sep (s, _, _) -> find_symbol s
     | Slist1 s -> find_symbol s
@@ -980,14 +957,6 @@ let find_entry e s =
     | Stree t -> find_tree t
     | Svala (_, s) -> find_symbol s
     | Sself | Snext | Scut | Stoken _ -> None
-  and find_symbol_list =
-    function
-      s :: sl ->
-        begin match find_symbol s with
-          None -> find_symbol_list sl
-        | x -> x
-        end
-    | [] -> None
   and find_tree =
     function
       Node {node = s; brother = bro; son = son} ->
-- 
cgit v1.2.3


From 7cb44913c4d3ba8ced49e00bc61a53ee6d95f213 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Nov 2018 18:35:29 +0100
Subject: Remove the Svala constructor from Gramlib.

It is only used in strict mode, which makes no sense for Coq grammar.
---
 gramlib/gramext.ml  |  17 ---------
 gramlib/gramext.mli |   1 -
 gramlib/grammar.ml  | 106 ++++++++--------------------------------------------
 gramlib/grammar.mli |   2 -
 gramlib/ploc.ml     |   4 --
 gramlib/ploc.mli    |   7 ----
 6 files changed, 15 insertions(+), 122 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index bd2631f747..3b2c3de760 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -41,7 +41,6 @@ and 'te g_symbol =
   | Scut
   | Stoken of Plexing.pattern
   | Stree of 'te g_tree
-  | Svala of string list * 'te g_symbol
 and g_action = Obj.t
 and 'te g_tree =
     Node of 'te g_node
@@ -68,7 +67,6 @@ let rec derive_eps =
   | Sopt _ | Sflag _ -> true
   | Sfacto s -> derive_eps s
   | Stree t -> tree_derive_eps t
-  | Svala (_, s) -> derive_eps s
   | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
     Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
       false
@@ -91,7 +89,6 @@ let rec eq_symbol s1 s2 =
       eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2
   | Sflag s1, Sflag s2 -> eq_symbol s1 s2
   | Sopt s1, Sopt s2 -> eq_symbol s1 s2
-  | Svala (ls1, s1), Svala (ls2, s2) -> ls1 = ls2 && eq_symbol s1 s2
   | Stree _, Stree _ -> false
   | Sfacto (Stree t1), Sfacto (Stree t2) ->
       (* The only goal of the node 'Sfacto' is to allow tree comparison
@@ -111,16 +108,6 @@ let rec eq_symbol s1 s2 =
   | _ -> s1 = s2
 
 let is_before s1 s2 =
-  let s1 =
-    match s1 with
-      Svala (_, s) -> s
-    | _ -> s1
-  in
-  let s2 =
-    match s2 with
-      Svala (_, s) -> s
-    | _ -> s2
-  in
   match s1, s2 with
     Stoken ("ANY", _), _ -> false
   | _, Stoken ("ANY", _) -> true
@@ -213,7 +200,6 @@ and token_exists_in_symbol f =
   | Sflag sy -> token_exists_in_symbol f sy
   | Stoken tok -> f tok
   | Stree t -> token_exists_in_tree f t
-  | Svala (_, sy) -> token_exists_in_symbol f sy
   | Snterm _ | Snterml (_, _) | Snext | Sself | Scut -> false
 
 let insert_level entry_name e1 symbols action slev =
@@ -347,7 +333,6 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
   | Sopt s -> check_gram entry s
   | Sflag s -> check_gram entry s
   | Stree t -> tree_check_gram entry t
-  | Svala (_, s) -> check_gram entry s
   | Snext | Sself | Scut | Stoken _ -> ()
 and tree_check_gram entry =
   function
@@ -376,7 +361,6 @@ let insert_tokens gram symbols =
     | Sopt s -> insert s
     | Sflag s -> insert s
     | Stree t -> tinsert t
-    | Svala (_, s) -> insert s
     | Stoken ("ANY", _) -> ()
     | Stoken tok ->
         gram.glexer.Plexing.tok_using tok;
@@ -511,7 +495,6 @@ let rec decr_keyw_use gram =
   | Sopt s -> decr_keyw_use gram s
   | Sflag s -> decr_keyw_use gram s
   | Stree t -> decr_keyw_use_in_tree gram t
-  | Svala (_, s) -> decr_keyw_use gram s
   | Sself | Snext | Scut | Snterm _ | Snterml (_, _) -> ()
 and decr_keyw_use_in_tree gram =
   function
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index f012d85bd0..eb2ea7576b 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -39,7 +39,6 @@ and 'te g_symbol =
   | Scut
   | Stoken of Plexing.pattern
   | Stree of 'te g_tree
-  | Svala of string list * 'te g_symbol
 and g_action = Obj.t
 and 'te g_tree =
     Node of 'te g_node
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index b38ce59fad..cdc3945323 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -54,7 +54,6 @@ let rec print_symbol ppf =
   | Sflag s -> fprintf ppf "FLAG %a" print_symbol1 s
   | Stoken (con, prm) when con <> "" && prm <> "" ->
       fprintf ppf "%s@ %a" con print_str prm
-  | Svala (_, s) -> fprintf ppf "V %a" print_symbol s
   | Snterml (e, l) ->
       fprintf ppf "%s%s@ LEVEL@ %a" e.ename (if e.elocal then "*" else "")
         print_str l
@@ -71,8 +70,7 @@ and print_symbol1 ppf =
   | Stoken (con, "") -> pp_print_string ppf con
   | Stree t -> print_level ppf pp_print_space (flatten_tree t)
   | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) |
-    Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Sflag _ | Stoken _ |
-    Svala (_, _) as s ->
+    Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Sflag _ | Stoken _ as s ->
       fprintf ppf "(%a)" print_symbol s
 and print_rule ppf symbols =
   fprintf ppf "@[<hov 0>";
@@ -147,9 +145,7 @@ let name_of_symbol entry =
 let rec get_token_list entry rev_tokl last_tok tree =
   match tree with
     Node {node = Stoken tok; son = son; brother = DeadEnd} ->
-      get_token_list entry (last_tok :: rev_tokl) (tok, None) son
-  | Node {node = Svala (ls, Stoken tok); son = son; brother = DeadEnd} ->
-      get_token_list entry (last_tok :: rev_tokl) (tok, Some ls) son
+      get_token_list entry (last_tok :: rev_tokl) tok son
   | _ -> if rev_tokl = [] then None else Some (rev_tokl, last_tok, tree)
 
 let rec name_of_symbol_failed entry =
@@ -162,15 +158,13 @@ let rec name_of_symbol_failed entry =
   | Sopt s -> name_of_symbol_failed entry s
   | Sflag s -> name_of_symbol_failed entry s
   | Stree t -> name_of_tree_failed entry t
-  | Svala (_, s) -> name_of_symbol_failed entry s
   | s -> name_of_symbol entry s
 and name_of_tree_failed entry =
   function
     Node {node = s; brother = bro; son = son} ->
       let tokl =
         match s with
-          Stoken tok -> get_token_list entry [] (tok, None) son
-        | Svala (ls, Stoken tok) -> get_token_list entry [] (tok, Some ls) son
+          Stoken tok -> get_token_list entry [] tok son
         | _ -> None
       in
       begin match tokl with
@@ -189,7 +183,7 @@ and name_of_tree_failed entry =
           txt
       | Some (rev_tokl, last_tok, son) ->
           List.fold_left
-            (fun s (tok, _) ->
+            (fun s tok ->
                (if s = "" then "" else s ^ " ") ^
                entry.egram.glexer.Plexing.tok_text tok)
             "" (List.rev (last_tok :: rev_tokl))
@@ -302,7 +296,7 @@ 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 _ | Sflag _ | Stree _ | Svala (_, _) -> txt ^ " expected"
+    | Sopt _ | Sflag _ | Stree _ -> txt ^ " expected"
     | _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb
   in
   if !error_verbose then
@@ -410,29 +404,9 @@ let call_and_push ps al strm =
   let a = ps strm in
   let al = if !item_skipped then al else a :: al in item_skipped := false; al
 
-let token_ematch gram (tok, vala) =
+let token_ematch gram tok =
   let tematch = gram.glexer.Plexing.tok_match tok in
-  match vala with
-    Some al ->
-      let pa =
-        match al with
-          [] ->
-            let t = "V " ^ fst tok in gram.glexer.Plexing.tok_match (t, "")
-        | al ->
-            let rec loop =
-              function
-                a :: al ->
-                  let pa = gram.glexer.Plexing.tok_match ("V", a) in
-                  let pal = loop al in
-                  (fun tok -> try pa tok with Stream.Failure -> pal tok)
-              | [] -> fun tok -> raise Stream.Failure
-            in
-            loop al
-      in
-      (fun tok ->
-         try Obj.repr (Ploc.VaAnt (Obj.magic (pa tok : string))) with
-           Stream.Failure -> Obj.repr (Ploc.VaVal (tematch tok)))
-  | None -> fun tok -> Obj.repr (tematch tok : string)
+  fun tok -> Obj.repr (tematch tok : string)
 
 let rec parser_of_tree entry nlevn alevn =
   function
@@ -454,8 +428,7 @@ let rec parser_of_tree entry nlevn alevn =
   | Node {node = s; son = son; brother = DeadEnd} ->
       let tokl =
         match s with
-          Stoken tok -> get_token_list entry [] (tok, None) son
-        | Svala (ls, Stoken tok) -> get_token_list entry [] (tok, Some ls) son
+          Stoken tok -> get_token_list entry [] tok son
         | _ -> None
       in
       begin match tokl with
@@ -472,24 +445,18 @@ let rec parser_of_tree entry nlevn alevn =
                    raise (Stream.Error (tree_failed entry a s son))
              in
              app act a)
-      | Some (rev_tokl, (last_tok, svala), son) ->
-          let lt =
-            let t = Stoken last_tok in
-            match svala with
-              Some l -> Svala (l, t)
-            | None -> t
-          in
+      | Some (rev_tokl, last_tok, son) ->
+          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
             (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl
-            (last_tok, svala)
+            last_tok
       end
   | Node {node = s; son = son; brother = bro} ->
       let tokl =
         match s with
-          Stoken tok -> get_token_list entry [] (tok, None) son
-        | Svala (ls, Stoken tok) -> get_token_list entry [] (tok, Some ls) son
+          Stoken tok -> get_token_list entry [] tok son
         | _ -> None
       in
       match tokl with
@@ -509,18 +476,13 @@ let rec parser_of_tree entry nlevn alevn =
                  | None -> raise (Stream.Error (tree_failed entry a s son))
                  end
              | None -> p2 strm)
-      | Some (rev_tokl, (last_tok, vala), son) ->
-          let lt =
-            let t = Stoken last_tok in
-            match vala with
-              Some ls -> Svala (ls, t)
-            | None -> t
-          in
+      | Some (rev_tokl, last_tok, son) ->
+          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, vala)
+            parser_of_token_list entry lt son p1 p2 rev_tokl last_tok
           in
           fun (strm__ : _ Stream.t) ->
             try p1 strm__ with Stream.Failure -> p2 strm__
@@ -696,40 +658,6 @@ and parser_of_symbol entry nlevn =
          let a = pt strm__ in
          let ep = Stream.count strm__ in
          let loc = loc_of_token_interval bp ep in app a loc)
-  | Svala (al, s) ->
-      let pa =
-        match al with
-          [] ->
-            let t =
-              match s with
-                Sflag _ -> Some "V FLAG"
-              | Sopt _ -> Some "V OPT"
-              | Slist0 _ | Slist0sep (_, _, _) -> Some "V LIST"
-              | Slist1 _ | Slist1sep (_, _, _) -> Some "V LIST"
-              | Stoken (con, "") -> Some ("V " ^ con)
-              | _ -> None
-            in
-            begin match t with
-              Some t -> parser_of_token entry (t, "")
-            | None -> fun (strm__ : _ Stream.t) -> raise Stream.Failure
-            end
-        | al ->
-            let rec loop =
-              function
-                a :: al ->
-                  let pa = parser_of_token entry ("V", a) in
-                  let pal = loop al in
-                  (fun (strm__ : _ Stream.t) ->
-                     try pa strm__ with Stream.Failure -> pal strm__)
-              | [] -> fun (strm__ : _ Stream.t) -> raise Stream.Failure
-            in
-            loop al
-      in
-      let ps = parser_of_symbol entry nlevn s in
-      (fun (strm__ : _ Stream.t) ->
-         match try Some (pa strm__) with Stream.Failure -> None with
-           Some a -> Obj.repr (Ploc.VaAnt (Obj.magic a : string))
-         | _ -> let a = ps strm__ in Obj.repr (Ploc.VaVal a))
   | Snterm e -> (fun (strm__ : _ Stream.t) -> e.estart 0 strm__)
   | Snterml (e, l) ->
       (fun (strm__ : _ Stream.t) -> e.estart (level_number e l) strm__)
@@ -955,7 +883,6 @@ let find_entry e s =
     | Sopt s -> find_symbol s
     | Sflag s -> find_symbol s
     | Stree t -> find_tree t
-    | Svala (_, s) -> find_symbol s
     | Sself | Snext | Scut | Stoken _ -> None
   and find_tree =
     function
@@ -1081,8 +1008,6 @@ module type S =
     val s_next : ('self, 'self) ty_symbol
     val s_token : Plexing.pattern -> ('self, string) ty_symbol
     val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
-    val s_vala :
-      string list -> ('self, 'a) ty_symbol -> ('self, 'a Ploc.vala) ty_symbol
     val r_stop : ('self, 'r, 'r) ty_rule
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
@@ -1169,7 +1094,6 @@ module GMake (L : GLexerType) =
     let s_next = Snext
     let s_token tok = Stoken tok
     let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t)
-    let s_vala sl s = Svala (sl, s)
     let r_stop = []
     let r_next r s = r @ [s]
     let r_cut r = r @ [Scut]
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 54b7eb5539..7bbf799938 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -129,8 +129,6 @@ module type S =
     val s_next : ('self, 'self) ty_symbol
     val s_token : Plexing.pattern -> ('self, string) ty_symbol
     val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
-    val s_vala :
-      string list -> ('self, 'a) ty_symbol -> ('self, 'a Ploc.vala) ty_symbol
     val r_stop : ('self, 'r, 'r) ty_rule
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index cb71f72678..6aa7c1a2bb 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -170,7 +170,3 @@ let raise loc exc =
   match exc with
     Exc (_, _) -> raise exc
   | _ -> raise (Exc (loc, exc))
-
-type 'a vala =
-    VaAnt of string
-  | VaVal of 'a
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index d2ab62db06..afddefcd6e 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -108,13 +108,6 @@ val from_file : string -> t -> string * int * int * int
 
 (* pervasives *)
 
-type 'a vala =
-    VaAnt of string
-  | VaVal of 'a
-   (** Encloser of many abstract syntax tree nodes types, in "strict" mode.
-       This allow the system of antiquotations of abstract syntax tree
-       quotations to work when using the quotation kit [q_ast.cmo]. *)
-
 val call_with : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    (** [Ploc.call_with r v f a] sets the reference [r] to the value [v],
        then call [f a], and resets [r] to its initial value. If [f a] raises
-- 
cgit v1.2.3


From c7fc066129b9147a50e8a06e990f23becf5f9deb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Nov 2018 19:09:48 +0100
Subject: Remove the Sfacto constructor from Gramlib.

Used by rule factorisation in theory, but appears to be unused in Coq.
---
 gramlib/gramext.ml  | 21 ---------------------
 gramlib/gramext.mli |  1 -
 gramlib/grammar.ml  |  7 -------
 gramlib/grammar.mli |  1 -
 4 files changed, 30 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 3b2c3de760..de9b1e864c 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -27,7 +27,6 @@ and 'te g_level =
     lprefix : 'te g_tree }
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
-    Sfacto of 'te g_symbol
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
@@ -65,7 +64,6 @@ let rec derive_eps =
     Slist0 _ -> true
   | Slist0sep (_, _, _) -> true
   | Sopt _ | Sflag _ -> true
-  | Sfacto s -> derive_eps s
   | Stree t -> tree_derive_eps t
   | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
     Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
@@ -90,21 +88,6 @@ let rec eq_symbol s1 s2 =
   | Sflag s1, Sflag s2 -> eq_symbol s1 s2
   | Sopt s1, Sopt s2 -> eq_symbol s1 s2
   | Stree _, Stree _ -> false
-  | Sfacto (Stree t1), Sfacto (Stree t2) ->
-      (* The only goal of the node 'Sfacto' is to allow tree comparison
-         (therefore factorization) without looking at the semantic
-         actions; allow factorization of rules like "SV foo" which are
-         actually expanded into a tree. *)
-      let rec eq_tree t1 t2 =
-        match t1, t2 with
-          Node n1, Node n2 ->
-            eq_symbol n1.node n2.node && eq_tree n1.son n2.son &&
-            eq_tree n1.brother n2.brother
-        | LocAct (_, _), LocAct (_, _) -> true
-        | DeadEnd, DeadEnd -> true
-        | _ -> false
-      in
-      eq_tree t1 t2
   | _ -> s1 = s2
 
 let is_before s1 s2 =
@@ -189,7 +172,6 @@ and token_exists_in_tree f =
   | LocAct (_, _) | DeadEnd -> false
 and token_exists_in_symbol f =
   function
-    Sfacto sy -> token_exists_in_symbol f sy
   | Slist0 sy -> token_exists_in_symbol f sy
   | Slist0sep (sy, sep, _) ->
       token_exists_in_symbol f sy || token_exists_in_symbol f sep
@@ -325,7 +307,6 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
           flush stderr;
           failwith "Grammar.extend error"
         end
-  | Sfacto s -> check_gram entry s
   | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist0 s -> check_gram entry s
@@ -353,7 +334,6 @@ let get_initial entry =
 let insert_tokens gram symbols =
   let rec insert =
     function
-      Sfacto s -> insert s
     | Slist0 s -> insert s
     | Slist1 s -> insert s
     | Slist0sep (s, t, _) -> insert s; insert t
@@ -487,7 +467,6 @@ let rec decr_keyw_use gram =
           Hashtbl.remove gram.gtokens tok;
           gram.glexer.Plexing.tok_removing tok
         end
-  | Sfacto s -> decr_keyw_use gram s
   | 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
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index eb2ea7576b..ff59bae578 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -25,7 +25,6 @@ and 'te g_level =
     lprefix : 'te g_tree }
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
-    Sfacto of 'te g_symbol
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index cdc3945323..6e99861423 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -41,7 +41,6 @@ let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s)
 
 let rec print_symbol ppf =
   function
-    Sfacto s -> print_symbol ppf s
   | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s
   | Slist0sep (s, t, osep) ->
       fprintf ppf "LIST0 %a SEP %a%s" print_symbol1 s print_symbol1 t
@@ -61,7 +60,6 @@ let rec print_symbol ppf =
       print_symbol1 ppf s
 and print_symbol1 ppf =
   function
-    Sfacto s -> print_symbol1 ppf s
   | Snterm e -> fprintf ppf "%s%s" e.ename (if e.elocal then "*" else "")
   | Sself -> pp_print_string ppf "SELF"
   | Snext -> pp_print_string ppf "NEXT"
@@ -150,7 +148,6 @@ let rec get_token_list entry rev_tokl last_tok tree =
 
 let rec name_of_symbol_failed entry =
   function
-    Sfacto s -> name_of_symbol_failed entry s
   | Slist0 s -> name_of_symbol_failed entry s
   | Slist0sep (s, _, _) -> name_of_symbol_failed entry s
   | Slist1 s -> name_of_symbol_failed entry s
@@ -538,7 +535,6 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok =
         let a = ps strm__ in let act = p1 strm__ in app act a
 and parser_of_symbol entry nlevn =
   function
-    Sfacto s -> parser_of_symbol entry nlevn s
   | Slist0 s ->
       let ps = call_and_push (parser_of_symbol entry nlevn s) in
       let rec loop al (strm__ : _ Stream.t) =
@@ -873,7 +869,6 @@ let find_entry e s =
         | x -> x
   and find_symbol =
     function
-      Sfacto s -> find_symbol s
     | Snterm e -> if e.ename = s then Some e else None
     | Snterml (e, _) -> if e.ename = s then Some e else None
     | Slist0 s -> find_symbol s
@@ -991,7 +986,6 @@ module type S =
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
     type 'a ty_production
-    val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol
     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
@@ -1081,7 +1075,6 @@ module GMake (L : GLexerType) =
     type ('self, 'a) ty_symbol = te Gramext.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
-    let s_facto s = Sfacto s
     let s_nterm e = Snterm e
     let s_nterml e l = Snterml (e, l)
     let s_list0 s = Slist0 s
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 7bbf799938..e115b9df43 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -112,7 +112,6 @@ module type S =
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
     type 'a ty_production
-    val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol
     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
-- 
cgit v1.2.3


From 1dac644da31bb25dd4e36360e5eb3febd0d5e158 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Nov 2018 19:18:54 +0100
Subject: Remove the Sflag constructor from Gramlib.

It is just a wrapper around Sopt. I do not really understand why it is
hardwired in the entry AST.
---
 gramlib/gramext.ml  |  8 +-------
 gramlib/gramext.mli |  1 -
 gramlib/grammar.ml  | 15 ++-------------
 gramlib/grammar.mli |  1 -
 4 files changed, 3 insertions(+), 22 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index de9b1e864c..159070b2f2 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -34,7 +34,6 @@ and 'te g_symbol =
   | Slist1 of 'te g_symbol
   | Slist1sep of 'te g_symbol * 'te g_symbol * bool
   | Sopt of 'te g_symbol
-  | Sflag of 'te g_symbol
   | Sself
   | Snext
   | Scut
@@ -63,7 +62,7 @@ let rec derive_eps =
   function
     Slist0 _ -> true
   | Slist0sep (_, _, _) -> true
-  | Sopt _ | Sflag _ -> true
+  | Sopt _ -> true
   | Stree t -> tree_derive_eps t
   | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
     Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
@@ -85,7 +84,6 @@ let rec eq_symbol s1 s2 =
   | 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
-  | Sflag s1, Sflag s2 -> eq_symbol s1 s2
   | Sopt s1, Sopt s2 -> eq_symbol s1 s2
   | Stree _, Stree _ -> false
   | _ -> s1 = s2
@@ -179,7 +177,6 @@ and token_exists_in_symbol f =
   | Slist1sep (sy, sep, _) ->
       token_exists_in_symbol f sy || token_exists_in_symbol f sep
   | Sopt sy -> token_exists_in_symbol f sy
-  | Sflag sy -> token_exists_in_symbol f sy
   | Stoken tok -> f tok
   | Stree t -> token_exists_in_tree f t
   | Snterm _ | Snterml (_, _) | Snext | Sself | Scut -> false
@@ -312,7 +309,6 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
   | Slist0 s -> check_gram entry s
   | Slist1 s -> check_gram entry s
   | Sopt s -> check_gram entry s
-  | Sflag s -> check_gram entry s
   | Stree t -> tree_check_gram entry t
   | Snext | Sself | Scut | Stoken _ -> ()
 and tree_check_gram entry =
@@ -339,7 +335,6 @@ let insert_tokens gram symbols =
     | Slist0sep (s, t, _) -> insert s; insert t
     | Slist1sep (s, t, _) -> insert s; insert t
     | Sopt s -> insert s
-    | Sflag s -> insert s
     | Stree t -> tinsert t
     | Stoken ("ANY", _) -> ()
     | Stoken tok ->
@@ -472,7 +467,6 @@ let rec decr_keyw_use gram =
   | 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
-  | Sflag s -> decr_keyw_use gram s
   | Stree t -> decr_keyw_use_in_tree gram t
   | Sself | Snext | Scut | Snterm _ | Snterml (_, _) -> ()
 and decr_keyw_use_in_tree gram =
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index ff59bae578..03b0c77bbe 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -32,7 +32,6 @@ and 'te g_symbol =
   | Slist1 of 'te g_symbol
   | Slist1sep of 'te g_symbol * 'te g_symbol * bool
   | Sopt of 'te g_symbol
-  | Sflag of 'te g_symbol
   | Sself
   | Snext
   | Scut
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 6e99861423..0cf8eb5bbb 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -50,7 +50,6 @@ let rec print_symbol ppf =
       fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t
         (if osep then " OPT_SEP" else "")
   | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s
-  | Sflag s -> fprintf ppf "FLAG %a" print_symbol1 s
   | Stoken (con, prm) when con <> "" && prm <> "" ->
       fprintf ppf "%s@ %a" con print_str prm
   | Snterml (e, l) ->
@@ -68,7 +67,7 @@ and print_symbol1 ppf =
   | Stoken (con, "") -> pp_print_string ppf con
   | Stree t -> print_level ppf pp_print_space (flatten_tree t)
   | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) |
-    Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Sflag _ | Stoken _ as s ->
+    Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ as s ->
       fprintf ppf "(%a)" print_symbol s
 and print_rule ppf symbols =
   fprintf ppf "@[<hov 0>";
@@ -153,7 +152,6 @@ let rec name_of_symbol_failed entry =
   | Slist1 s -> name_of_symbol_failed entry s
   | Slist1sep (s, _, _) -> name_of_symbol_failed entry s
   | Sopt s -> name_of_symbol_failed entry s
-  | Sflag 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 =
@@ -293,7 +291,7 @@ 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 _ | Sflag _ | Stree _ -> txt ^ " expected"
+    | Sopt _ | Stree _ -> txt ^ " expected"
     | _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb
   in
   if !error_verbose then
@@ -641,12 +639,6 @@ and parser_of_symbol entry nlevn =
          match try Some (ps strm__) with Stream.Failure -> None with
            Some a -> Obj.repr (Some a)
          | _ -> Obj.repr None)
-  | Sflag 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 _ -> Obj.repr true
-         | _ -> Obj.repr false)
   | Stree t ->
       let pt = parser_of_tree entry 1 0 t in
       (fun (strm__ : _ Stream.t) ->
@@ -876,7 +868,6 @@ let find_entry e s =
     | Slist1 s -> find_symbol s
     | Slist1sep (s, _, _) -> find_symbol s
     | Sopt s -> find_symbol s
-    | Sflag s -> find_symbol s
     | Stree t -> find_tree t
     | Sself | Snext | Scut | Stoken _ -> None
   and find_tree =
@@ -997,7 +988,6 @@ module type S =
       ('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_flag : ('self, 'a) ty_symbol -> ('self, bool) 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
@@ -1082,7 +1072,6 @@ module GMake (L : GLexerType) =
     let s_list1 s = Slist1 s
     let s_list1sep s sep b = Slist1sep (s, sep, b)
     let s_opt s = Sopt s
-    let s_flag s = Sflag s
     let s_self = Sself
     let s_next = Snext
     let s_token tok = Stoken tok
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index e115b9df43..fe06d1fa81 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -123,7 +123,6 @@ module type S =
       ('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_flag : ('self, 'a) ty_symbol -> ('self, bool) 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
-- 
cgit v1.2.3


From d382b815fd5ec0ee81f01aec6a72b1f7adf8b907 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Nov 2018 21:48:02 +0100
Subject: Remove the Scut constructor from Gramlib.

This constructor only makes sense in the backtracking mode, that has
been removed from our vendored version of camlp5.
---
 gramlib/gramext.ml  | 14 +++++---------
 gramlib/gramext.mli |  1 -
 gramlib/grammar.ml  | 10 ++--------
 gramlib/grammar.mli |  1 -
 4 files changed, 7 insertions(+), 19 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 159070b2f2..72468b540e 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -36,7 +36,6 @@ and 'te g_symbol =
   | Sopt of 'te g_symbol
   | Sself
   | Snext
-  | Scut
   | Stoken of Plexing.pattern
   | Stree of 'te g_tree
 and g_action = Obj.t
@@ -65,7 +64,7 @@ let rec derive_eps =
   | Sopt _ -> true
   | Stree t -> tree_derive_eps t
   | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
-    Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
+    Snterml (_, _) | Snext | Sself | Stoken _ ->
       false
 and tree_derive_eps =
   function
@@ -125,9 +124,6 @@ let insert_tree entry_name gsymbols action tree =
         if eq_symbol s s1 then
           let t = Node {node = s1; son = insert sl son; brother = bro} in
           Some t
-        else if s = Scut then
-          try_insert s sl (Node {node = s; son = tree; brother = DeadEnd})
-        else if s1 = Scut then try_insert s1 (s :: sl) tree
         else if is_before s1 s || derive_eps s && not (derive_eps s1) then
           let bro =
             match try_insert s sl bro with
@@ -179,7 +175,7 @@ and token_exists_in_symbol f =
   | Sopt sy -> token_exists_in_symbol f sy
   | Stoken tok -> f tok
   | Stree t -> token_exists_in_tree f t
-  | Snterm _ | Snterml (_, _) | Snext | Sself | Scut -> false
+  | Snterm _ | Snterml (_, _) | Snext | Sself -> false
 
 let insert_level entry_name e1 symbols action slev =
   match e1 with
@@ -310,7 +306,7 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
   | Slist1 s -> check_gram entry s
   | Sopt s -> check_gram entry s
   | Stree t -> tree_check_gram entry t
-  | Snext | Sself | Scut | Stoken _ -> ()
+  | Snext | Sself | Stoken _ -> ()
 and tree_check_gram entry =
   function
     Node {node = n; brother = bro; son = son} ->
@@ -344,7 +340,7 @@ 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 | Scut -> ()
+    | Snterm _ | Snterml (_, _) | Snext | Sself -> ()
   and tinsert =
     function
       Node {node = s; brother = bro; son = son} ->
@@ -468,7 +464,7 @@ 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 | Scut | Snterm _ | Snterml (_, _) -> ()
+  | Sself | Snext | Snterm _ | Snterml (_, _) -> ()
 and decr_keyw_use_in_tree gram =
   function
     DeadEnd | LocAct (_, _) -> ()
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index 03b0c77bbe..e888508277 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -34,7 +34,6 @@ and 'te g_symbol =
   | Sopt of 'te g_symbol
   | Sself
   | Snext
-  | Scut
   | Stoken of Plexing.pattern
   | Stree of 'te g_tree
 and g_action = Obj.t
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 0cf8eb5bbb..5340482a01 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -55,14 +55,13 @@ let rec print_symbol ppf =
   | Snterml (e, l) ->
       fprintf ppf "%s%s@ LEVEL@ %a" e.ename (if e.elocal then "*" else "")
         print_str l
-  | Snterm _ | Snext | Sself | Scut | Stoken _ | Stree _ as s ->
+  | 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 "")
   | Sself -> pp_print_string ppf "SELF"
   | Snext -> pp_print_string ppf "NEXT"
-  | Scut -> pp_print_string 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)
@@ -410,8 +409,6 @@ let rec parser_of_tree entry nlevn alevn =
   | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} ->
       (fun (strm__ : _ Stream.t) ->
          let a = entry.estart alevn strm__ in app act a)
-  | Node {node = Scut; son = son; brother = _} ->
-      parser_of_tree entry nlevn alevn son
   | Node {node = Sself; son = LocAct (act, _); brother = bro} ->
       let p2 = parser_of_tree entry nlevn alevn bro in
       (fun (strm__ : _ Stream.t) ->
@@ -651,7 +648,6 @@ and parser_of_symbol entry nlevn =
       (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__)
-  | Scut -> (fun (strm__ : _ Stream.t) -> Obj.repr ())
   | Stoken tok -> parser_of_token entry tok
 and parser_of_token entry tok =
   let f = entry.egram.glexer.Plexing.tok_match tok in
@@ -869,7 +865,7 @@ let find_entry e s =
     | Slist1sep (s, _, _) -> find_symbol s
     | Sopt s -> find_symbol s
     | Stree t -> find_tree t
-    | Sself | Snext | Scut | Stoken _ -> None
+    | Sself | Snext | Stoken _ -> None
   and find_tree =
     function
       Node {node = s; brother = bro; son = son} ->
@@ -996,7 +992,6 @@ module type S =
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
         ('self, 'b -> 'a, 'r) ty_rule
-    val r_cut : ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule
     val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
     module Unsafe :
       sig
@@ -1078,7 +1073,6 @@ module GMake (L : GLexerType) =
     let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t)
     let r_stop = []
     let r_next r s = r @ [s]
-    let r_cut r = r @ [Scut]
     let production
         (p : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f) : 'a ty_production =
       Obj.magic p
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index fe06d1fa81..53c8004a5b 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -131,7 +131,6 @@ module type S =
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
         ('self, 'b -> 'a, 'r) ty_rule
-    val r_cut : ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule
     val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
 
     module Unsafe :
-- 
cgit v1.2.3


From 9f17f5aad33d320e96d7cc4fa370b39e7d772697 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 4 Nov 2018 19:00:35 +0100
Subject: Remove patches of dead code in Gramlib.

---
 gramlib/ploc.ml  | 109 -------------------------------------------------------
 gramlib/ploc.mli |  29 ---------------
 2 files changed, 138 deletions(-)

(limited to 'gramlib')

diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index 6aa7c1a2bb..082686db01 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -55,115 +55,6 @@ let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}
 let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}
 let with_comment loc comm = {loc with comm = comm}
 
-let name = ref "loc"
-
-let from_file fname loc =
-  let (bp, ep) = first_pos loc, last_pos loc in
-  try
-    let ic = open_in_bin fname in
-    let strm = Stream.of_channel ic in
-    let rec loop fname lin =
-      let rec not_a_line_dir col (strm__ : _ Stream.t) =
-        let cnt = Stream.count strm__ in
-        match Stream.peek strm__ with
-          Some c ->
-            Stream.junk strm__;
-            let s = strm__ in
-            if cnt < bp then
-              if c = '\n' then loop fname (lin + 1)
-              else not_a_line_dir (col + 1) s
-            else let col = col - (cnt - bp) in fname, lin, col, col + ep - bp
-        | _ -> fname, lin, col, col + 1
-      in
-      let rec a_line_dir str n col (strm__ : _ Stream.t) =
-        match Stream.peek strm__ with
-          Some '\n' -> Stream.junk strm__; loop str n
-        | Some _ -> Stream.junk strm__; a_line_dir str n (col + 1) strm__
-        | _ -> raise Stream.Failure
-      in
-      let rec spaces col (strm__ : _ Stream.t) =
-        match Stream.peek strm__ with
-          Some ' ' -> Stream.junk strm__; spaces (col + 1) strm__
-        | _ -> col
-      in
-      let rec check_string str n col (strm__ : _ Stream.t) =
-        match Stream.peek strm__ with
-          Some '"' ->
-            Stream.junk strm__;
-            let col =
-              try spaces (col + 1) strm__ with
-                Stream.Failure -> raise (Stream.Error "")
-            in
-            a_line_dir str n col strm__
-        | Some c when c <> '\n' ->
-            Stream.junk strm__;
-            check_string (str ^ String.make 1 c) n (col + 1) strm__
-        | _ -> not_a_line_dir col strm__
-      in
-      let check_quote n col (strm__ : _ Stream.t) =
-        match Stream.peek strm__ with
-          Some '"' -> Stream.junk strm__; check_string "" n (col + 1) strm__
-        | _ -> not_a_line_dir col strm__
-      in
-      let rec check_num n col (strm__ : _ Stream.t) =
-        match Stream.peek strm__ with
-          Some ('0'..'9' as c) ->
-            Stream.junk strm__;
-            check_num (10 * n + Char.code c - Char.code '0') (col + 1) strm__
-        | _ -> let col = spaces col strm__ in check_quote n col strm__
-      in
-      let begin_line (strm__ : _ Stream.t) =
-        match Stream.peek strm__ with
-          Some '#' ->
-            Stream.junk strm__;
-            let col =
-              try spaces 1 strm__ with
-                Stream.Failure -> raise (Stream.Error "")
-            in
-            check_num 0 col strm__
-        | _ -> not_a_line_dir 0 strm__
-      in
-      begin_line strm
-    in
-    let r =
-      try loop fname 1 with
-        Stream.Failure ->
-          let bol = bol_pos loc in fname, line_nb loc, bp - bol, ep - bol
-    in
-    close_in ic; r
-  with Sys_error _ -> fname, 1, bp, ep
-
-let second_line fname ep0 (line, bp) ep =
-  let ic = open_in fname in
-  seek_in ic bp;
-  let rec loop line bol p =
-    if p = ep then
-      begin close_in ic; if bol = bp then line, ep0 else line, ep - bol end
-    else
-      let (line, bol) =
-        match input_char ic with
-          '\n' -> line + 1, p + 1
-        | _ -> line, bol
-      in
-      loop line bol (p + 1)
-  in
-  loop line bp bp
-
-let get loc =
-  if loc.fname = "" || loc.fname = "-" then
-    loc.line_nb, loc.bp - loc.bol_pos, loc.line_nb, loc.ep - loc.bol_pos,
-    loc.ep - loc.bp
-  else
-    let (bl, bc, ec) =
-      loc.line_nb, loc.bp - loc.bol_pos, loc.ep - loc.bol_pos
-    in
-    let (el, eep) = second_line loc.fname ec (bl, loc.bp) loc.ep in
-    bl, bc, el, eep, ec - bc
-
-let call_with r v f a =
-  let saved = !r in
-  try r := v; let b = f a in r := saved; b with e -> r := saved; raise e
-
 exception Exc of t * exn
 
 let raise loc exc =
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index afddefcd6e..2ce6382183 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -84,32 +84,3 @@ val after : t -> int -> int -> t
        [len]. *)
 val with_comment : t -> string -> t
    (** Change the comment part of the given location *)
-
-(* miscellaneous *)
-
-val name : string ref
-   (** [Ploc.name.val] is the name of the location variable used in grammars
-       and in the predefined quotations for OCaml syntax trees. Default:
-       ["loc"] *)
-
-val get : t -> int * int * int * int * int
-   (** [Ploc.get loc] returns in order: 1/ the line number of the begin
-       of the location, 2/ its column, 3/ the line number of the first
-       character not in the location, 4/ its column and 5/ the length
-       of the location. The file where the location occurs (if any) may
-       be read during this operation. *)
-
-val from_file : string -> t -> string * int * int * int
-   (** [Ploc.from_file fname loc] reads the file [fname] up to the
-       location [loc] and returns the real input file, the line number
-       and the characters location in the line; the real input file
-       can be different from [fname] because of possibility of line
-       directives typically generated by /lib/cpp. *)
-
-(* pervasives *)
-
-val call_with : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
-   (** [Ploc.call_with r v f a] sets the reference [r] to the value [v],
-       then call [f a], and resets [r] to its initial value. If [f a] raises
-       an exception, its initial value is also reset and the exception is
-       re-raised. The result is the result of [f a]. *)
-- 
cgit v1.2.3