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

git.iko.soy/Idris-dev

Replace projections from instance ctors with special names.

commit826fa9c8bfccce943caa058c33d2c60aa5305c87 authorMatus Tejiscak <ziman@functor.sk> dateFri 28 Feb 2014, 15:57 (13 years ago) parent0916929

3 files changed+26−20

compare with master

unifiedsplit

src/IRTS/Compiler.hs−16 src/Idris/Core/CaseTree.hs+17−3 src/Idris/Erasure.hs+9−1

src/IRTS/Compiler.hs−16

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

446446 subexpr (LConstCase _ e) = e

447447 subexpr (LDefaultCase e) = e

448448

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−

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

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

467451 ir' ImpossibleCase = return LNothing

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

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

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

44 Phase(..), CaseTree,

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

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

6+ substSC, substAlt) where

78import Idris.Core.TT

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

683684stripLambdas x = x

684685

685686

686−

687−

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

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

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

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

3333

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

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

3535

3636instance Show Arg where

3737 show (Arg i) = show i

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

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

275275 getDepsAlt fn es vs var (SucCase n sc)

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

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

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

279287 where