git.iko.soy/Idris-dev
on 1cdc9dd help sign in
Idris-dev/src/IRTS/Compiler.hs
712 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 logLvl 1 $ "MAIN: " ++ show md
64 return [(sMN 0 "runMain", md)]
65 objs <- getObjectFiles codegen
66 libs <- getLibs codegen
67 flags <- getFlags codegen
68 hdrs <- getHdrs codegen
69 impdirs <- allImportDirs
70 defsIn <- mkDecls reachableNames
71 -- if no 'main term' given, generate interface files
72 let iface = case mtm of
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 logLvl 1 "Defunctionalising"
87 let defuns_in = defunctionalise nexttag ctxtIn
88 logLvl 5 $ show defuns_in
89 logLvl 1 "Inlining"
90 let defuns = inline defuns_in
91 logLvl 5 $ show defuns
92 logLvl 1 "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 logLvl 1 "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 holes: " ++ 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-codegen-" ++ cg
139 args = ["--yes-really", mainmod, "-o", outputFile ir] ++ compilerFlags 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 "ifThenElse"
303 , d == txt "Delay"
304 , d' == txt "Delay"
305 , b == txt "Bool"
306 , p == txt "Prelude"
307 -> do
308 x' <- irTerm vs env x
309 t' <- irTerm vs env t
310 e' <- irTerm vs env e
311 return (LCase Shared x'
312 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
313 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
314 ])
316 -- data constructor
317 (P (DCon t arity _) n _, args) -> do
318 detag <- fgetState (opt_detaggable . ist_optimisation n)
319 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
321 let isNewtype = length used == 1 && detag
322 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
324 -- The following code removes fields from data constructors
325 -- and performs the newtype optimisation.
326 --
327 -- The general rule here is:
328 -- Everything we get as input is not touched by erasure,
329 -- so it conforms to the official arities and types
330 -- and we can reason about it like it's plain TT.
331 --
332 -- It's only the data that leaves this point that's erased
333 -- and possibly no longer typed as the original TT version.
334 --
335 -- Especially, underapplied constructors must yield functions
336 -- even if all the remaining arguments are erased
337 -- (the resulting function *will* be applied, to NULLs).
338 --
339 -- This will probably need rethinking when we get erasure from functions.
341 -- "padLams" will wrap our term in LLam-bdas and give us
342 -- the "list of future unerased args" coming from these lambdas.
343 --
344 -- We can do whatever we like with the list of unerased args,
345 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
346 let padLams = padLambdas used (length args) arity
348 case compare (length args) arity of
350 -- overapplied
351 GT -> ifail ("overapplied data constructor: " ++ show tm)
353 -- exactly saturated
354 EQ | isNewtype
355 -> irTerm vs env (head argsPruned)
357 | otherwise -- not newtype, plain data ctor
358 -> buildApp (LV $ Glob n) argsPruned
360 -- not saturated, underapplied
361 LT | isNewtype -- newtype
362 , length argsPruned == 1 -- and we already have the value
363 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
364 <$> irTerm vs env (head argsPruned)
366 | isNewtype -- newtype but the value is not among args yet
367 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
369 -- not a newtype, just apply to a constructor
370 | otherwise
371 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
373 -- type constructor
374 (P (TCon t a) n _, args) -> return LNothing
376 -- an external name applied to arguments
377 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
378 LOp (LExternal n) <$> mapM (irTerm vs env) args
380 -- a name applied to arguments
381 (P _ n _, args) -> do
382 case lookup n (idris_scprims ist) of
383 -- if it's a primitive that is already saturated,
384 -- compile to the corresponding op here already to save work
385 Just (arity, op) | length args == arity
386 -> LOp op <$> mapM (irTerm vs env) args
388 -- otherwise, just apply the name
389 _ -> applyName n ist args
391 -- turn de bruijn vars into regular named references and try again
392 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
394 (f, args)
395 -> LApp False
396 <$> irTerm vs env f
397 <*> mapM (irTerm vs env) args
399 where
400 buildApp :: LExp -> [Term] -> Idris LExp
401 buildApp e [] = return e
402 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
404 applyToNames :: LExp -> [Name] -> LExp
405 applyToNames tm [] = tm
406 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
408 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
409 padLambdas used startIdx endSIdx mkTerm
410 = LLam allNames $ mkTerm nonerasedNames
411 where
412 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
413 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
415 applyName :: Name -> IState -> [Term] -> Idris LExp
416 applyName n ist args =
417 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
418 where
419 erase (i, x)
420 | i >= arity || i `elem` used = x
421 | otherwise = Erased
423 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
424 Just (CaseOp ci ty tys def tot cdefs) -> length tys
425 Just (TyDecl (DCon tag ar _) _) -> ar
426 Just (TyDecl Ref ty) -> length $ getArgTys ty
427 Just (Operator ty ar op) -> ar
428 Just def -> error $ "unknown arity: " ++ show (n, def)
429 Nothing -> 0 -- no definition, probably local name => can't erase anything
431 -- name for purposes of usage info lookup
432 uName
433 | Just n' <- viMethod =<< M.lookup n vs = n'
434 | otherwise = n
436 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
437 fst4 (x,_,_,_) = x
439irTerm vs env (P _ n _) = return $ LV (Glob n)
440irTerm vs env (V i)
441 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
442 | otherwise = ifail $ "bad de bruijn index: " ++ show i
444irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
445 where
446 n' = uniqueName n env
448irTerm vs env (Bind n (Let _ v) sc)
449 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
451irTerm vs env (Bind _ _ _) = return $ LNothing
453irTerm vs env (Proj t (-1)) = do
454 t' <- irTerm vs env t
455 return $ LOp (LMinus (ATInt ITBig))
456 [t', LConst (BI 1)]
458irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
459irTerm vs env (Constant TheWorld) = return $ LNothing
460irTerm vs env (Constant c) = return $ LConst c
461irTerm vs env (TType _) = return $ LNothing
462irTerm vs env Erased = return $ LNothing
463irTerm vs env Impossible = return $ LNothing
465doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
466doForeign vs env (ret : fname : world : args)
467 = do args' <- mapM splitArg args
468 let fname' = toFDesc fname
469 let ret' = toFDesc ret
470 return $ LForeign ret' fname' args'
471 where
472 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
473 = do let l' = toFDesc l
474 r' <- irTerm vs env r
475 return (l', r')
476 splitArg _ = ifail "Badly formed foreign function call"
478 toFDesc (Constant (Str str)) = FStr str
479 toFDesc tm
480 | (P _ n _, []) <- unApply tm = FCon (deNS n)
481 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
482 toFDesc _ = FUnknown
484 deNS (NS n _) = n
485 deNS n = n
486doForeign vs env xs = ifail "Badly formed foreign function call"
488{-
489 - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
490 = case getFTypes fgnArgTys of
491 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
492 Just tys -> do
493 args' <- mapM (irTerm vs env) (init args)
494 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
496 | otherwise = ifail "Badly formed foreign function call"
497 where
498 getFTypes :: TT Name -> Maybe [FType]
499 getFTypes tm = case unApply tm of
500 -- nil : {a : Type} -> List a
501 (nil, [_]) -> Just []
502 -- cons : {a : Type} -> a -> List a -> List a
503 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
504 _ -> Nothing
506 mkIty' (P _ (UN ty) _) = mkIty (str ty)
507 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
508 | fi == txt "FIntT"
509 = mkIntIty (str intTy)
511 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
512 | ff == txt "FFunction"
513 , fa == txt "FAny"
514 , io == txt "IO"
515 = FFunctionIO
517 mkIty' (App (App (P _ (UN ff) _) _) _)
518 | ff == txt "FFunction"
519 = FFunction
521 mkIty' _ = FAny
523 -- would be better if these FInt types were evaluated at compile time
524 -- TODO: add %eval directive for such things
525 -- Issue #1742 on the issue tracker.
526 -- https://github.com/idris-lang/Idris-dev/issues/1742
527 mkIty "FFloat" = FArith ATFloat
528 mkIty "FInt" = mkIntIty "ITNative"
529 mkIty "FChar" = mkIntIty "ITChar"
530 mkIty "FByte" = mkIntIty "IT8"
531 mkIty "FShort" = mkIntIty "IT16"
532 mkIty "FLong" = mkIntIty "IT64"
533 mkIty "FBits8" = mkIntIty "IT8"
534 mkIty "FBits16" = mkIntIty "IT16"
535 mkIty "FBits32" = mkIntIty "IT32"
536 mkIty "FBits64" = mkIntIty "IT64"
537 mkIty "FString" = FString
538 mkIty "FPtr" = FPtr
539 mkIty "FManagedPtr" = FManagedPtr
540 mkIty "FUnit" = FUnit
541 mkIty "FFunction" = FFunction
542 mkIty "FFunctionIO" = FFunctionIO
543 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
544 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
545 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
546 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
547 mkIty x = error $ "Unknown type " ++ x
549 mkIntIty "ITNative" = FArith (ATInt ITNative)
550 mkIntIty "ITChar" = FArith (ATInt ITChar)
551 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
552 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
553 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
554 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
555-}
557irTree :: [Name] -> SC -> Idris LExp
558irTree args tree = do
559 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
560 LLam args <$> irSC M.empty tree
562irSC :: Vars -> SC -> Idris LExp
563irSC vs (STerm t) = irTerm vs [] t
564irSC vs (UnmatchedCase str) = return $ LError str
566irSC vs (ProjCase tm alts) = do
567 tm' <- irTerm vs [] tm
568 alts' <- mapM (irAlt vs tm') alts
569 return $ LCase Shared tm' alts'
571-- Transform matching on Delay to applications of Force.
572irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
573 | delay == txt "Delay"
574 = do sc' <- irSC vs $ mkForce n' n sc
575 return $ LLet n' (LForce (LV (Glob n))) sc'
577-- There are two transformations in this case:
578--
579-- 1. Newtype-case elimination:
580-- case {e0} of
581-- wrap({e1}) -> P({e1}) ==> P({e0})
582--
583-- This is important because newtyped constructors are compiled away entirely
584-- and we need to do that everywhere.
585--
586-- 2. Unused-case elimination (only valid for singleton branches):
587-- case {e0} of ==> P
588-- C(x,y) -> P[... x,y not used ...]
589--
590-- This is important for runtime because sometimes we case on irrelevant data:
591--
592-- In the example above, {e0} will most probably have been erased
593-- so this vain projection would make the resulting program segfault
594-- because the code generator still emits a PROJECT(...) G-machine instruction.
595--
596-- Hence, we check whether the variables are used at all
597-- and erase the casesplit if they are not.
598--
599irSC vs (Case up n [alt]) = do
600 replacement <- case alt of
601 ConCase cn a ns sc -> do
602 detag <- fgetState (opt_detaggable . ist_optimisation cn)
603 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
604 if detag && length used == 1
605 then return . Just $ substSC (ns !! head used) n sc
606 else return Nothing
607 _ -> return Nothing
609 case replacement of
610 Just sc -> irSC vs sc
611 _ -> do
612 alt' <- irAlt vs (LV (Glob n)) alt
613 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
614 [] -> subexpr alt' -- strip the unused top-most case
615 _ -> LCase up (LV (Glob n)) [alt']
616 where
617 namesBoundIn :: LAlt -> [Name]
618 namesBoundIn (LConCase cn i ns sc) = ns
619 namesBoundIn (LConstCase c sc) = []
620 namesBoundIn (LDefaultCase sc) = []
622 subexpr :: LAlt -> LExp
623 subexpr (LConCase _ _ _ e) = e
624 subexpr (LConstCase _ e) = e
625 subexpr (LDefaultCase e) = e
627-- FIXME: When we have a non-singleton case-tree of the form
628--
629-- case {e0} of
630-- C(x) => ...
631-- ... => ...
632--
633-- and C is detaggable (the only constructor of the family), we can be sure
634-- that the first branch will be always taken -- so we add special handling
635-- to remove the dead default branch.
636--
637-- If we don't do so and C is newtype-optimisable, we will miss this newtype
638-- transformation and the resulting code will probably segfault.
639--
640-- This work-around is not entirely optimal; the best approach would be
641-- to ensure that such case trees don't arise in the first place.
642--
643irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
644 detag <- fgetState (opt_detaggable . ist_optimisation cn)
645 if detag
646 then irSC vs (Case up n [ConCase cn a ns sc])
647 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
649irSC vs sc@(Case up n alts) = do
650 -- check that neither alternative needs the newtype optimisation,
651 -- see comment above
652 goneWrong <- or <$> mapM isDetaggable alts
653 when goneWrong
654 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
656 -- everything okay
657 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
658 where
659 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
660 isDetaggable _ = return False
662irSC vs ImpossibleCase = return LNothing
664irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
666-- this leaves out all unused arguments of the constructor
667irAlt vs _ (ConCase n t args sc) = do
668 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
669 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
670 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
671 where
672 methodVars = case n of
673 SN (InstanceCtorN className)
674 -> M.fromList [(v, VI
675 { viMethod = Just $ mkFieldName n i
676 }) | (v,i) <- zip args [0..]]
677 _
678 -> M.empty -- not an instance constructor
680irAlt vs _ (ConstCase x rhs)
681 | matchable x = LConstCase x <$> irSC vs rhs
682 | matchableTy x = LDefaultCase <$> irSC vs rhs
683 where
684 matchable (I _) = True
685 matchable (BI _) = True
686 matchable (Ch _) = True
687 matchable (Str _) = True
688 matchable _ = False
690 matchableTy (AType (ATInt ITNative)) = True
691 matchableTy (AType (ATInt ITBig)) = True
692 matchableTy (AType (ATInt ITChar)) = True
693 matchableTy StrType = True
695 matchableTy (AType (ATInt (ITFixed IT8))) = True
696 matchableTy (AType (ATInt (ITFixed IT16))) = True
697 matchableTy (AType (ATInt (ITFixed IT32))) = True
698 matchableTy (AType (ATInt (ITFixed IT64))) = True
700 matchableTy _ = False
702irAlt vs tm (SucCase n rhs) = do
703 rhs' <- irSC vs rhs
704 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
705 [tm,
706 LConst (BI 1)]) rhs')
708irAlt vs _ (ConstCase c rhs)
709 = ifail $ "Can't match on (" ++ show c ++ ")"
711irAlt vs _ (DefaultCase rhs)
712 = LDefaultCase <$> irSC vs rhs