git.iko.soy/Idris-dev
on 2bf2038 help sign in
Idris-dev/src/IRTS/Compiler.hs
674 lines 25 kB history raw
1{-|
2Module : IRTS.Compiler
3Description : Coordinates the compilation process.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
10module IRTS.Compiler(compile, generate) where
12import IRTS.Lang
13import IRTS.LangOpts
14import IRTS.Defunctionalise
15import IRTS.Simplified
16import IRTS.CodegenCommon
17import IRTS.CodegenC
18import IRTS.DumpBC
19import IRTS.CodegenJavaScript
20import IRTS.Inliner
21import IRTS.Exports
22import IRTS.Portable
24import Idris.AbsSyntax
25import Idris.AbsSyntaxTree
26import Idris.ASTUtils
27import Idris.Erasure
28import Idris.Error
29import Idris.Output
31import Debug.Trace
33import Idris.Core.TT
34import Idris.Core.Evaluate
35import Idris.Core.CaseTree
37import Control.Category
38import Prelude hiding (id, (.))
40import Control.Applicative
41import Control.Monad.State
43import Data.Maybe
44import Data.List
45import Data.Ord
46import Data.IntSet (IntSet)
47import qualified Data.IntSet as IS
48import qualified Data.Map as M
49import qualified Data.Set as S
51import System.Process
52import System.IO
53import System.Exit
54import System.Directory
55import System.Environment
56import System.FilePath ((</>), addTrailingPathSeparator)
58-- | Compile to simplified forms and return CodegenInfo
59compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
60compile codegen f mtm
61 = do checkMVs -- check for undefined metavariables
62 checkTotality -- refuse to compile if there are totality problems
63 exports <- findExports
64 let rootNames = case mtm of
65 Nothing -> []
66 Just t -> freeNames t
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 <- allImportDirs
80 defsIn <- mkDecls reachableNames
81 -- if no 'main term' given, generate interface files
82 let iface = case mtm of
83 Nothing -> True
84 Just _ -> False
86 let defs = defsIn ++ maindef
88 -- Inlined top level LDecl made here
89 let defsInlined = inlineAll defs
90 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
91 defsInlined
93 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)
94 let ctxtIn = addAlist tagged emptyContext
96 logCodeGen 1 "Defunctionalising"
97 let defuns_in = defunctionalise nexttag ctxtIn
98 logCodeGen 5 $ show defuns_in
99 logCodeGen 1 "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 "Building output"
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 (InstanceN 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 (InstanceCtorN 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 -- TMP HACK - until we get inlining.
267 (P _ (UN r) _, [_, _, _, _, _, arg])
268 | r == txt "replace"
269 -> irTerm top vs env arg
271 -- 'void' doesn't have any pattern clauses and only gets called on
272 -- erased things in higher order contexts (also a TMP HACK...)
273 (P _ (UN r) _, _)
274 | r == txt "void"
275 -> return LNothing
277 -- Laziness, the old way
278 (P _ (UN l) _, [_, arg])
279 | l == txt "lazy"
280 -> error "lazy has crept in somehow"
282 (P _ (UN l) _, [_, arg])
283 | l == txt "force"
284 -> LForce <$> irTerm top vs env arg
286 -- Laziness, the new way
287 (P _ (UN l) _, [_, _, arg])
288 | l == txt "Delay"
289 -> LLazyExp <$> irTerm top vs env arg
291 (P _ (UN l) _, [_, _, arg])
292 | l == txt "Force"
293 -> LForce <$> irTerm top vs env arg
295 (P _ (UN a) _, [_, _, _, arg])
296 | a == txt "assert_smaller"
297 -> irTerm top vs env arg
299 (P _ (UN a) _, [_, arg])
300 | a == txt "assert_total"
301 -> irTerm top vs env arg
303 (P _ (UN p) _, [_, arg])
304 | p == txt "par"
305 -> do arg' <- irTerm top vs env arg
306 return $ LOp LPar [LLazyExp arg']
308 (P _ (UN pf) _, [arg])
309 | pf == txt "prim_fork"
310 -> do arg' <- irTerm top vs env arg
311 return $ LOp LFork [LLazyExp arg']
313 (P _ (UN m) _, [_,size,t])
314 | m == txt "malloc"
315 -> irTerm top vs env t
317 (P _ (UN tm) _, [_,t])
318 | tm == txt "trace_malloc"
319 -> irTerm top vs env t -- TODO
321 -- This case is here until we get more general inlining. It's just
322 -- a really common case, and the laziness hurts...
323 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
324 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
325 | be == txt "ifThenElse"
326 , d == txt "Delay"
327 , d' == txt "Delay"
328 , b == txt "Bool"
329 , p == txt "Prelude"
330 -> do
331 x' <- irTerm top vs env x
332 t' <- irTerm top vs env t
333 e' <- irTerm top vs env e
334 return (LCase Shared x'
335 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
336 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
337 ])
339 -- data constructor
340 (P (DCon t arity _) n _, args) -> do
341 detag <- fgetState (opt_detaggable . ist_optimisation n)
342 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
344 let isNewtype = length used == 1 && detag
345 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
347 -- The following code removes fields from data constructors
348 -- and performs the newtype optimisation.
349 --
350 -- The general rule here is:
351 -- Everything we get as input is not touched by erasure,
352 -- so it conforms to the official arities and types
353 -- and we can reason about it like it's plain TT.
354 --
355 -- It's only the data that leaves this point that's erased
356 -- and possibly no longer typed as the original TT version.
357 --
358 -- Especially, underapplied constructors must yield functions
359 -- even if all the remaining arguments are erased
360 -- (the resulting function *will* be applied, to NULLs).
361 --
362 -- This will probably need rethinking when we get erasure from functions.
364 -- "padLams" will wrap our term in LLam-bdas and give us
365 -- the "list of future unerased args" coming from these lambdas.
366 --
367 -- We can do whatever we like with the list of unerased args,
368 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
369 let padLams = padLambdas used (length args) arity
371 case compare (length args) arity of
373 -- overapplied
374 GT -> ifail ("overapplied data constructor: " ++ show tm ++
375 "\nDEBUG INFO:\n" ++
376 "Arity: " ++ show arity ++ "\n" ++
377 "Arguments: " ++ show args ++ "\n" ++
378 "Pruned arguments: " ++ show argsPruned)
380 -- exactly saturated
381 EQ | isNewtype
382 -> irTerm top vs env (head argsPruned)
384 | otherwise -- not newtype, plain data ctor
385 -> buildApp (LV $ Glob n) argsPruned
387 -- not saturated, underapplied
388 LT | isNewtype -- newtype
389 , length argsPruned == 1 -- and we already have the value
390 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
391 <$> irTerm top vs env (head argsPruned)
393 | isNewtype -- newtype but the value is not among args yet
394 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
396 -- not a newtype, just apply to a constructor
397 | otherwise
398 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
400 -- type constructor
401 (P (TCon t a) n _, args) -> return LNothing
403 -- an external name applied to arguments
404 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
405 LOp (LExternal n) <$> mapM (irTerm top vs env) args
407 -- a name applied to arguments
408 (P _ n _, args) -> do
409 case lookup n (idris_scprims ist) of
410 -- if it's a primitive that is already saturated,
411 -- compile to the corresponding op here already to save work
412 Just (arity, op) | length args == arity
413 -> LOp op <$> mapM (irTerm top vs env) args
415 -- otherwise, just apply the name
416 _ -> applyName n ist args
418 -- turn de bruijn vars into regular named references and try again
419 (V i, args) -> irTerm top vs env $ mkApp (P Bound (env !! i) Erased) args
421 (f, args)
422 -> LApp False
423 <$> irTerm top vs env f
424 <*> mapM (irTerm top vs env) args
426 where
427 buildApp :: LExp -> [Term] -> Idris LExp
428 buildApp e [] = return e
429 buildApp e xs = LApp False e <$> mapM (irTerm top vs env) xs
431 applyToNames :: LExp -> [Name] -> LExp
432 applyToNames tm [] = tm
433 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
435 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
436 padLambdas used startIdx endSIdx mkTerm
437 = LLam allNames $ mkTerm nonerasedNames
438 where
439 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
440 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
442 applyName :: Name -> IState -> [Term] -> Idris LExp
443 applyName n ist args =
444 LApp False (LV $ Glob n) <$> mapM (irTerm top vs env . erase) (zip [0..] args)
445 where
446 erase (i, x)
447 | i >= arity || i `elem` used = x
448 | otherwise = Erased
450 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
451 Just (CaseOp ci ty tys def tot cdefs) -> length tys
452 Just (TyDecl (DCon tag ar _) _) -> ar
453 Just (TyDecl Ref ty) -> length $ getArgTys ty
454 Just (Operator ty ar op) -> ar
455 Just def -> error $ "unknown arity: " ++ show (n, def)
456 Nothing -> 0 -- no definition, probably local name => can't erase anything
458 -- name for purposes of usage info lookup
459 uName
460 | Just n' <- viMethod =<< M.lookup n vs = n'
461 | otherwise = n
463 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
464 fst4 (x,_,_,_,_) = x
466irTerm top vs env (P _ n _) = return $ LV (Glob n)
467irTerm top vs env (V i)
468 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
469 | otherwise = ifail $ "bad de bruijn index: " ++ show i
471irTerm top vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
472 where
473 n' = uniqueName n env
475irTerm top vs env (Bind n (Let _ v) sc)
476 = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc
478irTerm top vs env (Bind _ _ _) = return $ LNothing
480irTerm top vs env (Proj t (-1)) = do
481 t' <- irTerm top vs env t
482 return $ LOp (LMinus (ATInt ITBig))
483 [t', LConst (BI 1)]
485irTerm top vs env (Proj t i) = LProj <$> irTerm top vs env t <*> pure i
486irTerm top vs env (Constant TheWorld) = return LNothing
487irTerm top vs env (Constant c) = return (LConst c)
488irTerm top vs env (TType _) = return LNothing
489irTerm top vs env Erased = return LNothing
490irTerm top vs env Impossible = return LNothing
492doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
493doForeign vs env (ret : fname : world : args)
494 = do args' <- mapM splitArg args
495 let fname' = toFDesc fname
496 let ret' = toFDesc ret
497 return $ LForeign ret' fname' args'
498 where
499 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
500 = do let l' = toFDesc l
501 r' <- irTerm (sMN 0 "__foreignCall") vs env r
502 return (l', r')
503 splitArg _ = ifail "Badly formed foreign function call"
505 toFDesc (Constant (Str str)) = FStr str
506 toFDesc tm
507 | (P _ n _, []) <- unApply tm = FCon (deNS n)
508 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
509 toFDesc _ = FUnknown
511 deNS (NS n _) = n
512 deNS n = n
513doForeign vs env xs = ifail "Badly formed foreign function call"
515irTree :: Name -> [Name] -> SC -> Idris LExp
516irTree top args tree = do
517 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
518 LLam args <$> irSC top M.empty tree
520irSC :: Name -> Vars -> SC -> Idris LExp
521irSC top vs (STerm t) = irTerm top vs [] t
522irSC top vs (UnmatchedCase str) = return $ LError str
524irSC top vs (ProjCase tm alts) = do
525 tm' <- irTerm top vs [] tm
526 alts' <- mapM (irAlt top vs tm') alts
527 return $ LCase Shared tm' alts'
529-- Transform matching on Delay to applications of Force.
530irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
531 | delay == txt "Delay"
532 = do sc' <- irSC top vs sc -- mkForce n' n sc
533 return $ lsubst n' (LForce (LV (Glob n))) sc'
535-- There are two transformations in this case:
536--
537-- 1. Newtype-case elimination:
538-- case {e0} of
539-- wrap({e1}) -> P({e1}) ==> P({e0})
540--
541-- This is important because newtyped constructors are compiled away entirely
542-- and we need to do that everywhere.
543--
544-- 2. Unused-case elimination (only valid for singleton branches):
545-- case {e0} of ==> P
546-- C(x,y) -> P[... x,y not used ...]
547--
548-- This is important for runtime because sometimes we case on irrelevant data:
549--
550-- In the example above, {e0} will most probably have been erased
551-- so this vain projection would make the resulting program segfault
552-- because the code generator still emits a PROJECT(...) G-machine instruction.
553--
554-- Hence, we check whether the variables are used at all
555-- and erase the casesplit if they are not.
556--
557irSC top vs (Case up n [alt]) = do
558 replacement <- case alt of
559 ConCase cn a ns sc -> do
560 detag <- fgetState (opt_detaggable . ist_optimisation cn)
561 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
562 if detag && length used == 1
563 then return . Just $ substSC (ns !! head used) n sc
564 else return Nothing
565 _ -> return Nothing
567 case replacement of
568 Just sc -> irSC top vs sc
569 _ -> do
570 alt' <- irAlt top vs (LV (Glob n)) alt
571 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
572 [] -> subexpr alt' -- strip the unused top-most case
573 _ -> LCase up (LV (Glob n)) [alt']
574 where
575 namesBoundIn :: LAlt -> [Name]
576 namesBoundIn (LConCase cn i ns sc) = ns
577 namesBoundIn (LConstCase c sc) = []
578 namesBoundIn (LDefaultCase sc) = []
580 subexpr :: LAlt -> LExp
581 subexpr (LConCase _ _ _ e) = e
582 subexpr (LConstCase _ e) = e
583 subexpr (LDefaultCase e) = e
585-- FIXME: When we have a non-singleton case-tree of the form
586--
587-- case {e0} of
588-- C(x) => ...
589-- ... => ...
590--
591-- and C is detaggable (the only constructor of the family), we can be sure
592-- that the first branch will be always taken -- so we add special handling
593-- to remove the dead default branch.
594--
595-- If we don't do so and C is newtype-optimisable, we will miss this newtype
596-- transformation and the resulting code will probably segfault.
597--
598-- This work-around is not entirely optimal; the best approach would be
599-- to ensure that such case trees don't arise in the first place.
600--
601irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
602 detag <- fgetState (opt_detaggable . ist_optimisation cn)
603 if detag
604 then irSC top vs (Case up n [ConCase cn a ns sc])
605 else LCase up (LV (Glob n)) <$> mapM (irAlt top vs (LV (Glob n))) alts
607irSC top vs sc@(Case up n alts) = do
608 -- check that neither alternative needs the newtype optimisation,
609 -- see comment above
610 goneWrong <- or <$> mapM isDetaggable alts
611 when goneWrong
612 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
614 -- everything okay
615 LCase up (LV (Glob n)) <$> mapM (irAlt top vs (LV (Glob n))) alts
616 where
617 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
618 isDetaggable _ = return False
620irSC top vs ImpossibleCase = return LNothing
622irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt
624-- this leaves out all unused arguments of the constructor
625irAlt top vs _ (ConCase n t args sc) = do
626 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
627 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
628 LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc
629 where
630 methodVars = case n of
631 SN (InstanceCtorN className)
632 -> M.fromList [(v, VI
633 { viMethod = Just $ mkFieldName n i
634 }) | (v,i) <- zip args [0..]]
635 _
636 -> M.empty -- not an instance constructor
638irAlt top vs _ (ConstCase x rhs)
639 | matchable x = LConstCase x <$> irSC top vs rhs
640 | matchableTy x = LDefaultCase <$> irSC top vs rhs
641 where
642 matchable (I _) = True
643 matchable (BI _) = True
644 matchable (Ch _) = True
645 matchable (Str _) = True
646 matchable (B8 _) = True
647 matchable (B16 _) = True
648 matchable (B32 _) = True
649 matchable (B64 _) = True
650 matchable _ = False
652 matchableTy (AType (ATInt ITNative)) = True
653 matchableTy (AType (ATInt ITBig)) = True
654 matchableTy (AType (ATInt ITChar)) = True
655 matchableTy StrType = True
657 matchableTy (AType (ATInt (ITFixed IT8))) = True
658 matchableTy (AType (ATInt (ITFixed IT16))) = True
659 matchableTy (AType (ATInt (ITFixed IT32))) = True
660 matchableTy (AType (ATInt (ITFixed IT64))) = True
662 matchableTy _ = False
664irAlt top vs tm (SucCase n rhs) = do
665 rhs' <- irSC top vs rhs
666 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
667 [tm,
668 LConst (BI 1)]) rhs')
670irAlt top vs _ (ConstCase c rhs)
671 = ifail $ "Can't match on (" ++ show c ++ ")"
673irAlt top vs _ (DefaultCase rhs)
674 = LDefaultCase <$> irSC top vs rhs