From b9467f8918ef272a72b7280b5f372070aacef39c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Nov 2018 12:12:09 +0100
Subject: Remove the non-functorial interface of camlp5 grammars.

---
 gramlib/grammar.ml  | 106 ----------------------------------------------------
 gramlib/grammar.mli |  71 -----------------------------------
 2 files changed, 177 deletions(-)

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 5340482a01..760410894a 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -781,13 +781,6 @@ let delete_rule entry sl =
 
 (* Normal interface *)
 
-type token = string * string
-type g = token Gramext.grammar
-
-type ('self, 'a) ty_symbol = token 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 create_toktab () = Hashtbl.create 301
 let gcreate glexer =
   {gtokens = create_toktab (); glexer = glexer }
@@ -806,12 +799,6 @@ type 'te gen_parsable =
     pa_tok_strm : 'te Stream.t;
     pa_loc_func : Plexing.location_function }
 
-type parsable = token gen_parsable
-
-let parsable g cs =
-  let (ts, lf) = g.glexer.Plexing.tok_func cs in
-  {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
-
 let parse_parsable entry p =
   let efun = entry.estart 0 in
   let ts = p.pa_tok_strm in
@@ -843,93 +830,6 @@ let parse_parsable entry p =
       let loc = Stream.count cs, Stream.count cs + 1 in
       restore (); Ploc.raise (Ploc.make_unlined loc) exc
 
-let find_entry e s =
-  let rec find_levels =
-    function
-      [] -> None
-    | lev :: levs ->
-        match find_tree lev.lsuffix with
-          None ->
-            begin match find_tree lev.lprefix with
-              None -> find_levels levs
-            | x -> x
-            end
-        | x -> x
-  and find_symbol =
-    function
-    | 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
-    | Slist0sep (s, _, _) -> find_symbol s
-    | Slist1 s -> find_symbol s
-    | Slist1sep (s, _, _) -> find_symbol s
-    | Sopt s -> find_symbol s
-    | Stree t -> find_tree t
-    | Sself | Snext | Stoken _ -> None
-  and find_tree =
-    function
-      Node {node = s; brother = bro; son = son} ->
-        begin match find_symbol s with
-          None ->
-            begin match find_tree bro with
-              None -> find_tree son
-            | x -> x
-            end
-        | x -> x
-        end
-    | LocAct (_, _) | DeadEnd -> None
-  in
-  match e.edesc with
-    Dlevels levs ->
-      begin match find_levels levs with
-        Some e -> e
-      | None -> raise Not_found
-      end
-  | Dparser _ -> raise Not_found
-module Entry =
-  struct
-    type te = token
-    type 'a e = te g_entry
-    let create g n =
-      {egram = g; ename = n; elocal = false; estart = empty_entry n;
-       econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
-       edesc = Dlevels []}
-    let parse_parsable (entry : 'a e) p : 'a =
-      Obj.magic (parse_parsable entry p : Obj.t)
-    let parse (entry : 'a e) cs : 'a =
-      let parsable = parsable entry.egram cs in parse_parsable entry parsable
-    let parse_parsable_all (entry : 'a e) p : 'a =
-      begin try Obj.magic [(parse_parsable entry p : Obj.t)] with
-          Stream.Failure | Stream.Error _ -> []
-      end
-    let parse_all (entry : 'a e) cs : 'a =
-      let parsable = parsable entry.egram cs in
-      parse_parsable_all entry parsable
-    let parse_token_stream (entry : 'a e) ts : 'a =
-      Obj.magic (entry.estart 0 ts : Obj.t)
-    let _warned_using_parse_token = ref false
-    let parse_token (entry : 'a e) ts : 'a =
-      (* commented: too often warned in Coq...
-      if not warned_using_parse_token.val then do {
-        eprintf "<W> use of Grammar.Entry.parse_token ";
-        eprintf "deprecated since 2017-06-16\n%!";
-        eprintf "use Grammar.Entry.parse_token_stream instead\n%! ";
-        warned_using_parse_token.val := True
-      }
-      else ();
-      *)
-      parse_token_stream entry ts
-    let name e = e.ename
-    let of_parser g n (p : te Stream.t -> 'a) : 'a e =
-      {egram = g; ename = n; elocal = false;
-       estart = (fun _ -> (Obj.magic p : te Stream.t -> Obj.t));
-       econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
-       edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)}
-    external obj : 'a e -> te Gramext.g_entry = "%identity"
-    let print ppf e = fprintf ppf "%a@." print_entry (obj e)
-    let find e s = find_entry (obj e) s
-  end
-
 (* Unsafe *)
 
 let clear_entry e =
@@ -941,12 +841,6 @@ let clear_entry e =
 
 let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer
 
-module Unsafe =
-  struct
-    let gram_reinit = gram_reinit
-    let clear_entry = clear_entry
-  end
-
 (* Functorial interface *)
 
 module type GLexerType = sig type te val lexer : te Plexing.lexer end
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 53c8004a5b..244ab710dc 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -8,77 +8,6 @@
     Grammars entries can be extended using the [EXTEND] statement,
     added by loading the Camlp5 [pa_extend.cmo] file. *)
 
-type g
-   (** The type for grammars, holding entries. *)
-type token = string * string
-
-type parsable
-val parsable : g -> char Stream.t -> parsable
-   (** Type and value allowing to keep the same token stream between
-       several calls of entries of the same grammar, to prevent possible
-       loss of tokens. To be used with [Entry.parse_parsable] below *)
-
-module Entry :
-  sig
-    type 'a e
-    val create : g -> string -> 'a e
-    val parse : 'a e -> char Stream.t -> 'a
-    val parse_all : 'a e -> char Stream.t -> 'a list
-    val parse_parsable : 'a e -> parsable -> 'a
-    val name : 'a e -> string
-    val of_parser : g -> string -> (token Stream.t -> 'a) -> 'a e
-    val parse_token_stream : 'a e -> token Stream.t -> 'a
-    val print : Format.formatter -> 'a e -> unit
-    val find : 'a e -> string -> Obj.t e
-    external obj : 'a e -> token Gramext.g_entry = "%identity"
-    val parse_token : 'a e -> token Stream.t -> 'a
-  end
-   (** Module to handle entries.
--      [Entry.e] is the type for entries returning values of type ['a].
--      [Entry.create g n] creates a new entry named [n] in the grammar [g].
--      [Entry.parse e] returns the stream parser of the entry [e].
--      [Entry.parse_all e] returns the stream parser returning all possible
-          values while parsing with the entry [e]: may return more than one
-          value when the parsing algorithm is [Backtracking]
--      [Entry.parse_all e] returns the parser returning all possible values.
--      [Entry.parse_parsable e] returns the parsable parser of the entry [e].
--      [Entry.name e] returns the name of the entry [e].
--      [Entry.of_parser g n p] makes an entry from a token stream parser.
--      [Entry.parse_token_stream e] returns the token stream parser of the
-          entry [e].
--      [Entry.print e] displays the entry [e] using [Format].
--      [Entry.find e s] finds the entry named [s] in the rules of [e].
--      [Entry.obj e] converts an entry into a [Gramext.g_entry] allowing
-          to see what it holds.
--      [Entry.parse_token]: deprecated since 2017-06-16; old name for
-          [Entry.parse_token_stream] *)
-
-type ('self, 'a) ty_symbol
-(** Type of grammar symbols. A type-safe wrapper around Gramext.symbol. The
-    first type argument is the type of the ambient entry, the second one is the
-    type of the produced value. *)
-
-type ('self, 'f, 'r) ty_rule
-
-type 'a ty_production
-
-(** {6 Clearing grammars and entries} *)
-
-module Unsafe :
-  sig
-    val gram_reinit : g -> token Plexing.lexer -> unit
-    val clear_entry : 'a Entry.e -> unit
-  end
-   (** Module for clearing grammars and entries. To be manipulated with
-       care, because: 1) reinitializing a grammar destroys all tokens
-       and there may have problems with the associated lexer if there
-       are keywords; 2) clearing an entry does not destroy the tokens
-       used only by itself.
--      [Unsafe.reinit_gram g lex] removes the tokens of the grammar
--      and sets [lex] as a new lexer for [g]. Warning: the lexer
--      itself is not reinitialized.
--      [Unsafe.clear_entry e] removes all rules of the entry [e]. *)
-
 (** {6 Functorial interface} *)
 
    (** Alternative for grammars use. Grammars are no more Ocaml values:
-- 
cgit v1.2.3


From 909c215de105cc5965398656348d5486d57c1b87 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Nov 2018 12:18:24 +0100
Subject: Removing dead code in Plexing.

It was full with utility functions and wrappers that are unused in the Coq
codebase.
---
 gramlib/plexing.ml  | 198 ----------------------------------------------------
 gramlib/plexing.mli |  71 -------------------
 2 files changed, 269 deletions(-)

diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index beebcd016e..986363ec1f 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -17,201 +17,3 @@ type 'te lexer =
     mutable tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
     mutable tok_comm : location list option }
-
-let make_loc = Ploc.make_unlined
-let dummy_loc = Ploc.dummy
-
-let lexer_text (con, prm) =
-  if con = "" then "'" ^ prm ^ "'"
-  else if prm = "" then con
-  else con ^ " '" ^ prm ^ "'"
-
-let locerr () = failwith "Lexer: location function"
-let loct_create () = ref (Array.make 1024 None), ref false
-let loct_func (loct, ov) i =
-  match
-    if i < 0 || i >= Array.length !loct then
-      if !ov then Some dummy_loc else None
-    else Array.unsafe_get !loct i
-  with
-    Some loc -> loc
-  | None -> locerr ()
-let loct_add (loct, ov) i loc =
-  if i >= Array.length !loct then
-    let new_tmax = Array.length !loct * 2 in
-    if new_tmax < Sys.max_array_length then
-      let new_loct = Array.make new_tmax None in
-      Array.blit !loct 0 new_loct 0 (Array.length !loct);
-      loct := new_loct;
-      !loct.(i) <- Some loc
-    else ov := true
-  else !loct.(i) <- Some loc
-
-let make_stream_and_location next_token_loc =
-  let loct = loct_create () in
-  let ts =
-    Stream.from
-      (fun i ->
-         let (tok, loc) = next_token_loc () in loct_add loct i loc; Some tok)
-  in
-  ts, loct_func loct
-
-let lexer_func_of_parser next_token_loc cs =
-  let line_nb = ref 1 in
-  let bolpos = ref 0 in
-  make_stream_and_location (fun () -> next_token_loc (cs, line_nb, bolpos))
-
-let lexer_func_of_ocamllex lexfun cs =
-  let lb =
-    Lexing.from_function
-      (fun s n ->
-         try Bytes.set s 0 (Stream.next cs); 1 with Stream.Failure -> 0)
-  in
-  let next_token_loc _ =
-    let tok = lexfun lb in
-    let loc = make_loc (Lexing.lexeme_start lb, Lexing.lexeme_end lb) in
-    tok, loc
-  in
-  make_stream_and_location next_token_loc
-
-(* Char and string tokens to real chars and string *)
-
-let buff = ref (Bytes.create 80)
-let store len x =
-  if len >= Bytes.length !buff then
-    buff := Bytes.(cat !buff (create (length !buff)));
-  Bytes.set !buff len x;
-  succ len
-let get_buff len = Bytes.sub !buff 0 len
-
-let valch x = Char.code x - Char.code '0'
-let valch_a x = Char.code x - Char.code 'a' + 10
-let valch_A x = Char.code x - Char.code 'A' + 10
-
-let rec backslash s i =
-  if i = String.length s then raise Not_found
-  else
-    match s.[i] with
-      'n' -> '\n', i + 1
-    | 'r' -> '\r', i + 1
-    | 't' -> '\t', i + 1
-    | 'b' -> '\b', i + 1
-    | '\\' -> '\\', i + 1
-    | '"' -> '"', i + 1
-    | '\'' -> '\'', i + 1
-    | '0'..'9' as c -> backslash1 (valch c) s (i + 1)
-    | 'x' -> backslash1h s (i + 1)
-    | _ -> raise Not_found
-and backslash1 cod s i =
-  if i = String.length s then '\\', i - 1
-  else
-    match s.[i] with
-      '0'..'9' as c -> backslash2 (10 * cod + valch c) s (i + 1)
-    | _ -> '\\', i - 1
-and backslash2 cod s i =
-  if i = String.length s then '\\', i - 2
-  else
-    match s.[i] with
-      '0'..'9' as c -> Char.chr (10 * cod + valch c), i + 1
-    | _ -> '\\', i - 2
-and backslash1h s i =
-  if i = String.length s then '\\', i - 1
-  else
-    match s.[i] with
-      '0'..'9' as c -> backslash2h (valch c) s (i + 1)
-    | 'a'..'f' as c -> backslash2h (valch_a c) s (i + 1)
-    | 'A'..'F' as c -> backslash2h (valch_A c) s (i + 1)
-    | _ -> '\\', i - 1
-and backslash2h cod s i =
-  if i = String.length s then '\\', i - 2
-  else
-    match s.[i] with
-      '0'..'9' as c -> Char.chr (16 * cod + valch c), i + 1
-    | 'a'..'f' as c -> Char.chr (16 * cod + valch_a c), i + 1
-    | 'A'..'F' as c -> Char.chr (16 * cod + valch_A c), i + 1
-    | _ -> '\\', i - 2
-
-let rec skip_indent s i =
-  if i = String.length s then i
-  else
-    match s.[i] with
-      ' ' | '\t' -> skip_indent s (i + 1)
-    | _ -> i
-
-let skip_opt_linefeed s i =
-  if i = String.length s then i else if s.[i] = '\010' then i + 1 else i
-
-let eval_char s =
-  if String.length s = 1 then s.[0]
-  else if String.length s = 0 then failwith "invalid char token"
-  else if s.[0] = '\\' then
-    if String.length s = 2 && s.[1] = '\'' then '\''
-    else
-      try
-        let (c, i) = backslash s 1 in
-        if i = String.length s then c else raise Not_found
-      with Not_found -> failwith "invalid char token"
-  else failwith "invalid char token"
-
-let eval_string loc s =
-  let rec loop len i =
-    if i = String.length s then get_buff len
-    else
-      let (len, i) =
-        if s.[i] = '\\' then
-          let i = i + 1 in
-          if i = String.length s then failwith "invalid string token"
-          else if s.[i] = '"' then store len '"', i + 1
-          else
-            match s.[i] with
-              '\010' -> len, skip_indent s (i + 1)
-            | '\013' -> len, skip_indent s (skip_opt_linefeed s (i + 1))
-            | c ->
-                try let (c, i) = backslash s i in store len c, i with
-                  Not_found -> store (store len '\\') c, i + 1
-        else store len s.[i], i + 1
-      in
-      loop len i
-  in
-  Bytes.to_string (loop 0 0)
-
-let default_match =
-  function
-    "ANY", "" -> (fun (con, prm) -> prm)
-  | "ANY", v ->
-      (fun (con, prm) -> if v = prm then v else raise Stream.Failure)
-  | p_con, "" ->
-      (fun (con, prm) -> if con = p_con then prm else raise Stream.Failure)
-  | p_con, p_prm ->
-      fun (con, prm) ->
-        if con = p_con && prm = p_prm then prm else raise Stream.Failure
-
-let input_file = ref ""
-let line_nb = ref (ref 0)
-let bol_pos = ref (ref 0)
-let restore_lexing_info = ref None
-
-(* The lexing buffer used by pa_lexer.cmo *)
-
-let rev_implode l =
-  let s = Bytes.create (List.length l) in
-  let rec loop i =
-    function
-      c :: l -> Bytes.unsafe_set s i c; loop (i - 1) l
-    | [] -> s
-  in
-  Bytes.to_string (loop (Bytes.length s - 1) l)
-
-module Lexbuf :
-  sig
-    type t
-    val empty : t
-    val add : char -> t -> t
-    val get : t -> string
-  end =
-  struct
-    type t = char list
-    let empty = []
-    let add c l = c :: l
-    let get = rev_implode
-  end
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 6b5f718bc3..96b432a8ad 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -35,74 +35,3 @@ and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
 and location_function = int -> Ploc.t
   (** The type of a function giving the location of a token in the
       source from the token number in the stream (starting from zero). *)
-
-val lexer_text : pattern -> string
-   (** A simple [tok_text] function. *)
-
-val default_match : pattern -> string * string -> string
-   (** A simple [tok_match] function, appling to the token type
-       [(string * string)] *)
-
-(** Lexers from parsers or ocamllex
-
-   The functions below create lexer functions either from a [char stream]
-   parser or for an [ocamllex] function. With the returned function [f],
-   it is possible to get a simple lexer (of the type [Plexing.glexer] above):
-   {[
-          { Plexing.tok_func = f;
-            Plexing.tok_using = (fun _ -> ());
-            Plexing.tok_removing = (fun _ -> ());
-            Plexing.tok_match = Plexing.default_match;
-            Plexing.tok_text = Plexing.lexer_text;
-            Plexing.tok_comm = None }
-   ]}
-   Note that a better [tok_using] function should check the used tokens
-   and raise [Plexing.Error] for incorrect ones. The other functions
-   [tok_removing], [tok_match] and [tok_text] may have other implementations
-   as well. *)
-
-val lexer_func_of_parser :
-  (char Stream.t * int ref * int ref -> 'te * Ploc.t) -> 'te lexer_func
-   (** A lexer function from a lexer written as a char stream parser
-       returning the next token and its location. The two references
-       with the char stream contain the current line number and the
-       position of the beginning of the current line. *)
-val lexer_func_of_ocamllex : (Lexing.lexbuf -> 'te) -> 'te lexer_func
-   (** A lexer function from a lexer created by [ocamllex] *)
-
-(** Function to build a stream and a location function *)
-
-val make_stream_and_location :
-  (unit -> 'te * Ploc.t) -> 'te Stream.t * location_function
-   (** General function *)
-
-(** Useful functions and values *)
-
-val eval_char : string -> char
-val eval_string : Ploc.t -> string -> string
-   (** Convert a char or a string token, where the backslashes had not
-       been interpreted into a real char or string; raise [Failure] if
-       bad backslash sequence found; [Plexing.eval_char (Char.escaped c)]
-       would return [c] and [Plexing.eval_string (String.escaped s)] would
-       return [s] *)
-
-val restore_lexing_info : (int * int) option ref
-val input_file : string ref
-val line_nb : int ref ref
-val bol_pos : int ref ref
-   (** Special variables used to reinitialize line numbers and position
-       of beginning of line with their correct current values when a parser
-       is called several times with the same character stream. Necessary
-       for directives (e.g. #load or #use) which interrupt the parsing.
-       Without usage of these variables, locations after the directives
-       can be wrong. *)
-
-(** The lexing buffer used by streams lexers *)
-
-module Lexbuf :
-  sig
-    type t
-    val empty : t
-    val add : char -> t -> t
-    val get : t -> string
-  end
-- 
cgit v1.2.3