Removing dead code in Plexing.

It was full with utility functions and wrappers that are unused in the Coq
codebase.

2 files changed, 0 insertions, 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