git.iko.soy/Idris-dev
on 8935fed help sign in
Idris-dev/src/IRTS/Compiler.hs
710 lines 26 kB history raw
1{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
3module IRTS.Compiler(compile, generate) where
5import IRTS.Lang
6import IRTS.LangOpts
7import IRTS.Defunctionalise
8import IRTS.Simplified
9import IRTS.CodegenCommon
10import IRTS.CodegenC
11import IRTS.DumpBC
12import IRTS.CodegenJavaScript
13import IRTS.Inliner
14import IRTS.Exports
16import Idris.AbsSyntax
17import Idris.AbsSyntaxTree
18import Idris.ASTUtils
19import Idris.Erasure
20import Idris.Error
22import Debug.Trace
24import Idris.Core.TT
25import Idris.Core.Evaluate
26import Idris.Core.CaseTree
28import Control.Category
29import Prelude hiding (id, (.))
31import Control.Applicative
32import Control.Monad.State
33import Data.Maybe
34import Data.List
35import Data.Ord
36import Data.IntSet (IntSet)
37import qualified Data.IntSet as IS
38import qualified Data.Map as M
39import qualified Data.Set as S
40import System.Process
41import System.IO
42import System.Exit
43import System.Directory
44import System.Environment
45import System.FilePath ((</>), addTrailingPathSeparator)
47-- | Given a 'main' term to compiler, return the IRs which can be used to
48-- generate code.
49compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
50compile codegen f mtm
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
55 Nothing -> []
56 Just t -> freeNames t
58 reachableNames <- performUsageAnalysis
59 (rootNames ++ getExpNames exports)
60 maindef <- case mtm of
61 Nothing -> return []
62 Just tm -> do md <- irMain tm
63 iLOG $ "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
73 Nothing -> True
74 Just _ -> False
76 let defs = defsIn ++ maindef
77 -- iputStrLn $ showSep "\n" (map show defs)
78 -- Inlined top level LDecl made here
79 let defsInlined = inlineAll defs
80 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
81 defsInlined
83 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)
84 let ctxtIn = addAlist tagged emptyContext
86 iLOG "Defunctionalising"
87 let defuns_in = defunctionalise nexttag ctxtIn
88 logLvl 5 $ show defuns_in
89 iLOG "Inlining"
90 let defuns = inline defuns_in
91 logLvl 5 $ show defuns
92 iLOG "Resolving variables for CG"
93 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
94 let checked = simplifyDefs defuns (toAlist defuns)
95 outty <- outputTy
96 dumpCases <- getDumpCases
97 dumpDefun <- getDumpDefun
98 case dumpCases of
99 Nothing -> return ()
100 Just f -> runIO $ writeFile f (showCaseTrees defs)
101 case dumpDefun of
102 Nothing -> return ()
103 Just f -> runIO $ writeFile f (dumpDefuns defuns)
104 triple <- Idris.AbsSyntax.targetTriple
105 cpu <- Idris.AbsSyntax.targetCPU
106 iLOG "Building output"
107 case checked of
108 OK c -> do return $ CodegenInfo f outty triple cpu
109 hdrs impdirs objs libs flags
110 NONE c (toAlist defuns)
111 tagged iface exports
112-- runIO $ case codegen of
113-- ViaC -> codegenC cginfo
114-- ViaJava -> codegenJava cginfo
115-- ViaJavaScript -> codegenJavaScript cginfo
116-- ViaNode -> codegenNode cginfo
117-- ViaLLVM -> codegenLLVM cginfo
118-- Bytecode -> dumpBC c f
119 Error e -> ierror e
120 where checkMVs = do i <- getIState
121 case map fst (idris_metavars i) \\ primDefs of
122 [] -> return ()
123 ms -> ifail $ "There are undefined metavariables: " ++ show ms
124 checkTotality = do i <- getIState
125 case idris_totcheckfail i of
126 [] -> return ()
127 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
128 inDir d h = do let f = d </> h
129 ex <- doesFileExist f
130 if ex then return f else return h
132generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
133generate codegen mainmod ir
134 = case codegen of
135 -- Built-in code generators (FIXME: lift these out!)
136 Via "c" -> codegenC ir
137 -- Any external code generator
138 Via cg -> do let cmd = "idris-" ++ cg
139 args = [mainmod, "-o", outputFile ir]
140 exit <- rawSystem cmd args
141 when (exit /= ExitSuccess) $
142 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
143 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
145irMain :: TT Name -> Idris LDecl
146irMain tm = do
147 i <- irTerm M.empty [] tm
148 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
150mkDecls :: [Name] -> Idris [(Name, LDecl)]
151mkDecls used
152 = do i <- getIState
153 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
154 decls <- mapM build ds
155 return decls
157showCaseTrees :: [(Name, LDecl)] -> String
158showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
159 where
160 showCT (n, LFun _ f args lexp)
161 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
162 ++ show lexp
163 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
165 defnRank :: (Name, LDecl) -> String
166 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
167 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
169 nameRank :: Name -> String
170 nameRank (UN s) = "1" ++ show s
171 nameRank (MN i s) = "2" ++ show s ++ show i
172 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
173 nameRank (SN sn) = "4" ++ snRank sn
174 nameRank n = "5" ++ show n
176 snRank :: SpecialName -> String
177 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
178 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
179 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
180 snRank (MethodN n) = "4" ++ nameRank n
181 snRank (CaseN n) = "5" ++ nameRank n
182 snRank (ElimN n) = "6" ++ nameRank n
183 snRank (InstanceCtorN n) = "7" ++ nameRank n
184 snRank (WithN i n) = "8" ++ nameRank n ++ show i
186isCon (TyDecl _ _) = True
187isCon _ = False
189build :: (Name, Def) -> Idris (Name, LDecl)
190build (n, d)
191 = do i <- getIState
192 case getPrim n i of
193 Just (ar, op) ->
194 let args = map (\x -> sMN x "op") [0..] in
195 return (n, (LFun [] n (take ar args)
196 (LOp op (map (LV . Glob) (take ar args)))))
197 _ -> do def <- mkLDecl n d
198 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
199 return (n, def)
200 where getPrim n i
201 | Just (ar, op) <- lookup n (idris_scprims i)
202 = Just (ar, op)
203 | Just ar <- lookup n (S.toList (idris_externs i))
204 = Just (ar, LExternal n)
205 getPrim n i = Nothing
207declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
208declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
210mkLDecl n (Function tm _)
211 = declArgs [] True n <$> irTerm M.empty [] tm
213mkLDecl n (CaseOp ci _ _ _ pats cd)
214 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc
215 where
216 (args, sc) = cases_runtime cd
218 -- Always attempt to inline functions arising from 'case' expressions
219 caseName (SN (CaseN _)) = True
220 caseName (SN (WithN _ _)) = True
221 caseName (NS n _) = caseName n
222 caseName _ = False
224mkLDecl n (TyDecl (DCon tag arity _) _) =
225 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
227mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
228mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
230data VarInfo = VI
231 { viMethod :: Maybe Name
232 }
233 deriving Show
235type Vars = M.Map Name VarInfo
237irTerm :: Vars -> [Name] -> Term -> Idris LExp
238irTerm vs env tm@(App _ f a) = do
239 ist <- getIState
240 case unApply tm of
241 (P _ (UN m) _, args)
242 | m == txt "mkForeignPrim"
243 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
245 (P _ (UN u) _, [_, arg])
246 | u == txt "unsafePerformPrimIO"
247 -> irTerm vs env arg
249 -- TMP HACK - until we get inlining.
250 (P _ (UN r) _, [_, _, _, _, _, arg])
251 | r == txt "replace"
252 -> irTerm vs env arg
254 -- Laziness, the old way
255 (P _ (UN l) _, [_, arg])
256 | l == txt "lazy"
257 -> error "lazy has crept in somehow"
259 (P _ (UN l) _, [_, arg])
260 | l == txt "force"
261 -> LForce <$> irTerm vs env arg
263 -- Laziness, the new way
264 (P _ (UN l) _, [_, _, arg])
265 | l == txt "Delay"
266 -> LLazyExp <$> irTerm vs env arg
268 (P _ (UN l) _, [_, _, arg])
269 | l == txt "Force"
270 -> LForce <$> irTerm vs env arg
272 (P _ (UN a) _, [_, _, _, arg])
273 | a == txt "assert_smaller"
274 -> irTerm vs env arg
276 (P _ (UN a) _, [_, arg])
277 | a == txt "assert_total"
278 -> irTerm vs env arg
280 (P _ (UN p) _, [_, arg])
281 | p == txt "par"
282 -> do arg' <- irTerm vs env arg
283 return $ LOp LPar [LLazyExp arg']
285 (P _ (UN pf) _, [arg])
286 | pf == txt "prim_fork"
287 -> do arg' <- irTerm vs env arg
288 return $ LOp LFork [LLazyExp arg']
290 (P _ (UN m) _, [_,size,t])
291 | m == txt "malloc"
292 -> irTerm vs env t
294 (P _ (UN tm) _, [_,t])
295 | tm == txt "trace_malloc"
296 -> irTerm vs env t -- TODO
298 -- This case is here until we get more general inlining. It's just
299 -- a really common case, and the laziness hurts...
300 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
301 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
302 | be == txt "boolElim"
303 , d == txt "Delay"
304 , d' == txt "Delay"
305 -> do
306 x' <- irTerm vs env x
307 t' <- irTerm vs env t
308 e' <- irTerm vs env e
309 return (LCase Shared x'
310 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
311 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
312 ])
314 -- data constructor
315 (P (DCon t arity _) n _, args) -> do
316 detag <- fgetState (opt_detaggable . ist_optimisation n)
317 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
319 let isNewtype = length used == 1 && detag
320 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
322 -- The following code removes fields from data constructors
323 -- and performs the newtype optimisation.
324 --
325 -- The general rule here is:
326 -- Everything we get as input is not touched by erasure,
327 -- so it conforms to the official arities and types
328 -- and we can reason about it like it's plain TT.
329 --
330 -- It's only the data that leaves this point that's erased
331 -- and possibly no longer typed as the original TT version.
332 --
333 -- Especially, underapplied constructors must yield functions
334 -- even if all the remaining arguments are erased
335 -- (the resulting function *will* be applied, to NULLs).
336 --
337 -- This will probably need rethinking when we get erasure from functions.
339 -- "padLams" will wrap our term in LLam-bdas and give us
340 -- the "list of future unerased args" coming from these lambdas.
341 --
342 -- We can do whatever we like with the list of unerased args,
343 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
344 let padLams = padLambdas used (length args) arity
346 case compare (length args) arity of
348 -- overapplied
349 GT -> ifail ("overapplied data constructor: " ++ show tm)
351 -- exactly saturated
352 EQ | isNewtype
353 -> irTerm vs env (head argsPruned)
355 | otherwise -- not newtype, plain data ctor
356 -> buildApp (LV $ Glob n) argsPruned
358 -- not saturated, underapplied
359 LT | isNewtype -- newtype
360 , length argsPruned == 1 -- and we already have the value
361 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
362 <$> irTerm vs env (head argsPruned)
364 | isNewtype -- newtype but the value is not among args yet
365 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
367 -- not a newtype, just apply to a constructor
368 | otherwise
369 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
371 -- type constructor
372 (P (TCon t a) n _, args) -> return LNothing
374 -- an external name applied to arguments
375 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
376 LOp (LExternal n) <$> mapM (irTerm vs env) args
378 -- a name applied to arguments
379 (P _ n _, args) -> do
380 case lookup n (idris_scprims ist) of
381 -- if it's a primitive that is already saturated,
382 -- compile to the corresponding op here already to save work
383 Just (arity, op) | length args == arity
384 -> LOp op <$> mapM (irTerm vs env) args
386 -- otherwise, just apply the name
387 _ -> applyName n ist args
389 -- turn de bruijn vars into regular named references and try again
390 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
392 (f, args)
393 -> LApp False
394 <$> irTerm vs env f
395 <*> mapM (irTerm vs env) args
397 where
398 buildApp :: LExp -> [Term] -> Idris LExp
399 buildApp e [] = return e
400 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
402 applyToNames :: LExp -> [Name] -> LExp
403 applyToNames tm [] = tm
404 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
406 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
407 padLambdas used startIdx endSIdx mkTerm
408 = LLam allNames $ mkTerm nonerasedNames
409 where
410 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
411 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
413 applyName :: Name -> IState -> [Term] -> Idris LExp
414 applyName n ist args =
415 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
416 where
417 erase (i, x)
418 | i >= arity || i `elem` used = x
419 | otherwise = Erased
421 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
422 Just (CaseOp ci ty tys def tot cdefs) -> length tys
423 Just (TyDecl (DCon tag ar _) _) -> ar
424 Just (TyDecl Ref ty) -> length $ getArgTys ty
425 Just (Operator ty ar op) -> ar
426 Just def -> error $ "unknown arity: " ++ show (n, def)
427 Nothing -> 0 -- no definition, probably local name => can't erase anything
429 -- name for purposes of usage info lookup
430 uName
431 | Just n' <- viMethod =<< M.lookup n vs = n'
432 | otherwise = n
434 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
435 fst4 (x,_,_,_) = x
437irTerm vs env (P _ n _) = return $ LV (Glob n)
438irTerm vs env (V i)
439 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
440 | otherwise = ifail $ "bad de bruijn index: " ++ show i
442irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
443 where
444 n' = uniqueName n env
446irTerm vs env (Bind n (Let _ v) sc)
447 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
449irTerm vs env (Bind _ _ _) = return $ LNothing
451irTerm vs env (Proj t (-1)) = do
452 t' <- irTerm vs env t
453 return $ LOp (LMinus (ATInt ITBig))
454 [t', LConst (BI 1)]
456irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
457irTerm vs env (Constant TheWorld) = return $ LNothing
458irTerm vs env (Constant c) = return $ LConst c
459irTerm vs env (TType _) = return $ LNothing
460irTerm vs env Erased = return $ LNothing
461irTerm vs env Impossible = return $ LNothing
463doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
464doForeign vs env (ret : fname : world : args)
465 = do args' <- mapM splitArg args
466 let fname' = toFDesc fname
467 let ret' = toFDesc ret
468 return $ LForeign ret' fname' args'
469 where
470 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
471 = do let l' = toFDesc l
472 r' <- irTerm vs env r
473 return (l', r')
474 splitArg _ = ifail "Badly formed foreign function call"
476 toFDesc (Constant (Str str)) = FStr str
477 toFDesc tm
478 | (P _ n _, []) <- unApply tm = FCon (deNS n)
479 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
480 toFDesc _ = FUnknown
482 deNS (NS n _) = n
483 deNS n = n
484doForeign vs env xs = ifail "Badly formed foreign function call"
486{-
487 - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
488 = case getFTypes fgnArgTys of
489 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
490 Just tys -> do
491 args' <- mapM (irTerm vs env) (init args)
492 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
494 | otherwise = ifail "Badly formed foreign function call"
495 where
496 getFTypes :: TT Name -> Maybe [FType]
497 getFTypes tm = case unApply tm of
498 -- nil : {a : Type} -> List a
499 (nil, [_]) -> Just []
500 -- cons : {a : Type} -> a -> List a -> List a
501 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
502 _ -> Nothing
504 mkIty' (P _ (UN ty) _) = mkIty (str ty)
505 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
506 | fi == txt "FIntT"
507 = mkIntIty (str intTy)
509 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
510 | ff == txt "FFunction"
511 , fa == txt "FAny"
512 , io == txt "IO"
513 = FFunctionIO
515 mkIty' (App (App (P _ (UN ff) _) _) _)
516 | ff == txt "FFunction"
517 = FFunction
519 mkIty' _ = FAny
521 -- would be better if these FInt types were evaluated at compile time
522 -- TODO: add %eval directive for such things
523 -- Issue #1742 on the issue tracker.
524 -- https://github.com/idris-lang/Idris-dev/issues/1742
525 mkIty "FFloat" = FArith ATFloat
526 mkIty "FInt" = mkIntIty "ITNative"
527 mkIty "FChar" = mkIntIty "ITChar"
528 mkIty "FByte" = mkIntIty "IT8"
529 mkIty "FShort" = mkIntIty "IT16"
530 mkIty "FLong" = mkIntIty "IT64"
531 mkIty "FBits8" = mkIntIty "IT8"
532 mkIty "FBits16" = mkIntIty "IT16"
533 mkIty "FBits32" = mkIntIty "IT32"
534 mkIty "FBits64" = mkIntIty "IT64"
535 mkIty "FString" = FString
536 mkIty "FPtr" = FPtr
537 mkIty "FManagedPtr" = FManagedPtr
538 mkIty "FUnit" = FUnit
539 mkIty "FFunction" = FFunction
540 mkIty "FFunctionIO" = FFunctionIO
541 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
542 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
543 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
544 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
545 mkIty x = error $ "Unknown type " ++ x
547 mkIntIty "ITNative" = FArith (ATInt ITNative)
548 mkIntIty "ITChar" = FArith (ATInt ITChar)
549 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
550 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
551 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
552 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
553-}
555irTree :: [Name] -> SC -> Idris LExp
556irTree args tree = do
557 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
558 LLam args <$> irSC M.empty tree
560irSC :: Vars -> SC -> Idris LExp
561irSC vs (STerm t) = irTerm vs [] t
562irSC vs (UnmatchedCase str) = return $ LError str
564irSC vs (ProjCase tm alts) = do
565 tm' <- irTerm vs [] tm
566 alts' <- mapM (irAlt vs tm') alts
567 return $ LCase Shared tm' alts'
569-- Transform matching on Delay to applications of Force.
570irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
571 | delay == txt "Delay"
572 = do sc' <- irSC vs $ mkForce n' n sc
573 return $ LLet n' (LForce (LV (Glob n))) sc'
575-- There are two transformations in this case:
576--
577-- 1. Newtype-case elimination:
578-- case {e0} of
579-- wrap({e1}) -> P({e1}) ==> P({e0})
580--
581-- This is important because newtyped constructors are compiled away entirely
582-- and we need to do that everywhere.
583--
584-- 2. Unused-case elimination (only valid for singleton branches):
585-- case {e0} of ==> P
586-- C(x,y) -> P[... x,y not used ...]
587--
588-- This is important for runtime because sometimes we case on irrelevant data:
589--
590-- In the example above, {e0} will most probably have been erased
591-- so this vain projection would make the resulting program segfault
592-- because the code generator still emits a PROJECT(...) G-machine instruction.
593--
594-- Hence, we check whether the variables are used at all
595-- and erase the casesplit if they are not.
596--
597irSC vs (Case up n [alt]) = do
598 replacement <- case alt of
599 ConCase cn a ns sc -> do
600 detag <- fgetState (opt_detaggable . ist_optimisation cn)
601 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
602 if detag && length used == 1
603 then return . Just $ substSC (ns !! head used) n sc
604 else return Nothing
605 _ -> return Nothing
607 case replacement of
608 Just sc -> irSC vs sc
609 _ -> do
610 alt' <- irAlt vs (LV (Glob n)) alt
611 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
612 [] -> subexpr alt' -- strip the unused top-most case
613 _ -> LCase up (LV (Glob n)) [alt']
614 where
615 namesBoundIn :: LAlt -> [Name]
616 namesBoundIn (LConCase cn i ns sc) = ns
617 namesBoundIn (LConstCase c sc) = []
618 namesBoundIn (LDefaultCase sc) = []
620 subexpr :: LAlt -> LExp
621 subexpr (LConCase _ _ _ e) = e
622 subexpr (LConstCase _ e) = e
623 subexpr (LDefaultCase e) = e
625-- FIXME: When we have a non-singleton case-tree of the form
626--
627-- case {e0} of
628-- C(x) => ...
629-- ... => ...
630--
631-- and C is detaggable (the only constructor of the family), we can be sure
632-- that the first branch will be always taken -- so we add special handling
633-- to remove the dead default branch.
634--
635-- If we don't do so and C is newtype-optimisable, we will miss this newtype
636-- transformation and the resulting code will probably segfault.
637--
638-- This work-around is not entirely optimal; the best approach would be
639-- to ensure that such case trees don't arise in the first place.
640--
641irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
642 detag <- fgetState (opt_detaggable . ist_optimisation cn)
643 if detag
644 then irSC vs (Case up n [ConCase cn a ns sc])
645 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
647irSC vs sc@(Case up n alts) = do
648 -- check that neither alternative needs the newtype optimisation,
649 -- see comment above
650 goneWrong <- or <$> mapM isDetaggable alts
651 when goneWrong
652 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
654 -- everything okay
655 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
656 where
657 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
658 isDetaggable _ = return False
660irSC vs ImpossibleCase = return LNothing
662irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
664-- this leaves out all unused arguments of the constructor
665irAlt vs _ (ConCase n t args sc) = do
666 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
667 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
668 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
669 where
670 methodVars = case n of
671 SN (InstanceCtorN className)
672 -> M.fromList [(v, VI
673 { viMethod = Just $ mkFieldName n i
674 }) | (v,i) <- zip args [0..]]
675 _
676 -> M.empty -- not an instance constructor
678irAlt vs _ (ConstCase x rhs)
679 | matchable x = LConstCase x <$> irSC vs rhs
680 | matchableTy x = LDefaultCase <$> irSC vs rhs
681 where
682 matchable (I _) = True
683 matchable (BI _) = True
684 matchable (Ch _) = True
685 matchable (Str _) = True
686 matchable _ = False
688 matchableTy (AType (ATInt ITNative)) = True
689 matchableTy (AType (ATInt ITBig)) = True
690 matchableTy (AType (ATInt ITChar)) = True
691 matchableTy StrType = True
693 matchableTy (AType (ATInt (ITFixed IT8))) = True
694 matchableTy (AType (ATInt (ITFixed IT16))) = True
695 matchableTy (AType (ATInt (ITFixed IT32))) = True
696 matchableTy (AType (ATInt (ITFixed IT64))) = True
698 matchableTy _ = False
700irAlt vs tm (SucCase n rhs) = do
701 rhs' <- irSC vs rhs
702 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
703 [tm,
704 LConst (BI 1)]) rhs')
706irAlt vs _ (ConstCase c rhs)
707 = ifail $ "Can't match on (" ++ show c ++ ")"
709irAlt vs _ (DefaultCase rhs)
710 = LDefaultCase <$> irSC vs rhs