liquidhaskell-0.8.10.2: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

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

Creating the Environment

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

Creating an environment

Resolving symbols

class Qualify a where Source #

Methods

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

Instances

Instances details
Qualify Qualifier Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify Equation Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify Expr Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify Symbol Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify Body Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify SizeFun Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify DataCtor Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify DataDecl Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify SpecType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify RReft Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify TyConInfo Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify RTyCon Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify TyConP Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify TyConMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareMeasure Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify a => Qualify [a] Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify a => Qualify (Maybe a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify a => Qualify (Located a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify b => Qualify (a, b) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Qualify (Measure SpecType DataCon) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify (Def ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

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

Qualify various names

qualifyTopDummy :: Qualify a => Env -> ModName -> a -> a 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.

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

Conversions from Bare

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

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