update

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

diff --git a/afp/a12/testCash.icl b/afp/a12/testCash.icl
new file mode 100644 (file)
index 0000000..e234bfa
--- /dev/null
+++ b/afp/a12/testCash.icl
@@ -0,0 +1,48 @@
+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]
+       ]