tal (empty) → 0.1.0.0
raw patch · 11 files changed
+3373/−0 lines, 11 filesdep +basedep +containersdep +mtlsetup-changed
Dependencies added: base, containers, mtl, pretty, transformers, unbound
Files
- LICENSE +22/−0
- README.md +34/−0
- Setup.hs +2/−0
- src/A.hs +515/−0
- src/C.hs +470/−0
- src/F.hs +354/−0
- src/K.hs +329/−0
- src/TAL.hs +690/−0
- src/Translate.hs +738/−0
- src/Util.hs +184/−0
- tal.cabal +35/−0
+ LICENSE view
@@ -0,0 +1,22 @@+The MIT License (MIT)++Copyright (c) 2015 Stephanie Weirich++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.+
+ README.md view
@@ -0,0 +1,34 @@+An implementation of a type-preserving Compiler, derived from the paper++[From System F to Typed Assembly Language](https://www.cs.princeton.edu/~dpw/papers/tal-toplas.pdf)+by Morrisett, Walker, Crary, Glew++I was inspired to implement this paper while preparing a +[talk](https://www.youtube.com/watch?v=Epbaka9uTQ4) for Papers We Love Philadelphia. ++The implementation includes all passes described in the paper:++* F ==> K (Typed CPS conversion)+* K ==> C (Polymorphic closure conversion)+* C ==> H (Hoisting, reuses the C language)+* H ==> A (Allocation)+* A ==> TAL (Code generation)++Each language (F, K, C, A, TAL) is defined in the corresponding source+file. These implementations include the abstract syntax, small-step+operational semantics, and type checker for the languages. The file+[Util.hs](src/Util.hs) contains definitions common to all implementations.++The compiler itself is in the file [Translate.hs](src/Translate.hs). To run+the compiler, load this file into ghci and try out one of the sample programs+from [F.hs](src/F.hs).++In particular, you can try++ Translate*> printM $ compile F.sixfact++to see the TAL output for the factorial function applied to six.++If you would like to compile and then run this function you can try:++ Translate*> test F.sixfact
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/A.hs view
@@ -0,0 +1,515 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ TupleSections,+ GADTs #-}++module A where++++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)++import Unbound.LocallyNameless.Alpha+import Unbound.LocallyNameless.Types++import Control.Monad+import Control.Monad.Except++import Data.Monoid (Monoid(..))++import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+++import Util+import Text.PrettyPrint as PP+++------------------+-- should move to Unbound.LocallyNameless.Ops+-- patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t+-- patUnbind p (B _ t) = openT p t+------------------+++-- System A++type TyName = Name Ty+type ValName = Name Val++data Flag = Un | Init+ deriving (Eq, Ord, Show)++data Ty = TyVar TyName+ | TyInt+ | All (Bind [TyName] [Ty])+ | TyProd [(Ty, Flag)] -- new+ | Exists (Bind TyName Ty) + deriving Show++data Val = TmInt Int+ | TmVar ValName+ | TApp (Ann Val) Ty + | Pack Ty (Ann Val) + deriving Show + +data Ann v = Ann v Ty+ deriving Show+ +data Decl = + DeclVar ValName (Embed (Ann Val))+ | DeclPrj Int ValName (Embed (Ann Val))+ | DeclPrim ValName (Embed ((Ann Val), Prim, (Ann Val)))+ | DeclUnpack TyName ValName (Embed (Ann Val)) + | DeclMalloc ValName (Embed [Ty]) -- new+ | DeclAssign ValName (Embed ((Ann Val), Int, (Ann Val))) --new+ -- x = v1 [i] <- v2+ deriving Show+ +data Tm = + Let (Bind Decl Tm)+ | App (Ann Val) [(Ann Val)] + | TmIf0 (Ann Val) Tm Tm+ | Halt Ty (Ann Val) + deriving Show++data HeapVal = + Tuple [(Ann Val)]+ | Code (Bind [TyName] (Bind [ValName] Tm))+ deriving Show++newtype Heap = Heap (Map ValName (Ann HeapVal)) deriving Show++instance Monoid A.Heap where+ mempty = A.Heap Map.empty+ mappend (A.Heap h1) (A.Heap h2) = A.Heap (Map.union h1 h2)++$(derive [''HeapVal, ''Flag, ''Ty, ''Val, ''Ann, ''Decl, ''Tm])++------------------------------------------------------+instance Alpha Flag+instance Alpha Ty +instance Alpha Val +instance Alpha a => Alpha (Ann a)+instance Alpha Decl+instance Alpha Tm++instance Subst Ty Ty where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+instance Subst Ty Prim+instance Subst Ty Tm+instance Subst Ty (Ann Val)+instance Subst Ty Decl+instance Subst Ty Val+instance Subst Ty Flag++instance Subst Val Flag+instance Subst Val Prim+instance Subst Val Ty+instance Subst Val (Ann Val)+instance Subst Val Decl+instance Subst Val Tm+instance Subst Val Val where+ isvar (TmVar x) = Just (SubstName x)+ isvar _ = Nothing+ +------------------------------------------------------+-- Helper functions+------------------------------------------------------++mkTyApp :: (MonadError String m, Fresh m) => (Ann Val) -> [Ty] -> m (Ann Val)+mkTyApp av [] = return av+mkTyApp av@(Ann _ (All bnd)) (ty:tys) = do+ (as, atys) <- unbind bnd + case as of + a:as' -> + let atys' = subst a ty atys in+ mkTyApp (Ann (TApp av ty) (All (bind as' atys'))) tys+ _ -> throwError "type error: not a polymorphic All"+mkTyApp (Ann _ ty) _ = throwError "type error: not an All"++lets :: [Decl] -> Tm -> Tm+lets [] tm = tm +lets (d:ds) tm = Let (bind d (lets ds tm))++-----------------------------------------------------------------+-- Free variables, with types+-----------------------------------------------------------------++x :: Name Tm+y :: Name Tm+z :: Name Tm+(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")++a :: Name Ty+b :: Name Ty+c :: Name Ty+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------++type Delta = [ TyName ]+type Gamma = [ (ValName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+ if List.elem v (getDelta g) then+ return ()+ else+ throwError $ "Type variable not found " ++ (show v)++lookupTmVar :: Ctx -> ValName -> M Ty+lookupTmVar g v = do+ case lookup v (getGamma g) of+ Just s -> return s+ Nothing -> throwError $ "Term variable notFound " ++ (show v)++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta = n : (getDelta ctx) }++extendTys :: [TyName] -> Ctx -> Ctx+extendTys ns ctx = foldr extendTy ctx ns++extendTm :: ValName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++extendTms :: [ValName] -> [Ty] -> Ctx -> Ctx+extendTms [] [] ctx = ctx+extendTms (n:ns) (ty:tys) ctx = extendTm n ty (extendTms ns tys ctx)++{-+extendDecl :: Decl -> Ctx -> Ctx+extendDecl (DeclVar x (Embed (Ann _ ty))) = extendTm x ty+extendDecl (DeclPrj i x (Embed (Ann _ (TyProd tys)))) = extendTm x (tys !! i) +extendDecl (DeclPrim x _) = extendTm x TyInt+extendDecl (DeclUnpack b x (Embed (Ann _ (Exists bnd)))) = + extendTy b . extendTm x (patUnbind b bnd)+-}+++tcty :: Ctx -> Ty -> M ()+tcty g (TyVar x) =+ checkTyVar g x+tcty g (All b) = do+ (xs, tys) <- unbind b+ let g' = extendTys xs g -- XX+ mapM_ (tcty g') tys+tcty g TyInt = return ()+tcty g (TyProd tys) = do+ mapM_ (tcty g . fst) tys+tcty g (Exists b) = do + (a, ty) <- unbind b+ tcty (extendTy a g) ty+++typecheckHeapVal :: Ctx -> Ann HeapVal -> M Ty+typecheckHeapVal g (Ann (Code bnd) (All bnd')) = do + mb <- unbind2 bnd bnd' -- may fail+ case mb of + Just (as, bnd2, _, tys) -> do+ (xs, e) <- unbind bnd2+ let g' = extendTys as g+ mapM_ (tcty g') tys+ typecheck (extendTms xs tys g') e+ return (All bnd')+ Nothing -> throwError "wrong # of type variables"+ +typecheckHeapVal g (Ann (Tuple es) ty) = do + tys <- mapM (typecheckAnnVal g) es+ let ty' = TyProd $ map (,Un) tys + if ty `aeq` ty' + then return ty+ else throwError "incorrect annotation on tuple"++typecheckVal :: Ctx -> Val -> M Ty+typecheckVal g (TmVar x) = lookupTmVar g x+typecheckVal g (TmInt i) = return TyInt+typecheckVal g (TApp av ty) = do+ tcty g ty+ ty' <- typecheckAnnVal g av+ case ty' of + All bnd -> do + (as, bs) <- unbind bnd+ case as of + [] -> throwError "can't instantiate non-polymorphic function"+ (a:as') -> do+ let bs' = subst a ty bs+ return (All (bind as' bs'))++typecheckAnnVal g (Ann (Pack ty1 av) ty) = do+ case ty of + Exists bnd -> do + (a, ty2) <- unbind bnd+ tcty g ty1+ ty' <- typecheckAnnVal g av+ if (not (ty' `aeq` subst a ty1 ty2)) + then throwError "type error"+ else return ty +typecheckAnnVal g (Ann v ty) = do + tcty g ty+ ty' <- typecheckVal g v + if (ty `aeq` ty') + then return ty+ else throwError $ "wrong annotation on: " ++ pp v ++ "\nInferred: " ++ pp ty' ++ "\nAnnotated: " ++ pp ty ++typecheckDecl g (DeclVar x (Embed av)) = do+ ty <- typecheckAnnVal g av+ return $ extendTm x ty g+typecheckDecl g (DeclPrj i x (Embed av@(Ann v _))) = do+ ty <- typecheckAnnVal g av+ case ty of + TyProd tys | i < length tys -> + return $ extendTm x (fst (tys !! i)) g+ _ -> throwError "cannot project"+typecheckDecl g (DeclPrim x (Embed (av1, _, av2))) = do+ ty1 <- typecheckAnnVal g av1+ ty2 <- typecheckAnnVal g av2+ case (ty1 , ty2) of + (TyInt, TyInt) -> return $ extendTm x TyInt g+ _ -> throwError "TypeError"+typecheckDecl g (DeclUnpack a x (Embed av)) = do+ tya <- typecheckAnnVal g av+ case tya of + Exists bnd -> do + let ty = patUnbind a bnd + return $ extendTy a (extendTm x ty g)+ _ -> throwError "TypeError"+typecheckDecl g (DeclMalloc x (Embed tys)) = do + mapM_ (tcty g) tys+ return $ extendTm x (TyProd (map (,Un) tys)) g +typecheckDecl g (DeclAssign x (Embed (av1@(Ann v1 _), i, av2))) = do+ ty1 <- typecheckAnnVal g av1 + ty2 <- typecheckAnnVal g av2+ case ty1 of + TyProd tys | i < length tys -> + let (xs,(ty,_):ys) = splitAt i tys in+ if ty `aeq` ty2 + then return $ extendTm x (TyProd (xs ++ (ty,Init) : ys)) g+ else throwError "TypeError"+ +typecheck :: Ctx -> Tm -> M ()+typecheck g (Let bnd) = do+ (d,e) <- unbind bnd+ g' <- typecheckDecl g d+ typecheck g' e+typecheck g (App av es) = do+ ty <- typecheckAnnVal g av+ case ty of+ (All bnd) -> do+ (as, argtys) <- unbind bnd+ argtys' <- mapM (typecheckAnnVal g) es+ if length as /= 0 + then throwError "must use type application"+ else + if (length argtys /= length argtys') + then throwError "incorrect args"+ else if (not (all id (zipWith aeq argtys argtys'))) then + throwError "arg mismatch"+ else return ()+typecheck g (TmIf0 av e1 e2) = do+ ty0 <- typecheckAnnVal g av+ typecheck g e1+ typecheck g e2+ if ty0 `aeq` TyInt then + return ()+ else + throwError "TypeError"+typecheck g (Halt ty av) = do+ ty' <- typecheckAnnVal g av+ if (not (ty `aeq` ty'))+ then throwError "type error"+ else return ()+ + +progcheck (tm, Heap m) = do+ let g = + Map.foldlWithKey (\ctx x (Ann _ ty) -> extendTm x ty ctx) + emptyCtx m+ mapM_ (typecheckHeapVal g) (Map.elems m)+ typecheck g tm++++-----------------------------------------------------------------+-- Small-step semantics+-----------------------------------------------------------------+ +{-+mkSubst :: Decl -> M (Tm,Heap) -> (Tm,Heap)+mkSubst (DeclVar x (Embed (Ann v _))) = return $ subst x v+mkSubst (DeclPrj i x (Embed (Ann (TmProd avs) _))) | i < length avs =+ let Ann vi _ = avs !! i in return $ subst x vi+mkSubst (DeclPrim x (Embed (Ann (TmInt i1) _, p, Ann (TmInt i2) _))) = + let v = TmInt (evalPrim p i1 i2) in+ return $ subst x v+mkSubst (DeclUnpack a x (Embed (Ann (Pack ty (Ann u _)) _))) = + return $ subst a ty . subst x u +mkSubst (DeclPrj i x (Embed av)) = + throwError $ "invalid prj " ++ pp i ++ ": " ++ pp av+mkSubst (DeclUnpack a x (Embed av)) = + throwError $ "invalid unpack:" ++ pp av++++step :: (Tm, Heap) -> M (Tm, Heap)++step (Let bnd, heap) = do+ (d, e) <- unbind bnd+ ss <- mkSubst d+ return $ ss (e, heap)+ +step (App (Ann e1@(Fix bnd) _) avs) = do+ ((f, as), bnd2) <- unbind bnd+ (xtys, e) <- unbind bnd2+ let us = map (\(Ann u _) -> u) avs+ let xs = map fst xtys+ return $ substs ((f,e1):(zip xs us)) e++step (TmIf0 (Ann (TmInt i) _) e1 e2) = if i==0 then return e1 else return e2++step _ = throwError "cannot step"+ +evaluate :: Tm -> M Val+evaluate (Halt _ (Ann v _)) = return v+evaluate e = do+ e' <- step e+ evaluate e'+-} +-----------------------------------------------------------------+-- Pretty-printer+-----------------------------------------------------------------++instance Display Ty where+ display (TyVar n) = display n+ display (TyInt) = return $ text "Int"+ display (All bnd) = lunbind bnd $ \ (as,tys) -> do+ da <- displayList as+ dt <- displayList tys+ if null as + then return $ parens dt <+> text "-> void"+ else prefix "forall" (brackets da <> text "." <+> parens dt <+> text "-> void")+ display (TyProd tys) = displayTuple tys+ display (Exists bnd) = lunbind bnd $ \ (a,ty) -> do+ da <- display a + dt <- display ty+ prefix "exists" (da <> text "." <+> dt)+ +instance Display (Ty, Flag) where + display (ty, fl) = do+ dty <- display ty+ let f = case fl of { Un -> "0" ; Init -> "1" }+ return $ dty <> text "^" <> text f+ +instance Display (ValName,Embed Ty) where + display (n, Embed ty) = do+ dn <- display n+ dt <- display ty+ return $ dn <> colon <> dt+ +instance Display Val where + display (TmInt i) = return $ int i+ display (TmVar n) = display n+ display (Pack ty e) = do + dty <- display ty+ de <- display e + prefix "pack" (brackets (dty <> comma <> de))+ display (TApp av ty) = do+ dv <- display av+ dt <- display ty+ return $ dv <+> (brackets dt)++instance Display HeapVal where+ display (Code bnd) = lunbind bnd $ \(as, bnd2) -> lunbind bnd2 $ \(xtys, e) -> do+ ds <- displayList as + dargs <- displayList xtys+ de <- withPrec (precedence "code") $ display e+ let tyArgs = if null as then empty else brackets ds+ let tmArgs = if null xtys then empty else parens dargs+ prefix "code" (tyArgs <> tmArgs <> text "." $$ de)+ + display (Tuple es) = displayTuple es+ ++instance Display a => Display (Ann a) where+{- display (Ann av ty) = do+ da <- display av+ dt <- display ty+ return $ parens (da <> text ":" <> dt) -}+ display (Ann av _) = display av++instance Display Tm where+ display (App av args) = do+ da <- display av+ dargs <- displayList args+ let tmArgs = if null args then empty else space <> parens dargs+ return $ da <> tmArgs+ display (Halt ty v) = do + dv <- display v+ --dt <- display ty+ return $ text "halt" <+> dv -- <+> text ":" <+> dt+ display (Let bnd) = lunbind bnd $ \(d, e) -> do+ dd <- display d+ de <- display e+ return $ (text "let" <+> dd <+> text "in" $$ de)+ display (TmIf0 e0 e1 e2) = do+ d0 <- display e0+ d1 <- display e1+ d2 <- display e2+ prefix "if0" $ parens $ sep [d0 <> comma , d1 <> comma, d2]++instance Display Decl where+ display (DeclVar x (Embed av)) = do+ dx <- display x+ dv <- display av+ return $ dx <+> text "=" <+> dv+ display (DeclPrj i x (Embed av)) = do+ dx <- display x+ dv <- display av+ return $ dx <+> text "=" <+> text "pi" <> int i <+> dv+ display (DeclPrim x (Embed (e1, p, e2))) = do+ dx <- display x+ let str = show p+ d1 <- display e1 + d2 <- display e2 + return $ dx <+> text "=" <+> d1 <+> text str <+> d2+ display (DeclUnpack a x (Embed av)) = do+ da <- display a+ dx <- display x+ dav <- display av+ return $ brackets (da <> comma <> dx) <+> text "=" <+> dav+ display (DeclMalloc x (Embed tys)) = do+ dx <- display x+ dtys <- displayTuple tys+ return $ dx <+> text "= malloc" <> dtys+ display (DeclAssign x (Embed (av1, i, av2))) = do+ dx <- display x+ dav1 <- display av1+ dav2 <- display av2+ return $ dx <+> text "=" <+> dav1 <+> brackets (text (show i)) + <+> text "<-" <+> dav2++instance Display Heap where+ display (Heap m) = do+ fcns <- mapM (\(d,v) -> do + dn <- display d+ dv <- display v+ return (dn, dv)) (Map.toList m)+ return $ hang (text "letrec") 2 $ + vcat [ n <+> text "=" <+> dv | (n,dv) <- fcns ]++instance Display (Tm, Heap) where+ display (tm,h) = do+ dh <- display h+ dt <- display tm+ return $ dh $$ text "in" <+> dt
+ src/C.hs view
@@ -0,0 +1,470 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ GADTs #-}++module C where++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)++import Unbound.LocallyNameless.Alpha+import Unbound.LocallyNameless.Types++import Control.Monad+import Control.Monad.Except++import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+++import Util+import Text.PrettyPrint as PP+++------------------+-- should move to Unbound.LocallyNameless.Ops+-- patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t+-- patUnbind p (B _ t) = openT p t+------------------+++-- System C++type TyName = Name Ty+type TmName = Name Tm+type ValName = Name Val++data Ty = TyVar TyName+ | TyInt+ | All (Bind [TyName] [Ty])+ | TyProd [Ty]+ | Exists (Bind TyName Ty) -- new+ deriving Show++data Val = TmInt Int+ | TmVar ValName+ | Fix (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm))+ | TmProd [AnnVal]+ | TApp AnnVal Ty -- new+ | Pack Ty AnnVal -- new+ deriving Show + +data AnnVal = Ann Val Ty+ deriving Show+ +data Decl = + DeclVar ValName (Embed AnnVal)+ | DeclPrj Int ValName (Embed AnnVal)+ | DeclPrim ValName (Embed (AnnVal, Prim, AnnVal))+ | DeclUnpack TyName ValName (Embed AnnVal) -- new+ deriving Show+ +data Tm = Let (Bind Decl Tm)+ | App AnnVal [AnnVal] -- updated+ | TmIf0 AnnVal Tm Tm+ | Halt Ty AnnVal + deriving Show++-- For H++newtype Heap = Heap (Map ValName AnnVal) deriving Show++$(derive [''Ty, ''Val, ''AnnVal, ''Decl, ''Tm])++------------------------------------------------------+instance Alpha Ty +instance Alpha Val +instance Alpha AnnVal+instance Alpha Decl+instance Alpha Tm++instance Subst Ty Ty where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+instance Subst Ty Prim+instance Subst Ty Tm+instance Subst Ty AnnVal+instance Subst Ty Decl+instance Subst Ty Val+++instance Subst Val Prim+instance Subst Val Ty+instance Subst Val AnnVal+instance Subst Val Decl+instance Subst Val Tm+instance Subst Val Val where+ isvar (TmVar x) = Just (SubstName x)+ isvar _ = Nothing+ +------------------------------------------------------+-- Helper functions+------------------------------------------------------++mkTyApp :: (MonadError String m, Fresh m) => AnnVal -> [Ty] -> m AnnVal+mkTyApp av [] = return av+mkTyApp av@(Ann _ (All bnd)) (ty:tys) = do+ (as, atys) <- unbind bnd + case as of + a:as' -> + let atys' = subst a ty atys in+ mkTyApp (Ann (TApp av ty) (All (bind as' atys'))) tys+ _ -> throwError "type error: not a polymorphic All"+mkTyApp (Ann _ ty) _ = throwError "type error: not an All"++mkProd :: [AnnVal] -> AnnVal+mkProd vs = Ann (TmProd vs) (TyProd tys) where+ tys = map (\(Ann _ ty) -> ty) vs ++-----------------------------------------------------------------+-- Free variables, with types+-----------------------------------------------------------------++x :: Name Tm+y :: Name Tm+z :: Name Tm+(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")++a :: Name Ty+b :: Name Ty+c :: Name Ty+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (ValName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+ if List.elem v (getDelta g) then+ return ()+ else+ throwError $ "Type variable not found " ++ (show v)++lookupTmVar :: Ctx -> ValName -> M Ty+lookupTmVar g v = do+ case lookup v (getGamma g) of+ Just s -> return s+ Nothing -> throwError $ "Term variable notFound " ++ (show v)++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta = n : (getDelta ctx) }++extendTys :: [TyName] -> Ctx -> Ctx+extendTys ns ctx = foldr extendTy ctx ns++extendTm :: ValName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++extendTms :: [ValName] -> [Ty] -> Ctx -> Ctx+extendTms [] [] ctx = ctx+extendTms (n:ns) (ty:tys) ctx = extendTm n ty (extendTms ns tys ctx)++extendDecl :: Decl -> Ctx -> Ctx+extendDecl (DeclVar x (Embed (Ann _ ty))) = extendTm x ty+extendDecl (DeclPrj i x (Embed (Ann _ (TyProd tys)))) = extendTm x (tys !! i) +extendDecl (DeclPrim x _) = extendTm x TyInt+extendDecl (DeclUnpack b x (Embed (Ann _ (Exists bnd)))) = + extendTy b . extendTm x (patUnbind b bnd)+ +++tcty :: Ctx -> Ty -> M ()+tcty g (TyVar x) =+ checkTyVar g x+tcty g (All b) = do+ (xs, tys) <- unbind b+ let g' = extendTys xs g -- XX+ mapM_ (tcty g') tys+tcty g TyInt = return ()+tcty g (TyProd tys) = do+ mapM_ (tcty g) tys+tcty g (Exists b) = do + (a, ty) <- unbind b+ tcty (extendTy a g) ty+++typecheckVal :: Ctx -> Val -> M Ty+typecheckVal g (TmVar x) = lookupTmVar g x+typecheckVal g (Fix bnd) = do+ ((f, as), bnd2) <- unbind bnd+ (xtys, e) <- unbind bnd2+ let g' = extendTys as g+ let (xs,tys) = unzip $ map (\(x,Embed y) -> (x,y)) xtys + mapM_ (tcty g') tys+ let fty = All (bind as tys)+ typecheck (extendTm f fty (extendTms xs tys g')) e+ return fty+typecheckVal g (TmProd es) = do + tys <- mapM (typecheckAnnVal g) es+ return $ TyProd tys+typecheckVal g (TmInt i) = return TyInt+typecheckVal g (TApp av ty) = do+ tcty g ty+ ty' <- typecheckAnnVal g av+ case ty' of + All bnd -> do + (as, bs) <- unbind bnd+ case as of + [] -> throwError "can't instantiate non-polymorphic function"+ (a:as') -> do+ let bs' = subst a ty bs+ return (All (bind as' bs'))++typecheckAnnVal g (Ann (Pack ty1 av) ty) = do+ case ty of + Exists bnd -> do + (a, ty2) <- unbind bnd+ tcty g ty1+ ty' <- typecheckAnnVal g av+ if (not (ty' `aeq` subst a ty1 ty2)) + then throwError "type error"+ else return ty +typecheckAnnVal g (Ann v ty) = do + tcty g ty+ ty' <- typecheckVal g v + if (ty `aeq` ty') + then return ty+ else throwError $ "wrong annotation on: " ++ pp v ++ "\nInferred: " ++ pp ty ++ "\nAnnotated: " ++ pp ty' ++typecheckDecl g (DeclVar x (Embed av)) = do+ ty <- typecheckAnnVal g av+ return $ extendTm x ty g+typecheckDecl g (DeclPrj i x (Embed av)) = do+ ty <- typecheckAnnVal g av+ case ty of + TyProd tys | i < length tys -> + return $ extendTm x (tys !! i) g+ _ -> throwError "cannot project"+typecheckDecl g (DeclPrim x (Embed (av1, _, av2))) = do+ ty1 <- typecheckAnnVal g av1+ ty2 <- typecheckAnnVal g av2+ case (ty1 , ty2) of + (TyInt, TyInt) -> return $ extendTm x TyInt g+ _ -> throwError "TypeError"+typecheckDecl g (DeclUnpack a x (Embed av)) = do+ tya <- typecheckAnnVal g av+ case tya of + Exists bnd -> do + let ty = patUnbind a bnd + return $ extendTy a (extendTm x ty g)+ _ -> throwError "TypeError"+ +typecheck :: Ctx -> Tm -> M ()+typecheck g (Let bnd) = do+ (d,e) <- unbind bnd+ g' <- typecheckDecl g d+ typecheck g' e+typecheck g (App av es) = do+ ty <- typecheckAnnVal g av+ case ty of+ (All bnd) -> do+ (as, argtys) <- unbind bnd+ argtys' <- mapM (typecheckAnnVal g) es+ if length as /= 0 + then throwError "must use type application"+ else + if (length argtys /= length argtys') + then throwError "incorrect args"+ else if (not (all id (zipWith aeq argtys argtys'))) then + throwError "arg mismatch"+ else return ()+typecheck g (TmIf0 av e1 e2) = do+ ty0 <- typecheckAnnVal g av+ typecheck g e1+ typecheck g e2+ if ty0 `aeq` TyInt then + return ()+ else + throwError "TypeError"+typecheck g (Halt ty av) = do+ ty' <- typecheckAnnVal g av+ if (not (ty `aeq` ty'))+ then throwError "type error"+ else return ()++-----------------------------------------------------------------++heapvalcheck g ann@(Ann (Fix bnd) _) = + typecheckAnnVal g ann+heapvalcheck g (Ann _ _) = + throwError "type error: only code in heap"+ +hoistcheck (tm, Heap m) = do+ let g' = + Map.foldlWithKey (\ctx x (Ann _ ty) -> extendTm x ty ctx) + emptyCtx m+ mapM_ (heapvalcheck g') (Map.elems m)+ typecheck g' tm+ +-----------------------------------------------------------------+-- Small-step semantics+-----------------------------------------------------------------+ +mkSubst :: Decl -> M (Tm -> Tm)+mkSubst (DeclVar x (Embed (Ann v _))) = return $ subst x v+mkSubst (DeclPrj i x (Embed (Ann (TmProd avs) _))) | i < length avs =+ let Ann vi _ = avs !! i in return $ subst x vi+mkSubst (DeclPrim x (Embed (Ann (TmInt i1) _, p, Ann (TmInt i2) _))) = + let v = TmInt (evalPrim p i1 i2) in+ return $ subst x v+mkSubst (DeclUnpack a x (Embed (Ann (Pack ty (Ann u _)) _))) = + return $ subst a ty . subst x u+mkSubst (DeclPrj i x (Embed av)) = + throwError $ "invalid prj " ++ pp i ++ ": " ++ pp av+mkSubst (DeclUnpack a x (Embed av)) = + throwError $ "invalid unpack:" ++ pp av++++step :: Tm -> M Tm++step (Let bnd) = do+ (d, e) <- unbind bnd+ ss <- mkSubst d+ return $ ss e+ +step (App (Ann e1@(Fix bnd) _) avs) = do+ ((f, as), bnd2) <- unbind bnd+ (xtys, e) <- unbind bnd2+ let us = map (\(Ann u _) -> u) avs+ let xs = map fst xtys+ return $ substs ((f,e1):(zip xs us)) e++step (TmIf0 (Ann (TmInt i) _) e1 e2) = if i==0 then return e1 else return e2++step _ = throwError "cannot step"+ +evaluate :: Tm -> M Val+evaluate (Halt _ (Ann v _)) = return v+evaluate e = do+ e' <- step e+ evaluate e'+ +-----------------------------------------------------------------+-- Pretty-printer+-----------------------------------------------------------------++instance Display Ty where+ display (TyVar n) = display n+ display (TyInt) = return $ text "Int"+ display (All bnd) = lunbind bnd $ \ (as,tys) -> do+ da <- displayList as+ dt <- displayList tys+ if null as + then return $ parens dt <+> text "-> void"+ else prefix "forall" (brackets da <> text "." <+> parens dt <+> text "-> void")+ display (TyProd tys) = displayTuple tys+ display (Exists bnd) = lunbind bnd $ \ (a,ty) -> do+ da <- display a + dt <- display ty+ prefix "exists" (da <> text "." <+> dt)+ +instance Display (ValName,Embed Ty) where + display (n, Embed ty) = do+ dn <- display n+ dt <- display ty+ return $ dn <> colon <> dt+ +instance Display Val where + display (TmInt i) = return $ int i+ display (TmVar n) = display n+ display (Fix bnd) = lunbind bnd $ \((f, as), bnd2) -> lunbind bnd2 $ \(xtys, e) -> do+ df <- display f + ds <- displayList as + dargs <- displayList xtys+ de <- withPrec (precedence "fix") $ display e+ let tyArgs = if null as then empty else brackets ds+ let tmArgs = if null xtys then empty else parens dargs+ if f `elem` (fv e :: [ValName])+ then prefix "fix" (df <+> tyArgs <> tmArgs <> text "." $$ de)+ else prefix "\\" (tyArgs <> tmArgs <> text "." $$ de)+ + display (TmProd es) = displayTuple es+ + display (Pack ty e) = do + dty <- display ty+ de <- display e + prefix "pack" (brackets (dty <> comma <> de))+ display (TApp av ty) = do+ dv <- display av+ dt <- display ty+ return $ dv <+> (brackets dt)++instance Display AnnVal where+{- display (Ann av ty) = do+ da <- display av+ dt <- display ty+ return $ parens (da <> text ":" <> dt) -}+ display (Ann av _) = display av++instance Display Tm where+ display (App av args) = do+ da <- display av+ dargs <- displayList args+ let tmArgs = if null args then empty else space <> parens dargs+ return $ da <> tmArgs+ display (Halt ty v) = do + dv <- display v+ --dt <- display ty+ return $ text "halt" <+> dv -- <+> text ":" <+> dt+ display (Let bnd) = lunbind bnd $ \(d, e) -> do+ dd <- display d+ de <- display e+ return $ (text "let" <+> dd <+> text "in" $$ de)+ display (TmIf0 e0 e1 e2) = do+ d0 <- display e0+ d1 <- display e1+ d2 <- display e2+ prefix "if0" $ parens $ sep [d0 <> comma , d1 <> comma, d2]++instance Display Decl where+ display (DeclVar x (Embed av)) = do+ dx <- display x+ dv <- display av+ return $ dx <+> text "=" <+> dv+ display (DeclPrj i x (Embed av)) = do+ dx <- display x+ dv <- display av+ return $ dx <+> text "=" <+> text "pi" <> int i <+> dv+ display (DeclPrim x (Embed (e1, p, e2))) = do+ dx <- display x+ let str = show p+ d1 <- display e1 + d2 <- display e2 + return $ dx <+> text "=" <+> d1 <+> text str <+> d2+ display (DeclUnpack a x (Embed av)) = do+ da <- display a+ dx <- display x+ dav <- display av+ return $ brackets (da <> comma <> dx) <+> text "=" <+> dav+ +--------------------------------------------+-- C to H (actually C) Hoisting+-------------------------------------------- ++displayCode (Ann v ty) = display v++instance Display Heap where+ display (Heap m) = do+ fcns <- mapM (\(d,v) -> do + dn <- display d+ dv <- displayCode v+ return (dn, dv)) (Map.toList m)+ return $ hang (text "letrec") 2 $ + vcat [ n <+> text "=" <+> dv | (n,dv) <- fcns ]++instance Display (Tm, Heap) where+ display (tm,h) = do+ dh <- display h+ dt <- display tm+ return $ dh $$ text "in" <+> dt
+ src/F.hs view
@@ -0,0 +1,354 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ GADTs #-}++module F where++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl)++import Control.Monad+import Control.Monad.Trans.Except+import qualified Data.List as List++import Util+import Text.PrettyPrint as PP++------------------------------------------------------+-- System F with type and term variables+------------------------------------------------------++type TyName = Name Ty+type TmName = Name Tm++data Ty = TyVar TyName+ | TyInt+ | Arr Ty Ty+ | All (Bind TyName Ty)+ | TyProd [Ty]+ deriving Show++data Tm = TmInt Int+ | TmVar TmName+ | Fix (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)+ | App Tm Tm+ | TmProd [Tm]+ | TmPrj Tm Int+ | TmPrim Tm Prim Tm + | TmIf0 Tm Tm Tm+ | TLam (Bind TyName Tm)+ | TApp Tm Ty+ | Ann Tm Ty+ deriving Show+++$(derive [''Ty, ''Tm])++------------------------------------------------------+instance Alpha Ty +instance Alpha Tm ++instance Subst Tm Prim +instance Subst Tm Ty+instance Subst Ty Prim+instance Subst Ty Tm+instance Subst Tm Tm where+ isvar (TmVar x) = Just (SubstName x)+ isvar _ = Nothing+instance Subst Ty Ty where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+ +------------------------------------------------------+-- Example terms+------------------------------------------------------++x :: Name Tm+y :: Name Tm+z :: Name Tm+f :: Name Tm+n :: Name Tm+(x,y,z,f,n) = (string2Name "x", string2Name "y", string2Name "z", string2Name "f", string2Name "n")++a :: Name Ty+b :: Name Ty+c :: Name Ty+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")++-- /\a. \x:a. x+polyid :: Tm+polyid = TLam (bind a (Fix (bind (y, x, Embed (TyVar a, TyVar a)) (TmVar x))))+++-- /\a. \x:a. x+polyconst :: Tm+polyconst = TLam (bind a (Fix (bind (y, x, Embed (TyVar a, TyInt)) (TmInt 3))))+++-- All a. a -> a+polyidty :: Ty+polyidty = All (bind a (Arr (TyVar a) (TyVar a)))+++two :: Tm+two = App (Fix (bind (y, x, Embed (TyInt, TyInt))+ (TmPrim (TmVar x) Plus (TmInt 1)))) (TmInt 1)++-- 1 + 1+onePlusOne :: Tm +onePlusOne = TmPrim (TmInt 1) Plus (TmInt 1)++-- Factorial function applied to 6+sixfact :: Tm+sixfact = App (Fix (bind (f, n, Embed (TyInt, TyInt))+ (TmIf0 (TmVar n) (TmInt 1) + (TmPrim (TmVar n) Times+ (App (TmVar f) + (TmPrim (TmVar n) Minus (TmInt 1))))))) (TmInt 6)++++-- /\a. \f:a. \x:a. f+ctrue :: Tm+ctrue = TLam (bind a + (Fix (bind (y,n, Embed (TyVar a, (Arr (TyVar a) (TyVar a))))+ (Fix (bind (z, x, Embed (TyVar a, TyVar a))+ (TmVar n))))))+++-- /\a. \f:a -> a. \x:a. f (f x)+twice = TLam (bind a + (Fix (bind (y,f, Embed (Arr (TyVar a) (TyVar a), + (Arr (TyVar a) (TyVar a))))+ (Fix (bind (z, x, Embed (TyVar a, TyVar a))+ (App (TmVar f) (App (TmVar f) (TmVar x))))))))+ ++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (TmName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+ if List.elem v (getDelta g) then+ return ()+ else+ throwE "NotFound"++lookupTmVar :: Ctx -> TmName -> M Ty+lookupTmVar g v = do+ case lookup v (getGamma g) of+ Just s -> return s+ Nothing -> throwE "NotFound"++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta = n : (getDelta ctx) }++extendTm :: TmName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++-- could be replaced with fv+tcty :: Ctx -> Ty -> M ()+tcty g (TyVar x) =+ checkTyVar g x+tcty g (All b) = do+ (x, ty') <- unbind b+ tcty (extendTy x g) ty'+tcty g (Arr ty1 ty2) = do+ tcty g ty1+ tcty g ty2+tcty g TyInt = return ()+tcty g (TyProd tys) = do+ _ <- mapM (tcty g) tys+ return ()++typecheck :: Ctx -> Tm -> M Tm+typecheck g e@(TmVar x) = do + ty <- lookupTmVar g x+ return $ Ann e ty+typecheck g (Fix bnd) = do+ ((f, x, Embed (ty1, ty2)), e1) <- unbind bnd+ tcty g ty1+ tcty g ty2+ ae1@(Ann _ ty2') <- typecheck (extendTm f (Arr ty1 ty2) (extendTm x ty1 g)) e1+ if not (ty2 `aeq` ty2')+ then throwE $ "Type Error: Can't match " ++ pp ty2 ++ " and " ++ pp ty2'+ else return $ Ann + (Fix (bind (f,x, Embed (ty1, ty2)) ae1))+ (Arr ty1 ty2)+typecheck g e@(App e1 e2) = do+ ae1@(Ann _ ty1) <- typecheck g e1+ ae2@(Ann _ ty2) <- typecheck g e2+ case ty1 of+ Arr ty11 ty21 | ty2 `aeq` ty11 ->+ return (Ann (App ae1 ae2) ty21)+ _ -> throwE "TypeError"+typecheck g (TLam bnd) = do+ (x, e) <- unbind bnd+ ae@(Ann _ ty) <- typecheck (extendTy x g) e+ return $ Ann (TLam (bind x ae)) (All (bind x ty))+typecheck g (TApp e ty) = do+ ae@(Ann _ tyt) <- typecheck g e+ case tyt of+ (All b) -> do+ tcty g ty+ (n1, ty1) <- unbind b+ return $ Ann (TApp ae ty) (subst n1 ty ty1)+typecheck g (TmProd es) = do + atys <- mapM (typecheck g) es+ let tys = map (\(Ann _ ty) -> ty) atys+ return $ Ann (TmProd atys) (TyProd tys)+typecheck g (TmPrj e i) = do+ ae@(Ann _ ty) <- typecheck g e+ case ty of + TyProd tys | i < length tys -> return $ Ann (TmPrj ae i) (tys !! i)+ _ -> throwE "TypeError"+typecheck g (TmInt i) = return (Ann (TmInt i) TyInt)+typecheck g (TmPrim e1 p e2) = do+ ae1@(Ann _ ty1) <- typecheck g e1+ ae2@(Ann _ ty2) <- typecheck g e2 + case (ty1 , ty2) of + (TyInt, TyInt) -> return (Ann (TmPrim ae1 p ae2) TyInt)+ _ -> throwE "TypeError"+typecheck g (TmIf0 e0 e1 e2) = do+ ae0@(Ann _ ty0) <- typecheck g e0+ ae1@(Ann _ ty1) <- typecheck g e1+ ae2@(Ann _ ty2) <- typecheck g e2+ if ty1 `aeq` ty2 && ty0 `aeq` TyInt then + return (Ann (TmIf0 ae0 ae1 ae2) ty1)+ else + throwE "TypeError"++-----------------------------------------------------------------+-- Small-step semantics+-----------------------------------------------------------------++value :: Tm -> Bool+value (TmInt _) = True+value (Fix _) = True+value (TmProd es) = all value es+value (TLam _) = True+value _ = False++steps :: [Tm] -> M [Tm]+steps [] = throwE "can't step empty list"+steps (e:es) | value e = do+ es' <- steps es+ return (e : es')+steps (e:es) = do + e' <- step e+ return (e' : es)+ +step :: Tm -> M Tm+step e | value e = throwE "can't step value"+step (TmVar _) = throwE "unbound variable" +step (App e1@(Fix bnd) e2) = + if value e2 + then do+ ((f, x, _), t) <- unbind bnd+ return $ substs [ (x, e2), (f,e1) ] t+ else do + e2' <- step e2+ return (App e1 e2') +step (App e1 e2) = do+ e1' <- step e1+ return (App e1' e2)+step (TmPrj e1@(TmProd es) i) | value e1 && i < length es = return $ es !! i+step (TmPrj e1 i) = do + e1' <- step e1+ return (TmPrj e1' i) +step (TmProd es) = do+ es' <- steps es+ return (TmProd es')+step (TmPrim (TmInt i1) p (TmInt i2)) = + return (TmInt ((evalPrim p) i1 i2))+step (TmPrim e1 p e2) | value e1 = do+ e2' <- step e2+ return (TmPrim e1 p e2')+ | otherwise = do+ e1' <- step e1+ return (TmPrim e1' p e2)+step (TmIf0 (TmInt i) e1 e2) = if i==0 then return e1 else return e2+step (TmIf0 e0 e1 e2) = do + e0' <- step e0+ return (TmIf0 e0' e1 e2)+step (TApp (TLam bnd) ty) = do+ (a, e) <- unbind bnd+ return $ subst a ty e+step (TApp e ty) = do+ e' <- step e + return $ TApp e' ty+step (Ann e ty) = return e+ +evaluate :: Tm -> M Tm+evaluate e = if value e then return e else do+ e' <- step e+ evaluate e'+ +-----------------------------------------------------------------+-- Pretty-printer+-----------------------------------------------------------------++instance Display Ty where+ display (TyVar n) = display n+ display (TyInt) = return $ text "Int"+ display (Arr ty1 ty2) = do + d1 <- withPrec (precedence "->" + 1) $ display ty1+ d2 <- withPrec (precedence "->") $ display ty2+ binop d1 "->" d2+ display (All bnd) = lunbind bnd $ \ (a,ty) -> do+ da <- display a+ dt <- display ty+ prefix "forall" (da <> text "." <+> dt)+ display (TyProd tys) = displayTuple tys+ +instance Display Tm where+ display (TmInt i) = return $ int i+ display (TmVar n) = display n+ display (Fix bnd) = lunbind bnd $ \((f,x,Embed (ty1,ty2)), e) -> do+ df <- display f + dx <- display x + d1 <- display ty1 + d2 <- display ty2+ de <- withPrec (precedence "fix") $ display e+ let arg = parens (dx <> colon <> d1)+ --if f `elem` (fv e :: [F.TmName])+ -- then + prefix "fix" (df <+> arg <> colon <> d2 <> text "." <+> de)+ -- else prefix "\\" (arg <> text "." <+> de)+ display (App e1 e2) = do+ d1 <- withPrec (precedence " ") $ display e1+ d2 <- withPrec (precedence " " + 1) $ display e2+ binop d1 " " d2+ display (TmProd es) = displayTuple es++ display (TmPrj e i) = do+ de <- display e + return $ text "Pi" <> int i <+> de+ display (TmPrim e1 p e2) = do + let str = show p+ d1 <- withPrec (precedence str) $ display e1 + d2 <- withPrec (precedence str + 1) $ display e2 + binop d1 str d2+ display (TmIf0 e0 e1 e2) = do+ d0 <- display e0+ d1 <- display e1+ d2 <- display e2+ prefix "if0" $ sep [d0 , text "then" <+> d1 , text "else" <+> d2]+ display (TLam bnd) = lunbind bnd $ \(a,e) -> do+ da <- display a+ de <- withPrec (precedence "/\\") $ display e+ prefix "/\\" (da <> text "." <+> de)+ display (TApp e ty) = do+ d1 <- withPrec (precedence " ") $ display e+ d2 <- withPrec (precedence " " + 1) $ display ty+ binop d1 " " d2+ display (Ann e ty) = display e
+ src/K.hs view
@@ -0,0 +1,329 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ GADTs #-}++module K where++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)++import Control.Monad+import Control.Monad.Trans.Except+import qualified Data.List as List++import Util+import Text.PrettyPrint as PP++++-- System K++type TyName = Name Ty+type ValName = Name Val++data Ty = TyVar TyName+ | TyInt+ | All (Bind [TyName] [Ty])+ | TyProd [Ty]+ deriving Show++data Val = TmInt Int+ | TmVar ValName+ | Fix (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm))+ | TmProd [AnnVal]+ deriving Show + +data AnnVal = Ann Val Ty+ deriving Show+ +data Decl = + DeclVar ValName (Embed AnnVal)+ | DeclPrj Int ValName (Embed AnnVal)+ | DeclPrim ValName (Embed (AnnVal, Prim, AnnVal))+ deriving Show+ +data Tm = Let (Bind Decl Tm)+ | App AnnVal [Ty] [AnnVal]+ | TmIf0 AnnVal Tm Tm+ | Halt Ty AnnVal + deriving Show++$(derive [''Ty, ''Val, ''AnnVal, ''Decl, ''Tm])++------------------------------------------------------+instance Alpha Ty +instance Alpha Val +instance Alpha AnnVal+instance Alpha Decl+instance Alpha Tm++instance Subst Ty Ty where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+instance Subst Ty Prim+instance Subst Ty Tm+instance Subst Ty AnnVal+instance Subst Ty Decl+instance Subst Ty Val+++instance Subst Val Prim+instance Subst Val Ty+instance Subst Val AnnVal+instance Subst Val Decl+instance Subst Val Tm+instance Subst Val Val where+ isvar (TmVar x) = Just (SubstName x)+ isvar _ = Nothing+ +------------------------------------------------------+-- Example terms+------------------------------------------------------++x :: Name Tm+y :: Name Tm+z :: Name Tm+(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")++a :: Name Ty+b :: Name Ty+c :: Name Ty+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (ValName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+ if List.elem v (getDelta g) then+ return ()+ else+ throwE $ "NotFound " ++ (show v)++lookupTmVar :: Ctx -> ValName -> M Ty+lookupTmVar g v = do+ case lookup v (getGamma g) of+ Just s -> return s+ Nothing -> throwE $ "NotFound " ++ (show v)++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta = n : (getDelta ctx) }++extendTys :: [TyName] -> Ctx -> Ctx+extendTys ns ctx = foldr extendTy ctx ns++extendTm :: ValName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++extendTms :: [ValName] -> [Ty] -> Ctx -> Ctx+extendTms [] [] ctx = ctx+extendTms (n:ns) (ty:tys) ctx = extendTm n ty (extendTms ns tys ctx)++tcty :: Ctx -> Ty -> M ()+tcty g (TyVar x) =+ checkTyVar g x+tcty g (All b) = do+ (xs, tys) <- unbind b+ let g' = extendTys xs g+ mapM_ (tcty g') tys+tcty g TyInt = return ()+tcty g (TyProd tys) = do+ mapM_ (tcty g) tys++++typecheckVal :: Ctx -> Val -> M Ty+typecheckVal g (TmVar x) = lookupTmVar g x+typecheckVal g (Fix bnd) = do+ ((f, as), bnd2) <- unbind bnd+ (xtys, e) <- unbind bnd2+ let g' = extendTys as g+ let (xs,tys) = unzip $ map (\(x,Embed y) -> (x,y)) xtys + mapM_ (tcty g') tys+ let fty = All (bind as tys)+ typecheck (extendTm f fty (extendTms xs tys g')) e+ return fty+typecheckVal g (TmProd es) = do + tys <- mapM (typecheckAnnVal g) es+ return $ TyProd tys+typecheckVal g (TmInt i) = return TyInt+ +typecheckAnnVal g (Ann v ty) = do + tcty g ty+ ty' <- typecheckVal g v + if (ty `aeq` ty') + then return ty+ else throwE "wrong anntation"++typecheckDecl g (DeclVar x (Embed av)) = do+ ty <- typecheckAnnVal g av+ return $ extendTm x ty g+typecheckDecl g (DeclPrj i x (Embed av)) = do+ ty <- typecheckAnnVal g av+ case ty of + TyProd tys | i < length tys -> + return $ extendTm x (tys !! i) g+ _ -> throwE "cannot project"+typecheckDecl g (DeclPrim x (Embed (av1, _, av2))) = do+ ty1 <- typecheckAnnVal g av1+ ty2 <- typecheckAnnVal g av2+ case (ty1 , ty2) of + (TyInt, TyInt) -> return $ extendTm x TyInt g+ _ -> throwE "TypeError"++typecheck :: Ctx -> Tm -> M ()+typecheck g (Let bnd) = do+ (d,e) <- unbind bnd+ g' <- typecheckDecl g d+ typecheck g' e+typecheck g (App av tys es) = do+ ty <- typecheckAnnVal g av+ mapM_ (tcty g) tys+ case ty of+ (All bnd) -> do+ (as, argtys) <- unbind bnd+ let tys' = map (substs (zip as tys)) argtys+ argtys' <- mapM (typecheckAnnVal g) es+ if (length argtys /= length argtys') then throwE "incorrect args"+ else if (not (all id (zipWith aeq argtys argtys'))) then + throwE "arg mismatch"+ else return ()+typecheck g (TmIf0 av e1 e2) = do+ ty0 <- typecheckAnnVal g av+ typecheck g e1+ typecheck g e2+ if ty0 `aeq` TyInt then + return ()+ else + throwE "TypeError"+typecheck g (Halt ty av) = do+ ty' <- typecheckAnnVal g av+ if (not (ty `aeq` ty'))+ then throwE "type error"+ else return ()+++-----------------------------------------------------------------+-- Small-step semantics+-----------------------------------------------------------------+ +mkSubst :: Decl -> M (Tm -> Tm)+mkSubst (DeclVar x (Embed (Ann v _))) = return $ subst x v+mkSubst (DeclPrj i x (Embed (Ann (TmProd avs) _))) | i < length avs =+ let Ann vi _ = avs !! i in return $ subst x vi+mkSubst (DeclPrim x (Embed (Ann (TmInt i1) _, p, Ann (TmInt i2) _))) = + let v = TmInt (evalPrim p i1 i2) in+ return $ subst x v+mkSubst _ = throwE "invalid decl"++++step :: Tm -> M Tm++step (Let bnd) = do+ (d, e) <- unbind bnd+ ss <- mkSubst d+ return $ ss e+ +step (App (Ann e1@(Fix bnd) _) tys avs) = do+ ((f, as), bnd2) <- unbind bnd+ (xtys, e) <- unbind bnd2+ let us = map (\(Ann u _) -> u) avs+ let xs = map fst xtys+ return $ substs ((f,e1):(zip xs us)) (substs (zip as tys) e)++step (TmIf0 (Ann (TmInt i) _) e1 e2) = if i==0 then return e1 else return e2++step _ = throwE "cannot step"+ +evaluate :: Tm -> M Val+evaluate (Halt _ (Ann v _)) = return v+evaluate e = do+ e' <- step e+ evaluate e'+ +-----------------------------------------------------------------+-- Pretty-printer+-----------------------------------------------------------------++instance Display Ty where+ display (TyVar n) = display n+ display (TyInt) = return $ text "Int"+ display (All bnd) = lunbind bnd $ \ (as,tys) -> do+ da <- displayList as+ dt <- displayList tys+ if null as + then return $ parens dt <+> text "-> void"+ else prefix "forall" (brackets da <> text "." <+> parens dt <+> text "-> void")+ display (TyProd tys) = displayTuple tys+ +instance Display (ValName,Embed Ty) where + display (n, Embed ty) = do+ dn <- display n+ dt <- display ty+ return $ dn <> colon <> dt+ +instance Display Val where + display (TmInt i) = return $ int i+ display (TmVar n) = display n+ display (Fix bnd) = lunbind bnd $ \((f, as), bnd2) -> lunbind bnd2 $ \(xtys, e) -> do+ df <- display f + ds <- displayList as + dargs <- displayList xtys+ de <- withPrec (precedence "fix") $ display e+ let tyArgs = if null as then empty else brackets ds+ let tmArgs = if null xtys then empty else parens dargs+ if f `elem` (fv e :: [K.ValName])+ then prefix "fix" (df <+> tyArgs <> tmArgs <> text "." $$ de)+ else prefix "\\" (tyArgs <> tmArgs <> text "." $$ de)+ + display (TmProd es) = displayTuple es++instance Display AnnVal where+ display (Ann av _) = display av ++instance Display Tm where+ display (App av tys args) = do+ da <- display av+ dtys <- displayList tys+ dargs <- displayList args+ let tyArgs = if null tys then empty else brackets dtys+ let tmArgs = if null args then empty else parens dargs+ return $ da <> tyArgs <+> tmArgs+ display (Halt ty v) = do + dv <- display v+ return $ text "halt" <+> dv+ display (Let bnd) = lunbind bnd $ \(d, e) -> do+ dd <- display d+ de <- display e+ return $ (text "let" <+> dd <+> text "in" $$ de)+ display (TmIf0 e0 e1 e2) = do+ d0 <- display e0+ d1 <- display e1+ d2 <- display e2+ prefix "if0" $ parens $ sep [d0 <> comma , d1 <> comma, d2]++instance Display Decl where+ display (DeclVar x (Embed av)) = do+ dx <- display x+ dv <- display av+ return $ dx <+> text "=" <+> dv+ display (DeclPrj i x (Embed av)) = do+ dx <- display x+ dv <- display av+ return $ dx <+> text "=" <+> text "pi" <> int i <+> dv+ display (DeclPrim x (Embed (e1, p, e2))) = do+ dx <- display x+ let str = show p+ d1 <- display e1 + d2 <- display e2 + return $ dx <+> text "=" <+> d1 <+> text str <+> d2
+ src/TAL.hs view
@@ -0,0 +1,690 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ TupleSections,+ GeneralizedNewtypeDeriving,+ GADTs #-}++module TAL where++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)++import Unbound.LocallyNameless.Alpha+import Unbound.LocallyNameless.Types++import Control.Monad+import Control.Monad.Except+import Control.Monad.Reader+++import Data.Monoid (Monoid(..))++import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+++import Util+import Text.PrettyPrint as PP++-- Typed Assembly Language++type TyName = Name Ty++data Ty = TyVar TyName+ | TyInt+ | All (Bind [TyName] Gamma)+ | TyProd [(Ty, Flag)] + | Exists (Bind TyName Ty) + deriving Show++data Flag = Un | Init+ deriving (Eq, Ord, Show)++-- Heap types+type Psi = Map Label Ty ++-- Register file types+type Gamma = [(Register, Ty)]++newtype Register = Register String deriving (Eq, Ord)+instance Show Register where+ show (Register s) = s+ +-- designated result register+reg1 :: Register+reg1 = Register "r1"++-- temporary register names+rtmp :: Int -> Register+rtmp i = Register ("rt" ++ show i)++instance Enum Register where+ toEnum i = Register ("r" ++ show i)+ fromEnum (Register ('r' : str)) = read str++newtype Label = Label (Name Heap) deriving (Eq, Ord)+instance Show Label where+ show (Label n) = show n++data TyApp a = TyApp a Ty deriving Show++sapps :: SmallVal -> [Ty] -> SmallVal +sapps a tys = foldr (\ ty a -> SApp (TyApp a ty)) a tys++data Pack a = Pack Ty a Ty deriving Show++data WordVal = LabelVal Label+ | TmInt Int+ | Junk Ty + | WApp (TyApp WordVal)+ | WPack (Pack WordVal)+ deriving Show++data SmallVal = RegVal Register + | WordVal WordVal + | SApp (TyApp SmallVal) + | SPack (Pack SmallVal)+ deriving Show+ +data HeapVal = + Tuple [WordVal] + | Code [TyName] Gamma InstrSeq -- nominal binding+ deriving Show++type Heap = Map Label HeapVal+type RegisterFile = Map Register WordVal+ +data Instruction = + Add Register Register SmallVal+ | Bnz Register SmallVal+ | Ld Register Register Int+ | Malloc Register [Ty]+ | Mov Register SmallVal + | Mul Register Register SmallVal + | St Register Int Register + | Sub Register Register SmallVal + | Unpack TyName Register SmallVal -- binds type variable+ deriving Show+ +data InstrSeq = + Seq Instruction InstrSeq -- annoying to do bind here, skipping+ | Jump SmallVal+ | Halt Ty + deriving Show++--instance Monoid A.Heap where+-- mempty = A.Heap Map.empty+-- mappend (A.Heap h1) (A.Heap h2) = A.Heap (Map.union h1 h2)++type Machine = (Heap, RegisterFile, InstrSeq)++$(derive [''Ty, ''Flag, ''Register, ''Label, ''TyApp, ''Pack, + ''WordVal, ''SmallVal, ''HeapVal, ''Instruction, + ''InstrSeq])++------------------------------------------------------+instance Alpha Flag+instance Alpha Ty +instance Alpha Register +instance Alpha Label+instance Alpha a => Alpha (TyApp a)+instance Alpha a => Alpha (Pack a)+instance Alpha WordVal+instance Alpha SmallVal+instance Alpha HeapVal+instance Alpha Instruction+instance Alpha InstrSeq++-- need to replace this with a better instance+instance Alpha b => Alpha (Map Register b)++instance Subst Ty Ty where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+instance Subst Ty Flag+instance (Subst Ty a) => Subst Ty (TyApp a)+instance (Subst Ty a) => Subst Ty (Pack a)+instance Subst Ty WordVal+instance Subst Ty SmallVal+instance Subst Ty HeapVal+instance Subst Ty Instruction+instance Subst Ty InstrSeq+instance Subst Ty Label+instance Subst Ty Register+instance (Rep a, Subst Ty b) => Subst Ty (Map a b) ++freshForHeap :: Heap -> Label+freshForHeap h = Label (makeName str (i+1)) where+ Label nm = maximum (Map.keys h)+ (str, i) = (name2String nm, name2Integer nm)++-----------------------------------------------------+-- operational semantics+-----------------------------------------------------++getIntReg :: RegisterFile -> Register -> M Int+getIntReg r rs = + case Map.lookup rs r of+ Just (TmInt i) -> return i+ Just _ -> throwError "register not an int"+ Nothing -> throwError "register not found"++arith :: (Int -> Int -> Int) -> RegisterFile ->+ Register -> SmallVal -> M WordVal+arith op r rs v = do+ i <- getIntReg r rs+ (wv,_) <- loadReg r v + case wv of + TmInt j -> return (TmInt (i `op` j))+ _ -> throwError + $ "arith: word val " ++ pp wv ++" is not an int"++-- R^(sv)+loadReg :: RegisterFile -> SmallVal -> M (WordVal, [Ty])+loadReg r (RegVal rs) = case Map.lookup rs r of+ Just w -> return (w, [])+ Nothing -> throwError "register val not found"+loadReg r (WordVal w) = return (w, [])+loadReg r (SApp (TyApp sv ty)) = do + (w, tys) <- loadReg r sv+ return (w, ty:tys)+loadReg r (SPack (Pack t1 sv t2)) = do + (w, tys) <- loadReg r sv + return (WPack (Pack t1 (tyApp w tys) t2), [])+ +tyApp :: WordVal -> [Ty] -> WordVal +tyApp w [] = w+tyApp w (ty:tys) = tyApp (WApp (TyApp w ty)) tys+ +jmpReg :: Heap -> RegisterFile -> SmallVal -> M Machine+jmpReg h r v = do+ (w,tys) <- loadReg r v + case w of + LabelVal l ->+ case (Map.lookup l h) of+ Just (Code alphas gamma instrs') -> do+ when (length alphas /= length tys) $+ throwError "Bnz: wrong # type args"+ return (h, r, substs (zip alphas tys) instrs')+ _ -> throwError "Bnz: cannot jump, not code" + _ -> throwError "Bnz: cannot jump, not label"+ +step :: Machine -> M Machine+step (h, r, Add rd rs v `Seq` instrs) = do+ v' <- arith (+) r rs v + return (h, Map.insert rd v' r, instrs)++step (h, r, Mul rd rs v `Seq` instrs) = do+ v' <- arith (*) r rs v + return (h, Map.insert rd v' r, instrs)+step (h, r, Sub rd rs v `Seq` instrs) = do+ v' <- arith (-) r rs v + return (h, Map.insert rd v' r, instrs)+step (h, r, Bnz rs v `Seq` instrs) = do+ case Map.lookup rs r of + Just (TmInt 0) -> return (h, r, instrs)+ Just (TmInt _) -> jmpReg h r v+step (h, r, Jump v) = jmpReg h r v+step (h, r, Ld rd rs i `Seq` instrs) = do+ case Map.lookup rs r of + Just (LabelVal l) -> + case Map.lookup l h of + Just (Tuple ws) | i < length ws -> + return (h, Map.insert rd (ws !! i) r, instrs)+ _ -> throwError "ld: Cannot load location"+ _ -> throwError "ld: not label"+step (h, r, Malloc rd tys `Seq` instrs) = do+ let l = freshForHeap h+ return (Map.insert l (Tuple (map Junk tys)) h,+ Map.insert rd (LabelVal l) r, + instrs)+step (h, r, Mov rd v `Seq` instrs) = do + (w,tys) <- loadReg r v+ return (h, Map.insert rd (tyApp w tys) r, instrs)+step (h, r, St rd i rs `Seq` instrs) = do + case Map.lookup rs r of + Just w' ->+ case Map.lookup rd r of+ Just (LabelVal l) ->+ case Map.lookup l h of+ Just (Tuple ws) | i < length ws -> do+ let (ws0,(_:ws1)) = splitAt i ws+ return + (Map.insert l (Tuple (ws0 ++ (w':ws1))) h,+ r, instrs)+ _ -> throwError "heap label not found or wrong val"+ _ -> throwError "register not found or wrong val"+ _ -> throwError "register not found"+step (h, r, Unpack alpha rd v `Seq` instrs) = do+ (w0, tys) <- loadReg r v+ case tyApp w0 tys of + WPack (Pack ty w _) ->+ return (h, Map.insert rd w r, subst alpha ty instrs)+ _ -> throwError "not a pack"++run :: Machine -> M Machine+run m@(h, r, Halt t) = return m+run m = do + m' <- step m + run m'+ + +++------------------------------------------------------+-- Typechecker+------------------------------------------------------++type Delta = [ TyName ]++data Ctx = Ctx { getDelta :: Delta , + getGamma :: Gamma , + getPsi :: Psi }+emptyCtx = Ctx { getDelta = [], + getGamma = [], + getPsi = Map.empty }++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+ if List.elem v (getDelta g) then+ return ()+ else+ throwError $ "Type variable not found " ++ (show v)+++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta = n : (getDelta ctx) }++extendTys :: [TyName] -> Ctx -> Ctx+extendTys ns ctx = foldr extendTy ctx ns++insertGamma :: Register -> Ty -> Gamma -> Gamma+insertGamma r ty [] = [(r,ty)]+insertGamma r ty ((r',ty'):rest) | r < r' = (r',ty') : insertGamma r ty rest+insertGamma r ty ((r',ty'):rest) | r == r' = (r,ty) : rest++insertGamma r ty rest = (r,ty) : rest+++lookupHeapLabel :: Ctx -> Label -> M Ty+lookupHeapLabel ctx v = do+ case Map.lookup v (getPsi ctx) of+ Just s -> return s+ Nothing -> throwError $ "Label not found " ++ (show v)++lookupReg :: Ctx -> Register -> M Ty+lookupReg ctx v = do+ case lookup v (getGamma ctx) of+ Just s -> return s+ Nothing -> throwError $ "Register not found " ++ (show v)++-- tau is a well-formed type+tcty :: Ctx -> Ty -> M ()+tcty ctx (TyVar x) =+ checkTyVar ctx x+tcty ctx (All b) = do+ (xs, reg) <- unbind b+ let ctx' = extendTys xs ctx + tcGamma ctx' reg+tcty ctx TyInt = return ()+tcty ctx (TyProd tys) = do+ mapM_ (tcty ctx . fst) tys+tcty ctx (Exists b) = do + (a, ty) <- unbind b+ tcty (extendTy a ctx) ty++-- Psi is a well-formed heap type+-- Only uses D +tcPsi :: Ctx -> Psi -> M ()+tcPsi ctx psi = mapM_ (tcty ctx) (Map.elems psi)+ +-- Gamma is a well-formed register file+-- D |- G+tcGamma :: Ctx -> Gamma -> M ()+tcGamma ctx g = mapM_ (tcty ctx) (map snd g)++-- t1 is a subtype of t2+-- D |- t1 <= t2 +subtype :: Ctx -> Ty -> Ty -> M ()+subtype ctx (TyVar x) (TyVar y) | x == y = return ()+subtype ctx TyInt TyInt = return ()+subtype ctx (All bnd1) (All bnd2) = do+ Just (vs1, g1, vs2, g2) <- unbind2 bnd1 bnd2+ subGamma ctx g1 g2+subtype ctx (Exists bnd1) (Exists bnd2) = do+ Just (v1, t1, v2, t2) <- unbind2 bnd1 bnd2+ subtype ctx t1 t2+subtype ctx (TyProd tfs1) (TyProd tfs2) | (length tfs1 >= length tfs2) = do+ zipWithM_ (\ (t1, f1) (t2, f2) -> + if f2 == Un then return () + else subtype ctx t1 t2) tfs1 tfs2+subtype ctx t1 t2 = throwError $ "not a subtype:" ++ pp t1 ++ "\n" ++ pp t2 + +-- D |- G1 <= G2 +subGamma :: Ctx -> Gamma -> Gamma -> M ()+subGamma ctx g1 g2 = do+ mapM_ (\(r, t2) -> case lookup r g1 of + Just t1 -> subtype ctx t1 t1 + Nothing -> throwError $ + "subgamma -- register not found:" ++ show r ++ "\n" + ++ pp g1 ++ "\n" + ++ pp g2 ++ "\n") + g2+ +-- |- H : Psi +typeCheckHeap :: Heap -> Psi -> M ()+typeCheckHeap h psi = mapM_ tcHeapDecl (Map.assocs h) where+ ctx = emptyCtx { getPsi = psi } + + tcHeapDecl :: (Label, HeapVal) -> M ()+ tcHeapDecl (l,hv) = + case Map.lookup l psi of+ Just ty -> tcHeapVal hv ty+ Nothing -> throwError $ "heap type not found:" ++ show l+ + tcTuple (Junk ty', (ty,Un)) = + -- maybe we know these are the same already?+ subtype ctx ty' ty+ tcTuple (wv, (ty,Init)) = do+ ty' <- tcWordVal ctx wv + subtype ctx ty' ty + + tcHeapVal (Tuple wvs) (TyProd tys) | length wvs == length tys = do+ mapM_ tcTuple (zip wvs tys)+ + tcHeapVal (Code as g is) _ = do+ -- TODO: better error message. What if wrong # binders?+ -- let g' = patUnbind as bnd+ -- check (All bnd) ??+ let ctx = Ctx as g psi+ tcInstrSeq ctx is+ tcHeapVal _ _ = throwError $ "wrong type for heap val"++tcWordVal :: Ctx -> WordVal -> M Ty+tcWordVal ctx (LabelVal l) = lookupHeapLabel ctx l+tcWordVal ctx (TmInt i) = return TyInt+tcWordVal ctx (Junk ty') = throwError $ "BUG: no Junk here"+tcWordVal ctx (WApp tapp) = tcApp tcWordVal ctx tapp+tcWordVal ctx (WPack pack) = tcPack tcWordVal ctx pack++tcApp :: (Ctx -> a -> M Ty) -> Ctx -> TyApp a -> M Ty+tcApp f ctx (TyApp wv ty) = do+ tcty ctx ty+ ty' <- f ctx wv+ case ty' of + All bnd -> do + (as, bs) <- unbind bnd+ case as of + [] -> throwError "can't instantiate non-polymorphic function"+ (a:as') -> do+ let bs' = subst a ty bs+ return (All (bind as' bs'))++tcPack :: Display a => (Ctx -> a -> M Ty) -> Ctx -> Pack a -> M Ty +tcPack f ctx (Pack ty1 wv ty) = do+ case ty of + Exists bnd -> do + (a, ty2) <- unbind bnd+ tcty ctx ty1+ ty' <- f ctx wv+ --return ty+ + if (not (ty' `aeq` subst a ty1 ty2)) + then throwError $ "type error in pack " ++ pp wv ++ ":\n" + ++ pp ty' ++ "\n" + ++ " does not equal\n" + ++ pp (subst a ty1 ty2)+ else return ty + +tcSmallVal :: Ctx -> SmallVal -> M Ty +tcSmallVal ctx (RegVal r) = lookupReg ctx r +tcSmallVal ctx (WordVal wv) = tcWordVal ctx wv+tcSmallVal ctx (SApp app) = tcApp tcSmallVal ctx app+tcSmallVal ctx (SPack pack) = tcPack tcSmallVal ctx pack++tcInstrSeq :: Ctx -> InstrSeq -> M ()+tcInstrSeq ctx (Seq i is) = do + ctx' <- tcInstr ctx i+ tcInstrSeq ctx' is+tcInstrSeq ctx (Jump sv) = do+ ty <- tcSmallVal ctx sv+ case ty of + All bnd -> + let g = patUnbind [] bnd in+ subGamma ctx (getGamma ctx) g+tcInstrSeq ctx (Halt ty) = do+ ty' <- lookupReg ctx reg1 + subtype ctx ty ty' ++tcArith :: Ctx -> Register -> Register -> SmallVal -> M Ctx+tcArith ctx rd rs sv = do+ ty1 <- lookupReg ctx rs+ ty2 <- tcSmallVal ctx sv+ unless (ty1 `aeq` TyInt) $ throwError "source reg must be int" + unless (ty2 `aeq` TyInt) $ throwError "immediate must be int"+ let g' = insertGamma rd TyInt (getGamma ctx) + return (ctx { getGamma = g' })++tcInstr :: Ctx -> Instruction -> M Ctx+tcInstr ctx i = case i of+ (Add rd rs sv) -> tcArith ctx rd rs sv+ (Bnz r sv) -> do + ty1 <- lookupReg ctx r+ ty2 <- tcSmallVal ctx sv+ unless (ty1 `aeq` TyInt) $ throwError "source reg must be int" + case ty2 of+ All bnd -> do+ let g = patUnbind [] bnd + subGamma ctx (getGamma ctx) g+ return ctx + _ -> throwError "must bnz to code label"+ + (Ld rd rs i) -> do+ ty1 <- lookupReg ctx rs+ case ty1 of + TyProd tyfs -> do+ when (i >= length tyfs) $ throwError "Ld: index out of range"+ let (ty,f) = tyfs !! i+ unless (f == Init) $ throwError "Ld: load from unitialized field"+ let g = insertGamma rd ty (getGamma ctx)+ return $ ctx { getGamma = g } + _ -> throwError $ "Ld: not a tuple"+ + (Malloc rd tys) -> do + let ty = TyProd (map (,Un) tys)+ let g = insertGamma rd ty (getGamma ctx)+ return $ ctx { getGamma = g } + + (Mov rd sv) -> do+ ty <- tcSmallVal ctx sv+ let g = insertGamma rd ty (getGamma ctx)+ return $ ctx { getGamma = g } + + (Mul rd rs sv) -> tcArith ctx rd rs sv+ + (St rd i rs) -> do+ ty1 <- lookupReg ctx rd+ ty2 <- lookupReg ctx rs+ case ty1 of + TyProd tyfs -> do+ when (i >= length tyfs) $ throwError "St: index out of range"+ let (before, _:after) = List.splitAt i tyfs+ let ty = TyProd (before ++ [(ty2,Init)] ++ after)+ let g = insertGamma rd ty (getGamma ctx) + return $ ctx { getGamma = g }+ _ -> throwError $ "St: rd not a tuple"+ + (Sub rd rs sv) -> tcArith ctx rd rs sv+ + (Unpack a rd sv) -> do+ when (a `elem` getDelta ctx) $ throwError "Unpack: tyvar not fresh"+ ty1 <- tcSmallVal ctx sv+ case ty1 of + Exists bnd -> do+ let ty = patUnbind a bnd+ let g = insertGamma rd ty (getGamma ctx) + return $ ctx { getDelta = a : (getDelta ctx) }{ getGamma = g }++ +progcheck :: Machine -> M () +progcheck (heap, regfile, is) = do+ let getHeapTy (_,Tuple _ ) = throwError $ "only code to start"+ getHeapTy (l,Code as g _) = return $ (l,All (bind as g))+ psi_assocs <- mapM getHeapTy (Map.assocs heap)+ let psi = Map.fromList psi_assocs+ unless (Map.null regfile) $ throwError "must start with empty registers"+ let ctx = Ctx [] [] psi+ tcPsi ctx psi+ tcInstrSeq ctx is++-----------------------------------------------------------------+-- Pretty-printer+-----------------------------------------------------------------++instance Display Ty where+ display (TyVar n) = display n+ display (TyInt) = return $ text "Int"+ display (All bnd) = lunbind bnd $ \ (as,g) -> do+ da <- displayList as+ dt <- display g+ if null as + then return dt + else prefix "forall" (brackets da <> text "." <+> dt)+ display (TyProd tys) = displayTuple tys+ display (Exists bnd) = lunbind bnd $ \ (a,ty) -> do+ da <- display a + dt <- display ty+ prefix "exists" (da <> text "." <+> dt)+ +instance Display (Ty, Flag) where + display (ty, fl) = do+ dty <- display ty+ let f = case fl of { Un -> "0" ; Init -> "1" }+ return $ dty <> text "^" <> text f+ +instance Display a => Display (Map Register a) where+ display m = do+ fcns <- mapM (\(r,v) -> do + dv <- display v+ return (r, dv)) (Map.toList m)+ return $ braces (sep (punctuate comma + [ text (show n) + <+> text ":" <+> dv | (n,dv) <- fcns ]))+ +instance Display a => Display [(Register, a)] where+ display m = do+ fcns <- mapM (\(r,v) -> do + dv <- display v+ return (r, dv)) m+ return $ braces (sep (punctuate comma + [ text (show n) + <+> text ":" <+> dv | (n,dv) <- fcns ])) ++instance Display a => Display (Pack a) where+ display (Pack ty e _) = do + dty <- display ty+ de <- display e + prefix "pack" (brackets (dty <> comma <> de))++instance Display a => Display (TyApp a) where+ display (TyApp av ty) = do+ dv <- display av+ dt <- display ty+ return $ dv <+> (brackets dt)++instance Display WordVal where + display (LabelVal l) = return $ text ( show l)+ display (TmInt i) = return $ int i+ display (Junk ty) = return $ text "?"+ display (WPack p) = display p+ display (WApp a) = display a++instance Display SmallVal where + display (RegVal r) = return (text $ show r)+ display (WordVal n) = display n+ display (SPack p) = display p+ display (SApp a) = display a+++instance Display HeapVal where+ display (Code as gamma is) = do+ ds <- displayList as + dargs <- display gamma+ de <- display is+ let tyArgs = if null as then empty else brackets ds+ prefix "code" (tyArgs <> dargs <> text "." $$ de)+ + display (Tuple es) = displayTuple es++dispArith str rd rs sv = do+ dv <- display sv+ return $ text str <+> text (show rd) + <> comma <> text (show rs) <> comma <+> dv++instance Display Instruction where+ display i = case i of + Add rd rs sv -> dispArith "add" rd rs sv+ Bnz r sv -> do+ dv <- display sv+ return $ text "bnz" <+> text (show r) <> comma <> dv+ + (Ld rd rs i) -> + return $ text "ld" <+> text (show rd) <> comma <> text (show rs) + <> brackets (int i)+ + (Malloc rd tys) -> do + dtys <- displayList tys+ return $ text "malloc" <+> text (show rd) <> comma <> brackets dtys+ + (Mov rd sv) -> do+ dv <- display sv+ return $ text "mov" <+> text (show rd) <> comma <> dv+ + (Mul rd rs sv) -> dispArith "mul" rd rs sv+ + (St rd i rs) -> do+ return $ text "st" <+> text (show rd) <> brackets (int i) <> comma + <> text (show rs)+ + (Sub rd rs sv) -> dispArith "sub" rd rs sv+ + (Unpack a rd sv) -> do+ dv <- display sv+ return $ text "unpack" + <> brackets (text (show a) <> comma <> text (show rd))+ <> comma <> dv++instance Display InstrSeq where+ display (Seq i is) = do+ di <- display i + dis <- display is + return $ di $+$ dis+ display (Jump sv) = do + ds <- display sv+ return $ text "jmp" <+> ds+ display (Halt _) = do + return $ text "halt" +++instance Display Label where+ display l = return (text (show l))++instance Display a => Display (Map Label a) where+ display m = do+ fcns <- mapM (\(d,v) -> do + dn <- display d+ dv <- display v+ return (dn, dv)) (Map.toList m)+ return $ vcat [ n <+> text ":" $$ nest 4 dv | (n,dv) <- fcns ]+ ++instance Display (Heap, RegisterFile, InstrSeq) where+ display (h, r, is) = do+ dh <- display h+ dr <- display r+ di <- display is+ return $ dh $$ dr $$ text "main:" $$ nest 4 di
+ src/Translate.hs view
@@ -0,0 +1,738 @@+{-# LANGUAGE TupleSections #-}+{-# OPTIONS -fwarn-tabs -fno-warn-type-defaults -fno-warn-orphans #-}++module Translate where++import Unbound.LocallyNameless hiding (to)+++import Control.Monad.Except+import Control.Monad.Reader+import Control.Monad.State++import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+++import Util+import qualified F+import qualified K+import qualified C+import qualified A+import qualified TAL++------------------------------------+-- The compiler pipeline, all passes+------------------------------------++compile :: F.Tm -> M TAL.Machine+compile f = do+ af <- F.typecheck F.emptyCtx f+ k <- toProgK af+ K.typecheck K.emptyCtx k+ c <- toProgC k+ C.typecheck C.emptyCtx c+ h <- toProgH c+ C.hoistcheck h+ a <- toProgA h+ A.progcheck a+ tal <- toProgTAL a+ TAL.progcheck tal+ return tal++-------------------------------+-- Helper functions for testing+-------------------------------+test :: F.Tm -> IO ()+test f = printM $ do+ tal <- compile f+ (h, r, _) <- TAL.run tal+ case Map.lookup TAL.reg1 r of+ Just v -> return v+ Nothing -> throwError "no result!"++printM :: (Display a) => M a -> IO ()+printM x = putStrLn $ pp $ runM x++t1 = printM $ compile F.onePlusOne++t2 = printM $ compile F.two++t3 = printM $ compile F.ctrue++t4 = printM $ compile F.sixfact++t5 = printM $ compile F.twice++--------------------------------------------+-- F ==> K+--------------------------------------------++-- type translation++toTyK :: F.Ty -> M K.Ty+toTyK (F.TyVar n) = return $ K.TyVar (translate n)+toTyK F.TyInt = return $ K.TyInt+toTyK (F.Arr t1 t2) = do+ k1 <- toTyK t1+ k2 <- toTyContK t2+ return $ K.All (bind [] [k1,k2])+toTyK (F.All bnd) = do+ (a,ty) <- unbind bnd+ let a' = translate a+ ty' <- toTyContK ty+ return $ K.All (bind [a'][ty'])+toTyK (F.TyProd tys) = do+ tys' <- mapM toTyK tys+ return $ K.TyProd tys'++toTyContK :: F.Ty -> M K.Ty+toTyContK fty = do+ kty <- toTyK fty+ return $ K.All (bind [] [kty])++-- expression translation++-- Here we actually use Danvy & Filinski's "optimizing" closure-conversion+-- algorithm. It is actually no more complicated than the one presented in+-- the paper and produces output with no "administrative" redices.++toProgK :: F.Tm -> M K.Tm+toProgK ae@(F.Ann _ fty) = do+ kty <- toTyK fty+ toExpK ae (\kv -> return $ K.Halt kty kv)+toProgK _ = throwError "toProgK given unannotated expression!"++toExpK :: F.Tm -> (K.AnnVal -> M K.Tm) -> M K.Tm+toExpK (F.Ann ftm fty) k = to ftm where++ to (F.TmVar y) = do+ kty <- toTyK fty+ k (K.Ann (K.TmVar (translate y)) kty)++ to (F.TmInt i) = k (K.Ann (K.TmInt i) K.TyInt)++ to (F.Fix bnd) = do+ ((f, x, Embed (t1,t2)), e) <- unbind bnd+ kty1 <- toTyK t1+ kcty2 <- toTyContK t2+ kvar <- fresh (string2Name "k")+ ke <- toExpK e (\v -> return $ K.App (K.Ann (K.TmVar kvar) kcty2) [] [v])+ let kfix = K.Fix (bind (translate f, [])+ (bind [(translate x, Embed kty1),(kvar, Embed kcty2)]+ ke))+ k (K.Ann kfix (K.All (bind [] [kty1,kcty2])))++ to (F.App ae1 ae2) = do+ kty <- toTyK fty+ let body v1 v2 = do+ kv <- reifyCont k kty+ return (K.App v1 [] [v2, kv])+ toExpK ae1 (\v1 -> toExpK ae2 (\v2 -> body v1 v2))++ to (F.TmPrim ae1 p ae2) = do+ y <- fresh (string2Name "y")+ let body v1 v2 = do+ tm <- k (K.Ann (K.TmVar y) K.TyInt)+ return (K.Let (bind (K.DeclPrim y (Embed (v1,p, v2))) tm))+ toExpK ae1 (\ x1 -> toExpK ae2 (body x1))++ to (F.TmIf0 ae0 ae1 ae2) = do+ e1 <- toExpK ae1 k+ e2 <- toExpK ae2 k+ toExpK ae0 (\v1 -> return (K.TmIf0 v1 e1 e2))++ to (F.TmProd aes) = do+ kty <- toTyK fty+ let loop [] k = k []+ loop (ae:aes) k =+ toExpK ae (\v -> loop aes (\vs -> k (v:vs)))+ loop aes (\vs -> k (K.Ann (K.TmProd vs) kty))++ to (F.TmPrj ae i) = do+ y <- fresh (string2Name "y")+ yty <- toTyK fty+ toExpK ae (\ v1 -> do+ tm <- k (K.Ann (K.TmVar y) yty)+ return (K.Let (bind (K.DeclPrj i y (Embed v1)) tm)))++ to (F.TLam bnd) = do+ (a,e@(F.Ann _ ty)) <- unbind bnd+ kcty <- toTyContK ty+ kvar <- fresh (string2Name "k")+ ke <- toExpK e (\v -> return $ K.App (K.Ann (K.TmVar kvar) kcty) [] [v])+ f <- fresh (string2Name "f")+ let kfix = K.Fix (bind (f, [translate a])+ (bind [(kvar, Embed kcty)] ke))+ k (K.Ann kfix (K.All (bind [translate a] [kcty])))++ to (F.TApp ae ty) = do+ aty <- toTyK ty+ let body v1 = do+ kty <- toTyK fty+ kv <- reifyCont k kty+ return (K.App v1 [aty] [kv])+ toExpK ae body+++ to (F.Ann e ty) = throwError "found nested Ann"+toExpK _ _ = throwError "toExpK: found unannotated expression"+++-- Turn a meta continuation into an object language continuation+-- Requires knowing the type of the expected value.++reifyCont :: (K.AnnVal -> M K.Tm) -> K.Ty -> M K.AnnVal+reifyCont k vty = do+ kont <- fresh (string2Name "kont")+ v <- fresh (string2Name "v")+ body <- k (K.Ann (K.TmVar v) vty)+ return $ K.Ann (K.Fix (bind (kont, [])+ (bind [(v, Embed vty)] body)))+ (K.All (bind [][vty]))++--------------------------------------------+-- K to C Closure conversion+--------------------------------------------++-- NOTE: we need to keep track of the current context+-- so that we can find out the types of free variables+-- (The FV function only gives us free names, not free+-- annotated variables)+type N a = ReaderT C.Ctx M a++toTyC :: K.Ty -> N C.Ty+toTyC (K.TyVar v) = return $ C.TyVar (translate v)+toTyC K.TyInt = return $ C.TyInt+toTyC (K.All bnd) = do+ (as, tys) <- unbind bnd+ let as' = map translate as+ tys' <- local (C.extendTys as') $ mapM toTyC tys+ b' <- fresh (string2Name "b")+ let prod = C.TyProd [C.All (bind as' (C.TyVar b' : tys')), C.TyVar b']+ return $ (C.Exists (bind b' prod))+toTyC (K.TyProd tys) = do+ tys' <- mapM toTyC tys+ return $ C.TyProd tys'++toProgC :: K.Tm -> M C.Tm+toProgC k = runReaderT (toTmC k) C.emptyCtx++toTmC :: K.Tm -> N C.Tm+toTmC (K.Let bnd) = do+ (decl, tm) <- unbind bnd+ decl' <- toDeclC decl+ tm' <- local (C.extendDecl decl') (toTmC tm)+ return $ C.Let (bind decl' tm')+toTmC (K.App v@(K.Ann _ t) tys vs) = do+ z <- fresh $ string2Name "z"+ zcode <- fresh $ string2Name "zcode"+ zenv <- fresh $ string2Name "zenv"+ v' <- toAnnValC v+ t' <- toTyC t+ tys' <- mapM toTyC tys+ vs' <- mapM toAnnValC vs+ case t' of+ C.Exists bnd -> do+ (b, prodty) <- unbind bnd+ case prodty of+ C.TyProd [ tcode, C.TyVar b' ] | b == b' -> do+ let vz = C.Ann (C.TmVar z) prodty+ let ds = [C.DeclUnpack b z (Embed v'),+ C.DeclPrj 1 zenv (Embed vz),+ C.DeclPrj 0 zcode (Embed vz)]+ ann <- C.mkTyApp (C.Ann (C.TmVar zcode) tcode) tys'+ let prd = (C.Ann (C.TmVar zenv) (C.TyVar b)):vs'+ return $ foldr (\ b e -> C.Let (bind b e)) (C.App ann prd) ds+ _ -> throwError "type error"+ _ -> throwError "type error"+toTmC (K.TmIf0 v tm1 tm2) = do+ liftM3 C.TmIf0 (toAnnValC v) (toTmC tm1) (toTmC tm2)+toTmC (K.Halt ty v) =+ liftM2 C.Halt (toTyC ty) (toAnnValC v)++toDeclC :: K.Decl -> N C.Decl+toDeclC (K.DeclVar x (Embed v)) = do+ v' <- toAnnValC v+ return $ C.DeclVar (translate x) (Embed v')+toDeclC (K.DeclPrj i x (Embed v)) = do+ v' <- toAnnValC v+ return $ C.DeclPrj i (translate x) (Embed v')+toDeclC (K.DeclPrim x (Embed (v1, p, v2))) = do+ v1' <- toAnnValC v1+ v2' <- toAnnValC v2+ return $ C.DeclPrim (translate x) (Embed (v1',p, v2'))++toAnnValC :: K.AnnVal -> N C.AnnVal+toAnnValC (K.Ann (K.TmInt i) K.TyInt) =+ return $ C.Ann (C.TmInt i) C.TyInt+toAnnValC (K.Ann (K.TmVar v) ty) = do+ ty' <- toTyC ty+ return $ C.Ann (C.TmVar (translate v)) ty'+toAnnValC (K.Ann v@(K.Fix bnd1) t@(K.All _)) = do+ t' <- toTyC t+ ((f,as), bnd2) <- unbind bnd1+ (xtys, e) <- unbind bnd2+ let (xs,tys) = unzip $ map (\(x,Embed ty) -> (x,ty)) xtys+ let xs' = map translate xs+ tys' <- mapM toTyC tys+ let ys = (map translate (List.nub (fv v :: [K.ValName])))+ ctx <- ask+ ss' <- lift $ mapM (C.lookupTmVar ctx) ys+ let as' = map translate as+ let bs = (map translate (List.nub (fv v :: [K.TyName])))+ let tenv = C.TyProd ss'+ let trawcode = C.All (bind (bs ++ as') (tenv:tys'))+ zvar <- fresh $ string2Name "zfix"+ let zcode = C.Ann (C.TmVar zvar) trawcode+ zenvvar <- fresh $ string2Name "zfenv"+ let zenv = C.Ann (C.TmVar zenvvar) tenv+ tyAppZenv <- C.mkTyApp zcode (map C.TyVar bs)++ let mkprj (x, i) e =+ C.Let (bind (C.DeclPrj i x (Embed zenv)) e)+ let extend = \c -> foldr (uncurry C.extendTm) c (zip xs' tys')+ e' <- local (C.extendTm (translate f) t' . extend) $ toTmC e+ let vcode = C.Fix (bind (zvar, (bs ++ as'))+ (bind ((zenvvar, Embed tenv):+ zipWith (\x ty -> (x,Embed ty)) xs' tys')+ (C.Let (bind (C.DeclVar (translate f)+ (Embed (C.Ann (C.Pack tenv (C.mkProd [tyAppZenv, zenv]))+ t')))+ (foldr mkprj e' (zip ys [0..]))))))+ let venv = C.mkProd (zipWith (\y ty -> C.Ann (C.TmVar y) ty) ys ss')+ tyAppVcode <- (C.mkTyApp (C.Ann vcode trawcode) (map C.TyVar bs))+ return $+ C.Ann (C.Pack tenv (C.mkProd [tyAppVcode, venv])) t'++toAnnValC (K.Ann (K.TmProd vs) ty) = do+ ty' <- toTyC ty+ vs' <- mapM toAnnValC vs+ return $ C.Ann (C.TmProd vs') ty'+toAnnValC _ = throwError "toAnnValC: inconsistent annotation"++--------------------------------------------+-- C to H (actually C) Hoisting+--------------------------------------------++instance Monoid C.Heap where+ mempty = C.Heap Map.empty+ mappend (C.Heap h1) (C.Heap h2) = C.Heap (Map.union h1 h2)++-- we keep track of the current heap as we hoist+-- 'fix' expressions out of expressions+type H a = StateT C.Heap M a++toProgH :: C.Tm -> M (C.Tm, C.Heap)+toProgH tm = runStateT (toTmH tm) mempty++toTmH :: C.Tm -> H C.Tm+toTmH (C.Let bnd) = do+ (decl, tm) <- unbind bnd+ decl' <- toDeclH decl+ tm' <- toTmH tm+ return $ C.Let (bind decl' tm')+toTmH (C.App v vs) = do+ v' <- toAnnValH v+ vs' <- mapM toAnnValH vs+ return $ C.App v' vs'+toTmH (C.TmIf0 v tm1 tm2) = do+ liftM3 C.TmIf0 (toAnnValH v) (toTmH tm1) (toTmH tm2)+toTmH (C.Halt ty v) =+ liftM (C.Halt ty) (toAnnValH v)++toDeclH :: C.Decl -> H C.Decl+toDeclH (C.DeclVar x (Embed v)) = do+ v' <- toAnnValH v+ return $ C.DeclVar x (Embed v')+toDeclH (C.DeclPrj i x (Embed v)) = do+ v' <- toAnnValH v+ return $ C.DeclPrj i x (Embed v')+toDeclH (C.DeclPrim x (Embed (v1, p, v2))) = do+ v1' <- toAnnValH v1+ v2' <- toAnnValH v2+ return $ C.DeclPrim x (Embed (v1',p, v2'))+toDeclH (C.DeclUnpack g x (Embed v)) = do+ v' <- toAnnValH v+ return $ C.DeclUnpack g x (Embed v')+++toAnnValH :: C.AnnVal -> H C.AnnVal+toAnnValH (C.Ann (C.TmInt i) _) =+ return $ C.Ann (C.TmInt i) C.TyInt+toAnnValH (C.Ann (C.TmVar v) ty) = do+ return $ C.Ann (C.TmVar v) ty+toAnnValH (C.Ann (C.Fix bnd1) ty) = do+ ((f, as),bnd2) <- unbind bnd1+ (xtys, tm) <- unbind bnd2+ codef <- fresh f+ tm' <- toTmH tm+ let v' = (C.Ann (C.Fix (bind (f,as) (bind xtys tm'))) ty)+ modify (\s -> mappend s (C.Heap (Map.singleton codef v')))+ return (C.Ann (C.TmVar codef) ty)++toAnnValH (C.Ann (C.TmProd ps) ty) = do+ ps' <- mapM toAnnValH ps+ return $ C.Ann (C.TmProd ps') ty+toAnnValH (C.Ann (C.TApp v ty1) ty) = do+ v' <- toAnnValH v+ return $ C.Ann (C.TApp v' ty1) ty+toAnnValH (C.Ann (C.Pack ty1 v) ty) = do+ v' <- toAnnValH v+ return $ C.Ann (C.Pack ty1 v') ty++--------------------------------------------+-- H to A (Allocation)+--------------------------------------------++toTyA :: C.Ty -> M A.Ty+toTyA (C.TyVar v) = return $ A.TyVar (translate v)+toTyA C.TyInt = return $ A.TyInt+toTyA (C.All bnd) = do+ (as, tys) <- unbind bnd+ let as' = map translate as+ tys' <- mapM toTyA tys+ return (A.All (bind as' tys'))+toTyA (C.TyProd tys) = do+ tys' <- mapM toTyA tys+ return $ A.TyProd $ map (,A.Init) tys'+toTyA (C.Exists bnd) = do+ (a, ty) <- unbind bnd+ let a' = translate a+ ty' <- toTyA ty+ return $ A.Exists (bind a' ty')++toProgA :: (C.Tm, C.Heap) -> M (A.Tm, A.Heap)+toProgA (tm, C.Heap heap) = do+ asc <- mapM (\(x,hv) -> let x' = translate x in+ liftM (x',) (toHeapValA x' hv))+ (Map.assocs heap)+ let heap' = A.Heap (Map.fromDistinctAscList asc)+ tm' <- toExpA tm+ return (tm', heap')++toHeapValA :: A.ValName -> C.AnnVal -> M (A.Ann A.HeapVal)+toHeapValA f' (C.Ann (C.Fix bnd) _) = do+ ((f,as), bnd2) <- unbind bnd+ (xtys, e) <- unbind bnd2+ let e' = swaps (single (AnyName f')(AnyName f)) e+ let (xs,tys) = unzip $ map (\(x,Embed y) -> (x,y)) xtys+ tys' <- mapM toTyA tys+ let as' = map translate as+ let xs' = map translate xs+ e'' <- toExpA e'+ return (A.Ann (A.Code (bind as' (bind xs' e''))) (A.All (bind as' tys')))+toHeapValA _ _ = throwError "only code in the heap"+++toExpA :: C.Tm -> M A.Tm+toExpA (C.Let bnd) = do+ (d, tm) <- unbind bnd+ ds' <- toDeclA d+ tm' <- toExpA tm+ return $ A.lets ds' tm'+toExpA (C.App av avs) = do+ (ds', av') <- toAnnValA av+ dsav <- mapM toAnnValA avs+ let (dss, avs') = unzip dsav+ return $ A.lets (ds' ++ concat dss) (A.App av' avs')+toExpA (C.TmIf0 av e1 e2) = do+ (ds', av') <- toAnnValA av+ e1' <- toExpA e1+ e2' <- toExpA e2+ return $ A.lets ds' (A.TmIf0 av' e1' e2')+toExpA (C.Halt ty av) = do+ ty' <- toTyA ty+ (ds', av') <- toAnnValA av+ return (A.lets ds' (A.Halt ty' av'))+++toDeclA :: C.Decl -> M [A.Decl]+toDeclA (C.DeclVar x (Embed av)) = do+ (ds', av') <- toAnnValA av+ return (ds' ++ [A.DeclVar (translate x) (Embed av')])+toDeclA (C.DeclPrj i x (Embed av)) = do+ (ds', av') <- toAnnValA av+ return (ds' ++ [A.DeclPrj i (translate x) (Embed av')])+toDeclA (C.DeclPrim x (Embed (av1,p,av2))) = do+ (ds1', av1') <- toAnnValA av1+ (ds2', av2') <- toAnnValA av2+ return (ds1' ++ ds1' ++ [A.DeclPrim (translate x)+ (Embed (av1', p, av2'))])++toDeclA (C.DeclUnpack a x (Embed av)) = do+ (ds', av') <- toAnnValA av+ return (ds' ++ [A.DeclUnpack (translate a) (translate x)+ (Embed av')])++-- create the type [ ty_0^1 ... ty_{i-1}^1 ty_i^0 ty_{i+1}^0 ...]+updateProd :: [A.Ty] -> Int -> [(A.Ty,A.Flag)]+updateProd tys i = [ (ty, if j < i then A.Init else A.Un) |+ (ty, j) <- zip tys [0..] ]++++toAnnValA :: C.AnnVal -> M ([A.Decl],A.Ann A.Val)+toAnnValA (C.Ann (C.TmProd vs) (C.TyProd tys)) = do+ dvs' <- mapM toAnnValA vs+ let (dss', vs') = unzip dvs'+ tys' <- mapM toTyA tys+ y <- fresh $ string2Name "ym"+ -- combine helper function for initialization+ -- y -- name of tuple to initialize+ -- -- typle type [ ty_0^1 ... ty_{i-1}^1 ty_i^0 ...]+ -- ds -- current list of declarations+ -- i -- index of the tuple to initialize+ -- avi -- value initialize y[i]+ let initialize tys' (yt, ds) (i,avi) = do+ y1 <- fresh $ string2Name "ya"+ let ay0 = A.Ann (A.TmVar yt) (A.TyProd (updateProd tys' i))+ return (y1, ds ++ [A.DeclAssign y1 (Embed (ay0, i, avi))])+ (yn, ds') <- foldM (initialize tys')+ (y, concat dss' ++ [A.DeclMalloc y (Embed tys')])+ (zip [0..] vs')+ return $ (ds', A.Ann (A.TmVar yn) (A.TyProd (map (,A.Init) tys')))+++toAnnValA (C.Ann v ty) = do+ (d,v') <- toValA v+ ty' <- toTyA ty+ return $ (d, A.Ann v' ty')++toValA :: C.Val -> M ([A.Decl],A.Val)+toValA (C.TmInt i) = return ([], (A.TmInt i))+toValA (C.TmVar v) = return ([], A.TmVar (translate v))+toValA (C.TApp av ty) = do+ (ds', av') <- toAnnValA av+ ty' <- toTyA ty+ return $ (ds', A.TApp av' ty')+toValA (C.Pack ty av) = do+ ty' <- toTyA ty+ (ds', av') <- toAnnValA av+ return (ds', A.Pack ty' av')+toValA (C.Fix _) = throwError "no fix after hoist"+toValA (C.TmProd _) = throwError "catch in Annval"++--------------------------------------------+-- A to TAL (Code Generation)+--------------------------------------------++toFlag :: A.Flag -> TAL.Flag+toFlag A.Init = TAL.Init+toFlag A.Un = TAL.Un++toTyTAL :: A.Ty -> M TAL.Ty+toTyTAL (A.TyVar v) = return $ TAL.TyVar (translate v)+toTyTAL A.TyInt = return $ TAL.TyInt+toTyTAL (A.All bnd) = do+ (as, tys) <- unbind bnd+ let as' = map translate as+ tys' <- mapM toTyTAL tys+ let gamma = (zip [TAL.reg1 ..] tys')+ return (TAL.All (bind as' gamma))+toTyTAL (A.TyProd tys) = do+ tys' <- mapM (\(ty,f) -> liftM (,toFlag f) (toTyTAL ty)) tys+ return $ TAL.TyProd $ tys'+toTyTAL (A.Exists bnd) = do+ (a, ty) <- unbind bnd+ let a' = translate a+ ty' <- toTyTAL ty+ let ty2 = TAL.Exists $ bind a' ty'+ return $ TAL.Exists (bind a' ty')++-- Keep track of the mapping between variables and registers+-- or heap locations+type Varmap = Map A.ValName TAL.SmallVal++-- Create a register corresponding to a particular+-- value variable+var2reg :: A.ValName -> M (TAL.Register, Varmap)+var2reg x = let rd = TAL.Register ("r" ++ (name2String x) ++ show (name2Integer x)) in+ return $ (rd,Map.singleton x (TAL.RegVal rd))+++toSmallVal :: Varmap -> A.Ann A.Val -> M (TAL.SmallVal, TAL.Ty)+toSmallVal vm (A.Ann (A.TmInt i) _) =+ return (TAL.WordVal (TAL.TmInt i), TAL.TyInt)+toSmallVal vm (A.Ann (A.TmVar x) ty) = do+ ty' <- toTyTAL ty+ case Map.lookup x vm of+ Just sv -> return (sv, ty')+ Nothing -> throwError $ show x ++ " not found"+toSmallVal vm (A.Ann (A.TApp av ty) ty1) = do+ ty1' <- toTyTAL ty1+ ty' <- toTyTAL ty+ (sv',_) <- toSmallVal vm av+ return $ (TAL.SApp (TAL.TyApp sv' ty'), ty1')+toSmallVal vm (A.Ann (A.Pack ty1 av) ty2) = do+ ty1' <- toTyTAL ty1+ (av', _) <- toSmallVal vm av+ ty2' <- toTyTAL ty2+ return $ (TAL.SPack (TAL.Pack ty1' av' ty2'), ty2')++toWordVal :: Varmap -> A.Ann A.Val -> M TAL.WordVal+toWordVal vm (A.Ann (A.TmInt i) _) = return $ TAL.TmInt i+toWordVal vm (A.Ann (A.TmVar x) _) = case Map.lookup x vm of+ Just (TAL.WordVal wv) -> return wv+ Just _ -> throwError "must be wordval"+ Nothing -> throwError "not found"+toWordVal vm (A.Ann (A.TApp av ty) _) = do+ ty' <- toTyTAL ty+ sv' <- toWordVal vm av+ return $ TAL.WApp (TAL.TyApp sv' ty')+toWordVal vm (A.Ann (A.Pack ty1 av) ty2) = do+ ty1' <- toTyTAL ty1+ av' <- toWordVal vm av+ ty2' <- toTyTAL ty2+ return $ TAL.WPack (TAL.Pack ty1' av' ty2')+++toInstrsTAL :: Varmap -> TAL.Delta -> TAL.Gamma -> A.Tm+ -> M (TAL.Heap, TAL.InstrSeq)+toInstrsTAL vm delta gamma (A.Let bnd) = do+ (decl, tm) <- unbind bnd+ (vm', delta', gamma', is) <- toDeclTAL vm delta gamma decl+ (heap, is') <- toInstrsTAL vm' delta' gamma' tm+ return (heap, foldr TAL.Seq is' is)+toInstrsTAL vm delta gamma (A.App av args) = do+ (sv, _) <- toSmallVal vm av+ (svs,_) <- liftM unzip $ mapM (toSmallVal vm) args+ let rtmps = map (\ (i,_) -> TAL.rtmp i) (zip [1 ..] svs)+ let movs1 = zipWith TAL.Mov rtmps svs+ let movs2 = zipWith TAL.Mov [TAL.reg1 ..]+ (map TAL.RegVal rtmps)+ return (Map.empty,+ foldr TAL.Seq+ (TAL.Jump (TAL.RegVal (TAL.rtmp 0)))+ ([TAL.Mov (TAL.rtmp 0) sv] ++ movs1 ++ movs2))++toInstrsTAL vm delta gamma (A.TmIf0 av e1 e2) = do+ (sv,_) <- toSmallVal vm av+ (h1,is1) <- toInstrsTAL vm delta gamma e1+ (h2,is2) <- toInstrsTAL vm delta gamma e2+ l <- liftM TAL.Label (fresh (string2Name "l"))+ let h = Map.singleton l (TAL.Code (map translate delta) gamma is2)+ return (Map.unions [h1,h2, h],+ (TAL.Mov (TAL.rtmp 0) sv) `TAL.Seq`+ (TAL.Bnz (TAL.rtmp 0)+ (TAL.sapps (TAL.WordVal (TAL.LabelVal l))+ (map TAL.TyVar delta)) `TAL.Seq`+ is1))++toInstrsTAL vm delta gamma (A.Halt ty av) = do+ (sv,_) <- toSmallVal vm av+ ty' <- toTyTAL ty+ return (Map.empty,+ (TAL.Mov TAL.reg1 sv) `TAL.Seq`+ (TAL.Halt ty'))+++toDeclTAL :: Varmap -> TAL.Delta -> TAL.Gamma -> A.Decl -> M (Varmap, TAL.Delta, TAL.Gamma, [TAL.Instruction])+toDeclTAL vm delta gamma (A.DeclVar x (Embed av)) = do+ (sv, ty) <- toSmallVal vm av+ (rd, vm') <- var2reg x+ return $ (Map.union vm vm',+ delta,+ TAL.insertGamma rd ty gamma,+ [TAL.Mov rd sv])++toDeclTAL vm delta gamma (A.DeclPrj i x (Embed av)) = do+ (rd, vm') <- var2reg x+ (sv, ty) <- toSmallVal vm av+ ty1 <- case ty of+ TAL.TyProd tyfs -> do+ when (i >= length tyfs) $ throwError "Ld: index out of range"+ return $ fst (tyfs !! i)+ _ -> throwError "BUG: A.DeclPrj, not a product"+ return $ (Map.union vm vm',+ delta,+ TAL.insertGamma rd ty1 gamma,+ [TAL.Mov rd sv,+ TAL.Ld rd rd i])++toDeclTAL vm delta gamma (A.DeclPrim x (Embed (av1,p,av2))) = do+ (rd, vm') <- var2reg x+ (sv1, ty1) <- toSmallVal vm av1+ (sv2, ty2) <- toSmallVal vm av2+ let arith = case p of+ Plus -> TAL.Add+ Times -> TAL.Mul+ Minus -> TAL.Sub+ return $ (Map.union vm vm',+ delta,+ TAL.insertGamma rd TAL.TyInt gamma,+ [TAL.Mov rd sv1, arith rd rd sv2])+++toDeclTAL vm delta gamma (A.DeclUnpack a x (Embed av)) = do+ (rd, vm') <- var2reg x+ (sv, ty1) <- toSmallVal vm av+ let a' = translate a+ ty2 <- case ty1 of+ TAL.Exists bnd -> return $ patUnbind a' bnd+ _ -> throwError "BUG: Unpack, not an exists"+ return $ (Map.union vm vm',+ a' : delta,+ TAL.insertGamma rd ty2 gamma,+ [TAL.Unpack a' rd sv])++toDeclTAL vm delta gamma (A.DeclMalloc x (Embed tys)) = do+ (rd, vm') <- var2reg x+ tys' <- mapM toTyTAL tys+ return $ (Map.union vm vm',+ delta,+ TAL.insertGamma rd (TAL.TyProd (map (,TAL.Un) tys')) gamma,+ [TAL.Malloc rd tys'])++toDeclTAL vm delta gamma (A.DeclAssign x (Embed (av1, i, av2))) = do+ (rd, vm') <- var2reg x+ (sv1, ty1) <- toSmallVal vm av1+ (sv2, ty2) <- toSmallVal vm av2+ ty <- case ty1 of+ TAL.TyProd tyfs -> do+ when (i >= length tyfs) $ throwError "St: index out of range"+ let (before, _:after) = List.splitAt i tyfs+ return $ TAL.TyProd (before ++ [(ty2,TAL.Init)] ++ after)+ _ -> throwError "BUG: St: not a product"+ return $ (Map.union vm vm',+ delta,+ TAL.insertGamma rd ty gamma,+ [TAL.Mov rd sv1,+ TAL.Mov (TAL.rtmp 0) sv2,+ TAL.St rd i (TAL.rtmp 0)])++toHeapVal :: Varmap -> A.Ann A.HeapVal -> M (TAL.Heap, TAL.HeapVal)+toHeapVal vm (A.Ann (A.Code bnd) (A.All bnd')) = do+ mb <- unbind2 bnd bnd' -- may fail+ case mb of+ Just (as, bnd2, _, tys) -> do+ (xs, e) <- unbind bnd2+ tys' <- mapM toTyTAL tys+ let rs = [TAL.reg1 ..]+ let gamma = (zip rs tys')+ let vm' = Map.union vm (Map.fromList (zip xs (map TAL.RegVal rs)))+ let as' = map translate as+ (h, is) <- toInstrsTAL vm' as' gamma e+ return (h, TAL.Code as' gamma is)+ Nothing -> throwError "BUG!"++toHeapVal vm (A.Ann (A.Tuple avs) (A.TyProd tyfs)) = do+ wvs <- mapM (toWordVal vm) avs+ return (Map.empty, TAL.Tuple wvs)++toHeapVal vm _ = throwError "wrong type for heap val"+++toProgTAL :: (A.Tm, A.Heap) -> M TAL.Machine+toProgTAL (tm, A.Heap hp) = do+ let vars = Map.keys hp+ let labels = map (\n -> TAL.Label (translate n)) vars+ let vm =+ Map.fromList (zip vars (map (TAL.WordVal . TAL.LabelVal) labels))+ hhvs <- mapM (toHeapVal vm) (Map.elems hp)+ let (heaps, hvals) = unzip hhvs+ let hroot = Map.fromList (zip labels hvals)+ (hexp, is) <- toInstrsTAL vm [] [] tm+ let heap = Map.unions (hroot : heaps ++ [hexp])+ return (heap, Map.empty, is)
+ src/Util.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE TypeSynonymInstances,FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Util where++import Text.PrettyPrint as PP+import Control.Applicative+import Control.Monad.Identity+import Control.Monad.Trans.Except+import Control.Monad.Reader+import qualified Data.Set as Set+import qualified Data.List as List++import Unbound.LocallyNameless hiding (prec,empty,Data,Refl,Val)+import Unbound.LocallyNameless.Alpha+import Unbound.LocallyNameless.Types++------------------+-- should move to Unbound.LocallyNameless.Ops+-- ? what if the pattern binds the wrong number of variables???+patUnbind :: (Alpha p, Alpha t) => p -> Bind p t -> t+patUnbind p (B _ t) = openT p t++------------------+++-------------------------------------------------------------------------+-- Primitives+-------------------------------------------------------------------------++data Prim = Plus | Minus | Times deriving (Eq, Ord)++instance Show Prim where+ show Plus = "+"+ show Minus = "-"+ show Times = "*"++$(derive [''Prim])++instance Alpha Prim++evalPrim :: Prim -> Int -> Int -> Int+evalPrim Plus = (+)+evalPrim Times = (*)+evalPrim Minus = (-)+++-------------------------------------------------------------------------+-- Monad for evaluation, typechecking and translation.+-------------------------------------------------------------------------++type M = ExceptT String FreshM++runM :: M a -> a+runM m = case (runFreshM (runExceptT m)) of+ Left s -> error s+ Right a -> a+++-------------------------------------------------------------------------+-- The Display class and other pretty printing helper functions+-------------------------------------------------------------------------++-- | pretty-print +pp :: Display t => t -> String+pp d = render (runIdentity (runReaderT (runDM (display d)) initDI))+ +class Display t where+ -- | Convert a value to a 'Doc'.+ display :: t -> DM Doc + +newtype DM a = DM { runDM :: (ReaderT DispInfo Identity) a } + deriving (Functor,Applicative,Monad)++++maybeParens :: Bool -> Doc -> Doc+maybeParens b d = if b then parens d else d+ + +prefix :: String -> Doc -> DM Doc +prefix str d = do+ di <- ask+ return $ maybeParens (precedence str < prec di) (text str <+> d)+ +binop :: Doc -> String -> Doc -> DM Doc+binop d1 str d2 = do + di <- ask+ let dop = if str == " " then sep [d1, d2] else sep [d1, text str, d2]+ return $ maybeParens (precedence str < prec di) dop++ + +precedence :: String -> Int +precedence "->" = 10+precedence " " = 10+precedence "forall" = 9+precedence "if0" = 9+precedence "fix" = 9+precedence "\\" = 9+precedence "*" = 8+precedence "+" = 7+precedence "-" = 7+precedence _ = 0+ +++instance MonadReader DispInfo DM where+ ask = DM ask+ local f (DM m) = DM (local f m) ++-- | The data structure for information about the display+-- +data DispInfo = DI+ {+ prec :: Int, -- ^ precedence level + showTypes :: Bool, -- ^ should we show types? + dispAvoid :: Set.Set AnyName -- ^ names that have been used+ }++instance LFresh DM where+ lfresh nm = do+ let s = name2String nm+ di <- ask;+ return $ head (filter (\x -> AnyName x `Set.notMember` (dispAvoid di))+ (map (makeName s) [0..]))+ getAvoids = dispAvoid <$> ask+ avoid names = local upd where+ upd di = di { dispAvoid = + (Set.fromList names) `Set.union` (dispAvoid di) }+++-- | An empty 'DispInfo' context+initDI :: DispInfo+initDI = DI 10 False Set.empty++withPrec :: Int -> DM a -> DM a+withPrec i = + local $ \ di -> di { prec = i }+ +getPrec :: DM Int +getPrec = do+ di <- ask+ return (prec di)+ + +intersperse :: Doc -> [Doc] -> [Doc]+intersperse _ [] = []+intersperse _ [x] = [x]+intersperse sep (x:xs) = x <> sep : intersperse sep xs++displayList :: Display t => [t] -> DM Doc +displayList es = do+ ds <- mapM (withPrec 0 . display) es+ return $ cat (intersperse comma ds)+ +displayTuple :: Display t => [t] -> DM Doc +displayTuple es = do + ds <- displayList es+ return $ text "<" <> ds <> text ">" ++--------------------------------------------++instance Rep a => Display (Name a) where+ display n = return $ (text . show) n+ +--------------------------------------------++instance Display String where+ display = return . text+instance Display Int where+ display = return . text . show+instance Display Integer where+ display = return . text . show+instance Display Double where+ display = return . text . show+instance Display Float where+ display = return . text . show+instance Display Char where+ display = return . text . show+instance Display Bool where+ display = return . text . show+
+ tal.cabal view
@@ -0,0 +1,35 @@+-- Initial tal.cabal generated by cabal init. For further documentation,+-- see http://haskell.org/cabal/users-guide/++name: tal+version: 0.1.0.0+synopsis: An implementation of Typed Assembly Language (Morrisett, Walker, Crary, Glew)+-- description:+homepage: https://github.com/sweirich/tal+license: MIT+license-file: LICENSE+author: Stephanie Weirich+maintainer: sweirich@cis.upenn.edu+copyright: 2015 Stephanie Weirich+category: Language+build-type: Simple+extra-source-files: README.md+cabal-version: >=1.10+description: "From System F to Typed-Assembly Language"++library+ exposed-modules: A, C, Util, TAL, K, F, Translate+ -- other-modules:+ other-extensions: TemplateHaskell, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances, TupleSections, GADTs, TypeSynonymInstances, GeneralizedNewtypeDeriving+ build-depends: base >=4.7 && < 5+ , containers+ , mtl+ , pretty+ , transformers+ , unbound+ hs-source-dirs: src+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/sweirich/tal