git.iko.soy/Idris-dev
on 0b669c7 help sign in
Idris-dev/src/IRTS/Compiler.hs
688 lines 26 kB history raw
1{-|
2Module : IRTS.Compiler
3Description : Coordinates the compilation process.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}
10module IRTS.Compiler(compile, generate) where
12import Idris.AbsSyntax
13import Idris.ASTUtils
14import Idris.Core.CaseTree
15import Idris.Core.Evaluate
16import Idris.Core.TT
17import Idris.Erasure
18import Idris.Error
19import Idris.Options
20import Idris.Output
21import IRTS.CodegenC
22import IRTS.CodegenCommon
23import IRTS.Defunctionalise
24import IRTS.DumpBC
25import IRTS.Exports
26import IRTS.Inliner
27import IRTS.LangOpts
28import IRTS.Portable
29import IRTS.Simplified
31import Prelude hiding (id, (.))
33import Control.Category
34import Control.Monad.State
35import Data.List
36import qualified Data.Map as M
37import Data.Ord
38import qualified Data.Set as S
39import System.Directory
40import System.Exit
41import System.IO
42import System.Process
44-- | Compile to simplified forms and return CodegenInfo
45compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
46compile codegen f mtm = do
47 logCodeGen 1 "Compiling Output."
48 iReport 2 "Compiling Output."
49 checkMVs -- check for undefined metavariables
50 checkTotality -- refuse to compile if there are totality problems
51 exports <- findExports
52 let rootNames = case mtm of
53 Nothing -> []
54 Just t -> freeNames t
56 logCodeGen 1 "Running Erasure Analysis"
57 iReport 3 "Running Erasure Analysis"
58 reachableNames <- performUsageAnalysis
59 (rootNames ++ getExpNames exports)
60 maindef <- case mtm of
61 Nothing -> return []
62 Just tm -> do md <- irMain tm
63 logCodeGen 1 $ "MAIN: " ++ show md
64 return [(sMN 0 "runMain", md)]
65 objs <- getObjectFiles codegen
66 libs <- getLibs codegen
67 flags <- getFlags codegen
68 hdrs <- getHdrs codegen
69 impdirs <- rankedImportDirs f
70 ttDeclarations <- getDeclarations reachableNames
71 defsIn <- mkDecls reachableNames
72 -- if no 'main term' given, generate interface files
73 let iface = case mtm of
74 Nothing -> True
75 Just _ -> False
77 let defs = defsIn ++ maindef
79 -- Inlined top level LDecl made here
80 let defsInlined = inlineAll defs
81 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
82 defsInlined
84 logCodeGen 1 "Inlining"
86 dumpCases <- getDumpCases
87 case dumpCases of
88 Nothing -> return ()
89 Just f -> runIO $ writeFile f (showCaseTrees defsUniq)
91 let (nexttag, tagged) = addTags 65536 (liftAll defsInlined)
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 dumpDefun <- getDumpDefun
107 case dumpDefun of
108 Nothing -> return ()
109 Just f -> runIO $ writeFile f (dumpDefuns defuns)
110 triple <- Idris.AbsSyntax.targetTriple
111 cpu <- Idris.AbsSyntax.targetCPU
112 logCodeGen 1 "Generating Code."
113 iReport 2 "Generating Code."
114 case checked of
115 OK c -> do return $ CodegenInfo f outty triple cpu
116 hdrs impdirs objs libs flags
117 NONE c (toAlist defuns)
118 tagged iface exports
119 ttDeclarations
120 Error e -> ierror e
121 where checkMVs = do i <- getIState
122 case map fst (idris_metavars i) \\ primDefs of
123 [] -> return ()
124 ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
125 iputStrLn "\nEvaluation of any of these will crash at run time."
126 return ()
127 checkTotality = do i <- getIState
128 case idris_totcheckfail i of
129 [] -> return ()
130 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
132generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
133generate codegen mainmod ir
134 = case codegen of
135 -- Built-in code generators (FIXME: lift these out!)
136 Via _ "c" -> codegenC ir
137 -- Any external code generator
138 Via fm cg -> do input <- case fm of
139 IBCFormat -> return mainmod
140 JSONFormat -> do
141 tempdir <- getTemporaryDirectory
142 (fn, h) <- openTempFile tempdir "idris-cg.json"
143 writePortable h ir
144 hClose h
145 return fn
146 let cmd = "idris-codegen-" ++ cg
147 args = [input, "-o", outputFile ir] ++ compilerFlags ir
148 exit <- rawSystem cmd (if interfaces ir then "--interface" : args else args)
149 when (exit /= ExitSuccess) $
150 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
151 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
153irMain :: TT Name -> Idris LDecl
154irMain tm = do
155 i <- irTerm (sMN 0 "runMain") M.empty [] tm
156 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
158mkDecls :: [Name] -> Idris [(Name, LDecl)]
159mkDecls used
160 = do i <- getIState
161 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
162 decls <- mapM build ds
163 return decls
165getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
166getDeclarations used
167 = do i <- getIState
168 let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)
169 return ds
171showCaseTrees :: [(Name, LDecl)] -> String
172showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
173 where
174 showCT (n, LFun opts f args lexp)
175 = showOpts ++
176 show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
177 ++ show lexp
178 where
179 showOpts | Inline `elem` opts = "%inline "
180 | otherwise = ""
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 (ImplementationCtorN n) = "7" ++ nameRank n
201 snRank (WithN i n) = "8" ++ nameRank n ++ show i
203isCon (TyDecl _ _) = True
204isCon _ = False
206build :: (Name, Def) -> Idris (Name, LDecl)
207build (n, d)
208 = do i <- getIState
209 case getPrim n i of
210 Just (ar, op) ->
211 let args = map (\x -> sMN x "op") [0..] in
212 return (n, (LFun [] n (take ar args)
213 (LOp op (map LV (take ar args)))))
214 _ -> do def <- mkLDecl n d
215 logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
216 return (n, def)
217 where getPrim n i
218 | Just (ar, op) <- lookup n (idris_scprims i)
219 = Just (ar, op)
220 | Just ar <- lookup n (S.toList (idris_externs i))
221 = Just (ar, LExternal n)
222 getPrim n i = Nothing
224declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
225declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
227mkLDecl n (Function tm _)
228 = declArgs [] True n <$> irTerm n M.empty [] tm
230mkLDecl n (CaseOp ci _ _ _ pats cd)
231 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree n args sc
232 where
233 (args, sc) = cases_runtime cd
235 -- Always attempt to inline functions arising from 'case' expressions
236 caseName (SN (CaseN _ _)) = True
237 caseName (SN (WithN _ _)) = True
238 caseName (NS n _) = caseName n
239 caseName _ = False
241mkLDecl n (TyDecl (DCon tag arity _) _) =
242 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
244mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
245mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
247data VarInfo = VI
248 { viMethod :: Maybe Name
249 }
250 deriving Show
252type Vars = M.Map Name VarInfo
254irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
255irTerm top vs env tm@(App _ f a) = do
256 ist <- getIState
257 case unApply tm of
258 (P _ n _, args)
259 | n `elem` map fst (idris_metavars ist) \\ primDefs
260 -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
261 (P _ (UN m) _, args)
262 | m == txt "mkForeignPrim"
263 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
265 (P _ (UN u) _, [_, arg])
266 | u == txt "unsafePerformPrimIO"
267 -> irTerm top vs env arg
269 (P _ (UN u) _, _)
270 | u == txt "assert_unreachable"
271 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top
273 (P _ (UN u) _, [_, msg])
274 | u == txt "idris_crash"
275 -> do msg' <- irTerm top vs env msg
276 return $ LOp LCrash [msg']
278 -- TMP HACK - until we get inlining.
279 (P _ (UN r) _, [_, _, _, _, _, arg])
280 | r == txt "replace"
281 -> irTerm top vs env arg
283 -- 'void' doesn't have any pattern clauses and only gets called on
284 -- erased things in higher order contexts (also a TMP HACK...)
285 (P _ (UN r) _, _)
286 | r == txt "void"
287 -> return LNothing
289 -- Laziness, the old way
290 (P _ (UN l) _, [_, arg])
291 | l == txt "lazy"
292 -> error "lazy has crept in somehow"
294 (P _ (UN l) _, [_, arg])
295 | l == txt "force"
296 -> LForce <$> irTerm top vs env arg
298 -- Laziness, the new way
299 (P _ (UN l) _, [_, _, arg])
300 | l == txt "Delay"
301 -> LLazyExp <$> irTerm top vs env arg
303 (P _ (UN l) _, [_, _, arg])
304 | l == txt "Force"
305 -> LForce <$> irTerm top vs env arg
307 (P _ (UN a) _, [_, _, _, arg])
308 | a == txt "assert_smaller"
309 -> irTerm top vs env arg
311 (P _ (UN a) _, [_, arg])
312 | a == txt "assert_total"
313 -> irTerm top vs env arg
315 (P _ (UN p) _, [_, arg])
316 | p == txt "par"
317 -> do arg' <- irTerm top vs env arg
318 return $ LOp LPar [LLazyExp arg']
320 (P _ (UN pf) _, [arg])
321 | pf == txt "prim_fork"
322 -> do arg' <- irTerm top vs env arg
323 return $ LOp LFork [LLazyExp arg']
325 (P _ (UN m) _, [_,size,t])
326 | m == txt "malloc"
327 -> irTerm top vs env t
329 (P _ (UN tm) _, [_,t])
330 | tm == txt "trace_malloc"
331 -> irTerm top vs env t -- TODO
333 -- This case is here until we get more general inlining. It's just
334 -- a really common case, and the laziness hurts...
335 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
336 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
337 | be == txt "ifThenElse"
338 , d == txt "Delay"
339 , d' == txt "Delay"
340 , b == txt "Bool"
341 , p == txt "Prelude"
342 -> do
343 x' <- irTerm top vs env x
344 t' <- irTerm top vs env t
345 e' <- irTerm top vs env e
346 return (LCase Shared x'
347 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
348 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
349 ])
351 -- data constructor
352 (P (DCon t arity _) n _, args) -> do
353 detag <- fgetState (opt_detaggable . ist_optimisation n)
354 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
356 let isNewtype = length used == 1 && detag
357 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
359 -- The following code removes fields from data constructors
360 -- and performs the newtype optimisation.
361 --
362 -- The general rule here is:
363 -- Everything we get as input is not touched by erasure,
364 -- so it conforms to the official arities and types
365 -- and we can reason about it like it's plain TT.
366 --
367 -- It's only the data that leaves this point that's erased
368 -- and possibly no longer typed as the original TT version.
369 --
370 -- Especially, underapplied constructors must yield functions
371 -- even if all the remaining arguments are erased
372 -- (the resulting function *will* be applied, to NULLs).
373 --
374 -- This will probably need rethinking when we get erasure from functions.
376 -- "padLams" will wrap our term in LLam-bdas and give us
377 -- the "list of future unerased args" coming from these lambdas.
378 --
379 -- We can do whatever we like with the list of unerased args,
380 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
381 let padLams = padLambdas used (length args) arity
383 case compare (length args) arity of
385 -- overapplied
386 GT -> ifail ("overapplied data constructor: " ++ show tm ++
387 "\nDEBUG INFO:\n" ++
388 "Arity: " ++ show arity ++ "\n" ++
389 "Arguments: " ++ show args ++ "\n" ++
390 "Pruned arguments: " ++ show argsPruned)
392 -- exactly saturated
393 EQ | isNewtype
394 -> irTerm top vs env (head argsPruned)
396 | otherwise -- not newtype, plain data ctor
397 -> buildApp (LV n) argsPruned
399 -- not saturated, underapplied
400 LT | isNewtype -- newtype
401 , length argsPruned == 1 -- and we already have the value
402 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
403 <$> irTerm top vs env (head argsPruned)
405 | isNewtype -- newtype but the value is not among args yet
406 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
408 -- not a newtype, just apply to a constructor
409 | otherwise
410 -> padLams . applyToNames <$> buildApp (LV n) argsPruned
412 -- type constructor
413 (P (TCon t a) n _, args) -> return LNothing
415 -- an external name applied to arguments
416 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
417 LOp (LExternal n) <$> mapM (irTerm top vs env) args
419 -- a name applied to arguments
420 (P _ n _, args) -> do
421 case lookup n (idris_scprims ist) of
422 -- if it's a primitive that is already saturated,
423 -- compile to the corresponding op here already to save work
424 Just (arity, op) | length args == arity
425 -> LOp op <$> mapM (irTerm top vs env) args
427 -- otherwise, just apply the name
428 _ -> applyName n ist args
430 -- turn de bruijn vars into regular named references and try again
431 (V i, args) -> irTerm top vs env $ mkApp (P Bound (env !! i) Erased) args
433 (f, args)
434 -> LApp False
435 <$> irTerm top vs env f
436 <*> mapM (irTerm top vs env) args
438 where
439 buildApp :: LExp -> [Term] -> Idris LExp
440 buildApp e [] = return e
441 buildApp e xs = LApp False e <$> mapM (irTerm top vs env) xs
443 applyToNames :: LExp -> [Name] -> LExp
444 applyToNames tm [] = tm
445 applyToNames tm ns = LApp False tm $ map LV ns
447 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
448 padLambdas used startIdx endSIdx mkTerm
449 = LLam allNames $ mkTerm nonerasedNames
450 where
451 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
452 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
454 applyName :: Name -> IState -> [Term] -> Idris LExp
455 applyName n ist args =
456 LApp False (LV n) <$> mapM (irTerm top vs env . erase) (zip [0..] args)
457 where
458 erase (i, x)
459 | i >= arity || i `elem` used = x
460 | otherwise = Erased
462 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
463 Just (CaseOp ci ty tys def tot cdefs) -> length tys
464 Just (TyDecl (DCon tag ar _) _) -> ar
465 Just (TyDecl Ref ty) -> length $ getArgTys ty
466 Just (Operator ty ar op) -> ar
467 Just def -> error $ "unknown arity: " ++ show (n, def)
468 Nothing -> 0 -- no definition, probably local name => can't erase anything
470 -- name for purposes of usage info lookup
471 uName
472 | Just n' <- viMethod =<< M.lookup n vs = n'
473 | otherwise = n
475 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
476 fst4 (x,_,_,_,_,_) = x
478irTerm top vs env (P _ n _) = return $ LV n
479irTerm top vs env (V i)
480 | i >= 0 && i < length env = return $ LV (env!!i)
481 | otherwise = ifail $ "bad de bruijn index: " ++ show i
483irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
484 where
485 n' = uniqueName n env
487irTerm top vs env (Bind n (Let _ _ v) sc)
488 = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc
490irTerm top vs env (Bind _ _ _) = return $ LNothing
492irTerm top vs env (Proj t (-1)) = do
493 t' <- irTerm top vs env t
494 return $ LOp (LMinus (ATInt ITBig))
495 [t', LConst (BI 1)]
497irTerm top vs env (Proj t i) = LProj <$> irTerm top vs env t <*> pure i
498irTerm top vs env (Constant TheWorld) = return LNothing
499irTerm top vs env (Constant c) = return (LConst c)
500irTerm top vs env (TType _) = return LNothing
501irTerm top vs env Erased = return LNothing
502irTerm top vs env Impossible = return LNothing
504doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
505doForeign vs env (ret : fname : world : args)
506 = do args' <- mapM splitArg args
507 let fname' = toFDesc fname
508 let ret' = toFDesc ret
509 return $ LForeign ret' fname' args'
510 where
511 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
512 = do let l' = toFDesc l
513 r' <- irTerm (sMN 0 "__foreignCall") vs env r
514 return (l', r')
515 splitArg _ = ifail $ "Badly formed foreign function call: " ++
516 show (ret : fname : world : args)
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 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 n) alt
585 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
586 [] -> subexpr alt' -- strip the unused top-most case
587 _ -> LCase up (LV 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 n) <$> mapM (irAlt top vs (LV 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 n) <$> mapM (irAlt top vs (LV 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