summaryrefslogtreecommitdiff
path: root/src/elf_model/string_table.lem
diff options
context:
space:
mode:
authorKathy Gray2014-10-30 17:32:07 +0000
committerKathy Gray2014-10-30 17:32:23 +0000
commit74cc06dbe36e411133d392c846a9aff4b0a7df14 (patch)
treee2ab35b000bc29a4a5439e4a12a58216459d1616 /src/elf_model/string_table.lem
parent21738f049b1365c8436780449f9fbfdce1e9324d (diff)
Pull in updated elf model, make build work again (at least for me)
Diffstat (limited to 'src/elf_model/string_table.lem')
-rw-r--r--src/elf_model/string_table.lem17
1 files changed, 17 insertions, 0 deletions
diff --git a/src/elf_model/string_table.lem b/src/elf_model/string_table.lem
index 8cfe5056..105c5f43 100644
--- a/src/elf_model/string_table.lem
+++ b/src/elf_model/string_table.lem
@@ -1,3 +1,4 @@
+open import Basic_classes
open import List
open import Maybe
open import Num
@@ -40,6 +41,22 @@ let get_base_string tbl =
| 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.
*)