add itmap and itree_to_tree

[coq-hetmet.git] / src / General.v

diff --git a/src/General.v b/src/General.v
index 457b421..188a2dc 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -129,7 +129,14 @@ Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
     reflexivity.
     Qed.
 
-
+Open Scope string_scope.
+Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
+match t with
+  | T_Leaf None => "[]"
+  | T_Leaf (Some s) => "["+++s+++"]"
+  | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
+end.
+Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
 
 (*******************************************************************************)
 (* Lists                                                                       *)
@@ -582,7 +589,22 @@ Implicit Arguments INil    [ I F ].
 Implicit Arguments ILeaf   [ I F ].
 Implicit Arguments IBranch [ I F ].
 
+Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
+  induction il; intros; auto.
+  destruct a.
+  apply ILeaf.
+  apply f.
+  inversion X; auto.
+  apply INone.
+  apply IBranch; inversion X; auto.
+  Defined.
 
+Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
+  match il with
+  | INone     => []
+  | ILeaf _ a => [a]
+  | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
+  end.
 
 
 (*******************************************************************************)
@@ -633,6 +655,12 @@ Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 Variable eol : string.
 Extract Constant eol  => "'\n':[]".
 
+Class Monad {T:Type->Type} :=
+{ returnM : forall {a},     a -> T a
+; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
+}.
+Implicit Arguments Monad [ ].
+Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 
 (* the Error monad *)
 Inductive OrError (T:Type) :=
@@ -649,6 +677,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)
@@ -697,3 +737,9 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     rewrite e in v; apply OK; apply v.
     apply (Error (error_message (length l) n)).
     Defined.
+
+
+
+
+
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".