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