diff options
| -rw-r--r-- | assignment-12/cashModel.icl | 52 | ||||
| -rw-r--r-- | assignment-12/gastje.dcl | 34 | ||||
| -rw-r--r-- | assignment-12/gastje.icl | 49 |
3 files changed, 128 insertions, 7 deletions
diff --git a/assignment-12/cashModel.icl b/assignment-12/cashModel.icl index ed0174a..5c11b31 100644 --- a/assignment-12/cashModel.icl +++ b/assignment-12/cashModel.icl @@ -8,6 +8,9 @@ implementation module cashModel */ import StdEnv, GenEq +import gastje +from Data.Func import mapSt +import Data.Tuple class euro a :: a -> Euro instance euro Product @@ -46,3 +49,52 @@ model list (Rem p) | isMember p list = (removeMember p list,[~ (euro p)]) | otherwise = (list,[]) model list Pay = ([],[euro list]) + +derive gen Euro +derive string Euro +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 -> Equals Euro + prop_plus_zero_is_identity e = e + zero =.= e + + prop_plus_is_commutative :: Euro Euro -> Equals Euro + prop_plus_is_commutative a b = a + b =.= b + a + + prop_minus_zero_is_identity :: Euro -> Equals Euro + prop_minus_zero_is_identity e = e - zero =.= e + + prop_plus_minus_is_identity :: Euro Euro -> Equals Euro + prop_plus_minus_is_identity a b = a =.= a - b + b + + prop_double_neg_is_identity :: Euro -> Equals Euro + prop_double_neg_is_identity e = ~(~e) =.= e + + prop_neg_is_not_identity :: Euro -> Implies + prop_neg_is_not_identity e = e <> zero ==> e <> ~e + + prop_minus_is_plus_after_neg :: Euro Euro -> Equals Euro + prop_minus_is_plus_after_neg a b = a - b =.= a + ~b + + prop_neg_distributes_over_plus :: Euro Euro -> Equals Euro + prop_neg_distributes_over_plus a b = ~(a + b) =.= ~a + ~b diff --git a/assignment-12/gastje.dcl b/assignment-12/gastje.dcl new file mode 100644 index 0000000..a08d35b --- /dev/null +++ b/assignment-12/gastje.dcl @@ -0,0 +1,34 @@ +definition module gastje + +import StdGeneric +from StdOverloaded import class == +from GenEq import generic gEq + +test :: p -> [String] | prop p + +class prop a where holds :: a Prop -> [Prop] + +instance prop Bool + +instance prop (a->b) | prop b & testArg a + +class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a + +:: Prop + +generic gen a :: [a] +derive gen Int, Bool, Char, UNIT, PAIR, EITHER, CONS, OBJECT, RECORD, FIELD +generic string a :: a -> String +derive string Int, Bool, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT, RECORD of grd, FIELD of gfd + +:: For t = E.p: (For) infix 0 (t -> p) [t] & prop p + +instance prop (For t) | string{|*|} t + +:: Implies = E.p: (==>) infix 0 Bool p & prop p + +instance prop Implies + +:: Equals a = (=.=) infix 4 a a + +instance prop (Equals a) | ==, string{|*|} a diff --git a/assignment-12/gastje.icl b/assignment-12/gastje.icl index 6ad6d68..09fe76e 100644 --- a/assignment-12/gastje.icl +++ b/assignment-12/gastje.icl @@ -1,4 +1,4 @@ -module gastje +implementation module gastje /* Pieter Koopman, Radboud University, 2016, 2017 @@ -15,9 +15,9 @@ test p = check 1000 (holds p prop0) check :: Int [Prop] -> [String] check n [] = ["Proof\n"] check 0 l = ["Passed\n"] -check n [p:x] | p.bool - = check (n-1) x - = ["Fail for: ":reverse ["\n":p.info]] +check n [p:x] +| p.bool = check (n-1) x +| otherwise = ["Fail for: ":reverse ["\n":p.info]] class prop a where holds :: a Prop -> [Prop] @@ -35,7 +35,7 @@ class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a } prop0 = {bool = True, info = []} -generic gen a :: [ a ] +generic gen a :: [a] gen{|Int|} = [0,1,-1,maxint,minint,maxint-1,minint+1:[j\\i<-[2..], j<-[i,~i]]] gen{|Bool|} = [True,False] gen{|Char|} = [' '..'~'] ++ ['\t\n\b'] @@ -63,7 +63,9 @@ string{|CONS of gcd|} f (CONS x) | otherwise = gcd.gcd_name string{|OBJECT|} f (OBJECT x) = f x string{|RECORD of grd|} f (RECORD x) = "{" + grd.grd_name + "|" + f x + "}" -string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + " = " + f x + " " +string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + "=" + f x + if last "" "," +where + last = gfd.gfd_index == length gfd.gfd_cons.grd_fields - 1 maxint :: Int maxint =: IF_INT_64_OR_32 (2^63-1) (2^31-1) //2147483647 @@ -85,4 +87,37 @@ where rev [] accu = accu rev [x:r] accu = rev r [x:accu] -Start = () +:: For t = E.p: (For) infix 0 (t -> p) [t] & prop p + +instance prop (For t) | string{|*|} t +where + holds (f For xs) p = diagonal [holds (f x) {p & info=[string{|*|} x:p.info]} \\ x <- xs] + +:: Implies = E.p: (==>) infix 0 Bool p & prop p + +instance prop Implies +where + holds (True ==> t) p = holds t p + holds (False ==> _) p = [] + +:: Equals a = (=.=) infix 4 a a + +instance prop (Equals a) | ==, string{|*|} a +where + holds (x =.= y) p = [{bool=x==y, info=[string{|*|} x," <> ",string{|*|} y,"; ":p.info]}] + +Start = + [ ["pUpper: ":test (pUpper For ['a'..'z'])] + , ["pUpper lower: ":test (\c -> isLower c ==> pUpper c)] + , ["pFac: ":test (\i -> abs i < 10 ==> prod [1..i] =.= fac i)] + ] +where + pUpper :: Char -> Bool + pUpper c = c <> toUpper c + + // This fails for 0; should be <=. If we fix that, the test does not + // terminate, as there are no 1000 integers with abs i < 10. + fac :: Int -> Int + fac n + | n < 0 = 1 + | otherwise = n * fac (n-1) |