Idris.Core.CaseTree

Documentation

data CaseDef

Constructors

CaseDef [Name] !SC [Term]

Instances

Show CaseDef

type SC = SC' Term

data SC' t

Constructors

Case CaseType Name [CaseAlt' t]

invariant: lowest tags first

ProjCase t [CaseAlt' t]

special case for projections/thunk-forcing before inspection

STerm !t

UnmatchedCase String

error message

ImpossibleCase

already checked to be impossible

Instances

Functor SC'

Binary SC

TermSize SC

Eq t => Eq (SC' t)

Ord t => Ord (SC' t)

Show t => Show (SC' t)

NFData t => NFData (SC' t)

type CaseAlt = CaseAlt' Term

data CaseAlt' t

Constructors

ConCase Name Int [Name] !(SC' t)

FnCase Name [Name] !(SC' t)

reflection function

ConstCase Const !(SC' t)

SucCase Name !(SC' t)

DefaultCase !(SC' t)

Instances

Functor CaseAlt'

Binary CaseAlt

TermSize CaseAlt

Eq t => Eq (CaseAlt' t)

Ord t => Ord (CaseAlt' t)

Show t => Show (CaseAlt' t)

NFData t => NFData (CaseAlt' t)

type ErasureInfo = Name -> [Int]

data Phase

Constructors

CompileTime

RunTime

Instances

Eq Phase

Show Phase

type CaseTree = SC

data CaseType

Constructors

Updatable

Shared

Instances

Eq CaseType

Ord CaseType

Show CaseType

Binary CaseType

simpleCase :: Bool -> SC -> Bool -> Phase -> FC -> [Int] -> [Type] -> [([Name], Term, Term)] -> ErasureInfo -> TC CaseDef

small :: Name -> [Name] -> SC -> Bool

namesUsed :: SC -> [Name]

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

findUsedArgs :: SC -> [Name] -> [Name]

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

substAlt :: Name -> Name -> CaseAlt -> CaseAlt

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