Language.Fixpoint.Types.Names

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.

Symbols

data Symbol

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

Data Symbol

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

Defined in Language.Fixpoint.Types.Names

Methods

fromString :: String -> Symbol

Generic Symbol

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

Defined in Language.Fixpoint.Types.Names

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

Binary Symbol

Defined in Language.Fixpoint.Types.Names

Methods

put :: Symbol -> Put

get :: Get Symbol

putList :: [Symbol] -> Put

NFData Symbol

Defined in Language.Fixpoint.Types.Names

Methods

rnf :: Symbol -> ()

Eq Symbol

Defined in Language.Fixpoint.Types.Names

Methods

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

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

Ord Symbol

Defined in Language.Fixpoint.Types.Names

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

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

(>) :: Symbol -> Symbol -> Bool

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

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Hashable Symbol

Defined in Language.Fixpoint.Types.Names

Methods

hashWithSalt :: Int -> Symbol -> Int

hash :: Symbol -> Int

Interned Symbol

Defined in Language.Fixpoint.Types.Names

Associated Types

data Description Symbol

type Uninterned Symbol

Methods

describe :: Uninterned Symbol -> Description Symbol

identify :: Id -> Uninterned Symbol -> Symbol

seedIdentity :: p Symbol -> Id

cacheWidth :: p Symbol -> Int

modifyAdvice :: IO Symbol -> IO Symbol

cache :: Cache Symbol

Uninternable Symbol

Defined in Language.Fixpoint.Types.Names

Methods

unintern :: Symbol -> Uninterned Symbol

Inputable Symbol

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Symbol

rr' :: String -> String -> Symbol

SMTLIB2 LocSymbol

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> LocSymbol -> Builder

SMTLIB2 Symbol

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> Symbol -> Builder

Symbolic Symbol

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol

Fixpoint Symbol

NOTE: SymbolText

Use symbolSafeText if you want it to machine-readable, but symbolText if you want it to be human-readable.

Defined in Language.Fixpoint.Types.Names

Methods

toFix :: Symbol -> Doc

simplify :: Symbol -> Symbol

PPrint Symbol

Defined in Language.Fixpoint.Types.Names

Methods

pprintTidy :: Tidy -> Symbol -> Doc

pprintPrec :: Int -> Tidy -> Symbol -> Doc

Expression Symbol

The symbol may be an encoding of a SymConst.

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Symbol -> Expr

Predicate Symbol

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr

Subable Symbol

Defined in Language.Fixpoint.Types.Substitutions

Methods

syms :: Symbol -> [Symbol]

substa :: (Symbol -> Symbol) -> Symbol -> Symbol

substf :: (Symbol -> Expr) -> Symbol -> Symbol

subst :: Subst -> Symbol -> Symbol

subst1 :: Symbol -> (Symbol, Expr) -> Symbol

Store Symbol

Defined in Language.Fixpoint.Types.Names

Methods

size :: Size Symbol

poke :: Symbol -> Poke ()

peek :: Peek Symbol

Monoid (BindEnv a)

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)

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)

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv a -> ()

Eq (Description Symbol)

Defined in Language.Fixpoint.Types.Names

Methods

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

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

Hashable (Description Symbol)

Defined in Language.Fixpoint.Types.Names

Methods

hashWithSalt :: Int -> Description Symbol -> Int

hash :: Description Symbol -> Int

Defunc (BindEnv a)

Defined in Language.Fixpoint.Defunctionalize

Methods

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

Loc a => Elaborate (BindEnv a)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> BindEnv a -> BindEnv a

Gradual (BindEnv a)

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> BindEnv a -> BindEnv a

Fixpoint (BindEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: BindEnv a -> Doc

simplify :: BindEnv a -> BindEnv a

SymConsts (BindEnv a)

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv a -> [SymConst]

Visitable (BindEnv a)

Defined in Language.Fixpoint.Types.Visitor

Methods

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

Store a => Store (BindEnv a)

Defined in Language.Fixpoint.Types.Environments

Methods

size :: Size (BindEnv a)

poke :: BindEnv a -> Poke ()

peek :: Peek (BindEnv a)

Defunc (Symbol, SortedReft)

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft)

Defunc (Symbol, Sort)

Defined in Language.Fixpoint.Defunctionalize

Methods

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

SMTLIB2 (Symbol, Sort)

Defined in Language.Fixpoint.Smt.Serialize

Methods

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

Elaborate (Symbol, Sort)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> (Symbol, Sort) -> (Symbol, Sort)

Expression (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr

Visitable (Symbol, SortedReft, a)

Defined in Language.Fixpoint.Types.Visitor

Methods

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

type Rep Symbol

Defined in Language.Fixpoint.Types.Names

type Rep Symbol = D1 ('MetaData "Symbol" "Language.Fixpoint.Types.Names" "liquid-fixpoint-0.9.0.2.1-GsxNcg91pufGtKM5ikXQaF" '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

Defined in Language.Fixpoint.Types.Names

newtype Description Symbol = DT Text

type Uninterned Symbol

Defined in Language.Fixpoint.Types.Names

type Uninterned Symbol = Text

class Symbolic a where

Values that can be viewed as Symbols

Methods

symbol :: a -> Symbol

Instances

Symbolic Symbol

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol

Symbolic SymConst

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

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

Defined in Language.Fixpoint.Types.Refinements

Methods

symbol :: SymConst -> Symbol

Symbolic DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataCtor -> Symbol

Symbolic DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataDecl -> Symbol

Symbolic DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataField -> Symbol

Symbolic FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: FTycon -> Symbol

Symbolic Text

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Text -> Symbol

Symbolic String

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: String -> Symbol

Symbolic a => Symbolic (Located a)

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Located a -> Symbol

type LocSymbol = Located Symbol

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

type LocText = Located Text

symbolicString :: Symbolic a => a -> String

Conversion to/from Text

symbolSafeText :: Symbol -> SafeText

symbolSafeString :: Symbol -> String

symbolText :: Symbol -> Text

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

symbolString :: Symbol -> String

symbolBuilder :: Symbolic a => a -> Builder

buildMany :: [Builder] -> Builder

isPrefixOfSym :: Symbol -> Symbol -> Bool

isSuffixOfSym :: Symbol -> Symbol -> Bool

isNonSymbol :: Symbol -> Bool

isLitSymbol :: Symbol -> Bool

isTestSymbol :: Symbol -> Bool

isNontrivialVV :: Symbol -> Bool

isDummy :: Symbolic a => a -> Bool

isFixKey :: Text -> Bool

Destructors

prefixOfSym :: Symbol -> Symbol

suffixOfSym :: Symbol -> Symbol

stripPrefix :: Symbol -> Symbol -> Maybe Symbol

stripSuffix :: Symbol -> Symbol -> Maybe Symbol

consSym :: Char -> Symbol -> Symbol

unconsSym :: Symbol -> Maybe (Char, Symbol)

dropSym :: Int -> Symbol -> Symbol

dropPrefixOfSym :: Symbol -> Symbol

headSym :: Symbol -> Char

lengthSym :: Symbol -> Int

Transforms

nonSymbol :: Symbol

vvCon :: Symbol

tidySymbol :: Symbol -> Symbol

Widely used prefixes

anfPrefix :: Symbol

tempPrefix :: Symbol

vv :: Maybe Integer -> Symbol

symChars :: HashSet Char

Creating Symbols

dummySymbol :: Symbol

intSymbol :: Show a => Symbol -> a -> Symbol

tempSymbol :: Symbol -> Integer -> Symbol

gradIntSymbol :: Integer -> Symbol

appendSymbolText :: Symbol -> Text -> Text

Wrapping Symbols

litSymbol :: Symbol -> Symbol

bindSymbol :: Integer -> Symbol

Used to define functions corresponding to binding predicates

The integer is the BindId.

testSymbol :: Symbol -> Symbol

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

renameSymbol :: Symbol -> Int -> Symbol

kArgSymbol :: Symbol -> Symbol -> Symbol

existSymbol :: Symbol -> Integer -> Symbol

suffixSymbol :: Symbol -> Symbol -> Symbol

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

mappendSym :: Symbol -> Symbol -> Symbol

Unwrapping Symbols

unLitSymbol :: Symbol -> Maybe Symbol

Hardwired global names

dummyName :: Symbol

preludeName :: Symbol

boolConName :: Symbol

funConName :: Symbol

listConName :: Symbol

listLConName :: Symbol

tupConName :: Symbol

setConName :: Symbol

mapConName :: Symbol

strConName :: IsString a => a

charConName :: IsString a => a

nilName :: Symbol

consName :: Symbol

vvName :: Symbol

size32Name :: Symbol

size64Name :: Symbol

bitVecName :: Symbol

bvAndName :: Symbol

bvOrName :: Symbol

propConName :: Symbol

isPrim :: Symbol -> Bool

prims :: HashSet Symbol

mulFuncName :: Symbol

divFuncName :: Symbol

Casting function names

setToIntName :: Symbol

bitVecToIntName :: Symbol

mapToIntName :: Symbol

boolToIntName :: IsString a => a

realToIntName :: Symbol

toIntName :: Symbol

tyCastName :: Symbol

setApplyName :: Int -> Symbol

bitVecApplyName :: Int -> Symbol

mapApplyName :: Int -> Symbol

boolApplyName :: Int -> Symbol

realApplyName :: Int -> Symbol

intApplyName :: Int -> Symbol

applyName :: Symbol

coerceName :: Symbol

lambdaName :: Symbol

lamArgSymbol :: Int -> Symbol

isLamArgSymbol :: Symbol -> Bool

Orphan instances

Data InternedText

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

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

Associated Types

type Rep InternedText :: Type -> Type

Methods

from :: InternedText -> Rep InternedText x

to :: Rep InternedText x -> InternedText

Fixpoint Text

Methods

toFix :: Text -> Doc

simplify :: Text -> Text