@@ -18,15 +18,25 @@ import Util.LLVMStubs
1818import IRTS.Inliner
1919
2020import Idris.AbsSyntax
21−import Idris.UnusedArgs
21+import Idris.AbsSyntaxTree
22+import Idris.Erasure
2223import Idris.Error
2324
25+import Debug.Trace
26+
2427import Idris.Core.TT
2528import Idris.Core.Evaluate
2629import Idris.Core.CaseTree
2730
31+import Control.Applicative
2832import Control.Monad.State
33+import Data.Maybe
2934import Data.List
35+import Data.Ord
36+import Data.IntSet (IntSet)
37+import qualified Data.IntSet as IS
38+import qualified Data.Map as M
39+import qualified Data.Set as S
3040import System.Process
3141import System.IO
3242import System.Directory
@@ -37,18 +47,16 @@ import Paths_idris
3747
3848compile :: Codegen -> FilePath -> Term -> Idris ()
3949compile codegen f tm
40− = do checkMVs
41− let tmnames = namesUsed (STerm tm)
42− usedIn <- mapM (allNames []) tmnames
43− let used = [sUN "prim__subBigInt", sUN "prim__addBigInt"] : usedIn
44− defsIn <- mkDecls tm (concat used)
45− findUnusedArgs (concat used)
50+ = do checkMVs -- check for undefined metavariables
51+ reachableNames <- performUsageAnalysis
4652 maindef <- irMain tm
53+ iLOG $ "MAIN: " ++ show maindef
4754 objs <- getObjectFiles codegen
4855 libs <- getLibs codegen
4956 flags <- getFlags codegen
5057 hdrs <- getHdrs codegen
5158 impdirs <- allImportDirs
59+ defsIn <- mkDecls tm reachableNames
5260 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
5361 -- iputStrLn $ showSep "\n" (map show defs)
5462 let (nexttag, tagged) = addTags 65536 (liftAll defs)
@@ -71,25 +79,22 @@ compile codegen f tm
7179 case dumpDefun of
7280 Nothing -> return ()
7381 Just f -> runIO $ writeFile f (dumpDefuns defuns)
74− triple <- targetTriple
75− cpu <- targetCPU
76− optimize <- optLevel
82+ triple <- Idris.AbsSyntax.targetTriple
83+ cpu <- Idris.AbsSyntax.targetCPU
84+ optimise <- optLevel
7785 iLOG "Building output"
86+
7887 case checked of
79− OK c -> runIO $ case codegen of
80− ViaC ->
81− codegenC c f outty hdrs
82− (concatMap mkObj objs)
83− (concatMap mkLib libs)
84− (concatMap mkFlag flags ++
85− concatMap incdir impdirs) NONE
86− ViaJava ->
87− codegenJava [] c f hdrs libs outty
88− ViaJavaScript ->
89− codegenJavaScript JavaScript c hdrs f outty
90− ViaNode ->
91− codegenJavaScript Node c hdrs f outty
92− ViaLLVM -> codegenLLVM c triple cpu optimize f outty
88+ OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
89+ hdrs impdirs objs libs flags
90+ NONE c (toAlist defuns)
91+ tagged
92+ runIO $ case codegen of
93+ ViaC -> codegenC cginfo
94+ ViaJava -> codegenJava cginfo
95+ ViaJavaScript -> codegenJavaScript cginfo
96+ ViaNode -> codegenNode cginfo
97+ ViaLLVM -> codegenLLVM cginfo
9398 Bytecode -> dumpBC c f
9499 Error e -> ierror e
95100 where checkMVs = do i <- getIState
@@ -99,39 +104,50 @@ compile codegen f tm
99104 inDir d h = do let f = d </> h
100105 ex <- doesFileExist f
101106 if ex then return f else return h
102− mkObj f = f ++ " "
103− mkLib l = "-l" ++ l ++ " "
104− mkFlag l = l ++ " "
105−
106− incdir i = "-I" ++ i ++ " "
107−
108107
109108irMain :: TT Name -> Idris LDecl
110−irMain tm = do i <- ir tm
111− return $ LFun [] (sMN 0 "runMain") [] (LForce i)
109+irMain tm = do
110+ i <- irTerm M.empty [] tm
111+ return $ LFun [] (sMN 0 "runMain") [] (LForce i)
112112
113113mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
114114mkDecls t used
115115 = do i <- getIState
116− let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
117− mapM traceUnused used
116+ let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
118117 decls <- mapM build ds
119118 return decls
120119
121120showCaseTrees :: [(Name, LDecl)] -> String
122−showCaseTrees ds = showSep "\n\n" (map showCT ds)
121+showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
123122 where
124123 showCT (n, LFun _ f args lexp)
125− = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
124+ = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
126125 ++ show lexp
127126 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
128127
128+ defnRank :: (Name, LDecl) -> String
129+ defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
130+ defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
131+
132+ nameRank :: Name -> String
133+ nameRank (UN s) = "1" ++ show s
134+ nameRank (MN i s) = "2" ++ show s ++ show i
135+ nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
136+ nameRank (SN sn) = "4" ++ snRank sn
137+ nameRank n = "5" ++ show n
138+
139+ snRank :: SpecialName -> String
140+ snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
141+ snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
142+ snRank (ParentN n s) = "3" ++ nameRank n ++ show s
143+ snRank (MethodN n) = "4" ++ nameRank n
144+ snRank (CaseN n) = "5" ++ nameRank n
145+ snRank (ElimN n) = "6" ++ nameRank n
146+ snRank (InstanceCtorN n) = "7" ++ nameRank n
147+
129148isCon (TyDecl _ _) = True
130149isCon _ = False
131150
132−class ToIR a where
133− ir :: a -> Idris LExp
134−
135151build :: (Name, Def) -> Idris (Name, LDecl)
136152build (n, d)
137153 = do i <- getIState
@@ -144,295 +160,396 @@ build (n, d)
144160 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
145161 return (n, def)
146162
147−getPrim :: IState -> Name -> [LExp] -> Maybe LExp
148−getPrim i n args = case lookup n (idris_scprims i) of
149− Just (ar, op) ->
150− if (ar == length args)
151− then return (LOp op args)
152− else Nothing
153− _ -> Nothing
154−
155163declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
156164declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
157165
158−mkLDecl n (Function tm _) = do e <- ir tm
159− return (declArgs [] True n e)
166+mkLDecl n (Function tm _)
167+ = declArgs [] True n <$> irTerm M.empty [] tm
168+
160169mkLDecl n (CaseOp ci _ _ _ pats cd)
161− = let (args, sc) = cases_runtime cd in
162− do e <- ir (args, sc)
163− return (declArgs [] (case_inlinable ci) n e)
164−mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
170+ = declArgs [] (case_inlinable ci) n <$> irTree args sc
171+ where
172+ (args, sc) = cases_runtime cd
173+
174+mkLDecl n (TyDecl (DCon tag arity) _) =
175+ LConstructor n tag . erasedArity . lookup n <$> getIState
176+ where
177+ lookup n = lookupCtxtExact n . idris_callgraph
178+ erasedArity = maybe 0 (length . usedpos)
179+
165180mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
166181mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
167182
168−instance ToIR (TT Name) where
169− ir tm = ir' [] tm where
170− ir' env tm@(App f a)
171− | (P _ (UN m) _, args) <- unApply tm,
172− m == txt "mkForeignPrim"
173− = doForeign env args
174− | (P _ (UN u) _, [_, arg]) <- unApply tm,
175− u == txt "unsafePerformPrimIO"
176− = ir' env arg
177− -- TMP HACK - until we get inlining.
178− | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
179− r == txt "replace"
180− = ir' env arg
181− -- Laziness, the old way
182− | (P _ (UN l) _, [_, arg]) <- unApply tm,
183− l == txt "lazy"
184− = do arg' <- ir' env arg
185− error "lazy has crept in somehow"
186−-- return $ LLazyExp arg'
187− | (P _ (UN l) _, [_, arg]) <- unApply tm,
188− l == txt "force"
189− = do arg' <- ir' env arg
190− return $ LForce arg'
191− -- Laziness, the new way
192− | (P _ (UN l) _, [arg]) <- unApply tm,
193− l == txt "Delay"
194− = do arg' <- ir' env arg
195− return $ LLazyExp arg'
196− | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
197− l == txt "Force"
198− = do arg' <- ir' env arg
199− return $ LForce arg'
200− | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
201− a == txt "assert_smaller"
202− = ir' env arg
203− | (P _ (UN a) _, [_, arg]) <- unApply tm,
204− a == txt "assert_total"
205− = ir' env arg
206− | (P _ (UN p) _, [_, arg]) <- unApply tm,
207− p == txt "par"
208− = do arg' <- ir' env arg
209− return $ LOp LPar [LLazyExp arg']
210− | (P _ (UN pf) _, [arg]) <- unApply tm,
211− pf == txt "prim_fork"
212− = do arg' <- ir' env arg
213− return $ LOp LFork [LLazyExp arg']
214− | (P _ (UN m) _, [_,size,t]) <- unApply tm,
215− m == txt "malloc"
216− = do size' <- ir' env size
217− t' <- ir' env t
218− return t' -- TODO $ malloc_ size' t'
219− | (P _ (UN tm) _, [_,t]) <- unApply tm,
220− tm == txt "trace_malloc"
221− = do t' <- ir' env t
222− return t' -- TODO
223− -- This case is here until we get more general inlining. It's just
224− -- a really common case, and the laziness hurts...
225− | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
226− (App (P _ (UN d') _) e)]) <- unApply tm,
227− be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
228− = do x' <- ir' env x
229− t' <- ir' env t
230− e' <- ir' env e
231− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
232− LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
233− | (P (DCon t a) n _, args) <- unApply tm
234− = irCon env t a n args
235− | (P (TCon t a) n _, args) <- unApply tm
236− = return LNothing
237− | (P _ n _, args) <- unApply tm
238− = do i <- getIState
239− args' <- mapM (ir' env) args
240− case getPrim i n args' of
241− Just tm -> return tm
242− _ -> do
243− let collapse
244− = case lookupCtxtExact n
245− (idris_optimisation i) of
246− Just oi -> collapsible oi
247− _ -> False
248− let unused
249− = case lookupCtxtExact n
250− (idris_callgraph i) of
251− Just (CGInfo _ _ _ _ unusedpos) ->
252− unusedpos
253− _ -> []
254− if collapse
255− then return LNothing
256− else return (LApp False (LV (Glob n))
257− (mkUnused unused 0 args'))
258− | (f, args) <- unApply tm
259− = do f' <- ir' env f
260− args' <- mapM (ir' env) args
261− return (LApp False f' args')
262− where mkUnused u i [] = []
263− mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
264− | otherwise = x : mkUnused u (i + 1) xs
265−-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
266−-- = return $ LConst (BI 0)
267− ir' env (P _ n _) = return $ LV (Glob n)
268− ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
269− | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
270− ir' env (Bind n (Lam _) sc)
271− = do let n' = uniqueName n env
272− sc' <- ir' (n' : env) sc
273− return $ LLam [n'] sc'
274− ir' env (Bind n (Let _ v) sc)
275− = do sc' <- ir' (n : env) sc
276− v' <- ir' env v
277− return $ LLet n v' sc'
278− ir' env (Bind _ _ _) = return $ LNothing
279− ir' env (Proj t i) | i == -1
280− = do t' <- ir' env t
281− return $ LOp (LMinus (ATInt ITBig))
282− [t', LConst (BI 1)]
283− ir' env (Proj t i) = do t' <- ir' env t
284− return $ LProj t' i
285− ir' env (Constant c) = return $ LConst c
286− ir' env (TType _) = return $ LNothing
287− ir' env Erased = return $ LNothing
288− ir' env Impossible = return $ LNothing
289−-- ir' env _ = return $ LError "Impossible"
290−
291− irCon env t arity n args
292− | length args == arity = buildApp env (LV (Glob n)) args
293− | otherwise = let extra = satArgs (arity - length args) in
294− do sc' <- irCon env t arity n
295− (args ++ map (\n -> P Bound n undefined) extra)
296− return $ LLam extra sc'
297−
298− satArgs n = map (\i -> sMN i "sat") [1..n]
299−
300− buildApp env e [] = return e
301− buildApp env e xs = do xs' <- mapM (ir' env) xs
302− return $ LApp False e xs'
303−
304− doForeign :: [Name] -> [TT Name] -> Idris LExp
305− doForeign env (_ : fgn : args)
306− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
307− = let maybeTys = getFTypes fgnArgTys
308− rty = mkIty' ret in
309− case maybeTys of
310− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
311− Just tys -> do
312− args' <- mapM (ir' env) (init args)
313− -- wrap it in a prim__IO
314− -- return $ con_ 0 @@ impossible @@
315− return $ -- LLazyExp $
316− LForeign LANG_C rty fgnName (zip tys args')
317− | otherwise = ifail "Badly formed foreign function call"
318−
319−getFTypes :: TT Name -> Maybe [FType]
320−getFTypes tm = case unApply tm of
321− (nil, []) -> Just []
322− (cons, [ty, xs]) ->
323− fmap (mkIty' ty :) (getFTypes xs)
324− _ -> Nothing
325−
326−mkIty' (P _ (UN ty) _) = mkIty (str ty)
327−mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
328− | fi == txt "FIntT" = mkIntIty (str intTy)
329−mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
330− | ff == txt "FFunction" && fa == txt "FAny" &&
331− io == txt "IO"
183+data VarInfo = VI
184+ { viMethod :: Maybe Name
185+ }
186+ deriving Show
187+
188+type Vars = M.Map Name VarInfo
189+
190+irTerm :: Vars -> [Name] -> Term -> Idris LExp
191+irTerm vs env tm@(App f a) = case unApply tm of
192+ (P _ (UN m) _, args)
193+ | m == txt "mkForeignPrim"
194+ -> doForeign vs env args
195+
196+ (P _ (UN u) _, [_, arg])
197+ | u == txt "unsafePerformPrimIO"
198+ -> irTerm vs env arg
199+
200+ -- TMP HACK - until we get inlining.
201+ (P _ (UN r) _, [_, _, _, _, _, arg])
202+ | r == txt "replace"
203+ -> irTerm vs env arg
204+
205+ -- Laziness, the old way
206+ (P _ (UN l) _, [_, arg])
207+ | l == txt "lazy"
208+ -> error "lazy has crept in somehow"
209+
210+ (P _ (UN l) _, [_, arg])
211+ | l == txt "force"
212+ -> LForce <$> irTerm vs env arg
213+
214+ -- Laziness, the new way
215+ (P _ (UN l) _, [_, _, arg])
216+ | l == txt "Delay"
217+ -> LLazyExp <$> irTerm vs env arg
218+
219+ (P _ (UN l) _, [_, _, arg])
220+ | l == txt "Force"
221+ -> LForce <$> irTerm vs env arg
222+
223+ (P _ (UN a) _, [_, _, arg])
224+ | a == txt "assert_smaller"
225+ -> irTerm vs env arg
226+
227+ (P _ (UN a) _, [_, arg])
228+ | a == txt "assert_total"
229+ -> irTerm vs env arg
230+
231+ (P _ (UN p) _, [_, arg])
232+ | p == txt "par"
233+ -> do arg' <- irTerm vs env arg
234+ return $ LOp LPar [LLazyExp arg']
235+
236+ (P _ (UN pf) _, [arg])
237+ | pf == txt "prim_fork"
238+ -> do arg' <- irTerm vs env arg
239+ return $ LOp LFork [LLazyExp arg']
240+
241+ (P _ (UN m) _, [_,size,t])
242+ | m == txt "malloc"
243+ -> irTerm vs env t
244+
245+ (P _ (UN tm) _, [_,t])
246+ | tm == txt "trace_malloc"
247+ -> irTerm vs env t -- TODO
248+
249+ -- This case is here until we get more general inlining. It's just
250+ -- a really common case, and the laziness hurts...
251+ (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
252+ (App (P _ (UN d') _) e)])
253+ | be == txt "boolElim"
254+ , d == txt "Delay"
255+ , d' == txt "Delay"
256+ -> do
257+ x' <- irTerm vs env x
258+ t' <- irTerm vs env t
259+ e' <- irTerm vs env e
260+ return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
261+ ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
262+ ])
263+
264+ (P (DCon t arity) n _, args) -> do
265+ ist <- getIState
266+ let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
267+ used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
268+ args' = [a | (i,a) <- zip [0..] args, i `elem` used]
269+
270+ when (length args > arity) $
271+ ifail ("oversaturated data ctor: " ++ show tm)
272+
273+ if length args' == 1 && detag -- detaggable
274+ then irTerm vs env (head args') -- newtype
275+ else irCon vs env (length used) n args'
276+
277+ (P (TCon t a) n _, args) -> return LNothing
278+
279+ (P _ n _, args) -> do
280+ ist <- getIState
281+ case lookup n (idris_scprims ist) of
282+ -- if it's a primitive that is already saturated,
283+ -- compile to the corresponding op here already to save work
284+ Just (arity, op) | length args == arity
285+ -> LOp op <$> mapM (irTerm vs env) args
286+
287+ -- otherwise, just apply the name
288+ _ -> applyName n ist args
289+
290+ -- turn de bruijn vars into regular named references and try again
291+ (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
292+
293+ (f, args)
294+ -> LApp False
295+ <$> irTerm vs env f
296+ <*> mapM (irTerm vs env) args
297+
298+ where
299+ applyName :: Name -> IState -> [Term] -> Idris LExp
300+ applyName n ist args =
301+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
302+ where
303+ erase (i, x)
304+ | i >= arity || i `elem` used = x
305+ | otherwise = Erased
306+
307+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
308+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
309+ Just (TyDecl (DCon tag ar) _) -> ar
310+ Just (TyDecl Ref ty) -> length $ getArgTys ty
311+ Just (Operator ty ar op) -> ar
312+ Just def -> error $ "unknown arity: " ++ show (n, def)
313+ Nothing -> 0 -- no definition, probably local name => can't erase anything
314+
315+ -- name for purposes of usage info lookup
316+ uName
317+ | Just n' <- viMethod =<< M.lookup n vs = n'
318+ | otherwise = n
319+
320+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
321+ fst4 (x,_,_,_) = x
322+
323+irTerm vs env (P _ n _) = return $ LV (Glob n)
324+irTerm vs env (V i)
325+ | i >= 0 && i < length env = return $ LV (Glob (env!!i))
326+ | otherwise = ifail $ "bad de bruijn index: " ++ show i
327+
328+irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
329+ where
330+ n' = uniqueName n env
331+
332+irTerm vs env (Bind n (Let _ v) sc)
333+ = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
334+
335+irTerm vs env (Bind _ _ _) = return $ LNothing
336+
337+irTerm vs env (Proj t (-1)) = do
338+ t' <- irTerm vs env t
339+ return $ LOp (LMinus (ATInt ITBig))
340+ [t', LConst (BI 1)]
341+
342+irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
343+irTerm vs env (Constant c) = return $ LConst c
344+irTerm vs env (TType _) = return $ LNothing
345+irTerm vs env Erased = return $ LNothing
346+irTerm vs env Impossible = return $ LNothing
347+
348+irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
349+irCon vs env arity n args
350+ | length args > arity
351+ = error $ "oversaturated data constructor: " ++ show (n, args)
352+
353+ -- saturated
354+ | length args == arity
355+ = buildApp (LV (Glob n)) args
356+
357+ -- undersaturated, wrap in lambdas
358+ | otherwise
359+ = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
360+ extraTs = [P Bound n undefined | n <- extraNs]
361+ in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
362+ where
363+ buildApp e [] = return e
364+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
365+
366+doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
367+doForeign vs env (_ : fgn : args)
368+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
369+ = case getFTypes fgnArgTys of
370+ Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
371+ Just tys -> do
372+ args' <- mapM (irTerm vs env) (init args)
373+ return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
374+
375+ | otherwise = ifail "Badly formed foreign function call"
376+ where
377+ getFTypes :: TT Name -> Maybe [FType]
378+ getFTypes tm = case unApply tm of
379+ -- nil : {a : Type} -> List a
380+ (nil, [_]) -> Just []
381+ -- cons : {a : Type} -> a -> List a -> List a
382+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
383+ _ -> Nothing
384+
385+ mkIty' (P _ (UN ty) _) = mkIty (str ty)
386+ mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
387+ | fi == txt "FIntT"
388+ = mkIntIty (str intTy)
389+
390+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
391+ | ff == txt "FFunction"
392+ , fa == txt "FAny"
393+ , io == txt "IO"
332394 = FFunctionIO
333−mkIty' (App (App (P _ (UN ff) _) _) _)
334− | ff == txt "FFunction" = FFunction
335−mkIty' _ = FAny
336−
337−-- would be better if these FInt types were evaluated at compile time
338−-- TODO: add %eval directive for such things
339−
340−mkIty "FFloat" = FArith ATFloat
341−mkIty "FInt" = mkIntIty "ITNative"
342−mkIty "FChar" = mkIntIty "ITChar"
343−mkIty "FByte" = mkIntIty "IT8"
344−mkIty "FShort" = mkIntIty "IT16"
345−mkIty "FLong" = mkIntIty "IT64"
346−mkIty "FBits8" = mkIntIty "IT8"
347−mkIty "FBits16" = mkIntIty "IT16"
348−mkIty "FBits32" = mkIntIty "IT32"
349−mkIty "FBits64" = mkIntIty "IT64"
350−mkIty "FString" = FString
351−mkIty "FPtr" = FPtr
352−mkIty "FManagedPtr" = FManagedPtr
353−mkIty "FUnit" = FUnit
354−mkIty "FFunction" = FFunction
355−mkIty "FFunctionIO" = FFunctionIO
356−mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
357−mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
358−mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
359−mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
360−mkIty x = error $ "Unknown type " ++ x
361−
362−mkIntIty "ITNative" = FArith (ATInt ITNative)
363−mkIntIty "ITChar" = FArith (ATInt ITChar)
364−mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
365−mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
366−mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
367−mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
368−
369−zname = sNS (sUN "Z") ["Nat","Prelude"]
370−sname = sNS (sUN "S") ["Nat","Prelude"]
371−
372−instance ToIR ([Name], SC) where
373− ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
374− tree' <- ir tree
375− return $ LLam args tree'
376−
377−instance ToIR SC where
378− ir t = ir' t where
379−
380− ir' (STerm t) = ir t
381− ir' (UnmatchedCase str) = return $ LError str
382− ir' (ProjCase tm alts) = do tm' <- ir tm
383− alts' <- mapM (mkIRAlt tm') alts
384− return $ LCase tm' alts'
385− ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
386− return $ LCase (LV (Glob n)) alts'
387− ir' ImpossibleCase = return LNothing
388−
389− -- special cases for Z and S
390− -- Needs rethink: projections make this fail
391−-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
392−-- = mkIRAlt n (ConstCase (BI 0) rhs)
393−-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
394−-- = do n' <- ir n
395−-- rhs' <- ir rhs
396−-- return $ LDefaultCase
397−-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
398−-- rhs')
399− mkIRAlt _ (ConCase n t args rhs)
400− = do rhs' <- ir rhs
401− return $ LConCase (-1) n args rhs'
402− mkIRAlt _ (ConstCase x rhs)
403− | matchable x
404− = do rhs' <- ir rhs
405− return $ LConstCase x rhs'
406− | matchableTy x
407− = do rhs' <- ir rhs
408− return $ LDefaultCase rhs'
409− mkIRAlt tm (SucCase n rhs)
410− = do rhs' <- ir rhs
411− return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
412− [tm,
413− LConst (BI 1)]) rhs')
414−-- return $ LSucCase n rhs'
415− mkIRAlt _ (ConstCase c rhs)
416− = ifail $ "Can't match on (" ++ show c ++ ")"
417− mkIRAlt _ (DefaultCase rhs)
418− = do rhs' <- ir rhs
419− return $ LDefaultCase rhs'
420−
421− matchable (I _) = True
422− matchable (BI _) = True
423− matchable (Ch _) = True
424− matchable (Str _) = True
425− matchable _ = False
426−
427− matchableTy (AType (ATInt ITNative)) = True
428− matchableTy (AType (ATInt ITBig)) = True
429− matchableTy (AType (ATInt ITChar)) = True
430− matchableTy StrType = True
431−
432− matchableTy (AType (ATInt (ITFixed IT8))) = True
433− matchableTy (AType (ATInt (ITFixed IT16))) = True
434− matchableTy (AType (ATInt (ITFixed IT32))) = True
435− matchableTy (AType (ATInt (ITFixed IT64))) = True
436−
437− matchableTy _ = False
438395
396+ mkIty' (App (App (P _ (UN ff) _) _) _)
397+ | ff == txt "FFunction"
398+ = FFunction
399+
400+ mkIty' _ = FAny
401+
402+ -- would be better if these FInt types were evaluated at compile time
403+ -- TODO: add %eval directive for such things
404+
405+ mkIty "FFloat" = FArith ATFloat
406+ mkIty "FInt" = mkIntIty "ITNative"
407+ mkIty "FChar" = mkIntIty "ITChar"
408+ mkIty "FByte" = mkIntIty "IT8"
409+ mkIty "FShort" = mkIntIty "IT16"
410+ mkIty "FLong" = mkIntIty "IT64"
411+ mkIty "FBits8" = mkIntIty "IT8"
412+ mkIty "FBits16" = mkIntIty "IT16"
413+ mkIty "FBits32" = mkIntIty "IT32"
414+ mkIty "FBits64" = mkIntIty "IT64"
415+ mkIty "FString" = FString
416+ mkIty "FPtr" = FPtr
417+ mkIty "FManagedPtr" = FManagedPtr
418+ mkIty "FUnit" = FUnit
419+ mkIty "FFunction" = FFunction
420+ mkIty "FFunctionIO" = FFunctionIO
421+ mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
422+ mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
423+ mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
424+ mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
425+ mkIty x = error $ "Unknown type " ++ x
426+
427+ mkIntIty "ITNative" = FArith (ATInt ITNative)
428+ mkIntIty "ITChar" = FArith (ATInt ITChar)
429+ mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
430+ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
431+ mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
432+ mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
433+
434+irTree :: [Name] -> SC -> Idris LExp
435+irTree args tree = do
436+ logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
437+ LLam args <$> irSC M.empty tree
438+
439+irSC :: Vars -> SC -> Idris LExp
440+irSC vs (STerm t) = irTerm vs [] t
441+irSC vs (UnmatchedCase str) = return $ LError str
442+irSC vs (ProjCase tm alts) = do
443+ tm' <- irTerm vs [] tm
444+ alts' <- mapM (irAlt vs tm') alts
445+ return $ LCase tm' alts'
446+
447+-- Transform matching on Delay to applications of Force.
448+irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
449+ | delay == txt "Delay"
450+ = irSC vs $ mkForce n n' sc
451+
452+-- There are two transformations in this case:
453+--
454+-- 1. Newtype-case elimination:
455+-- case {e0} of
456+-- wrap({e1}) -> P({e1}) ==> P({e0})
457+--
458+-- This is important because newtyped constructors are compiled away entirely
459+-- and we need to do that everywhere.
460+--
461+-- 2. Unused-case elimination (only valid for singleton branches):
462+-- case {e0} of ==> P
463+-- C(x,y) -> P[... x,y not used ...]
464+--
465+-- This is important for runtime because sometimes we case on irrelevant data:
466+--
467+-- In the example above, {e0} will most probably have been erased
468+-- so this vain projection would make the resulting program segfault
469+-- because the code generator still emits a PROJECT(...) G-machine instruction.
470+--
471+-- Hence, we check whether the variables are used at all
472+-- and erase the casesplit if they are not.
473+irSC vs (Case n [alt]) = do
474+ replacement <- case alt of
475+ ConCase cn a ns sc -> do
476+ detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
477+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
478+ if detag && length used == 1
479+ then return . Just $ substSC (ns !! head used) n sc
480+ else return Nothing
481+ _ -> return Nothing
482+
483+ case replacement of
484+ Just sc -> irSC vs sc
485+ _ -> do
486+ alt' <- irAlt vs (LV (Glob n)) alt
487+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of
488+ [] -> subexpr alt' -- strip the unused top-most case
489+ _ -> LCase (LV (Glob n)) [alt']
490+ where
491+ namesBoundIn :: LAlt -> [Name]
492+ namesBoundIn (LConCase cn i ns sc) = ns
493+ namesBoundIn (LConstCase c sc) = []
494+ namesBoundIn (LDefaultCase sc) = []
495+
496+ subexpr :: LAlt -> LExp
497+ subexpr (LConCase _ _ _ e) = e
498+ subexpr (LConstCase _ e) = e
499+ subexpr (LDefaultCase e) = e
500+
501+irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
502+irSC vs ImpossibleCase = return LNothing
503+
504+irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
505+
506+-- this leaves out all unused arguments of the constructor
507+irAlt vs _ (ConCase n t args sc) = do
508+ used <- getUsed . lookup n <$> getIState
509+ let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
510+ LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
511+ where
512+ lookup n = lookupCtxtExact n . idris_callgraph
513+ getUsed = maybe [] (map fst . usedpos)
514+
515+ methodVars = case n of
516+ SN (InstanceCtorN className)
517+ -> M.fromList [(v, VI
518+ { viMethod = Just $ mkFieldName n i
519+ }) | (v,i) <- zip args [0..]]
520+ _
521+ -> M.empty -- not an instance constructor
522+
523+irAlt vs _ (ConstCase x rhs)
524+ | matchable x = LConstCase x <$> irSC vs rhs
525+ | matchableTy x = LDefaultCase <$> irSC vs rhs
526+ where
527+ matchable (I _) = True
528+ matchable (BI _) = True
529+ matchable (Ch _) = True
530+ matchable (Str _) = True
531+ matchable _ = False
532+
533+ matchableTy (AType (ATInt ITNative)) = True
534+ matchableTy (AType (ATInt ITBig)) = True
535+ matchableTy (AType (ATInt ITChar)) = True
536+ matchableTy StrType = True
537+
538+ matchableTy (AType (ATInt (ITFixed IT8))) = True
539+ matchableTy (AType (ATInt (ITFixed IT16))) = True
540+ matchableTy (AType (ATInt (ITFixed IT32))) = True
541+ matchableTy (AType (ATInt (ITFixed IT64))) = True
542+
543+ matchableTy _ = False
544+
545+irAlt vs tm (SucCase n rhs) = do
546+ rhs' <- irSC vs rhs
547+ return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
548+ [tm,
549+ LConst (BI 1)]) rhs')
550+
551+irAlt vs _ (ConstCase c rhs)
552+ = ifail $ "Can't match on (" ++ show c ++ ")"
553+
554+irAlt vs _ (DefaultCase rhs)
555+ = LDefaultCase <$> irSC vs rhs