Idris.Core.CaseTree

Note: The case-tree elaborator only produces (Case n alts)-cases; in other words, it never inspects anything else than variables.

ProjCase is a special powerful case construct that allows inspection of compound terms. Occurrences of ProjCase arise no earlier than in the function prune as a means of optimisation of already built case trees.

While the intermediate representation (follows in the pipeline, named LExp) allows casing on arbitrary terms, here we choose to maintain the distinction in order to allow for better optimisation opportunities.

Documentation

data CaseDef

Constructors

CaseDef [Name] !SC [Term]

Instances

Show CaseDef

Methods

showsPrec :: Int -> CaseDef -> ShowS

show :: CaseDef -> String

showList :: [CaseDef] -> ShowS

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'

Methods

fmap :: (a -> b) -> SC' a -> SC' b

(<$) :: a -> SC' b -> SC' a

TermSize SC

Methods

termsize :: Name -> SC -> Int

Eq t => Eq (SC' t)

Methods

(==) :: SC' t -> SC' t -> Bool

(/=) :: SC' t -> SC' t -> Bool

Ord t => Ord (SC' t)

Methods

compare :: SC' t -> SC' t -> Ordering

(<) :: SC' t -> SC' t -> Bool

(<=) :: SC' t -> SC' t -> Bool

(>) :: SC' t -> SC' t -> Bool

(>=) :: SC' t -> SC' t -> Bool

max :: SC' t -> SC' t -> SC' t

min :: SC' t -> SC' t -> SC' t

Show t => Show (SC' t)

Methods

showsPrec :: Int -> SC' t -> ShowS

show :: SC' t -> String

showList :: [SC' t] -> ShowS

Generic (SC' t)

Associated Types

type Rep (SC' t) :: * -> *

Methods

from :: SC' t -> Rep (SC' t) x

to :: Rep (SC' t) x -> SC' t

type Rep (SC' t)

type Rep (SC' t) = D1 * (MetaData "SC'" "Idris.Core.CaseTree" "idris-1.2.0-FcdjfAXrqrBWjK6eYRvw3" False) ((:+:) * ((:+:) * (C1 * (MetaCons "Case" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * CaseType)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [CaseAlt' t]))))) (C1 * (MetaCons "ProjCase" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * t)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [CaseAlt' t]))))) ((:+:) * (C1 * (MetaCons "STerm" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * t))) ((:+:) * (C1 * (MetaCons "UnmatchedCase" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * String))) (C1 * (MetaCons "ImpossibleCase" PrefixI False) (U1 *)))))

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'

Methods

fmap :: (a -> b) -> CaseAlt' a -> CaseAlt' b

(<$) :: a -> CaseAlt' b -> CaseAlt' a

TermSize CaseAlt

Methods

termsize :: Name -> CaseAlt -> Int

Eq t => Eq (CaseAlt' t)

Methods

(==) :: CaseAlt' t -> CaseAlt' t -> Bool

(/=) :: CaseAlt' t -> CaseAlt' t -> Bool

Ord t => Ord (CaseAlt' t)

Methods

compare :: CaseAlt' t -> CaseAlt' t -> Ordering

(<) :: CaseAlt' t -> CaseAlt' t -> Bool

(<=) :: CaseAlt' t -> CaseAlt' t -> Bool

(>) :: CaseAlt' t -> CaseAlt' t -> Bool

(>=) :: CaseAlt' t -> CaseAlt' t -> Bool

max :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t

min :: CaseAlt' t -> CaseAlt' t -> CaseAlt' t

Show t => Show (CaseAlt' t)

Methods

showsPrec :: Int -> CaseAlt' t -> ShowS

show :: CaseAlt' t -> String

showList :: [CaseAlt' t] -> ShowS

Generic (CaseAlt' t)

Associated Types

type Rep (CaseAlt' t) :: * -> *

Methods

from :: CaseAlt' t -> Rep (CaseAlt' t) x

to :: Rep (CaseAlt' t) x -> CaseAlt' t

type Rep (CaseAlt' t)

type Rep (CaseAlt' t) = D1 * (MetaData "CaseAlt'" "Idris.Core.CaseTree" "idris-1.2.0-FcdjfAXrqrBWjK6eYRvw3" False) ((:+:) * ((:+:) * (C1 * (MetaCons "ConCase" PrefixI False) ((:*:) * ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int))) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (SC' t)))))) (C1 * (MetaCons "FnCase" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [Name])) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (SC' t))))))) ((:+:) * (C1 * (MetaCons "ConstCase" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Const)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (SC' t))))) ((:+:) * (C1 * (MetaCons "SucCase" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (SC' t))))) (C1 * (MetaCons "DefaultCase" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * (SC' t)))))))

type ErasureInfo = Name -> [Int]

data Phase

Constructors

CoverageCheck [Int]

CompileTime

RunTime

Instances

Eq Phase

Methods

(==) :: Phase -> Phase -> Bool

(/=) :: Phase -> Phase -> Bool

Show Phase

Methods

showsPrec :: Int -> Phase -> ShowS

show :: Phase -> String

showList :: [Phase] -> ShowS

type CaseTree = SC

data CaseType

Constructors

Updatable

Shared

Instances

Eq CaseType

Methods

(==) :: CaseType -> CaseType -> Bool

(/=) :: CaseType -> CaseType -> Bool

Ord CaseType

Methods

compare :: CaseType -> CaseType -> Ordering

(<) :: CaseType -> CaseType -> Bool

(<=) :: CaseType -> CaseType -> Bool

(>) :: CaseType -> CaseType -> Bool

(>=) :: CaseType -> CaseType -> Bool

max :: CaseType -> CaseType -> CaseType

min :: CaseType -> CaseType -> CaseType

Show CaseType

Methods

showsPrec :: Int -> CaseType -> ShowS

show :: CaseType -> String

showList :: [CaseType] -> ShowS

Generic CaseType

Associated Types

type Rep CaseType :: * -> *

Methods

from :: CaseType -> Rep CaseType x

to :: Rep CaseType x -> CaseType

type Rep CaseType

type Rep CaseType = D1 * (MetaData "CaseType" "Idris.Core.CaseTree" "idris-1.2.0-FcdjfAXrqrBWjK6eYRvw3" False) ((:+:) * (C1 * (MetaCons "Updatable" PrefixI False) (U1 *)) (C1 * (MetaCons "Shared" PrefixI False) (U1 *)))

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

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

namesUsed :: SC -> [Name]

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

Return all called functions, and which arguments are used in each argument position for the call, in order to help reduce compilation time, and trace all unused arguments

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

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

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

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

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