diff options
Diffstat (limited to 'src/elf_model/string_table.lem')
| -rw-r--r-- | src/elf_model/string_table.lem | 104 |
1 files changed, 0 insertions, 104 deletions
diff --git a/src/elf_model/string_table.lem b/src/elf_model/string_table.lem deleted file mode 100644 index 105c5f43..00000000 --- a/src/elf_model/string_table.lem +++ /dev/null @@ -1,104 +0,0 @@ -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
\ No newline at end of file |