git.iko.soy/Idris-dev
on 30580db help sign in
Idris-dev/src/IRTS/Compiler.hs
663 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 optimise <- optLevel
93 iLOG "Building output"
95 case checked of
96 OK c -> do return $ CodegenInfo f outty triple cpu optimise
97 hdrs impdirs objs libs flags
98 NONE c (toAlist defuns)
99 tagged
100-- runIO $ case codegen of
101-- ViaC -> codegenC cginfo
102-- ViaJava -> codegenJava cginfo
103-- ViaJavaScript -> codegenJavaScript cginfo
104-- ViaNode -> codegenNode cginfo
105-- ViaLLVM -> codegenLLVM cginfo
106-- Bytecode -> dumpBC c f
107 Error e -> ierror e
108 where checkMVs = do i <- getIState
109 case map fst (idris_metavars i) \\ primDefs of
110 [] -> return ()
111 ms -> ifail $ "There are undefined metavariables: " ++ show ms
112 checkTotality = do i <- getIState
113 case idris_totcheckfail i of
114 [] -> return ()
115 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
116 inDir d h = do let f = d </> h
117 ex <- doesFileExist f
118 if ex then return f else return h
120generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
121generate codegen mainmod ir
122 = case codegen of
123 -- Built-in code generators (FIXME: lift these out!)
124 Via "c" -> codegenC ir
125 Via "java" -> codegenJava ir
126 -- Any external code generator
127 Via cg -> do let cmd = "idris-" ++ cg ++ " " ++ mainmod ++
128 " -o " ++ outputFile ir
129 exit <- system cmd
130 when (exit /= ExitSuccess) $
131 putStrLn ("FAILURE: " ++ show cmd)
132 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
134irMain :: TT Name -> Idris LDecl
135irMain tm = do
136 i <- irTerm M.empty [] tm
137 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
139mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
140mkDecls t used
141 = do i <- getIState
142 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
143 decls <- mapM build ds
144 return decls
146showCaseTrees :: [(Name, LDecl)] -> String
147showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
148 where
149 showCT (n, LFun _ f args lexp)
150 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
151 ++ show lexp
152 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
154 defnRank :: (Name, LDecl) -> String
155 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
156 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
158 nameRank :: Name -> String
159 nameRank (UN s) = "1" ++ show s
160 nameRank (MN i s) = "2" ++ show s ++ show i
161 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
162 nameRank (SN sn) = "4" ++ snRank sn
163 nameRank n = "5" ++ show n
165 snRank :: SpecialName -> String
166 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
167 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
168 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
169 snRank (MethodN n) = "4" ++ nameRank n
170 snRank (CaseN n) = "5" ++ nameRank n
171 snRank (ElimN n) = "6" ++ nameRank n
172 snRank (InstanceCtorN n) = "7" ++ nameRank n
173 snRank (WithN i n) = "8" ++ nameRank n ++ show i
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 || caseName n) n <$> irTree args sc
198 where
199 (args, sc) = cases_runtime cd
201 -- Always attempt to inline functions arising from 'case' expressions
202 caseName (SN (CaseN _)) = True
203 caseName (SN (WithN _ _)) = True
204 caseName (NS n _) = caseName n
205 caseName _ = False
207mkLDecl n (TyDecl (DCon tag arity _) _) =
208 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
210mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
211mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
213data VarInfo = VI
214 { viMethod :: Maybe Name
215 }
216 deriving Show
218type Vars = M.Map Name VarInfo
220irTerm :: Vars -> [Name] -> Term -> Idris LExp
221irTerm vs env tm@(App f a) = case unApply tm of
222 (P _ (UN m) _, args)
223 | m == txt "mkForeignPrim"
224 -> doForeign vs env args
226 (P _ (UN u) _, [_, arg])
227 | u == txt "unsafePerformPrimIO"
228 -> irTerm vs env arg
230 -- TMP HACK - until we get inlining.
231 (P _ (UN r) _, [_, _, _, _, _, arg])
232 | r == txt "replace"
233 -> irTerm vs env arg
235 -- Laziness, the old way
236 (P _ (UN l) _, [_, arg])
237 | l == txt "lazy"
238 -> error "lazy has crept in somehow"
240 (P _ (UN l) _, [_, arg])
241 | l == txt "force"
242 -> LForce <$> irTerm vs env arg
244 -- Laziness, the new way
245 (P _ (UN l) _, [_, _, arg])
246 | l == txt "Delay"
247 -> LLazyExp <$> irTerm vs env arg
249 (P _ (UN l) _, [_, _, arg])
250 | l == txt "Force"
251 -> LForce <$> irTerm vs env arg
253 (P _ (UN a) _, [_, _, _, arg])
254 | a == txt "assert_smaller"
255 -> irTerm vs env arg
257 (P _ (UN a) _, [_, arg])
258 | a == txt "assert_total"
259 -> irTerm vs env arg
261 (P _ (UN p) _, [_, arg])
262 | p == txt "par"
263 -> do arg' <- irTerm vs env arg
264 return $ LOp LPar [LLazyExp arg']
266 (P _ (UN pf) _, [arg])
267 | pf == txt "prim_fork"
268 -> do arg' <- irTerm vs env arg
269 return $ LOp LFork [LLazyExp arg']
271 (P _ (UN m) _, [_,size,t])
272 | m == txt "malloc"
273 -> irTerm vs env t
275 (P _ (UN tm) _, [_,t])
276 | tm == txt "trace_malloc"
277 -> irTerm vs env t -- TODO
279 -- This case is here until we get more general inlining. It's just
280 -- a really common case, and the laziness hurts...
281 (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),
282 (App (App (App (P _ (UN d') _) _) _) e)])
283 | be == txt "boolElim"
284 , d == txt "Delay"
285 , d' == txt "Delay"
286 -> do
287 x' <- irTerm vs env x
288 t' <- irTerm vs env t
289 e' <- irTerm vs env e
290 return (LCase Shared x'
291 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
292 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
293 ])
295 -- data constructor
296 (P (DCon t arity _) n _, args) -> do
297 detag <- fgetState (opt_detaggable . ist_optimisation n)
298 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
300 let isNewtype = length used == 1 && detag
301 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
303 -- The following code removes fields from data constructors
304 -- and performs the newtype optimisation.
305 --
306 -- The general rule here is:
307 -- Everything we get as input is not touched by erasure,
308 -- so it conforms to the official arities and types
309 -- and we can reason about it like it's plain TT.
310 --
311 -- It's only the data that leaves this point that's erased
312 -- and possibly no longer typed as the original TT version.
313 --
314 -- Especially, underapplied constructors must yield functions
315 -- even if all the remaining arguments are erased
316 -- (the resulting function *will* be applied, to NULLs).
317 --
318 -- This will probably need rethinking when we get erasure from functions.
320 -- "padLams" will wrap our term in LLam-bdas and give us
321 -- the "list of future unerased args" coming from these lambdas.
322 --
323 -- We can do whatever we like with the list of unerased args,
324 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
325 let padLams = padLambdas used (length args) arity
327 case compare (length args) arity of
329 -- overapplied
330 GT -> ifail ("overapplied data constructor: " ++ show tm)
332 -- exactly saturated
333 EQ | isNewtype
334 -> irTerm vs env (head argsPruned)
336 | otherwise -- not newtype, plain data ctor
337 -> buildApp (LV $ Glob n) argsPruned
339 -- not saturated, underapplied
340 LT | isNewtype -- newtype
341 , length argsPruned == 1 -- and we already have the value
342 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
343 <$> irTerm vs env (head argsPruned)
345 | isNewtype -- newtype but the value is not among args yet
346 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
348 -- not a newtype, just apply to a constructor
349 | otherwise
350 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
352 -- type constructor
353 (P (TCon t a) n _, args) -> return LNothing
355 -- a name applied to arguments
356 (P _ n _, args) -> do
357 ist <- getIState
358 case lookup n (idris_scprims ist) of
359 -- if it's a primitive that is already saturated,
360 -- compile to the corresponding op here already to save work
361 Just (arity, op) | length args == arity
362 -> LOp op <$> mapM (irTerm vs env) args
364 -- otherwise, just apply the name
365 _ -> applyName n ist args
367 -- turn de bruijn vars into regular named references and try again
368 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
370 (f, args)
371 -> LApp False
372 <$> irTerm vs env f
373 <*> mapM (irTerm vs env) args
375 where
376 buildApp :: LExp -> [Term] -> Idris LExp
377 buildApp e [] = return e
378 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
380 applyToNames :: LExp -> [Name] -> LExp
381 applyToNames tm [] = tm
382 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
384 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
385 padLambdas used startIdx endSIdx mkTerm
386 = LLam allNames $ mkTerm nonerasedNames
387 where
388 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
389 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
391 applyName :: Name -> IState -> [Term] -> Idris LExp
392 applyName n ist args =
393 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
394 where
395 erase (i, x)
396 | i >= arity || i `elem` used = x
397 | otherwise = Erased
399 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
400 Just (CaseOp ci ty tys def tot cdefs) -> length tys
401 Just (TyDecl (DCon tag ar _) _) -> ar
402 Just (TyDecl Ref ty) -> length $ getArgTys ty
403 Just (Operator ty ar op) -> ar
404 Just def -> error $ "unknown arity: " ++ show (n, def)
405 Nothing -> 0 -- no definition, probably local name => can't erase anything
407 -- name for purposes of usage info lookup
408 uName
409 | Just n' <- viMethod =<< M.lookup n vs = n'
410 | otherwise = n
412 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
413 fst4 (x,_,_,_) = x
415irTerm vs env (P _ n _) = return $ LV (Glob n)
416irTerm vs env (V i)
417 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
418 | otherwise = ifail $ "bad de bruijn index: " ++ show i
420irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
421 where
422 n' = uniqueName n env
424irTerm vs env (Bind n (Let _ v) sc)
425 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
427irTerm vs env (Bind _ _ _) = return $ LNothing
429irTerm vs env (Proj t (-1)) = do
430 t' <- irTerm vs env t
431 return $ LOp (LMinus (ATInt ITBig))
432 [t', LConst (BI 1)]
434irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
435irTerm vs env (Constant c) = return $ LConst c
436irTerm vs env (TType _) = return $ LNothing
437irTerm vs env Erased = return $ LNothing
438irTerm vs env Impossible = return $ LNothing
440doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
441doForeign vs env (_ : fgn : args)
442 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
443 = case getFTypes fgnArgTys of
444 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
445 Just tys -> do
446 args' <- mapM (irTerm vs env) (init args)
447 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
449 | otherwise = ifail "Badly formed foreign function call"
450 where
451 getFTypes :: TT Name -> Maybe [FType]
452 getFTypes tm = case unApply tm of
453 -- nil : {a : Type} -> List a
454 (nil, [_]) -> Just []
455 -- cons : {a : Type} -> a -> List a -> List a
456 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
457 _ -> Nothing
459 mkIty' (P _ (UN ty) _) = mkIty (str ty)
460 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
461 | fi == txt "FIntT"
462 = mkIntIty (str intTy)
464 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
465 | ff == txt "FFunction"
466 , fa == txt "FAny"
467 , io == txt "IO"
468 = FFunctionIO
470 mkIty' (App (App (P _ (UN ff) _) _) _)
471 | ff == txt "FFunction"
472 = FFunction
474 mkIty' _ = FAny
476 -- would be better if these FInt types were evaluated at compile time
477 -- TODO: add %eval directive for such things
479 mkIty "FFloat" = FArith ATFloat
480 mkIty "FInt" = mkIntIty "ITNative"
481 mkIty "FChar" = mkIntIty "ITChar"
482 mkIty "FByte" = mkIntIty "IT8"
483 mkIty "FShort" = mkIntIty "IT16"
484 mkIty "FLong" = mkIntIty "IT64"
485 mkIty "FBits8" = mkIntIty "IT8"
486 mkIty "FBits16" = mkIntIty "IT16"
487 mkIty "FBits32" = mkIntIty "IT32"
488 mkIty "FBits64" = mkIntIty "IT64"
489 mkIty "FString" = FString
490 mkIty "FPtr" = FPtr
491 mkIty "FManagedPtr" = FManagedPtr
492 mkIty "FUnit" = FUnit
493 mkIty "FFunction" = FFunction
494 mkIty "FFunctionIO" = FFunctionIO
495 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
496 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
497 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
498 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
499 mkIty x = error $ "Unknown type " ++ x
501 mkIntIty "ITNative" = FArith (ATInt ITNative)
502 mkIntIty "ITChar" = FArith (ATInt ITChar)
503 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
504 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
505 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
506 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
508irTree :: [Name] -> SC -> Idris LExp
509irTree args tree = do
510 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
511 LLam args <$> irSC M.empty tree
513irSC :: Vars -> SC -> Idris LExp
514irSC vs (STerm t) = irTerm vs [] t
515irSC vs (UnmatchedCase str) = return $ LError str
517irSC vs (ProjCase tm alts) = do
518 tm' <- irTerm vs [] tm
519 alts' <- mapM (irAlt vs tm') alts
520 return $ LCase Shared tm' alts'
522-- Transform matching on Delay to applications of Force.
523irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
524 | delay == txt "Delay"
525 = do sc' <- irSC vs $ mkForce n' n sc
526 return $ LLet n' (LForce (LV (Glob n))) sc'
528-- There are two transformations in this case:
529--
530-- 1. Newtype-case elimination:
531-- case {e0} of
532-- wrap({e1}) -> P({e1}) ==> P({e0})
533--
534-- This is important because newtyped constructors are compiled away entirely
535-- and we need to do that everywhere.
536--
537-- 2. Unused-case elimination (only valid for singleton branches):
538-- case {e0} of ==> P
539-- C(x,y) -> P[... x,y not used ...]
540--
541-- This is important for runtime because sometimes we case on irrelevant data:
542--
543-- In the example above, {e0} will most probably have been erased
544-- so this vain projection would make the resulting program segfault
545-- because the code generator still emits a PROJECT(...) G-machine instruction.
546--
547-- Hence, we check whether the variables are used at all
548-- and erase the casesplit if they are not.
549--
550irSC vs (Case up n [alt]) = do
551 replacement <- case alt of
552 ConCase cn a ns sc -> do
553 detag <- fgetState (opt_detaggable . ist_optimisation cn)
554 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
555 if detag && length used == 1
556 then return . Just $ substSC (ns !! head used) n sc
557 else return Nothing
558 _ -> return Nothing
560 case replacement of
561 Just sc -> irSC vs sc
562 _ -> do
563 alt' <- irAlt vs (LV (Glob n)) alt
564 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
565 [] -> subexpr alt' -- strip the unused top-most case
566 _ -> LCase up (LV (Glob n)) [alt']
567 where
568 namesBoundIn :: LAlt -> [Name]
569 namesBoundIn (LConCase cn i ns sc) = ns
570 namesBoundIn (LConstCase c sc) = []
571 namesBoundIn (LDefaultCase sc) = []
573 subexpr :: LAlt -> LExp
574 subexpr (LConCase _ _ _ e) = e
575 subexpr (LConstCase _ e) = e
576 subexpr (LDefaultCase e) = e
578-- FIXME: When we have a non-singleton case-tree of the form
579--
580-- case {e0} of
581-- C(x) => ...
582-- ... => ...
583--
584-- and C is detaggable (the only constructor of the family), we can be sure
585-- that the first branch will be always taken -- so we add special handling
586-- to remove the dead default branch.
587--
588-- If we don't do so and C is newtype-optimisable, we will miss this newtype
589-- transformation and the resulting code will probably segfault.
590--
591-- This work-around is not entirely optimal; the best approach would be
592-- to ensure that such case trees don't arise in the first place.
593--
594irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
595 detag <- fgetState (opt_detaggable . ist_optimisation cn)
596 if detag
597 then irSC vs (Case up n [ConCase cn a ns sc])
598 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
600irSC vs sc@(Case up n alts) = do
601 -- check that neither alternative needs the newtype optimisation,
602 -- see comment above
603 goneWrong <- or <$> mapM isDetaggable alts
604 when goneWrong
605 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
607 -- everything okay
608 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
609 where
610 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
611 isDetaggable _ = return False
613irSC vs ImpossibleCase = return LNothing
615irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
617-- this leaves out all unused arguments of the constructor
618irAlt vs _ (ConCase n t args sc) = do
619 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
620 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
621 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
622 where
623 methodVars = case n of
624 SN (InstanceCtorN className)
625 -> M.fromList [(v, VI
626 { viMethod = Just $ mkFieldName n i
627 }) | (v,i) <- zip args [0..]]
628 _
629 -> M.empty -- not an instance constructor
631irAlt vs _ (ConstCase x rhs)
632 | matchable x = LConstCase x <$> irSC vs rhs
633 | matchableTy x = LDefaultCase <$> irSC vs rhs
634 where
635 matchable (I _) = True
636 matchable (BI _) = True
637 matchable (Ch _) = True
638 matchable (Str _) = True
639 matchable _ = False
641 matchableTy (AType (ATInt ITNative)) = True
642 matchableTy (AType (ATInt ITBig)) = True
643 matchableTy (AType (ATInt ITChar)) = True
644 matchableTy StrType = True
646 matchableTy (AType (ATInt (ITFixed IT8))) = True
647 matchableTy (AType (ATInt (ITFixed IT16))) = True
648 matchableTy (AType (ATInt (ITFixed IT32))) = True
649 matchableTy (AType (ATInt (ITFixed IT64))) = True
651 matchableTy _ = False
653irAlt vs tm (SucCase n rhs) = do
654 rhs' <- irSC vs rhs
655 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
656 [tm,
657 LConst (BI 1)]) rhs')
659irAlt vs _ (ConstCase c rhs)
660 = ifail $ "Can't match on (" ++ show c ++ ")"
662irAlt vs _ (DefaultCase rhs)
663 = LDefaultCase <$> irSC vs rhs