liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Names

Description

This module contains Haskell variables representing globally visible names. Rather than have strings floating around the system, all constant names should be defined here, and the (exported) variables should be used and manipulated elsewhere.

Synopsis

Symbols

data Symbol Source #

Invariant: a SafeText is made up of:

'0'..'9'
++ [a...z] ++ [A..Z] ++ $

If the original text has ANY other chars, it is represented as:

lq$i

where i is a unique integer (for each text)

Instances

Instances details
Data Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

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

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

toConstr :: Symbol -> Constr #

dataTypeOf :: Symbol -> DataType #

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

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

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

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

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

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

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

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

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

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

IsString Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

fromString :: String -> Symbol #

Generic Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Associated Types

type Rep Symbol :: Type -> Type #

Methods

from :: Symbol -> Rep Symbol x #

to :: Rep Symbol x -> Symbol #

Show Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Binary Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

put :: Symbol -> Put #

get :: Get Symbol #

putList :: [Symbol] -> Put #

NFData Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

rnf :: Symbol -> () #

Eq Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

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

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

Ord Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Hashable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

hashWithSalt :: Int -> Symbol -> Int #

hash :: Symbol -> Int #

Interned Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Associated Types

data Description Symbol #

type Uninterned Symbol #

Uninternable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Inputable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Parse

SMTLIB2 LocSymbol Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

SMTLIB2 Symbol Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Symbol -> Builder Source #

Symbolic Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol Source #

Fixpoint Symbol Source #
NOTE: SymbolText
Use symbolSafeText if you want it to machine-readable, but symbolText if you want it to be human-readable.
Instance details

Defined in Language.Fixpoint.Types.Names

PPrint Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Expression Symbol Source #

The symbol may be an encoding of a SymConst.

Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Symbol -> Expr Source #

Predicate Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr Source #

Subable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Store Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

size :: Size Symbol #

poke :: Symbol -> Poke () #

peek :: Peek Symbol #

Monoid (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: BindEnv a #

mappend :: BindEnv a -> BindEnv a -> BindEnv a #

mconcat :: [BindEnv a] -> BindEnv a #

Semigroup (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: BindEnv a -> BindEnv a -> BindEnv a #

sconcat :: NonEmpty (BindEnv a) -> BindEnv a #

stimes :: Integral b => b -> BindEnv a -> BindEnv a #

NFData a => NFData (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv a -> () #

Eq (Description Symbol) Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Hashable (Description Symbol) Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Defunc (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: BindEnv a -> DF (BindEnv a) Source #

Loc a => Elaborate (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Gradual (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> BindEnv a -> BindEnv a Source #

Fixpoint (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

SymConsts (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv a -> [SymConst] Source #

Visitable (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> BindEnv a -> VisitM a0 (BindEnv a) Source #

Store a => Store (BindEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

size :: Size (BindEnv a) #

poke :: BindEnv a -> Poke () #

peek :: Peek (BindEnv a) #

Defunc (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Defunc (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: (Symbol, Sort) -> DF (Symbol, Sort) Source #

SMTLIB2 (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #

Elaborate (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Expression (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr Source #

Visitable (Symbol, SortedReft, a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> (Symbol, SortedReft, a) -> VisitM a0 (Symbol, SortedReft, a) Source #

type Rep Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

type Rep Symbol = D1 ('MetaData "Symbol" "Language.Fixpoint.Types.Names" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "S" 'PrefixI 'True) (S1 ('MetaSel ('Just "_symbolId") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Id) :*: (S1 ('MetaSel ('Just "symbolRaw") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "symbolEncoded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))))
newtype Description Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

type Uninterned Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

class Symbolic a where Source #

Values that can be viewed as Symbols

Methods

symbol :: a -> Symbol Source #

Instances

Instances details
Symbolic Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol Source #

Symbolic SymConst Source #

String Constants ----------------------------------------------------------

Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.

Instance details

Defined in Language.Fixpoint.Types.Refinements

Symbolic DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: FTycon -> Symbol Source #

Symbolic Text Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Text -> Symbol Source #

Symbolic String Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: String -> Symbol Source #

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

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol Source #

type LocSymbol = Located Symbol Source #

Located Symbols -----------------------------------------------------

Conversion to/from Text

symbolSafeText :: Symbol -> SafeText Source #

symbolText :: Symbol -> Text Source #

Decoding Symbols -----------------------------------------------------

Destructors

Transforms

Widely used prefixes

Creating Symbols

Wrapping Symbols

bindSymbol :: Integer -> Symbol Source #

Used to define functions corresponding to binding predicates

The integer is the BindId.

testSymbol :: Symbol -> Symbol Source #

'testSymbol c' creates the `is-c` symbol for the adt-constructor named c.

suffixSymbol :: Symbol -> Symbol -> Symbol Source #

Use this **EXCLUSIVELY** when you want to add stuff in front of a Symbol

Unwrapping Symbols

Hardwired global names

Casting function names

Orphan instances

Data InternedText Source #

Symbols --------------------------------------------------

Instance details

Methods

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

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

toConstr :: InternedText -> Constr #

dataTypeOf :: InternedText -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic InternedText Source # 
Instance details

Associated Types

type Rep InternedText :: Type -> Type #

Fixpoint Text Source # 
Instance details