old/afp/a12/gastyStart.icl

   1 implementation module gastyStart
   2
   3 /*
   4         Pieter Koopman, Radboud University, 2016, 2017
   5         pieter@cs.ru.nl
   6         Advanced programming
   7         A simplified MBT tool based on logical properties
   8
   9         Use the iTask environment!
  10         Execute with "Basic values only" option
  11 */
  12
  13 import StdEnv, StdGeneric, Data.GenEq
  14
  15 test :: p -> [String] | prop p
  16 test p = check 1000 (holds p prop0)
  17
  18 check :: Int [Prop] -> [String]
  19 check n [] = ["Proof\n"]
  20 check 0 l  = ["Passed\n"]
  21 check n [p:x] | p.bool
  22         = check (n-1) x
  23         = ["Fail for: ":reverse ["\n":p.info]]
  24
  25 class prop a where holds :: a Prop -> [Prop]
  26 instance prop Bool where holds b p = [{p & bool = b}]
  27 instance prop (a->b) | prop b & testArg a
  28 where
  29         holds f p = diagonal [holds (f a) {p & info = [" ",string{|*|} a:p.info]} \\ a <- gen{|*|}]
  30
  31 class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
  32
  33 :: Prop =
  34         { bool :: Bool
  35         , info :: [String]
  36         }
  37 prop0 = {bool = True, info = []}
  38
  39 generic gen a :: [ a ]
  40 gen{|Int|}  = [0,1,-1,maxint,minint,maxint-1,minint+1:[j\\i<-[2..], j<-[i,~i]]]
  41 gen{|Real|} = [0.0, 1.0, -1.0: reals]
  42 where
  43         reals = [r \\ (x,y) <- diag2 ints ints | x <> y, r <- let c = toReal x / toReal y in [c, ~c]]
  44         ints = [1: sieve [2..]]
  45         sieve [p:xs] = [p: sieve [x \\ x <- xs | x rem p <> 0]]
  46 gen{|Bool|} = [True,False]
  47 gen{|Char|} = [' '..'~'] ++ ['\t\n\b']
  48 gen{|UNIT|} = [UNIT]
  49 gen{|PAIR|}   f g       = map (\(a,b)=PAIR a b) (diag2 f g)
  50 gen{|EITHER|} f g = merge (map RIGHT g) (map LEFT f)
  51 where
  52   merge [a:x] ys = [a: merge ys x]
  53   merge []    ys = ys
  54 gen{|CONS|}   f  = map CONS f
  55 gen{|OBJECT|} f  = map (\x->OBJECT x) f
  56 gen{|RECORD|} f  = map RECORD f
  57 gen{|FIELD|}  f  = map (\x->FIELD x) f
  58
  59 generic string a :: a -> String
  60 string{|Int|}  i = toString i
  61 string{|Real|} x = toString x
  62 string{|Bool|} b = toString b
  63 string{|Char|} c = toString ['\'',c,'\'']
  64 string{|UNIT|} _ = ""
  65 string{|PAIR|} f g (PAIR x y) = f x + " " + g y
  66 string{|EITHER|} f g (LEFT x) = f x
  67 string{|EITHER|} f g (RIGHT y) = g y
  68 string{|CONS of gcd|} f (CONS x) | gcd.gcd_arity > 0
  69         = "(" + gcd.gcd_name + " " + f x + ")"
  70         = gcd.gcd_name
  71 string{|OBJECT|} f (OBJECT x) = f x
  72 string{|RECORD of grd|} f (RECORD x) = "{" + grd.grd_name + "|" + f x + "}"
  73 string{|FIELD of gfd|} f (FIELD x) = gfd.gfd_name + " = " + f x + " "
  74
  75 maxint :: Int
  76 maxint =: IF_INT_64_OR_32 (2^63-1) (2^31-1) //2147483647
  77
  78 minint :: Int
  79 minint =: IF_INT_64_OR_32 (2^63) (2^31) //-2147483648
  80
  81 instance + String where + s t = s +++ t
  82
  83 diagonal :: [[a]] -> [a]
  84 diagonal list = f 1 2 list []
  85 where
  86         f n m [] [] = []
  87         f 0 m xs ys = f m (m+1) (rev ys xs) []
  88         f n m [] ys = f m (m+1) (rev ys []) []
  89         f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]
  90         f n m [[]:xs] ys = f (n-1) m xs ys
  91
  92         rev []    accu = accu
  93         rev [x:r] accu = rev r [x:accu]
  94
  95 pUpper :: Char -> Bool
  96 pUpper c = c <> toUpper c
  97
  98 :: For = E.a b: (For) infix 0 (a -> b) [a] & prop b & string{|*|} a
  99 instance prop For
 100 where
 101         holds (f For l) p = diagonal [holds (f a) {p & info = [" ",string{|*|} a:p.info]}\\a<-l]
 102 //Start = ["pUpper: ":test (pUpper For ['a'..'z'])]
 103
 104 :: Select = E.p: (==>) infixl 0 Bool p & prop p
 105 instance prop Select
 106 where
 107         holds (c ==> b) p = if c (holds b p) [{p & bool = True, info = ["rejected ":p.info]}]
 108
 109 //Start = ["pUpper lower:": test (\c. isLower c ==> pUpper c)]
 110
 111 :: Equ = E.a: (=.=) infix 4 a a & testArg a
 112 instance prop Equ
 113 where
 114         holds (x =.= y) p = [{p & bool = x === y, info = [string{|*|} y," found: ",string{|*|} x," expected: ":p.info]}]
 115 //Start = test (\i->i =.= hd [i,0])