git.iko.soy/Idris-dev
on 13449b5 help sign in
Idris-dev/src/IRTS/Compiler.hs
669 lines 25 kB history raw
1{-|
2Module : IRTS.Compiler
3Description : Coordinates the compilation process.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances #-}
10module IRTS.Compiler(compile, generate) where
12import Idris.AbsSyntax
13import Idris.AbsSyntaxTree
14import Idris.ASTUtils
15import Idris.Core.CaseTree
16import Idris.Core.Evaluate
17import Idris.Core.TT
18import Idris.Erasure
19import Idris.Error
20import Idris.Output
21import IRTS.CodegenC
22import IRTS.CodegenCommon
23import IRTS.CodegenJavaScript
24import IRTS.Defunctionalise
25import IRTS.DumpBC
26import IRTS.Exports
27import IRTS.Inliner
28import IRTS.Lang
29import IRTS.LangOpts
30import IRTS.Portable
31import IRTS.Simplified
33import Prelude hiding (id, (.))
35import Control.Applicative
36import Control.Category
37import Control.Monad.State
38import Data.IntSet (IntSet)
39import qualified Data.IntSet as IS
40import Data.List
41import qualified Data.Map as M
42import Data.Maybe
43import Data.Ord
44import qualified Data.Set as S
45import Debug.Trace
46import System.Directory
47import System.Environment
48import System.Exit
49import System.FilePath (addTrailingPathSeparator, (</>))
50import System.IO
51import System.Process
53-- | Compile to simplified forms and return CodegenInfo
54compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
55compile codegen f mtm
56 = do checkMVs -- check for undefined metavariables
57 checkTotality -- refuse to compile if there are totality problems
58 exports <- findExports
59 let rootNames = case mtm of
60 Nothing -> []
61 Just t -> freeNames t
63 reachableNames <- performUsageAnalysis
64 (rootNames ++ getExpNames exports)
65 maindef <- case mtm of
66 Nothing -> return []
67 Just tm -> do md <- irMain tm
68 logCodeGen 1 $ "MAIN: " ++ show md
69 return [(sMN 0 "runMain", md)]
70 objs <- getObjectFiles codegen
71 libs <- getLibs codegen
72 flags <- getFlags codegen
73 hdrs <- getHdrs codegen
74 impdirs <- allImportDirs
75 defsIn <- mkDecls reachableNames
76 -- if no 'main term' given, generate interface files
77 let iface = case mtm of
78 Nothing -> True
79 Just _ -> False
81 let defs = defsIn ++ maindef
83 -- Inlined top level LDecl made here
84 let defsInlined = inlineAll defs
85 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
86 defsInlined
88 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)
89 let ctxtIn = addAlist tagged emptyContext
91 logCodeGen 1 "Defunctionalising"
92 let defuns_in = defunctionalise nexttag ctxtIn
93 logCodeGen 5 $ show defuns_in
94 logCodeGen 1 "Inlining"
95 let defuns = inline defuns_in
96 logCodeGen 5 $ show defuns
97 logCodeGen 1 "Resolving variables for CG"
99 let checked = simplifyDefs defuns (toAlist defuns)
100 outty <- outputTy
101 dumpCases <- getDumpCases
102 dumpDefun <- getDumpDefun
103 case dumpCases of
104 Nothing -> return ()
105 Just f -> runIO $ writeFile f (showCaseTrees defs)
106 case dumpDefun of
107 Nothing -> return ()
108 Just f -> runIO $ writeFile f (dumpDefuns defuns)
109 triple <- Idris.AbsSyntax.targetTriple
110 cpu <- Idris.AbsSyntax.targetCPU
111 logCodeGen 1 "Building output"
112 case checked of
113 OK c -> do return $ CodegenInfo f outty triple cpu
114 hdrs impdirs objs libs flags
115 NONE c (toAlist defuns)
116 tagged iface exports
117 Error e -> ierror e
118 where checkMVs = do i <- getIState
119 case map fst (idris_metavars i) \\ primDefs of
120 [] -> return ()
121 ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
122 iputStrLn "\nEvaluation of any of these will crash at run time."
123 return ()
124 checkTotality = do i <- getIState
125 case idris_totcheckfail i of
126 [] -> return ()
127 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
129generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
130generate codegen mainmod ir
131 = case codegen of
132 -- Built-in code generators (FIXME: lift these out!)
133 Via _ "c" -> codegenC ir
134 -- Any external code generator
135 Via fm cg -> do input <- case fm of
136 IBCFormat -> return mainmod
137 JSONFormat -> do
138 tempdir <- getTemporaryDirectory
139 (fn, h) <- openTempFile tempdir "idris-cg.json"
140 writePortable h ir
141 hClose h
142 return fn
143 let cmd = "idris-codegen-" ++ cg
144 args = [input, "-o", outputFile ir] ++ compilerFlags ir
145 exit <- rawSystem cmd args
146 when (exit /= ExitSuccess) $
147 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
148 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
150irMain :: TT Name -> Idris LDecl
151irMain tm = do
152 i <- irTerm (sMN 0 "runMain") M.empty [] tm
153 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
155mkDecls :: [Name] -> Idris [(Name, LDecl)]
156mkDecls used
157 = do i <- getIState
158 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
159 decls <- mapM build ds
160 return decls
162showCaseTrees :: [(Name, LDecl)] -> String
163showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
164 where
165 showCT (n, LFun _ f args lexp)
166 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
167 ++ show lexp
168 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
170 defnRank :: (Name, LDecl) -> String
171 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
172 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
174 nameRank :: Name -> String
175 nameRank (UN s) = "1" ++ show s
176 nameRank (MN i s) = "2" ++ show s ++ show i
177 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
178 nameRank (SN sn) = "4" ++ snRank sn
179 nameRank n = "5" ++ show n
181 snRank :: SpecialName -> String
182 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
183 snRank (ImplementationN n args) = "2" ++ nameRank n ++ concatMap show args
184 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
185 snRank (MethodN n) = "4" ++ nameRank n
186 snRank (CaseN _ n) = "5" ++ nameRank n
187 snRank (ElimN n) = "6" ++ nameRank n
188 snRank (ImplementationCtorN n) = "7" ++ nameRank n
189 snRank (WithN i n) = "8" ++ nameRank n ++ show i
191isCon (TyDecl _ _) = True
192isCon _ = False
194build :: (Name, Def) -> Idris (Name, LDecl)
195build (n, d)
196 = do i <- getIState
197 case getPrim n i of
198 Just (ar, op) ->
199 let args = map (\x -> sMN x "op") [0..] in
200 return (n, (LFun [] n (take ar args)
201 (LOp op (map (LV . Glob) (take ar args)))))
202 _ -> do def <- mkLDecl n d
203 logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
204 return (n, def)
205 where getPrim n i
206 | Just (ar, op) <- lookup n (idris_scprims i)
207 = Just (ar, op)
208 | Just ar <- lookup n (S.toList (idris_externs i))
209 = Just (ar, LExternal n)
210 getPrim n i = Nothing
212declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
213declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
215mkLDecl n (Function tm _)
216 = declArgs [] True n <$> irTerm n M.empty [] tm
218mkLDecl n (CaseOp ci _ _ _ pats cd)
219 = declArgs [] (case_inlinable ci || caseName n) n <$> irTree n args sc
220 where
221 (args, sc) = cases_runtime cd
223 -- Always attempt to inline functions arising from 'case' expressions
224 caseName (SN (CaseN _ _)) = True
225 caseName (SN (WithN _ _)) = True
226 caseName (NS n _) = caseName n
227 caseName _ = False
229mkLDecl n (TyDecl (DCon tag arity _) _) =
230 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
232mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
233mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
235data VarInfo = VI
236 { viMethod :: Maybe Name
237 }
238 deriving Show
240type Vars = M.Map Name VarInfo
242irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
243irTerm top vs env tm@(App _ f a) = do
244 ist <- getIState
245 case unApply tm of
246 (P _ n _, args)
247 | n `elem` map fst (idris_metavars ist) \\ primDefs
248 -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
249 (P _ (UN m) _, args)
250 | m == txt "mkForeignPrim"
251 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
253 (P _ (UN u) _, [_, arg])
254 | u == txt "unsafePerformPrimIO"
255 -> irTerm top vs env arg
257 (P _ (UN u) _, _)
258 | u == txt "assert_unreachable"
259 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top
261 -- TMP HACK - until we get inlining.
262 (P _ (UN r) _, [_, _, _, _, _, arg])
263 | r == txt "replace"
264 -> irTerm top vs env arg
266 -- 'void' doesn't have any pattern clauses and only gets called on
267 -- erased things in higher order contexts (also a TMP HACK...)
268 (P _ (UN r) _, _)
269 | r == txt "void"
270 -> return LNothing
272 -- Laziness, the old way
273 (P _ (UN l) _, [_, arg])
274 | l == txt "lazy"
275 -> error "lazy has crept in somehow"
277 (P _ (UN l) _, [_, arg])
278 | l == txt "force"
279 -> LForce <$> irTerm top vs env arg
281 -- Laziness, the new way
282 (P _ (UN l) _, [_, _, arg])
283 | l == txt "Delay"
284 -> LLazyExp <$> irTerm top vs env arg
286 (P _ (UN l) _, [_, _, arg])
287 | l == txt "Force"
288 -> LForce <$> irTerm top vs env arg
290 (P _ (UN a) _, [_, _, _, arg])
291 | a == txt "assert_smaller"
292 -> irTerm top vs env arg
294 (P _ (UN a) _, [_, arg])
295 | a == txt "assert_total"
296 -> irTerm top vs env arg
298 (P _ (UN p) _, [_, arg])
299 | p == txt "par"
300 -> do arg' <- irTerm top vs env arg
301 return $ LOp LPar [LLazyExp arg']
303 (P _ (UN pf) _, [arg])
304 | pf == txt "prim_fork"
305 -> do arg' <- irTerm top vs env arg
306 return $ LOp LFork [LLazyExp arg']
308 (P _ (UN m) _, [_,size,t])
309 | m == txt "malloc"
310 -> irTerm top vs env t
312 (P _ (UN tm) _, [_,t])
313 | tm == txt "trace_malloc"
314 -> irTerm top vs env t -- TODO
316 -- This case is here until we get more general inlining. It's just
317 -- a really common case, and the laziness hurts...
318 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),
319 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])
320 | be == txt "ifThenElse"
321 , d == txt "Delay"
322 , d' == txt "Delay"
323 , b == txt "Bool"
324 , p == txt "Prelude"
325 -> do
326 x' <- irTerm top vs env x
327 t' <- irTerm top vs env t
328 e' <- irTerm top vs env e
329 return (LCase Shared x'
330 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
331 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
332 ])
334 -- data constructor
335 (P (DCon t arity _) n _, args) -> do
336 detag <- fgetState (opt_detaggable . ist_optimisation n)
337 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
339 let isNewtype = length used == 1 && detag
340 let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]
342 -- The following code removes fields from data constructors
343 -- and performs the newtype optimisation.
344 --
345 -- The general rule here is:
346 -- Everything we get as input is not touched by erasure,
347 -- so it conforms to the official arities and types
348 -- and we can reason about it like it's plain TT.
349 --
350 -- It's only the data that leaves this point that's erased
351 -- and possibly no longer typed as the original TT version.
352 --
353 -- Especially, underapplied constructors must yield functions
354 -- even if all the remaining arguments are erased
355 -- (the resulting function *will* be applied, to NULLs).
356 --
357 -- This will probably need rethinking when we get erasure from functions.
359 -- "padLams" will wrap our term in LLam-bdas and give us
360 -- the "list of future unerased args" coming from these lambdas.
361 --
362 -- We can do whatever we like with the list of unerased args,
363 -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
364 let padLams = padLambdas used (length args) arity
366 case compare (length args) arity of
368 -- overapplied
369 GT -> ifail ("overapplied data constructor: " ++ show tm ++
370 "\nDEBUG INFO:\n" ++
371 "Arity: " ++ show arity ++ "\n" ++
372 "Arguments: " ++ show args ++ "\n" ++
373 "Pruned arguments: " ++ show argsPruned)
375 -- exactly saturated
376 EQ | isNewtype
377 -> irTerm top vs env (head argsPruned)
379 | otherwise -- not newtype, plain data ctor
380 -> buildApp (LV $ Glob n) argsPruned
382 -- not saturated, underapplied
383 LT | isNewtype -- newtype
384 , length argsPruned == 1 -- and we already have the value
385 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args
386 <$> irTerm top vs env (head argsPruned)
388 | isNewtype -- newtype but the value is not among args yet
389 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]
391 -- not a newtype, just apply to a constructor
392 | otherwise
393 -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned
395 -- type constructor
396 (P (TCon t a) n _, args) -> return LNothing
398 -- an external name applied to arguments
399 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do
400 LOp (LExternal n) <$> mapM (irTerm top vs env) args
402 -- a name applied to arguments
403 (P _ n _, args) -> do
404 case lookup n (idris_scprims ist) of
405 -- if it's a primitive that is already saturated,
406 -- compile to the corresponding op here already to save work
407 Just (arity, op) | length args == arity
408 -> LOp op <$> mapM (irTerm top vs env) args
410 -- otherwise, just apply the name
411 _ -> applyName n ist args
413 -- turn de bruijn vars into regular named references and try again
414 (V i, args) -> irTerm top vs env $ mkApp (P Bound (env !! i) Erased) args
416 (f, args)
417 -> LApp False
418 <$> irTerm top vs env f
419 <*> mapM (irTerm top vs env) args
421 where
422 buildApp :: LExp -> [Term] -> Idris LExp
423 buildApp e [] = return e
424 buildApp e xs = LApp False e <$> mapM (irTerm top vs env) xs
426 applyToNames :: LExp -> [Name] -> LExp
427 applyToNames tm [] = tm
428 applyToNames tm ns = LApp False tm $ map (LV . Glob) ns
430 padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
431 padLambdas used startIdx endSIdx mkTerm
432 = LLam allNames $ mkTerm nonerasedNames
433 where
434 allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]
435 nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]
437 applyName :: Name -> IState -> [Term] -> Idris LExp
438 applyName n ist args =
439 LApp False (LV $ Glob n) <$> mapM (irTerm top vs env . erase) (zip [0..] args)
440 where
441 erase (i, x)
442 | i >= arity || i `elem` used = x
443 | otherwise = Erased
445 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
446 Just (CaseOp ci ty tys def tot cdefs) -> length tys
447 Just (TyDecl (DCon tag ar _) _) -> ar
448 Just (TyDecl Ref ty) -> length $ getArgTys ty
449 Just (Operator ty ar op) -> ar
450 Just def -> error $ "unknown arity: " ++ show (n, def)
451 Nothing -> 0 -- no definition, probably local name => can't erase anything
453 -- name for purposes of usage info lookup
454 uName
455 | Just n' <- viMethod =<< M.lookup n vs = n'
456 | otherwise = n
458 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
459 fst4 (x,_,_,_,_) = x
461irTerm top vs env (P _ n _) = return $ LV (Glob n)
462irTerm top vs env (V i)
463 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
464 | otherwise = ifail $ "bad de bruijn index: " ++ show i
466irTerm top vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
467 where
468 n' = uniqueName n env
470irTerm top vs env (Bind n (Let _ v) sc)
471 = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc
473irTerm top vs env (Bind _ _ _) = return $ LNothing
475irTerm top vs env (Proj t (-1)) = do
476 t' <- irTerm top vs env t
477 return $ LOp (LMinus (ATInt ITBig))
478 [t', LConst (BI 1)]
480irTerm top vs env (Proj t i) = LProj <$> irTerm top vs env t <*> pure i
481irTerm top vs env (Constant TheWorld) = return LNothing
482irTerm top vs env (Constant c) = return (LConst c)
483irTerm top vs env (TType _) = return LNothing
484irTerm top vs env Erased = return LNothing
485irTerm top vs env Impossible = return LNothing
487doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
488doForeign vs env (ret : fname : world : args)
489 = do args' <- mapM splitArg args
490 let fname' = toFDesc fname
491 let ret' = toFDesc ret
492 return $ LForeign ret' fname' args'
493 where
494 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits
495 = do let l' = toFDesc l
496 r' <- irTerm (sMN 0 "__foreignCall") vs env r
497 return (l', r')
498 splitArg _ = ifail "Badly formed foreign function call"
500 toFDesc (Constant (Str str)) = FStr str
501 toFDesc tm
502 | (P _ n _, []) <- unApply tm = FCon (deNS n)
503 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
504 toFDesc _ = FUnknown
506 deNS (NS n _) = n
507 deNS n = n
508doForeign vs env xs = ifail "Badly formed foreign function call"
510irTree :: Name -> [Name] -> SC -> Idris LExp
511irTree top args tree = do
512 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
513 LLam args <$> irSC top M.empty tree
515irSC :: Name -> Vars -> SC -> Idris LExp
516irSC top vs (STerm t) = irTerm top vs [] t
517irSC top vs (UnmatchedCase str) = return $ LError str
519irSC top vs (ProjCase tm alts) = do
520 tm' <- irTerm top vs [] tm
521 alts' <- mapM (irAlt top vs tm') alts
522 return $ LCase Shared tm' alts'
524-- Transform matching on Delay to applications of Force.
525irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
526 | delay == txt "Delay"
527 = do sc' <- irSC top vs sc -- mkForce n' n sc
528 return $ lsubst n' (LForce (LV (Glob n))) sc'
530-- There are two transformations in this case:
531--
532-- 1. Newtype-case elimination:
533-- case {e0} of
534-- wrap({e1}) -> P({e1}) ==> P({e0})
535--
536-- This is important because newtyped constructors are compiled away entirely
537-- and we need to do that everywhere.
538--
539-- 2. Unused-case elimination (only valid for singleton branches):
540-- case {e0} of ==> P
541-- C(x,y) -> P[... x,y not used ...]
542--
543-- This is important for runtime because sometimes we case on irrelevant data:
544--
545-- In the example above, {e0} will most probably have been erased
546-- so this vain projection would make the resulting program segfault
547-- because the code generator still emits a PROJECT(...) G-machine instruction.
548--
549-- Hence, we check whether the variables are used at all
550-- and erase the casesplit if they are not.
551--
552irSC top vs (Case up n [alt]) = do
553 replacement <- case alt of
554 ConCase cn a ns sc -> do
555 detag <- fgetState (opt_detaggable . ist_optimisation cn)
556 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
557 if detag && length used == 1
558 then return . Just $ substSC (ns !! head used) n sc
559 else return Nothing
560 _ -> return Nothing
562 case replacement of
563 Just sc -> irSC top vs sc
564 _ -> do
565 alt' <- irAlt top vs (LV (Glob n)) alt
566 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
567 [] -> subexpr alt' -- strip the unused top-most case
568 _ -> LCase up (LV (Glob n)) [alt']
569 where
570 namesBoundIn :: LAlt -> [Name]
571 namesBoundIn (LConCase cn i ns sc) = ns
572 namesBoundIn (LConstCase c sc) = []
573 namesBoundIn (LDefaultCase sc) = []
575 subexpr :: LAlt -> LExp
576 subexpr (LConCase _ _ _ e) = e
577 subexpr (LConstCase _ e) = e
578 subexpr (LDefaultCase e) = e
580-- FIXME: When we have a non-singleton case-tree of the form
581--
582-- case {e0} of
583-- C(x) => ...
584-- ... => ...
585--
586-- and C is detaggable (the only constructor of the family), we can be sure
587-- that the first branch will be always taken -- so we add special handling
588-- to remove the dead default branch.
589--
590-- If we don't do so and C is newtype-optimisable, we will miss this newtype
591-- transformation and the resulting code will probably segfault.
592--
593-- This work-around is not entirely optimal; the best approach would be
594-- to ensure that such case trees don't arise in the first place.
595--
596irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
597 detag <- fgetState (opt_detaggable . ist_optimisation cn)
598 if detag
599 then irSC top vs (Case up n [ConCase cn a ns sc])
600 else LCase up (LV (Glob n)) <$> mapM (irAlt top vs (LV (Glob n))) alts
602irSC top vs sc@(Case up n alts) = do
603 -- check that neither alternative needs the newtype optimisation,
604 -- see comment above
605 goneWrong <- or <$> mapM isDetaggable alts
606 when goneWrong
607 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
609 -- everything okay
610 LCase up (LV (Glob n)) <$> mapM (irAlt top vs (LV (Glob n))) alts
611 where
612 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
613 isDetaggable _ = return False
615irSC top vs ImpossibleCase = return LNothing
617irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt
619-- this leaves out all unused arguments of the constructor
620irAlt top vs _ (ConCase n t args sc) = do
621 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
622 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
623 LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc
624 where
625 methodVars = case n of
626 SN (ImplementationCtorN interfaceName)
627 -> M.fromList [(v, VI
628 { viMethod = Just $ mkFieldName n i
629 }) | (v,i) <- zip args [0..]]
630 _
631 -> M.empty -- not an implementation constructor
633irAlt top vs _ (ConstCase x rhs)
634 | matchable x = LConstCase x <$> irSC top vs rhs
635 | matchableTy x = LDefaultCase <$> irSC top vs rhs
636 where
637 matchable (I _) = True
638 matchable (BI _) = True
639 matchable (Ch _) = True
640 matchable (Str _) = True
641 matchable (B8 _) = True
642 matchable (B16 _) = True
643 matchable (B32 _) = True
644 matchable (B64 _) = 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 top vs tm (SucCase n rhs) = do
660 rhs' <- irSC top vs rhs
661 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
662 [tm,
663 LConst (BI 1)]) rhs')
665irAlt top vs _ (ConstCase c rhs)
666 = ifail $ "Can't match on (" ++ show c ++ ")"
668irAlt top vs _ (DefaultCase rhs)
669 = LDefaultCase <$> irSC top vs rhs