module test

import Control.Applicative
import Control.Monad
import Data.Func
import Data.Functor
import Data.Either
import Data.Maybe
import StdEnv

:: In a b = In infixl 0 a b
class lambda v
where
	(@) infixr 1 :: (v ((v a) -> v b)) (v a) -> v b
	\| :: ((v a) -> v b) -> v ((v a) -> v b) | TC a & TC b & TC (v b)

class expr v
where
	lit :: a -> v a | toString a
	(+.) infixl 6 :: (v a) (v a) -> v a | + a
	(-.) infixl 6 :: (v a) (v a) -> v a | - a
	(*.) infixl 6 :: (v a) (v a) -> v a | * a
	(/.) infixl 6 :: (v a) (v a) -> v a | / a
	(==.) infix 4 :: (v a) (v a) -> v Bool | == a
	If :: (v Bool) (v a) (v a) -> v a

class let v
where
	lett :: ((v a) -> In (v a) (v b)) -> v b | TC a

:: St a = St (Env -> Either String (a, Env))
:: Env :== [(Int, Dynamic)]
instance Functor St where fmap f m = m >>= pure o f
instance pure St where pure x = St \s->Right (x, s)
instance <*> St where (<*>) mfa ma = mfa >>= \fa->ma >>= \a->pure (fa a)
instance Monad St where bind ma a2mb = St $ either Left (\(a,s)->evalSt (a2mb a) s) o evalSt ma

get    = St \s->Right (s, s)
put s  = St \_->Right ((), s)
fail e = St \_->Left e
evalSt (St m) = m
eval m = either Left (Right o fst) (evalSt m [])

instance expr St
where
	lit a = pure a
	(+.) l r = (+) <$> l <*> r
	(-.) l r = (-) <$> l <*> r
	(*.) l r = (*) <$> l <*> r
	(/.) l r = (/) <$> l <*> r
	(==.) l r = (==) <$> l <*> r
	If i t e = i >>= \b->if b t e

instance lambda St
where
	(@) l r = l >>= \l->l r
	\| def = pure \x->fresh >>= \l->putVar l x >>| def (getVar l)

instance let St
where
	lett def = fresh >>= \l->
		let (x In y) = def (getVar l)
		in  putVar l x >>| y

fresh = length <$> get
putVar l x = get >>= \s->put [(l, dynamic x):s]
getVar l = get >>= \s->hd [a\\(x, a :: St a^)<-s | x == l]

:: Print a = Print (Int [String] -> [String])
unPrint (Print f) = f
print :: (Print a) -> [String]
print f = unPrint f 0 []
var d i _ c = [d,toString i:c]
instance expr Print
where
	lit a = Print \i c->[toString a:c]
	(+.) l r = Print \i c->["(":unPrint l i ["+":unPrint r i [")":c]]]
	(-.) l r = Print \i c->["(":unPrint l i ["-":unPrint r i [")":c]]]
	(*.) l r = Print \i c->["(":unPrint l i ["*":unPrint r i [")":c]]]
	(/.) l r = Print \i c->["(":unPrint l i ["/":unPrint r i [")":c]]]
	(==.) l r = Print \i c->["(":unPrint l i ["==":unPrint r i [")":c]]]
	If p t e = Print \i c->["if ":unPrint p i [" ":unPrint t i [" ":unPrint e i c]]]
instance lambda Print
where
	(@) l r = Print \i c->["(":unPrint l i [" ":unPrint r i [")":c]]]
	\| def = Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i))) (inc i) [")":c]]]
instance let Print
where
	lett def = Print \i c->let (x In y) = def (Print (var "f" i))
		in ["(let ":var "f" i i ["=":unPrint x i ["\nin ":unPrint y (inc i) [")":c]]]]

meval :: (?a) -> ?a
meval a = a
instance expr (?)
where
	lit a = pure a
	(+.) l r = (+) <$> l <*> r
	(-.) l r = (-) <$> l <*> r
	(*.) l r = (*) <$> l <*> r
	(/.) l r = (/) <$> l <*> r
	(==.) l r = (==) <$> l <*> r
	If p t e = p >>= \b->if b t e
instance lambda (?)
where
	(@) l r = l >>= \l->l r
	\| def = pure def
instance let (?)
where
	lett def = let (x In y) = def x in y

:: Identity a =: Identity a
runIdentity (Identity a) = a
instance Functor Identity where fmap f a = Identity (f $ runIdentity a)
instance pure Identity where pure a = Identity a
instance <*> Identity where (<*>) mfa a = Identity (runIdentity mfa $ runIdentity a)
instance Monad Identity where bind ma a2mb = a2mb $ runIdentity ma
instance expr Identity
where
	lit a = pure a
	(+.) l r = (+) <$> l <*> r
	(-.) l r = (-) <$> l <*> r
	(*.) l r = (*) <$> l <*> r
	(/.) l r = (/) <$> l <*> r
	(==.) l r = (==) <$> l <*> r
	If p t e = p >>= \b->if b t e
instance lambda Identity
where
	(@) l r = l >>= \l->l r
	\| def = pure def
instance let Identity
where
	lett def = let (x In y) = def x in y

Start =
	( "--eval t1: ", eval t1
	, "\n--meval t1: ", meval t1
	, "\n--ieval t1: ", runIdentity t1
	, "\n--print t1:\n", print t1
	, "--eval t2: ", eval t2
	, "\n--meval t2: ", meval t2
	, "\n--ieval t2: ", runIdentity t2
	, "\n--print t2:\n", print t2
	)

t1 :: (v Int) | let, lambda, expr v & TC (v Int)
t1 =
	   lett \id     = (\| \x->x)
	In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
	In fac @ id @ lit 10

//Dit wil je niet zelf moeten typen......
t2 :: v Int | let, lambda, expr v & TC (v Int) & TC (v ((v Int) -> v Int)) & TC (v ((v ((v Int) -> v Int)) -> v ((v Int) -> v Int)))
t2 =
	   lett \id     = (\| \x->x)
	In lett \fix    = (\| \f->lett \x=f @ x In x)
	In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
	In lett \facfix = (\| \n->(fix @ \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1))) @ n)
	In facfix @ id @ lit 10