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