git.iko.soy/Idris-dev
on master help sign in
Fix erasure from data ctors.
5ae2e58Matus Tejiscak
src/IRTS/Compiler.hs+6−5
compare with master
unifiedsplit
@@ -208,6 +208,7 @@ instance ToIR (TT Name) where
208 tm == txt "trace_malloc"
208 tm == txt "trace_malloc"
209 = do t' <- ir' env t
209 = do t' <- ir' env t
210 return t' -- TODO
210 return t' -- TODO
211+
211 -- This case is here until we get more general inlining. It's just
212 -- This case is here until we get more general inlining. It's just
212 -- a really common case, and the laziness hurts...
213 -- a really common case, and the laziness hurts...
213 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
214 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
@@ -218,16 +219,14 @@ instance ToIR (TT Name) where
218 e' <- ir' env e
219 e' <- ir' env e
219 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
220 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
220 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
221 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
222+
221− | (P (DCon t a) n _, args) <- unApply tm
223+ | (P (DCon t a) n _, args) <- unApply tm = do
222− = do
223 cg <- idris_callgraph <$> getIState
224 cg <- idris_callgraph <$> getIState
224 case lookupCtxtExact n cg of
225 case lookupCtxtExact n cg of
225 Just (CGInfo _ _ _ _ usedpos)
226 Just (CGInfo _ _ _ _ usedpos)
226 -> irCon env t a n [if i `elem` map fst usedpos then a else Erased | (i,a) <- zip [0..] args]
227 -> irCon env t a n [if i `elem` map fst usedpos then a else Erased | (i,a) <- zip [0..] args]
227− Nothing -> irCon env t a n args
228+ Nothing -> return LNothing -- no usage info -> not used at all
228
229
229− | (P (DCon t a) n _, args) <- unApply tm
230− = irCon env t a n args
231 | (P (TCon t a) n _, args) <- unApply tm
230 | (P (TCon t a) n _, args) <- unApply tm
232 = return LNothing
231 = return LNothing
233
232
@@ -263,6 +262,8 @@ instance ToIR (TT Name) where
263
262
264 arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
263 arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
265 [CaseOp ci ty tys def tot cdefs] -> length tys
264 [CaseOp ci ty tys def tot cdefs] -> length tys
265+ [TyDecl (DCon tag ar) _] -> ar
266+ [Operator ty ar op] -> ar
266 _ -> 0
267 _ -> 0
267
268
268 used = fromMaybe [] (map fst . usedpos <$> lookupCtxtExact n (idris_callgraph ist))
269 used = fromMaybe [] (map fst . usedpos <$> lookupCtxtExact n (idris_callgraph ist))
src/Idris/Erasure.hs+2−1
@@ -393,7 +393,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
393 getArity n = case lookupDef n ctx of
393 getArity n = case lookupDef n ctx of
394 [CaseOp ci ty tys def tot cdefs] -> length tys
394 [CaseOp ci ty tys def tot cdefs] -> length tys
395 [TyDecl (DCon tag arity) _] -> arity
395 [TyDecl (DCon tag arity) _] -> arity
396− _ -> 0
396+ [Operator ty arity op] -> arity
397+ df -> error $ "unknown entity " ++ show n ++ ": " ++ show df
397
398
398 -- convert applications of lambdas to lets
399 -- convert applications of lambdas to lets
399 -- Note that this transformation preserves de bruijn numbering
400 -- Note that this transformation preserves de bruijn numbering