liquid-fixpoint-0.7.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 # 

Methods

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

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

Data Symbol Source # 

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 # 
Show Symbol Source # 
IsString Symbol Source # 

Methods

fromString :: String -> Symbol #

Generic Symbol Source # 

Associated Types

type Rep Symbol :: * -> * #

Methods

from :: Symbol -> Rep Symbol x #

to :: Rep Symbol x -> Symbol #

Monoid BindEnv # 
Binary Symbol Source # 

Methods

put :: Symbol -> Put #

get :: Get Symbol #

putList :: [Symbol] -> Put #

Binary BindEnv # 

Methods

put :: BindEnv -> Put #

get :: Get BindEnv #

putList :: [BindEnv] -> Put #

NFData Symbol Source # 

Methods

rnf :: Symbol -> () #

NFData BindEnv # 

Methods

rnf :: BindEnv -> () #

Hashable Symbol Source # 

Methods

hashWithSalt :: Int -> Symbol -> Int #

hash :: Symbol -> Int #

Interned Symbol Source # 
Uninternable Symbol Source # 
PPrint Symbol Source # 
Fixpoint Symbol Source # 
Fixpoint BindEnv Source # 
Symbolic Symbol Source # 

Methods

symbol :: Symbol -> Symbol Source #

Predicate Symbol Source # 

Methods

prop :: Symbol -> Expr Source #

Expression Symbol Source #

The symbol may be an encoding of a SymConst.

Methods

expr :: Symbol -> Expr Source #

Inputable Symbol Source # 
SymConsts BindEnv Source # 
Visitable BindEnv Source # 

Methods

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

Elaborate BindEnv Source # 
Gradual BindEnv Source # 

Methods

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

Defunc BindEnv Source # 

Methods

defunc :: BindEnv -> DF BindEnv Source #

Eq (Description Symbol) Source # 
Hashable (Description Symbol) Source # 
Visitable (Symbol, SortedReft) Source # 

Methods

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

Elaborate (Symbol, Sort) Source # 

Methods

elaborate :: String -> SymEnv -> (Symbol, Sort) -> (Symbol, Sort) Source #

Defunc (Symbol, Sort) Source # 

Methods

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

Defunc (Symbol, SortedReft) Source # 
type Rep Symbol Source # 
type Rep Symbol = D1 (MetaData "Symbol" "Language.Fixpoint.Types.Names" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "S" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "_symbolId") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Id)) ((:*:) (S1 (MetaSel (Just Symbol "symbolRaw") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Text)) (S1 (MetaSel (Just Symbol "symbolEncoded") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Text)))))
type Uninterned Symbol Source # 
data Description Symbol Source # 

class Symbolic a where Source #

Values that can be viewed as Symbols

Minimal complete definition

symbol

Methods

symbol :: a -> Symbol Source #

Instances

Symbolic Text Source # 

Methods

symbol :: Text -> Symbol Source #

Symbolic String Source # 

Methods

symbol :: String -> Symbol Source #

Symbolic Symbol Source # 

Methods

symbol :: Symbol -> Symbol Source #

Symbolic DataDecl Source # 
Symbolic DataCtor Source # 
Symbolic DataField Source # 
Symbolic FTycon Source # 

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.

Symbolic a => Symbolic (Located a) Source # 

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 # 

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 # 

Associated Types

type Rep InternedText :: * -> * #

Fixpoint Text Source #