| 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
| |