Permalink
Browse files

Moved from svn to hg.

  • Loading branch information...
0 parents commit 5f5cda8d0b7c7ce92b3a79ed27152960ae34903d Wouter Swierstra committed Dec 12, 2011
Showing with 1,586 additions and 0 deletions.
  1. +245 −0 Makefile
  2. +2 −0 scripts/cabal.patch
  3. +12 −0 scripts/core.patch
  4. +18 −0 scripts/operations.patch
  5. +32 −0 scripts/properties.patch
  6. +6 −0 scripts/sedscript
  7. +88 −0 src/Aux.v
  8. +84 −0 src/Extraction.v
  9. +466 −0 src/Properties.v
  10. +470 −0 src/StackSet.v
  11. +163 −0 src/StackSetHeader.hs
245 Makefile
@@ -0,0 +1,245 @@
+#############################################################################
+## v # The Coq Proof Assistant ##
+## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
+## \VV/ # ##
+## // # Makefile automagically generated by coq_makefile V8.3 ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile src/Aux.v src/StackSet.v src/Extraction.v -I src
+#
+
+#
+# This Makefile may take 3 arguments passed as environment variables:
+# - COQBIN to specify the directory where Coq binaries resides;
+# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
+COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
+CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
+ifndef CAMLP4BIN
+ CAMLP4BIN:=$(CAMLBIN)
+endif
+
+CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
+
+##########################
+# #
+# Libraries definitions. #
+# #
+##########################
+
+OCAMLLIBS:=-I src
+COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
+ -I $(COQLIB)/library -I $(COQLIB)/parsing \
+ -I $(COQLIB)/pretyping -I $(COQLIB)/interp \
+ -I $(COQLIB)/proofs -I $(COQLIB)/tactics \
+ -I $(COQLIB)/toplevel \
+ -I $(COQLIB)/plugins/cc \
+ -I $(COQLIB)/plugins/dp \
+ -I $(COQLIB)/plugins/extraction \
+ -I $(COQLIB)/plugins/field \
+ -I $(COQLIB)/plugins/firstorder \
+ -I $(COQLIB)/plugins/fourier \
+ -I $(COQLIB)/plugins/funind \
+ -I $(COQLIB)/plugins/groebner \
+ -I $(COQLIB)/plugins/interface \
+ -I $(COQLIB)/plugins/micromega \
+ -I $(COQLIB)/plugins/nsatz \
+ -I $(COQLIB)/plugins/omega \
+ -I $(COQLIB)/plugins/quote \
+ -I $(COQLIB)/plugins/ring \
+ -I $(COQLIB)/plugins/romega \
+ -I $(COQLIB)/plugins/rtauto \
+ -I $(COQLIB)/plugins/setoid_ring \
+ -I $(COQLIB)/plugins/subtac \
+ -I $(COQLIB)/plugins/subtac/test \
+ -I $(COQLIB)/plugins/syntax \
+ -I $(COQLIB)/plugins/xml
+COQLIBS:=-I src
+COQDOCLIBS:=
+
+##########################
+# #
+# Variables definitions. #
+# #
+##########################
+
+ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+OPT:=
+COQFLAGS:= $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+ifdef CAMLBIN
+ COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
+endif
+COQC:=$(COQBIN)coqc
+COQDEP:=$(COQBIN)coqdep -c
+GALLINA:=$(COQBIN)gallina
+COQDOC:=$(COQBIN)coqdoc
+COQMKTOP:=$(COQBIN)coqmktop
+CAMLLIB:=$(shell $(CAMLBIN)ocamlc.opt -where)
+CAMLC:=$(CAMLBIN)ocamlc.opt -c -rectypes
+CAMLOPTC:=$(CAMLBIN)ocamlopt.opt -c -rectypes
+CAMLLINK:=$(CAMLBIN)ocamlc.opt -rectypes
+CAMLOPTLINK:=$(CAMLBIN)ocamlopt.opt -rectypes
+GRAMMARS:=grammar.cma
+CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
+CAMLP4OPTIONS:=
+PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
+
+BUILDDIR:=build
+XMONADDIR:=$(BUILDDIR)/xmonad-0.9.2/
+
+###################################
+# #
+# Definition of the "all" target. #
+# #
+###################################
+
+EXTRACTION_FILE:=src/Extraction.v
+VFILES:=src/Aux.v\
+ src/StackSet.v\
+ src/Properties.v
+VOFILES:=$(VFILES:.v=.vo)
+VOFILES0:=$(filter-out ,$(VOFILES))
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+SEDSCRIPT:=scripts/sedscript
+HSFILE:=StackSet.hs
+HSHEADER:=src/StackSetHeader.hs
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+
+#GET RID OF THESE FILES
+#HSFILES+=Datatypes.hs List.hs Logic.hs Peano_dec.hs Specif.hs Sumbool.hs
+
+all: $(VOFILES)
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+ - mkdir -p html
+ $(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+ - mkdir -p html
+ $(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+ $(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.ps: $(VFILES)
+ $(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+ $(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.pdf: $(VFILES)
+ $(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+
+
+####################
+# #
+# Special targets. #
+# #
+####################
+
+.PHONY: all opt byte archclean clean install depend html
+
+%.vo %.glob: %.v
+ $(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+ $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+ $(GALLINA) $<
+
+%.tex: %.v
+ $(COQDOC) -latex $< -o $@
+
+%.html: %.v %.glob
+ $(COQDOC) -html $< -o $@
+
+%.g.tex: %.v
+ $(COQDOC) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+ $(COQDOC) -html -g $< -o $@
+
+%.v.d: %.v
+ $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+byte:
+ $(MAKE) all "OPT:=-byte"
+
+opt:
+ $(MAKE) all "OPT:=-opt"
+
+install:
+ mkdir -p $(COQLIB)/user-contrib
+ (for i in $(VOFILES0); do \
+ install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \
+ install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \
+ done)
+
+clean:
+ rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(HSFILE) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
+ rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
+ - rm -rf html $(BUILDDIR)
+
+archclean:
+ rm -f *.cmx *.o
+
+patched_xmonad:
+ mkdir -p $(BUILDDIR)
+ curl http://hackage.haskell.org/packages/archive/xmonad/0.9.2/xmonad-0.9.2.tar.gz\
+ -o $(BUILDDIR)/xmonad-0.9.2.tar.gz
+ cd $(BUILDDIR); tar zxf xmonad-0.9.2.tar.gz
+ patch $(XMONADDIR)/xmonad.cabal -i scripts/cabal.patch
+ patch $(XMONADDIR)/XMonad/Core.hs -i scripts/core.patch
+ patch $(XMONADDIR)/XMonad/Operations.hs -i scripts/operations.patch
+ patch $(XMONADDIR)/tests/Properties.hs -i scripts/properties.patch
+
+extraction: patched_xmonad
+ mkdir -p $(BUILDDIR)
+ $(MAKE) all
+ $(COQC) $(COQFLAGS) $(EXTRACTION_FILE)
+ cp $(HSHEADER) $(XMONADDIR)/XMonad/$(HSFILE)
+ sed -f $(SEDSCRIPT) $(HSFILE) >> $(XMONADDIR)/XMonad/$(HSFILE)
+ rm $(HSFILE)
+
+integration: extraction
+ cd $(XMONADDIR); cabal configure --flags="testing"; cabal build
+
+quickcheck: integration
+ cd $(XMONADDIR); dist/build/xmonad/xmonad --run-tests
+
+theorems:
+ @echo 'Total quickcheck properties defined: 111'
+ @echo -n 'Total theorems proven: '
+ @grep Theorem src/Properties.v | wc -l
+
+printenv:
+ @echo CAMLC = $(CAMLC)
+ @echo CAMLOPTC = $(CAMLOPTC)
+ @echo CAMLP4LIB = $(CAMLP4LIB)
+
+-include $(VFILES:.v=.v.d)
+.SECONDARY: $(VFILES:.v=.v.d)
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
@@ -0,0 +1,2 @@
+88d87
+< ghc-options: -Werror
@@ -0,0 +1,12 @@
+23c23
+< ScreenId(..), ScreenDetail(..), XState(..),
+---
+> ScreenDetail(..), XState(..),
+109c109
+< type WindowSet = StackSet WorkspaceId (Layout Window) Window ScreenId ScreenDetail
+---
+> type WindowSet = StackSet WorkspaceId (Layout Window) Window ScreenDetail
+115,117d114
+< -- | Physical screen indices
+< newtype ScreenId = S Int deriving (Eq,Ord,Show,Read,Enum,Num,Integral,Real)
+<
@@ -0,0 +1,18 @@
+131,132c131,132
+< >>= W.filter (`M.notMember` W.floating ws)
+< >>= W.filter (`notElem` vis)
+---
+> >>= W.filterStack (`M.notMember` W.floating ws)
+> >>= W.filterStack (`notElem` vis)
+376c376
+< screenWorkspace :: ScreenId -> X (Maybe WorkspaceId)
+---
+> screenWorkspace :: W.ScreenId -> X (Maybe WorkspaceId)
+424c424
+< floatLocation :: Window -> X (ScreenId, W.RationalRect)
+---
+> floatLocation :: Window -> X (W.ScreenId, W.RationalRect)
+442c442
+< -> X (Maybe (W.Screen WorkspaceId (Layout Window) Window ScreenId ScreenDetail))
+---
+> -> X (Maybe (W.Screen WorkspaceId (Layout Window) Window ScreenDetail))
@@ -0,0 +1,32 @@
+4c4
+< import XMonad.StackSet hiding (filter)
+---
+> import XMonad.StackSet
+8d7
+< import qualified XMonad.StackSet as S (filter)
+42,43c41,42
+< instance (Integral i, Integral s, Eq a, Arbitrary a, Arbitrary l, Arbitrary sd)
+< => Arbitrary (StackSet i l a s sd) where
+---
+> instance (Integral i, Integral s, Eq a, Arbitrary a, Arbitrary l, Arbitrary s)
+> => Arbitrary (StackSet i l a s) where
+70c69
+< fromList :: (Integral i, Integral s, Eq a) => (i, [sd], [Maybe Int], [[a]], l) -> StackSet i l a s sd
+---
+> fromList :: (Integral i, Integral s, Eq a) => (i, [s], [Maybe Int], [[a]], l) -> StackSet i l a s
+87c86
+< type T = StackSet (NonNegative Int) Int Char Int Int
+---
+> type T = StackSet (NonNegative Int) Int Char Int
+477c476
+< Just s@(Stack i _ _) -> integrate' (S.filter (/= i) s) == filter (/= i) (integrate' (Just s))
+---
+> Just s@(Stack _ i _) -> integrate' (filterStack (/= i) s) == filter (/= i) (integrate' (Just s))
+594c593
+< else (differentiate xs) == Just (Stack (head xs) [] (tail xs))
+---
+> else (differentiate xs) == Just (Stack [] (head xs) (tail xs))
+979c978
+< ,("new fails with abort", mytest prop_new_abort)
+---
+> -- ,("new fails with abort", mytest prop_new_abort)
@@ -0,0 +1,6 @@
+1,4d
+s/delete :: /delete :: Ord a3 => /g
+s/remove0 :: /remove0 :: Ord a1 => /g
+s/insert :: /insert :: Ord a1 => /g
+s/sink :: /sink :: Ord a3 => /g
+s/float ::/float :: Ord a3=> /g
Oops, something went wrong.

0 comments on commit 5f5cda8

Please sign in to comment.