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]
	]