idris-1.3.1: 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

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) :: * -> * #

Methods

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

to :: Rep (SC' t) x -> 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 #

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

Defined in Idris.Core.DeepSeq

Methods

rnf :: SC' t -> () #

type Rep (SC' t) Source # 
Instance details

Defined in Idris.Core.CaseTree

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) :: * -> * #

Methods

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

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

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

Defined in IRTS.Portable

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

Defined in Idris.Core.DeepSeq

Methods

rnf :: 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.1-HMhXn3ahTlmAYa6dTdYaVB" 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))))))

data Phase Source #

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

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

Show CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

Generic CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

Associated Types

type Rep CaseType :: * -> * #

Methods

from :: CaseType -> Rep CaseType x #

to :: Rep CaseType x -> CaseType #

ToJSON CaseType # 
Instance details

Defined in IRTS.Portable

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

type Rep CaseType Source # 
Instance details

Defined in Idris.Core.CaseTree

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