0203531 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix case-inspection of lazy values.

0203531Matus Tejiscak13 years ago

src/IRTS/Compiler.hs+4−4

compare with master

unifiedsplit

@@ -418,10 +418,10 @@ irTree args tree = do

418irSC :: Vars -> SC -> Idris LExp

419irSC vs (STerm t) = irTerm vs [] t

420irSC vs (UnmatchedCase str) = return $ LError str

421−irSC vs (ProjCase tm alt) = do

421+irSC vs (ProjCase tm alts) = do

422− tm' <- irTerm vs [] tm

422+ tm' <- irTerm vs [] tm

423− alt' <- irAlt vs tm' alt

423+ alts' <- mapM (irAlt vs tm') alts

424− return $ LCase tm' [alt']

424+ return $ LCase tm' alts'

425

426-- There are two transformations in this case:

427--

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

@@ -16,7 +16,7 @@ data CaseDef = CaseDef [Name] !SC [Term]

16 deriving Show

18data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

19− | ProjCase t (CaseAlt' t) -- ^ special case for projections

19+ | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection

20 | STerm !t

21 | UnmatchedCase String -- ^ error message

22 | ImpossibleCase -- ^ already checked to be impossible

@@ -46,8 +46,8 @@ instance Show t => Show (SC' t) where

46 where

47 show' i (Case n alts) = "case " ++ show n ++ " of\n" ++ indent i ++

48 showSep ("\n" ++ indent i) (map (showA i) alts)

49− show' i (ProjCase tm alt) = "case " ++ show tm ++ " of " ++

49+ show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++

50− showSep ("\n" ++ indent i) (map (showA i) [alt])

50+ showSep ("\n" ++ indent i) (map (showA i) alts)

51 show' i (STerm tm) = show tm

52 show' i (UnmatchedCase str) = "error " ++ show str

53 show' i ImpossibleCase = "impossible"

@@ -97,7 +97,7 @@ small n args t = let as = findAllUsedArgs t args in

97namesUsed :: SC -> [Name]

98namesUsed sc = nub $ nu' [] sc where

99 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]

100− nu' ps (ProjCase t alt) = nub $ nut ps t ++ nua ps alt

100+ nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

101 nu' ps (STerm t) = nub $ nut ps t

102 nu' ps _ = []

103

@@ -122,7 +122,7 @@ namesUsed sc = nub $ nu' [] sc where

122findCalls :: SC -> [Name] -> [(Name, [[Name]])]

123findCalls sc topargs = nub $ nu' topargs sc where

124 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

125− nu' ps (ProjCase t alt) = nub (nut ps t ++ nua ps alt)

125+ nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

126 nu' ps (STerm t) = nub $ nut ps t

127 nu' ps _ = []

128

@@ -175,7 +175,7 @@ findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

175

176findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where

177 nu' (Case n alts) = n : concatMap nua alts

178− nu' (ProjCase t alt) = directUse t ++ nua alt

178+ nu' (ProjCase t alts) = directUse t ++ concatMap nua alts

179 nu' (STerm t) = directUse t

180 nu' _ = []

181

@@ -581,13 +581,14 @@ depatt ns tm = dp [] tm

581prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

582 -> SC -> SC

583prune proj (Case n alts)

584− = let alts' = filter notErased (map pruneAlt alts) in

584+ = let alts' = filter notErased $ map pruneAlt alts

585− case alts' of

585+ in case alts' of

586 [] -> ImpossibleCase

587+

587− as@(ConCase (UN delay) i [arg] sc : _)

588+ [ConCase (UN delay) i [t, a, arg] sc]

589+ | proj

588− | delay == txt "Delay"

590+ , delay == txt "Delay"

589− -> if proj then mkForce n arg sc

591+ -> mkForce n arg sc

590− else Case n as

591

592

592 -- Projection transformations prevent us from seeing some uses of ctor fields

593 -- Projection transformations prevent us from seeing some uses of ctor fields

593 -- because they delete information about which ctor is being used.

594 -- because they delete information about which ctor is being used.

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

599 --as@[ConCase cn i args sc]

600 --as@[ConCase cn i args sc]

600 -- | proj -> mkProj n 0 args (prune proj sc)

601 -- | proj -> mkProj n 0 args (prune proj sc)

601

602

602− as@[SucCase cn sc]

603+ [SucCase cn sc]

603 | proj

604 | proj

604− , not (cn `improjectibleSC` sc)

605+ , cn `projectibleInSC` sc -- TODO: remove this and use the almighty ProjCase

605 -> projRep cn n (-1) $ prune proj sc

606 -> projRep cn n (-1) $ prune proj sc

606

607

607− as@[ConstCase _ sc]

608+ [ConstCase _ sc]

608 -> prune proj sc

609 -> prune proj sc

609

610

610 -- Bit of a hack here! The default case will always be 0, make sure

611 -- Bit of a hack here! The default case will always be 0, make sure

@@ -613,87 +614,86 @@ prune proj (Case n alts)

613 -> Case n [ConstCase (BI 0) dc, s]

614 -> Case n [ConstCase (BI 0) dc, s]

614

615

615 as -> Case n as

616 as -> Case n as

617+ where

616− where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)

618+ pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)

617− pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)

619+ pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)

618− pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)

620+ pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)

619− pruneAlt (SucCase n sc) = SucCase n (prune proj sc)

621+ pruneAlt (SucCase n sc) = SucCase n (prune proj sc)

620− pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

622+ pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

621−

623+

622− notErased (DefaultCase (STerm Erased)) = False

624+ notErased (DefaultCase (STerm Erased)) = False

623− notErased (DefaultCase ImpossibleCase) = False

625+ notErased (DefaultCase ImpossibleCase) = False

624− notErased _ = True

626+ notErased _ = True

625−

627+

628+ -- single-alternative case on a forced value

629+ -- can be translated to a ProjCase directly

626− mkForce n arg (Case x [alt])

630+ mkForce n arg (Case x alts) | x == arg

627− | x == arg = ProjCase (forceArg n) (mkForceAlt n arg alt)

631+ = ProjCase (forceArg n) $ map (mkForceAlt n arg) alts

632+

628− mkForce n arg (Case x alts)

633+ mkForce n arg (Case x alts)

629− = Case x (map (mkForceAlt n arg) alts)

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

635+

630− mkForce n arg (ProjCase t alt)

636+ mkForce n arg (ProjCase t alts)

631− = ProjCase (forceTm n arg t) (mkForceAlt n arg alt)

637+ = ProjCase (forceTm n arg t) $ map (mkForceAlt n arg) alts

638+

632− mkForce n arg (STerm t) = STerm (forceTm n arg t)

639+ mkForce n arg (STerm t) = STerm (forceTm n arg t)

633− mkForce n arg c = c

640+ mkForce n arg c = c

634−

641+

635− mkForceAlt n arg (ConCase cn t args rhs)

642+ mkForceAlt n arg (ConCase cn t args rhs)

636− = ConCase cn t args (mkForce n arg rhs)

643+ = ConCase cn t args (mkForce n arg rhs)

637− mkForceAlt n arg (FnCase cn args rhs)

644+ mkForceAlt n arg (FnCase cn args rhs)

638− = FnCase cn args (mkForce n arg rhs)

645+ = FnCase cn args (mkForce n arg rhs)

639− mkForceAlt n arg (ConstCase t rhs)

646+ mkForceAlt n arg (ConstCase t rhs)

640− = ConstCase t (mkForce n arg rhs)

647+ = ConstCase t (mkForce n arg rhs)

641− mkForceAlt n arg (SucCase sn rhs)

648+ mkForceAlt n arg (SucCase sn rhs)

642− = SucCase sn (mkForce n arg rhs)

649+ = SucCase sn (mkForce n arg rhs)

643− mkForceAlt n arg (DefaultCase rhs)

650+ mkForceAlt n arg (DefaultCase rhs)

644− = DefaultCase (mkForce n arg rhs)

651+ = DefaultCase (mkForce n arg rhs)

645−

652+

646− -- Figure out whether the name is improjectible in the SC:

653+ -- Figure out whether the name is projectible in the SC:

647− -- For example, (Case n _) only admits /names/ as "n"

654+ -- For example, (Case n _) only admits /names/ as "n"

648− -- so we cannot replace n with a projection of anything.

655+ -- so we cannot replace n with a projection of anything.

649− improjectibleSC :: Name -> SC -> Bool

656+ projectibleInSC :: Name -> SC -> Bool

650− n `improjectibleSC` Case x alts = n == x || (n `improjectibleAlt`) `any` alts

657+ n `projectibleInSC` Case x alts = (n /= x) && (n `projectibleInAlt`) `all` alts

651− n `improjectibleSC` ProjCase t alt = n `improjectibleAlt` alt

658+ n `projectibleInSC` ProjCase t alts = (n `projectibleInAlt`) `all` alts

652− n `improjectibleSC` _ = False -- we can replace freely in terms

659+ n `projectibleInSC` _ = True -- we can replace freely in terms

653−

660+

654− improjectibleAlt :: Name -> CaseAlt -> Bool

661+ projectibleInAlt :: Name -> CaseAlt -> Bool

655− n `improjectibleAlt` ConCase cn t args sc = n `improjectibleSC` sc

662+ n `projectibleInAlt` ConCase cn t args sc = n `projectibleInSC` sc

656− n `improjectibleAlt` FnCase cn args sc = n `improjectibleSC` sc

663+ n `projectibleInAlt` FnCase cn args sc = n `projectibleInSC` sc

657− n `improjectibleAlt` ConstCase t sc = n `improjectibleSC` sc

664+ n `projectibleInAlt` ConstCase t sc = n `projectibleInSC` sc

658− n `improjectibleAlt` SucCase cn sc = n `improjectibleSC` sc

665+ n `projectibleInAlt` SucCase cn sc = n `projectibleInSC` sc

659− n `improjectibleAlt` DefaultCase sc = n `improjectibleSC` sc

666+ n `projectibleInAlt` DefaultCase sc = n `projectibleInSC` sc

660−

667+

661− forceTm n arg t = subst arg (forceArg n) t

668+ forceTm n arg t = subst arg (forceArg n) t

662−

669+

663− forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

670+ forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

664− (P Bound n Erased)

671+ (P Bound n Erased)

665−

672+

666− mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs

673+ mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs

667−

674+

668− -- Change every 'n' in sc to 'n-1'

669−-- mkProjS n cn sc = prune proj (fmap projn sc) where

670−-- projn pn@(P _ n' _)

671−-- | cn == n' = App (App (P Ref (UN "prim__subBigInt") Erased)

672−-- (P Bound n Erased)) (Constant (BI 1))

673−-- projn t = t

674−

675− projRep :: Name -> Name -> Int -> SC -> SC

675+ projRep :: Name -> Name -> Int -> SC -> SC

676− projRep arg n i (Case x [alt]) | x == arg

676+ projRep arg n i (Case x alts) | x == arg

677− = ProjCase (Proj (P Bound n Erased) i) (projRepAlt arg n i alt)

677+ = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts

678− projRep arg n i (Case x alts)

678+ projRep arg n i (Case x alts)

679− = Case x (map (projRepAlt arg n i) alts)

679+ = Case x (map (projRepAlt arg n i) alts)

680− projRep arg n i (ProjCase t alt)

680+ projRep arg n i (ProjCase t alts)

681− = ProjCase (projRepTm arg n i t) (projRepAlt arg n i alt)

681+ = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts

682− projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

682+ projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

683− projRep arg n i c = c -- unmatched

683+ projRep arg n i c = c

684−

684+

685− projRepAlt arg n i (ConCase cn t args rhs)

685+ projRepAlt arg n i (ConCase cn t args rhs)

686− = ConCase cn t args (projRep arg n i rhs)

686+ = ConCase cn t args (projRep arg n i rhs)

687− projRepAlt arg n i (FnCase cn args rhs)

687+ projRepAlt arg n i (FnCase cn args rhs)

688− = FnCase cn args (projRep arg n i rhs)

688+ = FnCase cn args (projRep arg n i rhs)

689− projRepAlt arg n i (ConstCase t rhs)

689+ projRepAlt arg n i (ConstCase t rhs)

690− = ConstCase t (projRep arg n i rhs)

690+ = ConstCase t (projRep arg n i rhs)

691− projRepAlt arg n i (SucCase sn rhs)

691+ projRepAlt arg n i (SucCase sn rhs)

692− = SucCase sn (projRep arg n i rhs)

692+ = SucCase sn (projRep arg n i rhs)

693− projRepAlt arg n i (DefaultCase rhs)

693+ projRepAlt arg n i (DefaultCase rhs)

694− = DefaultCase (projRep arg n i rhs)

694+ = DefaultCase (projRep arg n i rhs)

695−

695+

696− projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t

696+ projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t

697

698prune _ t = t

699

src/Idris/Core/Evaluate.hs+2−2

@@ -389,9 +389,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

389 etm' <- ev ntimes stk (not (conHeaded tm))

390 (amap ++ env) etm

391 return $ Just etm'

392− evTree ntimes stk top env amap (ProjCase t alt)

392+ evTree ntimes stk top env amap (ProjCase t alts)

393 = do t' <- ev ntimes stk top env t

394− doCase ntimes stk top env amap t' [alt]

394+ doCase ntimes stk top env amap t' alts

395 evTree ntimes stk top env amap (Case n alts)

396 = case lookup n amap of

397 Just v -> doCase ntimes stk top env amap v alts

src/Idris/IBC.hs+3−3

@@ -177,9 +177,9 @@ ibc i (IBCDef n) f

177

178 updateSC (Case n alts) = do alts' <- mapM updateAlt alts

179 return (Case n alts')

180− updateSC (ProjCase t alt) = do t' <- update t

180+ updateSC (ProjCase t alts) = do t' <- update t

181− alt' <- updateAlt alt

181+ alts' <- mapM updateAlt alts

182− return (ProjCase t' alt')

182+ return (ProjCase t' alts')

183 updateSC (STerm t) = do t' <- update t

184 return (STerm t')

185 updateSC t = return t