1 files changed, 86 insertions, 0 deletions
diff --git a/src/elf_model/error.lem b/src/elf_model/error.lem
new file mode 100644
index 00000000..ca34a5d4
--- /dev/null
+++ b/src/elf_model/error.lem
@@ -0,0 +1,86 @@
+open import List
+open import Num
+open import String
+
+open import Show
+
+(** [error] is a type used to represent potentially failing computations. [Success]
+  * marks a successful completion of a computation, whilst [Fail err] marks a failure,
+  * with [err] as the reason.
+  *)
+type error 'a
+	= Success of 'a
+	| Fail of string
+
+(** [return] is the monadic lifting function for [error], representing a successful
+  * computation.
+  *)
+val return : forall 'a. 'a -> error 'a
+let return r = Success r
+
+(** [fail err] represents a failing computation, with error message [err].
+  *)
+val fail : forall 'a. string -> error 'a
+let fail err = Fail err
+
+(** [(>>=)] is the monadic binding function for [error].
+  *)
+val (>>=) : forall 'a 'b. error 'a -> ('a -> error 'b) -> error 'b
+let (>>=) x f =
+	match x with
+		| Success s -> f s
+		| Fail err  -> Fail err
+	end
+
+(** [repeatM count action] fails if [action] is a failing computation, or
+  * successfully produces a list [count] elements long, where each element is
+  * the value successfully returned by [action].
+  *)
+val repeatM : forall 'a. nat -> error 'a -> error (list 'a)
+let rec repeatM count action =
+	match count with
+		| 0 -> return []
+		| m ->
+				action >>= fun head ->
+				repeatM (m - 1) action >>= fun tail ->
+				return (head::tail)
+	end
+
+(** [repeatM' count seed action] is a variant of [repeatM] that acts like [repeatM]
+  * apart from any successful result returns a tuple whose second component is [seed]
+  * and whose first component is the same as would be returned by [repeatM].
+  *)
+val repeatM' : forall 'a 'b. nat -> 'b -> ('b -> error ('a * 'b)) -> error ((list 'a) * 'b)
+let rec repeatM' count seed action =
+	match count with
+		| 0 -> return ([], seed)
+		| m ->
+				action seed >>= fun (head, seed) ->
+				repeatM' (m - 1) seed action >>= fun (tail, seed) ->
+				return (head::tail, seed)
+	end
+	
+(** [mapM f xs] maps [f] across [xs], failing if [f] fails on any element of [xs].
+  *)
+val mapM : forall 'a 'b. ('a -> error 'b) -> list 'a -> error (list 'b)
+let rec mapM f xs =
+	match xs with
+		| []    -> return []
+		| x::xs ->
+				f x >>= fun hd ->
+				mapM f xs >>= fun tl ->
+				return (hd::tl)
+	end
+
+(** [string_of_error err] produces a string representation of [err].
+  *)
+val string_of_error : forall 'a. Show 'a => error 'a -> string
+let string_of_error e =
+	match e with
+		| Fail err -> "Fail: " ^ err
+		| Success s -> show s
+	end
+
+instance forall 'a. Show 'a => (Show (error 'a))
+	let show = string_of_error
+end
+\ No newline at end of file