Language.Haskell.Liquid.Constraint.Env

This module defines the representation for Environments needed during constraint generation.

Insert

(+++=) :: (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

(-=) :: CGEnv -> Symbol -> CGEnv

globalize :: CGEnv -> CGEnv

Construction

fromListREnv :: [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv

toListREnv :: REnv -> [(Symbol, SpecType)]

insertREnv :: Symbol -> SpecType -> REnv -> REnv

Query

localBindsOfType :: RRType r -> REnv -> [Symbol]

lookupREnv :: Symbol -> REnv -> Maybe SpecType

(?=) :: (?callStack :: CallStack) => CGEnv -> Symbol -> Maybe SpecType

Pruning refinements (TODO: move!)

rTypeSortedReft' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r)) => CGEnv -> Templates -> RRType r -> SortedReft

Extend CGEnv

setLocation :: CGEnv -> Span -> CGEnv

setBind :: CGEnv -> Var -> CGEnv

setRecs :: CGEnv -> [Var] -> CGEnv

setTRec :: CGEnv -> [(Var, SpecType)] -> CGEnv

Lookup CGEnv

getLocation :: CGEnv -> SrcSpan