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