X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=ae27b9f99cc725f7b68a5a2cf719e83421825146;hp=db77f344df6bf4e9361bf583700b048e2035fc56;hb=b59a8ad4356f9ab4e3a7f2b005a05d0f340ac018;hpb=327fd294a7a4d3c02b5491708aadcd9acef9e376

diff --git a/src/General.v b/src/General.v
index db77f34..ae27b9f 100644
--- a/src/General.v
+++ b/src/General.v
@@ -469,6 +469,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                                                                  *)
 
@@ -856,6 +866,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.
@@ -943,6 +955,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".