| 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 -> GHCTyLookupEnv -> [Id] -> TcGblEnv -> InstEnvs -> LocalVars -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
- makeLocalVars :: [CoreBind] -> LocalVars
- makeGHCTyLookupEnv :: CoreProgram -> TcRn GHCTyLookupEnv
- data GHCTyLookupEnv = GHCTyLookupEnv {}
- type Lookup a = Either [Error] a
- lookupGhcDataConLHName :: HasCallStack => Env -> Located LHName -> Lookup DataCon
- lookupGhcDnTyCon :: Env -> ModName -> DataName -> Lookup (Maybe TyCon)
- lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Id
- lookupLocalVar :: Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Var)
- lookupGhcTyConLHName :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Lookup TyCon
- lookupGhcTyThingFromName :: GHCTyLookupEnv -> Name -> Maybe TyThing
- lookupGhcId :: Env -> Name -> Maybe Id
- knownGhcType :: Env -> LocBareType -> Bool
- coSubRReft :: CoSub -> RReft -> RReft
- unQualifySymbol :: Symbol -> (Maybe Symbol, Symbol)
- ofBareTypeE :: HasCallStack => Env -> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
- ofBareType :: HasCallStack => Env -> SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
- ofBPVar :: Env -> 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 -> GHCTyLookupEnv -> [Id] -> TcGblEnv -> InstEnvs -> LocalVars -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env Source #
Creating an environment
makeLocalVars :: [CoreBind] -> LocalVars Source #
data GHCTyLookupEnv Source #
Constructors
| GHCTyLookupEnv | |
Fields
| |
Resolving symbols
Looking up names
lookupGhcDataConLHName :: HasCallStack => Env -> Located LHName -> Lookup DataCon Source #
lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Id Source #
lookupLocalVar :: Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Var) Source #
lookupLocalVar takes as input the list of "global" (top-level) vars
that also match the name lx; we then pick the "closest" definition.
See testsnamesLocalSpec.hs for a motivating example.
lookupGhcTyConLHName :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Lookup TyCon Source #
Checking if names exist
knownGhcType :: Env -> LocBareType -> Bool Source #
Checking existence of names
Misc
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 :: HasCallStack => Env -> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType Source #
ofBareType :: HasCallStack => Env -> 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