Source file string_table.ml

(*Generated by Lem from string_table.lem.*)
(** The [string_table] module implements string tables.  An ELF file may have
  * multiple different string tables used for different purposes.  A string
  * table is a string coupled with a delimiting character.  Strings may be indexed
  * at any position, not necessarily on a delimiter boundary.
  *)

open Lem_basic_classes
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
open Byte_sequence

open Error
open Missing_pervasives
open Show

(** [string_table] type, represents a string table with a fixed delimiting
  * character and underlying string.
  *)
type string_table
  = Strings of (char * string)

      
(*val dummy_strtab : string_table*)
let dummy_strtab:string_table=  (Strings ('\n',""))
      
(** [mk_string_table base sep] constructs a string table using [base] as the
  * base string and [sep] as the delimiting character to use to split [base]
  * when trying to access the string stored in the table using the functions below.
  *)
(*val mk_string_table : string -> char -> string_table*)
let mk_string_table base sep:string_table=
   (Strings (sep, base))

(** [string_table_of_byte_sequence seq] constructs a string table, using the NUL
  * character as terminator, from a byte sequence. *)
(*val string_table_of_byte_sequence : byte_sequence -> string_table*)
let string_table_of_byte_sequence seq:string_table=  (mk_string_table (string_of_byte_sequence seq) null_char)

(** [empty] is the empty string table with an arbitrary choice of delimiter.
  *)
(*val empty : string_table*)
let empty0:string_table=  (Strings (null_char, Xstring.implode [null_char]))

(** [get_delimiating_character tbl] returns the delimiting character associated
  * with the string table [tbl], used to split the strings.
  *)
(*val get_delimiting_character : string_table -> char*)
let get_delimiting_character tbl:char=
   ((match tbl with
    | Strings (sep, base) -> sep
  ))

(** [get_base_string tbl] returns the base string of the string table [tbl].
  *)
(*val get_base_string : string_table -> string*)
let get_base_string tbl:string=
   ((match tbl with
    | Strings (sep, base) -> base
  ))

(** [size tbl] returns the size in bytes of the string table [tbl].
  *)
(*val size : string_table -> natural*)
let size0 tbl:Nat_big_num.num=  (Nat_big_num.of_int (String.length (get_base_string tbl)))

(** [concat xs] concatenates several string tables into one providing they all
  * have the same delimiting character.
  *)
(*val concat : list string_table -> error string_table*)
let concat0 xs:(string_table)error=
   ((match xs with
    | []    -> return empty0
    | x::xs ->
      let delim = (get_delimiting_character x) in
        if (List.for_all (fun x -> get_delimiting_character x = delim) (x::xs)) then
          let base = (List.fold_right (^) (Lem_list.map get_base_string (x::xs)) "") in
            return (mk_string_table base delim)
        else
          fail "concat: string tables must have same delimiting characters"
  ))

(** [get_string_at index tbl] returns the string starting at character [index]
  * from the start of the base string until the first occurrence of the delimiting
  * character.
  *)
(*val get_string_at : natural -> string_table -> error string*)
let get_string_at index tbl:(string)error=
   ((match Ml_bindings.string_suffix index (get_base_string tbl) with
    | None     -> Fail "get_string_at: index out of range"
    | Some suffix ->
      let delim = (get_delimiting_character tbl) in
      (match Ml_bindings.string_index_of delim suffix with
        | Some idx1 ->
          (match Ml_bindings.string_prefix idx1 suffix with
            | Some s  -> Success s
            | None -> Fail "get_string_at: index out of range"
          )
        | None -> Success suffix
      )
  ))

(*val find_string : string -> string_table -> maybe natural*)
let find_string s t:(Nat_big_num.num)option= 
     ((match t with
        Strings(delim, base) -> Ml_bindings.find_substring (s ^ Xstring.implode [delim]) base
    ))

(*val insert_string : string -> string_table -> (natural * string_table)*)
let insert_string s t:Nat_big_num.num*string_table=
     ( 
    (*let _ = errln ("Inserting string `" ^ s ^ "' into a string table") in*)let (inserted_idx, new_strtab) = ((match find_string s t with
        None -> (match t with
            Strings(delim, base) -> (Nat_big_num.of_int (String.length base), Strings(delim, (base ^ (s ^ (Xstring.implode [delim])))))
            )
        | Some pos -> (pos, t)
    ))
    in
    (*let _ = errln ("Inserted string at idx " ^ (show inserted_idx) ^ ", see: " ^ (show (find_string s new_strtab)))
    in*)
    (inserted_idx, new_strtab))

let instance_Show_Show_String_table_string_table_dict:(string_table)show_class= ({

  show_method = (fun tbl->Xstring.implode (Lem_list.map (fun c -> if c = '\000' then '\n' else c) (Xstring.explode (get_base_string tbl))))})