1{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
3module IRTS.Compiler(compile, generate) where
7import IRTS.Defunctionalise
9import IRTS.CodegenCommon
12import IRTS.CodegenJavaScript
17import Idris.AbsSyntaxTree
26import Idris.Core.Evaluate
27import Idris.Core.CaseTree
29import Control.Category
30import Prelude hiding (id, (.))
32import Control.Applicative
33import Control.Monad.State
37import Data.IntSet (IntSet)
38import qualified Data.IntSet as IS
39import qualified Data.Map as M
40import qualified Data.Set as S
44import System.Directory
45import System.Environment
46import System.FilePath ((</>), addTrailingPathSeparator)
48-- | Compile to simplified forms and return CodegenInfo
49compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
51 = do checkMVs -- check for undefined metavariables
52 checkTotality -- refuse to compile if there are totality problems
53 exports <- findExports
54 let rootNames = case mtm of
58 reachableNames <- performUsageAnalysis
59 (rootNames ++ getExpNames exports)
60 maindef <- case mtm of
62 Just tm -> do md <- irMain tm
63 logCodeGen 1 $ "MAIN: " ++ show md
64 return [(sMN 0 "runMain", md)]
65 objs <- getObjectFiles codegen
66 libs <- getLibs codegen
67 flags <- getFlags codegen
68 hdrs <- getHdrs codegen
69 impdirs <- allImportDirs
70 defsIn <- mkDecls reachableNames
71 -- if no 'main term' given, generate interface files
72 let iface = case mtm of
76 let defs = defsIn ++ maindef
78 -- Inlined top level LDecl made here
79 let defsInlined = inlineAll defs
80 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
83 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)
84 let ctxtIn = addAlist tagged emptyContext
86 logCodeGen 1 "Defunctionalising"
87 let defuns_in = defunctionalise nexttag ctxtIn
88 logCodeGen 5 $ show defuns_in
89 logCodeGen 1 "Inlining"
90 let defuns = inline defuns_in
91 logCodeGen 5 $ show defuns
92 logCodeGen 1 "Resolving variables for CG"
94 let checked = simplifyDefs defuns (toAlist defuns)
96 dumpCases <- getDumpCases
97 dumpDefun <- getDumpDefun
100 Just f -> runIO $ writeFile f (showCaseTrees defs)
103 Just f -> runIO $ writeFile f (dumpDefuns defuns)
104 triple <- Idris.AbsSyntax.targetTriple
105 cpu <- Idris.AbsSyntax.targetCPU
106 logCodeGen 1 "Building output"
108 OK c -> do return $ CodegenInfo f outty triple cpu
109 hdrs impdirs objs libs flags
110 NONE c (toAlist defuns)
113 where checkMVs = do i <- getIState
114 case map fst (idris_metavars i) \\ primDefs of
116 ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
117 iputStrLn "\nEvaluation of any of these will crash at run time."
119 checkTotality = do i <- getIState
120 case idris_totcheckfail i of
122 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
124generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
125generate codegen mainmod ir
127 -- Built-in code generators (FIXME: lift these out!)
128 Via "c" -> codegenC ir
129 -- Any external code generator
130 Via cg -> do let cmd = "idris-codegen-" ++ cg
131 args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir
132 exit <- rawSystem cmd args
133 when (exit /= ExitSuccess) $
134 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
135 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
137irMain :: TT Name -> Idris LDecl
139 i <- irTerm M.empty [] tm
140 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
142mkDecls :: [Name] -> Idris [(Name, LDecl)]
145 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
146 decls <- mapM build ds
149showCaseTrees :: [(Name, LDecl)] -> String
150showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
152 showCT (n, LFun _ f args lexp)
153 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
155 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
157 defnRank :: (Name, LDecl) -> String
158 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
159 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
161 nameRank :: Name -> String
162 nameRank (UN s) = "1" ++ show s
163 nameRank (MN i s) = "2" ++ show s ++ show i
164 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
165 nameRank (SN sn) = "4" ++ snRank sn
166 nameRank n = "5" ++ show n
168 snRank :: SpecialName -> String
169 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
170 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
171 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
172 snRank (MethodN n) = "4" ++ nameRank n
173 snRank (CaseN _ n) = "5" ++ nameRank n
174 snRank (ElimN n) = "6" ++ nameRank n
175 snRank (InstanceCtorN n) = "7" ++ nameRank n
176 snRank (WithN i n) = "8" ++ nameRank n ++ show i
178isCon (TyDecl _ _) = True
181build :: (Name, Def) -> Idris (Name, LDecl)
186 let args = map (\x -> sMN x "op") [0..] in
187 return (n, (LFun [] n (take ar args)
188 (LOp op (map (LV . Glob) (take ar args)))))
189 _ -> do def <- mkLDecl n d
190 logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
193 | Just (ar, op) <- lookup n (idris_scprims i)
195 | Just ar <- lookup n (S.toList (idris_externs i))
196 = Just (ar, LExternal n)
197 getPrim n i = Nothing
199declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
200declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
202mkLDecl n (Function tm _)
203 = declArgs [] True n <$> irTerm M.empty [] tm
205mkLDecl n (CaseOp ci _ _ _ pats cd)
206 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc
208 (args, sc) = cases_runtime cd
210 -- Always attempt to inline functions arising from 'case' expressions
211 caseName (SN (CaseN _ _)) = True
212 caseName (SN (WithN _ _)) = True
213 caseName (NS n _) = caseName n
216mkLDecl n (TyDecl (DCon tag arity _) _) =
217 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
219mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
220mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
223 { viMethod :: Maybe Name
227type Vars = M.Map Name VarInfo
229irTerm :: Vars -> [Name] -> Term -> Idris LExp
230irTerm vs env tm@(App _ f a) = do
234 | n `elem` map fst (idris_metavars ist) \\ primDefs
235 -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
237 | m == txt "mkForeignPrim"
238 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
240 (P _ (UN u) _, [_, arg])
241 | u == txt "unsafePerformPrimIO"
244 -- TMP HACK - until we get inlining.
245 (P _ (UN r) _, [_, _, _, _, _, arg])
249 -- Laziness, the old way
250 (P _ (UN l) _, [_, arg])
252 -> error "lazy has crept in somehow"
254 (P _ (UN l) _, [_, arg])
256 -> LForce <$> irTerm vs env arg
258 -- Laziness, the new way
259 (P _ (UN l) _, [_, _, arg])
261 -> LLazyExp <$> irTerm vs env arg
263 (P _ (UN l) _, [_, _, arg])
265 -> LForce <$> irTerm vs env arg
267 (P _ (UN a) _, [_, _, _, arg])
268 | a == txt "assert_smaller"
271 (P _ (UN a) _, [_, arg])
272 | a == txt "assert_total"
275 (P _ (UN p) _, [_, arg])
277 -> do arg' <- irTerm vs env arg
278 return $ LOp LPar [LLazyExp arg']
280 (P _ (UN pf) _, [arg])
281 | pf == txt "prim_fork"
282 -> do arg' <- irTerm vs env arg
283 return $ LOp LFork [LLazyExp arg']
285 (P _ (UN m) _, [_,size,t])
289 (P _ (UN tm) _, [_,t])
290 | tm == txt "trace_malloc"
291 -> irTerm vs env t -- TODO
293 -- This case is here until we get more general inlining. It's just
294 -- a really common case, and the laziness hurts...
295 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
296 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
297 | be == txt "ifThenElse"
303 x' <- irTerm vs env x
304 t' <- irTerm vs env t
305 e' <- irTerm vs env e
306 return (LCase Shared x'
307 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
308 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
312 (P (DCon t arity _) n _, args) -> do
313 detag <- fgetState (opt_detaggable . ist_optimisation n)
314 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
316 let isNewtype = length used == 1 && detag
317 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
319 -- The following code removes fields from data constructors
320 -- and performs the newtype optimisation.
322 -- The general rule here is:
323 -- Everything we get as input is not touched by erasure,
324 -- so it conforms to the official arities and types
325 -- and we can reason about it like it's plain TT.
327 -- It's only the data that leaves this point that's erased
328 -- and possibly no longer typed as the original TT version.
330 -- Especially, underapplied constructors must yield functions
331 -- even if all the remaining arguments are erased
332 -- (the resulting function *will* be applied, to NULLs).
334 -- This will probably need rethinking when we get erasure from functions.
336 -- "padLams" will wrap our term in LLam-bdas and give us
337 -- the "list of future unerased args" coming from these lambdas.
339 -- We can do whatever we like with the list of unerased args,
340 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
341 let padLams = padLambdas used (length args) arity
343 case compare (length args) arity of
346 GT -> ifail ("overapplied data constructor: " ++ show tm ++
348 "Arity: " ++ show arity ++ "\n" ++
349 "Arguments: " ++ show args ++ "\n" ++
350 "Pruned arguments: " ++ show argsPruned)
354 -> irTerm vs env (head argsPruned)
356 | otherwise -- not newtype, plain data ctor
357 -> buildApp (LV $ Glob n) argsPruned
359 -- not saturated, underapplied
360 LT | isNewtype -- newtype
361 , length argsPruned == 1 -- and we already have the value
362 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
363 <$> irTerm vs env (head argsPruned)
365 | isNewtype -- newtype but the value is not among args yet
366 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
368 -- not a newtype, just apply to a constructor
370 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
373 (P (TCon t a) n _, args) -> return LNothing
375 -- an external name applied to arguments
376 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
377 LOp (LExternal n) <$> mapM (irTerm vs env) args
379 -- a name applied to arguments
380 (P _ n _, args) -> do
381 case lookup n (idris_scprims ist) of
382 -- if it's a primitive that is already saturated,
383 -- compile to the corresponding op here already to save work
384 Just (arity, op) | length args == arity
385 -> LOp op <$> mapM (irTerm vs env) args
387 -- otherwise, just apply the name
388 _ -> applyName n ist args
390 -- turn de bruijn vars into regular named references and try again
391 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
396 <*> mapM (irTerm vs env) args
399 buildApp :: LExp -> [Term] -> Idris LExp
400 buildApp e [] = return e
401 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
403 applyToNames :: LExp -> [Name] -> LExp
404 applyToNames tm [] = tm
405 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
407 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
408 padLambdas used startIdx endSIdx mkTerm
409 = LLam allNames $ mkTerm nonerasedNames
411 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
412 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
414 applyName :: Name -> IState -> [Term] -> Idris LExp
415 applyName n ist args =
416 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
419 | i >= arity || i `elem` used = x
422 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
423 Just (CaseOp ci ty tys def tot cdefs) -> length tys
424 Just (TyDecl (DCon tag ar _) _) -> ar
425 Just (TyDecl Ref ty) -> length $ getArgTys ty
426 Just (Operator ty ar op) -> ar
427 Just def -> error $ "unknown arity: " ++ show (n, def)
428 Nothing -> 0 -- no definition, probably local name => can't erase anything
430 -- name for purposes of usage info lookup
432 | Just n' <- viMethod =<< M.lookup n vs = n'
435 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
438irTerm vs env (P _ n _) = return $ LV (Glob n)
440 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
441 | otherwise = ifail $ "bad de bruijn index: " ++ show i
443irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
445 n' = uniqueName n env
447irTerm vs env (Bind n (Let _ v) sc)
448 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
450irTerm vs env (Bind _ _ _) = return $ LNothing
452irTerm vs env (Proj t (-1)) = do
453 t' <- irTerm vs env t
454 return $ LOp (LMinus (ATInt ITBig))
457irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
458irTerm vs env (Constant TheWorld) = return $ LNothing
459irTerm vs env (Constant c) = return $ LConst c
460irTerm vs env (TType _) = return $ LNothing
461irTerm vs env Erased = return $ LNothing
462irTerm vs env Impossible = return $ LNothing
464doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
465doForeign vs env (ret : fname : world : args)
466 = do args' <- mapM splitArg args
467 let fname' = toFDesc fname
468 let ret' = toFDesc ret
469 return $ LForeign ret' fname' args'
471 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
472 = do let l' = toFDesc l
473 r' <- irTerm vs env r
475 splitArg _ = ifail $ "Badly formed foreign function call"
477 toFDesc (Constant (Str str)) = FStr str
479 | (P _ n _, []) <- unApply tm = FCon (deNS n)
480 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
485doForeign vs env xs = ifail "Badly formed foreign function call"
487irTree :: [Name] -> SC -> Idris LExp
489 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
490 LLam args <$> irSC M.empty tree
492irSC :: Vars -> SC -> Idris LExp
493irSC vs (STerm t) = irTerm vs [] t
494irSC vs (UnmatchedCase str) = return $ LError str
496irSC vs (ProjCase tm alts) = do
497 tm' <- irTerm vs [] tm
498 alts' <- mapM (irAlt vs tm') alts
499 return $ LCase Shared tm' alts'
501-- Transform matching on Delay to applications of Force.
502irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
503 | delay == txt "Delay"
504 = do sc' <- irSC vs $ mkForce n' n sc
505 return $ LLet n' (LForce (LV (Glob n))) sc'
507-- There are two transformations in this case:
509-- 1. Newtype-case elimination:
511-- wrap({e1}) -> P({e1}) ==> P({e0})
513-- This is important because newtyped constructors are compiled away entirely
514-- and we need to do that everywhere.
516-- 2. Unused-case elimination (only valid for singleton branches):
518-- C(x,y) -> P[... x,y not used ...]
520-- This is important for runtime because sometimes we case on irrelevant data:
522-- In the example above, {e0} will most probably have been erased
523-- so this vain projection would make the resulting program segfault
524-- because the code generator still emits a PROJECT(...) G-machine instruction.
526-- Hence, we check whether the variables are used at all
527-- and erase the casesplit if they are not.
529irSC vs (Case up n [alt]) = do
530 replacement <- case alt of
531 ConCase cn a ns sc -> do
532 detag <- fgetState (opt_detaggable . ist_optimisation cn)
533 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
534 if detag && length used == 1
535 then return . Just $ substSC (ns !! head used) n sc
540 Just sc -> irSC vs sc
542 alt' <- irAlt vs (LV (Glob n)) alt
543 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
544 [] -> subexpr alt' -- strip the unused top-most case
545 _ -> LCase up (LV (Glob n)) [alt']
547 namesBoundIn :: LAlt -> [Name]
548 namesBoundIn (LConCase cn i ns sc) = ns
549 namesBoundIn (LConstCase c sc) = []
550 namesBoundIn (LDefaultCase sc) = []
552 subexpr :: LAlt -> LExp
553 subexpr (LConCase _ _ _ e) = e
554 subexpr (LConstCase _ e) = e
555 subexpr (LDefaultCase e) = e
557-- FIXME: When we have a non-singleton case-tree of the form
563-- and C is detaggable (the only constructor of the family), we can be sure
564-- that the first branch will be always taken -- so we add special handling
565-- to remove the dead default branch.
567-- If we don't do so and C is newtype-optimisable, we will miss this newtype
568-- transformation and the resulting code will probably segfault.
570-- This work-around is not entirely optimal; the best approach would be
571-- to ensure that such case trees don't arise in the first place.
573irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
574 detag <- fgetState (opt_detaggable . ist_optimisation cn)
576 then irSC vs (Case up n [ConCase cn a ns sc])
577 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
579irSC vs sc@(Case up n alts) = do
580 -- check that neither alternative needs the newtype optimisation,
582 goneWrong <- or <$> mapM isDetaggable alts
584 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
587 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
589 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
590 isDetaggable _ = return False
592irSC vs ImpossibleCase = return LNothing
594irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
596-- this leaves out all unused arguments of the constructor
597irAlt vs _ (ConCase n t args sc) = do
598 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
599 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
600 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
602 methodVars = case n of
603 SN (InstanceCtorN className)
604 -> M.fromList [(v, VI
605 { viMethod = Just $ mkFieldName n i
606 }) | (v,i) <- zip args [0..]]
608 -> M.empty -- not an instance constructor
610irAlt vs _ (ConstCase x rhs)
611 | matchable x = LConstCase x <$> irSC vs rhs
612 | matchableTy x = LDefaultCase <$> irSC vs rhs
614 matchable (I _) = True
615 matchable (BI _) = True
616 matchable (Ch _) = True
617 matchable (Str _) = True
618 matchable (B8 _) = True
619 matchable (B16 _) = True
620 matchable (B32 _) = True
621 matchable (B64 _) = True
624 matchableTy (AType (ATInt ITNative)) = True
625 matchableTy (AType (ATInt ITBig)) = True
626 matchableTy (AType (ATInt ITChar)) = True
627 matchableTy StrType = True
629 matchableTy (AType (ATInt (ITFixed IT8))) = True
630 matchableTy (AType (ATInt (ITFixed IT16))) = True
631 matchableTy (AType (ATInt (ITFixed IT32))) = True
632 matchableTy (AType (ATInt (ITFixed IT64))) = True
634 matchableTy _ = False
636irAlt vs tm (SucCase n rhs) = do
638 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
640 LConst (BI 1)]) rhs')
642irAlt vs _ (ConstCase c rhs)
643 = ifail $ "Can't match on (" ++ show c ++ ")"
645irAlt vs _ (DefaultCase rhs)
646 = 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