add distinct_decidable, in_decidable to General.v

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

diff --git a/src/General.v b/src/General.v
index 188a2dc..b0266f4 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -301,6 +301,16 @@ Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
     | (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
@@ -312,6 +322,50 @@ Inductive distinct {T:Type} : list T -> Prop :=
 | distinct_nil  : distinct nil
 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 
+Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
+  intros.
+  induction lv.
+  right.
+  unfold not.
+  intros.
+  inversion H.
+  destruct IHlv.
+  left.
+  simpl.
+  auto.
+  set (eqd_dec v a) as dec.
+  destruct dec.
+  subst.
+  left; simpl; auto.
+  right.
+  unfold not; intros.
+  destruct H.
+  subst.
+  apply n0; auto.
+  apply n.
+  apply H.
+  Defined.
+
+Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
+  intros.
+  induction lv.
+  left; apply distinct_nil.
+  destruct IHlv.
+  set (in_decidable a lv) as dec.
+  destruct dec.
+  right; unfold not; intros.
+  inversion H.
+  subst.
+  apply H2; auto.
+  left.
+  apply distinct_cons; auto.
+  right.
+  unfold not; intros.
+  inversion H.
+  subst.
+  apply n; auto.
+  Defined.
+
 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
   induction l; auto.
   simpl.
@@ -738,7 +792,59 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     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).
+
+
+
+
+
+
+Record FreshMonad {T:Type} :=
+{ FMT       :  Type -> Type
+; FMT_Monad :> Monad FMT
+; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
+}.
+Implicit Arguments FreshMonad [ ].
+Coercion FMT       : FreshMonad >-> Funclass.