}.
Coercion eqd_type : EqDecidable >-> Sortclass.
+Instance EqDecidableOption (T:Type)(EQDT:EqDecidable T) : EqDecidable ??T.
+ apply Build_EqDecidable.
+ intros.
+ destruct v1;
+ destruct v2.
+ destruct (eqd_dec t t0).
+ subst.
+ left; auto.
+ right.
+ unfold not; intros.
+ inversion H.
+ subst.
+ apply n.
+ auto.
+ right; unfold not; intro; inversion H.
+ right; unfold not; intro; inversion H.
+ left; auto.
+ Defined.
Class ToString (T:Type) := { toString : T -> string }.
Instance StringToString : ToString string := { toString := fun x => x }.
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
apply eqd_dec.
Defined.
+Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string :=
+ match l with
+ | nil => "nil"
+ | a::b => (toString a) +++ "::" +++ listToString b
+ end.
+
+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 =>
| Some x => f x
end.
+(* decidable quality on a tree of elements which have decidable equality *)
+Definition tree_eq_dec : forall {T:Type}(l1 l2:Tree T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
+ sumbool (eq l1 l2) (not (eq l1 l2)).
+ intro T.
+ intro l1.
+ induction l1; intros.
+ destruct l2.
+ destruct (dec a t).
+ subst.
+ left; auto.
+ right; unfold not; intro; apply n; inversion H; auto.
+ right.
+ unfold not; intro.
+ inversion H.
+
+ destruct l2.
+ right; unfold not; intro; inversion H.
+ destruct (IHl1_1 l2_1 dec);
+ destruct (IHl1_2 l2_2 dec); subst.
+ left; auto.
+ right.
+ unfold not; intro.
+ inversion H; subst.
+ apply n; auto.
+ right.
+ unfold not; intro.
+ inversion H; subst.
+ apply n; auto.
+ right.
+ unfold not; intro.
+ inversion H; subst.
+ apply n; auto.
+ Defined.
+
+Instance EqDecidableTree {T:Type}(eqd:EqDecidable T) : EqDecidable (Tree T).
+ apply Build_EqDecidable.
+ intros.
+ apply tree_eq_dec.
+ apply eqd_dec.
+ Defined.
+
(*******************************************************************************)
(* Length-Indexed Lists *)
(* 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".