implementation module cashModel
/*
	Pieter Koopman, Radboud University, 2017
	pieter@cs.ru.nl
	Advanced programming

	A simple state model for an automated cash register
*/

import StdEnv, GenEq
import gastje
from Data.Func import mapSt
import Data.Tuple

class euro a :: a -> Euro
instance euro Product
where
	euro Pizza = euro (4,99)
	euro Beer  = euro (0,65)
	euro _     = euro 1

instance euro Int where euro e = {euro = e, cent = 0}
instance euro (Int, Int) where euro (e,c) = {euro = e, cent = c}
instance euro [e] | euro e where euro l = sum (map euro l)
instance euro Euro where euro e = e

instance + Euro
where
	+ x y = {euro = c / 100, cent = (abs c) rem 100}
	where
		c = (x.euro + y.euro) * 100 + sign x.euro * x.cent + sign y.euro * y.cent

instance - Euro
where
	- x y = {euro = c / 100, cent = (abs c) rem 100}
	where
		c = (x.euro - y.euro) * 100 + sign x.euro * x.cent - sign y.euro * y.cent

instance zero Euro where zero = {euro = 0, cent = 0}
derive gEq Euro, Product
instance == Product where (==) p q = p === q
instance == Euro where (==) p q = p === q

instance ~ Euro where ~ e = {e & euro = ~e.euro}

model :: [Product] Action -> ([Product],[Euro])
model list (Add p) = ([p:list],[euro p])
model list (Rem p)
| isMember p list = (removeMember p list,[~ (euro p)])
| otherwise       = (list,[])
model list Pay = ([],[euro list])

derive gEq Action
derive gen Euro, Action, Product, []
derive string Euro, Action, Product, []
derive bimap []

/**
 * plus_zero_is_identity:          Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
 * plus_is_commutative:            Passed
 * minus_zero_is_identity:         Fail for: {Euro|euro=0, cent=1} ; {Euro|euro=0, cent=1} <> {Euro|euro=0, cent=0}
 * prop_double_neg_is_identity:    Passed
 * prop_neg_is_not_identity:       Fail for: {Euro|euro=0, cent=1}
 * prop_minus_is_plus_after_neg:   Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=0, cent=99} <> {Euro|euro=1, cent=1}
 * prop_neg_distributes_over_plus: Fail for: {Euro|euro=1, cent=0} {Euro|euro=-9223372036854775808, cent=1} ; {Euro|euro=-1, cent=1} <> {Euro|euro=0, cent=99}
 * prop_plus_minus_is_identity:    Fail for: {Euro|euro=0, cent=1} {Euro|euro=0, cent=0} ; {Euro|euro=0, cent=0} <> {Euro|euro=0, cent=1}
 */
Start =
	[ ["plus_zero_is_identity:          ": test prop_plus_zero_is_identity]
	, ["plus_is_commutative:            ": test prop_plus_is_commutative]
	, ["minus_zero_is_identity:         ": test prop_minus_zero_is_identity]
	, ["prop_double_neg_is_identity:    ": test prop_double_neg_is_identity]
	, ["prop_neg_is_not_identity:       ": test prop_neg_is_not_identity]
	, ["prop_minus_is_plus_after_neg:   ": test prop_minus_is_plus_after_neg]
	, ["prop_neg_distributes_over_plus: ": test prop_neg_distributes_over_plus]
	, ["prop_plus_minus_is_identity:    ": test prop_plus_minus_is_identity]
	]
where
	prop_plus_zero_is_identity :: Euro -> Property
	prop_plus_zero_is_identity e = e + zero =.= e

	prop_plus_is_commutative :: Euro Euro -> Property
	prop_plus_is_commutative a b = a + b =.= b + a

	prop_minus_zero_is_identity :: Euro -> Property
	prop_minus_zero_is_identity e = e - zero =.= e

	prop_plus_minus_is_identity :: Euro Euro -> Property
	prop_plus_minus_is_identity a b = a =.= a - b + b

	prop_double_neg_is_identity :: Euro -> Property
	prop_double_neg_is_identity e = ~(~e) =.= e

	prop_neg_is_not_identity :: Euro -> Property
	prop_neg_is_not_identity e = e <> zero ==> e <> ~e

	prop_minus_is_plus_after_neg :: Euro Euro -> Property
	prop_minus_is_plus_after_neg a b = a - b =.= a + ~b

	prop_neg_distributes_over_plus :: Euro Euro -> Property
	prop_neg_distributes_over_plus a b = ~(a + b) =.= ~a + ~b

/**
 * Passed
 *
 * NB: this only checks Rem (as requested). The same property holds for Add.
 * For Pay, the output of the model should be negated.
 */
Start = test fairness
where
	fairness :: [Product] Product -> Property
	fairness ps p = euro newps =.= euro ps + euro out
	where (newps, out) = model ps (Rem p)