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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
(*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)
(** [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 concat1 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))))})
|
