{- In stack.yaml:

resolver: nightly-2024-01-26
packages:
  - .
extra-deps:
  - rest-rewrite-0.4.3
  - smtlib-backends-0.3
  - smtlib-backends-process-0.3
  - store-0.7.18
  - store-core-0.4.4.7
  - liquidhaskell-0.9.8.1
  - liquidhaskell-boot-0.9.8.1
  - liquid-fixpoint-0.9.6.3
  - liquid-prelude-0.9.2.8.1@rev:1
  - liquid-vector-0.13.1.0.1

-}

{- In package.yaml:

name: lh
dependencies:
- base >= 4.7 && < 5

ghc-options:
- -Wno-x-partial

executables:
  lh-exe:
    main: Main.hs
    source-dirs: app
    dependencies:
    - liquidhaskell
-}

-- Then place this file in app/Main.hs, and run `stack build` or `stack ghci`

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

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

{-@ type NonEmpty a = {v:[a] | 0 < size v} @-}

{-@ head' :: NonEmpty a -> a @-}
head' :: [a] -> a
head' (x:_) = x

{-@ type OrdList a = [a]<{\x v -> x <= v}> @-}

{-@ insertionSort :: Ord a => [a] -> OrdList a @-}
insertionSort :: Ord a => [a] -> [a]
insertionSort = foldr insert []

-- {-@ insert :: Ord a => a -> OrdList a -> OrdList a @-}
insert :: Ord a => a -> [a] -> [a]
insert x [] = [x]
insert x (y:ys)
    | x <= y    = x : y : ys
    | otherwise = y : insert x ys

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

{-@ fac :: Nat -> Nat @-}
fac :: Int -> Int
fac 0 = 1
fac n = n * fac (n - 1)

main :: IO ()
main = do
    print $ head' ([1,2,3] :: [Int])

{-
"Measures are functions which: take one parameter, which:
    - must be an algebraic data type;
    - are defined by a single equation for each constructor;
    - and in their body call only primitive (e.g., arithmetic) functions and measures.
For this restricted class of functions, refinement types can still be checked fully automatically."
-}

----------------------------------------------
-- This stuff needs proof-combinators package

-- import LiquidHaskell.ProofCombinators
-- import Language.Haskell.Liquid.ProofCombinators

-- data MyList a = Emp
--               | a ::: MyList a
--               deriving (Eq)

-- (+++) :: MyList a -> MyList a -> MyList a
-- Emp +++ ys = ys
-- (x ::: xs) +++ ys = x ::: (xs +++ ys)

-- associativityTheorem :: Eq a => MyList a -> MyList a -> MyList a -> Bool
-- associativityTheorem xs ys zs = ((xs +++ ys) +++ zs) == (xs +++ (ys +++ zs))

-- {-@ associativityProof :: xs:_ -> ys:_ -> zs:_ -> { associativityTheorem xs ys zs } @-}
-- associativityProof Emp ys zs =
--     ((Emp +++ ys) +++ zs) ==. (Emp +++ (ys +++ zs)) *** QED
-- associativityProof (x ::: xs) ys zs 
--     =   ((x ::: xs) +++ ys) +++ zs
--     ==. (x ::: (xs +++ ys)) +++ zs
--     ==. x ::: ((xs +++ ys) +++ zs)
--     ==. (x ::: (xs +++ (ys +++ zs))) ? associativityProof xs ys zs
--     ==. (x ::: xs) +++ (ys +++ zs)
--         *** QED