Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Names

Contents

Symbols
Conversion to/from Text
Destructors
Transforms
Widely used prefixes
Creating Symbols
Wrapping Symbols
Unwrapping Symbols
Hardwired global names
Casting function names
Orphan instances

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

data Symbol
class Symbolic a where
- symbol :: a -> Symbol
type LocSymbol = Located Symbol
type LocText = Located Text
symbolicString :: Symbolic a => a -> String
symbolSafeText :: Symbol -> SafeText
symbolSafeString :: Symbol -> String
symbolText :: Symbol -> Text
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
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
nonSymbol :: Symbol
vvCon :: Symbol
tidySymbol :: Symbol -> Symbol
anfPrefix :: Symbol
tempPrefix :: Symbol
vv :: Maybe Integer -> Symbol
symChars :: HashSet Char
dummySymbol :: Symbol
intSymbol :: Show a => Symbol -> a -> Symbol
tempSymbol :: Symbol -> Integer -> Symbol
gradIntSymbol :: Integer -> Symbol
litSymbol :: Symbol -> Symbol
testSymbol :: Symbol -> Symbol
renameSymbol :: Symbol -> Int -> Symbol
kArgSymbol :: Symbol -> Symbol -> Symbol
existSymbol :: Symbol -> Integer -> Symbol
suffixSymbol :: Symbol -> Symbol -> Symbol
mappendSym :: Symbol -> Symbol -> Symbol
unLitSymbol :: Symbol -> Maybe Symbol
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
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

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

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 :: 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 Source #
Instance details 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 Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
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 Methods (<>) :: BindEnv -> BindEnv -> BindEnv # sconcat :: NonEmpty BindEnv -> BindEnv # stimes :: Integral b => b -> BindEnv -> BindEnv #
Monoid BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods mempty :: BindEnv # mappend :: BindEnv -> BindEnv -> BindEnv # mconcat :: [BindEnv] -> BindEnv #
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
PPrint Symbol Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods pprintTidy :: Tidy -> Symbol -> Doc Source # pprintPrec :: Int -> Tidy -> Symbol -> Doc 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 Methods toFix :: Symbol -> Doc Source # simplify :: Symbol -> Symbol Source #
Fixpoint BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: BindEnv -> Doc Source # simplify :: BindEnv -> BindEnv Source #
Interned Symbol Source #
Instance details 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 Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods unintern :: Symbol -> Uninterned Symbol
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 Methods syms :: Symbol -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Symbol -> Symbol Source # substf :: (Symbol -> Expr) -> Symbol -> Symbol Source # subst :: Subst -> Symbol -> Symbol Source # subst1 :: Symbol -> (Symbol, Expr) -> Symbol Source #
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 Methods symConsts :: BindEnv -> [SymConst] Source #
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 Methods smt2 :: SymEnv -> LocSymbol -> Builder Source #
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 Methods elaborate :: Located String -> SymEnv -> BindEnv -> BindEnv Source #
Inputable Symbol Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Symbol Source # rr' :: String -> String -> Symbol Source #
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 Methods (==) :: Description Symbol -> Description Symbol -> Bool # (/=) :: Description Symbol -> Description Symbol -> Bool #
Hashable (Description Symbol) Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods hashWithSalt :: Int -> Description Symbol -> Int hash :: Description Symbol -> Int
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 Methods elaborate :: Located String -> SymEnv -> (Symbol, Sort) -> (Symbol, Sort) Source #
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 Methods defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft) 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.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 Source #
Instance details Defined in Language.Fixpoint.Types.Names newtype Description Symbol = DT Text
type Uninterned Symbol Source #
Instance details Defined in Language.Fixpoint.Types.Names type Uninterned Symbol = Text

class Symbolic a where Source #

Values that can be viewed as Symbols

Methods

symbol :: a -> Symbol Source #

Instances

Instances details

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 Methods symbol :: DataDecl -> Symbol Source #
Symbolic DataCtor Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods symbol :: DataCtor -> Symbol Source #
Symbolic DataField Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods symbol :: DataField -> Symbol Source #
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 Methods symbol :: SymConst -> 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 -----------------------------------------------------

type LocText = Located Text Source #

symbolicString :: Symbolic a => a -> String Source #

Conversion to/from Text

symbolSafeText :: Symbol -> SafeText Source #

symbolSafeString :: Symbol -> String Source #

symbolText :: Symbol -> Text Source #

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

symbolString :: Symbol -> String Source #

symbolBuilder :: Symbolic a => a -> Builder Source #

buildMany :: [Builder] -> Builder Source #

isPrefixOfSym :: Symbol -> Symbol -> Bool Source #

isSuffixOfSym :: Symbol -> Symbol -> Bool Source #

isNonSymbol :: Symbol -> Bool Source #

isLitSymbol :: Symbol -> Bool Source #

isTestSymbol :: Symbol -> Bool Source #

isNontrivialVV :: Symbol -> Bool Source #

isDummy :: Symbolic a => a -> Bool Source #

Destructors

stripPrefix :: Symbol -> Symbol -> Maybe Symbol Source #

stripSuffix :: Symbol -> Symbol -> Maybe Symbol Source #

consSym :: Char -> Symbol -> Symbol Source #

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

dropSym :: Int -> Symbol -> Symbol Source #

headSym :: Symbol -> Char Source #

lengthSym :: Symbol -> Int Source #

Transforms

nonSymbol :: Symbol Source #

vvCon :: Symbol Source #

tidySymbol :: Symbol -> Symbol Source #

Widely used prefixes

anfPrefix :: Symbol Source #

tempPrefix :: Symbol Source #

vv :: Maybe Integer -> Symbol Source #

symChars :: HashSet Char Source #

Creating Symbols

dummySymbol :: Symbol Source #

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

tempSymbol :: Symbol -> Integer -> Symbol Source #

gradIntSymbol :: Integer -> Symbol Source #

Wrapping Symbols

litSymbol :: Symbol -> Symbol Source #

testSymbol :: Symbol -> Symbol Source #

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

renameSymbol :: Symbol -> Int -> Symbol Source #

kArgSymbol :: Symbol -> Symbol -> Symbol Source #

existSymbol :: Symbol -> Integer -> Symbol Source #

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

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

mappendSym :: Symbol -> Symbol -> Symbol Source #

Unwrapping Symbols

unLitSymbol :: Symbol -> Maybe Symbol Source #

Hardwired global names

dummyName :: Symbol Source #

preludeName :: Symbol Source #

boolConName :: Symbol Source #

funConName :: Symbol Source #

listConName :: Symbol Source #

listLConName :: Symbol Source #

tupConName :: Symbol Source #

setConName :: Symbol Source #

mapConName :: Symbol Source #

strConName :: IsString a => a Source #

charConName :: IsString a => a Source #

nilName :: Symbol Source #

consName :: Symbol Source #

vvName :: Symbol Source #

size32Name :: Symbol Source #

size64Name :: Symbol Source #

bitVecName :: Symbol Source #

bvAndName :: Symbol Source #

bvOrName :: Symbol Source #

propConName :: Symbol Source #

isPrim :: Symbol -> Bool Source #

prims :: HashSet Symbol Source #

mulFuncName :: Symbol Source #

divFuncName :: Symbol Source #

Casting function names

setToIntName :: Symbol Source #

bitVecToIntName :: Symbol Source #

mapToIntName :: Symbol Source #

boolToIntName :: IsString a => a Source #

realToIntName :: Symbol Source #

toIntName :: Symbol Source #

setApplyName :: Int -> Symbol Source #

bitVecApplyName :: Int -> Symbol Source #

mapApplyName :: Int -> Symbol Source #

boolApplyName :: Int -> Symbol Source #

realApplyName :: Int -> Symbol Source #

intApplyName :: Int -> Symbol Source #

applyName :: Symbol Source #

coerceName :: Symbol Source #

lambdaName :: Symbol Source #

lamArgSymbol :: Int -> Symbol Source #

isLamArgSymbol :: Symbol -> Bool Source #

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 # Methods from :: InternedText -> Rep InternedText x # to :: Rep InternedText x -> InternedText #
Fixpoint Text Source #
Instance details Methods toFix :: Text -> Doc Source # simplify :: Text -> Text Source #