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

Grisette.Core.Data.FileLocation

Contents

Symbolic constant generation with location

Description

Synopsis

data FileLocation = FileLocation {
- locPath :: String
- locLineno :: Int
- locSpan :: (Int, Int)
}
nameWithLoc :: String -> SpliceQ FreshIdent
slocsym :: Solvable c s => String -> SpliceQ s
ilocsym :: Solvable c s => String -> Int -> SpliceQ s

Symbolic constant generation with location

data FileLocation Source #

Constructors

FileLocation
Fields locPath :: String locLineno :: Int locSpan :: (Int, Int)

Instances

Instances details

Generic FileLocation Source #
Instance details Defined in Grisette.Core.Data.FileLocation Associated Types type Rep FileLocation :: Type -> Type # Methods from :: FileLocation -> Rep FileLocation x # to :: Rep FileLocation x -> FileLocation #
Show FileLocation Source #
Instance details Defined in Grisette.Core.Data.FileLocation Methods showsPrec :: Int -> FileLocation -> ShowS # show :: FileLocation -> String # showList :: [FileLocation] -> ShowS #
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 Methods (==) :: FileLocation -> FileLocation -> Bool # (/=) :: FileLocation -> FileLocation -> Bool #
Ord FileLocation Source #
Instance details Defined in Grisette.Core.Data.FileLocation Methods compare :: FileLocation -> FileLocation -> Ordering # (<) :: FileLocation -> FileLocation -> Bool # (<=) :: FileLocation -> FileLocation -> Bool # (>) :: FileLocation -> FileLocation -> Bool # (>=) :: FileLocation -> FileLocation -> Bool # max :: FileLocation -> FileLocation -> FileLocation # min :: FileLocation -> FileLocation -> FileLocation #
Hashable FileLocation Source #
Instance details Defined in Grisette.Core.Data.FileLocation Methods hashWithSalt :: Int -> FileLocation -> Int # hash :: FileLocation -> Int #
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.