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	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Core.Data.Symbol

Description

Synopsis

data Identifier where
- Identifier :: Text -> Identifier
- IdentifierWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier
identifier :: Text -> Identifier
withInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier
withLoc :: Identifier -> SpliceQ Identifier
data Symbol where
- SimpleSymbol :: Identifier -> Symbol
- IndexedSymbol :: Identifier -> Int -> Symbol
simple :: Identifier -> Symbol
indexed :: Identifier -> Int -> Symbol

Documentation

data Identifier where 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 information

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

>>> withInfo "a" (1 :: Int)
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.

>>> $$(withLoc "a") -- a sample result could be "a:<interactive>:18:4-18"
a:<interactive>:...

Constructors

Identifier :: Text -> Identifier
IdentifierWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier

Instances

Instances details

IsString Identifier Source #
Instance details Defined in Grisette.Internal.Core.Data.Symbol Methods fromString :: String -> Identifier #
Show Identifier Source #
Instance details Defined in Grisette.Internal.Core.Data.Symbol Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
NFData Identifier Source #
Instance details Defined in Grisette.Internal.Core.Data.Symbol Methods rnf :: Identifier -> () #
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 #
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 #

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.

withInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier Source #

Identifier with extra information.

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

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

withLoc :: Identifier -> SpliceQ Identifier Source #

Identifier with the current location as extra information.

>>> $$(withLoc "a") -- a sample result could be "a:<interactive>:18:4-18"
a:<interactive>:...

The uniqueness is ensured for the call to identifier at different location.

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

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 :: Type -> Type # 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 #
NFData Symbol Source #
Instance details Defined in Grisette.Internal.Core.Data.Symbol Methods rnf :: Symbol -> () #
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 #
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.5.0.1-IKpKourvCOdG0l1QW5fLHa" '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.