License | BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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
- 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
- type ErasureInfo = Name -> [Int]
- data Phase
- = CoverageCheck [Int]
- | CompileTime
- | RunTime
- type CaseTree = SC
- data CaseType
- 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
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 # | |
Binary SC | |
TermSize SC Source # | |
ToJSON t => ToJSON (SC' t) | |
Defined in IRTS.Portable Methods toEncoding :: SC' t -> Encoding toJSONList :: [SC' t] -> Value toEncodingList :: [SC' t] -> Encoding | |
Generic (SC' t) Source # | |
Show t => Show (SC' t) Source # | |
NFData t => NFData (SC' t) | |
Defined in Idris.Core.DeepSeq | |
Eq t => Eq (SC' t) Source # | |
Ord t => Ord (SC' t) Source # | |
type Rep (SC' t) Source # | |
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)))) |
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 # | |
Binary CaseAlt | |
TermSize CaseAlt Source # | |
ToJSON t => ToJSON (CaseAlt' t) | |
Defined in IRTS.Portable Methods toEncoding :: CaseAlt' t -> Encoding toJSONList :: [CaseAlt' t] -> Value toEncodingList :: [CaseAlt' t] -> Encoding | |
Generic (CaseAlt' t) Source # | |
Show t => Show (CaseAlt' t) Source # | |
NFData t => NFData (CaseAlt' t) | |
Defined in Idris.Core.DeepSeq | |
Eq t => Eq (CaseAlt' t) Source # | |
Ord t => Ord (CaseAlt' t) Source # | |
type Rep (CaseAlt' t) Source # | |
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 #
Constructors
CoverageCheck [Int] | |
CompileTime | |
RunTime |
Instances
ToJSON CaseType | |
Defined in IRTS.Portable Methods toEncoding :: CaseType -> Encoding toJSONList :: [CaseType] -> Value toEncodingList :: [CaseType] -> Encoding | |
Data CaseType | |
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 # | |
Show CaseType Source # | |
Binary CaseType | |
NFData CaseType | |
Defined in Idris.Core.DeepSeq | |
Eq CaseType Source # | |
Ord CaseType Source # | |
Defined in Idris.Core.CaseTree | |
type Rep CaseType Source # | |
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 #