1{-# LANGUAGE UnicodeSyntax #-} 2module Main where 3 4import System.Environment 5 6main :: IO () 7main = do 8 as <-getArgs 9 print $ as 10 print $ test 0 11 print $ test2 0 12 print $ testRewrite 0 13 print $ testRewriteReverse 0 14 print $ testRewrite2 0 15 print $ testRewriteReverse2 0 16 17test :: a ->Bool 18test x = pi 19 where 20 f = replicate 2000 x 21 i = repeat x 22 pf = f |> 300 23 pi = i |> 300 24 25test2 :: a ->(Bool,Bool) 26test2 x = (pf,pi) 27 where 28 f = replicate 2000 x 29 i = repeat x 30 pf = f |> 300 31 pi = i |> 300 32 33testRewrite :: a ->Bool 34testRewrite x = pi 35 where 36 f = replicate 2000 x 37 i = repeat x 38 lf = length f 39 li = length i 40 pf = lf > 300 41 pi = li > 300 42 43testRewriteReverse :: a ->Bool 44testRewriteReverse x = pi 45 where 46 f = replicate 2000 x 47 i = repeat x 48 lf = length f 49 li = length i 50 pf = 300 d lf 51 pi = 300 d li 52 53testRewrite2 :: a ->(Bool,Bool) 54testRewrite2 x = (length i > 300,300 > length i) 55 where 56-- f = replicate 2000 x 57 i = repeat x 58-- lf = length f 59-- li = length i 60-- pf = lf > 300 61-- pi = li > 300 62 63testRewriteReverse2 :: a ->(Bool,Bool) 64testRewriteReverse2 x = (2000 < length i,length i > 20) 65 where 66 f = replicate 2000 x 67 i = repeat x 68 lf = length f 69 li = length i 70 pf = 2000 == lf 71 pi = lf e li 72 73 74lengthOP :: (Num a, Ord a) =>Bool ->(a ->a ->Bool) ->[b] ->a ->Bool 75lengthOP v (�) [] n = 0 � n 76lengthOP v (�) xxs n = co xxs 0 77 where 78 co (_:xs) c | n > c = co xs (c+1) 79 | otherwise = v 80 co [] c = c � n 81 82(c) = (==) 83(d) = (<=) 84(e) = (>=) 85 86(|c) = lengthOP False (c) 87(|<) = lengthOP False (<) 88(|d) = lengthOP False (d) 89(|>) = lengthOP True (>) 90(|e) = lengthOP True (e) 91 92(|=) = lengthOP False (==) 93(|==) = lengthOP False (==) 94(|<=) = lengthOP False (<=) 95(|>=) = lengthOP False (>=) 96 97 98-- cde 99(c|) = flip (|c) 100(<|) = flip (|e) 101(d|) = flip (|>) 102(>|) = flip (|d) 103(e|) = flip (|<) 104 105{-# RULES 106-- length 107"xs |\8803 n"forallxsn. (length xs) == n = xs |c n 108"xs |< n" forall xs n. (length xs) < n = xs |< n 109"xs |\8804 n"forallxsn. (length xs) <= n = xs |d n 110"xs |> n" forall xs n. (length xs) > n = xs |> n 111"xs |\8805 n"forallxsn. (length xs) >= n = xs |e n 112 113"n \8803| xs"forallxsn. n == (length xs) = xs |c n 114"n <| xs" forall xs n. n < (length xs) = xs |e n 115"n \8804| xs"forallxsn. n <= (length xs) = xs |> n 116"n >| xs" forall xs n. n > (length xs) = xs |d n 117"n \8805| xs"forallxsn. n >= (length xs) = xs |< n 118 #-} 119 120