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