| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
SSTG.Core.Language.Syntax
Description
SSTG Syntax Definitions
- newtype Program = Program [Binds]
- data NameSpace
- data Name = Name String (Maybe String) NameSpace Int
- data Var = Var Name Type
- data Lit
- data Atom
- data PrimFun = PrimFun Name Type
- data Expr
- data Alt = Alt AltCon Expr
- data AltCon
- data Binds = Binds RecForm [(Var, BindRhs)]
- data RecForm
- data BindRhs
- data DataCon = DataCon Name Type [Type]
- data Type
- data TyBinder
- data TyLit
- data Coercion = Coercion Type Type
- data TyCon
- data AlgTyRhs
- = AbstractTyCon Bool
- | DataTyCon [Name]
- | NewTyCon Name
- | TupleTyCon Name
Documentation
Variables, data constructors, type variables, and type constructors.
Constructors
| VarNSpace | |
| DataNSpace | |
| TvNSpace | |
| TcClsNSpace |
Literals are largely augmented from the original GHC implementation, with
additional annotations to denote BlankAddr for lifting, AddrLit for
value deriviation, and LitEval to represent symbolic literal evaluation,
as literal manipulation functions are defined in the Haskell Prelude, and
thus outside of scope for us.
Primitive functions.
Expressions closely correspond to their representation in GHC.
Alt Constructor
Bindings
Recursive?
BindRhs taken straight from STG can be either in constructor form, or
function form. Empty parameter list denotes a thunk.
Data Constructor consists of its tag, the type that corresponds to its ADT, and a list of paramters it takes.
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.
Type binder for ForAllTy.
Constructors
| NamedTyBndr Name | |
| AnonTyBndr |
Type literal.
Coercion. I have no idea what this does :)