remove old elf sources

1 files changed, 0 insertions, 87 deletions

diff --git a/src/elf_model/bitstring.lem b/src/elf_model/bitstring.lem
deleted file mode 100644
index ed9df857..00000000
--- a/src/elf_model/bitstring.lem
+++ /dev/null
@@ -1,87 +0,0 @@
-open import Basic_classes
-open import Bool
-open import Num
-open import Show
-
-open import Error
-
-declare {ocaml} rename module = bitstring_local
-
-type bitstring
-
-declare ocaml target_rep type bitstring = `Bitstring.bitstring`
-
-(** [empty] is the empty bitstring.
-  *)
-val empty : bitstring
-
-declare ocaml target_rep function empty = `Bitstring.empty`
-
-(** [zeros m] creates a bitstring of length [m] containing all zeros.
-  *)
-val zeros : nat -> bitstring
-
-declare ocaml target_rep function zeros = `Bitstring.create_bitstring`
-
-(** [create m c] creates a bitstring of length [m] containing all [c]
-  * characters.
-  *)
-val create : nat -> char -> bitstring
-
-declare ocaml target_rep function create = `Bitstring.make_bitstring`
-
-(** [concat xs] concatenates a list of bitstrings [xs] into a single bitstring.
-  *)
-val concat : list bitstring -> bitstring
-
-declare ocaml target_rep function concat = `Bitstring.concat`
-
-(** [acquire fname] acquires a bitstring from a binary file, located at [fname].
-  *)
-val acquire : string -> error bitstring
-
-declare ocaml target_rep function acquire = `Ml_bindings.acquire_bitstring`
-
-(** [length bs0] returns the length of bitstring [bs0].
-  *)
-val length : bitstring -> nat
-
-declare ocaml target_rep function length = `Bitstring.bitstring_length`
-
-(** [partition offset bs0] cuts [bs0] into two pieces at offset [offset].  Throws
-  * an exception if 
-  *)
-val partition : nat -> bitstring -> (bitstring * bitstring)
-
-declare ocaml target_rep function partition = `Ml_bindings.partition_bitstring`
-
-(** [offset_and_cut offset size bs0] cuts a [size]-lengthed bitstring out of [bs0]
-  * at offset [offset].
-  *)
-val offset_and_cut : nat -> nat -> bitstring -> bitstring
-let offset_and_cut offset size bs0 =
-  let (_, cut) = partition offset bs0 in
-  let (rel, _) = partition size cut in
-    rel
-
-(** [equal bs0 bs1] tests whether [bs0] and [bs1] are equal.
-  *)
-val equal : bitstring -> bitstring -> bool
-
-declare ocaml target_rep function equal = unsafe_structural_equality
-
-(** [string_of_bitstring bs0] produces a string-based representation of bitstring
-  * [bs0].
-  *)
-val string_of_bitstring : bitstring -> string
-
-declare ocaml target_rep function string_of_bitstring = `Bitstring.string_of_bitstring`
-
-instance (Eq bitstring)
-  let (=) = equal
-  let (<>) l r = not (equal l r)
-end
-
-instance (Show bitstring)
-  let show = string_of_bitstring
-end