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

#ifdef ParallelEvaluation
-- verification in deriving classes diverges
instance Functor     List where
  fmap f N = N
  fmap f (C x xs) = f x `C` fmap f xs 

instance Foldable    List where

  GHC bug ? default traverse method diverges
instance Traversable List where
   traverse f N = pure N
   traverse f (C x xs) = C <$> f x <*> traverse f xs
#else 
#endif


{-@ data List [llen] a 
  = N | C {lhead :: a , ltail :: List a} @-}

instance Show a => Show (List a) where
  show xs = "[" ++ go xs ++ "]"
    where
      go N = ""
      go (C x N)  = show x 
      go (C x xs) = show x ++ ", " ++ go xs  

{-@ measure llen @-}
{-@ llen :: List a -> {v:Integer | 0 <= v } @-} 
llen :: List a -> Integer 
llen N        = 0 
llen (C _ xs) = 1 + llen xs 

{-@ reflect map @-}
@ map : : ( a - > b ) - > is : List a - > { os : List b | llen is = = llen os } @
map :: (a -> b) -> List a -> List b
map _ N        = N
map f (C x xs) = C (f x) (map f xs)

{-@ axiomatize append @-}
append :: List a -> List a -> List a 
append N        ys = ys 
append (C x xs) ys = x `C` (append xs ys)

{-@ type Pos  = {v:Integer | 0 < v } @-}
@ type INat = { v : Integer | 0 < = v } @

{-@ reflect chunk @-}
@ chunk : : i : Pos - > xs : List a - > { v : List ( List a ) | if ( llen xs < = i ) then ( llen v = = 1 ) else ( if ( i = = 1 ) then ( llen v = = llen xs ) else ( llen v < llen xs ) ) } / [ llen xs ] @
chunk :: Integer -> List a -> List (List a)
chunk i xs 
  | llen xs <= i 
  = C xs N 
  | otherwise
  = C (take i xs) (chunk i (drop i xs))

{-@ axiomatize drop @-}
{-@ drop :: i:INat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-} 
drop :: Integer -> List a -> List a 
drop i N = N 
drop i (C x xs)
  | i == 0 
  = C x xs  
  | otherwise 
  = drop (i-1) xs 

{-@ axiomatize take @-}
{-@ take :: i:INat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-} 
take :: Integer -> List a -> List a 
take i N = N 
take i (C x xs)
  | i == 0 
  = N  
  | otherwise 
  = C x (take (i-1) xs)


  
 verification in deriving classes diverges
@ data List [llen] a 
  = N | C {lhead :: a , ltail :: List a} @
@ measure llen @
@ llen :: List a -> {v:Integer | 0 <= v } @
@ reflect map @
@ axiomatize append @
@ type Pos  = {v:Integer | 0 < v } @
@ reflect chunk @
@ axiomatize drop @
@ drop :: i:INat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @
@ axiomatize take @
@ take :: i:INat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @
data List a = N | C a (List a) 
  deriving (Eq)

#ifdef ParallelEvaluation
instance Functor     List where
  fmap f N = N
  fmap f (C x xs) = f x `C` fmap f xs 

instance Foldable    List where

  GHC bug ? default traverse method diverges
instance Traversable List where
   traverse f N = pure N
   traverse f (C x xs) = C <$> f x <*> traverse f xs
#else 
#endif



instance Show a => Show (List a) where
  show xs = "[" ++ go xs ++ "]"
    where
      go N = ""
      go (C x N)  = show x 
      go (C x xs) = show x ++ ", " ++ go xs  

llen :: List a -> Integer 
llen N        = 0 
llen (C _ xs) = 1 + llen xs 

@ map : : ( a - > b ) - > is : List a - > { os : List b | llen is = = llen os } @
map :: (a -> b) -> List a -> List b
map _ N        = N
map f (C x xs) = C (f x) (map f xs)

append :: List a -> List a -> List a 
append N        ys = ys 
append (C x xs) ys = x `C` (append xs ys)

@ type INat = { v : Integer | 0 < = v } @

@ chunk : : i : Pos - > xs : List a - > { v : List ( List a ) | if ( llen xs < = i ) then ( llen v = = 1 ) else ( if ( i = = 1 ) then ( llen v = = llen xs ) else ( llen v < llen xs ) ) } / [ llen xs ] @
chunk :: Integer -> List a -> List (List a)
chunk i xs 
  | llen xs <= i 
  = C xs N 
  | otherwise
  = C (take i xs) (chunk i (drop i xs))

drop :: Integer -> List a -> List a 
drop i N = N 
drop i (C x xs)
  | i == 0 
  = C x xs  
  | otherwise 
  = drop (i-1) xs 

take :: Integer -> List a -> List a 
take i N = N 
take i (C x xs)
  | i == 0 
  = N  
  | otherwise 
  = C x (take (i-1) xs)


  