Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.Names

Synopsis

class CompatibleBinder b b' where
- coerceBinder :: b' -> b
lenLocSymbol :: Located Symbol
anyTypeSymbol :: Symbol
propSymbol :: Symbol
getPropIndex :: ReftV Symbol -> Maybe (ExprV Symbol)
selfSymbol :: Symbol
tyTupleSizedSymbol :: Int -> Symbol
isTyTupleSizedSymbol :: Symbol -> Maybe Int
tmTupleSizedSymbol :: Int -> Symbol
data LogicName
- = LogicName !Symbol !Module !(Maybe Name)
- | GeneratedLogicName Symbol
data LHResolvedName
- = LHRLogic !LogicName
- | LHRGHC !Name
- | LHRLocal !Symbol
- | LHRIndex Word
data LHName
- = LHNResolved !LHResolvedName !Symbol
- | LHNUnresolved !LHNameSpace !Symbol
data LHNameSpace
- = LHTcName LHThisModuleNameFlag
- | LHDataConName LHThisModuleNameFlag
- | LHVarName LHThisModuleNameFlag
- | LHLogicNameBinder
- | LHLogicName
data LHThisModuleNameFlag
- = LHThisModuleNameF
- | LHAnyModuleNameF
makeResolvedLHName :: LHResolvedName -> Symbol -> LHName
getLHGHCName :: LHName -> Maybe Name
getLHNameResolved :: HasCallStack => LHName -> LHResolvedName
getLHNameSymbol :: LHName -> Symbol
lhNameToResolvedSymbol :: LHName -> Symbol
lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol
makeGHCLHName :: Name -> Symbol -> LHName
makeGHCLHNameFromId :: Id -> LHName
makeGHCLHNameLocated :: (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocatedFromId :: Id -> Located LHName
makeLocalLHName :: Symbol -> LHName
makeLogicLHName :: Symbol -> Module -> Maybe Name -> LHName
makeGeneratedLogicLHName :: Symbol -> LHName
makeUnresolvedLHName :: LHNameSpace -> Symbol -> LHName
mapLHNames :: Data a => (LHName -> LHName) -> a -> a
mapMLocLHNames :: forall m a. (Data a, Monad m) => (Located LHName -> m (Located LHName)) -> a -> m a
maybeReflectedLHName :: LHName -> Maybe Name
reflectGHCName :: Module -> Name -> LHName
reflectLHName :: HasCallStack => Module -> LHName -> LHName
updateLHNameSymbol :: (Symbol -> Symbol) -> LHName -> LHName
isNonReflectedLogicName :: LHName -> Bool
logicNameOriginModule :: LHName -> Module
isResolvedLogicName :: LHName -> Bool
isGeneratedLogicName :: LHName -> Bool

Documentation

class CompatibleBinder b b' where Source #

Highly temporary class as a compatability layer to express that a binder, especially type variables tv, are in the same namespace as another binder.

Minimal complete definition

Nothing

Methods

coerceBinder :: b' -> b Source #

default coerceBinder :: b ~ b' => b' -> b Source #

Instances

Instances details

CompatibleBinder Symbol Symbol Source #
Instance details Defined in Language.Haskell.Liquid.Types.Names Methods coerceBinder :: Symbol -> Symbol Source #
CompatibleBinder Symbol BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods coerceBinder :: BTyVar -> Symbol Source #
CompatibleBinder Symbol (Located Symbol) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Names Methods coerceBinder :: Located Symbol -> Symbol Source #
CompatibleBinder (Located Symbol) BTyVar Source #
Instance details Defined in Language.Haskell.Liquid.Types.RType Methods coerceBinder :: BTyVar -> Located Symbol Source #
CompatibleBinder (Located Symbol) (Located Symbol) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Names Methods coerceBinder :: Located Symbol -> Located Symbol Source #

lenLocSymbol :: Located Symbol Source #

anyTypeSymbol :: Symbol Source #

propSymbol :: Symbol Source #

getPropIndex :: ReftV Symbol -> Maybe (ExprV Symbol) Source #

selfSymbol :: Symbol Source #

tyTupleSizedSymbol :: Int -> Symbol Source #

isTyTupleSizedSymbol :: Symbol -> Maybe Int Source #

tmTupleSizedSymbol :: Int -> Symbol Source #

data LogicName Source #

A name for an entity that does not exist in Haskell

For instance, this can be used to represent predicate aliases or uninterpreted functions.

Constructors

LogicName
Fields !Symbol Unqualified symbol !Module Module where the entity was defined !(Maybe Name) If the named entity is the reflection of some Haskell name
GeneratedLogicName Symbol

Instances

Instances details

NFData LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

rnf :: LogicName -> () #

Binary LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

put_ :: WriteBinHandle -> LogicName -> IO () #

put :: WriteBinHandle -> LogicName -> IO (Bin LogicName) #

get :: ReadBinHandle -> IO LogicName #

Eq LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

(==) :: LogicName -> LogicName -> Bool #

(/=) :: LogicName -> LogicName -> Bool #

Ord LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

compare :: LogicName -> LogicName -> Ordering #

(<) :: LogicName -> LogicName -> Bool #

(<=) :: LogicName -> LogicName -> Bool #

(>) :: LogicName -> LogicName -> Bool #

(>=) :: LogicName -> LogicName -> Bool #

max :: LogicName -> LogicName -> LogicName #

min :: LogicName -> LogicName -> LogicName #

Data LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LogicName -> c LogicName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LogicName #

toConstr :: LogicName -> Constr #

dataTypeOf :: LogicName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LogicName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicName) #

gmapT :: (forall b. Data b => b -> b) -> LogicName -> LogicName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LogicName -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LogicName -> r #

gmapQ :: (forall d. Data d => d -> u) -> LogicName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LogicName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LogicName -> m LogicName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LogicName -> m LogicName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LogicName -> m LogicName #

Generic LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Associated Types

type Rep LogicName

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LogicName = D1 ('MetaData "LogicName" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LogicName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Module) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Name)))) :+: C1 ('MetaCons "GeneratedLogicName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

Methods

from :: LogicName -> Rep LogicName x #

to :: Rep LogicName x -> LogicName #

Show LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

showsPrec :: Int -> LogicName -> ShowS #

show :: LogicName -> String #

showList :: [LogicName] -> ShowS #

Hashable LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

hashWithSalt :: Int -> LogicName -> Int #

hash :: LogicName -> Int #

type Rep LogicName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LogicName = D1 ('MetaData "LogicName" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LogicName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Module) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Name)))) :+: C1 ('MetaCons "GeneratedLogicName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

data LHResolvedName Source #

A name whose procedence is known.

Constructors

LHRLogic !LogicName
LHRGHC !Name	A name for an entity that exists in Haskell
LHRLocal !Symbol	A name for a local variable, e.g. one that is bound by a type alias.
LHRIndex Word	The index of a name in some environment Before serializing names, they are converted to indices. The names themselves are kept in an environment or table that is serialized separately. This is to acommodate how GHC serializes its Names.

Instances

Instances details

Binary LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

put :: LHResolvedName -> Put #

get :: Get LHResolvedName #

putList :: [LHResolvedName] -> Put #

NFData LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

rnf :: LHResolvedName -> () #

Binary LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

put_ :: WriteBinHandle -> LHResolvedName -> IO () #

put :: WriteBinHandle -> LHResolvedName -> IO (Bin LHResolvedName) #

get :: ReadBinHandle -> IO LHResolvedName #

Eq LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

(==) :: LHResolvedName -> LHResolvedName -> Bool #

(/=) :: LHResolvedName -> LHResolvedName -> Bool #

Ord LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

compare :: LHResolvedName -> LHResolvedName -> Ordering #

(<) :: LHResolvedName -> LHResolvedName -> Bool #

(<=) :: LHResolvedName -> LHResolvedName -> Bool #

(>) :: LHResolvedName -> LHResolvedName -> Bool #

(>=) :: LHResolvedName -> LHResolvedName -> Bool #

max :: LHResolvedName -> LHResolvedName -> LHResolvedName #

min :: LHResolvedName -> LHResolvedName -> LHResolvedName #

Data LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHResolvedName -> c LHResolvedName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHResolvedName #

toConstr :: LHResolvedName -> Constr #

dataTypeOf :: LHResolvedName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHResolvedName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHResolvedName) #

gmapT :: (forall b. Data b => b -> b) -> LHResolvedName -> LHResolvedName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r #

gmapQ :: (forall d. Data d => d -> u) -> LHResolvedName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHResolvedName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHResolvedName -> m LHResolvedName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHResolvedName -> m LHResolvedName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHResolvedName -> m LHResolvedName #

Generic LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Associated Types

type Rep LHResolvedName

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHResolvedName = D1 ('MetaData "LHResolvedName" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) ((C1 ('MetaCons "LHRLogic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LogicName)) :+: C1 ('MetaCons "LHRGHC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name))) :+: (C1 ('MetaCons "LHRLocal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "LHRIndex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word))))

Methods

from :: LHResolvedName -> Rep LHResolvedName x #

to :: Rep LHResolvedName x -> LHResolvedName #

Show LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

showsPrec :: Int -> LHResolvedName -> ShowS #

show :: LHResolvedName -> String #

showList :: [LHResolvedName] -> ShowS #

Hashable LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

hashWithSalt :: Int -> LHResolvedName -> Int #

hash :: LHResolvedName -> Int #

type Rep LHResolvedName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHResolvedName = D1 ('MetaData "LHResolvedName" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) ((C1 ('MetaCons "LHRLogic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LogicName)) :+: C1 ('MetaCons "LHRGHC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name))) :+: (C1 ('MetaCons "LHRLocal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "LHRIndex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word))))

data LHName Source #

A name that is potentially unresolved, carrying along the Symbol found by the parser.

Constructors

LHNResolved !LHResolvedName !Symbol	In order to integrate the resolved names gradually, we keep the unresolved names.
LHNUnresolved !LHNameSpace !Symbol

Instances

Instances details

Binary LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

put :: LHName -> Put #

get :: Get LHName #

putList :: [LHName] -> Put #

NFData LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

rnf :: LHName -> () #

Eq LHName Source #

An Eq instance that ignores the Symbol in resolved names

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

(==) :: LHName -> LHName -> Bool #

(/=) :: LHName -> LHName -> Bool #

Ord LHName Source #

An Ord instance that ignores the Symbol in resolved names

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

compare :: LHName -> LHName -> Ordering #

(<) :: LHName -> LHName -> Bool #

(<=) :: LHName -> LHName -> Bool #

(>) :: LHName -> LHName -> Bool #

(>=) :: LHName -> LHName -> Bool #

max :: LHName -> LHName -> LHName #

min :: LHName -> LHName -> LHName #

Data LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHName -> c LHName #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHName #

toConstr :: LHName -> Constr #

dataTypeOf :: LHName -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHName) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHName) #

gmapT :: (forall b. Data b => b -> b) -> LHName -> LHName #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r #

gmapQ :: (forall d. Data d => d -> u) -> LHName -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHName -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHName -> m LHName #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHName -> m LHName #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHName -> m LHName #

Generic LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Associated Types

type Rep LHName

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHName = D1 ('MetaData "LHName" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LHNResolved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LHResolvedName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "LHNUnresolved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LHNameSpace) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)))

Methods

from :: LHName -> Rep LHName x #

to :: Rep LHName x -> LHName #

Show LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

showsPrec :: Int -> LHName -> ShowS #

show :: LHName -> String #

showList :: [LHName] -> ShowS #

Hashable LHName Source #

A Hashable instance that ignores the Symbol in resolved names

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

hashWithSalt :: Int -> LHName -> Int #

hash :: LHName -> Int #

Fixpoint LHName

Instance details

Defined in Language.Haskell.Liquid.Types.PrettyPrint

Methods

toFix :: LHName -> Doc

simplify :: LHName -> LHName

PPrint LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

pprintTidy :: Tidy -> LHName -> Doc #

pprintPrec :: Int -> Tidy -> LHName -> Doc #

Expand BareDef Source #

Instance details

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareDef -> BareDef Source #

Expand BareMeasure Source #

Instance details

Defined in Language.Haskell.Liquid.Bare.Expand

Methods

expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure Source #

type Rep LHName Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHName = D1 ('MetaData "LHName" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LHNResolved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LHResolvedName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "LHNUnresolved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LHNameSpace) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)))

data LHNameSpace Source #

Constructors

LHTcName LHThisModuleNameFlag	Type constructors
LHDataConName LHThisModuleNameFlag	Data constructors with procedence
LHVarName LHThisModuleNameFlag	Variables with procedence
LHLogicNameBinder	Logic names (LHS)
LHLogicName	Logic names (RHS)

Instances

Instances details

Binary LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

put :: LHNameSpace -> Put #

get :: Get LHNameSpace #

putList :: [LHNameSpace] -> Put #

NFData LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

rnf :: LHNameSpace -> () #

Eq LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

(==) :: LHNameSpace -> LHNameSpace -> Bool #

(/=) :: LHNameSpace -> LHNameSpace -> Bool #

Ord LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

compare :: LHNameSpace -> LHNameSpace -> Ordering #

(<) :: LHNameSpace -> LHNameSpace -> Bool #

(<=) :: LHNameSpace -> LHNameSpace -> Bool #

(>) :: LHNameSpace -> LHNameSpace -> Bool #

(>=) :: LHNameSpace -> LHNameSpace -> Bool #

max :: LHNameSpace -> LHNameSpace -> LHNameSpace #

min :: LHNameSpace -> LHNameSpace -> LHNameSpace #

Data LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHNameSpace -> c LHNameSpace #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHNameSpace #

toConstr :: LHNameSpace -> Constr #

dataTypeOf :: LHNameSpace -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHNameSpace) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHNameSpace) #

gmapT :: (forall b. Data b => b -> b) -> LHNameSpace -> LHNameSpace #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r #

gmapQ :: (forall d. Data d => d -> u) -> LHNameSpace -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHNameSpace -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace #

Generic LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Associated Types

type Rep LHNameSpace

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHNameSpace = D1 ('MetaData "LHNameSpace" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) ((C1 ('MetaCons "LHTcName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHThisModuleNameFlag)) :+: C1 ('MetaCons "LHDataConName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHThisModuleNameFlag))) :+: (C1 ('MetaCons "LHVarName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHThisModuleNameFlag)) :+: (C1 ('MetaCons "LHLogicNameBinder" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LHLogicName" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: LHNameSpace -> Rep LHNameSpace x #

to :: Rep LHNameSpace x -> LHNameSpace #

Show LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

showsPrec :: Int -> LHNameSpace -> ShowS #

show :: LHNameSpace -> String #

showList :: [LHNameSpace] -> ShowS #

Hashable LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

hashWithSalt :: Int -> LHNameSpace -> Int #

hash :: LHNameSpace -> Int #

type Rep LHNameSpace Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHNameSpace = D1 ('MetaData "LHNameSpace" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) ((C1 ('MetaCons "LHTcName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHThisModuleNameFlag)) :+: C1 ('MetaCons "LHDataConName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHThisModuleNameFlag))) :+: (C1 ('MetaCons "LHVarName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHThisModuleNameFlag)) :+: (C1 ('MetaCons "LHLogicNameBinder" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LHLogicName" 'PrefixI 'False) (U1 :: Type -> Type))))

data LHThisModuleNameFlag Source #

Whether the name should be looked up in the current module only or in any module

Constructors

LHThisModuleNameF
LHAnyModuleNameF

Instances

Instances details

Binary LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

put :: LHThisModuleNameFlag -> Put #

get :: Get LHThisModuleNameFlag #

putList :: [LHThisModuleNameFlag] -> Put #

NFData LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

rnf :: LHThisModuleNameFlag -> () #

Eq LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

(==) :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool #

(/=) :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool #

Ord LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

compare :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Ordering #

(<) :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool #

(<=) :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool #

(>) :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool #

(>=) :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool #

max :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> LHThisModuleNameFlag #

min :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> LHThisModuleNameFlag #

Data LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHThisModuleNameFlag -> c LHThisModuleNameFlag #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHThisModuleNameFlag #

toConstr :: LHThisModuleNameFlag -> Constr #

dataTypeOf :: LHThisModuleNameFlag -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHThisModuleNameFlag) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHThisModuleNameFlag) #

gmapT :: (forall b. Data b => b -> b) -> LHThisModuleNameFlag -> LHThisModuleNameFlag #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r #

gmapQ :: (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHThisModuleNameFlag -> m LHThisModuleNameFlag #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHThisModuleNameFlag -> m LHThisModuleNameFlag #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHThisModuleNameFlag -> m LHThisModuleNameFlag #

Generic LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Associated Types

type Rep LHThisModuleNameFlag
Instance details Defined in Language.Haskell.Liquid.Types.Names type Rep LHThisModuleNameFlag = D1 ('MetaData "LHThisModuleNameFlag" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LHThisModuleNameF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LHAnyModuleNameF" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: LHThisModuleNameFlag -> Rep LHThisModuleNameFlag x #

to :: Rep LHThisModuleNameFlag x -> LHThisModuleNameFlag #

Show LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

showsPrec :: Int -> LHThisModuleNameFlag -> ShowS #

show :: LHThisModuleNameFlag -> String #

showList :: [LHThisModuleNameFlag] -> ShowS #

Hashable LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

Methods

hashWithSalt :: Int -> LHThisModuleNameFlag -> Int #

hash :: LHThisModuleNameFlag -> Int #

type Rep LHThisModuleNameFlag Source #

Instance details

Defined in Language.Haskell.Liquid.Types.Names

type Rep LHThisModuleNameFlag = D1 ('MetaData "LHThisModuleNameFlag" "Language.Haskell.Liquid.Types.Names" "liquidhaskell-boot-0.9.14.1-inplace" 'False) (C1 ('MetaCons "LHThisModuleNameF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LHAnyModuleNameF" 'PrefixI 'False) (U1 :: Type -> Type))

makeResolvedLHName :: LHResolvedName -> Symbol -> LHName Source #

getLHGHCName :: LHName -> Maybe Name Source #

getLHNameResolved :: HasCallStack => LHName -> LHResolvedName Source #

Get the resolved Symbol from an LHName.

getLHNameSymbol :: LHName -> Symbol Source #

Get the unresolved Symbol from an LHName.

lhNameToResolvedSymbol :: LHName -> Symbol Source #

Converts resolved names to symbols.

One important postcondition of this function is that the symbol for reflected names must match exactly the symbol for the corresponding Haskell function. Otherwise, LH would fail to link the two at various places where it is needed.

lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol Source #

makeGHCLHName :: Name -> Symbol -> LHName Source #

makeGHCLHNameFromId :: Id -> LHName Source #

makeGHCLHNameLocated :: (NamedThing a, Symbolic a) => a -> Located LHName Source #

makeGHCLHNameLocatedFromId :: Id -> Located LHName Source #

makeLocalLHName :: Symbol -> LHName Source #

makeLogicLHName :: Symbol -> Module -> Maybe Name -> LHName Source #

makeGeneratedLogicLHName :: Symbol -> LHName Source #

makeUnresolvedLHName :: LHNameSpace -> Symbol -> LHName Source #

mapLHNames :: Data a => (LHName -> LHName) -> a -> a Source #

mapMLocLHNames :: forall m a. (Data a, Monad m) => (Located LHName -> m (Located LHName)) -> a -> m a Source #