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