218c735 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Mark 'case' on unique types as updatable

commit218c735d11a0ae71c632759b9d82dd7213ddc7db authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 16 Aug 2014, 17:28 (12 years ago) parent9abbc3f

9 files changed+103−95

compare with master

unifiedsplit

src/IRTS/Compiler.hs+5−5 src/Idris/Core/CaseTree.hs+69−74 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/Core/Evaluate.hs+2−2 src/Idris/Core/Execute.hs+1−1 src/Idris/Erasure.hs+2−2 src/Idris/IBC.hs+19−6 src/Idris/Transforms.hs+2−2 src/Idris/WhoCalls.hs+2−2

src/IRTS/Compiler.hs+5−5

@@ -513,7 +513,7 @@ irSC vs (ProjCase tm alts) = do

513513 return $ LCase tm' alts'

514514

515515-- Transform matching on Delay to applications of Force.

516−irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

516+irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

517517 | delay == txt "Delay"

518518 = do sc' <- irSC vs $ mkForce n' n sc

519519 return $ LLet n' (LForce (LV (Glob n))) sc'

@@ -540,7 +540,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

540540-- Hence, we check whether the variables are used at all

541541-- and erase the casesplit if they are not.

542542--

543−irSC vs (Case n [alt]) = do

543+irSC vs (Case up n [alt]) = do

544544 replacement <- case alt of

545545 ConCase cn a ns sc -> do

546546 detag <- fgetState (opt_detaggable . ist_optimisation cn)

@@ -584,13 +584,13 @@ irSC vs (Case n [alt]) = do

584584-- This work-around is not entirely optimal; the best approach would be

585585-- to ensure that such case trees don't arise in the first place.

586586--

587−irSC vs (Case n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

587+irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

588588 detag <- fgetState (opt_detaggable . ist_optimisation cn)

589589 if detag

590− then irSC vs (Case n [ConCase cn a ns sc])

590+ then irSC vs (Case up n [ConCase cn a ns sc])

591591 else LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

592592

593−irSC vs sc@(Case n alts) = do

593+irSC vs sc@(Case up n alts) = do

594594 -- check that neither alternative needs the newtype optimisation,

595595 -- see comment above

596596 goneWrong <- or <$> mapM isDetaggable alts

src/Idris/Core/CaseTree.hs+69−74

@@ -1,7 +1,7 @@

11{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

33module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo,

4− Phase(..), CaseTree,

4+ Phase(..), CaseTree, CaseType(..),

55 simpleCase, small, namesUsed, findCalls, findUsedArgs,

66 substSC, substAlt, mkForce) where

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

3030-- allows casing on arbitrary terms, here we choose to maintain the distinction

3131-- in order to allow for better optimisation opportunities.

3232--

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

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

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

3535 | STerm !t

3636 | UnmatchedCase String -- ^ error message

@@ -41,6 +41,9 @@ deriving instance Binary SC'

4141deriving instance NFData SC'

4242!-}

4343

44+data CaseType = Updatable | Shared

45+ deriving (Eq, Ord)

46+

4447type SC = SC' Term

4548

4649data CaseAlt' t = ConCase Name Int [Name] !(SC' t)

@@ -59,8 +62,11 @@ type CaseAlt = CaseAlt' Term

5962instance Show t => Show (SC' t) where

6063 show sc = show' 1 sc

6164 where

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

65+ show' i (Case up n alts) = "case" ++ u ++ show n ++ " of\n" ++ indent i ++

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

67+ where u = case up of

68+ Updatable -> "! "

69+ Shared -> " "

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

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

6672 show' i (STerm tm) = show tm

@@ -88,7 +94,7 @@ type Clause = ([Pat], (Term, Term))

8894type CS = ([Term], Int, [(Name, Type)])

8995

9096instance TermSize SC where

91− termsize n (Case n' as) = termsize n as

97+ termsize n (Case _ n' as) = termsize n as

9298 termsize n (ProjCase n' as) = termsize n as

9399 termsize n (STerm t) = termsize n t

94100 termsize n _ = 1

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

111117

112118namesUsed :: SC -> [Name]

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

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

120+ nu' ps (Case _ n alts) = nub (concatMap (nua ps) alts) \\ [n]

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

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

117123 nu' ps _ = []

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

136142

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

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

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

145+ nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

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

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

142148 nu' ps _ = []

@@ -189,7 +195,7 @@ findUsedArgs :: SC -> [Name] -> [Name]

189195findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

190196

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

192− nu' (Case n alts) = n : concatMap nua alts

198+ nu' (Case _ n alts) = n : concatMap nua alts

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

194200 nu' (STerm t) = directUse t

195201 nu' _ = []

@@ -204,7 +210,7 @@ findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where

204210isUsed :: SC -> Name -> Bool

205211isUsed sc n = used sc where

206212

207− used (Case n' alts) = n == n' || or (map usedA alts)

213+ used (Case _ n' alts) = n == n' || or (map usedA alts)

208214 used (ProjCase t alts) = n `elem` freeNames t || or (map usedA alts)

209215 used (STerm t) = n `elem` freeNames t

210216 used _ = False

@@ -276,7 +282,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

276282

277283 acc [] n = Error (Inaccessible n)

278284 acc (PV x t : xs) n | x == n = OK ()

279− acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

285+ acc (PCon _ _ _ ps : xs) n = acc (ps ++ xs) n

280286 acc (PSuc p : xs) n = acc (p : xs) n

281287 acc (_ : xs) n = acc xs n

282288

@@ -285,7 +291,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

285291-- going on).

286292

287293checkSameTypes :: [(Name, Type)] -> SC -> Bool

288−checkSameTypes tys (Case n alts)

294+checkSameTypes tys (Case _ n alts)

289295 = case lookup n tys of

290296 Just t -> and (map (checkAlts t) alts)

291297 _ -> and (map ((checkSameTypes tys).getSC) alts)

@@ -324,7 +330,7 @@ isConstType (B32V _) (AType (ATInt _)) = True

324330isConstType (B64V _) (AType (ATInt _)) = True

325331isConstType _ _ = False

326332

327−data Pat = PCon Name Int [Pat]

333+data Pat = PCon Bool Name Int [Pat]

328334 | PConst Const

329335 | PV Name Type

330336 | PSuc Pat -- special case for n+1 on Integer

@@ -344,34 +350,18 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

344350toPat :: Bool -> Bool -> [Term] -> [Pat]

345351toPat reflect tc = map $ toPat' []

346352 where

347− toPat' [_,_,arg](P (DCon t a _) nm@(UN n) _)

353+ toPat' [_,_,arg](P (DCon t a uniq) nm@(UN n) _)

348354 | n == txt "Delay"

349− = PCon nm t [PAny, PAny, toPat' [] arg]

355+ = PCon uniq nm t [PAny, PAny, toPat' [] arg]

350356

351− toPat' args (P (DCon t a _) n _)

352− = PCon n t $ map (toPat' []) args

357+ toPat' args (P (DCon t a uniq) n _)

358+ = PCon uniq n t $ map (toPat' []) args

353359

354360 -- n + 1

355361 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)

356362 | pabi == txt "prim__addBigInt"

357363 = PSuc $ toPat' [] p

358364

359− -- Typecase

360−-- toPat' (P (TCon t a) n _) args | tc

361−-- = do args' <- mapM (\x -> toPat' x []) args

362−-- return $ PCon n t args'

363−-- toPat' (Constant (AType (ATInt ITNative))) []

364−-- | tc = return $ PCon (UN "Int") 1 []

365−-- toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

366−-- toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

367−-- toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

368−-- toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

369−-- toPat' (Constant (AType (ATInt ITBig))) []

370−-- | tc = return $ PCon (UN "Integer") 6 []

371−-- toPat' (Constant (AType (ATInt (ITFixed n)))) []

372−-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

373−--

374−

375365 toPat' [] (P Bound n ty) = PV n ty

376366 toPat' args (App f a) = toPat' (a : args) f

377367 toPat' [] (Constant (AType _)) = PTyPat

@@ -405,7 +395,7 @@ isVarPat (PAny : ps , _) = True

405395isVarPat (PTyPat : ps , _) = True

406396isVarPat _ = False

407397

408−isConPat (PCon _ _ _ : ps, _) = True

398+isConPat (PCon _ _ _ _ : ps, _) = True

409399isConPat (PReflected _ _ : ps, _) = True

410400isConPat (PSuc _ : ps, _) = True

411401isConPat (PConst _ : ps, _) = True

@@ -449,18 +439,18 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

449439 noClash [] = True

450440 noClash (p : ps) = not (any (clashPat p) ps) && noClash ps

451441

452− clashPat (PCon _ _ _) (PConst _) = True

453− clashPat (PConst _) (PCon _ _ _) = True

454− clashPat (PCon _ _ _) (PSuc _) = True

455− clashPat (PSuc _) (PCon _ _ _) = True

456− clashPat (PCon n i _) (PCon n' i' _) | i == i' = n /= n'

442+ clashPat (PCon _ _ _ _) (PConst _) = True

443+ clashPat (PConst _) (PCon _ _ _ _) = True

444+ clashPat (PCon _ _ _ _) (PSuc _) = True

445+ clashPat (PSuc _) (PCon _ _ _ _) = True

446+ clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'

457447 clashPat _ _ = False

458448

459449 -- this compares (+isInaccessible, -numberOfCases)

460450 moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))

461451 (snd . fst . head $ ys, numNames [] (map snd xs))

462452

463− numNames xs (PCon n _ _ : ps)

453+ numNames xs (PCon _ n _ _ : ps)

464454 | not (Left n `elem` xs) = numNames (Left n : xs) ps

465455 numNames xs (PConst c : ps)

466456 | not (Right c `elem` xs) = numNames (Right c : xs) ps

@@ -497,7 +487,8 @@ data ConType = CName Name Int -- named constructor

497487 | CConst Const -- constant, not implemented yet

498488 deriving (Show, Eq)

499489

500−data Group = ConGroup ConType -- Constructor

490+data Group = ConGroup Bool -- Uniqueness flag

491+ ConType -- Constructor

501492 [([Pat], Clause)] -- arguments and rest of alternative

502493 deriving Show

503494

@@ -507,26 +498,30 @@ conRule (v:vs) cs err = do groups <- groupCons cs

507498

508499caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC

509500caseGroups (v:vs) gs err = do g <- altGroups gs

510− return $ Case v (sort g)

501+ return $ Case (getShared gs) v (sort g)

511502 where

503+ getShared (ConGroup True _ _ : _) = Updatable

504+ getShared _ = Shared

505+

512506 altGroups [] = return [DefaultCase err]

513507

514− altGroups (ConGroup (CName n i) args : cs)

508+ altGroups (ConGroup _ (CName n i) args : cs)

515509 = (:) <$> altGroup n i args <*> altGroups cs

516510

517− altGroups (ConGroup (CFn n) args : cs)

511+ altGroups (ConGroup _ (CFn n) args : cs)

518512 = (:) <$> altFnGroup n args <*> altGroups cs

519513

520− altGroups (ConGroup CSuc args : cs)

514+ altGroups (ConGroup _ CSuc args : cs)

521515 = (:) <$> altSucGroup args <*> altGroups cs

522516

523− altGroups (ConGroup (CConst c) args : cs)

517+ altGroups (ConGroup _ (CConst c) args : cs)

524518 = (:) <$> altConstGroup c args <*> altGroups cs

525519

526− altGroup n i args = do inacc <- inaccessibleArgs n

527− (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

528− matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

529− return $ ConCase n i newVars matchCs

520+ altGroup n i args

521+ = do inacc <- inaccessibleArgs n

522+ (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

523+ matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

524+ return $ ConCase n i newVars matchCs

530525

531526 altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args

532527 matchCs <- match (newVars ++ vs) nextCs err

@@ -601,21 +596,21 @@ groupCons cs = gc [] cs

601596 do acc' <- addGroup p ps res acc

602597 gc acc' cs

603598 addGroup p ps res acc = case p of

604− PCon con i args -> return $ addg (CName con i) args (ps, res) acc

599+ PCon uniq con i args -> return $ addg uniq (CName con i) args (ps, res) acc

605600 PConst cval -> return $ addConG cval (ps, res) acc

606− PSuc n -> return $ addg CSuc [n] (ps, res) acc

607− PReflected fn args -> return $ addg (CFn fn) args (ps, res) acc

601+ PSuc n -> return $ addg False CSuc [n] (ps, res) acc

602+ PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc

608603 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"

609604

610− addg c conargs res []

611− = [ConGroup c [(conargs, res)]]

612− addg c conargs res (g@(ConGroup c' cs):gs)

613− | c == c' = ConGroup c (cs ++ [(conargs, res)]) : gs

614− | otherwise = g : addg c conargs res gs

605+ addg uniq c conargs res []

606+ = [ConGroup uniq c [(conargs, res)]]

607+ addg uniq c conargs res (g@(ConGroup _ c' cs):gs)

608+ | c == c' = ConGroup uniq c (cs ++ [(conargs, res)]) : gs

609+ | otherwise = g : addg uniq c conargs res gs

615610

616− addConG con res [] = [ConGroup (CConst con) [([], res)]]

617− addConG con res (g@(ConGroup (CConst n) cs) : gs)

618− | con == n = ConGroup (CConst n) (cs ++ [([], res)]) : gs

611+ addConG con res [] = [ConGroup False (CConst con) [([], res)]]

612+ addConG con res (g@(ConGroup False (CConst n) cs) : gs)

613+ | con == n = ConGroup False (CConst n) (cs ++ [([], res)]) : gs

619614-- | otherwise = g : addConG con res gs

620615 addConG con res (g : gs) = g : addConG con res gs

621616

@@ -637,7 +632,7 @@ depatt :: [Name] -> SC -> SC

637632depatt ns tm = dp [] tm

638633 where

639634 dp ms (STerm tm) = STerm (applyMaps ms tm)

640− dp ms (Case x alts) = Case x (map (dpa ms x) alts)

635+ dp ms (Case up x alts) = Case up x (map (dpa ms x) alts)

641636 dp ms sc = sc

642637

643638 dpa ms x (ConCase n i args sc)

@@ -667,7 +662,7 @@ depatt ns tm = dp [] tm

667662-- FIXME: Do this for SucCase too

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

669664 -> SC -> SC

670−prune proj (Case n alts) = case alts' of

665+prune proj (Case up n alts) = case alts' of

671666 [] -> ImpossibleCase

672667

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

@@ -689,7 +684,7 @@ prune proj (Case n alts) = case alts' of

689684 as@[ConCase cn i args sc]

690685 | proj -> let sc' = prune proj sc in

691686 if any (isUsed sc') args

692− then Case n [ConCase cn i args sc']

687+ then Case up n [ConCase cn i args sc']

693688 else sc'

694689

695690 [SucCase cn sc]

@@ -702,9 +697,9 @@ prune proj (Case n alts) = case alts' of

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

703698 -- it gets caught first.

704699 [s@(SucCase _ _), DefaultCase dc]

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

700+ -> Case up n [ConstCase (BI 0) dc, s]

706701

707− as -> Case n as

702+ as -> Case up n as

708703 where

709704 alts' = filter (not . erased) $ map pruneAlt alts

710705

@@ -719,10 +714,10 @@ prune proj (Case n alts) = case alts' of

719714 erased _ = False

720715

721716 projRep :: Name -> Name -> Int -> SC -> SC

722− projRep arg n i (Case x alts) | x == arg

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

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

724− projRep arg n i (Case x alts)

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

719+ projRep arg n i (Case up x alts)

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

726721 projRep arg n i (ProjCase t alts)

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

728723 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

@@ -749,9 +744,9 @@ stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

749744stripLambdas x = x

750745

751746substSC :: Name -> Name -> SC -> SC

752−substSC n repl (Case n' alts)

753− | n == n' = Case repl (map (substAlt n repl) alts)

754− | otherwise = Case n' (map (substAlt n repl) alts)

747+substSC n repl (Case up n' alts)

748+ | n == n' = Case up repl (map (substAlt n repl) alts)

749+ | otherwise = Case up n' (map (substAlt n repl) alts)

755750substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t

756751substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

757752substSC n repl ImpossibleCase = ImpossibleCase

@@ -771,11 +766,11 @@ substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)

771766mkForce :: Name -> Name -> SC -> SC

772767mkForce = mkForceSC

773768 where

774− mkForceSC n arg (Case x alts) | x == arg

775− = Case n $ map (mkForceAlt n arg) alts

769+ mkForceSC n arg (Case up x alts) | x == arg

770+ = Case up n $ map (mkForceAlt n arg) alts

776771

777− mkForceSC n arg (Case x alts)

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

772+ mkForceSC n arg (Case up x alts)

773+ = Case up x (map (mkForceAlt n arg) alts)

779774

780775 mkForceSC n arg (ProjCase t alts)

781776 = ProjCase t $ map (mkForceAlt n arg) alts

src/Idris/Core/DeepSeq.hs+1−1

@@ -101,7 +101,7 @@ instance (NFData n) => NFData (TT n) where

101101 rnf (UType _) = ()

102102

103103instance (NFData t) => NFData (SC' t) where

104− rnf (Case x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

104+ rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

105105 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

106106 rnf (STerm x1) = rnf x1 `seq` ()

107107 rnf (UnmatchedCase x1) = rnf x1 `seq` ()

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

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

396396 evTree ntimes stk top env amap (ProjCase t alts)

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

398398 doCase ntimes stk top env amap t' alts

399− evTree ntimes stk top env amap (Case n alts)

399+ evTree ntimes stk top env amap (Case _ n alts)

400400 = case lookup n amap of

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

402402 _ -> return Nothing

@@ -589,7 +589,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

589589 ceq ps _ Erased = return True

590590 ceq ps x y = return False

591591

592− caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'

592+ caseeq ps (Case _ n cs) (Case _ n' cs') = caseeqA ((n,n'):ps) cs cs'

593593 where

594594 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')

595595 = do q1 <- caseeq (zip as as' ++ ps) sc sc'

src/Idris/Core/Execute.hs+1−1

@@ -434,7 +434,7 @@ execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVa

434434execCase' env ctxt amap (UnmatchedCase _) = return Nothing

435435execCase' env ctxt amap (STerm tm) =

436436 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

437−execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

437+execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =

438438 case chooseAlt tm alts of

439439 Just (newCase, newBindings) ->

440440 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

src/Idris/Erasure.hs+2−2

@@ -281,13 +281,13 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

281281

282282 -- for the purposes of erasure, we can disregard the projection

283283 getDepsSC fn es vs (ProjCase (Proj t i) alts) = getDepsSC fn es vs (ProjCase t alts) -- step

284− getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case n alts) -- base

284+ getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case Shared n alts) -- base

285285

286286 -- other ProjCase's are not supported

287287 getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)

288288

289289 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)

290− getDepsSC fn es vs (Case n alts)

290+ getDepsSC fn es vs (Case sh n alts)

291291 -- we case-split on this variable, which marks it as used

292292 -- (unless there is exactly one case branch)

293293 -- hence we add a new dependency, whose only precondition is

src/Idris/IBC.hs+19−6

@@ -183,8 +183,8 @@ ibc i (IBCDef n) f

183183 = do c' <- updateSC c; r' <- updateSC r

184184 return (CaseDefs (ts, t) (cs, c') (is, i) (rs, r'))

185185

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

187− return (Case n alts')

186+ updateSC (Case up n alts) = do alts' <- mapM updateAlt alts

187+ return (Case up n alts')

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

189189 alts' <- mapM updateAlt alts

190190 return (ProjCase t' alts')

@@ -631,12 +631,24 @@ instance Binary CGInfo where

631631 x4 <- get

632632 x5 <- get

633633 return (CGInfo x1 x2 [] x4 x5)

634+

635+instance Binary CaseType where

636+ put x = case x of

637+ Updatable -> putWord8 0

638+ Shared -> putWord8 1

639+ get = do i <- getWord8

640+ case i of

641+ 0 -> return Updatable

642+ 1 -> return Shared

643+ _ -> error "Corrupted binary data for CaseType"

644+

634645instance Binary SC where

635646 put x

636647 = case x of

637− Case x1 x2 -> do putWord8 0

638− put x1

639− put x2

648+ Case x1 x2 x3 -> do putWord8 0

649+ put x1

650+ put x2

651+ put x3

640652 ProjCase x1 x2 -> do putWord8 1

641653 put x1

642654 put x2

@@ -650,7 +662,8 @@ instance Binary SC where

650662 case i of

651663 0 -> do x1 <- get

652664 x2 <- get

653− return (Case x1 x2)

665+ x3 <- get

666+ return (Case x1 x2 x3)

654667 1 -> do x1 <- get

655668 x2 <- get

656669 return (ProjCase x1 x2)

src/Idris/Transforms.hs+2−2

@@ -25,10 +25,10 @@ instance Transform a => Transform (Binder a) where

2525

2626instance Transform SC where

2727 transform o@(CaseTrans t) sc = trans t sc where

28− trans t (Case n alts) = t (Case n (map (transform o) alts))

28+ trans t (Case up n alts) = t (Case up n (map (transform o) alts))

2929 trans t x = t x

3030 transform o@(TermTrans t) sc = trans t sc where

31− trans t (Case n alts) = Case n (map (transform o) alts)

31+ trans t (Case up n alts) = Case up n (map (transform o) alts)

3232 trans t (STerm tm) = STerm (t tm)

3333 trans t x = x

3434

src/Idris/WhoCalls.hs+2−2

@@ -36,13 +36,13 @@ namesBinder (NLet ty val) = names ty ++ names val

3636namesBinder b = names (binderTy b)

3737

3838occursSC :: Name -> SC -> Bool

39−occursSC n (Case _ alts) = any (occursCaseAlt n) alts

39+occursSC n (Case _ _ alts) = any (occursCaseAlt n) alts

4040occursSC n (ProjCase t alts) = occurs n t || any (occursCaseAlt n) alts

4141occursSC n (STerm t) = occurs n t

4242occursSC n _ = False

4343

4444namesSC :: SC -> [Name]

45−namesSC (Case _ alts) = concatMap namesCaseAlt alts

45+namesSC (Case _ _ alts) = concatMap namesCaseAlt alts

4646namesSC (ProjCase t alts) = names t ++ concatMap namesCaseAlt alts

4747namesSC (STerm t) = names t

4848namesSC _ = []