X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FGeneral.v;h=3c8252849faa7cbca0b3e22963216901e25adaef;hb=8efffc7368b5e54c42461f45a9708ff2828409a4;hp=b58bb96035057bbbf7a12b47b9ef351c03699266;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index b58bb96..3c82528 100644
--- a/src/General.v
+++ b/src/General.v
@@ -21,6 +21,10 @@ Class EqDecidable (T:Type) :=
 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                                                                       *)
 
@@ -525,6 +529,50 @@ Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 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 []
@@ -567,9 +615,24 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 
 
 
+
+
+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':[]".
+
 
 (* the Error monad *)
 Inductive OrError (T:Type) :=
@@ -586,6 +649,18 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
   end.
 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 
+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)