module expr_gadt
import StdEnv

:: BM a b = { ab :: a -> b, ba  :: b -> a }
bm :: BM a a
bm = {ab=id, ba=id}

:: Expr a
	= E.e: Lit (BM a e) e                    & toString e
	| E.e: Add (BM a e) (Expr e) (Expr e)    & + e
	| E.e: Eq  (BM a Bool) (Expr e) (Expr e) & == e
lit e = Lit bm e
add l r = Add bm l r
eq l r = Eq bm l r

eval :: (Expr a) -> a
eval (Lit bm e)   = bm.ba e
eval (Add bm l r) = bm.ba (eval l + eval r)
eval (Eq  bm l r) = bm.ba (eval l == eval r)

print :: (Expr a) -> String
print (Lit _ e)   = toString e
print (Add _ l r) = print l +++ "+" +++ print r
print (Eq  _ l r) = print l +++ "==" +++ print r

Start = 42