idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Core.CaseTree

Documentation

data CaseDef Source

Constructors

CaseDef [Name] !SC [Term] 

Instances

type SC = SC' Term Source

data SC' t Source

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 Source

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) 

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] Source

data Phase Source

Constructors

CompileTime 
RunTime 

Instances

type CaseTree = SC Source

data CaseType Source

Constructors

Updatable 
Shared 

Instances

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

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

namesUsed :: SC -> [Name] Source

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

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

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

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

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