| (a::b) => (unleaves'' b),,(T_Leaf a)
end.
+Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
+ induction t.
+ destruct a; auto.
+ simpl.
+ rewrite IHt1.
+ rewrite IHt2.
+ rewrite map_app.
+ auto.
+ Qed.
+
Fixpoint filter {T:Type}(l:list ??T) : list T :=
match l with
| nil => nil
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.
(*******************************************************************************)
apply (Error (error_message (length l) n)).
Defined.
+(* Uniques *)
+Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
+Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".
+Variable uniqFromSupply : UniqSupply -> Unique. Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
+Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
+ Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
+Variable unique_eq : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
+ Extract Inlined Constant unique_eq => "(==)".
+Variable unique_toString : Unique -> string.
+ Extract Inlined Constant unique_toString => "show".
+Instance EqDecidableUnique : EqDecidable Unique :=
+ { eqd_dec := unique_eq }.
+Instance EqDecidableToString : ToString Unique :=
+ { toString := unique_toString }.
+
+Inductive UniqM {T:Type} : Type :=
+ | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
+ Implicit Arguments UniqM [ ].
+
+Instance UniqMonad : Monad UniqM :=
+{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
+; bindM := fun a b (x:UniqM a) (f:a->UniqM b) =>
+ uniqM (fun u =>
+ match x with
+ | uniqM fa =>
+ match fa u with
+ | Error s => Error s
+ | OK (u',va) => match f va with
+ | uniqM fb => fb u'
+ end
+ end
+ end)
+}.
+
+Definition getU : UniqM Unique :=
+ uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
+
+Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
+Notation "'return' x" := (returnM x) (at level 100).
+Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100).