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