Language.Haskell.Liquid.Bare.Resolve

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.

Creating the Environment

makeEnv :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env

Creating an environment

Resolving symbols

class ResolveSym a where

Using the environment

Methods

resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup a

Instances

ResolveSym DataCon

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup DataCon

ResolveSym TyCon

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon

ResolveSym Var

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup Var

ResolveSym Symbol

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup Symbol

class Qualify a where

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> a -> a

Instances

Qualify Equation

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Equation -> Equation

Qualify Qualifier

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Qualifier -> Qualifier

Qualify Symbol

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol

Qualify Expr

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr

Qualify ModSpecs

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs

Qualify BareSpec

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec

Qualify BareMeasure

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure

Qualify BareType

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType

Qualify Body

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body

Qualify DataCtor

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataCtor -> DataCtor

Qualify DataDecl

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataDecl -> DataDecl

Qualify RReft

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft

Qualify RTyCon

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTyCon -> RTyCon

Qualify SizeFun

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun

Qualify SpecType

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType

Qualify TyConInfo

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConInfo -> TyConInfo

Qualify TyConMap

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap

Qualify TyConP

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP

Qualify a => Qualify (Located a)

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Located a -> Located a

Qualify a => Qualify (Maybe a)

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Maybe a -> Maybe a

Qualify a => Qualify [a]

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> [a] -> [a]

Qualify (Def ty ctor)

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Def ty ctor -> Def ty ctor

Qualify (Measure SpecType DataCon)

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Measure SpecType DataCon -> Measure SpecType DataCon

Qualify a => Qualify (RTAlias Symbol a)

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTAlias Symbol a -> RTAlias Symbol a

Qualify b => Qualify (a, b)

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> (a, b) -> (a, b)

type Lookup a = Either [Error] a

qualifyTop :: Qualify a => Env -> ModName -> SourcePos -> a -> a

Qualify various names

qualifyTopDummy :: Qualify a => Env -> ModName -> a -> a

Looking up names

maybeResolveSym :: ResolveSym a => Env -> ModName -> String -> LocSymbol -> Maybe a

maybeResolve wraps the plain resolve to return Nothing if the name being searched for is unknown.

lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> Lookup DataCon

lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe TyCon)

lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon

lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Var

lookupGhcNamedVar :: (NamedThing a, Symbolic a) => Env -> ModName -> a -> Maybe Var

Checking if names exist

knownGhcVar :: Env -> ModName -> LocSymbol -> Bool

knownGhcTyCon :: Env -> ModName -> LocSymbol -> Bool

knownGhcDataCon :: Env -> ModName -> LocSymbol -> Bool

knownGhcType :: Env -> ModName -> LocBareType -> Bool

Checking existence of names

Misc

srcVars :: GhcSrc -> [Var]

We prioritize the Ghc.Var in srcVars because _giDefVars and gsTyThings have _different_ values for the same binder, with different types where the type params are alpha-renamed. However, for absref, we need _the same_ type parameters as used by GHC as those are used inside the lambdas and other bindings in the code. See also [NOTE: Plug-Holes-TyVars] and tests-absref-pos-Papp00.hs

coSubRReft :: CoSub -> RReft -> RReft

unQualifySymbol :: Symbol -> (Maybe Symbol, Symbol)

`unQualifySymbol name sym` splits sym into a pair `(mod, rest)` where mod is the name of the module, derived from sym if qualified.

Conversions from Bare

ofBareTypeE :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType

ofBareType :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType

ofBareType and ofBareTypeE should be the _only_ SpecType constructors

ofBPVar :: Env -> ModName -> SourcePos -> BPVar -> RPVar

Post-processing types

txRefSort :: TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType

Is this the SAME as addTyConInfo? No. txRefSort (1) adds the _real_ sorts to RProp, (2) gathers _extra_ RProp at turns them into refinements, e.g. testsposmulti-pred-app-00.hs

errResolve :: Doc -> String -> LocSymbol -> Error

Fixing local variables

resolveLocalBinds :: Env -> [(Var, LocBareType, Maybe [Located Expr])] -> [(Var, LocBareType, Maybe [Located Expr])]

resolveLocalBinds resolves that the "free" variables that appear in the type-sigs for non-toplevel binders (that correspond to other locally bound) source variables that are visible at that at non-top-level scope. e.g. tests-names-pos-local02.hs

partitionLocalBinds :: [(Var, a)] -> ([(Var, a)], [(Var, a)])