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

Eq Symbol

Defined in Language.Fixpoint.Types.Names

Methods

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

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

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

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

Show Symbol

Defined in Language.Fixpoint.Types.Names

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

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

Semigroup BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

(<>) :: BindEnv -> BindEnv -> BindEnv

sconcat :: NonEmpty BindEnv -> BindEnv

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

Monoid BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

mempty :: BindEnv

mappend :: BindEnv -> BindEnv -> BindEnv

mconcat :: [BindEnv] -> BindEnv

Binary Symbol

Defined in Language.Fixpoint.Types.Names

Methods

put :: Symbol -> Put

get :: Get Symbol

putList :: [Symbol] -> Put

Binary BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

put :: BindEnv -> Put

get :: Get BindEnv

putList :: [BindEnv] -> Put

NFData Symbol

Defined in Language.Fixpoint.Types.Names

Methods

rnf :: Symbol -> ()

NFData BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

rnf :: BindEnv -> ()

Hashable Symbol

Defined in Language.Fixpoint.Types.Names

Methods

hashWithSalt :: Int -> Symbol -> Int

hash :: Symbol -> Int

PPrint Symbol

Defined in Language.Fixpoint.Types.Names

Methods

pprintTidy :: Tidy -> Symbol -> Doc

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

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

Fixpoint BindEnv

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: BindEnv -> Doc

simplify :: BindEnv -> BindEnv

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

Symbolic Symbol

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol

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

Predicate Symbol

Defined in Language.Fixpoint.Types.Refinements

Methods

prop :: Symbol -> Expr

Expression Symbol

The symbol may be an encoding of a SymConst.

Defined in Language.Fixpoint.Types.Refinements

Methods

expr :: Symbol -> Expr

SymConsts BindEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: BindEnv -> [SymConst]

Visitable BindEnv

Defined in Language.Fixpoint.Types.Visitor

Methods

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

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

Elaborate BindEnv

Defined in Language.Fixpoint.SortCheck

Methods

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

Inputable Symbol

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Symbol

rr' :: String -> String -> Symbol

Gradual BindEnv

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> BindEnv -> BindEnv

Defunc BindEnv

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: BindEnv -> DF BindEnv

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

Expression (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Substitutions

Methods

expr :: (Symbol, SortedReft) -> Expr

Visitable (Symbol, SortedReft)

Defined in Language.Fixpoint.Types.Visitor

Methods

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

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)

Defunc (Symbol, Sort)

Defined in Language.Fixpoint.Defunctionalize

Methods

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

Defunc (Symbol, SortedReft)

Defined in Language.Fixpoint.Defunctionalize

Methods

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

type Rep Symbol

Defined in Language.Fixpoint.Types.Names

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

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 String

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: String -> Symbol

Symbolic Text

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Text -> Symbol

Symbolic Symbol

Defined in Language.Fixpoint.Types.Names

Methods

symbol :: Symbol -> Symbol

Symbolic DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataDecl -> Symbol

Symbolic DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataCtor -> 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 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 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

Destructors

stripPrefix :: Symbol -> Symbol -> Maybe Symbol

stripSuffix :: Symbol -> Symbol -> Maybe Symbol

consSym :: Char -> Symbol -> Symbol

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

dropSym :: Int -> 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

Wrapping Symbols

litSymbol :: Symbol -> Symbol

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

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