{-@ LIQUID "--prune-unsorted" @-}
{-@ LIQUID "--total"          @-}

{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE QuasiQuotes          #-}

module LiquidR
  ( array
  , combine
  , indexNullary
   -- and,
   -- add,
   -- indexUnary,
   -- indexNAry
  ) where

import Prelude hiding (product, length)
-- import LiquidHaskell

--------------------------------------------------------------------------------
-- Basic List Refinements ------------------------------------------------------
--------------------------------------------------------------------------------

{-@ class measure size :: forall a. a -> Int @-}

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

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

{-@ type ListN a N = {v:[a] | size v = N} @-}
{-@ type ListNE a = {v:[a] | size v > 0}  @-}
{-@ type Pos      = {v:Int | 0 < v}       @-}

-- Generic R Container Types ---------------------------------------------------

{-@ class R c where
      index  :: forall a. c a -> Int -> a
      length :: forall a. me:c a -> {v:Nat | v = size me}
  @-}
class R c where
  index  :: c a -> Int -> a
  length :: c a -> Int

-- A Generic Non-Empty Container -----------------------------------------------

{-@ type RNE c a = {v:c a | 0 < size v} @-}

-- Vector Instance -------------------------------------------------------------

newtype Vector a = V [a]

{-@ instance measure size :: Vector a -> Int
    size (V xs) = size xs
  @-}

instance R Vector where
  index  (V xs) i = xs `at` i
  length (V xs)   = listLength xs

at :: [a] -> Int -> a
at (x:_) 0  = x
at (_:xs) n = at xs (n-1)
at _      _ = undefined

-- Arrays ----------------------------------------------------------------------

data Array a = Array {
    shape :: [Int]
  , elems :: [a]
  }

{-@ measure product @-}
product :: [Int] -> Int
product []     = 1
product (x:xs) = x * product xs

{-@ data Array a = Array {
      shape :: ListNE Pos,
      elems :: ListN a (product shape)
    }                                     @-}

instance R Array where
  index  = undefined
  length = undefined

-- Modes -----------------------------------------------------------------------

class Mode a

type Logical = Maybe Bool
type Numeric = Maybe Int

-- | `Dim` is a refinement of `Numeric` where the values are defined

type Dim = Numeric
{-@ type Dim = {v:Numeric | isJust v} @-}

instance Mode Logical
instance Mode Numeric

class (Mode a) => IntoNumeric a where
  intoNumeric :: a -> Numeric

instance IntoNumeric Numeric where
  intoNumeric = id

instance IntoNumeric Logical where
  intoNumeric Nothing = Nothing
  intoNumeric (Just True)  = Just 1 -- (1.0 :: Double)
  intoNumeric (Just False) = Just 0 -- (0.0 :: Double)

-- Constructor for Arrays ------------------------------------------------------

array :: (R sh, R el, Mode v) => sh Dim -> el v -> Array v

{-@ array :: (R sh, R el, Mode v) => RNE sh Dim -> RNE el v -> Array v @-}
array _shape _elems = undefined

-- IndexNullary ----------------------------------------------------------------
{-@ type VectorN a N = {v:Vector a | size v = N} @-}

{-@ indexNullary :: (R c) => a:(c m) -> VectorN m (size a) @-}
indexNullary :: (R c) => c a -> (Vector a)
indexNullary _ = undefined

--------------------------------------------------------------------------------
-- Container Constructors ------------------------------------------------------
--------------------------------------------------------------------------------

{-@ append :: xs:_ -> ys:_ -> ListN _ {size xs + size ys} @-}
append :: [a] -> [a] -> [a]
append []     ys = ys
append (x:xs) ys = x : append xs ys

-- Constructor for vectors
{-@ measure lsize :: [[a]] -> Int
    lsize []     = 0
    lsize (x:xs) = size x + lsize xs
  @-}

{-@ combine :: ys:[[a]] -> ListN a (lsize ys) @-}
combine :: [[a]] ->  [a]
combine []       = []
combine (xs:xss) = append xs (combine xss)