idris-1.3.2: Functional Programming Language with Dependent Types

LicenseBSD3
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
Show CaseDef Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

showsPrec :: Int -> CaseDef -> ShowS

show :: CaseDef -> String

showList :: [CaseDef] -> ShowS

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 # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

Binary SC 
Instance details

Defined in Idris.IBC

Methods

put :: SC -> Put

get :: Get SC

putList :: [SC] -> Put

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

Defined in Idris.Core.CaseTree

Methods

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

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

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

Defined in Idris.Core.CaseTree

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 # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

show :: SC' t -> String

showList :: [SC' t] -> ShowS

Generic (SC' t) Source # 
Instance details

Defined in Idris.Core.CaseTree

Associated Types

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

Methods

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

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

NFData t => NFData (SC' t) 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: SC' t -> ()

ToJSON t => ToJSON (SC' t) 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: SC' t -> Value

toEncoding :: SC' t -> Encoding

toJSONList :: [SC' t] -> Value

toEncodingList :: [SC' t] -> Encoding

type Rep (SC' t) Source # 
Instance details

Defined in Idris.Core.CaseTree

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

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 # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

Binary CaseAlt 
Instance details

Defined in Idris.IBC

Methods

put :: CaseAlt -> Put

get :: Get CaseAlt

putList :: [CaseAlt] -> Put

TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

Defined in Idris.Core.CaseTree

Methods

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

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

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

Defined in Idris.Core.CaseTree

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 # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

show :: CaseAlt' t -> String

showList :: [CaseAlt' t] -> ShowS

Generic (CaseAlt' t) Source # 
Instance details

Defined in Idris.Core.CaseTree

Associated Types

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

Methods

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

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

NFData t => NFData (CaseAlt' t) 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: CaseAlt' t -> ()

ToJSON t => ToJSON (CaseAlt' t) 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: CaseAlt' t -> Value

toEncoding :: CaseAlt' t -> Encoding

toJSONList :: [CaseAlt' t] -> Value

toEncodingList :: [CaseAlt' t] -> Encoding

type Rep (CaseAlt' t) Source # 
Instance details

Defined in Idris.Core.CaseTree

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

type ErasureInfo = Name -> [Int] Source #

data Phase Source #

Constructors

CoverageCheck [Int] 
CompileTime 
RunTime 
Instances
Eq Phase Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

Show Phase Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

showsPrec :: Int -> Phase -> ShowS

show :: Phase -> String

showList :: [Phase] -> ShowS

data CaseType Source #

Constructors

Updatable 
Shared 
Instances
Eq CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

Data CaseType 
Instance details

Defined in IRTS.JavaScript.LangTransforms

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CaseType -> c CaseType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CaseType

toConstr :: CaseType -> Constr

dataTypeOf :: CaseType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CaseType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType)

gmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CaseType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CaseType -> r

gmapQ :: (forall d. Data d => d -> u) -> CaseType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType

Ord CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

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 Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

showsPrec :: Int -> CaseType -> ShowS

show :: CaseType -> String

showList :: [CaseType] -> ShowS

Generic CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

Associated Types

type Rep CaseType :: Type -> Type

Methods

from :: CaseType -> Rep CaseType x

to :: Rep CaseType x -> CaseType

Binary CaseType 
Instance details

Defined in Idris.IBC

Methods

put :: CaseType -> Put

get :: Get CaseType

putList :: [CaseType] -> Put

NFData CaseType 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: CaseType -> ()

ToJSON CaseType 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: CaseType -> Value

toEncoding :: CaseType -> Encoding

toJSONList :: [CaseType] -> Value

toEncodingList :: [CaseType] -> Encoding

type Rep CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

type Rep CaseType = D1 (MetaData "CaseType" "Idris.Core.CaseTree" "idris-1.3.2-J2hjWptWQ7ZDydvTOeZFZI" False) (C1 (MetaCons "Updatable" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Shared" PrefixI False) (U1 :: Type -> Type))

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 #