git.iko.soy/Idris-dev
on master help sign in
Ensure erasure happens under 'force'
32d47a5Edwin Brady
src/IRTS/Compiler.hs+4−2
compare with master
unifiedsplit
@@ -486,6 +486,7 @@ irTree args tree = do
486irSC :: Vars -> SC -> Idris LExp
486irSC :: Vars -> SC -> Idris LExp
487irSC vs (STerm t) = irTerm vs [] t
487irSC vs (STerm t) = irTerm vs [] t
488irSC vs (UnmatchedCase str) = return $ LError str
488irSC vs (UnmatchedCase str) = return $ LError str
489+
489irSC vs (ProjCase tm alts) = do
490irSC vs (ProjCase tm alts) = do
490 tm' <- irTerm vs [] tm
491 tm' <- irTerm vs [] tm
491 alts' <- mapM (irAlt vs tm') alts
492 alts' <- mapM (irAlt vs tm') alts
@@ -494,8 +495,9 @@ irSC vs (ProjCase tm alts) = do
494-- Transform matching on Delay to applications of Force.
495-- Transform matching on Delay to applications of Force.
495irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
496irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
496 | delay == txt "Delay"
497 | delay == txt "Delay"
497− = irSC vs $ mkForce n n' sc
498+ = do sc' <- irSC vs $ mkForce n' n sc
498−
499+ return $ LLet n' (LForce (LV (Glob n))) sc'
500+
499-- There are two transformations in this case:
501-- There are two transformations in this case:
500--
502--
501-- 1. Newtype-case elimination:
503-- 1. Newtype-case elimination:
src/Idris/Core/CaseTree.hs+5−6
@@ -766,19 +766,20 @@ substAlt n repl (SucCase n' sc)
766 | otherwise = SucCase n' (substSC n repl sc)
766 | otherwise = SucCase n' (substSC n repl sc)
767substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
767substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
768
768
769+-- mkForce n' n t updates the tree t under the assumption that
770+-- n' = force n (so basically updating n to n')
769mkForce :: Name -> Name -> SC -> SC
771mkForce :: Name -> Name -> SC -> SC
770mkForce = mkForceSC
772mkForce = mkForceSC
771 where
773 where
772 mkForceSC n arg (Case x alts) | x == arg
774 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
774
776
775 mkForceSC n arg (Case x alts)
777 mkForceSC n arg (Case x alts)
776 = Case x (map (mkForceAlt n arg) alts)
778 = Case x (map (mkForceAlt n arg) alts)
777
779
778 mkForceSC n arg (ProjCase t alts)
780 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
780
782
781− mkForceSC n arg (STerm t) = STerm (forceTm n arg t)
782 mkForceSC n arg c = c
783 mkForceSC n arg c = c
783
784
784 mkForceAlt n arg (ConCase cn t args rhs)
785 mkForceAlt n arg (ConCase cn t args rhs)
@@ -792,7 +793,5 @@ mkForce = mkForceSC
792 mkForceAlt n arg (DefaultCase rhs)
793 mkForceAlt n arg (DefaultCase rhs)
793 = DefaultCase (mkForceSC n arg rhs)
794 = DefaultCase (mkForceSC n arg rhs)
794
795
795− forceTm n arg t = subst arg (forceArg n) t
796+ forceTm n arg t = subst n arg t
796
797
797− forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)
798− (P Bound n Erased)