1{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
3module IRTS.Compiler(compile, generate) where
7import IRTS.Defunctionalise
9import IRTS.CodegenCommon
12import IRTS.CodegenJavaScript
17import Idris.AbsSyntaxTree
25import Idris.Core.Evaluate
26import Idris.Core.CaseTree
28import Control.Category
29import Prelude hiding (id, (.))
31import Control.Applicative
32import Control.Monad.State
36import Data.IntSet (IntSet)
37import qualified Data.IntSet as IS
38import qualified Data.Map as M
39import qualified Data.Set as S
43import System.Directory
44import System.Environment
45import System.FilePath ((</>), addTrailingPathSeparator)
47-- | Compile to simplified forms and return CodegenInfo
48compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
50 = do checkMVs -- check for undefined metavariables
51 checkTotality -- refuse to compile if there are totality problems
52 exports <- findExports
53 let rootNames = case mtm of
57 reachableNames <- performUsageAnalysis
58 (rootNames ++ getExpNames exports)
59 maindef <- case mtm of
61 Just tm -> do md <- irMain tm
62 logCodeGen 1 $ "MAIN: " ++ show md
63 return [(sMN 0 "runMain", md)]
64 objs <- getObjectFiles codegen
65 libs <- getLibs codegen
66 flags <- getFlags codegen
67 hdrs <- getHdrs codegen
68 impdirs <- allImportDirs
69 defsIn <- mkDecls reachableNames
70 -- if no 'main term' given, generate interface files
71 let iface = case mtm of
75 let defs = defsIn ++ maindef
77 -- Inlined top level LDecl made here
78 let defsInlined = inlineAll defs
79 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
82 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)
83 let ctxtIn = addAlist tagged emptyContext
85 logCodeGen 1 "Defunctionalising"
86 let defuns_in = defunctionalise nexttag ctxtIn
87 logCodeGen 5 $ show defuns_in
88 logCodeGen 1 "Inlining"
89 let defuns = inline defuns_in
90 logCodeGen 5 $ show defuns
91 logCodeGen 1 "Resolving variables for CG"
93 let checked = simplifyDefs defuns (toAlist defuns)
95 dumpCases <- getDumpCases
96 dumpDefun <- getDumpDefun
99 Just f -> runIO $ writeFile f (showCaseTrees defs)
102 Just f -> runIO $ writeFile f (dumpDefuns defuns)
103 triple <- Idris.AbsSyntax.targetTriple
104 cpu <- Idris.AbsSyntax.targetCPU
105 logCodeGen 1 "Building output"
107 OK c -> do return $ CodegenInfo f outty triple cpu
108 hdrs impdirs objs libs flags
109 NONE c (toAlist defuns)
112 where checkMVs = do i <- getIState
113 case map fst (idris_metavars i) \\ primDefs of
115 ms -> ifail $ "There are undefined holes: " ++ show ms
116 checkTotality = do i <- getIState
117 case idris_totcheckfail i of
119 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
121generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
122generate codegen mainmod ir
124 -- Built-in code generators (FIXME: lift these out!)
125 Via "c" -> codegenC ir
126 -- Any external code generator
127 Via cg -> do let cmd = "idris-codegen-" ++ cg
128 args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir
129 exit <- rawSystem cmd args
130 when (exit /= ExitSuccess) $
131 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
132 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
134irMain :: TT Name -> Idris LDecl
136 i <- irTerm M.empty [] tm
137 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
139mkDecls :: [Name] -> Idris [(Name, LDecl)]
142 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
143 decls <- mapM build ds
146showCaseTrees :: [(Name, LDecl)] -> String
147showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
149 showCT (n, LFun _ f args lexp)
150 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
152 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
154 defnRank :: (Name, LDecl) -> String
155 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
156 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
158 nameRank :: Name -> String
159 nameRank (UN s) = "1" ++ show s
160 nameRank (MN i s) = "2" ++ show s ++ show i
161 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
162 nameRank (SN sn) = "4" ++ snRank sn
163 nameRank n = "5" ++ show n
165 snRank :: SpecialName -> String
166 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
167 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
168 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
169 snRank (MethodN n) = "4" ++ nameRank n
170 snRank (CaseN _ n) = "5" ++ nameRank n
171 snRank (ElimN n) = "6" ++ nameRank n
172 snRank (InstanceCtorN n) = "7" ++ nameRank n
173 snRank (WithN i n) = "8" ++ nameRank n ++ show i
175isCon (TyDecl _ _) = True
178build :: (Name, Def) -> Idris (Name, LDecl)
183 let args = map (\x -> sMN x "op") [0..] in
184 return (n, (LFun [] n (take ar args)
185 (LOp op (map (LV . Glob) (take ar args)))))
186 _ -> do def <- mkLDecl n d
187 logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
190 | Just (ar, op) <- lookup n (idris_scprims i)
192 | Just ar <- lookup n (S.toList (idris_externs i))
193 = Just (ar, LExternal n)
194 getPrim n i = Nothing
196declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
197declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
199mkLDecl n (Function tm _)
200 = declArgs [] True n <$> irTerm M.empty [] tm
202mkLDecl n (CaseOp ci _ _ _ pats cd)
203 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc
205 (args, sc) = cases_runtime cd
207 -- Always attempt to inline functions arising from 'case' expressions
208 caseName (SN (CaseN _ _)) = True
209 caseName (SN (WithN _ _)) = True
210 caseName (NS n _) = caseName n
213mkLDecl n (TyDecl (DCon tag arity _) _) =
214 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
216mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
217mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
220 { viMethod :: Maybe Name
224type Vars = M.Map Name VarInfo
226irTerm :: Vars -> [Name] -> Term -> Idris LExp
227irTerm vs env tm@(App _ f a) = do
231 | m == txt "mkForeignPrim"
232 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
234 (P _ (UN u) _, [_, arg])
235 | u == txt "unsafePerformPrimIO"
238 -- TMP HACK - until we get inlining.
239 (P _ (UN r) _, [_, _, _, _, _, arg])
243 -- Laziness, the old way
244 (P _ (UN l) _, [_, arg])
246 -> error "lazy has crept in somehow"
248 (P _ (UN l) _, [_, arg])
250 -> LForce <$> irTerm vs env arg
252 -- Laziness, the new way
253 (P _ (UN l) _, [_, _, arg])
255 -> LLazyExp <$> irTerm vs env arg
257 (P _ (UN l) _, [_, _, arg])
259 -> LForce <$> irTerm vs env arg
261 (P _ (UN a) _, [_, _, _, arg])
262 | a == txt "assert_smaller"
265 (P _ (UN a) _, [_, arg])
266 | a == txt "assert_total"
269 (P _ (UN p) _, [_, arg])
271 -> do arg' <- irTerm vs env arg
272 return $ LOp LPar [LLazyExp arg']
274 (P _ (UN pf) _, [arg])
275 | pf == txt "prim_fork"
276 -> do arg' <- irTerm vs env arg
277 return $ LOp LFork [LLazyExp arg']
279 (P _ (UN m) _, [_,size,t])
283 (P _ (UN tm) _, [_,t])
284 | tm == txt "trace_malloc"
285 -> irTerm vs env t -- TODO
287 -- This case is here until we get more general inlining. It's just
288 -- a really common case, and the laziness hurts...
289 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
290 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
291 | be == txt "ifThenElse"
297 x' <- irTerm vs env x
298 t' <- irTerm vs env t
299 e' <- irTerm vs env e
300 return (LCase Shared x'
301 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
302 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
306 (P (DCon t arity _) n _, args) -> do
307 detag <- fgetState (opt_detaggable . ist_optimisation n)
308 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
310 let isNewtype = length used == 1 && detag
311 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
313 -- The following code removes fields from data constructors
314 -- and performs the newtype optimisation.
316 -- The general rule here is:
317 -- Everything we get as input is not touched by erasure,
318 -- so it conforms to the official arities and types
319 -- and we can reason about it like it's plain TT.
321 -- It's only the data that leaves this point that's erased
322 -- and possibly no longer typed as the original TT version.
324 -- Especially, underapplied constructors must yield functions
325 -- even if all the remaining arguments are erased
326 -- (the resulting function *will* be applied, to NULLs).
328 -- This will probably need rethinking when we get erasure from functions.
330 -- "padLams" will wrap our term in LLam-bdas and give us
331 -- the "list of future unerased args" coming from these lambdas.
333 -- We can do whatever we like with the list of unerased args,
334 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
335 let padLams = padLambdas used (length args) arity
337 case compare (length args) arity of
340 GT -> ifail ("overapplied data constructor: " ++ show tm)
344 -> irTerm vs env (head argsPruned)
346 | otherwise -- not newtype, plain data ctor
347 -> buildApp (LV $ Glob n) argsPruned
349 -- not saturated, underapplied
350 LT | isNewtype -- newtype
351 , length argsPruned == 1 -- and we already have the value
352 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
353 <$> irTerm vs env (head argsPruned)
355 | isNewtype -- newtype but the value is not among args yet
356 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
358 -- not a newtype, just apply to a constructor
360 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
363 (P (TCon t a) n _, args) -> return LNothing
365 -- an external name applied to arguments
366 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
367 LOp (LExternal n) <$> mapM (irTerm vs env) args
369 -- a name applied to arguments
370 (P _ n _, args) -> do
371 case lookup n (idris_scprims ist) of
372 -- if it's a primitive that is already saturated,
373 -- compile to the corresponding op here already to save work
374 Just (arity, op) | length args == arity
375 -> LOp op <$> mapM (irTerm vs env) args
377 -- otherwise, just apply the name
378 _ -> applyName n ist args
380 -- turn de bruijn vars into regular named references and try again
381 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
386 <*> mapM (irTerm vs env) args
389 buildApp :: LExp -> [Term] -> Idris LExp
390 buildApp e [] = return e
391 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
393 applyToNames :: LExp -> [Name] -> LExp
394 applyToNames tm [] = tm
395 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
397 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
398 padLambdas used startIdx endSIdx mkTerm
399 = LLam allNames $ mkTerm nonerasedNames
401 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
402 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
404 applyName :: Name -> IState -> [Term] -> Idris LExp
405 applyName n ist args =
406 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
409 | i >= arity || i `elem` used = x
412 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
413 Just (CaseOp ci ty tys def tot cdefs) -> length tys
414 Just (TyDecl (DCon tag ar _) _) -> ar
415 Just (TyDecl Ref ty) -> length $ getArgTys ty
416 Just (Operator ty ar op) -> ar
417 Just def -> error $ "unknown arity: " ++ show (n, def)
418 Nothing -> 0 -- no definition, probably local name => can't erase anything
420 -- name for purposes of usage info lookup
422 | Just n' <- viMethod =<< M.lookup n vs = n'
425 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
428irTerm vs env (P _ n _) = return $ LV (Glob n)
430 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
431 | otherwise = ifail $ "bad de bruijn index: " ++ show i
433irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
435 n' = uniqueName n env
437irTerm vs env (Bind n (Let _ v) sc)
438 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
440irTerm vs env (Bind _ _ _) = return $ LNothing
442irTerm vs env (Proj t (-1)) = do
443 t' <- irTerm vs env t
444 return $ LOp (LMinus (ATInt ITBig))
447irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
448irTerm vs env (Constant TheWorld) = return $ LNothing
449irTerm vs env (Constant c) = return $ LConst c
450irTerm vs env (TType _) = return $ LNothing
451irTerm vs env Erased = return $ LNothing
452irTerm vs env Impossible = return $ LNothing
454doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
455doForeign vs env (ret : fname : world : args)
456 = do args' <- mapM splitArg args
457 let fname' = toFDesc fname
458 let ret' = toFDesc ret
459 return $ LForeign ret' fname' args'
461 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
462 = do let l' = toFDesc l
463 r' <- irTerm vs env r
465 splitArg _ = ifail $ "Badly formed foreign function call"
467 toFDesc (Constant (Str str)) = FStr str
469 | (P _ n _, []) <- unApply tm = FCon (deNS n)
470 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
475doForeign vs env xs = ifail "Badly formed foreign function call"
477irTree :: [Name] -> SC -> Idris LExp
479 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
480 LLam args <$> irSC M.empty tree
482irSC :: Vars -> SC -> Idris LExp
483irSC vs (STerm t) = irTerm vs [] t
484irSC vs (UnmatchedCase str) = return $ LError str
486irSC vs (ProjCase tm alts) = do
487 tm' <- irTerm vs [] tm
488 alts' <- mapM (irAlt vs tm') alts
489 return $ LCase Shared tm' alts'
491-- Transform matching on Delay to applications of Force.
492irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
493 | delay == txt "Delay"
494 = do sc' <- irSC vs $ mkForce n' n sc
495 return $ LLet n' (LForce (LV (Glob n))) sc'
497-- There are two transformations in this case:
499-- 1. Newtype-case elimination:
501-- wrap({e1}) -> P({e1}) ==> P({e0})
503-- This is important because newtyped constructors are compiled away entirely
504-- and we need to do that everywhere.
506-- 2. Unused-case elimination (only valid for singleton branches):
508-- C(x,y) -> P[... x,y not used ...]
510-- This is important for runtime because sometimes we case on irrelevant data:
512-- In the example above, {e0} will most probably have been erased
513-- so this vain projection would make the resulting program segfault
514-- because the code generator still emits a PROJECT(...) G-machine instruction.
516-- Hence, we check whether the variables are used at all
517-- and erase the casesplit if they are not.
519irSC vs (Case up n [alt]) = do
520 replacement <- case alt of
521 ConCase cn a ns sc -> do
522 detag <- fgetState (opt_detaggable . ist_optimisation cn)
523 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
524 if detag && length used == 1
525 then return . Just $ substSC (ns !! head used) n sc
530 Just sc -> irSC vs sc
532 alt' <- irAlt vs (LV (Glob n)) alt
533 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
534 [] -> subexpr alt' -- strip the unused top-most case
535 _ -> LCase up (LV (Glob n)) [alt']
537 namesBoundIn :: LAlt -> [Name]
538 namesBoundIn (LConCase cn i ns sc) = ns
539 namesBoundIn (LConstCase c sc) = []
540 namesBoundIn (LDefaultCase sc) = []
542 subexpr :: LAlt -> LExp
543 subexpr (LConCase _ _ _ e) = e
544 subexpr (LConstCase _ e) = e
545 subexpr (LDefaultCase e) = e
547-- FIXME: When we have a non-singleton case-tree of the form
553-- and C is detaggable (the only constructor of the family), we can be sure
554-- that the first branch will be always taken -- so we add special handling
555-- to remove the dead default branch.
557-- If we don't do so and C is newtype-optimisable, we will miss this newtype
558-- transformation and the resulting code will probably segfault.
560-- This work-around is not entirely optimal; the best approach would be
561-- to ensure that such case trees don't arise in the first place.
563irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
564 detag <- fgetState (opt_detaggable . ist_optimisation cn)
566 then irSC vs (Case up n [ConCase cn a ns sc])
567 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
569irSC vs sc@(Case up n alts) = do
570 -- check that neither alternative needs the newtype optimisation,
572 goneWrong <- or <$> mapM isDetaggable alts
574 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
577 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
579 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
580 isDetaggable _ = return False
582irSC vs ImpossibleCase = return LNothing
584irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
586-- this leaves out all unused arguments of the constructor
587irAlt vs _ (ConCase n t args sc) = do
588 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
589 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
590 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
592 methodVars = case n of
593 SN (InstanceCtorN className)
594 -> M.fromList [(v, VI
595 { viMethod = Just $ mkFieldName n i
596 }) | (v,i) <- zip args [0..]]
598 -> M.empty -- not an instance constructor
600irAlt vs _ (ConstCase x rhs)
601 | matchable x = LConstCase x <$> irSC vs rhs
602 | matchableTy x = LDefaultCase <$> irSC vs rhs
604 matchable (I _) = True
605 matchable (BI _) = True
606 matchable (Ch _) = True
607 matchable (Str _) = True
608 matchable (B8 _) = True
609 matchable (B16 _) = True
610 matchable (B32 _) = True
611 matchable (B64 _) = True
614 matchableTy (AType (ATInt ITNative)) = True
615 matchableTy (AType (ATInt ITBig)) = True
616 matchableTy (AType (ATInt ITChar)) = True
617 matchableTy StrType = True
619 matchableTy (AType (ATInt (ITFixed IT8))) = True
620 matchableTy (AType (ATInt (ITFixed IT16))) = True
621 matchableTy (AType (ATInt (ITFixed IT32))) = True
622 matchableTy (AType (ATInt (ITFixed IT64))) = True
624 matchableTy _ = False
626irAlt vs tm (SucCase n rhs) = do
628 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
630 LConst (BI 1)]) rhs')
632irAlt vs _ (ConstCase c rhs)
633 = ifail $ "Can't match on (" ++ show c ++ ")"
635irAlt vs _ (DefaultCase rhs)
636 = LDefaultCase <$> irSC vs rhs
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list