-

[clean-tests.git] / afp / a12 / testCash.icl

diff --git a/afp/a12/testCash.icl b/afp/a12/testCash.icl
deleted file mode 100644 (file)
index e234bfa..0000000
--- a/afp/a12/testCash.icl
+++ /dev/null
@@ -1,48 +0,0 @@
-module testCash
-
-import cashModel
-import gastyStart
-
-//gen{|Euro|} = [f {euro=e,cent=c}\\e<-[0..], c <- [0..99], f<-[id,(~)]]
-gen{|Euro|} = [f {euro=e,cent=c}\\e<-[0..], c <- merge [0..50] [51..99], f<-[id,(~)]]
-where
-       merge [a:x] ys = [a:merge ys x]
-       merge [] ys =ys
-derive string Euro, Product, []
-derive gen Product, []
-derive bimap []
-derive gEq Product
-
-pPlusAssociative :: Euro Euro Euro -> Equ
-pPlusAssociative a b c = a + (b + c) =.= (a + b) + c
-
-pPlusCommutative :: Euro Euro -> Equ
-pPlusCommutative a b = a + b =.= b + a
-
-pPlusIdentity :: Euro -> Equ
-pPlusIdentity i = i + zero =.= i
-
-pNegSub :: Euro -> Equ
-pNegSub i = zero - i =.= ~i
-
-pNegNegId :: Euro -> Equ
-pNegNegId i = ~ (~i) =.= i
-
-//model :: [Product] Action -> ([Product],[Euro])
-pFair :: [Product] Product -> Equ
-pFair state p = euro state =.= euro t - euro o
-where
-       (t,o) = model state (Rem p)
-//
-//pFair2 :: [Product] Action -> Equ //Euro
-//pFair2 state action = euro state =.= euro t - euro o
-//where (t,o) = model state action
-
-Start = flatten
-       [ ["pPlusAssociative: ":test pPlusAssociative]
-       , ["pPlusCommutative: ":test pPlusCommutative]
-       , ["pPlusIdentity: ":test pPlusIdentity]
-       , ["pNegSub: ":test pNegSub]
-       , ["pNegNegId: ":test pNegNegId]
-//     , ["pFair: ":test pFair]
-       ]