Permalink
Browse files

Added defunctionalisation to IRTS

idris --fovm now gives a full defunctionalising compiler for a
supercombinator language
  • Loading branch information...
1 parent 517acc1 commit 4e0fe225274d1537dab3d462404f367154bbfb01 Edwin Brady committed Sep 4, 2012
Showing with 194 additions and 39 deletions.
  1. +1 −1 idris.cabal
  2. +30 −0 iif/adder.iif
  3. +18 −0 iif/testmap.iif
  4. +1 −1 rts/idris_rts.h
  5. +22 −28 src/IRTS/CodegenC.hs
  6. +106 −2 src/IRTS/Defunctionalise.hs
  7. +10 −1 src/IRTS/LParser.hs
  8. +6 −6 src/IRTS/Lang.hs
View
@@ -71,7 +71,7 @@ Executable idris
RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,
IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
- IRTS.CodegenC,
+ IRTS.CodegenC, IRTS.Defunctionalise,
Paths_idris
View
@@ -0,0 +1,30 @@
+data O 0
+data S 1
+
+fun plus(x, y) = case x of {
+ O => y
+ | S(k) => S (plus(k, y))
+ }
+
+fun natToInt(x) = case x of {
+ O => 0
+ | S(k) => let y = natToInt(k) in y + 1
+ }
+
+fun adder(arity, acc) = case arity of {
+ O => acc
+ | S(k) => adderAux(k, acc)
+ }
+
+fun adderAux(k, acc, n) = adder(k, plus(acc, n))
+
+fun zero() = O
+fun one() = S(zero)
+fun two() = S(one)
+fun three() = S(two)
+fun four() = S(three)
+fun five() = S(four)
+
+fun main() = %WriteInt(natToInt(adder(three, two, three, four, five)))
+
+
View
@@ -0,0 +1,18 @@
+data Nil 0
+data Cons 2
+
+fun twice(f, x) = f(f(x))
+
+fun map(f, xs) = case xs of {
+ Nil => Nil
+ | Cons(y, ys) => Cons(f(y), map(f, ys))
+ }
+
+fun dumpList(xs) = case xs of {
+ Nil => "END"
+ | Cons(y, ys) => %IntString(y) ++ ", " ++ dumpList(ys)
+ }
+
+fun double(x) = x + x
+
+fun main() = %WriteString(dumpList(map(twice(double), Cons(4, Cons(6, Nil)))))
View
@@ -64,7 +64,7 @@ typedef void(*func)(VM*, VAL*);
#define GETPTR(x) (((VAL)(x))->info.ptr)
#define GETFLOAT(x) (((VAL)(x))->info.f)
-#define TAG(x) ((x)->info.c.tag)
+#define TAG(x) (ISINT(x) ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag : (-1)) )
// Integers, floats and operators
View
@@ -18,7 +18,7 @@ import Control.Monad
data DbgLevel = NONE | DEBUG | TRACE
-codegenC :: [(Name, LDecl)] ->
+codegenC :: [(Name, SDecl)] ->
String -> -- output file name
Bool -> -- generate executable if True, only .o if False
[FilePath] -> -- include files
@@ -27,33 +27,27 @@ codegenC :: [(Name, LDecl)] ->
IO ()
codegenC defs out exec incs libs dbg
= do -- print defs
- let tagged = addTags defs
- let ctxtIn = addAlist tagged emptyContext
- let checked = checkDefs ctxtIn tagged
- case checked of
- OK c -> do let bc = map toBC c
- let h = concatMap toDecl (map fst bc)
- let cc = concatMap (uncurry toC) bc
- d <- getDataDir
- mprog <- readFile (d ++ "/rts/idris_main.c")
- let cout = headers incs ++ debug dbg ++ h ++ cc ++
- (if exec then mprog else "")
- (tmpn, tmph) <- tempfile
- hPutStr tmph cout
- hFlush tmph
- hClose tmph
- let gcc = "gcc -x c " ++
- (if exec then "" else " - c ") ++
- gccDbg dbg ++
- " " ++ tmpn ++
- " `idris --link` `idris --include` " ++ libs ++
- " -lidris_rts -o " ++ out
--- putStrLn cout
- exit <- system gcc
- when (exit /= ExitSuccess) $
- putStrLn ("FAILURE: " ++ gcc)
-
- Error e -> fail $ "Can't happen: Something went wrong in codegenC\n" ++ show e
+ let bc = map toBC defs
+ let h = concatMap toDecl (map fst bc)
+ let cc = concatMap (uncurry toC) bc
+ d <- getDataDir
+ mprog <- readFile (d ++ "/rts/idris_main.c")
+ let cout = headers incs ++ debug dbg ++ h ++ cc ++
+ (if exec then mprog else "")
+ (tmpn, tmph) <- tempfile
+ hPutStr tmph cout
+ hFlush tmph
+ hClose tmph
+ let gcc = "gcc -x c " ++
+ (if exec then "" else " - c ") ++
+ gccDbg dbg ++
+ " " ++ tmpn ++
+ " `idris --link` `idris --include` " ++ libs ++
+ " -lidris_rts -o " ++ out
+-- putStrLn cout
+ exit <- system gcc
+ when (exit /= ExitSuccess) $
+ putStrLn ("FAILURE: " ++ gcc)
headers [] = "#include <idris_rts.h>\n\n"
headers (x : xs) = "#include <" ++ x ++ ">\n" ++ headers xs
@@ -3,8 +3,22 @@ module IRTS.Defunctionalise where
import IRTS.Lang
import Core.TT
-defunctionalise :: [(Name, LDecl)] -> [(Name, LDecl)]
-defunctionalise defs = defs -- TODO!
+import Debug.Trace
+import Data.Maybe
+
+defunctionalise :: Int -> LDefs -> LDefs
+defunctionalise nexttag defs
+ = let all = toAlist defs
+ newcons = concatMap toCons (getFn all)
+ eval = mkEval newcons
+ app = mkApply newcons
+ condecls = declare nexttag newcons in
+ addAlist (eval : app : condecls ++ (map (addApps defs) all)) emptyContext
+
+getFn :: [(Name, LDecl)] -> [(Name, Int)]
+getFn xs = mapMaybe fnData xs
+ where fnData (n, LFun _ args _) = Just (n, length args)
+ fnData _ = Nothing
-- To defunctionalise:
--
@@ -16,5 +30,95 @@ defunctionalise defs = defs -- TODO!
-- 5 Create an APPLY function which adds an argument to each underapplication (or calls
-- APPLY again for an exact application)
-- 6 Wrap overapplications in chains of APPLY
+-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY
+-- 8 Add explicit EVAL to case, primitives, and foreign calls
+
+addApps :: LDefs -> (Name, LDecl) -> (Name, LDecl)
+addApps defs o@(n, LConstructor _ _ _) = o
+addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))
+ where
+ aa env (LV (Glob n)) | n `elem` env = LV (Glob n)
+ | otherwise = aa env (LApp False n [])
+-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e
+ aa env (LApp tc n args)
+ = let args' = map (aa env) args in
+ case lookupCtxt Nothing n defs of
+ [LConstructor _ i ar] -> LApp tc n args'
+ [LFun _ as _] -> let arity = length as in
+ fixApply tc n args' arity
+ [] -> chainAPPLY (LV (Glob n)) args'
+ aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)
+ aa env (LCon i n args) = LCon i n (map (aa env) args)
+ aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)
+ aa env (LConst c) = LConst c
+ aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args)
+ aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args)
+
+ aaF env (t, e) = (t, eEVAL (aa env e))
+
+ aaAlt env (LConCase i n args e) = LConCase i n args (aa (args ++ env) e)
+ aaAlt env (LConstCase c e) = LConstCase c (aa env e)
+ aaAlt env (LDefaultCase e) = LDefaultCase (aa env e)
+
+ eEVAL x = LApp False (MN 0 "EVAL") [x]
+
+ fixApply tc n args ar
+ | length args == ar = LApp tc n args
+ | length args < ar = LApp tc (mkUnderCon n (ar - length args)) args
+ | length args > ar = chainAPPLY (LApp tc n (take ar args)) (drop ar args)
+
+ chainAPPLY f [] = f
+ chainAPPLY f (a : as) = chainAPPLY (LApp False (MN 0 "APPLY") [f, a]) as
+
+data EvalApply a = EvalCase a
+ | ApplyCase a
+ deriving Show
+
+-- For a function name, generate a list of
+-- data constuctors, and whether to handle them in EVAL or APPLY
+
+toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]
+toCons (n, i) = (mkFnCon n, i,
+ EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))
+ (LApp False n (map (LV . Glob) (take i (genArgs 0))))))
+ :
+ mkApplyCase n 0 i
+
+mkApplyCase fname n ar | n == ar = []
+mkApplyCase fname n ar
+ = let nm = mkUnderCon fname (ar - n) in
+ (nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0))
+ (LApp False (mkUnderCon fname (ar - (n + 1)))
+ (map (LV . Glob) (take n (genArgs 0) ++
+ [MN 0 "arg"])))))
+ : mkApplyCase fname (n + 1) ar
+
+mkEval :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
+mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"]
+ (LCase (LV (Glob (MN 0 "arg")))
+ (mapMaybe evalCase xs ++
+ [LDefaultCase (LV (Glob (MN 0 "arg")))])))
+ where
+ evalCase (n, t, EvalCase x) = Just x
+ evalCase _ = Nothing
+
+mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
+mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]
+ (LCase (LApp False (MN 0 "EVAL") [LV (Glob (MN 0 "fn"))])
+ (mapMaybe applyCase xs)))
+ where
+ applyCase (n, t, ApplyCase x) = Just x
+ applyCase _ = Nothing
+
+declare :: Int -> [(Name, Int, EvalApply LAlt)] -> [(Name, LDecl)]
+declare t xs = dec' t xs [] where
+ dec' t [] acc = reverse acc
+ dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, LConstructor n t ar) : acc)
+
+
+genArgs i = MN i "P_c" : genArgs (i + 1)
+mkFnCon n = MN 0 ("P_" ++ show n)
+mkUnderCon n 0 = n
+mkUnderCon n missing = MN missing ("U_" ++ show n)
View
@@ -6,6 +6,7 @@ import IRTS.Lang
import IRTS.Simplified
import IRTS.Bytecode
import IRTS.CodegenC
+import IRTS.Defunctionalise
import Paths_idris
import Text.ParserCombinators.Parsec
@@ -46,7 +47,15 @@ lchar = lexeme.char
fovm :: FilePath -> IO ()
fovm f = do defs <- parseFOVM f
- codegenC defs "a.out" True ["math.h"] "" TRACE
+ let (nexttag, tagged) = addTags 0 defs
+ let ctxtIn = addAlist tagged emptyContext
+ let defuns = defunctionalise nexttag ctxtIn
+-- print defuns
+ let checked = checkDefs defuns (toAlist defuns)
+-- print checked
+ case checked of
+ OK c -> codegenC c "a.out" True ["math.h"] "" TRACE
+ Error e -> fail $ show e
parseFOVM :: FilePath -> IO [(Name, LDecl)]
parseFOVM fname = do -- putStrLn $ "Reading " ++ fname
View
@@ -41,10 +41,10 @@ data LDecl = LFun Name [Name] LExp -- name, arg names, definition
type LDefs = Ctxt LDecl
-addTags :: [(Name, LDecl)] -> [(Name, LDecl)]
-addTags ds = tag 0 ds
- where tag i ((n, LConstructor n' t a) : as)
- = (n, LConstructor n' i a) : tag (i + 1) as
- tag i (x : as) = x : tag i as
- tag i [] = []
+addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
+addTags i ds = tag i ds []
+ where tag i ((n, LConstructor n' t a) : as) acc
+ = tag (i + 1) as ((n, LConstructor n' i a) : acc)
+ tag i (x : as) acc = tag i as (x : acc)
+ tag i [] acc = (i, reverse acc)

0 comments on commit 4e0fe22

Please sign in to comment.