blob: 105c5f43173f785fd90d49a89134daefe7c4605b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
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
|
