A Program is defined as a list of bindings. The bnd is an identifier that determines a unique binder to the var. In practice, these are defined to be Name and Var respectively.

Constructors

Program [GenBinding bnd var]

Instances

(Eq var, Eq bnd) => Eq (GenProgram bnd var) Source #
Methods (==) :: GenProgram bnd var -> GenProgram bnd var -> Bool # (/=) :: GenProgram bnd var -> GenProgram bnd var -> Bool #
(Read var, Read bnd) => Read (GenProgram bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenProgram bnd var) # readList :: ReadS [GenProgram bnd var] # readPrec :: ReadPrec (GenProgram bnd var) # readListPrec :: ReadPrec [GenProgram bnd var] #
(Show var, Show bnd) => Show (GenProgram bnd var) Source #
Methods showsPrec :: Int -> GenProgram bnd var -> ShowS # show :: GenProgram bnd var -> String # showList :: [GenProgram bnd var] -> ShowS #

data NameSpace Source #

Variables, data constructors, type variables, and type constructors.

Constructors

VarNSpace
DataNSpace
TvNSpace
TcClsNSpace

Instances

Eq NameSpace Source #
Methods (==) :: NameSpace -> NameSpace -> Bool # (/=) :: NameSpace -> NameSpace -> Bool #
Ord NameSpace Source #
Methods compare :: NameSpace -> NameSpace -> Ordering # (<) :: NameSpace -> NameSpace -> Bool # (<=) :: NameSpace -> NameSpace -> Bool # (>) :: NameSpace -> NameSpace -> Bool # (>=) :: NameSpace -> NameSpace -> Bool # max :: NameSpace -> NameSpace -> NameSpace # min :: NameSpace -> NameSpace -> NameSpace #
Read NameSpace Source #
Methods readsPrec :: Int -> ReadS NameSpace # readList :: ReadS [NameSpace] # readPrec :: ReadPrec NameSpace # readListPrec :: ReadPrec [NameSpace] #
Show NameSpace Source #
Methods showsPrec :: Int -> NameSpace -> ShowS # show :: NameSpace -> String # showList :: [NameSpace] -> ShowS #

data Name Source #

The occurrence name is defined as a string, with a Maybe module name appearing. The Int denotes a Unique translated from GHC. For instance, in the case of Map.empty, the occurrence name is "empty", while the module name is some variant of Just "Data.Map".

Constructors

Name String (Maybe String) NameSpace Int

Instances

Eq Name Source #
Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source #
Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Read Name Source #
Methods readsPrec :: Int -> ReadS Name # readList :: ReadS [Name] # readPrec :: ReadPrec Name # readListPrec :: ReadPrec [Name] #
Show Name Source #
Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #

data Var Source #

Variables consist of a Name and a Type.

Constructors

Var Name (GenType Name)

Instances

Eq Var Source #
Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Read Var Source #
Methods readsPrec :: Int -> ReadS Var # readList :: ReadS [Var] # readPrec :: ReadPrec Var # readListPrec :: ReadPrec [Var] #
Show Var Source #
Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #

data GenLit bnd var Source #

Literals are largely augmented from the original GHC implementation, with additional annotations to denote BlankAddr for lifting, AddrLit for value deriviation, SymLit for symbolic literals, and SymLitEval to represent symbolic literal evaluation, as literal manipulation functions are defined in the Haskell Prelude, and thus outside of scope for us.

Constructors

MachChar Char (GenType bnd)
MachStr String (GenType bnd)
MachInt Int (GenType bnd)
MachWord Int (GenType bnd)
MachFloat Rational (GenType bnd)
MachDouble Rational (GenType bnd)
MachNullAddr (GenType bnd)
MachLabel String (Maybe Int) (GenType bnd)
BlankAddr
AddrLit Int
SymLit var
SymLitEval (GenPrimFun bnd var) [GenLit bnd var]

Instances

(Eq var, Eq bnd) => Eq (GenLit bnd var) Source #
Methods (==) :: GenLit bnd var -> GenLit bnd var -> Bool # (/=) :: GenLit bnd var -> GenLit bnd var -> Bool #
(Read var, Read bnd) => Read (GenLit bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenLit bnd var) # readList :: ReadS [GenLit bnd var] # readPrec :: ReadPrec (GenLit bnd var) # readListPrec :: ReadPrec [GenLit bnd var] #
(Show var, Show bnd) => Show (GenLit bnd var) Source #
Methods showsPrec :: Int -> GenLit bnd var -> ShowS # show :: GenLit bnd var -> String # showList :: [GenLit bnd var] -> ShowS #

data GenAtom bnd var Source #

Atomic objects. VarAtom may be used for variable lookups, while LitAtom is used to denote literals.

Constructors

VarAtom var
LitAtom (GenLit bnd var)

Instances

(Eq bnd, Eq var) => Eq (GenAtom bnd var) Source #
Methods (==) :: GenAtom bnd var -> GenAtom bnd var -> Bool # (/=) :: GenAtom bnd var -> GenAtom bnd var -> Bool #
(Read bnd, Read var) => Read (GenAtom bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenAtom bnd var) # readList :: ReadS [GenAtom bnd var] # readPrec :: ReadPrec (GenAtom bnd var) # readListPrec :: ReadPrec [GenAtom bnd var] #
(Show bnd, Show var) => Show (GenAtom bnd var) Source #
Methods showsPrec :: Int -> GenAtom bnd var -> ShowS # show :: GenAtom bnd var -> String # showList :: [GenAtom bnd var] -> ShowS #

data GenPrimFun bnd var Source #

Primitive functions.

Constructors

PrimFun bnd (GenType bnd)

Instances

Eq bnd => Eq (GenPrimFun bnd var) Source #
Methods (==) :: GenPrimFun bnd var -> GenPrimFun bnd var -> Bool # (/=) :: GenPrimFun bnd var -> GenPrimFun bnd var -> Bool #
Read bnd => Read (GenPrimFun bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenPrimFun bnd var) # readList :: ReadS [GenPrimFun bnd var] # readPrec :: ReadPrec (GenPrimFun bnd var) # readListPrec :: ReadPrec [GenPrimFun bnd var] #
Show bnd => Show (GenPrimFun bnd var) Source #
Methods showsPrec :: Int -> GenPrimFun bnd var -> ShowS # show :: GenPrimFun bnd var -> String # showList :: [GenPrimFun bnd var] -> ShowS #

data GenExpr bnd var Source #

Expressions closely correspond to their representation in GHC.

Constructors

Atom (GenAtom bnd var)
PrimApp (GenPrimFun bnd var) [GenAtom bnd var]
ConApp (GenDataCon bnd) [GenAtom bnd var]
FunApp var [GenAtom bnd var]
Let (GenBinding bnd var) (GenExpr bnd var)
Case (GenExpr bnd var) var [GenAlt bnd var]

Instances

(Eq var, Eq bnd) => Eq (GenExpr bnd var) Source #
Methods (==) :: GenExpr bnd var -> GenExpr bnd var -> Bool # (/=) :: GenExpr bnd var -> GenExpr bnd var -> Bool #
(Read var, Read bnd) => Read (GenExpr bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenExpr bnd var) # readList :: ReadS [GenExpr bnd var] # readPrec :: ReadPrec (GenExpr bnd var) # readListPrec :: ReadPrec [GenExpr bnd var] #
(Show var, Show bnd) => Show (GenExpr bnd var) Source #
Methods showsPrec :: Int -> GenExpr bnd var -> ShowS # show :: GenExpr bnd var -> String # showList :: [GenExpr bnd var] -> ShowS #

data GenAlt bnd var Source #

Alternatives utilize an AltCon, a list of parameters of that match to the appropriate DataAlt as applicable, and an expression for the result.

Constructors

Alt (GenAltCon bnd var) [var] (GenExpr bnd var)

Instances

(Eq bnd, Eq var) => Eq (GenAlt bnd var) Source #
Methods (==) :: GenAlt bnd var -> GenAlt bnd var -> Bool # (/=) :: GenAlt bnd var -> GenAlt bnd var -> Bool #
(Read bnd, Read var) => Read (GenAlt bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenAlt bnd var) # readList :: ReadS [GenAlt bnd var] # readPrec :: ReadPrec (GenAlt bnd var) # readListPrec :: ReadPrec [GenAlt bnd var] #
(Show bnd, Show var) => Show (GenAlt bnd var) Source #
Methods showsPrec :: Int -> GenAlt bnd var -> ShowS # show :: GenAlt bnd var -> String # showList :: [GenAlt bnd var] -> ShowS #

data GenAltCon bnd var Source #

Alt Constructor

Constructors

DataAlt (GenDataCon bnd)
LitAlt (GenLit bnd var)
Default

Instances

(Eq var, Eq bnd) => Eq (GenAltCon bnd var) Source #
Methods (==) :: GenAltCon bnd var -> GenAltCon bnd var -> Bool # (/=) :: GenAltCon bnd var -> GenAltCon bnd var -> Bool #
(Read var, Read bnd) => Read (GenAltCon bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenAltCon bnd var) # readList :: ReadS [GenAltCon bnd var] # readPrec :: ReadPrec (GenAltCon bnd var) # readListPrec :: ReadPrec [GenAltCon bnd var] #
(Show var, Show bnd) => Show (GenAltCon bnd var) Source #
Methods showsPrec :: Int -> GenAltCon bnd var -> ShowS # show :: GenAltCon bnd var -> String # showList :: [GenAltCon bnd var] -> ShowS #

data GenBinding bnd var Source #

Binding

Constructors

Binding RecForm [(var, GenBindRhs bnd var)]

Instances

(Eq bnd, Eq var) => Eq (GenBinding bnd var) Source #
Methods (==) :: GenBinding bnd var -> GenBinding bnd var -> Bool # (/=) :: GenBinding bnd var -> GenBinding bnd var -> Bool #
(Read bnd, Read var) => Read (GenBinding bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenBinding bnd var) # readList :: ReadS [GenBinding bnd var] # readPrec :: ReadPrec (GenBinding bnd var) # readListPrec :: ReadPrec [GenBinding bnd var] #
(Show bnd, Show var) => Show (GenBinding bnd var) Source #
Methods showsPrec :: Int -> GenBinding bnd var -> ShowS # show :: GenBinding bnd var -> String # showList :: [GenBinding bnd var] -> ShowS #

data RecForm Source #

Recursive?

Constructors

Rec
NonRec

Instances

Eq RecForm Source #
Methods (==) :: RecForm -> RecForm -> Bool # (/=) :: RecForm -> RecForm -> Bool #
Read RecForm Source #
Methods readsPrec :: Int -> ReadS RecForm # readList :: ReadS [RecForm] # readPrec :: ReadPrec RecForm # readListPrec :: ReadPrec [RecForm] #
Show RecForm Source #
Methods showsPrec :: Int -> RecForm -> ShowS # show :: RecForm -> String # showList :: [RecForm] -> ShowS #

data GenBindRhs bnd var Source #

BindRhs taken straight from STG can be either in constructor form, or function form. Empty parameter list denotes a thunk.

Constructors

ConForm (GenDataCon bnd) [GenAtom bnd var]
FunForm [var] (GenExpr bnd var)

Instances

(Eq var, Eq bnd) => Eq (GenBindRhs bnd var) Source #
Methods (==) :: GenBindRhs bnd var -> GenBindRhs bnd var -> Bool # (/=) :: GenBindRhs bnd var -> GenBindRhs bnd var -> Bool #
(Read var, Read bnd) => Read (GenBindRhs bnd var) Source #
Methods readsPrec :: Int -> ReadS (GenBindRhs bnd var) # readList :: ReadS [GenBindRhs bnd var] # readPrec :: ReadPrec (GenBindRhs bnd var) # readListPrec :: ReadPrec [GenBindRhs bnd var] #
(Show var, Show bnd) => Show (GenBindRhs bnd var) Source #
Methods showsPrec :: Int -> GenBindRhs bnd var -> ShowS # show :: GenBindRhs bnd var -> String # showList :: [GenBindRhs bnd var] -> ShowS #

data GenConTag bnd Source #

Data Constructor tag that uniquely identifiers data constructors.

Constructors

ConTag bnd Int

Instances

Eq bnd => Eq (GenConTag bnd) Source #
Methods (==) :: GenConTag bnd -> GenConTag bnd -> Bool # (/=) :: GenConTag bnd -> GenConTag bnd -> Bool #
Read bnd => Read (GenConTag bnd) Source #
Methods readsPrec :: Int -> ReadS (GenConTag bnd) # readList :: ReadS [GenConTag bnd] # readPrec :: ReadPrec (GenConTag bnd) # readListPrec :: ReadPrec [GenConTag bnd] #
Show bnd => Show (GenConTag bnd) Source #
Methods showsPrec :: Int -> GenConTag bnd -> ShowS # show :: GenConTag bnd -> String # showList :: [GenConTag bnd] -> ShowS #

data GenDataCon bnd Source #

Data Constructor consists of its tag, the type that corresponds to its ADT, and a list of paramters it takes.

Constructors

DataCon (GenConTag bnd) (GenType bnd) [GenType bnd]

Instances

Eq bnd => Eq (GenDataCon bnd) Source #
Methods (==) :: GenDataCon bnd -> GenDataCon bnd -> Bool # (/=) :: GenDataCon bnd -> GenDataCon bnd -> Bool #
Read bnd => Read (GenDataCon bnd) Source #
Methods readsPrec :: Int -> ReadS (GenDataCon bnd) # readList :: ReadS [GenDataCon bnd] # readPrec :: ReadPrec (GenDataCon bnd) # readListPrec :: ReadPrec [GenDataCon bnd] #
Show bnd => Show (GenDataCon bnd) Source #
Methods showsPrec :: Int -> GenDataCon bnd -> ShowS # show :: GenDataCon bnd -> String # showList :: [GenDataCon bnd] -> ShowS #

data GenType bnd Source #

Types are information that are useful to keep during symbolic execution in order to generate correct feeds into the SMT solver. Overapproxmation is currently performed, and is likely to be cut back in the future.

Constructors

TyVarTy bnd (GenType bnd)
AppTy (GenType bnd) (GenType bnd)
ForAllTy (GenTyBinder bnd) (GenType bnd)
CastTy (GenType bnd) (GenCoercion bnd)
TyConApp (GenTyCon bnd) [GenType bnd]
CoercionTy (GenCoercion bnd)
LitTy TyLit
FunTy (GenType bnd) (GenType bnd)
Bottom

Instances

Eq bnd => Eq (GenType bnd) Source #
Methods (==) :: GenType bnd -> GenType bnd -> Bool # (/=) :: GenType bnd -> GenType bnd -> Bool #
Read bnd => Read (GenType bnd) Source #
Methods readsPrec :: Int -> ReadS (GenType bnd) # readList :: ReadS [GenType bnd] # readPrec :: ReadPrec (GenType bnd) # readListPrec :: ReadPrec [GenType bnd] #
Show bnd => Show (GenType bnd) Source #
Methods showsPrec :: Int -> GenType bnd -> ShowS # show :: GenType bnd -> String # showList :: [GenType bnd] -> ShowS #

data GenTyBinder bnd Source #

Type binder for ForAllTy.

Constructors

NamedTyBndr bnd (GenType bnd)
AnonTyBndr (GenType bnd)

Instances

Eq bnd => Eq (GenTyBinder bnd) Source #
Methods (==) :: GenTyBinder bnd -> GenTyBinder bnd -> Bool # (/=) :: GenTyBinder bnd -> GenTyBinder bnd -> Bool #
Read bnd => Read (GenTyBinder bnd) Source #
Methods readsPrec :: Int -> ReadS (GenTyBinder bnd) # readList :: ReadS [GenTyBinder bnd] # readPrec :: ReadPrec (GenTyBinder bnd) # readListPrec :: ReadPrec [GenTyBinder bnd] #
Show bnd => Show (GenTyBinder bnd) Source #
Methods showsPrec :: Int -> GenTyBinder bnd -> ShowS # show :: GenTyBinder bnd -> String # showList :: [GenTyBinder bnd] -> ShowS #

data TyLit Source #

Type literal.

Constructors

NumTyLit Int
StrTyLit String

Instances

Eq TyLit Source #
Methods (==) :: TyLit -> TyLit -> Bool # (/=) :: TyLit -> TyLit -> Bool #
Read TyLit Source #
Methods readsPrec :: Int -> ReadS TyLit # readList :: ReadS [TyLit] # readPrec :: ReadPrec TyLit # readListPrec :: ReadPrec [TyLit] #
Show TyLit Source #
Methods showsPrec :: Int -> TyLit -> ShowS # show :: TyLit -> String # showList :: [TyLit] -> ShowS #

data GenCoercion bnd Source #

Coercion. I have no idea what this does :)

Constructors

Coercion (GenType bnd) (GenType bnd)

Instances

Eq bnd => Eq (GenCoercion bnd) Source #
Methods (==) :: GenCoercion bnd -> GenCoercion bnd -> Bool # (/=) :: GenCoercion bnd -> GenCoercion bnd -> Bool #
Read bnd => Read (GenCoercion bnd) Source #
Methods readsPrec :: Int -> ReadS (GenCoercion bnd) # readList :: ReadS [GenCoercion bnd] # readPrec :: ReadPrec (GenCoercion bnd) # readListPrec :: ReadPrec [GenCoercion bnd] #
Show bnd => Show (GenCoercion bnd) Source #
Methods showsPrec :: Int -> GenCoercion bnd -> ShowS # show :: GenCoercion bnd -> String # showList :: [GenCoercion bnd] -> ShowS #

data GenTyCon bnd Source #

Type constructor.

Constructors

FunTyCon bnd
AlgTyCon bnd (GenAlgTyRhs bnd)
SynonymTyCon bnd
FamilyTyCon bnd
PrimTyCon bnd
Promoted bnd (GenDataCon bnd)
TcTyCon bnd

Instances

Eq bnd => Eq (GenTyCon bnd) Source #
Methods (==) :: GenTyCon bnd -> GenTyCon bnd -> Bool # (/=) :: GenTyCon bnd -> GenTyCon bnd -> Bool #
Read bnd => Read (GenTyCon bnd) Source #
Methods readsPrec :: Int -> ReadS (GenTyCon bnd) # readList :: ReadS [GenTyCon bnd] # readPrec :: ReadPrec (GenTyCon bnd) # readListPrec :: ReadPrec [GenTyCon bnd] #
Show bnd => Show (GenTyCon bnd) Source #
Methods showsPrec :: Int -> GenTyCon bnd -> ShowS # show :: GenTyCon bnd -> String # showList :: [GenTyCon bnd] -> ShowS #

data GenAlgTyRhs bnd Source #

ADT RHS.

Constructors

AbstractTyCon Bool
DataTyCon [GenConTag bnd]
TupleTyCon (GenConTag bnd)
NewTyCon (GenConTag bnd)

Instances

Eq bnd => Eq (GenAlgTyRhs bnd) Source #
Methods (==) :: GenAlgTyRhs bnd -> GenAlgTyRhs bnd -> Bool # (/=) :: GenAlgTyRhs bnd -> GenAlgTyRhs bnd -> Bool #
Read bnd => Read (GenAlgTyRhs bnd) Source #
Methods readsPrec :: Int -> ReadS (GenAlgTyRhs bnd) # readList :: ReadS [GenAlgTyRhs bnd] # readPrec :: ReadPrec (GenAlgTyRhs bnd) # readListPrec :: ReadPrec [GenAlgTyRhs bnd] #
Show bnd => Show (GenAlgTyRhs bnd) Source #
Methods showsPrec :: Int -> GenAlgTyRhs bnd -> ShowS # show :: GenAlgTyRhs bnd -> String # showList :: [GenAlgTyRhs bnd] -> ShowS #