end.
Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
+Lemma mapOptionTree_distributes
+ : forall T R (a b:Tree ??T) (f:T->R),
+ mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
+ reflexivity.
+ Qed.
Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
match tt with
Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
{ toString := @listToString _ _ }.
+
(*******************************************************************************)
(* Tree Flags *)
end
end.
+Definition takeT' {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
+ match takeT tf with
+ | None => []
+ | Some x => x
+ end.
+
(* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *)
Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
fun t =>
(* boolean "not" *)
Definition bnot (b:bool) : bool := if b then false else true.
+Definition band (b1 b2:bool) : bool := if b1 then b2 else false.
+Definition bor (b1 b2:bool) : bool := if b1 then true else b2.
(* string stuff *)
Variable eol : string.
apply (Error (error_message (length l) n)).
Defined.
+(* this makes a type function application, ensuring not to oversaturate it (though if it was undersaturated we can't fix that) *)
+Fixpoint split_list {T}(l:list T)(n:nat) : ???(list T * list T) :=
+ match n with
+ | O => OK (nil , l)
+ | S n' => match l with
+ | nil => Error "take_list failed"
+ | h::t => split_list t n' >>= fun t' => let (t1,t2) := t' in OK ((h::t1),t2)
+ end
+ end.
+
(* Uniques *)
Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".