ReflectLib4.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}

module ReflectLib4 where

-- | Lists ---------------------------------------------------------------------

{-@ data List [llen] @-} 
data List a = Nil | Cons {lHd :: a, lTl :: List a} 

{-@ measure llen @-}
{-@ llen :: List a -> Nat @-}
llen :: List a -> Int
llen Nil        = 0
llen (Cons h t) = 1 + llen t

-- TODO: make this work WITHOUT the invariant
{- invariant {v:List a | 0 <= llen v} @-}

{-@ reflect app @-}
app :: List a -> List a -> List a
app Nil         ys = ys
app (Cons x xs) ys = Cons x (app xs ys)

{-@ reflect gapp @-}
gapp :: List a -> List a
gapp Nil         = Nil
gapp (Cons x xs) = Nil

{-@ test4 :: { gapp Nil = Nil } @-}
test4 = ()