| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Bare.Resolve
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
- makeEnv :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
- class ResolveSym a where
- class Qualify a where
- type Lookup a = Either [Error] a
- qualifyTop :: Qualify a => Env -> ModName -> SourcePos -> a -> a
- qualifyTopDummy :: Qualify a => Env -> ModName -> a -> a
- maybeResolveSym :: ResolveSym a => Env -> ModName -> String -> LocSymbol -> Maybe a
- 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
- knownGhcVar :: Env -> ModName -> LocSymbol -> Bool
- knownGhcTyCon :: Env -> ModName -> LocSymbol -> Bool
- knownGhcDataCon :: Env -> ModName -> LocSymbol -> Bool
- knownGhcType :: Env -> ModName -> LocBareType -> Bool
- srcVars :: GhcSrc -> [Var]
- coSubRReft :: CoSub -> RReft -> RReft
- unQualifySymbol :: Symbol -> (Maybe Symbol, Symbol)
- ofBareTypeE :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
- ofBareType :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
- ofBPVar :: Env -> ModName -> SourcePos -> BPVar -> RPVar
- txRefSort :: TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
- errResolve :: Doc -> String -> LocSymbol -> Error
- resolveLocalBinds :: Env -> [(Var, LocBareType, Maybe [Located Expr])] -> [(Var, LocBareType, Maybe [Located Expr])]
- partitionLocalBinds :: [(Var, a)] -> ([(Var, a)], [(Var, a)])
Creating the Environment
makeEnv :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env Source #
Creating an environment
Resolving symbols
class ResolveSym a where Source #
Using the environment
Instances
| ResolveSym DataCon Source # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
| ResolveSym TyCon Source # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
| ResolveSym Var Source # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
| ResolveSym Symbol Source # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
class Qualify a where Source #
Instances
| Qualify Equation Source # | |
| Qualify Qualifier Source # | |
| Qualify Symbol Source # | |
| Qualify Expr Source # | |
| Qualify ModSpecs Source # | |
| Qualify BareSpec Source # | |
| Qualify BareMeasure Source # | |
Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure Source # | |
| Qualify BareType Source # | |
| Qualify Body Source # | |
| Qualify DataCtor Source # | |
| Qualify DataDecl Source # | |
| Qualify RReft Source # | |
| Qualify RTyCon Source # | |
| Qualify SizeFun Source # | |
| Qualify SpecType Source # | |
| Qualify TyConInfo Source # | |
| Qualify TyConMap Source # | |
| Qualify TyConP Source # | |
| Qualify a => Qualify (Located a) Source # | |
| Qualify a => Qualify (Maybe a) Source # | |
| Qualify a => Qualify [a] Source # | |
| Qualify (Def ty ctor) Source # | |
| Qualify (Measure SpecType DataCon) Source # | |
| Qualify a => Qualify (RTAlias Symbol a) Source # | |
| Qualify b => Qualify (a, b) Source # | |
Looking up names
maybeResolveSym :: ResolveSym a => Env -> ModName -> String -> LocSymbol -> Maybe a Source #
maybeResolve wraps the plain resolve to return Nothing
if the name being searched for is unknown.
lookupGhcNamedVar :: (NamedThing a, Symbolic a) => Env -> ModName -> a -> Maybe Var Source #
Checking if names exist
knownGhcType :: Env -> ModName -> LocBareType -> Bool Source #
Checking existence of names
Misc
srcVars :: GhcSrc -> [Var] Source #
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
unQualifySymbol :: Symbol -> (Maybe Symbol, Symbol) Source #
`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 Source #
ofBareType :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType Source #
ofBareType and ofBareTypeE should be the _only_ SpecType constructors
Post-processing types
txRefSort :: TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType Source #
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
Fixing local variables
resolveLocalBinds :: Env -> [(Var, LocBareType, Maybe [Located Expr])] -> [(Var, LocBareType, Maybe [Located Expr])] Source #
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