826fa9c · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs−16

compare with master

unifiedsplit

@@ -446,22 +446,6 @@ instance ToIR SC where

446 subexpr (LConstCase _ e) = e

447 subexpr (LDefaultCase e) = e

448

449− substSC :: Name -> Name -> SC -> SC

450− substSC n repl (Case n' alts)

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

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

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

454− substSC n repl sc = error $ "unsupported in substSC: " ++ show sc

455−

456− substAlt :: Name -> Name -> CaseAlt -> CaseAlt

457− substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)

458− substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)

459− substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)

460− substAlt n repl (SucCase n' sc)

461− | n == n' = SucCase n (substSC n repl sc)

462− | otherwise = SucCase n' (substSC n repl sc)

463− substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)

464−

465 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts

449 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts

466 return $ LCase (LV (Glob n)) alts'

450 return $ LCase (LV (Glob n)) alts'

467 ir' ImpossibleCase = return LNothing

451 ir' ImpossibleCase = return LNothing

src/Idris/Core/CaseTree.hs+17−3

@@ -2,7 +2,8 @@

2

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

4 Phase(..), CaseTree,

5− simpleCase, small, namesUsed, findCalls, findUsedArgs) where

5+ simpleCase, small, namesUsed, findCalls, findUsedArgs,

6+ substSC, substAlt) where

6

7

7import Idris.Core.TT

8import Idris.Core.TT

8

9

@@ -683,5 +684,18 @@ stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

683stripLambdas x = x

684stripLambdas x = x

684

685

686

686−

687+substSC :: Name -> Name -> SC -> SC

687−

688+substSC n repl (Case n' alts)

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

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

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

692+substSC n repl sc = error $ "unsupported in substSC: " ++ show sc

693+

694+substAlt :: Name -> Name -> CaseAlt -> CaseAlt

695+substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)

696+substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)

697+substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)

698+substAlt n repl (SucCase n' sc)

699+ | n == n' = SucCase n (substSC n repl sc)

700+ | otherwise = SucCase n' (substSC n repl sc)

701+substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)

src/Idris/Erasure.hs+9−1

@@ -31,7 +31,7 @@ import qualified Data.Text as T

31-- UseMap maps names to the set of used (reachable) argument positions.

32type UseMap = Map Name (IntMap (Set Reason))

33

34−data Arg = Arg !Int | Result deriving (Eq, Ord)

34+data Arg = Arg Int | Result deriving (Eq, Ord)

35

36instance Show Arg where

37 show (Arg i) = show i

@@ -274,6 +274,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

274 getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc

275 getDepsAlt fn es vs var (SucCase n sc)

276 = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased

277+

278+ -- instance constructors

279+ getDepsAlt fn es vs var (ConCase ctn@(SN (InstanceCtorN cln)) cnt ns sc) = getDepsSC fn es vs (renameIn sc)

280+ where

281+ renameIn = foldr ((.) . rename) id $ zip [0..] ns

282+ rename (i, n) = substSC n (SN (WhereN i ctn n))

283+

284+ -- data constructors

277 getDepsAlt fn es vs var (ConCase n cnt ns sc)

285 getDepsAlt fn es vs var (ConCase n cnt ns sc)

278 = getDepsSC fn es (vs' `union` vs) sc -- left-biased union

286 = getDepsSC fn es (vs' `union` vs) sc -- left-biased union

279 where

287 where