{-@ LIQUID "--short-names"    @-}
{-@ LIQUID "--no-warnings"    @-}
{-@ LIQUID "--diffcheck"    @-}
{-@ LIQUID "--no-termination" @-}

module Refinements where

import Prelude hiding (map, foldr, foldr1)


wtAverage :: List (Int, Int) -> Int


-----------------------------------------------------------------------
-- | 1. Simple Refinement Types
-----------------------------------------------------------------------

{-@ type Nat = {v:Int | v >= 0} @-}
{-@ type Pos = {v:Int | v >  0} @-}


-----------------------------------------------------------------------
-- | 2. Function Contracts: Preconditions & Dead Code 
-----------------------------------------------------------------------

{-@ dead :: {v:_ | false} -> a @-}
dead msg = error msg

-----------------------------------------------------------------------
-- | 3. Function Contracts: Safe Division 
-----------------------------------------------------------------------



{-@ divide :: _ -> {v:_ | v > 0 } -> Int @-}
divide     :: Int -> Int -> Int
divide x 0 = dead 12  -- "divide-by-zero"
divide x n = x `div` n



-----------------------------------------------------------------------
-- | 4. Dividing Safely
-----------------------------------------------------------------------



-----------------------------------------------------------------------
-- | 4. Data Types
-----------------------------------------------------------------------

data List a = N | C a (List a)

infixr 9 `C`

 
-----------------------------------------------------------------------
-- | 4. Measuring the Size of Data
-----------------------------------------------------------------------

{-@ measure size @-}
size          :: List a -> Int
size (C x xs) = 1 + size xs 
size N        = 0

-- data List a where
--   N :: forall a. {v: List a | size v = 0}
--   C :: forall a. x:a -> xs:List a -> {v: List a | size v = 1 + size xs}
                
-----------------------------------------------------------------------
-- | 5. A few Higher-Order Functions
-----------------------------------------------------------------------

{-@ map              :: (a -> b) -> xs:List a -> {v: List b | size v = size xs} @-}
map f (N)            = N
map f (C x xs)       = C (f x) (map f xs) 

{-@ foldr1           :: (a -> a -> a) -> {v: List a | 0 < size v } -> a @-}
foldr1 f (C x xs)    = foldr f x xs
foldr1 f N           = dead "foldr1"

foldr f acc N        = acc
foldr f acc (C x xs) = f x (foldr f acc xs)
 

-----------------------------------------------------------------------
-- | 5. Weighted-Averages 
-----------------------------------------------------------------------

{-@ wtAverage :: {v : List (Pos, Pos) | size v > 0} -> Int @-}
wtAverage wxs = total `divide` weights
  where
    total     = sum $ map (\(w, x) -> w * x) wxs
    weights   = sum $ map (\(w, _) -> w    ) wxs
    sum       = foldr1 (+)


-- | Exercise: How would you modify the types to get output `Pos` above? 

-----------------------------------------------------------------------
-- | 5. Ordered Lists: Take 1
-----------------------------------------------------------------------

{- data List a = N | C {x :: a, xs :: List {v:a | x <= v}} @-}

okList :: List Int
okList = 1 `C` 2 `C` 4 `C` N

-- Note that adding ordering BREAKS `map`...



{-@ insert         :: _ -> xs:_ -> {v:_ | size v = 1 + size xs} @-}
insert x N         = x `C` N
insert x (C y ys)
  | x <= y         = x `C` y `C` ys
  | otherwise      = y `C` insert x ys 




{-@ insertSort     :: (Ord a) => xs:[a] -> {v:List a | size v = len xs} @-}
insertSort []      = N
insertSort (x:xs)  = insert x (insertSort xs)