| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Constraint.Env
Description
This module defines the representation for Environments needed during constraint generation.
Synopsis
- (+++=) :: (CGEnv, String) -> (Symbol, CoreExpr, SpecType) -> CG CGEnv
- (+=) :: CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
- extendEnvWithVV :: CGEnv -> SpecType -> CG CGEnv
- addBinders :: CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
- addSEnv :: CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
- addEEnv :: CGEnv -> (Symbol, SpecType) -> CG CGEnv
- addRewritesForNextBinding :: LocalRewrites -> CG ()
- (-=) :: CGEnv -> Symbol -> CGEnv
- globalize :: CGEnv -> CGEnv
- fromListREnv :: [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv
- toListREnv :: REnv -> [(Symbol, SpecType)]
- insertREnv :: Symbol -> SpecType -> REnv -> REnv
- localBindsOfType :: RRType r -> REnv -> [Symbol]
- lookupREnv :: Symbol -> REnv -> Maybe SpecType
- (?=) :: (?callStack :: CallStack) => CGEnv -> Symbol -> Maybe SpecType
- rTypeSortedReft' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r)) => CGEnv -> Templates -> RRType r -> SortedReft
- setLocation :: CGEnv -> Span -> CGEnv
- setBind :: CGEnv -> Var -> CGEnv
- setRecs :: CGEnv -> [Var] -> CGEnv
- setTRec :: CGEnv -> [(Var, SpecType)] -> CGEnv
- getLocation :: CGEnv -> SrcSpan
Insert
addRewritesForNextBinding :: LocalRewrites -> CG () Source #
Add local rewrites associated to the next binding that will be inserted.
Construction
Query
Pruning refinements (TODO: move!)
rTypeSortedReft' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r)) => CGEnv -> Templates -> RRType r -> SortedReft Source #
Extend CGEnv
Lookup CGEnv
getLocation :: CGEnv -> SrcSpan Source #