0203531 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix case-inspection of lazy values.

commit02035313b33d90bfe52a7e88f00ad5510da9d606 authorMatus Tejiscak <ziman@functor.sk> dateThu 27 Mar 2014, 14:08 (13 years ago) parent128d070

4 files changed+105−105

compare with master

unifiedsplit

src/IRTS/Compiler.hs+4−4 src/Idris/Core/CaseTree.hs+96−96 src/Idris/Core/Evaluate.hs+2−2 src/Idris/IBC.hs+3−3

src/IRTS/Compiler.hs+4−4

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

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

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

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

421−irSC vs (ProjCase tm alt) = do

422− tm' <- irTerm vs [] tm

423− alt' <- irAlt vs tm' alt

424− return $ LCase tm' [alt']

421+irSC vs (ProjCase tm alts) = do

422+ tm' <- irTerm vs [] tm

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

424+ return $ LCase tm' alts'

425425

426426-- There are two transformations in this case:

427427--

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

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

1616 deriving Show

1717

1818data 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

2020 | STerm !t

2121 | UnmatchedCase String -- ^ error message

2222 | ImpossibleCase -- ^ already checked to be impossible

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

4646 where

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

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

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

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

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

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

5151 show' i (STerm tm) = show tm

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

5353 show' i ImpossibleCase = "impossible"

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

9797namesUsed :: SC -> [Name]

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

9999 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

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

102102 nu' ps _ = []

103103

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

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

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

124124 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

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

127127 nu' ps _ = []

128128

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

175175

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

177177 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

179179 nu' (STerm t) = directUse t

180180 nu' _ = []

181181

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

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

582582 -> SC -> SC

583583prune proj (Case n alts)

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

585− case alts' of

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

585+ in case alts' of

586586 [] -> ImpossibleCase

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

588− | delay == txt "Delay"

589− -> if proj then mkForce n arg sc

590− else Case n as

587+

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

589+ | proj

590+ , delay == txt "Delay"

591+ -> mkForce n arg sc

591592

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

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

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

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

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

601602

602− as@[SucCase cn sc]

603+ [SucCase cn sc]

603604 | proj

604− , not (cn `improjectibleSC` sc)

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

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

606607

607− as@[ConstCase _ sc]

608+ [ConstCase _ sc]

608609 -> prune proj sc

609610

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

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

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

614615

615616 as -> Case n as

616− where 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)

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

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

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

621−

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

623− notErased (DefaultCase ImpossibleCase) = False

624− notErased _ = True

625−

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

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

628− mkForce n arg (Case x alts)

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

630− mkForce n arg (ProjCase t alt)

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

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

633− mkForce n arg c = c

634−

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

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

637− mkForceAlt n arg (FnCase cn args rhs)

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

639− mkForceAlt n arg (ConstCase t rhs)

640− = ConstCase t (mkForce n arg rhs)

641− mkForceAlt n arg (SucCase sn rhs)

642− = SucCase sn (mkForce n arg rhs)

643− mkForceAlt n arg (DefaultCase rhs)

644− = DefaultCase (mkForce n arg rhs)

645−

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

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

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

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

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

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

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

653−

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

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

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

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

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

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

660−

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

662−

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

664− (P Bound n Erased)

665−

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

667−

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

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

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

678− projRep arg n i (Case x alts)

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

680− projRep arg n i (ProjCase t alt)

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

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

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

684−

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

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

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

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

689− projRepAlt arg n i (ConstCase t rhs)

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

691− projRepAlt arg n i (SucCase sn rhs)

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

693− projRepAlt arg n i (DefaultCase rhs)

694− = DefaultCase (projRep arg n i rhs)

695−

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

617+ where

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

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

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

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

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

623+

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

625+ notErased (DefaultCase ImpossibleCase) = False

626+ notErased _ = True

627+

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

629+ -- can be translated to a ProjCase directly

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

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

632+

633+ mkForce n arg (Case x alts)

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

635+

636+ mkForce n arg (ProjCase t alts)

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

638+

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

640+ mkForce n arg c = c

641+

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

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

644+ mkForceAlt n arg (FnCase cn args rhs)

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

646+ mkForceAlt n arg (ConstCase t rhs)

647+ = ConstCase t (mkForce n arg rhs)

648+ mkForceAlt n arg (SucCase sn rhs)

649+ = SucCase sn (mkForce n arg rhs)

650+ mkForceAlt n arg (DefaultCase rhs)

651+ = DefaultCase (mkForce n arg rhs)

652+

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

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

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

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

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

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

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

660+

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

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

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

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

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

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

667+

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

669+

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

671+ (P Bound n Erased)

672+

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

674+

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

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

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

678+ projRep arg n i (Case x alts)

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

680+ projRep arg n i (ProjCase t alts)

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)

683+ projRep arg n i c = c

684+

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

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

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

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

689+ projRepAlt arg n i (ConstCase t rhs)

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

691+ projRepAlt arg n i (SucCase sn rhs)

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

693+ projRepAlt arg n i (DefaultCase rhs)

694+ = DefaultCase (projRep arg n i rhs)

695+

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

697697

698698prune _ t = t

699699

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

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

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

390390 (amap ++ env) etm

391391 return $ Just etm'

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

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

393393 = 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

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

396396 = case lookup n amap of

397397 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

177177

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

179179 return (Case n alts')

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

181− alt' <- updateAlt alt

182− return (ProjCase t' alt')

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

181+ alts' <- mapM updateAlt alts

182+ return (ProjCase t' alts')

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

184184 return (STerm t')

185185 updateSC t = return t