git.iko.soy/Idris-dev
on ab2a29f help sign in
Idris-dev/src/IRTS/Compiler.hs
662 lines 24 kB history raw
1{-# LANGUAGE PatternGuards, TypeSynonymInstances, CPP #-}
3module IRTS.Compiler(compile, generate) where
5import IRTS.Lang
6import IRTS.LangOpts
7import IRTS.Defunctionalise
8import IRTS.Simplified
9import IRTS.CodegenCommon
10import IRTS.CodegenC
11import IRTS.CodegenJava
12import IRTS.DumpBC
13import IRTS.CodegenJavaScript
14import IRTS.Inliner
16import Idris.AbsSyntax
17import Idris.AbsSyntaxTree
18import Idris.ASTUtils
19import Idris.Erasure
20import Idris.Error
22import Debug.Trace
24import Idris.Core.TT
25import Idris.Core.Evaluate
26import Idris.Core.CaseTree
28import Control.Category
29import Prelude hiding (id, (.))
31import Control.Applicative
32import Control.Monad.State
33import Data.Maybe
34import Data.List
35import Data.Ord
36import Data.IntSet (IntSet)
37import qualified Data.IntSet as IS
38import qualified Data.Map as M
39import qualified Data.Set as S
40import System.Process
41import System.IO
42import System.Exit
43import System.Directory
44import System.Environment
45import System.FilePath ((</>), addTrailingPathSeparator)
47-- | Given a 'main' term to compiler, return the IRs which can be used to
48-- generate code.
49compile :: Codegen -> FilePath -> Term -> Idris CodegenInfo
50compile codegen f tm
51 = do checkMVs -- check for undefined metavariables
52 checkTotality -- refuse to compile if there are totality problems
53 reachableNames <- performUsageAnalysis
54 maindef <- irMain tm
55 iLOG $ "MAIN: " ++ show maindef
56 objs <- getObjectFiles codegen
57 libs <- getLibs codegen
58 flags <- getFlags codegen
59 hdrs <- getHdrs codegen
60 impdirs <- allImportDirs
61 defsIn <- mkDecls tm reachableNames
62 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
63 -- iputStrLn $ showSep "\n" (map show defs)
64 -- Inlined top level LDecl made here
65 let defsInlined = inlineAll defs
66 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
67 defsInlined
69 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)
70 let ctxtIn = addAlist tagged emptyContext
72 iLOG "Defunctionalising"
73 let defuns_in = defunctionalise nexttag ctxtIn
74 logLvl 5 $ show defuns_in
75 iLOG "Inlining"
76 let defuns = inline defuns_in
77 logLvl 5 $ show defuns
78 iLOG "Resolving variables for CG"
79 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
80 let checked = simplifyDefs defuns (toAlist defuns)
81 outty <- outputTy
82 dumpCases <- getDumpCases
83 dumpDefun <- getDumpDefun
84 case dumpCases of
85 Nothing -> return ()
86 Just f -> runIO $ writeFile f (showCaseTrees defs)
87 case dumpDefun of
88 Nothing -> return ()
89 Just f -> runIO $ writeFile f (dumpDefuns defuns)
90 triple <- Idris.AbsSyntax.targetTriple
91 cpu <- Idris.AbsSyntax.targetCPU
92 iLOG "Building output"
94 case checked of
95 OK c -> do return $ CodegenInfo f outty triple cpu
96 hdrs impdirs objs libs flags
97 NONE c (toAlist defuns)
98 tagged
99-- runIO $ case codegen of
100-- ViaC -> codegenC cginfo
101-- ViaJava -> codegenJava cginfo
102-- ViaJavaScript -> codegenJavaScript cginfo
103-- ViaNode -> codegenNode cginfo
104-- ViaLLVM -> codegenLLVM cginfo
105-- Bytecode -> dumpBC c f
106 Error e -> ierror e
107 where checkMVs = do i <- getIState
108 case map fst (idris_metavars i) \\ primDefs of
109 [] -> return ()
110 ms -> ifail $ "There are undefined metavariables: " ++ show ms
111 checkTotality = do i <- getIState
112 case idris_totcheckfail i of
113 [] -> return ()
114 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
115 inDir d h = do let f = d </> h
116 ex <- doesFileExist f
117 if ex then return f else return h
119generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
120generate codegen mainmod ir
121 = case codegen of
122 -- Built-in code generators (FIXME: lift these out!)
123 Via "c" -> codegenC ir
124 Via "java" -> codegenJava ir
125 -- Any external code generator
126 Via cg -> do let cmd = "idris-" ++ cg ++ " " ++ mainmod ++
127 " -o " ++ outputFile ir
128 exit <- system cmd
129 when (exit /= ExitSuccess) $
130 putStrLn ("FAILURE: " ++ show cmd)
131 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
133irMain :: TT Name -> Idris LDecl
134irMain tm = do
135 i <- irTerm M.empty [] tm
136 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
138mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
139mkDecls t used
140 = do i <- getIState
141 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
142 decls <- mapM build ds
143 return decls
145showCaseTrees :: [(Name, LDecl)] -> String
146showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
147 where
148 showCT (n, LFun _ f args lexp)
149 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
150 ++ show lexp
151 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
153 defnRank :: (Name, LDecl) -> String
154 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
155 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
157 nameRank :: Name -> String
158 nameRank (UN s) = "1" ++ show s
159 nameRank (MN i s) = "2" ++ show s ++ show i
160 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
161 nameRank (SN sn) = "4" ++ snRank sn
162 nameRank n = "5" ++ show n
164 snRank :: SpecialName -> String
165 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
166 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
167 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
168 snRank (MethodN n) = "4" ++ nameRank n
169 snRank (CaseN n) = "5" ++ nameRank n
170 snRank (ElimN n) = "6" ++ nameRank n
171 snRank (InstanceCtorN n) = "7" ++ nameRank n
172 snRank (WithN i n) = "8" ++ nameRank n ++ show i
174isCon (TyDecl _ _) = True
175isCon _ = False
177build :: (Name, Def) -> Idris (Name, LDecl)
178build (n, d)
179 = do i <- getIState
180 case lookup n (idris_scprims i) of
181 Just (ar, op) ->
182 let args = map (\x -> sMN x "op") [0..] in
183 return (n, (LFun [] n (take ar args)
184 (LOp op (map (LV . Glob) (take ar args)))))
185 _ -> do def <- mkLDecl n d
186 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
187 return (n, def)
189declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
190declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
192mkLDecl n (Function tm _)
193 = declArgs [] True n <$> irTerm M.empty [] tm
195mkLDecl n (CaseOp ci _ _ _ pats cd)
196 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc
197 where
198 (args, sc) = cases_runtime cd
200 -- Always attempt to inline functions arising from 'case' expressions
201 caseName (SN (CaseN _)) = True
202 caseName (SN (WithN _ _)) = True
203 caseName (NS n _) = caseName n
204 caseName _ = False
206mkLDecl n (TyDecl (DCon tag arity _) _) =
207 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
209mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
210mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
212data VarInfo = VI
213 { viMethod :: Maybe Name
214 }
215 deriving Show
217type Vars = M.Map Name VarInfo
219irTerm :: Vars -> [Name] -> Term -> Idris LExp
220irTerm vs env tm@(App f a) = case unApply tm of
221 (P _ (UN m) _, args)
222 | m == txt "mkForeignPrim"
223 -> doForeign vs env args
225 (P _ (UN u) _, [_, arg])
226 | u == txt "unsafePerformPrimIO"
227 -> irTerm vs env arg
229 -- TMP HACK - until we get inlining.
230 (P _ (UN r) _, [_, _, _, _, _, arg])
231 | r == txt "replace"
232 -> irTerm vs env arg
234 -- Laziness, the old way
235 (P _ (UN l) _, [_, arg])
236 | l == txt "lazy"
237 -> error "lazy has crept in somehow"
239 (P _ (UN l) _, [_, arg])
240 | l == txt "force"
241 -> LForce <$> irTerm vs env arg
243 -- Laziness, the new way
244 (P _ (UN l) _, [_, _, arg])
245 | l == txt "Delay"
246 -> LLazyExp <$> irTerm vs env arg
248 (P _ (UN l) _, [_, _, arg])
249 | l == txt "Force"
250 -> LForce <$> irTerm vs env arg
252 (P _ (UN a) _, [_, _, _, arg])
253 | a == txt "assert_smaller"
254 -> irTerm vs env arg
256 (P _ (UN a) _, [_, arg])
257 | a == txt "assert_total"
258 -> irTerm vs env arg
260 (P _ (UN p) _, [_, arg])
261 | p == txt "par"
262 -> do arg' <- irTerm vs env arg
263 return $ LOp LPar [LLazyExp arg']
265 (P _ (UN pf) _, [arg])
266 | pf == txt "prim_fork"
267 -> do arg' <- irTerm vs env arg
268 return $ LOp LFork [LLazyExp arg']
270 (P _ (UN m) _, [_,size,t])
271 | m == txt "malloc"
272 -> irTerm vs env t
274 (P _ (UN tm) _, [_,t])
275 | tm == txt "trace_malloc"
276 -> irTerm vs env t -- TODO
278 -- This case is here until we get more general inlining. It's just
279 -- a really common case, and the laziness hurts...
280 (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),
281 (App (App (App (P _ (UN d') _) _) _) e)])
282 | be == txt "boolElim"
283 , d == txt "Delay"
284 , d' == txt "Delay"
285 -> do
286 x' <- irTerm vs env x
287 t' <- irTerm vs env t
288 e' <- irTerm vs env e
289 return (LCase Shared x'
290 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
291 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
292 ])
294 -- data constructor
295 (P (DCon t arity _) n _, args) -> do
296 detag <- fgetState (opt_detaggable . ist_optimisation n)
297 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
299 let isNewtype = length used == 1 && detag
300 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
302 -- The following code removes fields from data constructors
303 -- and performs the newtype optimisation.
304 --
305 -- The general rule here is:
306 -- Everything we get as input is not touched by erasure,
307 -- so it conforms to the official arities and types
308 -- and we can reason about it like it's plain TT.
309 --
310 -- It's only the data that leaves this point that's erased
311 -- and possibly no longer typed as the original TT version.
312 --
313 -- Especially, underapplied constructors must yield functions
314 -- even if all the remaining arguments are erased
315 -- (the resulting function *will* be applied, to NULLs).
316 --
317 -- This will probably need rethinking when we get erasure from functions.
319 -- "padLams" will wrap our term in LLam-bdas and give us
320 -- the "list of future unerased args" coming from these lambdas.
321 --
322 -- We can do whatever we like with the list of unerased args,
323 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
324 let padLams = padLambdas used (length args) arity
326 case compare (length args) arity of
328 -- overapplied
329 GT -> ifail ("overapplied data constructor: " ++ show tm)
331 -- exactly saturated
332 EQ | isNewtype
333 -> irTerm vs env (head argsPruned)
335 | otherwise -- not newtype, plain data ctor
336 -> buildApp (LV $ Glob n) argsPruned
338 -- not saturated, underapplied
339 LT | isNewtype -- newtype
340 , length argsPruned == 1 -- and we already have the value
341 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
342 <$> irTerm vs env (head argsPruned)
344 | isNewtype -- newtype but the value is not among args yet
345 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
347 -- not a newtype, just apply to a constructor
348 | otherwise
349 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
351 -- type constructor
352 (P (TCon t a) n _, args) -> return LNothing
354 -- a name applied to arguments
355 (P _ n _, args) -> do
356 ist <- getIState
357 case lookup n (idris_scprims ist) of
358 -- if it's a primitive that is already saturated,
359 -- compile to the corresponding op here already to save work
360 Just (arity, op) | length args == arity
361 -> LOp op <$> mapM (irTerm vs env) args
363 -- otherwise, just apply the name
364 _ -> applyName n ist args
366 -- turn de bruijn vars into regular named references and try again
367 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
369 (f, args)
370 -> LApp False
371 <$> irTerm vs env f
372 <*> mapM (irTerm vs env) args
374 where
375 buildApp :: LExp -> [Term] -> Idris LExp
376 buildApp e [] = return e
377 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
379 applyToNames :: LExp -> [Name] -> LExp
380 applyToNames tm [] = tm
381 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
383 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
384 padLambdas used startIdx endSIdx mkTerm
385 = LLam allNames $ mkTerm nonerasedNames
386 where
387 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
388 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
390 applyName :: Name -> IState -> [Term] -> Idris LExp
391 applyName n ist args =
392 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
393 where
394 erase (i, x)
395 | i >= arity || i `elem` used = x
396 | otherwise = Erased
398 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
399 Just (CaseOp ci ty tys def tot cdefs) -> length tys
400 Just (TyDecl (DCon tag ar _) _) -> ar
401 Just (TyDecl Ref ty) -> length $ getArgTys ty
402 Just (Operator ty ar op) -> ar
403 Just def -> error $ "unknown arity: " ++ show (n, def)
404 Nothing -> 0 -- no definition, probably local name => can't erase anything
406 -- name for purposes of usage info lookup
407 uName
408 | Just n' <- viMethod =<< M.lookup n vs = n'
409 | otherwise = n
411 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
412 fst4 (x,_,_,_) = x
414irTerm vs env (P _ n _) = return $ LV (Glob n)
415irTerm vs env (V i)
416 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
417 | otherwise = ifail $ "bad de bruijn index: " ++ show i
419irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
420 where
421 n' = uniqueName n env
423irTerm vs env (Bind n (Let _ v) sc)
424 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
426irTerm vs env (Bind _ _ _) = return $ LNothing
428irTerm vs env (Proj t (-1)) = do
429 t' <- irTerm vs env t
430 return $ LOp (LMinus (ATInt ITBig))
431 [t', LConst (BI 1)]
433irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
434irTerm vs env (Constant c) = return $ LConst c
435irTerm vs env (TType _) = return $ LNothing
436irTerm vs env Erased = return $ LNothing
437irTerm vs env Impossible = return $ LNothing
439doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
440doForeign vs env (_ : fgn : args)
441 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
442 = case getFTypes fgnArgTys of
443 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
444 Just tys -> do
445 args' <- mapM (irTerm vs env) (init args)
446 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
448 | otherwise = ifail "Badly formed foreign function call"
449 where
450 getFTypes :: TT Name -> Maybe [FType]
451 getFTypes tm = case unApply tm of
452 -- nil : {a : Type} -> List a
453 (nil, [_]) -> Just []
454 -- cons : {a : Type} -> a -> List a -> List a
455 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
456 _ -> Nothing
458 mkIty' (P _ (UN ty) _) = mkIty (str ty)
459 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
460 | fi == txt "FIntT"
461 = mkIntIty (str intTy)
463 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
464 | ff == txt "FFunction"
465 , fa == txt "FAny"
466 , io == txt "IO"
467 = FFunctionIO
469 mkIty' (App (App (P _ (UN ff) _) _) _)
470 | ff == txt "FFunction"
471 = FFunction
473 mkIty' _ = FAny
475 -- would be better if these FInt types were evaluated at compile time
476 -- TODO: add %eval directive for such things
478 mkIty "FFloat" = FArith ATFloat
479 mkIty "FInt" = mkIntIty "ITNative"
480 mkIty "FChar" = mkIntIty "ITChar"
481 mkIty "FByte" = mkIntIty "IT8"
482 mkIty "FShort" = mkIntIty "IT16"
483 mkIty "FLong" = mkIntIty "IT64"
484 mkIty "FBits8" = mkIntIty "IT8"
485 mkIty "FBits16" = mkIntIty "IT16"
486 mkIty "FBits32" = mkIntIty "IT32"
487 mkIty "FBits64" = mkIntIty "IT64"
488 mkIty "FString" = FString
489 mkIty "FPtr" = FPtr
490 mkIty "FManagedPtr" = FManagedPtr
491 mkIty "FUnit" = FUnit
492 mkIty "FFunction" = FFunction
493 mkIty "FFunctionIO" = FFunctionIO
494 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
495 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
496 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
497 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
498 mkIty x = error $ "Unknown type " ++ x
500 mkIntIty "ITNative" = FArith (ATInt ITNative)
501 mkIntIty "ITChar" = FArith (ATInt ITChar)
502 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
503 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
504 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
505 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
507irTree :: [Name] -> SC -> Idris LExp
508irTree args tree = do
509 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
510 LLam args <$> irSC M.empty tree
512irSC :: Vars -> SC -> Idris LExp
513irSC vs (STerm t) = irTerm vs [] t
514irSC vs (UnmatchedCase str) = return $ LError str
516irSC vs (ProjCase tm alts) = do
517 tm' <- irTerm vs [] tm
518 alts' <- mapM (irAlt vs tm') alts
519 return $ LCase Shared tm' alts'
521-- Transform matching on Delay to applications of Force.
522irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
523 | delay == txt "Delay"
524 = do sc' <- irSC vs $ mkForce n' n sc
525 return $ LLet n' (LForce (LV (Glob n))) sc'
527-- There are two transformations in this case:
528--
529-- 1. Newtype-case elimination:
530-- case {e0} of
531-- wrap({e1}) -> P({e1}) ==> P({e0})
532--
533-- This is important because newtyped constructors are compiled away entirely
534-- and we need to do that everywhere.
535--
536-- 2. Unused-case elimination (only valid for singleton branches):
537-- case {e0} of ==> P
538-- C(x,y) -> P[... x,y not used ...]
539--
540-- This is important for runtime because sometimes we case on irrelevant data:
541--
542-- In the example above, {e0} will most probably have been erased
543-- so this vain projection would make the resulting program segfault
544-- because the code generator still emits a PROJECT(...) G-machine instruction.
545--
546-- Hence, we check whether the variables are used at all
547-- and erase the casesplit if they are not.
548--
549irSC vs (Case up n [alt]) = do
550 replacement <- case alt of
551 ConCase cn a ns sc -> do
552 detag <- fgetState (opt_detaggable . ist_optimisation cn)
553 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
554 if detag && length used == 1
555 then return . Just $ substSC (ns !! head used) n sc
556 else return Nothing
557 _ -> return Nothing
559 case replacement of
560 Just sc -> irSC vs sc
561 _ -> do
562 alt' <- irAlt vs (LV (Glob n)) alt
563 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
564 [] -> subexpr alt' -- strip the unused top-most case
565 _ -> LCase up (LV (Glob n)) [alt']
566 where
567 namesBoundIn :: LAlt -> [Name]
568 namesBoundIn (LConCase cn i ns sc) = ns
569 namesBoundIn (LConstCase c sc) = []
570 namesBoundIn (LDefaultCase sc) = []
572 subexpr :: LAlt -> LExp
573 subexpr (LConCase _ _ _ e) = e
574 subexpr (LConstCase _ e) = e
575 subexpr (LDefaultCase e) = e
577-- FIXME: When we have a non-singleton case-tree of the form
578--
579-- case {e0} of
580-- C(x) => ...
581-- ... => ...
582--
583-- and C is detaggable (the only constructor of the family), we can be sure
584-- that the first branch will be always taken -- so we add special handling
585-- to remove the dead default branch.
586--
587-- If we don't do so and C is newtype-optimisable, we will miss this newtype
588-- transformation and the resulting code will probably segfault.
589--
590-- This work-around is not entirely optimal; the best approach would be
591-- to ensure that such case trees don't arise in the first place.
592--
593irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
594 detag <- fgetState (opt_detaggable . ist_optimisation cn)
595 if detag
596 then irSC vs (Case up n [ConCase cn a ns sc])
597 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
599irSC vs sc@(Case up n alts) = do
600 -- check that neither alternative needs the newtype optimisation,
601 -- see comment above
602 goneWrong <- or <$> mapM isDetaggable alts
603 when goneWrong
604 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
606 -- everything okay
607 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
608 where
609 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
610 isDetaggable _ = return False
612irSC vs ImpossibleCase = return LNothing
614irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
616-- this leaves out all unused arguments of the constructor
617irAlt vs _ (ConCase n t args sc) = do
618 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
619 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
620 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
621 where
622 methodVars = case n of
623 SN (InstanceCtorN className)
624 -> M.fromList [(v, VI
625 { viMethod = Just $ mkFieldName n i
626 }) | (v,i) <- zip args [0..]]
627 _
628 -> M.empty -- not an instance constructor
630irAlt vs _ (ConstCase x rhs)
631 | matchable x = LConstCase x <$> irSC vs rhs
632 | matchableTy x = LDefaultCase <$> irSC vs rhs
633 where
634 matchable (I _) = True
635 matchable (BI _) = True
636 matchable (Ch _) = True
637 matchable (Str _) = True
638 matchable _ = False
640 matchableTy (AType (ATInt ITNative)) = True
641 matchableTy (AType (ATInt ITBig)) = True
642 matchableTy (AType (ATInt ITChar)) = True
643 matchableTy StrType = True
645 matchableTy (AType (ATInt (ITFixed IT8))) = True
646 matchableTy (AType (ATInt (ITFixed IT16))) = True
647 matchableTy (AType (ATInt (ITFixed IT32))) = True
648 matchableTy (AType (ATInt (ITFixed IT64))) = True
650 matchableTy _ = False
652irAlt vs tm (SucCase n rhs) = do
653 rhs' <- irSC vs rhs
654 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
655 [tm,
656 LConst (BI 1)]) rhs')
658irAlt vs _ (ConstCase c rhs)
659 = ifail $ "Can't match on (" ++ show c ++ ")"
661irAlt vs _ (DefaultCase rhs)
662 = LDefaultCase <$> irSC vs rhs