module mylist where

-- C-x C-v RET to reload file in emacs
open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String; _++_)
open import Data.Char using (Char)
open import Foreign.Haskell using (fromColist; Colist; Unit)
open import Function
open import Data.Unit
open import Data.Nat.Show using (show)

open import Category.Monad.Identity
open import Data.Bool
open import Data.Nat
open import Data.Nat.Properties

-- unicode 2237 = double colon
-- data List (a : Set) : ℕ → Set where
--    [] : List a zero
--    _∷_ : {n : ℕ} → a → List a n → List a (suc n)

-- unicode 2237 = double colon
-- append : {a : Set} → {m , n : ℕ} → List a m → List a n → List a (m + n)
-- append [] ys = ys
-- append (x ∷ xs) ys = x ∷ append xs ys

data NatList : Set where
   []  :               NatList
   _,_ : ℕ → NatList → NatList

-- unicode 2237 = double colon
append : {N : ℕ} → ℕ → NatList → NatList
append N [] = N , []
append N y = N , y

length : NatList → ℕ
length []       = 0
length (x , xs) = 1 + length xs

fromString : String → Colist Char
fromString = fromColist ∘ toCostring 

main : IO Unit
-- main = putStrLn (fromString ("Hello, "++" world!"))
main = putStrLn ∘ fromString $ ("length of list: " ++ show (length []))