idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Core.CaseTree

Description

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

Instances details
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

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

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

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

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

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

Defined in Idris.Core.DeepSeq

Methods

rnf :: SC' t -> ()

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

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.4-3WzTclJnDGuF9nqMis99Gw" '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

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

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

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

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

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

Defined in Idris.Core.DeepSeq

Methods

rnf :: CaseAlt' t -> ()

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

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.4-3WzTclJnDGuF9nqMis99Gw" '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

Instances details
Show Phase Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

showsPrec :: Int -> Phase -> ShowS

show :: Phase -> String

showList :: [Phase] -> ShowS

Eq Phase Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

data CaseType Source #

Constructors

Updatable 
Shared 

Instances

Instances details
ToJSON CaseType 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: CaseType -> Value

toEncoding :: CaseType -> Encoding

toJSONList :: [CaseType] -> Value

toEncodingList :: [CaseType] -> Encoding

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 :: forall r r'. (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

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

Show CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

showsPrec :: Int -> CaseType -> ShowS

show :: CaseType -> String

showList :: [CaseType] -> ShowS

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 -> ()

Eq CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

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

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

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

type Rep CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

type Rep CaseType = D1 ('MetaData "CaseType" "Idris.Core.CaseTree" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" '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 #