module bug

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

:: 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, TC 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

import Data.Either
import Data.Tuple
:: St a = St (Env -> Either String (a, Env))
:: Env :== [(Int, Dynamic)]
instance Functor St where fmap f m = St $ fmap (appFst f) o evalSt m
instance pure St where pure x = St \s->Right (x, s)
instance <*> St where (<*>) mfa ma = ap mfa ma
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)
evalSt (St m) = 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 = if` <$> i <*> 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 >>= \s->hd [d\\(x, d :: St a^)<-s | l == x]
		in  get >>= \s->put [(l, dynamic x):s] >>| y

Start = evalSt t2 []
where
// Geeft:
/*
initial_unification_environment [module: _SystemDynamic]
_initial_unification_environment [module: _SystemDynamic]
_f111;111 [module: bug]
<lambda>[line:65];38;90 [module: bug]
<case>[line:39];27;103 [module: bug]
evalSt [module: bug]
<lambda>[line:39];23;11 [module: bug]
evalSt [module: bug]
<lambda>[line:39];23;11 [module: bug]
evalSt [module: bug]
evalSt [module: bug]
<lambda>[line:39];23;11 [module: bug]
*/
	t1  = 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 fac @ id @ lit 10
// Geeft:
/*
unify_ [module: _SystemDynamic]
unify_ [module: _SystemDynamic]
unify_ [module: _SystemDynamic]
unify_types [module: _SystemDynamic]
_unify [module: _SystemDynamic]
_f143;143 [module: bug]
<lambda>[line:65];38;101 [module: bug]
<case>[line:39];27;135 [module: bug]
evalSt [module: bug]
<lambda>[line:39];23;22 [module: bug]
evalSt [module: bug]
evalSt [module: bug]
*/
	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