Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Bare.Types

Contents

Name resolution environment
Tycon and Datacon processing environment
Signature processing environment
Measure related environment
Misc

Description

This module has the code that uses the GHC definitions to: 1. MAKE a name-resolution environment, 2. USE the environment to translate plain symbols into Var, TyCon, etc.

Synopsis

data Env = RE {
- reLMap :: !LogicMap
- reSyms :: ![(Symbol, Var)]
- _reSubst :: !Subst
- _reTyThings :: !TyThingMap
- reCfg :: !Config
- reQualImps :: !QImports
- reAllImps :: !(HashSet Symbol)
- reLocalVars :: !LocalVars
- reGlobSyms :: !(HashSet Symbol)
- reSrc :: !GhcSrc
}
type TyThingMap = HashMap Symbol [(Symbol, TyThing)]
type ModSpecs = HashMap ModName BareSpec
type LocalVars = HashMap Symbol [(Int, Var)]
data TycEnv = TycEnv {
- tcTyCons :: ![TyConP]
- tcDataCons :: ![DataConP]
- tcSelMeasures :: ![Measure SpecType DataCon]
- tcSelVars :: ![(Var, LocSpecType)]
- tcTyConMap :: !TyConMap
- tcAdts :: ![DataDecl]
- tcDataConMap :: !DataConMap
- tcEmbs :: !(TCEmb TyCon)
- tcName :: !ModName
}
type DataConMap = HashMap (Symbol, Int) Symbol
data TyConMap
data SigEnv = SigEnv {
- sigEmbs :: !(TCEmb TyCon)
- sigTyRTyMap :: !TyConMap
- sigExports :: !(HashSet StableName)
- sigRTEnv :: !BareRTEnv
}
data MeasEnv = MeasEnv {
- meMeasureSpec :: !(MSpec SpecType DataCon)
- meClassSyms :: ![(Symbol, Located (RRType Reft))]
- meSyms :: ![(Symbol, Located (RRType Reft))]
- meDataCons :: ![(Var, LocSpecType)]
- meClasses :: ![DataConP]
- meMethods :: ![(ModName, Var, LocSpecType)]
- meCLaws :: ![(Class, [(ModName, Var, LocSpecType)])]
}
data PlugTV v
- = HsTV v
- | LqTV v
- | GenTV
- | RawTV
plugSrc :: PlugTV v -> Maybe v
varRSort :: Var -> RSort
varSortedReft :: TCEmb TyCon -> Var -> SortedReft
failMaybe :: Env -> ModName -> Either UserError r -> Maybe r

Name resolution environment

data Env #

Constructors

RE

Fields

reLMap :: !LogicMap
reSyms :: ![(Symbol, Var)]
see "syms" in old makeGhcSpec'
_reSubst :: !Subst
see "su" in old makeGhcSpec'
_reTyThings :: !TyThingMap
reCfg :: !Config
reQualImps :: !QImports
qualified imports
reAllImps :: !(HashSet Symbol)
all imported modules
reLocalVars :: !LocalVars
lines at which local variables are defined.
reGlobSyms :: !(HashSet Symbol)
global symbols, typically unlifted measures like len, fromJust
reSrc :: !GhcSrc
all source info

Instances

Instances details

HasConfig Env #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods getConfig :: Env -> Config #

type TyThingMap = HashMap Symbol [(Symbol, TyThing)] #

A TyThingMap is used to resolve symbols into GHC TyThing and, from there into Var, TyCon, DataCon, etc.

type ModSpecs = HashMap ModName BareSpec #

type LocalVars = HashMap Symbol [(Int, Var)] #

LocalVars is a map from names to lists of pairs of Ghc.Var and the lines at which they were defined.

Tycon and Datacon processing environment

data TycEnv #

A TycEnv contains the information needed to process Type- and Data- Constructors

Constructors

TycEnv
Fields tcTyCons :: ![TyConP] tcDataCons :: ![DataConP] tcSelMeasures :: ![Measure SpecType DataCon] tcSelVars :: ![(Var, LocSpecType)] tcTyConMap :: !TyConMap tcAdts :: ![DataDecl] tcDataConMap :: !DataConMap tcEmbs :: !(TCEmb TyCon) tcName :: !ModName

type DataConMap = HashMap (Symbol, Int) Symbol #

data TyConMap #

Information about Type Constructors

Instances

Instances details

Qualify TyConMap #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap #

Signature processing environment

data SigEnv #

A SigEnv contains the needed to process type signatures

Constructors

SigEnv
Fields sigEmbs :: !(TCEmb TyCon) sigTyRTyMap :: !TyConMap sigExports :: !(HashSet StableName) sigRTEnv :: !BareRTEnv

Measure related environment

data MeasEnv #

Intermediate representation for Measure information

Constructors

MeasEnv
Fields meMeasureSpec :: !(MSpec SpecType DataCon) meClassSyms :: ![(Symbol, Located (RRType Reft))] meSyms :: ![(Symbol, Located (RRType Reft))] meDataCons :: ![(Var, LocSpecType)] meClasses :: ![DataConP] meMethods :: ![(ModName, Var, LocSpecType)] meCLaws :: ![(Class, [(ModName, Var, LocSpecType)])]

Misc

data PlugTV v #

See [NOTE: Plug-Holes-TyVars] for a rationale for PlugTV

Constructors

HsTV v	Use tyvars from GHC specification (in the `v`)
LqTV v	Use tyvars from Liquid specification
GenTV	Generalize ty-vars
RawTV	Do NOT generalize ty-vars (e.g. for type-aliases)

Instances

Instances details

Show v => Show (PlugTV v) #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods showsPrec :: Int -> PlugTV v -> ShowS # show :: PlugTV v -> String # showList :: [PlugTV v] -> ShowS #
(Show v, PPrint v) => PPrint (PlugTV v) #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods pprintTidy :: Tidy -> PlugTV v -> Doc # pprintPrec :: Int -> Tidy -> PlugTV v -> Doc #

plugSrc :: PlugTV v -> Maybe v #

varRSort :: Var -> RSort #

varSortedReft :: TCEmb TyCon -> Var -> SortedReft #

Converting Var to Sort

failMaybe :: Env -> ModName -> Either UserError r -> Maybe r #

Handling failed resolution