diff options
Diffstat (limited to 'assignment-12/gastje.icl')
-rw-r--r-- | assignment-12/gastje.icl | 49 |
1 files changed, 42 insertions, 7 deletions
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) |