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

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 #
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 #
Methods showsPrec :: Int -> Symbol -> ShowS # show :: Symbol -> String # showList :: [Symbol] -> ShowS #
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 #
Methods mempty :: BindEnv # mappend :: BindEnv -> BindEnv -> BindEnv # mconcat :: [BindEnv] -> 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 #
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 #
Methods unintern :: Symbol -> Uninterned Symbol #
PPrint Symbol Source #
Methods pprintTidy :: Tidy -> Symbol -> Doc Source # pprintPrec :: Int -> Tidy -> Symbol -> Doc Source #
Fixpoint Symbol Source #
Methods toFix :: Symbol -> Doc Source # simplify :: Symbol -> Symbol Source #
Fixpoint BindEnv Source #
Methods toFix :: BindEnv -> Doc Source # simplify :: BindEnv -> 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 #
Methods rr :: String -> Symbol Source # rr' :: String -> String -> Symbol Source #
SymConsts BindEnv Source #
Methods symConsts :: BindEnv -> [SymConst] Source #
Visitable BindEnv Source #
Methods visit :: Monoid a => Visitor a c -> c -> BindEnv -> VisitM a BindEnv Source #
Elaborate BindEnv Source #
Methods elaborate :: String -> SymEnv -> BindEnv -> BindEnv Source #
Gradual BindEnv Source #
Methods gsubst :: GSol -> BindEnv -> BindEnv Source #
Defunc BindEnv Source #
Methods defunc :: BindEnv -> DF BindEnv Source #
Eq (Description Symbol) Source #
Methods (==) :: Description Symbol -> Description Symbol -> Bool # (/=) :: Description Symbol -> Description Symbol -> Bool #
Hashable (Description Symbol) Source #
Methods hashWithSalt :: Int -> Description Symbol -> Int # hash :: Description Symbol -> Int #
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 #
Methods defunc :: (Symbol, SortedReft) -> DF (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 #
type Uninterned Symbol = Text
data Description Symbol Source #
data Description Symbol = DT Text

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 #
Methods symbol :: DataDecl -> Symbol Source #
Symbolic DataCtor Source #
Methods symbol :: DataCtor -> Symbol Source #
Symbolic DataField Source #
Methods symbol :: DataField -> Symbol 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.
Methods symbol :: SymConst -> Symbol Source #
Symbolic a => Symbolic (Located a) Source #
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 #

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

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 #

nilName :: Symbol Source #

consName :: Symbol Source #

vvName :: Symbol Source #

size32Name :: Symbol Source #

size64Name :: Symbol Source #

bitVecName :: Symbol Source #

bvAndName :: Symbol Source #

bvOrName :: Symbol Source #

prims :: [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 #

lambdaName :: Symbol Source #

lamArgSymbol :: Int -> Symbol Source #

isLamArgSymbol :: Symbol -> Bool Source #

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