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

Data Symbol

Ord Symbol

Show Symbol

IsString Symbol

Generic Symbol

Monoid BindEnv

Binary Symbol

Binary BindEnv

NFData Symbol

NFData BindEnv

Hashable Symbol

Interned Symbol

Uninternable Symbol

PPrint Symbol

Fixpoint Symbol

Fixpoint BindEnv

Symbolic Symbol

Predicate Symbol

Expression Symbol

The symbol may be an encoding of a SymConst.

SymConsts BindEnv

Inputable Symbol

Eq (Description Symbol)

Hashable (Description Symbol)

type Rep Symbol

type Uninterned Symbol = Text

data Description Symbol = DT Text

class Symbolic a where

Values that can be viewed as Symbols

Methods

symbol :: a -> Symbol

Instances

Symbolic String

Symbolic Text

Symbolic 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.

Symbolic a => Symbolic (Located a)

type LocSymbol = Located Symbol

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

type LocText = Located Text

Conversion to/from Text

symbolSafeText :: Symbol -> SafeText

symbolSafeString :: Symbol -> String

symbolText :: Symbol -> Text

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

symbolString :: Symbol -> String

isPrefixOfSym :: Symbol -> Symbol -> Bool

isSuffixOfSym :: Symbol -> Symbol -> Bool

isNonSymbol :: Symbol -> Bool

isNontrivialVV :: Symbol -> Bool

isDummy :: Symbolic a => a -> Bool

Destructors

stripPrefix :: 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

Wrapping Symbols

litSymbol :: Symbol -> Symbol

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

Unwrapping Symbols

unLitSymbol :: Symbol -> Maybe Symbol

Hardwired global names

dummyName :: Symbol

preludeName :: Symbol

boolConName :: Symbol

funConName :: Symbol

listConName :: Symbol

listLConName :: Symbol

tupConName :: Symbol

propConName :: Symbol

hpropConName :: Symbol

strConName :: Symbol

nilName :: Symbol

consName :: Symbol

vvName :: Symbol

size32Name :: Symbol

size64Name :: Symbol

bitVecName :: Symbol

bvAndName :: Symbol

bvOrName :: Symbol

prims :: [Symbol]

mulFuncName :: Symbol

divFuncName :: Symbol

Casting function names

setToIntName :: Symbol

bitVecToIntName :: Symbol

mapToIntName :: Symbol

boolToIntName :: Symbol

realToIntName :: Symbol

setApplyName :: Int -> Symbol

bitVecApplyName :: Int -> Symbol

mapApplyName :: Int -> Symbol

boolApplyName :: Int -> Symbol

realApplyName :: Int -> Symbol

intApplyName :: Int -> Symbol