liquid-fixpoint-0.8.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Names

Contents

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
Eq Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

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

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

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 :: (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 #

Ord Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Show Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

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 #

Semigroup BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Monoid BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Binary Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

put :: Symbol -> Put #

get :: Get Symbol #

putList :: [Symbol] -> Put #

Binary BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

put :: BindEnv -> Put #

get :: Get BindEnv #

putList :: [BindEnv] -> Put #

NFData Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

rnf :: Symbol -> () #

NFData BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv -> () #

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 #

type Uninterned Symbol :: Type #

Uninternable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

PPrint Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

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

Fixpoint BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Symbolic Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol Source #

Subable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Predicate Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr Source #

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 #

SymConsts BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Visitable BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

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

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 #

Elaborate BindEnv Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Inputable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Parse

Gradual BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

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

Defunc BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: BindEnv -> DF BindEnv Source #

Eq (Description Symbol) Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Hashable (Description Symbol) Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Expression (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Methods

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

Visitable (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> (Symbol, SortedReft) -> VisitM a (Symbol, SortedReft) 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

Defunc (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

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

Defunc (Symbol, SortedReft) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

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.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "S" PrefixI True) (S1 (MetaSel (Just "_symbolId") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Id) :*: (S1 (MetaSel (Just "symbolRaw") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Text) :*: S1 (MetaSel (Just "symbolEncoded") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Text))))
type Uninterned Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

newtype Description 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
Symbolic String Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: String -> Symbol Source #

Symbolic Text Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Text -> Symbol Source #

Symbolic Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol Source #

Symbolic DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic DataCtor 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 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 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

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 :: (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