diff options
| author | Kathy Gray | 2014-10-30 17:32:07 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-10-30 17:32:23 +0000 |
| commit | 74cc06dbe36e411133d392c846a9aff4b0a7df14 (patch) | |
| tree | e2ab35b000bc29a4a5439e4a12a58216459d1616 /src/elf_model/string_table.lem | |
| parent | 21738f049b1365c8436780449f9fbfdce1e9324d (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.lem | 17 |
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. *) |
