Copyright | Benjamin Jones 2016 |
---|---|
License | ISC |
Maintainer | bjones@galois.com |
Stability | experimental |
Portability | unknown |
Safe Haskell | Safe |
Language | Haskell2010 |
Language.Sally.Types
Description
This module defines types reflecting the basic Sally input language sections and base types.
- data Name
- textFromName :: Name -> Text
- nameFromT :: Text -> Name
- nameFromS :: String -> Name
- catNamesWith :: Text -> Name -> Name -> Name
- bangNames :: Name -> Name -> Name
- scoreNames :: Name -> Name -> Name
- nextName :: Name -> Name
- stateName :: Name -> Name
- inputName :: Name -> Name
- varFromName :: Name -> SallyVar
- data SallyBaseType
- data SallyConst
- data SallyState = SallyState {
- sName :: Name
- sVars :: [(Name, SallyBaseType)]
- sInVars :: [(Name, SallyBaseType)]
- data SallyPred
- newtype SallyVar = SallyVar {
- textFromVar :: Text
- data SallyArith
- data SallyExpr
- class ToSallyExpr a where
- data SallyStateFormula = SallyStateFormula {}
- type SallyLet = (SallyVar, SallyExpr)
- data SallyTransition = SallyTransition {}
- data SallySystem = SallySystem {}
- data TrResult = TrResult {}
Name type
A Name
is a wrapped up strict Text.
catNamesWith :: Text -> Name -> Name -> Name Source #
Concatenate names with the given seperating text in between
scoreNames :: Name -> Name -> Name Source #
Concatenate names with an underscore
separated in between
Base types
data SallyBaseType Source #
Base data types in Sally: Booleans, (mathematical) Integers, and (mathematical) Reals
Instances
data SallyConst Source #
A defined constant. For our purposes, a real number is represented (approximated) by an exact rational number.
Constructors
SConstBool Bool | |
SConstInt Integer | |
SConstReal Rational |
Instances
Types for defining transition systems
data SallyState Source #
The state type in Sally
This consists of 1) a name for the type, 2) a set of state variables (and their associated base type) and, 3) (optionally) a set in input variabels which are uninterpreted in the model; they can be thought of as varying non-deterministically in any system trace.
Constructors
SallyState | |
Fields
|
Instances
Predicates
Constructors
SPConst Bool | boolean constant |
SPExpr SallyExpr | a boolean valued expression |
SPAnd (Seq SallyPred) | and |
SPOr (Seq SallyPred) | or |
SPImpl SallyPred SallyPred | implication |
SPNot SallyPred | logical negation |
SPEq SallyExpr SallyExpr | == |
SPLEq SallyExpr SallyExpr | <= |
SPGEq SallyExpr SallyExpr | = |
SPLt SallyExpr SallyExpr | < |
SPGt SallyExpr SallyExpr |
A SallyVar
is a wrapped up variable name.
Constructors
SallyVar | |
Fields
|
data SallyArith Source #
Arithmetic terms
Constructors
SAAdd SallyExpr SallyExpr | addition |
SAMult SallyExpr SallyExpr | constant mult |
SADiv SallyExpr SallyExpr | constant division |
SAExpr SallyExpr | general expression |
Instances
Expressions
class ToSallyExpr a where Source #
A typeclass for types that can be converted to a SallyExpr
.
Minimal complete definition
data SallyStateFormula Source #
A named formula over a state type
Constructors
SallyStateFormula | |
Instances
type SallyLet = (SallyVar, SallyExpr) Source #
A "let" binding: each let binds a SallyVar
to a Sally expression,
which can be a constant literal, a predicate (boolean value), or an
arithmetic expression.
data SallyTransition Source #
A transition over a given state type
Constructors
SallyTransition | |
Instances
data SallySystem Source #
A transition system declaration
Constructors
SallySystem | |
Instances
Eq SallySystem Source # | |
Show SallySystem Source # | |
ToSExp SallySystem Source # | Pretty print a |
The result of translation, a specific form of the Sally AST.
Constructors
TrResult | |
Fields
|