grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.FileLocation

Description

 
Synopsis

Symbolic constant generation with location

data FileLocation Source #

Constructors

FileLocation 

Fields

Instances

Instances details
Generic FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

Associated Types

type Rep FileLocation :: Type -> Type #

Show FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

NFData FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

Methods

rnf :: FileLocation -> () #

Eq FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

Ord FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

Hashable FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

Lift FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

Methods

lift :: Quote m => FileLocation -> m Exp #

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

type Rep FileLocation Source # 
Instance details

Defined in Grisette.Core.Data.FileLocation

type Rep FileLocation = D1 ('MetaData "FileLocation" "Grisette.Core.Data.FileLocation" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'False) (C1 ('MetaCons "FileLocation" 'PrefixI 'True) (S1 ('MetaSel ('Just "locPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "locLineno") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "locSpan") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Int)))))

nameWithLoc :: String -> SpliceQ FreshIdent Source #

Identifier with the current location as extra information.

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

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

slocsym :: Solvable c s => String -> SpliceQ s Source #

Generate simply-named symbolic variables. The file location will be attached to the identifier.

>>> $$(slocsym "a") :: SymBool
a:<interactive>:...

Calling slocsymb with the same name at different location will always generate different symbolic constants. Calling slocsymb at the same location for multiple times will generate the same symbolic constants.

>>> ($$(slocsym "a") :: SymBool) == $$(slocsym "a")
False
>>> let f _ = $$(slocsym "a") :: SymBool
>>> f () == f ()
True

ilocsym :: Solvable c s => String -> Int -> SpliceQ s Source #

Generate indexed symbolic variables. The file location will be attached to identifier.

>>> $$(ilocsym "a" 1) :: SymBool
a@1:<interactive>:...

Calling ilocsymb with the same name and index at different location will always generate different symbolic constants. Calling slocsymb at the same location for multiple times will generate the same symbolic constants.