git.iko.soy/Idris-dev
on master help sign in
More small fixes.
7688a12Matus Tejiscak
src/IRTS/Compiler.hs+10−6
compare with master
unifiedsplit
@@ -222,10 +222,9 @@ instance ToIR (TT Name) where
222
222
223 | (P (DCon t a) n _, args) <- unApply tm = do
223 | (P (DCon t a) n _, args) <- unApply tm = do
224 cg <- idris_callgraph <$> getIState
224 cg <- idris_callgraph <$> getIState
225− case lookupCtxtExact n cg of
225+ let used = maybe [] (map fst . usedpos) $ lookupCtxtExact n cg
226− Just (CGInfo _ _ _ _ usedpos)
227− -> irCon env t a n [if i `elem` map fst usedpos then a else Erased | (i,a) <- zip [0..] args]
226+ args' = [if i `elem` used then a else Erased | (i,a) <- zip [0..] args]
228− Nothing -> return LNothing -- no usage info -> not used at all
227+ irCon env t a n args'
229
228
230 | (P (TCon t a) n _, args) <- unApply tm
229 | (P (TCon t a) n _, args) <- unApply tm
231 = return LNothing
230 = return LNothing
@@ -238,14 +237,19 @@ instance ToIR (TT Name) where
238 Just (arity, op) | length args == arity
237 Just (arity, op) | length args == arity
239 -> LOp op <$> mapM (ir' env) args
238 -> LOp op <$> mapM (ir' env) args
240
239
240+ _ -> applyName n ist args
241+
242+{- collapsibility is turned off for now
241 _
243 _
242 -- if it's collapsible, compile to LNothing
244 -- if it's collapsible, compile to LNothing
243 | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True
245 | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True
244 -> return LNothing
246 -> return LNothing
245−
247+
246 -- otherwise, compile normally
248 -- otherwise, compile normally
247 | otherwise -> applyName n ist args
249 | otherwise -> applyName n ist args
248
250
251+-}
252+
249 | (f, args) <- unApply tm
253 | (f, args) <- unApply tm
250 = do f' <- ir' env f
254 = do f' <- ir' env f
251 args' <- mapM (ir' env) args
255 args' <- mapM (ir' env) args
@@ -266,7 +270,7 @@ instance ToIR (TT Name) where
266 [Operator ty ar op] -> ar
270 [Operator ty ar op] -> ar
267 _ -> 0
271 _ -> 0
268
272
269− used = fromMaybe [] (map fst . usedpos <$> lookupCtxtExact n (idris_callgraph ist))
273+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
270 fst4 (x,_,_,_) = x
274 fst4 (x,_,_,_) = x
271
275
272-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
276-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
src/Idris/Core/CaseTree.hs+10
@@ -587,15 +587,25 @@ prune proj (Case n alts)
587 | delay == txt "Delay"
587 | delay == txt "Delay"
588 -> if proj then mkForce n arg sc
588 -> if proj then mkForce n arg sc
589 else Case n as
589 else Case n as
590+
591+ -- Projection transformations prevent us from seeing some uses of ctor fields
592+ -- because they delete information about which ctor is being used.
593+ -- Consider:
594+ -- f (X x) = ... x ...
595+ -- vs.
596+ -- f x = ... x!0 ...
597+ -- There's currently no code to handle this stuff. (TODO)
590 as@[ConCase cn i args sc] -> if proj && False then mkProj n 0 args sc
598 as@[ConCase cn i args sc] -> if proj && False then mkProj n 0 args sc
591 else Case n as
599 else Case n as
592 as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc
600 as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc
593 else Case n as
601 else Case n as
594 as@[ConstCase _ sc] -> prune proj sc
602 as@[ConstCase _ sc] -> prune proj sc
603+
595 -- Bit of a hack here! The default case will always be 0, make sure
604 -- Bit of a hack here! The default case will always be 0, make sure
596 -- it gets caught first.
605 -- it gets caught first.
597 [s@(SucCase _ _), DefaultCase dc]
606 [s@(SucCase _ _), DefaultCase dc]
598 -> Case n [ConstCase (BI 0) dc, s]
607 -> Case n [ConstCase (BI 0) dc, s]
608+
599 as -> Case n as
609 as -> Case n as
600 where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
610 where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
601 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
611 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
src/Idris/Erasure.hs+6−4
@@ -174,9 +174,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
174 [ [(sUN "main" `sNS` ["Main"], Result)]
174 [ [(sUN "main" `sNS` ["Main"], Result)]
175 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]
175 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]
176
176
177− -- MkIO is presumably read by run__IO but this cannot be observed
177+ -- MkIO is presumably read by run__IO
178− -- in the source code of programs.
178+ -- but this cannot be observed in the source code of programs.
179 , it "MkIO" [1]
179 , it "MkIO" [1]
180+ , it "prim__IO" [1]
180
181
181 -- these have been discovered as builtins but are not listed
182 -- these have been discovered as builtins but are not listed
182 -- among Idris.Primitives.primitives
183 -- among Idris.Primitives.primitives
@@ -360,7 +361,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
360 `ins` unconditionalDeps args
361 `ins` unconditionalDeps args
361
362
362 Proj t i
363 Proj t i
363− -> error $ "cannot analyse projection !" ++ show i ++ " of " ++ show t
364+ -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t
364
365
365 Erased -> M.empty
366 Erased -> M.empty
366
367
@@ -377,7 +378,8 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
377 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
378 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
378
379
379 -- projections (= methods)
380 -- projections (= methods)
381+ getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
380− getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t -- TODO?
382+ -- getDepsTerm vs bs cd t -- TODO?
381
383
382 -- the easy cases
384 -- the easy cases
383 getDepsTerm vs bs cd (Constant _) = M.empty
385 getDepsTerm vs bs cd (Constant _) = M.empty