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