idris-0.9.11: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Core.CaseTree

Documentation

data CaseDef Source

Constructors

CaseDef [Name] !SC [Term] 

Instances

data SC' t Source

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) 

data CaseAlt' t Source

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) 

data Phase Source

Constructors

CompileTime 
RunTime 

Instances

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

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

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