\documentclass[preprint,authoryear]{sigplanconf} %include lhs2TeX.fmt %include polycode.fmt \usepackage{txfonts} %format itf = "\mathbf{itf}" %format ty = "ty" %format env = "env" %format chn = "\mathbf{chn}" %format visit = "\mathbf{visit}" %format clause = "\mathbf{clause}" %format default = "\mathbf{default}" %format self = "\mathbf{self}" %format . = "." %format inh = "\mathbf{inh}" %format syn = "\mathbf{syn}" %format sem = "\mathbf{sem}" %format tail = "\mathbf{tail}" %format clause = "\mathbf{clause}" %format match = "\mathbf{match}" %format child = "\mathbf{child}" %format rename = "\mathbf{rename}" \begin{document} \begin{code} { -- Haskell code translate = sem derivExpr :: DerivExpr } itf DerivExpr visit dispatch sem derivExpr clause exprVar of dispatch clause exprApp of dispatch clause exprLam of dispatch sem exprVar match (VarS loc.nm) = lhs.expr sem exprApp match (AppS loc.f loc.a) = lhs.expr child f :: DerivExpr = translate child a :: DerivExpr = translate f.expr = loc.f a.expr = loc.a f.env = lhs.env a.env = lhs.env sem derivExpr default env itf DerivExpr syn ty :: Ty chn subst1 :: Subst data Ty = TyVar Var | TyInt | TyBool | TyArr Ty Ty data Subst -- left implicit sem derivExpr default subst1 itf Lookup inh nm :: Ident inh ty :: Ty inh env :: Env itf Unify visit dispatch inh ty1 :: Ty inh ty2 :: Ty itf Fresh inh ty :: Ty chn subst :: Ty lookup = sem lookupDeriv :: Lookup unify = sem unifyDeriv :: Unify fresh = sem freshDeriv :: Fresh sem freshDeriv (lhs.subst, loc.var) = varFresh lhs.subst lhs.ty = TyVar loc.var sem exprVar child fr :: Fresh = fresh child lk :: Lookup = lookup lk.nm = loc.nm lhs.ty = fr.ty sem exprVar fr.subst = lhs.subst1 -- pass down lhs.subst1 = fr.subst -- pass up sem exprVar rename fr subst := subst1 sem exprApp child fr :: Fresh = fresh child u :: Unify = unify rename fr subst := subst1 u.ty1 = f.ty u.ty2 = TyArr a.ty fr.ty lhs.ty = fr.ty sem unifyDeriv clause matchEqVars of dispatch clause matchVarL of dispatch clause matchVarR of dispatch clause matchArr of dispatch clause matchBase of dispatch clause matchFail of dispatch itf Unify visit dispatch chn subst1 :: Subst syn success :: Bool syn changes :: Bool visit outcome inh subst2 :: Subst syn errs :: Errs sem unifyDeriv default success = and default changes = or default errors = concat loc.ty1 = tyExpand lhs.subst1 lhs.ty1 loc.ty2 = tyExpand lhs.subst1 lhs.ty2 sem matchVars match True = sameVars lhs.ty1 lhs.ty2 || sameVars loc.ty1 loc.ty2 { -- haskell code sameVars (TyVar v1) (TyVar v2) | v1 == v2 = True sameVars _ = False } sem matchVarL match (TyVar loc.var) = loc.ty1 loc.ty = loc.ty2 sem matchVarR match (TyVar loc.var) = loc.ty2 loc.ty = loc.ty1 sem matchVarL matchVarR child f :: Ftv = ftv f.var = loc.var child b :: Bind = bind b.var = loc.var b.ty = loc.ty rename f b subst := subst1 loc.cyclic = loc.var `elem` f.vars lhs.subst1 = if loc.cyclic then lhs.subst1 else b.subst1 lhs.success = not loc.cyclic lhs.changes = not loc.cyclic lhs.errs = [CyclErr lhs.subst2 loc.var loc.ty] sem matchArr match (TyArr t1 t2) = loc.ty1 match (TyArr t3 t4) = loc.ty2 child l :: Unify = unify child r :: Unify = unify l.ty1 = t1 l.ty2 = t3 r.ty1 = t2 r.ty2 = t4 sem matchBase match True = loc.ty1 == loc.ty2 sem matchFail lhs.errs = [UnifyErr lhs.subst2 lhs.ty1 lhs.ty2] itf Ftv inh ty :: Ty syn vars :: [Var] inh subst :: Subst itf Bind inh var :: Var inh ty :: Ty chn subst :: Subst ftv = sem ftv :: Ftv bind = sem bind :: Bind sem exprLam match (LamS loc.nm loc.u loc.b) = lhs.expr child b :: DerivExpr = translate child fr :: Fresh = fresh b.expr = loc.b b.env = insertWith (++) loc.nm [loc.lk] env lhs.ty = TyArr fr.ty b.ty loc.lk = sem lookupLam :: LookupOne itf LookupOne visit dispatch inh ty :: Ty sem lookupDeriv child lk :: LookupMany = lookupMany lk.lks = find [] lhs.nm lhs.env itf LookupMany visit dispatch inh lks :: [LookupOne] inh ty :: Ty lookupMany = sem lkManyDeriv :: LookupMany sem lkManyDeriv default succeeded = or clause lkNil of dispatch clause lkCons of dispatch sem lkNil match [] = lhs.lks sem lkCons match (loc.hd : loc.tl) = lhs.lks child hd :: LookupOne = loc.lk child tl :: LookupMany = loc.tl default ty itf Lookup visit* resolve chn subst :: Subst syn status :: Status syn depth :: Int itf Lookup LookupOne LookupMany visit dispatch chn subst :: Subst syn status :: Status syn depth :: Int visit resolved data Status = Fails | Succeeds Bool Bool itf ExprDeriv inh depth :: Int sem derivExpr default depth sem exprLam b.depth = 1 + lhs.depth sem lookupLam child u :: Unify = unify rename u subst1 := subst u.ty1 = outer.fr.ty -- of enclosing sem u.ty2 = lhs.ty lhs.status = if u.success then Succeeds False u.changes else Fails lhs.depth = outer.lhs.depth sem lkNil lhs.depth = 0 lhs.subst = lhs.subst lhs.status = Fails sem lkCons hd.subst = lhs.subst tl.subst = lhs.subst (lhs.status, lhs.depth, lhs.subst) = case hd.status of Fails -> (tl.status, tl.depth, tl.subst) Succeeds _ hdChanged -> case tl.status of Fails -> (hd.status, hd.depth, hd.subst) Succeeds _ tlChanged -> let sc = Succeeds True True hdRes = (sc, hd.depth, hd.subst) tlRes = (sc, tl.depth, tl.subst) in if hdChanged && tlChanged then if hd.depth >= tl.depth then hdRes else tlRes else if hd.Changed then hdRes else tlRes sem lookupDeriv clause lkRunning of resolve match Nothing = visit.state loc.cont = detach resolved of lk visit.state = case lk.status of Success True _ -> Nothing _ -> Just loc.cont default status depth subst clause lkFinished of resolve match (Just _) = visit.resolve.state lhs.status = Fails lhs.depth = 0 default subst sem lookupDeriv visit.resolve.state = Nothing loc.mbCont = visit.resolve.state itf Expr syn self itStart :: Lookup_resolve inh self itFinished :: Lookup_resolve sem exprVar lhs.itStart = detach resolve of lk attach resolve of lk = lhs.itFinished itf Program inh expr :: ExprS syn ty :: Ty transProg = sem wrapper :: Program sem wrapper child e :: ExprDeriv e.expr = lhs.expr e.env = empty default ty (e.itFinished, e.subst2) = enumerate (fixpSolve e.subst1) e.itStart { enumerate :: Self s => (forall z . [(z, a)] -> ([(z, b)], c)) -> s a -> (s b, c) data St z = St { subst_St :: Subst, depths_St :: IntMap [Subst] , changed1_St :: Bool, changed2_St :: Bool , funs_St :: [(z, Lookup_resolve)] } fixpSolve :: Subst -> [(z, Lookup_resolve)] -> ([(z, Lookup_resolve)], Subst) fixpSolve subst items = let init = St { substSt = subst, depths_St = empty , changed1_St = True, changed2_St = True , funs_St = items } final = execState loop1 init in (funs_St final, subst_St final) loop1 :: State (St z) () loop1 = do modify (\st -> st { changed1_St = False }) loop2 defaulting changed <- gets changed1_St when changed loop1 loop2 :: State (St z) () loop2 = do funs <- gets funs_St modify (\st -> st { changed2_St = False , depths_St = empty }) funs' <- mapM appFun funs modify (\st -> st { funs_St = funs' }) changed <- gets changed2_St when changed loop2 appFun :: (z, Lookup_resolve) -> State (St z) (z, Lookup_resolve) appFun (z, fun) = do subst <- gets subst_St let inh = Inh_Lookup_resolve { subst_Inh_Lookup_resolve = subst } syn = invoke_Lookup_resolve inh subst' = subst_Syn_Lookup_resolve syn status = status_Syn_Lookup_resolve syn depth = depth_Syn_Lookup_resolve syn case status of Succeeds True _ -> modify (\st -> st { depths_St = insertWith (++) depth [subst'] (depths_St st) }) _ -> return () defaulting :: State (St z) () defaulting = do list <- gets (toAscList . depths_St) case list of (substs : _) -> modify (\st -> st { subst_St = foldl mergeSubst (subst_St st) substs }) _ -> return () } itf Expr visit generate syn trans :: ExprT syn errs :: Errs data ExprT = VarT Ident | AppT ExprT ExprT | LamT Ident ExprT sem exprVar lhs.trans = VarT lk.nm' sem exprApp lhs.trans = AppT f.trans a.trans sem exprLam lhs.trans = LamT loc.u b.trans sem exprDeriv default errs = concat itf LookupOne syn nm' :: Ident sem lookupLam lhs.nm' = outer.loc itf Lookup visit resolved syn nm' :: Ident syn errs :: Errs sem lookupDeriv clause lkAmbiguous of resolved clause lkFinal of resolved sem lkAmbiguous match Nothing = loc.mbCont lhs.nm' = lhs.nm lhs.errs = [Err_Ambiguous lhs.nm] sem lkFinal match (Just loc.cont) = loc.mbCont attach resolved of lk = loc.cont loc.names = catMaybes lk.names lhs.errs = if null lk.answers then [Err_Undefined lhs.nm] else if null loc.names then [Err_Unresolved lhs.nm] else [] lhs.nm' = head (loc.names ++ [lhs.nm]) itf LookupMany syn names :: [Maybe Ident] sem lkNil lhs.names = [] sem lkCons loc.mbName = case hd.status of Succeeds _ _ -> Just hd.nm' Fails -> Nothing lhs.names = loc.mbName : tl.names itf Expr inh subst2 :: Subst sem exprDeriv default subst2 itf Program syn ty :: Ty syn subst :: Subst syn trans :: ExprT sem wrapper default ty trans \end{code} \end{document}