| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Names
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
- 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
- isFixKey :: Text -> Bool
- 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
- nonSymbol :: Symbol
- vvCon :: Symbol
- tidySymbol :: Symbol -> Symbol
- unKArgSymbol :: 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
- appendSymbolText :: Symbol -> Text -> Text
- hvarArgSymbol :: Symbol -> Int -> Symbol
- litSymbol :: Symbol -> Symbol
- bindSymbol :: Integer -> 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
- boolLConName :: Symbol
- funConName :: Symbol
- listConName :: Symbol
- listLConName :: Symbol
- setConName :: Symbol
- mapConName :: Symbol
- bagConName :: Symbol
- arrayConName :: Symbol
- strConName :: IsString a => a
- charConName :: IsString a => a
- nilName :: Symbol
- consName :: Symbol
- vvName :: Symbol
- sizeName :: Symbol
- bitVecName :: Symbol
- intbv32Name :: Symbol
- intbv64Name :: Symbol
- bv32intName :: Symbol
- bv64intName :: Symbol
- propConName :: Symbol
- isPrim :: Symbol -> Bool
- prims :: HashSet Symbol
- mulFuncName :: Symbol
- divFuncName :: Symbol
- setToIntName :: Symbol
- bitVecToIntName :: Symbol
- mapToIntName :: Symbol
- bagToIntName :: 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
- etaExpSymbol :: Int -> Symbol
Symbols
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
class Symbolic a where Source #
Values that can be viewed as Symbols
Instances
| Symbolic 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 DataCtor Source # | |
| Symbolic DataDecl Source # | |
| Symbolic DataField Source # | |
| Symbolic FTycon Source # | |
| Symbolic Text Source # | |
| Symbolic String Source # | |
| Symbolic a => Symbolic (Located a) Source # | |
type LocSymbol = Located Symbol Source #
Located Symbols -----------------------------------------------------
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 #
isNonSymbol :: Symbol -> Bool Source #
isLitSymbol :: Symbol -> Bool Source #
isTestSymbol :: Symbol -> Bool Source #
isNontrivialVV :: Symbol -> Bool Source #
Destructors
prefixOfSym :: Symbol -> Symbol Source #
suffixOfSym :: Symbol -> Symbol Source #
dropPrefixOfSym :: Symbol -> Symbol Source #
Transforms
tidySymbol :: Symbol -> Symbol Source #
tidySymbol is used to prettify the names of parameters of kvars appearing in solutions.(*)
For example, if you have a kvar $k0 with two parameters, you may have a solution that looks like
0 < lq_karg$nnf_arg$##k0
where we know it is a kvar-arg because of the
- kArgPrefix (lq_arg)
- hvarArgPrefix (nnf_arg)
- k0 the name of the kvar
- `0` the parameter index
- k0 again (IDK why?!)
all of which are separated by ##
So tidySymbol tests if indeed it is a kArgPrefix-ed symbol and if so converts
`lq_karg$nnf_arg$##k0` ----> `$k0##0`
unKArgSymbol :: Symbol -> Symbol Source #
unKArgSymbol is like tidySymbol (see comment below) except it
(a) *removes* the argument-index, and
(b) *preserves* the nnf_arg (without replacing it with $)
For example `unKArgSymbol lq_karg$nnf_arg$##k0` ---> `nnf_arg##k0`
Widely used prefixes
tempPrefix :: Symbol Source #
Creating Symbols
dummySymbol :: Symbol Source #
gradIntSymbol :: Integer -> Symbol Source #
Wrapping Symbols
bindSymbol :: Integer -> Symbol Source #
Used to define functions corresponding to binding predicates
The integer is the BindId.
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
preludeName :: Symbol Source #
boolConName :: Symbol Source #
funConName :: Symbol Source #
listConName :: Symbol Source #
setConName :: Symbol Source #
mapConName :: Symbol Source #
bagConName :: Symbol Source #
strConName :: IsString a => a Source #
charConName :: IsString a => a Source #
bitVecName :: Symbol Source #
intbv32Name :: Symbol Source #
intbv64Name :: Symbol Source #
bv32intName :: Symbol Source #
bv64intName :: Symbol Source #
propConName :: Symbol Source #
mulFuncName :: Symbol Source #
divFuncName :: Symbol Source #
Casting function names
boolToIntName :: IsString a => a Source #
tyCastName :: 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 #
coerceName :: Symbol Source #
lambdaName :: Symbol Source #
lamArgSymbol :: Int -> Symbol Source #
isLamArgSymbol :: Symbol -> Bool Source #
etaExpSymbol :: Int -> Symbol Source #
Orphan instances
| Data InternedText Source # | 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 Source # | |
Associated Types type Rep InternedText :: Type -> Type # | |
| Fixpoint Text Source # | |