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