Grisette.Internal.Core.Data.Symbol

Documentation

data Identifier

Identifier type used for GenSym

The constructor is hidden intentionally. You can construct an identifier by:

• a raw identifier

The following two expressions will refer to the same identifier (the solver won't distinguish them and would assign the same value to them). The user may need to use unique names to avoid unintentional identifier collision.

>>> identifier "a"
a

>>> "a" :: Identifier -- available when OverloadedStrings is enabled
a

• bundle the identifier with some user provided metadata

Identifiers created with different name or different additional information will not be the same.

>>> withMetadata "a" (NumberAtom 1)
a:1

• bundle the calling file location with the identifier to ensure global uniqueness

Identifiers created at different locations will not be the same. The identifiers created at the same location will be the same.

>>> $$(withLocation "a") -- a sample result could be "a:[grisette-file-location <interactive> 18 (4 18)]"
a:[grisette-file-location <interactive>...]

Constructors

Identifier

Fields

• baseIdent :: Text
• metadata :: SExpr

Instances

IsString Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

fromString :: String -> Identifier

Generic Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Associated Types

type Rep Identifier :: Type -> Type

Methods

from :: Identifier -> Rep Identifier x

to :: Rep Identifier x -> Identifier

Show Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

showsPrec :: Int -> Identifier -> ShowS

show :: Identifier -> String

showList :: [Identifier] -> ShowS

Binary Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Identifier -> Put

get :: Get Identifier

putList :: [Identifier] -> Put

Serial Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

serialize :: MonadPut m => Identifier -> m ()

deserialize :: MonadGet m => m Identifier

Serialize Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Putter Identifier

get :: Get Identifier

NFData Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

rnf :: Identifier -> ()

Eq Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

(==) :: Identifier -> Identifier -> Bool

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

Ord Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

compare :: Identifier -> Identifier -> Ordering

(<) :: Identifier -> Identifier -> Bool

(<=) :: Identifier -> Identifier -> Bool

(>) :: Identifier -> Identifier -> Bool

(>=) :: Identifier -> Identifier -> Bool

max :: Identifier -> Identifier -> Identifier

min :: Identifier -> Identifier -> Identifier

PPrint Identifier

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: Identifier -> Doc ann

pformatPrec :: Int -> Identifier -> Doc ann

pformatList :: [Identifier] -> Doc ann

Hashable Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

hashWithSalt :: Int -> Identifier -> Int

hash :: Identifier -> Int

Lift Identifier

Defined in Grisette.Internal.Core.Data.Symbol

Methods

lift :: Quote m => Identifier -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Identifier -> Code m Identifier

type Rep Identifier

Defined in Grisette.Internal.Core.Data.Symbol

type Rep Identifier = D1 ('MetaData "Identifier" "Grisette.Internal.Core.Data.Symbol" "grisette-0.11.0.0-En6Ko5xIwnQLAUQ39GJ2kN" 'False) (C1 ('MetaCons "Identifier" 'PrefixI 'True) (S1 ('MetaSel ('Just "baseIdent") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "metadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SExpr)))

identifier :: Text -> Identifier

Simple identifier. The same identifier refers to the same symbolic variable in the whole program.

The user may need to use unique identifiers to avoid unintentional identifier collision.

withMetadata :: Text -> SExpr -> Identifier

Identifier with extra metadata.

The same identifier with the same metadata refers to the same symbolic variable in the whole program.

The user may need to use unique identifiers or additional metadata to avoid unintentional identifier collision.

withLocation :: Text -> SpliceQ Identifier

Identifier with the file location.

mapMetadata :: (SExpr -> SExpr) -> Identifier -> Identifier

Modify the metadata of an identifier.

uniqueIdentifier :: Text -> IO Identifier

Get a globally unique identifier within the IO monad.

data Symbol where

Symbol types for a symbolic variable.

The symbols can be indexed with an integer.

Constructors

SimpleSymbol :: Identifier -> Symbol

IndexedSymbol :: Identifier -> Int -> Symbol

Instances

IsString Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

fromString :: String -> Symbol

Generic Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Associated Types

type Rep Symbol :: Type -> Type

Methods

from :: Symbol -> Rep Symbol x

to :: Rep Symbol x -> Symbol

Show Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

Binary Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Symbol -> Put

get :: Get Symbol

putList :: [Symbol] -> Put

Serial Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

serialize :: MonadPut m => Symbol -> m ()

deserialize :: MonadGet m => m Symbol

Serialize Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Putter Symbol

get :: Get Symbol

NFData Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

rnf :: Symbol -> ()

Eq Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

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

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

Ord Symbol

Defined in Grisette.Internal.Core.Data.Symbol

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

PPrint Symbol

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: Symbol -> Doc ann

pformatPrec :: Int -> Symbol -> Doc ann

pformatList :: [Symbol] -> Doc ann

Hashable Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

hashWithSalt :: Int -> Symbol -> Int

hash :: Symbol -> Int

Lift Symbol

Defined in Grisette.Internal.Core.Data.Symbol

Methods

lift :: Quote m => Symbol -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Symbol -> Code m Symbol

type Rep Symbol

Defined in Grisette.Internal.Core.Data.Symbol

type Rep Symbol = D1 ('MetaData "Symbol" "Grisette.Internal.Core.Data.Symbol" "grisette-0.11.0.0-En6Ko5xIwnQLAUQ39GJ2kN" 'False) (C1 ('MetaCons "SimpleSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier)) :+: C1 ('MetaCons "IndexedSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

simple :: Identifier -> Symbol

Create a simple symbol.

indexed :: Identifier -> Int -> Symbol

Create an indexed symbol.

symbolIdentifier :: Symbol -> Identifier

Get the identifier of a symbol.

mapIdentifier :: (Identifier -> Identifier) -> Symbol -> Symbol

Modify the identifier of a symbol.