clean up demo code

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

diff --git a/src/General.v b/src/General.v
index cf9d28d..ee5cb16 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -20,6 +20,24 @@ Class EqDecidable (T:Type) :=
 }.
 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 }.
@@ -88,6 +106,11 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre
   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
@@ -451,6 +474,16 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
   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                                                                  *)
 
@@ -492,6 +525,12 @@ Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
       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 =>
@@ -500,6 +539,47 @@ Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
       | 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                                                        *)
 
@@ -797,6 +877,8 @@ Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd 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.
@@ -884,6 +966,16 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->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".