module test

import StdEnv

:: Either l r = Left l | Right r
either f _ (Left x) = f x
either _ f (Right x) = f x
class Functor m
where
	fmap :: (a -> b) (m a) -> m b
	(<$>) infixl 4 :: (a -> b) (m a) -> m b
	(<$>) a b = fmap a b
class Applicative m
where
	pure :: a -> m a
	(<*>) infixl 4 :: (m (a -> b)) (m a) -> m b
class Monad m
where
	bind :: (m a) (a -> m b) -> m b
	(>>=) infixl 1 :: (m a) (a -> m b) -> m b
	(>>=) a b = bind a b
	(>>|) infixl 1 :: (m a) (m b) -> m b
	(>>|) a b = bind a \_->b

:: In a b = In infixl 0 a b
class lambda v
where
	(@) infixr 1 :: (v (a -> v b)) (v a) -> v b
	\| :: ((v a) -> v b) -> 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 :== [Dynamic]
instance Functor St where fmap f m = m >>= \a->pure (f a)
instance Applicative St
where
	pure x = St \s->Right (x, s)
	(<*>) mfa ma = mfa >>= \fa->ma >>= \a->pure (fa a)
instance Monad St
where
	bind ma a2mb = St \s->case evalSt ma s of
		Left err = Left err
		Right (a, s) = evalSt (a2mb a) s

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->r >>= \r->l r
	\| def = pure (def o pure)

instance let St
where
	lett def = length <$> get >>= \l->
		let (x In y) = def (get >>= deref o flip (!!) l)
		in  get >>= \s->put (s ++ [dynamic x]) >>| y

deref a = abort (toString (typeCodeOfDynamic a))
deref (a :: a^) = a
deref _ = fail "Variable not known???"

:: 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]]]]

Start =
	( "--eval t1: ", eval t1
	, "\n--print t1:\n", print t1
	, "--eval t2: ", eval t2
	, "\n--pritn 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

t2 :: (v Int) | let, lambda, expr v & TC (v Int) & TC (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