{-@ LIQUID "--no-totality"    @-}

{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE CPP,  NoImplicitPrelude, MagicHash #-}
{-# OPTIONS_HADDOCK hide #-}

module Take (
    take0
  , take
  ) where

import Data.Maybe
import GHC.Base 
import Language.Haskell.Liquid.Prelude (liquidAssert, liquidError, unsafeError) 



{-@ assert take0  :: n: {v: Int | 0 <= v} -> [a] -> {v:[a] | (len(v) = n)} @-}
take0 :: Int -> [a] -> [a]
take0 (I# n#) xs = take_unsafe_UInt0 n# xs

take_unsafe_UInt0 :: Int# -> [a] -> [a]
take_unsafe_UInt0 0#  _     = []
take_unsafe_UInt0 n  (x:xs) = x : take_unsafe_UInt0 (n -# 1#) xs
take_unsafe_UInt0 _   _     = unsafeError "unsafe take"

{-@ assert take  :: n: {v: Int | v >= 0 } -> xs:[a] -> {v:[a] | len v = if len xs < n then (len xs) else n } @-}
take (I# n#) xs = takeUInt n# xs
-- take (I# n#) xs = take_unsafe_UInt n# xs

takeUInt :: Int# -> [a] -> [a]
takeUInt n xs
  | isTrue# (n >=# 0#) =  take_unsafe_UInt n xs
  | otherwise          =  liquidAssert False []

take_unsafe_UInt :: Int# -> [a] -> [a]
take_unsafe_UInt 0#  _     = []
take_unsafe_UInt n ls      =
  case ls of
    []     -> []
    (x:xs) -> x : take_unsafe_UInt (n -# 1#) xs