Add ErrorT monad, and Show class

1 files changed, 23 insertions, 0 deletions

diff --git a/src/Util/ErrorT.v b/src/Util/ErrorT.v
new file mode 100644
index 000000000..ab8634e2c
--- /dev/null
+++ b/src/Util/ErrorT.v
@@ -0,0 +1,23 @@
+Require Import Crypto.Util.Notations.
+
+Inductive ErrorT {ErrT T} :=
+| Success (v : T)
+| Error (msg : ErrT).
+
+Global Arguments ErrorT : clear implicits.
+Delimit Scope error_scope with error.
+Bind Scope error_scope with ErrorT.
+
+Definition invert_result {ErrT T} (v : ErrorT ErrT T)
+  := match v return match v with Success _ => T | _ => ErrT end with
+     | Success v => v
+     | Error msg => msg
+     end.
+
+Definition bind {A B ErrT} (x : ErrorT ErrT A) (k : A -> ErrorT ErrT B) : ErrorT ErrT B
+  := match x with
+     | Success v => k v
+     | Error msg => Error msg
+     end.
+
+Notation "x <- y ; f" := (bind y (fun x => f%error)) : error_scope.