idris-1.1.0: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Core.CaseTree

Description

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.

Synopsis

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' Source # 

Methods

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

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

TermSize SC Source # 

Methods

termsize :: Name -> SC -> Int Source #

Eq t => Eq (SC' t) Source # 

Methods

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

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

Ord t => Ord (SC' t) Source # 

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) Source # 

Methods

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

show :: SC' t -> String #

showList :: [SC' t] -> ShowS #

Generic (SC' t) Source # 

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) 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' Source # 

Methods

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

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

TermSize CaseAlt Source # 

Methods

termsize :: Name -> CaseAlt -> Int Source #

Eq t => Eq (CaseAlt' t) Source # 

Methods

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

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

Ord t => Ord (CaseAlt' t) Source # 

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) Source # 

Methods

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

show :: CaseAlt' t -> String #

showList :: [CaseAlt' t] -> ShowS #

Generic (CaseAlt' t) Source # 

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) Source # 
type Rep (CaseAlt' t) = D1 (MetaData "CaseAlt'" "Idris.Core.CaseTree" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" 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)))))))

data Phase Source #

Instances

Eq Phase Source # 

Methods

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

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

Show Phase Source # 

Methods

showsPrec :: Int -> Phase -> ShowS #

show :: Phase -> String #

showList :: [Phase] -> ShowS #

data CaseType Source #

Constructors

Updatable 
Shared 

Instances

Eq CaseType Source # 
Ord CaseType Source # 
Show CaseType Source # 
Generic CaseType Source # 

Associated Types

type Rep CaseType :: * -> * #

Methods

from :: CaseType -> Rep CaseType x #

to :: Rep CaseType x -> CaseType #

type Rep CaseType Source # 
type Rep CaseType = D1 (MetaData "CaseType" "Idris.Core.CaseTree" "idris-1.1.0-K6A3QFl6ipd3Ns1JdzUkhF" 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 Source #

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

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

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

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

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