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