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