{-# 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 ≤ lf
    pi = 300 ≤ 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 ≥ 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

(≣) = (==)
(≤) = (<=)
(≥) = (>=)

(|≣)  = lengthOP False (≣)
(|<)  = lengthOP False (<)
(|≤)  = lengthOP False (≤)
(|>)  = lengthOP True  (>)
(|≥)  = lengthOP True  (≥)

(|=)  = lengthOP False (==)
(|==) = lengthOP False (==)
(|<=) = lengthOP False (<=)
(|>=) = lengthOP False (>=)


-- ≣≤≥
(≣|) = flip (|≣)
(<|) = flip (|≥)
(≤|) = flip (|>)
(>|) = flip (|≤)
(≥|) = flip (|<)

{-# RULES
-- length
"xs |≣ n" forall xs n.  (length xs) == n = xs |≣ n
"xs |< n" forall xs n.  (length xs) <  n = xs |< n
"xs |≤ n" forall xs n.  (length xs) <= n = xs |≤ n
"xs |> n" forall xs n.  (length xs) >  n = xs |> n
"xs |≥ n" forall xs n.  (length xs) >= n = xs |≥ n

"n ≣| xs" forall xs n.  n == (length xs) = xs |≣ n
"n <| xs" forall xs n.  n <  (length xs) = xs |≥ n
"n ≤| xs" forall xs n.  n <= (length xs) = xs |> n
"n >| xs" forall xs n.  n >  (length xs) = xs |≤ n
"n ≥| xs" forall xs n.  n >= (length xs) = xs |< n
  #-}