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