Idris.Core.CaseTree

Documentation

data CaseDef

Constructors

CaseDef [Name] !SC [Term]

Instances

Show CaseDef

type SC = SC' Term

data SC' t

Constructors

Case Name [CaseAlt' t]

invariant: lowest tags first

ProjCase t [CaseAlt' t]

special case for projections

STerm !t

UnmatchedCase String

error message

ImpossibleCase

already checked to be impossible

Instances

Functor SC'

Binary SC

TermSize SC

ToIR SC

Transform SC

Eq t => Eq (SC' t)

Ord t => Ord (SC' t)

Show t => Show (SC' t)

NFData t => NFData (SC' t)

ToIR ([Name], SC)

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

Transform CaseAlt

Eq t => Eq (CaseAlt' t)

Ord t => Ord (CaseAlt' t)

Show t => Show (CaseAlt' t)

NFData t => NFData (CaseAlt' t)

data Phase

Constructors

CompileTime

RunTime

Instances

Eq Phase

Show Phase

type CaseTree = SC

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

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

namesUsed :: SC -> [Name]

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

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