module ReWrite where

{-@ LIQUID "--rw-termination-check" @-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
{-@ infix ++ @-}

import Prelude hiding ((++))


{-@ rewriteWith assoc2 [assoc] @-} 
{-@ assoc2 :: xs:[a] -> ys:[a] -> zs:[a] -> ws:[a]
          -> { xs ++ (ys ++ (zs ++ ws)) == ((xs ++ ys) ++ zs) ++ ws } @-}
assoc2 :: [a] -> [a] -> [a] -> [a] -> ()
assoc2 xs ys zs ws 
  = () {-
    assoc xs ys (zs ++ ws)
    `const` assoc (xs ++ ys) zs ws 
-}


{-@ rewrite assoc @-}
{-@ assoc :: xs:[a] -> ys:[a] -> zs:[a] 
          -> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs } @-}
assoc :: [a] -> [a] -> [a] -> ()
assoc [] _ _       = ()
assoc (_:xs) ys zs = assoc xs ys zs 

{-@ reflect lhs @-}
lhs xs ys zs ws = ((xs ++ ys) ++ zs) ++ ws

{-@ reflect rhs @-}
rhs xs ys zs ws = xs ++ (ys ++ (zs ++ ws))

{-@ rewriteWith assoc3 [assoc] @-} 
{-@ assoc3 :: xs:[a] -> ys:[a] -> zs:[a] -> ws:[a]
          -> { lhs xs ys zs ws = rhs xs ys zs ws } @-}
assoc3 :: [a] -> [a] -> [a] -> [a] -> ()
assoc3 xs ys zs ws = () 


{-@ reflect ++ @-}
(++)::[a] -> [a] -> [a]
[]     ++ ys = ys 
(x:xs) ++ ys = x:(xs ++ys)