module Example where

-- Chameleon examples

data Exp = Zero | Succ Exp | Plus Exp Exp | Fun (Exp->Exp) | App Exp Exp 

-- We use meta-variables (i.e. Haskell variables) to represent variables
-- in our object language.
-- That is, we're using Higher-Order Abstract Syntax (HOAS)

-- We define our own Show instance

{-
instance Show Exp where
   show Zero = show 0                                  -- show zero as "0"
   show (Succ e) =  show (((read (show e))::Int) + 1)  
                    -- we show e --> somestring
                    -- (read somestring)::Int yields the integer interpretation of the string
                    -- we add one, and show again
   show (Plus e1 e2) = "Plus" ++ show e1 ++ show e2
   show (Fun f) = show f
   show (App e1 e2) = "App " ++ show e1 ++ " " ++ show e2

instance Show (Exp -> Exp) where
      show f = "Functions!"

-}

eval :: Exp -> Exp
eval Zero = Zero
eval (Succ e) = Succ (eval e)
eval (Plus Zero e) = eval e
eval (Plus (Succ e1) e2) = Succ (eval (Plus e1 e2))
eval (Fun f) = Fun f 
-- Chameleon demands (...) for case patterns
eval (App f e) = case (eval f) of 
                  (Fun f') -> eval (f' (eval e))



-- stack example

-- Prelude functions
null :: [a]->Bool
null [] = True
null _  = False

tail :: [a]->[a]
tail (x:xs) = xs

head :: [a]->a
head (x:xs) = x

data Stack a = forall s. Stack s           -- self
                               (a->s->s)   -- push
                               (s->s)      -- pop
                               (s->a)      -- top
                               (s->Bool)   -- empty


push :: a -> Stack a -> Stack a
push x (Stack s push' pop top empty) = Stack (push' x s) push' pop top empty

pop :: Stack a -> Stack a
pop (Stack s push pop' top empty) = Stack (pop' s) push pop' top empty

top :: Stack a -> a
top (Stack s push pop top' empty) = top' s

empty :: Stack a -> Bool
empty (Stack s push pop top empty') = empty' s


-- examples
mkListStack :: [a] -> Stack a
mkListStack xs = Stack xs (:) tail head null

s1 = mkListStack [1::Int]
s2 = push 2 s1


-- stack using type classes with existential types

class StackM s a | s -> a where
    pushM  :: a->s->s
    popM   :: s->s
    topM   :: s->a
    emptyM :: s->Bool


data Stack2 a = forall s. StackM s a => Stack2 s   


push2 :: a -> Stack2 a -> Stack2 a
push2 x (Stack2 s) = Stack2 (pushM x s) 

pop2 :: Stack2 a -> Stack2 a
pop2 (Stack2 s) = Stack2 (popM s) 

top2 :: Stack2 a -> a
top2 (Stack2 s) = topM s

empty2 :: Stack2 a -> Bool
empty2 (Stack2 s) = emptyM s


-- examples
instance StackM [a] a where
   pushM  = (:)
   popM   = tail
   topM   = head
   emptyM = null


mkListStack2 :: [a] -> Stack2 a
mkListStack2 xs = Stack2 xs 

s3 = mkListStack2 [1::Int]
s4 = push2 2 s3



-- A well-typed interpreter for simply-typed programs

data Exp2 a = (a=Int) => Zero2 | (a=Int)=> Succ2 (Exp2 Int) 
           | (a=Int) => Plus2 (Exp2 Int) (Exp2 Int)
           | forall b c. (a=b->c) => Fun2 (Exp2 b->Exp2 c) 
           | forall b. App2 (Exp2 (b->a)) (Exp2 b)
           | Lift2 a

plus = undef

undef = undef

zero :: Int
zero = undef

one :: Int
one = undef

eval2 :: Exp2 a -> a
eval2 Zero2 = zero
eval2 (Succ2 n) = (eval2 n) `plus` one
eval2 (Plus2 e1 e2) = (eval2 e1) `plus` (eval2 e2)
eval2 (Fun2 f) = let g x = eval2 (f (Lift2 x))          
                in g
eval2 (App2 f e) = (eval2 f) (eval2 e)
eval2 (Lift2 x) = x




-- Chameleon unifies GADTs, type classes with functional depdendencies and existential types

data Z
data S x


class Add x y z | x y -> z
instance Add Z m m
instance Add l m n' => Add (S l) m (S n')

{-
rule Add l m n, Add l m n' ==> n=n'
rule Add Zero m n <==> m=n
rule Add (Succ l) m n <==> Add l m n', n=Succ n'
-}

-- type indexed data type
-- we keep track of the length of the list
data List a n =  (n= Z) => Nil 
            | forall m. Add (S Z) m n => 
                        Cons a (List a m) 


append ::  Add l m n => 
           List a l -> List a m -> List a n
append (Cons x xs) ys = Cons x (append xs ys)
append Nil ys = ys