git.iko.soy/Idris-dev
on a5e76fc help sign in
Idris-dev/src/IRTS/Compiler.hs
695 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 lookup n (idris_scprims 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)
197declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
198declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
200mkLDecl n (Function tm _)
201 = declArgs [] True n <$> irTerm M.empty [] tm
203mkLDecl n (CaseOp ci _ _ _ pats cd)
204 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc
205 where
206 (args, sc) = cases_runtime cd
208 -- Always attempt to inline functions arising from 'case' expressions
209 caseName (SN (CaseN _)) = True
210 caseName (SN (WithN _ _)) = True
211 caseName (NS n _) = caseName n
212 caseName _ = False
214mkLDecl n (TyDecl (DCon tag arity _) _) =
215 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
217mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
218mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
220data VarInfo = VI
221 { viMethod :: Maybe Name
222 }
223 deriving Show
225type Vars = M.Map Name VarInfo
227irTerm :: Vars -> [Name] -> Term -> Idris LExp
228irTerm vs env tm@(App f a) = case unApply tm of
229 (P _ (UN m) _, args)
230 | m == txt "mkForeignPrim"
231 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
233 (P _ (UN u) _, [_, arg])
234 | u == txt "unsafePerformPrimIO"
235 -> irTerm vs env arg
237 -- TMP HACK - until we get inlining.
238 (P _ (UN r) _, [_, _, _, _, _, arg])
239 | r == txt "replace"
240 -> irTerm vs env arg
242 -- Laziness, the old way
243 (P _ (UN l) _, [_, arg])
244 | l == txt "lazy"
245 -> error "lazy has crept in somehow"
247 (P _ (UN l) _, [_, arg])
248 | l == txt "force"
249 -> LForce <$> irTerm vs env arg
251 -- Laziness, the new way
252 (P _ (UN l) _, [_, _, arg])
253 | l == txt "Delay"
254 -> LLazyExp <$> irTerm vs env arg
256 (P _ (UN l) _, [_, _, arg])
257 | l == txt "Force"
258 -> LForce <$> irTerm vs env arg
260 (P _ (UN a) _, [_, _, _, arg])
261 | a == txt "assert_smaller"
262 -> irTerm vs env arg
264 (P _ (UN a) _, [_, arg])
265 | a == txt "assert_total"
266 -> irTerm vs env arg
268 (P _ (UN p) _, [_, arg])
269 | p == txt "par"
270 -> do arg' <- irTerm vs env arg
271 return $ LOp LPar [LLazyExp arg']
273 (P _ (UN pf) _, [arg])
274 | pf == txt "prim_fork"
275 -> do arg' <- irTerm vs env arg
276 return $ LOp LFork [LLazyExp arg']
278 (P _ (UN m) _, [_,size,t])
279 | m == txt "malloc"
280 -> irTerm vs env t
282 (P _ (UN tm) _, [_,t])
283 | tm == txt "trace_malloc"
284 -> irTerm vs env t -- TODO
286 -- This case is here until we get more general inlining. It's just
287 -- a really common case, and the laziness hurts...
288 (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),
289 (App (App (App (P _ (UN d') _) _) _) e)])
290 | be == txt "boolElim"
291 , d == txt "Delay"
292 , d' == txt "Delay"
293 -> do
294 x' <- irTerm vs env x
295 t' <- irTerm vs env t
296 e' <- irTerm vs env e
297 return (LCase Shared x'
298 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
299 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
300 ])
302 -- data constructor
303 (P (DCon t arity _) n _, args) -> do
304 detag <- fgetState (opt_detaggable . ist_optimisation n)
305 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
307 let isNewtype = length used == 1 && detag
308 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
310 -- The following code removes fields from data constructors
311 -- and performs the newtype optimisation.
312 --
313 -- The general rule here is:
314 -- Everything we get as input is not touched by erasure,
315 -- so it conforms to the official arities and types
316 -- and we can reason about it like it's plain TT.
317 --
318 -- It's only the data that leaves this point that's erased
319 -- and possibly no longer typed as the original TT version.
320 --
321 -- Especially, underapplied constructors must yield functions
322 -- even if all the remaining arguments are erased
323 -- (the resulting function *will* be applied, to NULLs).
324 --
325 -- This will probably need rethinking when we get erasure from functions.
327 -- "padLams" will wrap our term in LLam-bdas and give us
328 -- the "list of future unerased args" coming from these lambdas.
329 --
330 -- We can do whatever we like with the list of unerased args,
331 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
332 let padLams = padLambdas used (length args) arity
334 case compare (length args) arity of
336 -- overapplied
337 GT -> ifail ("overapplied data constructor: " ++ show tm)
339 -- exactly saturated
340 EQ | isNewtype
341 -> irTerm vs env (head argsPruned)
343 | otherwise -- not newtype, plain data ctor
344 -> buildApp (LV $ Glob n) argsPruned
346 -- not saturated, underapplied
347 LT | isNewtype -- newtype
348 , length argsPruned == 1 -- and we already have the value
349 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
350 <$> irTerm vs env (head argsPruned)
352 | isNewtype -- newtype but the value is not among args yet
353 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
355 -- not a newtype, just apply to a constructor
356 | otherwise
357 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
359 -- type constructor
360 (P (TCon t a) n _, args) -> return LNothing
362 -- a name applied to arguments
363 (P _ n _, args) -> do
364 ist <- getIState
365 case lookup n (idris_scprims ist) of
366 -- if it's a primitive that is already saturated,
367 -- compile to the corresponding op here already to save work
368 Just (arity, op) | length args == arity
369 -> LOp op <$> mapM (irTerm vs env) args
371 -- otherwise, just apply the name
372 _ -> applyName n ist args
374 -- turn de bruijn vars into regular named references and try again
375 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
377 (f, args)
378 -> LApp False
379 <$> irTerm vs env f
380 <*> mapM (irTerm vs env) args
382 where
383 buildApp :: LExp -> [Term] -> Idris LExp
384 buildApp e [] = return e
385 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
387 applyToNames :: LExp -> [Name] -> LExp
388 applyToNames tm [] = tm
389 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
391 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
392 padLambdas used startIdx endSIdx mkTerm
393 = LLam allNames $ mkTerm nonerasedNames
394 where
395 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
396 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
398 applyName :: Name -> IState -> [Term] -> Idris LExp
399 applyName n ist args =
400 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
401 where
402 erase (i, x)
403 | i >= arity || i `elem` used = x
404 | otherwise = Erased
406 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
407 Just (CaseOp ci ty tys def tot cdefs) -> length tys
408 Just (TyDecl (DCon tag ar _) _) -> ar
409 Just (TyDecl Ref ty) -> length $ getArgTys ty
410 Just (Operator ty ar op) -> ar
411 Just def -> error $ "unknown arity: " ++ show (n, def)
412 Nothing -> 0 -- no definition, probably local name => can't erase anything
414 -- name for purposes of usage info lookup
415 uName
416 | Just n' <- viMethod =<< M.lookup n vs = n'
417 | otherwise = n
419 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
420 fst4 (x,_,_,_) = x
422irTerm vs env (P _ n _) = return $ LV (Glob n)
423irTerm vs env (V i)
424 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
425 | otherwise = ifail $ "bad de bruijn index: " ++ show i
427irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
428 where
429 n' = uniqueName n env
431irTerm vs env (Bind n (Let _ v) sc)
432 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
434irTerm vs env (Bind _ _ _) = return $ LNothing
436irTerm vs env (Proj t (-1)) = do
437 t' <- irTerm vs env t
438 return $ LOp (LMinus (ATInt ITBig))
439 [t', LConst (BI 1)]
441irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
442irTerm vs env (Constant TheWorld) = return $ LNothing
443irTerm vs env (Constant c) = return $ LConst c
444irTerm vs env (TType _) = return $ LNothing
445irTerm vs env Erased = return $ LNothing
446irTerm vs env Impossible = return $ LNothing
448doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
449doForeign vs env (ret : fname : world : args)
450 = do args' <- mapM splitArg args
451 let fname' = toFDesc fname
452 let ret' = toFDesc ret
453 return $ LForeign ret' fname' args'
454 where
455 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
456 = do let l' = toFDesc l
457 r' <- irTerm vs env r
458 return (l', r')
459 splitArg _ = ifail "Badly formed foreign function call"
461 toFDesc (Constant (Str str)) = FStr str
462 toFDesc tm
463 | (P _ n _, []) <- unApply tm = FCon (deNS n)
464 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
465 toFDesc _ = FUnknown
467 deNS (NS n _) = n
468 deNS n = n
469doForeign vs env xs = ifail "Badly formed foreign function call"
471{-
472 - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
473 = case getFTypes fgnArgTys of
474 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
475 Just tys -> do
476 args' <- mapM (irTerm vs env) (init args)
477 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
479 | otherwise = ifail "Badly formed foreign function call"
480 where
481 getFTypes :: TT Name -> Maybe [FType]
482 getFTypes tm = case unApply tm of
483 -- nil : {a : Type} -> List a
484 (nil, [_]) -> Just []
485 -- cons : {a : Type} -> a -> List a -> List a
486 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
487 _ -> Nothing
489 mkIty' (P _ (UN ty) _) = mkIty (str ty)
490 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
491 | fi == txt "FIntT"
492 = mkIntIty (str intTy)
494 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
495 | ff == txt "FFunction"
496 , fa == txt "FAny"
497 , io == txt "IO"
498 = FFunctionIO
500 mkIty' (App (App (P _ (UN ff) _) _) _)
501 | ff == txt "FFunction"
502 = FFunction
504 mkIty' _ = FAny
506 -- would be better if these FInt types were evaluated at compile time
507 -- TODO: add %eval directive for such things
508 -- Issue #1742 on the issue tracker.
509 -- https://github.com/idris-lang/Idris-dev/issues/1742
510 mkIty "FFloat" = FArith ATFloat
511 mkIty "FInt" = mkIntIty "ITNative"
512 mkIty "FChar" = mkIntIty "ITChar"
513 mkIty "FByte" = mkIntIty "IT8"
514 mkIty "FShort" = mkIntIty "IT16"
515 mkIty "FLong" = mkIntIty "IT64"
516 mkIty "FBits8" = mkIntIty "IT8"
517 mkIty "FBits16" = mkIntIty "IT16"
518 mkIty "FBits32" = mkIntIty "IT32"
519 mkIty "FBits64" = mkIntIty "IT64"
520 mkIty "FString" = FString
521 mkIty "FPtr" = FPtr
522 mkIty "FManagedPtr" = FManagedPtr
523 mkIty "FUnit" = FUnit
524 mkIty "FFunction" = FFunction
525 mkIty "FFunctionIO" = FFunctionIO
526 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
527 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
528 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
529 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
530 mkIty x = error $ "Unknown type " ++ x
532 mkIntIty "ITNative" = FArith (ATInt ITNative)
533 mkIntIty "ITChar" = FArith (ATInt ITChar)
534 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
535 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
536 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
537 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
538-}
540irTree :: [Name] -> SC -> Idris LExp
541irTree args tree = do
542 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
543 LLam args <$> irSC M.empty tree
545irSC :: Vars -> SC -> Idris LExp
546irSC vs (STerm t) = irTerm vs [] t
547irSC vs (UnmatchedCase str) = return $ LError str
549irSC vs (ProjCase tm alts) = do
550 tm' <- irTerm vs [] tm
551 alts' <- mapM (irAlt vs tm') alts
552 return $ LCase Shared tm' alts'
554-- Transform matching on Delay to applications of Force.
555irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
556 | delay == txt "Delay"
557 = do sc' <- irSC vs $ mkForce n' n sc
558 return $ LLet n' (LForce (LV (Glob n))) sc'
560-- There are two transformations in this case:
561--
562-- 1. Newtype-case elimination:
563-- case {e0} of
564-- wrap({e1}) -> P({e1}) ==> P({e0})
565--
566-- This is important because newtyped constructors are compiled away entirely
567-- and we need to do that everywhere.
568--
569-- 2. Unused-case elimination (only valid for singleton branches):
570-- case {e0} of ==> P
571-- C(x,y) -> P[... x,y not used ...]
572--
573-- This is important for runtime because sometimes we case on irrelevant data:
574--
575-- In the example above, {e0} will most probably have been erased
576-- so this vain projection would make the resulting program segfault
577-- because the code generator still emits a PROJECT(...) G-machine instruction.
578--
579-- Hence, we check whether the variables are used at all
580-- and erase the casesplit if they are not.
581--
582irSC vs (Case up n [alt]) = do
583 replacement <- case alt of
584 ConCase cn a ns sc -> do
585 detag <- fgetState (opt_detaggable . ist_optimisation cn)
586 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
587 if detag && length used == 1
588 then return . Just $ substSC (ns !! head used) n sc
589 else return Nothing
590 _ -> return Nothing
592 case replacement of
593 Just sc -> irSC vs sc
594 _ -> do
595 alt' <- irAlt vs (LV (Glob n)) alt
596 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
597 [] -> subexpr alt' -- strip the unused top-most case
598 _ -> LCase up (LV (Glob n)) [alt']
599 where
600 namesBoundIn :: LAlt -> [Name]
601 namesBoundIn (LConCase cn i ns sc) = ns
602 namesBoundIn (LConstCase c sc) = []
603 namesBoundIn (LDefaultCase sc) = []
605 subexpr :: LAlt -> LExp
606 subexpr (LConCase _ _ _ e) = e
607 subexpr (LConstCase _ e) = e
608 subexpr (LDefaultCase e) = e
610-- FIXME: When we have a non-singleton case-tree of the form
611--
612-- case {e0} of
613-- C(x) => ...
614-- ... => ...
615--
616-- and C is detaggable (the only constructor of the family), we can be sure
617-- that the first branch will be always taken -- so we add special handling
618-- to remove the dead default branch.
619--
620-- If we don't do so and C is newtype-optimisable, we will miss this newtype
621-- transformation and the resulting code will probably segfault.
622--
623-- This work-around is not entirely optimal; the best approach would be
624-- to ensure that such case trees don't arise in the first place.
625--
626irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
627 detag <- fgetState (opt_detaggable . ist_optimisation cn)
628 if detag
629 then irSC vs (Case up n [ConCase cn a ns sc])
630 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
632irSC vs sc@(Case up n alts) = do
633 -- check that neither alternative needs the newtype optimisation,
634 -- see comment above
635 goneWrong <- or <$> mapM isDetaggable alts
636 when goneWrong
637 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
639 -- everything okay
640 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
641 where
642 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
643 isDetaggable _ = return False
645irSC vs ImpossibleCase = return LNothing
647irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
649-- this leaves out all unused arguments of the constructor
650irAlt vs _ (ConCase n t args sc) = do
651 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
652 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
653 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
654 where
655 methodVars = case n of
656 SN (InstanceCtorN className)
657 -> M.fromList [(v, VI
658 { viMethod = Just $ mkFieldName n i
659 }) | (v,i) <- zip args [0..]]
660 _
661 -> M.empty -- not an instance constructor
663irAlt vs _ (ConstCase x rhs)
664 | matchable x = LConstCase x <$> irSC vs rhs
665 | matchableTy x = LDefaultCase <$> irSC vs rhs
666 where
667 matchable (I _) = True
668 matchable (BI _) = True
669 matchable (Ch _) = True
670 matchable (Str _) = True
671 matchable _ = False
673 matchableTy (AType (ATInt ITNative)) = True
674 matchableTy (AType (ATInt ITBig)) = True
675 matchableTy (AType (ATInt ITChar)) = True
676 matchableTy StrType = True
678 matchableTy (AType (ATInt (ITFixed IT8))) = True
679 matchableTy (AType (ATInt (ITFixed IT16))) = True
680 matchableTy (AType (ATInt (ITFixed IT32))) = True
681 matchableTy (AType (ATInt (ITFixed IT64))) = True
683 matchableTy _ = False
685irAlt vs tm (SucCase n rhs) = do
686 rhs' <- irSC vs rhs
687 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
688 [tm,
689 LConst (BI 1)]) rhs')
691irAlt vs _ (ConstCase c rhs)
692 = ifail $ "Can't match on (" ++ show c ++ ")"
694irAlt vs _ (DefaultCase rhs)
695 = LDefaultCase <$> irSC vs rhs