Language.Haskell.Liquid.Bare.Types

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.

Name resolution environment

data Env

Name resolution environment

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

HasConfig Env

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

Qualify TyConMap

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

Show v => Show (PlugTV v)

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)

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