Grisette.Core.Data.FileLocation

Symbolic constant generation with location

data FileLocation

Constructors

FileLocation

Fields

• locPath :: String
• locLineno :: Int
• locSpan :: (Int, Int)

Instances

Generic FileLocation

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

Defined in Grisette.Core.Data.FileLocation

Methods

showsPrec :: Int -> FileLocation -> ShowS

show :: FileLocation -> String

showList :: [FileLocation] -> ShowS

NFData FileLocation

Defined in Grisette.Core.Data.FileLocation

Methods

rnf :: FileLocation -> ()

Eq FileLocation

Defined in Grisette.Core.Data.FileLocation

Methods

(==) :: FileLocation -> FileLocation -> Bool

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

Ord FileLocation

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

Defined in Grisette.Core.Data.FileLocation

Methods

hashWithSalt :: Int -> FileLocation -> Int

hash :: FileLocation -> Int

Lift FileLocation

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

Defined in Grisette.Core.Data.FileLocation

type Rep FileLocation = D1 ('MetaData "FileLocation" "Grisette.Core.Data.FileLocation" "grisette-0.3.0.0-D2Nbhnc0iuRKig0VAC9Xli" '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

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

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

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.