Generalizable All Variables.
Require Import Omega.
-
+Definition EqDecider T := forall (n1 n2:T), sumbool (n1=n2) (not (n1=n2)).
Class EqDecidable (T:Type) :=
{ eqd_type := T
; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
-; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _))
}.
Coercion eqd_type : EqDecidable >-> Sortclass.
+Class ToString (T:Type) := { toString : T -> string }.
+Instance StringToString : ToString string := { toString := fun x => x }.
+Notation "a +++ b" := (append (toString a) (toString b)) (at level 100).
+
(*******************************************************************************)
(* Trees *)
inversion H; auto.
Defined.
-
-
+Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
+ (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)).
+ induction l.
+ destruct a.
+ reflexivity.
+ reflexivity.
+ simpl.
+ rewrite IHl1.
+ rewrite IHl2.
+ reflexivity.
+ Qed.
+
+Open Scope string_scope.
+Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
+match t with
+ | T_Leaf None => "[]"
+ | T_Leaf (Some s) => "["+++s+++"]"
+ | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
+end.
+Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
(*******************************************************************************)
(* Lists *)
auto.
Defined.
-
-
+Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
+ apply Build_EqDecidable.
+ intros.
+ apply list_eq_dec.
+ apply eqd_dec.
+ Defined.
(*******************************************************************************)
(* Length-Indexed Lists *)
inversion v; subst; auto.
Defined.
+Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
+ induction v; auto.
+ simpl.
+ omega.
+ Qed.
+
+Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
+ induction v; auto.
+ simpl. rewrite IHv.
+ reflexivity.
+ Qed.
+
+Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
+ induction v; auto.
+ set (vec2list (list2vec (a :: v))) as q.
+ rewrite <- IHv.
+ unfold q.
+ clear q.
+ simpl.
+ reflexivity.
+ Qed.
+
Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
Implicit Arguments INil [ I F ].
Implicit Arguments ICons [ I F ].
+Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
+
+Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
+ intro il.
+ inversion il.
+ subst.
+ apply X.
+ Defined.
+
+Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
+ intro il.
+ inversion il.
+ subst.
+ apply X0.
+ Defined.
+
+Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
+ induction il; intros; auto.
+ apply INil.
+ inversion X; subst.
+ apply ICons; auto.
+ Defined.
+
+Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
+ induction l1; auto.
+ apply INil.
+ apply ICons.
+ inversion v; auto.
+ apply IHl1.
+ inversion v; auto.
+ Defined.
+
+Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
+ induction l1; auto.
+ apply IHl1.
+ inversion v; subst; auto.
+ Defined.
+
+Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
+ match il with
+ | INil => nil
+ | a::::b => a::(ilist_to_list b)
+ end.
+
(* a tree indexed by a (Tree (option X)) *)
Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
| INone : ITree I F []
+CoInductive Fresh A T :=
+{ next : forall a:A, (T a * Fresh A T)
+; split : Fresh A T * Fresh A T
+}.
+
+
+
+
+
+Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
+
+
+(* string stuff *)
+Variable eol : string.
+Extract Constant eol => "'\n':[]".
+
+Class Monad {T:Type->Type} :=
+{ returnM : forall {a}, a -> T a
+; bindM : forall {a}{b}, T a -> (a -> T b) -> T b
+}.
+Implicit Arguments Monad [ ].
+Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
(* the Error monad *)
Inductive OrError (T:Type) :=
end.
Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
-Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) :=
- match n as N return ???(vec _ N) with
- | O => match l with
- | nil => OK vec_nil
- | _ => Error "list2vecOrError: list was too long"
- end
- | S n' => match l with
- | nil => Error "list2vecOrError: list was too short"
- | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'')
- end
+Open Scope string_scope.
+Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
+ match oe with
+ | Error s => Error (err_msg +++ eol +++ " " +++ s)
+ | OK t => f t
end.
+Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
+
+Definition addErrorMessage s {T} (x:OrError T) :=
+ x >>=[ s ] (fun y => OK y).
+
Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
| Indexed_Error : forall error_message:string, Indexed f (Error error_message)
| Indexed_OK : forall t, f t -> Indexed f (OK t)
.
-Ltac xauto := try apply Indexed_Error; try apply Indexed_OK.
-
-
-
+Require Import Coq.Arith.EqNat.
+Instance EqDecidableNat : EqDecidable nat.
+ apply Build_EqDecidable.
+ intros.
+ apply eq_nat_dec.
+ Defined.
(* for a type with decidable equality, we can maintain lists of distinct elements *)
Section DistinctList.
| cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
end.
End DistinctList.
+
+Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
+ set (list2vec l) as v.
+ destruct (eqd_dec (length l) n).
+ rewrite e in v; apply OK; apply v.
+ apply (Error (error_message (length l) n)).
+ Defined.
+
+
+
+
+
+Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".