git.iko.soy/Idris-dev
on master help sign in
Ensure erasure happens under 'force'

Fixes #1367 I'm not yet convinced there isn't still potentially a similar problem under other forms of ProjCase, but since these only arise in unusual circumstances at the moment there isn't a problem *yet*!

commit32d47a5304959b85c8e0d092ab6e9385f2a537db authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 8 Jul 2014, 20:46 (12 years ago) parent6f6a167
2 files changed+9−8
compare with master
unifiedsplit
src/IRTS/Compiler.hs+4−2 src/Idris/Core/CaseTree.hs+5−6
src/IRTS/Compiler.hs+4−2
@@ -486,6 +486,7 @@ irTree args tree = do
486486irSC :: Vars -> SC -> Idris LExp
487487irSC vs (STerm t) = irTerm vs [] t
488488irSC vs (UnmatchedCase str) = return $ LError str
489+
489490irSC vs (ProjCase tm alts) = do
490491 tm' <- irTerm vs [] tm
491492 alts' <- mapM (irAlt vs tm') alts
@@ -494,8 +495,9 @@ irSC vs (ProjCase tm alts) = do
494495-- Transform matching on Delay to applications of Force.
495496irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
496497 | delay == txt "Delay"
497− = irSC vs $ mkForce n n' sc
498−
498+ = do sc' <- irSC vs $ mkForce n' n sc
499+ return $ LLet n' (LForce (LV (Glob n))) sc'
500+
499501-- There are two transformations in this case:
500502--
501503-- 1. Newtype-case elimination:
src/Idris/Core/CaseTree.hs+5−6
@@ -766,19 +766,20 @@ substAlt n repl (SucCase n' sc)
766766 | otherwise = SucCase n' (substSC n repl sc)
767767substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
768768
769+-- mkForce n' n t updates the tree t under the assumption that
770+-- n' = force n (so basically updating n to n')
769771mkForce :: Name -> Name -> SC -> SC
770772mkForce = mkForceSC
771773 where
772774 mkForceSC n arg (Case x alts) | x == arg
773− = ProjCase (forceArg n) $ map (mkForceAlt n arg) alts
775+ = Case n $ map (mkForceAlt n arg) alts
774776
775777 mkForceSC n arg (Case x alts)
776778 = Case x (map (mkForceAlt n arg) alts)
777779
778780 mkForceSC n arg (ProjCase t alts)
779− = ProjCase (forceTm n arg t) $ map (mkForceAlt n arg) alts
781+ = ProjCase t $ map (mkForceAlt n arg) alts
780782
781− mkForceSC n arg (STerm t) = STerm (forceTm n arg t)
782783 mkForceSC n arg c = c
783784
784785 mkForceAlt n arg (ConCase cn t args rhs)
@@ -792,7 +793,5 @@ mkForce = mkForceSC
792793 mkForceAlt n arg (DefaultCase rhs)
793794 = DefaultCase (mkForceSC n arg rhs)
794795
795− forceTm n arg t = subst arg (forceArg n) t
796+ forceTm n arg t = subst n arg t
796797
797− forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)
798− (P Bound n Erased)