ISortTicked.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}
module ISort where 

import Prelude hiding (return, pure, (<*>), length, (>>=), head)







sortedValISort :: Ord a => [a] -> () 
{-@ sortedValISort :: Ord a => xs:(SList a) 
                  -> { tval (isort xs)  == xs } @-}
sortedValISort []  = () 
sortedValISort [x] = ()
sortedValISort (x:xs) = sortedValISort xs
{- 
    =   tval (isort (x:xs))
    ==. tval (leqBind (length xs) (isort xs) (insert x) )
    ==. tval (insert x (tval (isort xs)))
        ? sortedValISort xs
    ==. tval (insert x xs)
    ==. x:xs
    *** QED 
-}







{-@ type SList a = [a]<{\i j -> i <= j }>@-}


{-@ head :: is:{[a] | 0 < length is } -> a @-}
head :: [a] -> a 
head (x:_) = x

{-@ measure length @-}
length :: [a] -> Int 
{-@ length :: [a] -> Nat @-}
length [] = 0 
length (_:xs) = 1 + length xs 

{-@ reflect isort @-}
{-@ isort :: Ord a => is:[a] -> {t:Tick {os:(SList a) | length os == length is } | tcost t <= length is * length is } @-}
isort :: Ord a => [a] -> Tick [a]
isort []     = return [] 
isort (x:xs) = leqBind (length xs) (isort xs) (insert x) 

{-@ reflect insert @-}
{-@ insert :: Ord a => x:a -> xs:(SList a) 
           -> {t:Tick {os:(SList a) | length os == 1 + length xs}  | tcost t <= length xs }@-}

insert :: Ord a => a -> [a] -> Tick [a]
insert x [] = return [x]
insert x (y:ys)
  | x <= y    = step 1 (return (x:y:ys))
  | otherwise = step 1 (pure (y:) <*> insert x ys)







-- From Proof Combinators 

data QED = QED 

infixl 1 ***


infixl 3 ==., <=.

infixl 3 ?
{-@ (<=.) :: x:a -> y:{a | x <= y} -> {v:a | v == y && x <= v} @-}
(<=.) :: a -> a -> a
_ <=. x = x

{-@ (==.) :: x:a -> y:{a | x == y} -> {v:a | v == y && v == x} @-}
(==.) :: a -> a -> a
_ ==. x = x

(***) :: a -> QED -> () 
_ *** QED = () 


{-@ (?) :: x:a -> b -> {v:a| v == x} @-}
(?):: a -> b -> a 
x ? _ = x 

-- From the Tick LIB 

data Tick a = Tick {tcost :: Int, tval :: a} 
{-@ data Tick a = Tick {tcost :: Nat, tval :: a}  @-}


{-@ reflect step @-}
{-@ step :: n:Nat -> t1:Tick a -> { t2:Tick a | tval t2 == tval t1 &&
    tcost t2 == tcost t1 + n } @-}
step :: Int -> Tick a -> Tick a
step m (Tick n x) = Tick (m + n) x


{-@ reflect pure @-}
{-@ pure :: x:a -> {t:Tick a | tcost t == 0 && tval t == x } @-}
pure :: a -> Tick a 
pure x = Tick 0 x


{-@ reflect <*> @-}
{-@ infix   <*> @-}
{-@ <*> :: t1:(Tick (a -> b)) -> t2:Tick a -> { t3:Tick b | tcost t3 ==
    tcost t1 + tcost t2 } @-}
(<*>) :: Tick (a -> b) -> Tick a -> Tick b
Tick m f <*> Tick n x = Tick (m + n) (f x)
    


{-@ reflect return @-}
{-@ return :: x:a -> { t:Tick a | tcost t == 0 && tval t == x } @-}
return :: a -> Tick a
return x = Tick 0 x

{-@ reflect leqBind @-}
{-@ leqBind :: n:Nat -> t1:Tick a 
              -> f:(a -> {tf:Tick b | tcost tf <= n}) 
            -> { t2:Tick b | tcost t2 <= tcost t1 + n } @-}
leqBind :: Int -> Tick a -> (a -> Tick b) -> Tick b
leqBind _ (Tick m x) f = let Tick n y = f x in Tick (m + n) y