X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FGeneral.v;h=f2e451f60b44ef7a203ac65db7ee1598abbef0dd;hb=af8dfc24d60a82c1229af9ffcddf704eec2d14ce;hp=4e73755be3425865f4e3cbaaaf14181f20cfe553;hpb=3d4dc42bf3f6e2ad7dc35b14ecb8facdb89e9324;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index 4e73755..f2e451f 100644
--- a/src/General.v
+++ b/src/General.v
@@ -23,6 +23,7 @@ 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).
 
 (*******************************************************************************)
@@ -41,6 +42,13 @@ Notation "[ q ]"    := (@T_Leaf (option _) (Some q))            : tree_scope.
 Notation "[ ]"      := (@T_Leaf (option _) None)                : tree_scope.
 Notation "[]"       := (@T_Leaf (option _) None)                : tree_scope.
 
+Fixpoint InT {A} (a:A) (t:Tree ??A) {struct t} : Prop :=
+  match t with
+    | T_Leaf None     => False
+    | T_Leaf (Some x) => x = a
+    | T_Branch b1 b2  => InT a b1 \/ InT a b2
+  end.
+
 Open Scope tree_scope.
 
 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
@@ -341,6 +349,11 @@ 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).
 
+Inductive distinctT {T:Type} : Tree ??T -> Prop :=
+| distinctT_nil  : distinctT []
+| distinctT_leaf : forall t, distinctT [t]
+| distinctT_cons : forall t1 t2, (forall v, InT v t1 -> InT v t2 -> False) -> distinctT (t1,,t2).
+
 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.
@@ -893,8 +906,29 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
 
 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
   admit.
-  Qed.
+  Defined.
 
 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
   admit.
   Defined.
+
+(* escapifies any characters which might cause trouble for LaTeX *)
+Variable sanitizeForLatex    : string      -> string.
+   Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
+Inductive Latex : Type := latex : string -> Latex.
+Instance LatexToString : ToString Latex := { toString := fun x => match x with latex s => s end }.
+Class ToLatex (T:Type) := { toLatex : T -> Latex }.
+Instance StringToLatex : ToLatex string := { toLatex := fun x => latex (sanitizeForLatex x) }.
+Instance LatexToLatex  : ToLatex Latex  := { toLatex := fun x => x }.
+Definition concatLatex {T1}{T2}(l1:T1)(l2:T2){L1:ToLatex T1}{L2:ToLatex T2} : Latex :=
+  match toLatex l1 with
+    latex s1 =>
+  match toLatex l2 with
+    latex s2 =>
+    latex (s1 +++ s2)
+    end
+    end.
+Notation "a +=+ b" := (concatLatex a b) (at level 60, right associativity).
+
+
+