diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2015 Danny Gratzer + +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,127 @@ +## pcf + +A one file compiler for PCF to C. It's currently about 275 lines of +compiler and 75 lines of extremely boring instances. The compiler is +fully explained in [this blog post][post]. + +## What's PCF + +PCF is a tiny typed, higher-order functional language. It has 3 main +constructs, + +1. Natural Numbers + + In PCF there are two constants for natural numbers. `Zero` and + `Suc`. `Zero` is pretty self explanatory. `Suc e` is the successor + of a natural number, it's `1 + e` in other languages. Finally, + when given a natural number you can pattern match on it with + `ifz`. + + ifz e { + Zero => ... + | Suc x => ... + } + + Here the first branch runs if `e` evaluates to zero and the second + branch is run if `e` evaluates to `Suc ...`. `x` is bound to the + predecessor of `e` in the successor case. + +2. Functions + + PCF has functions. They can close over variables and are higher + order. Their pretty much what you would expect from a functional + language. The relevant words here are `Lam` and `App`. Note that + functions must be annotated with their arguments type. + +3. General Recursion + + PCF has general recursion (and is thus Turing complete). It + provides it in a slightly different way than you might be used + to. In PCF you have the expression `fix x : t in ...` and in the + `...` `x` would be bound. The intuition here is that `x` stands for + the whole `fix x : t in ...` expression. If you're a Haskell person + you can just desugar this to `fix $ \x : t -> ...`. + + +## Example + +For a quick example of how this all hangs together, here is how you +would define `plus` in PCF + +``` haskell + plus = + fix rec : nat -> nat -> nat in + λ m : nat. + λ n : nat. + ifz m { + Zero => n + | Suc x => Suc (rec x n) + } +``` + +For this library we'd write this AST as + +``` haskell + let lam x e = Lam Nat $ abstract1 x e + fix x e = Fix (Arr Nat (Arr Nat Nat)) $ abstract1 x e + ifz i t x e = Ifz i t (abstract1 x e) + plus = fix 1 $ lam 2 $ lam 3 $ + ifz (V 2) + (V 3) + 4 (Suc (App (V 1) (V 4) `App` (V 3))) + in App (App plus (Suc Zero)) (Suc Zero) +``` + +We can then chuck this into the compiler and it will spit out the +following C code + +``` c + tagged_ptr _21(tagged_ptr * _30) + { + tagged_ptr _31 = dec(_30[1]); + tagged_ptr _35 = EMPTY; + if (isZero(_30[1])) + { + _35 = _30[2]; + } + else + { + tagged_ptr _32 = apply(_30[0], _31); + tagged_ptr _33 = apply(_32, _30[2]); + tagged_ptr _34 = inc(_33); + _35 = _34; + } + return _35; + } + tagged_ptr _18(tagged_ptr * _36) + { + tagged_ptr _37 = mkClos(_21, 2, _36[0], _36[1]); + return _37; + } + tagged_ptr _16(tagged_ptr * _38) + { + tagged_ptr _39 = mkClos(_18, 1, _38[0]); + return _39; + } + tagged_ptr _29(tagged_ptr * _40) + { + tagged_ptr _41 = mkClos(_16, 0); + tagged_ptr _42 = fixedPoint(_41); + tagged_ptr _43 = mkZero(); + tagged_ptr _49 = inc(_43); + tagged_ptr _50 = apply(_42, _49); + tagged_ptr _51 = mkZero(); + tagged_ptr _56 = inc(_51); + tagged_ptr _57 = apply(_50, _56); + return _57; + } + int main() + { + call(_29); + } +``` + +Which when run with `preamble.c` pasted on top it prints out `2`. As +you'd hope. + +[post]: http://jozefg.bitbucket.org/posts/2015-03-24-pcf.html 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/pcf.cabal b/pcf.cabal new file mode 100644 --- /dev/null +++ b/pcf.cabal @@ -0,0 +1,39 @@ +name: pcf +version: 0.1.0.0 +synopsis: A one file compiler for PCF +description: PCF is a small programming language with higher order + functions, natural numbers, and recursion. It is + statically tpyed and turing complete (general + recursion and all that). This compiler transformers + a PCF expression into a file of C code that when run + outputs the answer. + + It is mostly intended as a + demonstration of how to write such a compiler. The + curious reader should look at the . +license: MIT +license-file: LICENSE +author: Danny Gratzer +maintainer: jozefg@cmu.edu +category: Compiler +build-type: Simple +extra-source-files: README.md +data-files: src/preamble.c +cabal-version: >=1.10 +source-repository head + type: git + location: http://github.com/jozefg/pcf +library + hs-source-dirs: src + exposed-modules: Language.Pcf + other-modules: Paths_pcf + build-depends: base >=4.0 && <5 + , bound == 1.* + , c-dsl + , containers >= 0.5 + , monad-gen + , mtl == 2.* + , prelude-extras + , transformers + , void + default-language: Haskell2010 diff --git a/src/Language/Pcf.hs b/src/Language/Pcf.hs new file mode 100644 --- /dev/null +++ b/src/Language/Pcf.hs @@ -0,0 +1,354 @@ +{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-} +{-# LANGUAGE LambdaCase, OverloadedStrings #-} +module Language.Pcf (Ty(..), Exp(..), compile, output) where +import Bound +import Control.Applicative +import Control.Monad +import Control.Monad.Gen +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import Control.Monad.Writer +import Data.Foldable +import Data.List (elemIndex) +import qualified Data.Map as M +import Data.Maybe (fromJust) +import qualified Data.Set as S +import Data.String +import Data.Traversable hiding (mapM) +import Language.C.DSL +import Prelude.Extras +import Paths_pcf + +data Ty = Arr Ty Ty + | Nat + deriving Eq + +data Exp a = V a + | App (Exp a) (Exp a) + | Ifz (Exp a) (Exp a) (Scope () Exp a) + | Lam Ty (Scope () Exp a) + | Fix Ty (Scope () Exp a) + | Suc (Exp a) + | Zero + deriving (Eq, Functor, Foldable, Traversable) + +-------------------------------------------------------- +--------------- Type Checking -------------------------- +-------------------------------------------------------- + +type TyM a = MaybeT (Gen a) + +assertTy :: Ord a => M.Map a Ty -> Exp a -> Ty -> TyM a () +assertTy env e t = (== t) <$> typeCheck env e >>= guard + +typeCheck :: Ord a => M.Map a Ty -> Exp a -> TyM a Ty +typeCheck _ Zero = return Nat +typeCheck env (Suc e) = assertTy env e Nat >> return Nat +typeCheck env (V a) = MaybeT . return $ M.lookup a env +typeCheck env (App f a) = typeCheck env f >>= \case + Arr fTy tTy -> assertTy env a fTy >> return tTy + _ -> mzero +typeCheck env (Lam t bind) = do + v <- gen + Arr t <$> typeCheck (M.insert v t env) (instantiate1 (V v) bind) +typeCheck env (Fix t bind) = do + v <- gen + assertTy (M.insert v t env) (instantiate1 (V v) bind) t + return t +typeCheck env (Ifz i t e) = do + assertTy env i Nat + ty <- typeCheck env t + v <- gen + assertTy (M.insert v Nat env) (instantiate1 (V v) e) ty + return ty + +-------------------------------------------------------- +--------------- Closure Conversion --------------------- +-------------------------------------------------------- + +-- Invariant, Clos only contains VCs, can't be enforced statically due +-- to annoying monad instance +type Clos a = [ExpC a] + +data ExpC a = VC a + | AppC (ExpC a) (ExpC a) + | LamC Ty (Clos a) (Scope Int ExpC a) + | FixC Ty (Clos a) (Scope Int ExpC a) + | IfzC (ExpC a) (ExpC a) (Scope () ExpC a) + | SucC (ExpC a) + | ZeroC + deriving (Eq, Functor, Foldable, Traversable) + +closConv :: Ord a => Exp a -> Gen a (ExpC a) +closConv (V a) = return (VC a) +closConv Zero = return ZeroC +closConv (Suc e) = SucC <$> closConv e +closConv (App f a) = AppC <$> closConv f <*> closConv a +closConv (Ifz i t e) = do + v <- gen + e' <- abstract1 v <$> closConv (instantiate1 (V v) e) + IfzC <$> closConv i <*> closConv t <*> return e' +closConv (Fix t bind) = do + v <- gen + body <- closConv (instantiate1 (V v) bind) + let freeVars = S.toList . S.delete v $ foldMap S.singleton body + rebind v' = elemIndex v' freeVars <|> + (guard (v' == v) *> (Just $ length freeVars)) + return $ FixC t (map VC freeVars) (abstract rebind body) +closConv (Lam t bind) = do + v <- gen + body <- closConv (instantiate1 (V v) bind) + let freeVars = S.toList . S.delete v $ foldMap S.singleton body + rebind v' = elemIndex v' freeVars <|> + (guard (v' == v) *> (Just $ length freeVars)) + return $ LamC t (map VC freeVars) (abstract rebind body) + +-------------------------------------------------------- +--------------- Lambda + Fixpoint lifting -------------- +-------------------------------------------------------- + +data BindL a = RecL Ty [ExpL a] (Scope Int ExpL a) + | NRecL Ty [ExpL a] (Scope Int ExpL a) + deriving (Eq, Functor, Foldable, Traversable) +data ExpL a = VL a + | AppL (ExpL a) (ExpL a) + | LetL [BindL a] (Scope Int ExpL a) + | IfzL (ExpL a) (ExpL a) (Scope () ExpL a) + | SucL (ExpL a) + | ZeroL + deriving (Eq, Functor, Foldable, Traversable) + +trivLetBody :: Scope Int ExpL a +trivLetBody = fromJust . closed . abstract (const $ Just 0) $ VL () + +llift :: Eq a => ExpC a -> Gen a (ExpL a) +llift (VC a) = return (VL a) +llift ZeroC = return ZeroL +llift (SucC e) = SucL <$> llift e +llift (AppC f a) = AppL <$> llift f <*> llift a +llift (IfzC i t e) = do + v <- gen + e' <- abstract1 v <$> llift (instantiate1 (VC v) e) + IfzL <$> llift i <*> llift t <*> return e' +llift (LamC t clos bind) = do + vs <- replicateM (length clos + 1) gen + body <- llift $ instantiate (VC . (!!) vs) bind + clos' <- mapM llift clos + let bind' = abstract (flip elemIndex vs) body + return (LetL [NRecL t clos' bind'] trivLetBody) +llift (FixC t clos bind) = do + vs <- replicateM (length clos + 1) gen + body <- llift $ instantiate (VC . (!!) vs) bind + clos' <- mapM llift clos + let bind' = abstract (flip elemIndex vs) body + return (LetL [RecL t clos' bind'] trivLetBody) + +-------------------------------------------------------- +--------------- Conversion to Faux-C ------------------- +-------------------------------------------------------- + +-- Invariant: the Integer part of a FauxCTop is a globally unique +-- identifier that will be used as a name for that binding. +type NumArgs = Int +data BindTy = Int | Clos deriving Eq + +data FauxCTop a = FauxCTop Integer NumArgs (Scope Int FauxC a) + deriving (Eq, Functor, Foldable, Traversable) +data BindFC a = NRecFC Integer [FauxC a] + | RecFC BindTy Integer [FauxC a] + deriving (Eq, Functor, Foldable, Traversable) +data FauxC a = VFC a + | AppFC (FauxC a) (FauxC a) + | IfzFC (FauxC a) (FauxC a) (Scope () FauxC a) + | LetFC [BindFC a] (Scope Int FauxC a) + | SucFC (FauxC a) + | ZeroFC + deriving (Eq, Functor, Foldable, Traversable) + +type FauxCM a = WriterT [FauxCTop a] (Gen a) + +fauxc :: ExpL Integer -> FauxCM Integer (FauxC Integer) +fauxc (VL a) = return (VFC a) +fauxc (AppL f a) = AppFC <$> fauxc f <*> fauxc a +fauxc ZeroL = return ZeroFC +fauxc (SucL e) = SucFC <$> fauxc e +fauxc (IfzL i t e) = do + v <- gen + e' <- abstract1 v <$> fauxc (instantiate1 (VL v) e) + IfzFC <$> fauxc i <*> fauxc t <*> return e' +fauxc (LetL binds e) = do + binds' <- mapM liftBinds binds + vs <- replicateM (length binds) gen + body <- fauxc $ instantiate (VL . (!!) vs) e + let e' = abstract (flip elemIndex vs) body + return (LetFC binds' e') + where lifter bindingConstr clos bind = do + guid <- gen + vs <- replicateM (length clos + 1) gen + body <- fauxc $ instantiate (VL . (!!) vs) bind + let bind' = abstract (flip elemIndex vs) body + tell [FauxCTop guid (length clos + 1) bind'] + bindingConstr guid <$> mapM fauxc clos + bindTy (Arr _ _) = Clos + bindTy Nat = Int + liftBinds (NRecL t clos bind) = lifter NRecFC clos bind + liftBinds (RecL t clos bind) = lifter (RecFC $ bindTy t) clos bind + +-------------------------------------------------------- +--------------- Conversion to Real C ------------------- +-------------------------------------------------------- + +type RealCM = WriterT [CBlockItem] (Gen Integer) + +i2d :: Integer -> CDeclr +i2d = fromString . ('_':) . show + +i2e :: Integer -> CExpr +i2e = var . fromString . ('_':) . show + +taggedTy :: CDeclSpec +taggedTy = CTypeSpec "tagged_ptr" + +tellDecl :: CExpr -> RealCM CExpr +tellDecl e = do + i <- gen + tell [CBlockDecl $ decl taggedTy (i2d i) $ Just e] + return (i2e i) + +realc :: FauxC CExpr -> RealCM CExpr +realc (VFC e) = return e +realc (AppFC f a) = ("apply" #) <$> mapM realc [f, a] >>= tellDecl +realc ZeroFC = tellDecl $ "mkZero" # [] +realc (SucFC e) = realc e >>= tellDecl . ("inc"#) . (:[]) +realc (IfzFC i t e) = do + outi <- realc i + deci <- tellDecl ("dec" # [outi]) + let e' = instantiate1 (VFC deci) e + (outt, blockt) <- lift . runWriterT $ (realc t) + (oute, blocke) <- lift . runWriterT $ (realc e') + out <- tellDecl "EMPTY" + let branch b tempOut = + CCompound [] (b ++ [CBlockStmt . liftE $ out <-- tempOut]) undefNode + ifStat = + cifElse ("isZero"#[outi]) (branch blockt outt) (branch blocke oute) + tell [CBlockStmt ifStat] + return out +realc (LetFC binds bind) = do + bindings <- mapM goBind binds + realc $ instantiate (VFC . (bindings !!)) bind + where sizeOf Int = "INT_SIZE" + sizeOf Clos = "CLOS_SIZE" + goBind (NRecFC i cs) = + ("mkClos" #) <$> (i2e i :) . (fromIntegral (length cs) :) + <$> mapM realc cs + >>= tellDecl + goBind (RecFC t i cs) = do + f <- ("mkClos" #) <$> (i2e i :) . (fromIntegral (length cs) :) + <$> mapM realc cs + >>= tellDecl + tellDecl ("fixedPoint"#[f, sizeOf t]) + +topc :: FauxCTop CExpr -> Gen Integer CFunDef +topc (FauxCTop i numArgs body) = do + binds <- gen + let getArg = (!!) (args (i2e binds) numArgs) + (out, block) <- runWriterT . realc $ instantiate getArg body + return $ + fun [taggedTy] ('_' : show i) [decl taggedTy $ ptr (i2d binds)] $ + CCompound [] (block ++ [CBlockStmt . creturn $ out]) undefNode + where indexArg binds i = binds ! fromIntegral i + args binds na = map (VFC . indexArg binds) [0..na - 1] + +-- | Given an expression where free variables are integers, convert it +-- to C. This function doesn't include all of the runtime system in +-- the translation unit which makes it unsuitable for running all on +-- its own. It's primarly for inspecting the copmiled result of a +-- given expression. +compile :: Exp Integer -> Maybe CTranslUnit +compile e = runGen . runMaybeT $ do + assertTy M.empty e Nat + funs <- lift $ pipe e + return . transUnit . map export $ funs + where pipe e = do + simplified <- closConv e >>= llift + (main, funs) <- runWriterT $ fauxc simplified + i <- gen + let topMain = FauxCTop i 1 (abstract (const Nothing) main) + funs' = map (i2e <$>) (funs ++ [topMain]) + (++ [makeCMain i]) <$> mapM topc funs' + makeCMain entry = + fun [intTy] "main"[] $ hBlock ["call"#[i2e entry]] + +-- | Compiles ane expression using 'compile'. If we can compile +-- program this function returns an @Just s@ action which returns this +-- where @s@ is a runnable C program which outputs the result. If +-- there was a type error, this gives back 'Nothing'. +output :: Exp Integer -> IO (Maybe String) +output e = case compile e of + Nothing -> return Nothing + Just p -> Just $ do + rts <- getDataFileName "src/preamble.c" >>= readFile + return . Just $ rts ++ '\n' : pretty p + + +------------------------------------------------------------------- +------------------- Extremely Boring Instances -------------------- +------------------------------------------------------------------- + +instance Eq1 Exp where +instance Applicative Exp where + pure = return + (<*>) = ap +instance Monad Exp where + return = V + V a >>= f = f a + App l r >>= f = App (l >>= f) (r >>= f) + Lam t body >>= f = Lam t (body >>>= f) + Fix t body >>= f = Fix t (body >>>= f) + Ifz i t e >>= f = Ifz (i >>= f) (t >>= f) (e >>>= f) + Suc e >>= f = Suc (e >>= f) + Zero >>= _ = Zero + +instance Eq1 ExpC where +instance Applicative ExpC where + pure = return + (<*>) = ap +instance Monad ExpC where + return = VC + VC a >>= f = f a + AppC l r >>= f = AppC (l >>= f) (r >>= f) + LamC t clos body >>= f = LamC t (map (>>= f) clos) (body >>>= f) + FixC t clos body >>= f = FixC t (map (>>= f) clos) (body >>>= f) + IfzC i t e >>= f = IfzC (i >>= f) (t >>= f) (e >>>= f) + SucC e >>= f = SucC (e >>= f) + ZeroC >>= _ = ZeroC + +instance Eq1 ExpL where +instance Applicative ExpL where + pure = return + (<*>) = ap +instance Monad ExpL where + return = VL + VL a >>= f = f a + AppL l r >>= f = AppL (l >>= f) (r >>= f) + SucL e >>= f = SucL (e >>= f) + ZeroL >>= _ = ZeroL + IfzL i t e >>= f = IfzL (i >>= f) (t >>= f) (e >>>= f) + LetL binds body >>= f = LetL (map go binds) (body >>>= f) + where go (RecL t es scope) = RecL t (map (>>= f) es) (scope >>>= f) + go (NRecL t es scope) = NRecL t (map (>>= f) es) (scope >>>= f) + +instance Eq1 FauxC where +instance Applicative FauxC where + pure = return + (<*>) = ap +instance Monad FauxC where + return = VFC + VFC a >>= f = f a + AppFC l r >>= f = AppFC (l >>= f) (r >>= f) + SucFC e >>= f = SucFC (e >>= f) + ZeroFC >>= _ = ZeroFC + IfzFC i t e >>= f = IfzFC (i >>= f) (t >>= f) (e >>>= f) + LetFC binds body >>= f = LetFC (map go binds) (body >>>= f) + where go (NRecFC i es) = NRecFC i (map (>>= f) es) + go (RecFC t i es) = RecFC t i (map (>>= f) es) diff --git a/src/preamble.c b/src/preamble.c new file mode 100644 --- /dev/null +++ b/src/preamble.c @@ -0,0 +1,111 @@ +#include +#include +#include +#include + +#define EMPTY {.blackhole = NULL, .ptr = NULL} +#define INT_SIZE sizeof(int) +#define CLOS_SIZE sizeof(clos) + +typedef struct { + void *ptr; + int *blackhole; +} tagged_ptr; + +typedef tagged_ptr (*raw_fun)(tagged_ptr *); + +typedef struct { + raw_fun fun; + int numArgs; + tagged_ptr *args; +} clos; + +tagged_ptr apply(tagged_ptr fun, tagged_ptr arg){ + if(*fun.blackhole || *arg.blackhole) exit(1); + + clos *c = fun.ptr; + c->args[c->numArgs - 1] = arg; + return c->fun(c->args); +} + +tagged_ptr mkZero(){ + int *ptr = malloc(sizeof(int)); + int *hole = malloc(sizeof(int)); + + *ptr = 0; + *hole = 0; + + tagged_ptr new_ptr = {.ptr = ptr, .blackhole = hole}; + return new_ptr; +} + +tagged_ptr inc(tagged_ptr i){ + int *ptr = malloc(sizeof(int)); + int *hole = malloc(sizeof(int)); + + if(*i.blackhole) exit(1); + + *ptr = *((int *) i.ptr) + 1; + *hole = 0; + + tagged_ptr new_ptr = {.ptr = ptr, .blackhole = hole}; + return new_ptr; + +} + +tagged_ptr dec(tagged_ptr i){ + int *ptr = malloc(sizeof(int)); + int *hole = malloc(sizeof(int)); + + if(*i.blackhole) exit(1); + + *ptr = *((int *) i.ptr) - 1; + *hole = 0; + + tagged_ptr new_ptr = {.ptr = ptr, .blackhole = hole}; + return new_ptr; +} + +int isZero(tagged_ptr i){ + return *((int *) i.ptr) == 0; +} + +tagged_ptr mkClos(raw_fun f, int numArgs, ...){ + clos *c = malloc(sizeof(clos)); + int *hole = malloc(sizeof(int)); + va_list l; + + c->fun = f; + c->numArgs = numArgs + 1; + c->args = malloc(sizeof(tagged_ptr) * (numArgs + 1)); + *hole = 0; + + va_start(l, numArgs); + for(int i = 0; i < numArgs; ++i) + c->args[i] = va_arg(l, tagged_ptr); + tagged_ptr new_ptr = {.ptr = c, .blackhole = hole}; + return new_ptr; +} + +tagged_ptr fixedPoint(tagged_ptr f, size_t i){ + int *hole = malloc(sizeof(int)); + tagged_ptr sized_dummy = {.ptr = malloc(i), + .blackhole = hole}; + *hole = 1; + + clos *c = f.ptr; + c->args[c->numArgs - 1] = sized_dummy; + tagged_ptr res = c->fun(c->args); + + if(*res.blackhole) exit(1); + + memcpy(sized_dummy.ptr, res.ptr, i); + *sized_dummy.blackhole = 0; + + return res; +} + +void call(raw_fun f){ + tagged_ptr i = f(NULL); + printf("%d\n", *((int *) i.ptr)); +}