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

git.iko.soy/Idris-dev

on master help sign in

Mark 'case' on unique types as updatable

218c735Edwin Brady12 years ago

src/IRTS/Compiler.hs+5−5

compare with master

unifiedsplit

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

513 return $ LCase tm' alts'

514

515-- 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])

517 | delay == txt "Delay"

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

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

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

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

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

542--

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

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

544 replacement <- case alt of

545 ConCase cn a ns sc -> do

546 detag <- fgetState (opt_detaggable . ist_optimisation cn)

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

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

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

586--

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

588 detag <- fgetState (opt_detaggable . ist_optimisation cn)

589 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])

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

592

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

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

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

595 -- see comment above

596 goneWrong <- or <$> mapM isDetaggable alts

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

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

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

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

4− Phase(..), CaseTree,

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

5 simpleCase, small, namesUsed, findCalls, findUsedArgs,

6 substSC, substAlt, mkForce) where

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

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

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

32--

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

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

35 | STerm !t

36 | UnmatchedCase String -- ^ error message

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

41deriving instance NFData SC'

42!-}

44+data CaseType = Updatable | Shared

45+ deriving (Eq, Ord)

46+

44type SC = SC' Term

47type SC = SC' Term

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

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

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

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

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

60 show sc = show' 1 sc

63 show sc = show' 1 sc

61 where

64 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 ++

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

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

67+ where u = case up of

68+ Updatable -> "! "

69+ Shared -> " "

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

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

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

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

66 show' i (STerm tm) = show tm

72 show' i (STerm tm) = show tm

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

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

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

90instance TermSize SC where

96instance TermSize SC where

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

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

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

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

93 termsize n (STerm t) = termsize n t

99 termsize n (STerm t) = termsize n t

94 termsize n _ = 1

100 termsize n _ = 1

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

111

117

112namesUsed :: SC -> [Name]

118namesUsed :: SC -> [Name]

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

119namesUsed 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]

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

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

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

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

117 nu' ps _ = []

123 nu' ps _ = []

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

136

142

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

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

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

144findCalls 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)

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

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

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

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

142 nu' ps _ = []

148 nu' ps _ = []

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

189findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

195findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

190

196

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

197findAllUsedArgs 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

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

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

194 nu' (STerm t) = directUse t

200 nu' (STerm t) = directUse t

195 nu' _ = []

201 nu' _ = []

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

204isUsed :: SC -> Name -> Bool

210isUsed :: SC -> Name -> Bool

205isUsed sc n = used sc where

211isUsed sc n = used sc where

206

212

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

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

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

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

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

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

210 used _ = False

216 used _ = False

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

276

282

277 acc [] n = Error (Inaccessible n)

283 acc [] n = Error (Inaccessible n)

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

284 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

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

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

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

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

282

288

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

285-- going on).

291-- going on).

286

292

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

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

288−checkSameTypes tys (Case n alts)

294+checkSameTypes tys (Case _ n alts)

289 = case lookup n tys of

295 = case lookup n tys of

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

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

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

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

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

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

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

325isConstType _ _ = False

331isConstType _ _ = False

326

332

327−data Pat = PCon Name Int [Pat]

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

328 | PConst Const

334 | PConst Const

329 | PV Name Type

335 | PV Name Type

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

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

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

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

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

345toPat reflect tc = map $ toPat' []

351toPat reflect tc = map $ toPat' []

346 where

352 where

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

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

348 | n == txt "Delay"

354 | n == txt "Delay"

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

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

350

356

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

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

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

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

353

359

354 -- n + 1

360 -- n + 1

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

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

356 | pabi == txt "prim__addBigInt"

362 | pabi == txt "prim__addBigInt"

357 = PSuc $ toPat' [] p

363 = PSuc $ toPat' [] p

358

364

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−

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

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

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

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

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

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

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

405isVarPat (PTyPat : ps , _) = True

395isVarPat (PTyPat : ps , _) = True

406isVarPat _ = False

396isVarPat _ = False

407

397

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

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

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

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

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

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

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

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

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

449 noClash [] = True

439 noClash [] = True

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

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

451

441

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

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

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

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

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

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

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

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

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

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

457 clashPat _ _ = False

447 clashPat _ _ = False

458

448

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

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

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

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

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

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

462

452

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

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

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

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

465 numNames xs (PConst c : ps)

455 numNames xs (PConst c : ps)

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

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

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

497 | CConst Const -- constant, not implemented yet

487 | CConst Const -- constant, not implemented yet

498 deriving (Show, Eq)

488 deriving (Show, Eq)

499

489

490+data Group = ConGroup Bool -- Uniqueness flag

500−data Group = ConGroup ConType -- Constructor

491+ ConType -- Constructor

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

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

502 deriving Show

493 deriving Show

503

494

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

507

498

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

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

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

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

510− return $ Case v (sort g)

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

511 where

502 where

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

504+ getShared _ = Shared

505+

512 altGroups [] = return [DefaultCase err]

506 altGroups [] = return [DefaultCase err]

513

507

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

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

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

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

516

510

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

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

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

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

519

513

520− altGroups (ConGroup CSuc args : cs)

514+ altGroups (ConGroup _ CSuc args : cs)

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

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

522

516

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

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

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

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

525

519

520+ altGroup n i args

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

521+ = do inacc <- inaccessibleArgs n

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

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

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

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

529− return $ ConCase n i newVars matchCs

524+ return $ ConCase n i newVars matchCs

530

525

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

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

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

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

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

601 do acc' <- addGroup p ps res acc

596 do acc' <- addGroup p ps res acc

602 gc acc' cs

597 gc acc' cs

603 addGroup p ps res acc = case p of

598 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

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

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

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

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

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

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

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

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

609

604

610− addg c conargs res []

605+ addg uniq c conargs res []

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

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

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

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

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

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

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

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

615

610

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

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

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

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

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

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

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

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

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

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

621

616

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

637depatt ns tm = dp [] tm

632depatt ns tm = dp [] tm

638 where

633 where

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

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

641 dp ms sc = sc

636 dp ms sc = sc

642

637

643 dpa ms x (ConCase n i args sc)

638 dpa ms x (ConCase n i args sc)

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

667-- FIXME: Do this for SucCase too

662-- FIXME: Do this for SucCase too

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

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

669 -> SC -> SC

664 -> SC -> SC

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

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

671 [] -> ImpossibleCase

666 [] -> ImpossibleCase

672

667

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

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

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

689 as@[ConCase cn i args sc]

684 as@[ConCase cn i args sc]

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

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

691 if any (isUsed sc') args

686 if any (isUsed sc') args

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

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

693 else sc'

688 else sc'

694

689

695 [SucCase cn sc]

690 [SucCase cn sc]

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

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

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

703 -- it gets caught first.

698 -- it gets caught first.

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

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

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

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

706

701

707− as -> Case n as

702+ as -> Case up n as

708 where

703 where

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

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

710

705

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

719 erased _ = False

714 erased _ = False

720

715

721 projRep :: Name -> Name -> Int -> SC -> SC

716 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

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

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

724− projRep arg n i (Case x alts)

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

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

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

726 projRep arg n i (ProjCase t alts)

721 projRep arg n i (ProjCase t alts)

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

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

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

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

749stripLambdas x = x

744stripLambdas x = x

750

745

751substSC :: Name -> Name -> SC -> SC

746substSC :: Name -> Name -> SC -> SC

752−substSC n repl (Case n' alts)

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

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

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

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

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

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

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

756substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

751substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

757substSC n repl ImpossibleCase = ImpossibleCase

752substSC n repl ImpossibleCase = ImpossibleCase

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

771mkForce :: Name -> Name -> SC -> SC

766mkForce :: Name -> Name -> SC -> SC

772mkForce = mkForceSC

767mkForce = mkForceSC

773 where

768 where

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

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

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

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

776

771

777− mkForceSC n arg (Case x alts)

772+ mkForceSC n arg (Case up x alts)

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

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

779

774

780 mkForceSC n arg (ProjCase t alts)

775 mkForceSC n arg (ProjCase t alts)

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

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

101 rnf (UType _) = ()

102

103instance (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` ()

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

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

107 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

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

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

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

400 = case lookup n amap of

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

402 _ -> return Nothing

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

589 ceq ps _ Erased = return True

590 ceq ps x y = return False

591

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'

593 where

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

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

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

435execCase' env ctxt amap (STerm tm) =

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

438 case chooseAlt tm alts of

439 Just (newCase, newBindings) ->

440 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]

281

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

283 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

285

286 -- other ProjCase's are not supported

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

288

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

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

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

293 -- 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

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

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

185

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

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

187− return (Case n alts')

187+ return (Case up n alts')

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

189 alts' <- mapM updateAlt alts

190 return (ProjCase t' alts')

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

631 x4 <- get

632 x5 <- get

633 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+

634instance Binary SC where

645instance Binary SC where

635 put x

646 put x

636 = case x of

647 = case x of

637− Case x1 x2 -> do putWord8 0

648+ Case x1 x2 x3 -> do putWord8 0

638− put x1

649+ put x1

639− put x2

650+ put x2

651+ put x3

640 ProjCase x1 x2 -> do putWord8 1

652 ProjCase x1 x2 -> do putWord8 1

641 put x1

653 put x1

642 put x2

654 put x2

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

650 case i of

662 case i of

651 0 -> do x1 <- get

663 0 -> do x1 <- get

652 x2 <- get

664 x2 <- get

665+ x3 <- get

653− return (Case x1 x2)

666+ return (Case x1 x2 x3)

654 1 -> do x1 <- get

667 1 -> do x1 <- get

655 x2 <- get

668 x2 <- get

656 return (ProjCase x1 x2)

669 return (ProjCase x1 x2)

src/Idris/Transforms.hs+2−2

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

26instance Transform SC where

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

29 trans t x = t x

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

32 trans t (STerm tm) = STerm (t tm)

33 trans t x = x

src/Idris/WhoCalls.hs+2−2

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

36namesBinder b = names (binderTy b)

38occursSC :: Name -> SC -> Bool

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

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

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

41occursSC n (STerm t) = occurs n t

42occursSC n _ = False

44namesSC :: SC -> [Name]

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

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

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

47namesSC (STerm t) = names t

48namesSC _ = []