| Safe Haskell | None |
|---|---|
| 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
- 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 -> DataCon
- lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Maybe TyCon
- lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> TyCon
- lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> 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]
- ofBareTypeE :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> Either UserError 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 -> UserError
- resolveLocalBinds :: Env -> [(Var, LocBareType, Maybe [Located Expr])] -> [(Var, LocBareType, Maybe [Located Expr])]
- partitionLocalBinds :: [(Var, a)] -> ([(Var, a)], [(Var, a)])
Creating the Environment
Resolving symbols
class ResolveSym a where #
Using the environment
Instances
| ResolveSym DataCon # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
| ResolveSym Var # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
| ResolveSym TyCon # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
| ResolveSym Symbol # | |
Defined in Language.Haskell.Liquid.Bare.Resolve | |
Instances
| Qualify Equation # | |
| Qualify Qualifier # | |
| Qualify Symbol # | |
| Qualify Expr # | |
| Qualify Body # | |
| Qualify SizeFun # | |
| Qualify DataCtor # | |
| Qualify DataDecl # | |
| Qualify SpecType # | |
| Qualify BareType # | |
| Qualify RReft # | |
| Qualify TyConInfo # | |
| Qualify RTyCon # | |
| Qualify TyConP # | |
| Qualify TyConMap # | |
| Qualify BareMeasure # | |
Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareMeasure -> BareMeasure # | |
| Qualify BareSpec # | |
| Qualify ModSpecs # | |
| Qualify a => Qualify [a] # | |
| Qualify a => Qualify (Maybe a) # | |
| Qualify a => Qualify (Located a) # | |
| Qualify b => Qualify (a, b) # | |
| Qualify (Measure SpecType DataCon) # | |
| Qualify (Def ty ctor) # | |
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.
lookupGhcNamedVar :: (NamedThing a, Symbolic a) => Env -> ModName -> a -> Maybe Var #
Checking if names exist
knownGhcType :: Env -> ModName -> LocBareType -> Bool #
Checking existence of names
Misc
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
Conversions from Bare
ofBareTypeE :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> Either UserError SpecType #
ofBareType :: Env -> ModName -> SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType #
ofBareType and ofBareTypeE should be the _only_ SpecType constructors
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
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)]) #