e2dec8b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix single-arg-ness of ProjCase.

commite2dec8b830df16191acf18d5ab23d766c821cc93 authorMatus Tejiscak <ziman@functor.sk> dateTue 18 Feb 2014, 15:15 (13 years ago) parent58c0106

1 file changed+5−5

unifiedsplit

src/Idris/Core/CaseTree.hs+5−5

@@ -617,12 +617,12 @@ prune proj (Case n alts)

617617 notErased (DefaultCase ImpossibleCase) = False

618618 notErased _ = True

619619

620+ mkForce n arg (Case x [alt])

621+ | x == arg = ProjCase (forceArg n) (mkForceAlt n arg alt)

620622 mkForce n arg (Case x alts)

621− | x == arg = ProjCase (forceArg n)

622− (map (mkForceAlt n arg) alts)

623− | otherwise = Case x (map (mkForceAlt n arg) alts)

624− mkForce n arg (ProjCase t alts)

625− = ProjCase (forceTm n arg t) (map (mkForceAlt n arg) alts)

623+ = Case x (map (mkForceAlt n arg) alts)

624+ mkForce n arg (ProjCase t alt)

625+ = ProjCase (forceTm n arg t) (mkForceAlt n arg alt)

626626 mkForce n arg (STerm t) = STerm (forceTm n arg t)

627627 mkForce n arg c = c

628628