{-@ LIQUID "--no-termination" @-}

module ListDemo where

-----------------------------------------------------------------------
-- 1. Lets define a List data-type
-----------------------------------------------------------------------

data List a = E | (:::) { h :: a, t :: List a }

-- We'll want to use the "cons" in an infix fashion

infixr  9 ::: 

-- Ok, now here are some lists

aList :: List Int
aList = 0 ::: 2 ::: 7 ::: E

-- Lets define some simple refinements.

-- | The set of things  that are greater then `N`

{-@ type Geq a N = {v:a | N <= v} @-}

-- | now we can define the *natural* and *positive* numbers as:

{-@ type Nat   = Geq Int 0    @-}
{-@ type Grand = Geq Int 1000 @-}

-- > Lets go back and see if we can refine our lists:

{- up  :: List Grand @-}

-- Whoops, that didn't work of course, how about

{- up  :: List Nat  @-}

-----------------------------------------------------------------------
-- 2. Lets write a function that generates a sequence: n, n+1, n+2, ...
-----------------------------------------------------------------------

{-@ countUp :: n:Nat -> List Nat @-}
countUp n  = n ::: countUp (n + 1)

-- > How shall we type it? Well, one option:

{- countUp :: n:Nat -> List Nat @-}

-- So if you start with a `Nat` you get a list of `Nat`

-- > How about 

{- countUp :: n:Nat -> List Grand @-}

-- Of course not! Lets see the error. Ah, so you can do:

{- countUp :: n:Grand -> List Grand @-}


-----------------------------------------------------------------------
-- 3. ORDERED sequences ...
-----------------------------------------------------------------------

-- Now, really we want to say that `countUp` returns ORDERED sequences,
-- i.e. it returns an INCREASING list of numbers (starting at `n`).

-- Lets specify this by REFINING `List` to only allow INCREASING sequences ...

-- > Lets look at the data type.
-- > Key: INCREASING means `t` must ONLY contain values GREATER THAN head `h`.
                                      
-- that is,

-- t :: List (Geq a h)

-- lets specify that in a REFINED definition of `List`

{-@ data List a = E | (:::) { h :: a, t :: List (Geq a h) } @-}

-- Now lets look at some lists

ups = 0 ::: 1 ::: 3 ::: E 

-- But how about

downs = 7 ::: 2 ::: E

-- > Now lets go back and revisit `countUp` ... whoops there is an ERROR!
-- > This is because we only know the TAIL is a list of Nat, we ALSO need that
-- > the tail is greater than `n` and so ...

{- countUp :: n:Nat -> List (Geq n) @-}


insert x E          = x ::: E
insert x (y ::: ys)
  | x <= y          = x ::: y ::: ys
  | otherwise       = y ::: insert x ys