License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

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

data CaseDef = CaseDef [Name] !SC [Term]
type SC = SC' Term
data SC' t
- = Case CaseType Name [CaseAlt' t]
- | ProjCase t [CaseAlt' t]
- | STerm !t
- | UnmatchedCase String
- | ImpossibleCase
type CaseAlt = CaseAlt' Term
data CaseAlt' t
- = ConCase Name Int [Name] !(SC' t)
- | FnCase Name [Name] !(SC' t)
- | ConstCase Const !(SC' t)
- | SucCase Name !(SC' t)
- | DefaultCase !(SC' t)
type ErasureInfo = Name -> [Int]
data Phase
- = CoverageCheck [Int]
- | CompileTime
- | RunTime
type CaseTree = SC
data CaseType
- = Updatable
- | Shared
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]])]
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

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 Source #
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 #
ToJSON t => ToJSON (SC' t) Source #
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) Source #
Instance details Defined in Idris.Core.DeepSeq Methods rnf :: 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.2-3LpOXLFJmzJ3DT7fAtaO1v" 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))))

type CaseAlt = CaseAlt' Term 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 #
Instance details Defined in Idris.Core.CaseTree Methods fmap :: (a -> b) -> CaseAlt' a -> CaseAlt' b # (<$) :: a -> CaseAlt' b -> CaseAlt' a #
Binary CaseAlt Source #
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 #
ToJSON t => ToJSON (CaseAlt' t) Source #
Instance details Defined in IRTS.Portable Methods toJSON :: CaseAlt' t -> Value # toEncoding :: CaseAlt' t -> Encoding # toJSONList :: [CaseAlt' t] -> Value # toEncodingList :: [CaseAlt' t] -> Encoding #
NFData t => NFData (CaseAlt' t) Source #
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.2-3LpOXLFJmzJ3DT7fAtaO1v" 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 #

type CaseTree = SC Source #

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 Source #
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 #
ToJSON CaseType Source #
Instance details Defined in IRTS.Portable Methods toJSON :: CaseType -> Value # toEncoding :: CaseType -> Encoding # toJSONList :: [CaseType] -> Value # toEncodingList :: [CaseType] -> Encoding #
Binary CaseType Source #
Instance details Defined in Idris.IBC Methods put :: CaseType -> Put # get :: Get CaseType # putList :: [CaseType] -> Put #
NFData CaseType Source #
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.2-3LpOXLFJmzJ3DT7fAtaO1v" 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 #

namesUsed :: SC -> [Name] 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 #

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

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

substAlt :: Name -> Name -> CaseAlt -> CaseAlt Source #

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