X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FGeneral.v;h=3c8252849faa7cbca0b3e22963216901e25adaef;hb=273645efdb974dd04042e6c59bbedbe0ad658298;hp=7af1fc3897e9621760520584e368afb297f19f75;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index 7af1fc3..3c82528 100644
--- a/src/General.v
+++ b/src/General.v
@@ -629,6 +629,10 @@ CoInductive Fresh A T :=
 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 
 
+(* string stuff *)
+Variable eol : string.
+Extract Constant eol  => "'\n':[]".
+
 
 (* the Error monad *)
 Inductive OrError (T:Type) :=
@@ -645,6 +649,18 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
   end.
 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 
+Open Scope string_scope.
+Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
+  match oe with
+    | Error s => Error (err_msg +++ eol +++ "  " +++ s)
+    | OK    t => f t
+  end.
+
+Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
+
+Definition addErrorMessage s {T} (x:OrError T) :=
+  x >>=[ s ] (fun y => OK y).
+
 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 | Indexed_OK    : forall t, f t -> Indexed f (OK t)