{-# LANGUAGE ExistentialQuantification, TypeOperators, EmptyDataDecls #-}

module SList where
import PhantomTypes

data Safe
data Unsafe

-- Reimplemention of standard list constructors
-- instead of wrapping
-- Also switching the order of arguments to make 
-- casting easier.
data List b a =            Nil  (a :=: Unsafe) 
              |  forall c. Cons (a :=: Safe)   b  (List b c)


instance Show b => Show (List b a) where
  show (Nil _) = "nil"
  show (Cons _ x xs) = "(cons " ++ show x ++ " " ++ show xs ++ ")"

nil :: List b Unsafe 
nil = undefined

cons :: b -> List b c -> List b Safe
cons = undefined

testnull :: List b a -> (List b Unsafe -> c) -> (List b Safe -> c) -> c
testnull l@(Nil p)     is isnot = is undefined
testnull l@(Cons p _ _) is isnot = isnot undefined 

-- For flexibilty, note we don't want the opposite conversion

-- Can't do this one.
-- forget :: List Safe b -> List Unsafe b
-- instead, can only do this one.
data ListUnsafe b = forall a. L ( List b a)

forget :: List b Safe -> ListUnsafe b
forget = undefined

instance Show a => Show (ListUnsafe a) where
  show (L l) = show l


toList :: List b a -> [b]
toList (Nil _) = []
toList (Cons _ hd tl) = hd : toList tl

fromList :: [b] -> ListUnsafe b
fromList l = foldr (\x (L xs) -> L (cons x xs)) (L nil) l 

-- Four operations that require non-empty lists

sHead :: List a Safe -> a 
sHead (Cons _ hd tl) = hd

sTail :: List a Safe -> ListUnsafe a
sTail (Cons _ hd tl) = L tl

sLast :: List a Safe -> a
-- from prelude
-- last [x] = x
---last (x : xs) = last xs
sLast = undefined

sInit :: List a Safe -> ListUnsafe a 
sInit = undefined

-- Other standard operations that work for any list

sElem :: Eq b => b -> List b a -> Bool
sElem b (Cons _ x xs) = if b == x then True else sElem b xs
sElem b (Nil _) = False

sMap  :: (b1 -> b2) -> List b1 a -> List b2 a
sMap = undefined
-- Doesn't quite work
-- sMap f (Nil p)       = nil
-- sMap f (Cons p x xs) =  (cons (f x) (sMap f xs))

sFilter :: (b -> Bool) -> List b a -> ListUnsafe b
sFilter f (Nil _)       = L nil
sFilter f (Cons _ x xs) =  
  if f x then case  (sFilter f xs) of 
               L l -> L (cons x l)
  else sFilter f xs

sLength :: List b a -> Int
sLength (Nil _) = 0
sLength (Cons _ x xs) = 1 + sLength xs

-- what is type of (binary) concat??
sConcat :: List b a1 -> List b a2 -> ListUnsafe b
sConcat (Nil _) l = L l
sConcat (Cons _ x xs) l = case (sConcat xs l) of 
                                L l -> L (cons x l)