liquid-types.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}

module Foo where

import Data.Proxy
import GHC.Types

data L a = Nil | Cons a (L a)

{-@ myList :: {xs : L Bool | mySize xs == 2} @-}
myList :: L Bool
myList = Cons True (Cons False Nil)

{-@ assume mySucc2 :: (Ord a, Enum a, Bounded a) => {x:a| not (isUpperBound x)} -> {y : a | y > x } @-}
mySucc2 :: (Ord a, Enum a, Bounded a) => a -> a
mySucc2 x = succ x

{-@ myFunc :: {x : a | x > x} -> {y : a | y == x} @-}
myFunc :: a -> a
myFunc = id

-- {-@ assume mySucc3 :: (Ord a, Enum a, Bounded a) => x:a -> {y : a | y > x } @-}
-- mySucc3 :: (Ord a, Enum a, Bounded a) => a -> a
-- mySucc3 = mySucc2 maxBound

{-@ type TRUE = {v:Bool | v } @-}
{-@ type FALSE = {v:Bool | not v} @-}


{-@ class measure mySize :: forall a. a -> Int @-}
{-@ instance measure mySize :: L a -> Int
    mySize Nil = 0
    mySize (Cons x xs) = 1 + (mySize xs)
@-}

data MyNat = MySuc MyNat | MyNil
{-@ instance measure mySize :: MyNat -> Int
    mySize MyNil = 0
    mySize (MySuc n) = 1 + (mySize n)
@-}

{-@ class measure isUpperBound :: forall a. a -> Bool @-}

{-@ assume gt :: Ord a => x:a -> y:a -> {v:GHC.Types.Bool | ((v) <=> x > y) && ((mySize x > mySize y) <=> x > y) && (isUpperBound x ==> not (isUpperBound y))} @-}
gt :: Ord a => a -> a -> Bool
gt = (>)

{-@ assume maxBound :: Bounded a => {x:a| isUpperBound x} @-}

drewFunc :: (Ord a, Enum a, Bounded a) => a -> a
drewFunc a = if gt maxBound a
  then mySucc2 a
  else a


{-@ n0 :: {x : MyNat | mySize x == 0} @-}
{-@ n1 :: {x : MyNat | mySize x == 1} @-}
{-@ n2 :: {x : MyNat | mySize x == 2} @-}
{-@ n3 :: {x : MyNat | mySize x == 3} @-}
{-@ n4 :: {x : MyNat | mySize x == 4} @-}
{-@ n5 :: {x : MyNat | mySize x == 5} @-}
{-@ n6 :: {x : MyNat | mySize x == 6} @-}
{-@ n7 :: {x : MyNat | mySize x == 7} @-}
{-@ n8 :: {x : MyNat | mySize x == 8} @-}
n0,n1,n2,n3,n4,n5,n6,n7,n8 :: MyNat
n0 = MyNil
n1 = MySuc n0
n2 = MySuc n1
n3 = MySuc n2
n4 = MySuc n3
n5 = MySuc n4
n6 = MySuc n5
n7 = MySuc n6
n8 = MySuc n7

{-@ assume mySucc :: Enum a => x:a -> {y : a | mySize y = (mySize x) + 1} @-}
mySucc :: Enum a => a -> a
mySucc x = succ x

{-@ assume myPred :: Enum a => x:a -> {y : a | mySize y = (mySize x) - 1} @-}
myPred :: Enum a => a -> a
myPred x = pred x

{-@ data Diet a = DietNil | DietCons { hd :: a, tl :: Diet {v:a | mySize hd > mySize v + 1}} @-}
data Diet a
  = DietNil
  | DietCons a (Diet a)

{-@ measure dietMax :: forall a. Diet a -> Int
    dietMax DietNil = 0
    dietMax (DietCons x _) = mySize x
@-}

{-@ myDiet :: Diet MyNat @-}
myDiet :: Diet MyNat
myDiet = DietCons n7 (DietCons n5 (DietCons n2 DietNil))