e2dec8b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix single-arg-ness of ProjCase.

e2dec8bMatus Tejiscak13 years ago

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

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

617 notErased (DefaultCase ImpossibleCase) = False

618 notErased _ = True

619

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

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

620 mkForce n arg (Case x alts)

622 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)

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

624− mkForce n arg (ProjCase t alts)

624+ mkForce n arg (ProjCase t alt)

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

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

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

627 mkForce n arg c = c

628