git.iko.soy/Idris-dev
on ee8fce0 help sign in
Idris-dev/src/IRTS/Compiler.hs
685 lines 25 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 (reverse (drop 4 args)) -- drop implicits
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 TheWorld) = return $ LNothing
433irTerm vs env (Constant c) = return $ LConst c
434irTerm vs env (TType _) = return $ LNothing
435irTerm vs env Erased = return $ LNothing
436irTerm vs env Impossible = return $ LNothing
438doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
439doForeign vs env (ret : fname : world : args)
440 = do args' <- mapM splitArg args
441 let fname' = toFDesc fname
442 let ret' = toFDesc ret
443 return $ LForeign ret' fname' args'
444 where
445 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
446 = do let l' = toFDesc l
447 r' <- irTerm vs env r
448 return (l', r')
449 splitArg _ = ifail "Badly formed foreign function call"
451 toFDesc (Constant (Str str)) = FStr str
452 toFDesc tm
453 | (P _ n _, []) <- unApply tm = FCon (deNS n)
454 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
455 toFDesc _ = FUnknown
457 deNS (NS n _) = n
458 deNS n = n
459doForeign vs env xs = ifail "Badly formed foreign function call"
461{-
462 - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
463 = case getFTypes fgnArgTys of
464 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
465 Just tys -> do
466 args' <- mapM (irTerm vs env) (init args)
467 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
469 | otherwise = ifail "Badly formed foreign function call"
470 where
471 getFTypes :: TT Name -> Maybe [FType]
472 getFTypes tm = case unApply tm of
473 -- nil : {a : Type} -> List a
474 (nil, [_]) -> Just []
475 -- cons : {a : Type} -> a -> List a -> List a
476 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
477 _ -> Nothing
479 mkIty' (P _ (UN ty) _) = mkIty (str ty)
480 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
481 | fi == txt "FIntT"
482 = mkIntIty (str intTy)
484 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
485 | ff == txt "FFunction"
486 , fa == txt "FAny"
487 , io == txt "IO"
488 = FFunctionIO
490 mkIty' (App (App (P _ (UN ff) _) _) _)
491 | ff == txt "FFunction"
492 = FFunction
494 mkIty' _ = FAny
496 -- would be better if these FInt types were evaluated at compile time
497 -- TODO: add %eval directive for such things
498 -- Issue #1742 on the issue tracker.
499 -- https://github.com/idris-lang/Idris-dev/issues/1742
500 mkIty "FFloat" = FArith ATFloat
501 mkIty "FInt" = mkIntIty "ITNative"
502 mkIty "FChar" = mkIntIty "ITChar"
503 mkIty "FByte" = mkIntIty "IT8"
504 mkIty "FShort" = mkIntIty "IT16"
505 mkIty "FLong" = mkIntIty "IT64"
506 mkIty "FBits8" = mkIntIty "IT8"
507 mkIty "FBits16" = mkIntIty "IT16"
508 mkIty "FBits32" = mkIntIty "IT32"
509 mkIty "FBits64" = mkIntIty "IT64"
510 mkIty "FString" = FString
511 mkIty "FPtr" = FPtr
512 mkIty "FManagedPtr" = FManagedPtr
513 mkIty "FUnit" = FUnit
514 mkIty "FFunction" = FFunction
515 mkIty "FFunctionIO" = FFunctionIO
516 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
517 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
518 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
519 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
520 mkIty x = error $ "Unknown type " ++ x
522 mkIntIty "ITNative" = FArith (ATInt ITNative)
523 mkIntIty "ITChar" = FArith (ATInt ITChar)
524 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
525 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
526 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
527 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
528-}
530irTree :: [Name] -> SC -> Idris LExp
531irTree args tree = do
532 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
533 LLam args <$> irSC M.empty tree
535irSC :: Vars -> SC -> Idris LExp
536irSC vs (STerm t) = irTerm vs [] t
537irSC vs (UnmatchedCase str) = return $ LError str
539irSC vs (ProjCase tm alts) = do
540 tm' <- irTerm vs [] tm
541 alts' <- mapM (irAlt vs tm') alts
542 return $ LCase Shared tm' alts'
544-- Transform matching on Delay to applications of Force.
545irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
546 | delay == txt "Delay"
547 = do sc' <- irSC vs $ mkForce n' n sc
548 return $ LLet n' (LForce (LV (Glob n))) sc'
550-- There are two transformations in this case:
551--
552-- 1. Newtype-case elimination:
553-- case {e0} of
554-- wrap({e1}) -> P({e1}) ==> P({e0})
555--
556-- This is important because newtyped constructors are compiled away entirely
557-- and we need to do that everywhere.
558--
559-- 2. Unused-case elimination (only valid for singleton branches):
560-- case {e0} of ==> P
561-- C(x,y) -> P[... x,y not used ...]
562--
563-- This is important for runtime because sometimes we case on irrelevant data:
564--
565-- In the example above, {e0} will most probably have been erased
566-- so this vain projection would make the resulting program segfault
567-- because the code generator still emits a PROJECT(...) G-machine instruction.
568--
569-- Hence, we check whether the variables are used at all
570-- and erase the casesplit if they are not.
571--
572irSC vs (Case up n [alt]) = do
573 replacement <- case alt of
574 ConCase cn a ns sc -> do
575 detag <- fgetState (opt_detaggable . ist_optimisation cn)
576 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
577 if detag && length used == 1
578 then return . Just $ substSC (ns !! head used) n sc
579 else return Nothing
580 _ -> return Nothing
582 case replacement of
583 Just sc -> irSC vs sc
584 _ -> do
585 alt' <- irAlt vs (LV (Glob n)) alt
586 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
587 [] -> subexpr alt' -- strip the unused top-most case
588 _ -> LCase up (LV (Glob n)) [alt']
589 where
590 namesBoundIn :: LAlt -> [Name]
591 namesBoundIn (LConCase cn i ns sc) = ns
592 namesBoundIn (LConstCase c sc) = []
593 namesBoundIn (LDefaultCase sc) = []
595 subexpr :: LAlt -> LExp
596 subexpr (LConCase _ _ _ e) = e
597 subexpr (LConstCase _ e) = e
598 subexpr (LDefaultCase e) = e
600-- FIXME: When we have a non-singleton case-tree of the form
601--
602-- case {e0} of
603-- C(x) => ...
604-- ... => ...
605--
606-- and C is detaggable (the only constructor of the family), we can be sure
607-- that the first branch will be always taken -- so we add special handling
608-- to remove the dead default branch.
609--
610-- If we don't do so and C is newtype-optimisable, we will miss this newtype
611-- transformation and the resulting code will probably segfault.
612--
613-- This work-around is not entirely optimal; the best approach would be
614-- to ensure that such case trees don't arise in the first place.
615--
616irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
617 detag <- fgetState (opt_detaggable . ist_optimisation cn)
618 if detag
619 then irSC vs (Case up n [ConCase cn a ns sc])
620 else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
622irSC vs sc@(Case up n alts) = do
623 -- check that neither alternative needs the newtype optimisation,
624 -- see comment above
625 goneWrong <- or <$> mapM isDetaggable alts
626 when goneWrong
627 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
629 -- everything okay
630 LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
631 where
632 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
633 isDetaggable _ = return False
635irSC vs ImpossibleCase = return LNothing
637irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
639-- this leaves out all unused arguments of the constructor
640irAlt vs _ (ConCase n t args sc) = do
641 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
642 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
643 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
644 where
645 methodVars = case n of
646 SN (InstanceCtorN className)
647 -> M.fromList [(v, VI
648 { viMethod = Just $ mkFieldName n i
649 }) | (v,i) <- zip args [0..]]
650 _
651 -> M.empty -- not an instance constructor
653irAlt vs _ (ConstCase x rhs)
654 | matchable x = LConstCase x <$> irSC vs rhs
655 | matchableTy x = LDefaultCase <$> irSC vs rhs
656 where
657 matchable (I _) = True
658 matchable (BI _) = True
659 matchable (Ch _) = True
660 matchable (Str _) = True
661 matchable _ = False
663 matchableTy (AType (ATInt ITNative)) = True
664 matchableTy (AType (ATInt ITBig)) = True
665 matchableTy (AType (ATInt ITChar)) = True
666 matchableTy StrType = True
668 matchableTy (AType (ATInt (ITFixed IT8))) = True
669 matchableTy (AType (ATInt (ITFixed IT16))) = True
670 matchableTy (AType (ATInt (ITFixed IT32))) = True
671 matchableTy (AType (ATInt (ITFixed IT64))) = True
673 matchableTy _ = False
675irAlt vs tm (SucCase n rhs) = do
676 rhs' <- irSC vs rhs
677 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
678 [tm,
679 LConst (BI 1)]) rhs')
681irAlt vs _ (ConstCase c rhs)
682 = ifail $ "Can't match on (" ++ show c ++ ")"
684irAlt vs _ (DefaultCase rhs)
685 = LDefaultCase <$> irSC vs rhs