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