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