open import Basic_classes
open import List
open import Maybe
open import Num
open import String

open import Error
open import Missing_pervasives
open import Show

type string_table
  = Strings of (char * string)

(** [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 =
  Strings (sep, base)

(** [empty] is the empty string table with an arbitrary choice of delimiter.
  *)
val empty : string_table
let empty = Strings (Missing_pervasives.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 =
  match tbl with
    | Strings (sep, base) -> sep
  end

(** [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 =
  match tbl with
    | Strings (sep, base) -> base
  end

(** [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 concat xs =
  match xs with
    | []    -> return empty
    | x::xs ->
      let delim = get_delimiting_character x in
        if (List.all (fun x -> get_delimiting_character x = delim) (x::xs)) then
          let base = List.foldr (^) "" (List.map get_base_string (x::xs)) in
            return (mk_string_table base delim)
        else
          fail "concat: string tables must have same delimiting characters"
  end

(** [get_strings tbl] obtains the strings stored in the table, separated using
  * the designated separator as a delimiting character.
  *)
val get_strings : string_table -> list string
let get_strings tbl =
  match tbl with
    | Strings (sep, base) ->
        Missing_pervasives.split_string_on_char base sep
  end

(** [size tbl] returns the number of strings separated by the designated
  * separator in the string table [tbl].
  *)
val size : string_table -> nat
let size tbl =
  List.length (get_strings tbl)

(** [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 : nat -> string_table -> error string
let get_string_at index tbl =
  match Missing_pervasives.string_suffix index (get_base_string tbl) with
    | Nothing     -> Fail "get_string_at: invalid index into string"
    | Just suffix ->
        let delim = get_delimiting_character tbl in
        let tbl   = mk_string_table suffix delim in
          match get_strings tbl with
            | []    -> Fail "get_string_at: empty string returned"
            | x::xs -> return x
          end
  end

class (HasElf32SectionHeaderStringTable 'a)
  val get_elf32_section_header_string_table : 'a -> string_table
end

class (HasElf64SectionHeaderStringTable 'a)
  val get_elf64_section_header_string_table : 'a -> string_table
end

instance (Show string_table)
  let show tbl = unlines (get_strings tbl)
end