module gadt

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

:: BM a b = {to :: a->b, fro :: b->a}
bm = {to=id,fro=id}
:: Expr a
	= Lit (BM a Int) Int
	| Var (BM a Int) String
	| E.e: Plus (BM a e) (Expr a) (Expr a) & + e

eval :: (Expr Int) -> ([(String, Int)] -> Either String Int)
eval (Lit _ i) = const $ pure i
eval (Var _ s) = maybe (Left $ "Undefined variable " +++ s) Right o lookup s
eval (Plus _ a b) = \s->liftM2 (+) (eval a s) (eval b s)

print :: (Expr a) -> String
print (Lit _ i) = toString i
print (Var _ s) = s
print (Plus _ a b) = print a +++ " + " +++ print b

Start = eval (Plus bm (Lit bm 5) (Lit bm 37)) []