git.iko.soy/Idris-dev
on c8f7604 help sign in
Idris-dev/src/IRTS/Compiler.hs
805 lines 30 kB history raw
1{-|
2Module : IRTS.Compiler
3Description : Coordinates the compilation process.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, NamedFieldPuns, PatternGuards,
9 TypeSynonymInstances #-}
11module IRTS.Compiler(compile, generate) where
13import Idris.AbsSyntax
14import Idris.ASTUtils
15import Idris.Core.CaseTree
16import Idris.Core.Evaluate
17import Idris.Core.TT
18import Idris.Erasure
19import Idris.Error
20import Idris.Options
21import Idris.Output
22import IRTS.CodegenC
23import IRTS.CodegenCommon
24import IRTS.Defunctionalise
25import IRTS.DumpBC
26import IRTS.Exports
27import IRTS.Inliner
28import IRTS.LangOpts
29import IRTS.Portable
30import IRTS.Simplified
32import Prelude hiding (id, (.))
34import Control.Category
35import Control.Monad.State
36import Data.List
37import qualified Data.Map as M
38import Data.Maybe (maybe)
39import Data.Ord
40import qualified Data.Set as S
41import System.Directory
42import System.Exit
43import System.IO
44import System.Process
46-- | Compile to simplified forms and return CodegenInfo
47compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
48compile codegen f mtm = do
49 logCodeGen 1 "Compiling Output."
50 iReport 2 "Compiling Output."
51 checkMVs -- check for undefined metavariables
52 checkTotality -- refuse to compile if there are totality problems
53 exports <- findExports
54 let rootNames = case mtm of
55 Nothing -> []
56 Just t -> freeNames t
58 logCodeGen 1 "Running Erasure Analysis"
59 iReport 3 "Running Erasure Analysis"
60 reachableNames <- performUsageAnalysis
61 (rootNames ++ getExpNames exports)
62 maindef <- case mtm of
63 Nothing -> return []
64 Just tm -> do md <- irMain tm
65 logCodeGen 1 $ "MAIN: " ++ show md
66 return [(sMN 0 "runMain", md)]
67 objs <- getObjectFiles codegen
68 libs <- getLibs codegen
69 flags <- getFlags codegen
70 hdrs <- getHdrs codegen
71 impdirs <- rankedImportDirs f
72 ttDeclarations <- getDeclarations reachableNames
73 defsIn <- mkDecls reachableNames
74 -- if no 'main term' given, generate interface files
75 let iface = case mtm of
76 Nothing -> True
77 Just _ -> False
79 let defs = defsIn ++ maindef
81 -- Inlined top level LDecl made here
82 let defsInlined = inlineAll defs
83 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
84 defsInlined
86 logCodeGen 1 "Inlining"
88 dumpCases <- getDumpCases
89 case dumpCases of
90 Nothing -> return ()
91 Just f -> runIO $ writeFile f (showCaseTrees defsUniq)
93 let (nexttag, tagged) = addTags 65536 (liftAll defsInlined)
94 let ctxtIn = addAlist tagged emptyContext
96 logCodeGen 1 "Defunctionalising"
97 iReport 3 "Defunctionalising"
98 let defuns_in = defunctionalise nexttag ctxtIn
99 logCodeGen 5 $ show defuns_in
100 logCodeGen 1 "Inlining"
101 iReport 3 "Inlining"
102 let defuns = inline defuns_in
103 logCodeGen 5 $ show defuns
104 logCodeGen 1 "Resolving variables for CG"
106 let checked = simplifyDefs defuns (toAlist defuns)
107 outty <- outputTy
108 dumpDefun <- getDumpDefun
109 case dumpDefun of
110 Nothing -> return ()
111 Just f -> runIO $ writeFile f (dumpDefuns defuns)
112 triple <- Idris.AbsSyntax.targetTriple
113 cpu <- Idris.AbsSyntax.targetCPU
114 logCodeGen 1 "Generating Code."
115 iReport 2 "Generating Code."
116 case checked of
117 OK c -> do return $ CodegenInfo f outty triple cpu
118 hdrs impdirs objs libs flags
119 NONE c (toAlist defuns)
120 tagged iface exports
121 ttDeclarations
122 Error e -> ierror e
123 where checkMVs = do i <- getIState
124 case map fst (idris_metavars i) \\ primDefs of
125 [] -> return ()
126 ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
127 iputStrLn "\nEvaluation of any of these will crash at run time."
128 return ()
129 checkTotality = do i <- getIState
130 case idris_totcheckfail i of
131 [] -> return ()
132 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
134generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
135generate codegen mainmod ir
136 = case codegen of
137 -- Built-in code generators (FIXME: lift these out!)
138 Via _ "c" -> codegenC ir
139 -- Any external code generator
140 Via fm cg -> do input <- case fm of
141 IBCFormat -> return mainmod
142 JSONFormat -> do
143 tempdir <- getTemporaryDirectory
144 (fn, h) <- openTempFile tempdir "idris-cg.json"
145 writePortable h ir
146 hClose h
147 return fn
148 let cmd = "idris-codegen-" ++ cg
149 args = [input, "-o", outputFile ir] ++ compilerFlags ir
150 exit <- rawSystem cmd (if interfaces ir then "--interface" : args else args)
151 when (exit /= ExitSuccess) $
152 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
153 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
155irMain :: TT Name -> Idris LDecl
156irMain tm = do
157 i <- irTerm (sMN 0 "runMain") M.empty [] tm
158 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
160mkDecls :: [Name] -> Idris [(Name, LDecl)]
161mkDecls used
162 = do i <- getIState
163 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
164 decls <- mapM build ds
165 return decls
167getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
168getDeclarations used
169 = do i <- getIState
170 let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)
171 return ds
173showCaseTrees :: [(Name, LDecl)] -> String
174showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
175 where
176 showCT (n, LFun opts f args lexp)
177 = showOpts ++
178 show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
179 ++ show lexp
180 where
181 showOpts | Inline `elem` opts = "%inline "
182 | otherwise = ""
183 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
185 defnRank :: (Name, LDecl) -> String
186 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
187 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
189 nameRank :: Name -> String
190 nameRank (UN s) = "1" ++ show s
191 nameRank (MN i s) = "2" ++ show s ++ show i
192 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
193 nameRank (SN sn) = "4" ++ snRank sn
194 nameRank n = "5" ++ show n
196 snRank :: SpecialName -> String
197 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
198 snRank (ImplementationN n args) = "2" ++ nameRank n ++ concatMap show args
199 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
200 snRank (MethodN n) = "4" ++ nameRank n
201 snRank (CaseN _ n) = "5" ++ nameRank n
202 snRank (ImplementationCtorN n) = "7" ++ nameRank n
203 snRank (WithN i n) = "8" ++ nameRank n ++ show i
205isCon (TyDecl _ _) = True
206isCon _ = False
208build :: (Name, Def) -> Idris (Name, LDecl)
209build (n, d)
210 = do i <- getIState
211 case getPrim n i of
212 Just (ar, op) ->
213 let args = map (\x -> sMN x "op") [0..] in
214 return (n, (LFun [] n (take ar args)
215 (LOp op (map LV (take ar args)))))
216 _ -> do def <- mkLDecl n d
217 logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
218 return (n, def)
219 where getPrim n i
220 | Just (ar, op) <- lookup n (idris_scprims i)
221 = Just (ar, op)
222 | Just ar <- lookup n (S.toList (idris_externs i))
223 = Just (ar, LExternal n)
224 getPrim n i = Nothing
226declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
227declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
229mkLDecl n (Function tm _)
230 = declArgs [] True n <$> irTerm n M.empty [] tm
232mkLDecl n (CaseOp ci _ _ _ pats cd)
233 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree n args sc
234 where
235 (args, sc) = cases_runtime cd
237 -- Always attempt to inline functions arising from 'case' expressions
238 caseName (SN (CaseN _ _)) = True
239 caseName (SN (WithN _ _)) = True
240 caseName (NS n _) = caseName n
241 caseName _ = False
243mkLDecl n (TyDecl (DCon tag arity _) _) =
244 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
246mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
247mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
249data VarInfo = VI
250 { viMethod :: Maybe Name
251 }
252 deriving Show
254type Vars = M.Map Name VarInfo
256irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
257irTerm top vs env tm@(App _ f a) = do
258 ist <- getIState
259 case unApply tm of
260 (P _ n _, args)
261 | n `elem` map fst (idris_metavars ist) \\ primDefs
262 -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
263 (P _ (UN m) _, args)
264 | m == txt "mkForeignPrim"
265 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
267 (P _ (UN u) _, [_, arg])
268 | u == txt "unsafePerformPrimIO"
269 -> irTerm top vs env arg
271 (P _ (UN u) _, _)
272 | u == txt "assert_unreachable"
273 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top
275 (P _ (UN u) _, [_, msg])
276 | u == txt "idris_crash"
277 -> do msg' <- irTerm top vs env msg
278 return $ LOp LCrash [msg']
280 -- TMP HACK - until we get inlining.
281 (P _ (UN r) _, [_, _, _, _, _, arg])
282 | r == txt "replace"
283 -> irTerm top vs env arg
285 -- 'void' doesn't have any pattern clauses and only gets called on
286 -- erased things in higher order contexts (also a TMP HACK...)
287 (P _ (UN r) _, _)
288 | r == txt "void"
289 -> return LNothing
291 -- Laziness, the old way
292 (P _ (UN l) _, [_, arg])
293 | l == txt "lazy"
294 -> error "lazy has crept in somehow"
296 (P _ (UN l) _, [_, arg])
297 | l == txt "force"
298 -> LForce <$> irTerm top vs env arg
300 -- Laziness, the new way
301 (P _ (UN l) _, [_, _, arg])
302 | l == txt "Delay"
303 -> LLazyExp <$> irTerm top vs env arg
305 (P _ (UN l) _, [_, _, arg])
306 | l == txt "Force"
307 -> LForce <$> irTerm top vs env arg
309 (P _ (UN a) _, [_, _, _, arg])
310 | a == txt "assert_smaller"
311 -> irTerm top vs env arg
313 (P _ (UN a) _, [_, arg])
314 | a == txt "assert_total"
315 -> irTerm top vs env arg
317 (P _ (UN p) _, [_, arg])
318 | p == txt "par"
319 -> do arg' <- irTerm top vs env arg
320 return $ LOp LPar [LLazyExp arg']
322 (P _ (UN pf) _, [arg])
323 | pf == txt "prim_fork"
324 -> do arg' <- irTerm top vs env arg
325 return $ LOp LFork [LLazyExp arg']
327 (P _ (UN m) _, [_,size,t])
328 | m == txt "malloc"
329 -> irTerm top vs env t
331 (P _ (UN tm) _, [_,t])
332 | tm == txt "trace_malloc"
333 -> irTerm top vs env t -- TODO
335 -- This case is here until we get more general inlining. It's just
336 -- a really common case, and the laziness hurts...
337 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
338 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
339 | be == txt "ifThenElse"
340 , d == txt "Delay"
341 , d' == txt "Delay"
342 , b == txt "Bool"
343 , p == txt "Prelude"
344 -> do
345 x' <- irTerm top vs env x
346 t' <- irTerm top vs env t
347 e' <- irTerm top vs env e
348 return (LCase Shared x'
349 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
350 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
351 ])
353 -- data constructor
354 (P (DCon t arity _) n _, args) -> do
355 detag <- fgetState (opt_detaggable . ist_optimisation n)
356 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
358 let isNewtype = length used == 1 && detag
359 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
361 -- The following code removes fields from data constructors
362 -- and performs the newtype optimisation.
363 --
364 -- The general rule here is:
365 -- Everything we get as input is not touched by erasure,
366 -- so it conforms to the official arities and types
367 -- and we can reason about it like it's plain TT.
368 --
369 -- It's only the data that leaves this point that's erased
370 -- and possibly no longer typed as the original TT version.
371 --
372 -- Especially, underapplied constructors must yield functions
373 -- even if all the remaining arguments are erased
374 -- (the resulting function *will* be applied, to NULLs).
375 --
376 -- This will probably need rethinking when we get erasure from functions.
378 -- "padLams" will wrap our term in LLam-bdas and give us
379 -- the "list of future unerased args" coming from these lambdas.
380 --
381 -- We can do whatever we like with the list of unerased args,
382 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
383 let padLams = padLambdas used (length args) arity
385 case compare (length args) arity of
387 -- overapplied
388 GT -> ifail ("overapplied data constructor: " ++ show tm ++
389 "\nDEBUG INFO:\n" ++
390 "Arity: " ++ show arity ++ "\n" ++
391 "Arguments: " ++ show args ++ "\n" ++
392 "Pruned arguments: " ++ show argsPruned)
394 -- exactly saturated
395 EQ | isNewtype
396 -> irTerm top vs env (head argsPruned)
398 -- compile Nat-likes as bigints
399 | Just LikeZ <- isLikeNat ist n
400 -> irTerm top vs env $ Constant (BI 0)
402 -- compile Nat-likes as bigints
403 | Just LikeS <- isLikeNat ist n
404 -> irTerm top vs env $ mkApp
405 (P Ref (sUN "prim__addBigInt") Erased)
406 (Constant (BI 1) : argsPruned)
408 | otherwise -- not newtype, plain data ctor
409 -> buildApp (LV n) argsPruned
411 -- not saturated, underapplied
412 LT | isNewtype -- newtype
413 , length argsPruned == 1 -- and we already have the value
414 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
415 <$> irTerm top vs env (head argsPruned)
417 | isNewtype -- newtype but the value is not among args yet
418 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
420 -- compile Nat-likes as bigints
421 -- it seems that prim applications needn't be saturated
422 | Just LikeS <- isLikeNat ist n
423 -> irTerm top vs env $
424 App Complete
425 (P Ref (sUN "prim__addBigInt") Erased)
426 (Constant $ BI 1)
428 -- not a newtype, just apply to a constructor
429 | otherwise
430 -> padLams . applyToNames <$> buildApp (LV n) argsPruned
432 -- type constructor
433 (P (TCon t a) n _, args) -> return LNothing
435 -- an external name applied to arguments
436 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
437 LOp (LExternal n) <$> mapM (irTerm top vs env) args
439 -- a name applied to arguments
440 (P _ n _, args) -> do
441 case lookup n (idris_scprims ist) of
442 -- if it's a primitive that is already saturated,
443 -- compile to the corresponding op here already to save work
444 Just (arity, op) | length args == arity
445 -> LOp op <$> mapM (irTerm top vs env) args
447 -- otherwise, just apply the name
448 _ -> applyName n ist args
450 -- turn de bruijn vars into regular named references and try again
451 (V i, args) -> irTerm top vs env $ mkApp (P Bound (env !! i) Erased) args
453 (f, args)
454 -> LApp False
455 <$> irTerm top vs env f
456 <*> mapM (irTerm top vs env) args
458 where
459 buildApp :: LExp -> [Term] -> Idris LExp
460 buildApp e [] = return e
461 buildApp e xs = LApp False e <$> mapM (irTerm top vs env) xs
463 applyToNames :: LExp -> [Name] -> LExp
464 applyToNames tm [] = tm
465 applyToNames tm ns = LApp False tm $ map LV ns
467 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
468 padLambdas used startIdx endSIdx mkTerm
469 = LLam allNames $ mkTerm nonerasedNames
470 where
471 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
472 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
474 applyName :: Name -> IState -> [Term] -> Idris LExp
475 applyName n ist args =
476 LApp False (LV n) <$> mapM (irTerm top vs env . erase) (zip [0..] args)
477 where
478 erase (i, x)
479 | i >= arity || i `elem` used = x
480 | otherwise = Erased
482 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
483 Just (CaseOp ci ty tys def tot cdefs) -> length tys
484 Just (TyDecl (DCon tag ar _) _) -> ar
485 Just (TyDecl Ref ty) -> length $ getArgTys ty
486 Just (Operator ty ar op) -> ar
487 Just def -> error $ "unknown arity: " ++ show (n, def)
488 Nothing -> 0 -- no definition, probably local name => can't erase anything
490 -- name for purposes of usage info lookup
491 uName
492 | Just n' <- viMethod =<< M.lookup n vs = n'
493 | otherwise = n
495 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
496 fst4 (x,_,_,_,_,_) = x
498irTerm top vs env (P _ n _) = return $ LV n
499irTerm top vs env (V i)
500 | i >= 0 && i < length env = return $ LV (env!!i)
501 | otherwise = ifail $ "bad de bruijn index: " ++ show i
503irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
504 where
505 n' = uniqueName n env
507irTerm top vs env (Bind n (Let _ _ v) sc)
508 = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc
510irTerm top vs env (Bind _ _ _) = return $ LNothing
512irTerm top vs env (Proj t (-1)) = do
513 t' <- irTerm top vs env t
514 return $ LOp (LMinus (ATInt ITBig))
515 [t', LConst (BI 1)]
517irTerm top vs env (Proj t i) = LProj <$> irTerm top vs env t <*> pure i
518irTerm top vs env (Constant TheWorld) = return LNothing
519irTerm top vs env (Constant c) = return (LConst c)
520irTerm top vs env (TType _) = return LNothing
521irTerm top vs env Erased = return LNothing
522irTerm top vs env Impossible = return LNothing
524data LikeNat = LikeZ | LikeS
526isLikeNat :: IState -> Name -> Maybe LikeNat
527isLikeNat ist cn
528 -- Nat itself is special-cased in Idris/DataOpts.hs,
529 -- which will have already happened at this point.
531 -- If the optimisation is disabled then nothing looks like Nat.
532 | GeneralisedNatHack `notElem` opt_optimise (idris_options ist)
533 = Nothing
535 | Just cTy <- lookupTyExact cn $ tt_ctxt ist
536 , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
537 , Just (z, s) <- natLikeCtors tyN
538 = if | cn == z -> Just LikeZ
539 | cn == s -> Just LikeS
540 | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)
542 | otherwise = Nothing
543 where
544 natLikeCtors :: Name -> Maybe (Name, Name)
545 natLikeCtors tyN = case lookupCtxtExact tyN $ idris_datatypes ist of
546 Just TI{con_names = [z, s]}
547 | 0 <- getUsedCount z
548 , looksLikeS s
549 -> Just (z, s)
551 Just TI{con_names = [s, z]}
552 | 0 <- getUsedCount z
553 , looksLikeS s
554 -> Just (z, s)
556 _ -> Nothing
558 getUsedCount :: Name -> Int
559 getUsedCount n =
560 maybe 0 (length . usedpos)
561 $ lookupCtxtExact n
562 $ idris_callgraph ist
564 looksLikeS :: Name -> Bool
565 looksLikeS cn
566 | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist
567 , Just cTy <- lookupTyExact cn $ tt_ctxt ist
568 , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]
569 , (P TCon{} recTyN _, _) <- unApply recTy
570 , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
571 , recTyN == tyN
572 = True
574 | otherwise = False
576doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
577doForeign vs env (ret : fname : world : args)
578 = do args' <- mapM splitArg args
579 let fname' = toFDesc fname
580 let ret' = toFDesc ret
581 return $ LForeign ret' fname' args'
582 where
583 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
584 = do let l' = toFDesc l
585 r' <- irTerm (sMN 0 "__foreignCall") vs env r
586 return (l', r')
587 splitArg _ = ifail $ "Badly formed foreign function call: " ++
588 show (ret : fname : world : args)
591 toFDesc (Constant (Str str)) = FStr str
592 toFDesc tm
593 | (P _ n _, []) <- unApply tm = FCon (deNS n)
594 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
595 toFDesc _ = FUnknown
597 deNS (NS n _) = n
598 deNS n = n
599doForeign vs env xs = ifail "Badly formed foreign function call"
601irTree :: Name -> [Name] -> SC -> Idris LExp
602irTree top args tree = do
603 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
604 LLam args <$> irSC top M.empty tree
606irSC :: Name -> Vars -> SC -> Idris LExp
607irSC top vs (STerm t) = irTerm top vs [] t
608irSC top vs (UnmatchedCase str) = return $ LError str
610irSC top vs (ProjCase tm alts) = do
611 tm' <- irTerm top vs [] tm
612 alts' <- mapM (irAlt top vs tm') alts
613 return $ LCase Shared tm' alts'
615-- Transform matching on Delay to applications of Force.
616irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
617 | delay == txt "Delay"
618 = do sc' <- irSC top vs sc -- mkForce n' n sc
619 return $ lsubst n' (LForce (LV n)) sc'
621-- There are two transformations in this case:
622--
623-- 1. Newtype-case elimination:
624-- case {e0} of
625-- wrap({e1}) -> P({e1}) ==> P({e0})
626--
627-- This is important because newtyped constructors are compiled away entirely
628-- and we need to do that everywhere.
629--
630-- 2. Unused-case elimination (only valid for singleton branches):
631-- case {e0} of ==> P
632-- C(x,y) -> P[... x,y not used ...]
633--
634-- This is important for runtime because sometimes we case on irrelevant data:
635--
636-- In the example above, {e0} will most probably have been erased
637-- so this vain projection would make the resulting program segfault
638-- because the code generator still emits a PROJECT(...) G-machine instruction.
639--
640-- Hence, we check whether the variables are used at all
641-- and erase the casesplit if they are not.
642--
643irSC top vs (Case up n [alt]) = do
644 replacement <- case alt of
645 ConCase cn a ns sc -> do
646 detag <- fgetState (opt_detaggable . ist_optimisation cn)
647 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
648 if detag && length used == 1
649 then return . Just $ substSC (ns !! head used) n sc
650 else return Nothing
651 _ -> return Nothing
653 case replacement of
654 Just sc -> irSC top vs sc
655 _ -> do
656 alt' <- irAlt top vs (LV n) alt
657 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
658 [] -> subexpr alt' -- strip the unused top-most case
659 _ -> LCase up (LV n) [alt']
660 where
661 namesBoundIn :: LAlt -> [Name]
662 namesBoundIn (LConCase cn i ns sc) = ns
663 namesBoundIn (LConstCase c sc) = []
664 namesBoundIn (LDefaultCase sc) = []
666 subexpr :: LAlt -> LExp
667 subexpr (LConCase _ _ _ e) = e
668 subexpr (LConstCase _ e) = e
669 subexpr (LDefaultCase e) = e
671-- FIXME: When we have a non-singleton case-tree of the form
672--
673-- case {e0} of
674-- C(x) => ...
675-- ... => ...
676--
677-- and C is detaggable (the only constructor of the family), we can be sure
678-- that the first branch will be always taken -- so we add special handling
679-- to remove the dead default branch.
680--
681-- If we don't do so and C is newtype-optimisable, we will miss this newtype
682-- transformation and the resulting code will probably segfault.
683--
684-- This work-around is not entirely optimal; the best approach would be
685-- to ensure that such case trees don't arise in the first place.
686--
687irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
688 detag <- fgetState (opt_detaggable . ist_optimisation cn)
689 if detag
690 then irSC top vs (Case up n [ConCase cn a ns sc])
691 else do
692 likeNat <- isLikeNat <$> getIState <*> pure cn
693 case likeNat of
694 -- the annoying case: LikeS is translated into a default case
695 -- so we need to change the original DefaultCase to Z-case
696 -- and reorder it before this one
697 Just LikeS -> do
698 zCase <- LConstCase (BI 0) <$> irSC top vs sc'
699 sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)
700 return $ LCase up (LV n) [zCase, sCase]
702 -- the usual case
703 _ -> LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
705irSC top vs sc@(Case up n alts) = getIState >>= rhs
706 where
707 rhs ist
708 | [ConCase cns as nss scs, ConCase cnz az nsz scz] <- alts
709 , Just LikeS <- isLikeNat ist cns
710 = do
711 -- reorder to make the Z case come first
712 zCase <- LConstCase (BI 0) <$> irSC top vs scz
713 sCase <- irAlt top vs (LV n) (ConCase cns as nss scs)
714 return $ LCase up (LV n) [zCase, sCase]
716 | otherwise = do
717 -- check that neither alternative needs the newtype optimisation,
718 -- see comment above
719 goneWrong <- or <$> mapM isDetaggable alts
720 when goneWrong
721 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
723 -- everything okay
724 LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
726 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
727 isDetaggable _ = return False
729irSC top vs ImpossibleCase = return LNothing
731irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt
733-- this leaves out all unused arguments of the constructor
734irAlt top vs tm (ConCase n t args sc) = do
735 likeNat <- isLikeNat <$> getIState <*> pure n
736 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
737 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
739 case likeNat of
740 -- like S
741 Just LikeS -> do
742 sc' <- irSC top vs sc
743 case usedArgs of
744 [pv] -> return $ LDefaultCase $ LLet pv
745 ( LOp
746 (LMinus (ATInt ITBig))
747 [ tm
748 , LConst (BI 1)
749 ]
750 )
751 sc'
753 _ -> ifail $ "irAlt/LikeS: multiple used args: " ++ show usedArgs
755 -- like Z
756 Just LikeZ -> LConstCase (BI 0) <$> irSC top vs sc
758 -- not like Nat
759 Nothing -> LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc
760 where
761 methodVars = case n of
762 SN (ImplementationCtorN interfaceName)
763 -> M.fromList [(v, VI
764 { viMethod = Just $ mkFieldName n i
765 }) | (v,i) <- zip args [0..]]
766 _
767 -> M.empty -- not an implementation constructor
769irAlt top vs _ (ConstCase x rhs)
770 | matchable x = LConstCase x <$> irSC top vs rhs
771 | matchableTy x = LDefaultCase <$> irSC top vs rhs
772 where
773 matchable (I _) = True
774 matchable (BI _) = True
775 matchable (Ch _) = True
776 matchable (Str _) = True
777 matchable (B8 _) = True
778 matchable (B16 _) = True
779 matchable (B32 _) = True
780 matchable (B64 _) = True
781 matchable _ = False
783 matchableTy (AType (ATInt ITNative)) = True
784 matchableTy (AType (ATInt ITBig)) = True
785 matchableTy (AType (ATInt ITChar)) = True
786 matchableTy StrType = True
788 matchableTy (AType (ATInt (ITFixed IT8))) = True
789 matchableTy (AType (ATInt (ITFixed IT16))) = True
790 matchableTy (AType (ATInt (ITFixed IT32))) = True
791 matchableTy (AType (ATInt (ITFixed IT64))) = True
793 matchableTy _ = False
795irAlt top vs tm (SucCase n rhs) = do
796 rhs' <- irSC top vs rhs
797 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
798 [tm,
799 LConst (BI 1)]) rhs')
801irAlt top vs _ (ConstCase c rhs)
802 = ifail $ "Can't match on (" ++ show c ++ ")"
804irAlt top vs _ (DefaultCase rhs)
805 = LDefaultCase <$> irSC top vs rhs