| 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
- 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
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
type ErasureInfo = Name -> [Int] #
Constructors
| CoverageCheck [Int] | |
| CompileTime | |
| RunTime |
Instances
| Eq CaseType # | |
| 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 :: (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 # | |
Defined in Idris.Core.CaseTree | |
| Show CaseType # | |
| Generic CaseType # | |
| ToJSON CaseType # | |
Defined in IRTS.Portable | |
| Binary CaseType # | |
| NFData CaseType # | |
Defined in Idris.Core.DeepSeq | |
| type Rep CaseType # | |
simpleCase :: Bool -> SC -> Bool -> Phase -> FC -> [Int] -> [(Type, Bool)] -> [([Name], Term, Term)] -> ErasureInfo -> TC CaseDef #
findCalls :: SC -> [Name] -> [(Name, [[Name]])] #
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
findUsedArgs :: SC -> [Name] -> [Name] #