Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.Core.Data.Symbol

Description

Synopsis

data Identifier = Identifier {
- baseIdent :: Text
- metadata :: SExpr
}
identifier :: Text -> Identifier
withMetadata :: AsMetadata a => Text -> a -> Identifier
withLocation :: Text -> SpliceQ Identifier
mapMetadata :: AsMetadata a => (SExpr -> a) -> Identifier -> Identifier
uniqueIdentifier :: Text -> IO Identifier
data Symbol where
- SimpleSymbol :: Identifier -> Symbol
- IndexedSymbol :: Identifier -> Int -> Symbol
simple :: Identifier -> Symbol
indexed :: Identifier -> Int -> Symbol
symbolIdentifier :: Symbol -> Identifier
mapIdentifier :: (Identifier -> Identifier) -> Symbol -> Symbol
class AsMetadata a where
- asMetadata :: a -> SExpr
- fromMetadata :: SExpr -> Maybe a
pattern Metadata :: AsMetadata a => a -> SExpr

Documentation

data Identifier Source #

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

Instances details

Binary Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Identifier -> Put #

get :: Get Identifier #

putList :: [Identifier] -> Put #

Serial Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

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

deserialize :: MonadGet m => m Identifier #

Serialize Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Putter Identifier #

get :: Get Identifier #

NFData Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

rnf :: Identifier -> () #

IsString Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

fromString :: String -> Identifier #

Generic Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Associated Types

type Rep Identifier

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

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

Methods

from :: Identifier -> Rep Identifier x #

to :: Rep Identifier x -> Identifier #

Show Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

showsPrec :: Int -> Identifier -> ShowS #

show :: Identifier -> String #

showList :: [Identifier] -> ShowS #

Eq Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

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

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

Ord Identifier Source #

Instance details

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 Source #

Instance details

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

Methods

pformat :: Identifier -> Doc ann Source #

pformatPrec :: Int -> Identifier -> Doc ann Source #

pformatList :: [Identifier] -> Doc ann Source #

Hashable Identifier Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

hashWithSalt :: Int -> Identifier -> Int #

hash :: Identifier -> Int #

Lift Identifier Source #

Instance details

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 Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

type Rep Identifier = D1 ('MetaData "Identifier" "Grisette.Internal.Core.Data.Symbol" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" '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 Source #

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 :: AsMetadata a => Text -> a -> Identifier Source #

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 Source #

Identifier with the file location.

mapMetadata :: AsMetadata a => (SExpr -> a) -> Identifier -> Identifier Source #

Modify the metadata of an identifier.

uniqueIdentifier :: Text -> IO Identifier Source #

Get a globally unique identifier within the IO monad.

data Symbol where Source #

Symbol types for a symbolic variable.

The symbols can be indexed with an integer.

Constructors

SimpleSymbol :: Identifier -> Symbol
IndexedSymbol :: Identifier -> Int -> Symbol

Instances

Instances details

Binary Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Symbol -> Put #

get :: Get Symbol #

putList :: [Symbol] -> Put #

Serial Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

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

deserialize :: MonadGet m => m Symbol #

Serialize Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

put :: Putter Symbol #

get :: Get Symbol #

NFData Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

rnf :: Symbol -> () #

IsString Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

fromString :: String -> Symbol #

Generic Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Associated Types

type Rep Symbol

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

type Rep Symbol = D1 ('MetaData "Symbol" "Grisette.Internal.Core.Data.Symbol" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" '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)))

Methods

from :: Symbol -> Rep Symbol x #

to :: Rep Symbol x -> Symbol #

Show Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

showsPrec :: Int -> Symbol -> ShowS #

show :: Symbol -> String #

showList :: [Symbol] -> ShowS #

Eq Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

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

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

Ord Symbol Source #

Instance details

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 Source #

Instance details

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

Methods

pformat :: Symbol -> Doc ann Source #

pformatPrec :: Int -> Symbol -> Doc ann Source #

pformatList :: [Symbol] -> Doc ann Source #

Hashable Symbol Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

Methods

hashWithSalt :: Int -> Symbol -> Int #

hash :: Symbol -> Int #

Lift Symbol Source #

Instance details

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 Source #

Instance details

Defined in Grisette.Internal.Core.Data.Symbol

type Rep Symbol = D1 ('MetaData "Symbol" "Grisette.Internal.Core.Data.Symbol" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" '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 Source #

Create a simple symbol.

indexed :: Identifier -> Int -> Symbol Source #

Create an indexed symbol.

symbolIdentifier :: Symbol -> Identifier Source #

Get the identifier of a symbol.

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

Modify the identifier of a symbol.

class AsMetadata a where Source #

A type class for embedding a type into a metadata represented as an S-expression.

Methods

asMetadata :: a -> SExpr Source #

fromMetadata :: SExpr -> Maybe a Source #

Instances

Instances details

AsMetadata SExpr Source #
Instance details Defined in Grisette.Internal.Core.Data.Symbol Methods asMetadata :: SExpr -> SExpr Source # fromMetadata :: SExpr -> Maybe SExpr Source #

pattern Metadata :: AsMetadata a => a -> SExpr Source #

A pattern for extracting a value from a metadata represented as an S-expression.