1 files changed, 123 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/string_table.ml b/lib/ocaml_rts/linksem/string_table.ml
new file mode 100644
index 00000000..fc74e323
--- /dev/null
+++ b/lib/ocaml_rts/linksem/string_table.ml
@@ -0,0 +1,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))))})