Added logo

--HG--
rename : README => README.md

Makefile

@@ -228,10 +228,12 @@ quickcheck: integration
 	cd $(XMONADDIR); dist/build/xmonad/xmonad --run-tests
 
 theorems:
-	@echo 'Total quickcheck properties defined: 111'
-	@echo -n 'Total theorems proven: '
+	@echo -n 'Total theorems stated: '
 	@grep Theorem src/Properties.v | wc -l
-
+	@echo -n 'Total theorems admitted: '
+	@grep Admitted src/Properties.v | wc -l
+	@echo -n 'Remaing theorems: '
+	@wc -l src/properties.txt
 printenv: 
 	@echo CAMLC =	$(CAMLC)
 	@echo CAMLOPTC =	$(CAMLOPTC)

src/Properties.v

@@ -612,3 +612,128 @@ Theorem prop_focusMaster_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l
     apply (Permutation_refl).
     Admitted.
 
+Ltac destruct_stackset x := destruct x; destruct getCurrent; destruct getWorkspace; destruct getStack.
+
+Theorem prop_mapLayoutId (s : stackSet i l a sd) :
+  mapLayout (fun x => x) s = s.
+  Proof.
+    destruct s; destruct getCurrent; destruct getWorkspace.
+    apply stackSet_eq; try reflexivity.
+    induction getVisible.
+    reflexivity.
+    simpl in *.
+    destruct a0.
+    destruct getWorkspace.
+    rewrite IHgetVisible.
+    reflexivity.
+    simpl.
+    induction getHidden; try reflexivity.
+    simpl; rewrite IHgetHidden; destruct a0; reflexivity.
+  Qed.
+
+Theorem prop_mapLayoutInverse (s : stackSet i nat a sd) :
+  mapLayout pred (mapLayout S s) = s.
+  Proof.
+    destruct s.
+    simpl.
+    f_equal.
+    destruct getCurrent.
+    f_equal.
+    destruct getWorkspace.
+    reflexivity.
+    induction getVisible.
+    reflexivity.
+    destruct a0.
+    simpl.
+    rewrite IHgetVisible.
+    destruct getWorkspace.
+    reflexivity.
+    induction getHidden; try reflexivity.
+    destruct a0; simpl; rewrite IHgetHidden; reflexivity.
+  Qed.
+
+Definition predTag (w : workspace nat l a) : workspace nat l a :=
+  match w with
+    | Workspace t l s => Workspace (pred t) l s
+  end.
+
+Definition succTag (w : workspace nat l a) : workspace nat l a :=
+  match w with
+    | Workspace t l s => Workspace (S t) l s
+  end.
+
+Theorem prop_mapWorkspaceInverse (s : stackSet nat l a sd) :
+  mapWorkspace predTag (mapWorkspace succTag s) = s.
+  Proof.
+    destruct s; destruct getCurrent; destruct getWorkspace.
+    unfold mapWorkspace.
+    f_equal.
+    induction getVisible; try reflexivity.
+    simpl; destruct a0; rewrite IHgetVisible; unfold predTag; unfold succTag; simpl. 
+    destruct getWorkspace. reflexivity.
+    induction getHidden; try reflexivity.
+    destruct a0.
+    simpl. rewrite IHgetHidden.
+    reflexivity.
+  Qed.
+
+Theorem prop_screens (s : stackSet i l a sd) :
+  In (getCurrent s) (screens s).
+  Proof.
+    destruct s.
+    destruct getCurrent; left; reflexivity.
+  Qed.
+
+Theorem prop_lookup_current (x : stackSet i l a sd) :
+  lookupWorkspace (getScreen (getCurrent x)) x = Some (getTag (getWorkspace (getCurrent x))).
+  Proof.
+    destruct x.
+    destruct getCurrent.
+    simpl.
+    unfold lookupWorkspace.
+    simpl.
+    destruct (beqsid getScreen getScreen) as [b T].
+    destruct b.
+    reflexivity.
+    exfalso; apply T; reflexivity.
+  Qed.
+
+Theorem prop_lookup_visible (x : stackSet i l a sd) : 
+  getVisible x <> nil ->
+  (forall (x y : screen i l a sd), getScreen x = getScreen y -> x = y) -> (* the StackSet invariant *)
+  match last (map (fun x => Some (getScreen x)) (getVisible x)) None with
+    | None => True
+    | Some sc =>
+      In (lookupWorkspace sc x) (map (fun x => Some (getTag (getWorkspace x))) (getVisible x))
+  end.
+  Proof.
+    remember (last (map (fun x => Some (getScreen x)) (getVisible x)) None).
+    destruct y; try trivial.
+    intros F; induction getVisible as [ | y ys].
+    exfalso; apply F; reflexivity.
+    induction ys as [ | z zs].
+    left.
+    destruct x.
+    unfold lookupWorkspace.
+    simpl.
+    injection Heqy.
+    intros Eq.
+    rewrite Eq.
+    destruct (beqsid (getScreen y) (getScreen getCurrent)) as [b B].
+    destruct b; simpl in *.
+    rewrite (H _ _ B).
+    destruct getCurrent; reflexivity.
+    Focus 2.
+    intros H.
+    right.
+    apply IHys.
+    assumption.
+    discriminate.
+    assumption.
+    destruct y.
+    simpl in *.
+    destruct getCurrent.
+    simpl in *.
+  Admitted.
+
+

src/discarded.txt

@@ -0,0 +1,18 @@
+ -- Not about stacksets but about Xmonad.Layout
+        ,("tile 1 window fullsize", mytest prop_tile_fullscreen)
+        ,("tiles never overlap",    mytest prop_tile_non_overlap)
+        ,("split hozizontally",     mytest prop_split_hoziontal)
+        ,("split verticalBy",       mytest prop_splitVertically)
+        ,("pure layout tall",       mytest prop_purelayout_tall)
+        ,("send shrink    tall",    mytest prop_shrink_tall)
+        ,("send expand    tall",    mytest prop_expand_tall)
+        ,("send incmaster tall",    mytest prop_incmaster_tall)
+        ,("pure layout full",       mytest prop_purelayout_full)
+        ,("send message full",      mytest prop_sendmsg_full)
+        ,("describe full",          mytest prop_desc_full)
+        ,("describe mirror",        mytest prop_desc_mirror)
+-- about Xmonad.Operations
+        ,("window hints: inc",      mytest prop_resize_inc)
+        ,("window hints: inc all",  mytest prop_resize_inc_extra)
+        ,("window hints: max",      mytest prop_resize_max)
+        ,("window hints: max all ", mytest prop_resize_max_extra)

src/properties.txt

@@ -0,0 +1,73 @@
+       [("StackSet invariants" , mytest prop_invariant)
+        ,("empty: invariant"    , mytest prop_empty_I)
+        ,("empty is empty"      , mytest prop_empty)
+        ,("empty / current"     , mytest prop_empty_current)
+        ,("empty / member"      , mytest prop_member_empty)
+        ,("view : invariant"    , mytest prop_view_I)
+        ,("view sets current"   , mytest prop_view_current)
+        ,("view idempotent"     , mytest prop_view_idem)
+        ,("view reversible"    , mytest prop_view_reversible)
+        ,("view is local"       , mytest prop_view_local)
+        ,("greedyView : invariant"    , mytest prop_greedyView_I)
+        ,("greedyView sets current"   , mytest prop_greedyView_current)
+        ,("greedyView is safe "   ,   mytest prop_greedyView_current_id)
+        ,("greedyView idempotent"     , mytest prop_greedyView_idem)
+        ,("greedyView reversible"     , mytest prop_greedyView_reversible)
+        ,("greedyView is local"       , mytest prop_greedyView_local)
+        ,("peek/member "        , mytest prop_member_peek)
+        ,("index/length"        , mytest prop_index_length)
+        ,("focus master : invariant", mytest prop_focusMaster_I)
+        ,("focusWindow: invariant", mytest prop_focus_I)
+        ,("focus left/master"   , mytest prop_focus_left_master)
+        ,("focus right/master"  , mytest prop_focus_right_master)
+        ,("focus master/master"  , mytest prop_focus_master_master)
+        ,("focusWindow master"  , mytest prop_focusWindow_master)
+        ,("focus all left  "    , mytest prop_focus_all_l)
+        ,("focus all right "    , mytest prop_focus_all_r)
+        ,("focus master idemp"  , mytest prop_focusMaster_idem)
+        ,("focusWindow is local", mytest prop_focusWindow_local)
+        ,("focusWindow works"   , mytest prop_focusWindow_works)
+        ,("focusWindow identity", mytest prop_focusWindow_identity)
+        ,("findTag"           , mytest prop_findIndex)
+        ,("allWindows/member"   , mytest prop_allWindowsMember)
+        ,("currentTag"          , mytest prop_currentTag)
+        ,("insert: invariant"   , mytest prop_insertUp_I)
+        ,("insert/new"          , mytest prop_insert_empty)
+        ,("insert is idempotent", mytest prop_insert_idem)
+        ,("insert is reversible", mytest prop_insert_delete)
+        ,("insert duplicates"   , mytest prop_insert_duplicate)
+        ,("insert/peek "        , mytest prop_insert_peek)
+        ,("insert/size"         , mytest prop_size_insert)
+        ,("delete: invariant"   , mytest prop_delete_I)
+        ,("delete/empty"        , mytest prop_empty)
+        ,("delete/member"       , mytest prop_delete)
+        ,("delete is reversible", mytest prop_delete_insert)
+        ,("delete is local"     , mytest prop_delete_local)
+        ,("delete/focus"        , mytest prop_delete_focus)
+        ,("delete  last/focus up", mytest prop_delete_focus_end)
+        ,("delete ~last/focus down", mytest prop_delete_focus_not_end)
+        ,("filter preserves order", mytest prop_filter_order)
+        ,("swapUp: invariant" , mytest prop_swap_left_I)
+        ,("swapDown: invariant", mytest prop_swap_right_I)
+        ,("swapUp id on focus", mytest prop_swap_left_focus)
+        ,("swap all left  "     , mytest prop_swap_all_l)
+        ,("swap all right "     , mytest prop_swap_all_r)
+        ,("shiftMaster id on focus", mytest prop_shift_master_focus)
+        ,("shiftMaster is idempotent", mytest prop_shift_master_idempotent)
+        ,("shiftMaster preserves ordering", mytest prop_shift_master_ordering)
+        ,("shift: invariant"    , mytest prop_shift_I)
+        ,("shift is reversible" , mytest prop_shift_reversible)
+        ,("shiftWin: invariant" , mytest prop_shift_win_I)
+        ,("shiftWin is shift on focus" , mytest prop_shift_win_focus)
+        ,("shiftWin fix current" , mytest prop_shift_win_fix_current)
+        ,("floating is reversible" , mytest prop_float_reversible)
+        ,("floating sets geometry" , mytest prop_float_geometry)
+        ,("floats can be deleted", mytest prop_float_delete)
+        ,("screens includes current", mytest prop_screens)
+        ,("lookupTagOnScreen", mytest prop_lookup_current)
+        ,("lookupTagOnVisbleScreen", mytest prop_lookup_visible)
+        ,("screens works",      mytest prop_screens_works)
+        ,("renaming works",     mytest prop_rename1)
+        ,("ensure works",     mytest prop_ensure)
+        ,("ensure hidden semantics",     mytest prop_ensure_append)
+        ,("shiftWin identity",      mytest prop_shift_win_indentity)