diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. + diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/A.hs b/src/A.hs new file mode 100644 --- /dev/null +++ b/src/A.hs @@ -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 diff --git a/src/C.hs b/src/C.hs new file mode 100644 --- /dev/null +++ b/src/C.hs @@ -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 diff --git a/src/F.hs b/src/F.hs new file mode 100644 --- /dev/null +++ b/src/F.hs @@ -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 diff --git a/src/K.hs b/src/K.hs new file mode 100644 --- /dev/null +++ b/src/K.hs @@ -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 diff --git a/src/TAL.hs b/src/TAL.hs new file mode 100644 --- /dev/null +++ b/src/TAL.hs @@ -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 diff --git a/src/Translate.hs b/src/Translate.hs new file mode 100644 --- /dev/null +++ b/src/Translate.hs @@ -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) diff --git a/src/Util.hs b/src/Util.hs new file mode 100644 --- /dev/null +++ b/src/Util.hs @@ -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 + diff --git a/tal.cabal b/tal.cabal new file mode 100644 --- /dev/null +++ b/tal.cabal @@ -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