language-sally-0.1.0.0: AST and pretty printer for Sally

CopyrightBenjamin Jones 2016
LicenseISC
Maintainerbjones@galois.com
Stabilityexperimental
Portabilityunknown
Safe HaskellSafe
LanguageHaskell2010

Language.Sally.Types

Contents

Description

This module defines types reflecting the basic Sally input language sections and base types.

Synopsis

Name type

data Name Source #

A Name is a wrapped up strict Text.

Instances

nameFromT :: Text -> Name Source #

Convert a Text to a Name.

nameFromS :: String -> Name Source #

Convert a String to a Name.

catNamesWith :: Text -> Name -> Name -> Name Source #

Concatenate names with the given seperating text in between

bangNames :: Name -> Name -> Name Source #

Concatenate names with a bang separated in between

scoreNames :: Name -> Name -> Name Source #

Concatenate names with an underscore separated in between

nextName :: Name -> Name Source #

Return the name of the given name in the "next" namespace

stateName :: Name -> Name Source #

Return the name of the given name in the "state" namespace

inputName :: Name -> Name Source #

Return the name of the given name in the "input" namespace

varFromName :: Name -> SallyVar Source #

Create a SallyVar from a Name.

Base types

data SallyBaseType Source #

Base data types in Sally: Booleans, (mathematical) Integers, and (mathematical) Reals

Constructors

SBool 
SInt 
SReal 

data SallyConst Source #

A defined constant. For our purposes, a real number is represented (approximated) by an exact rational number.

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

newtype SallyVar Source #

A SallyVar is a wrapped up variable name.

Constructors

SallyVar 

Fields

class ToSallyExpr a where Source #

A typeclass for types that can be converted to a SallyExpr.

Minimal complete definition

toSallyExpr

Methods

toSallyExpr :: a -> SallyExpr Source #

Convert a value to a SallyExpr.

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 

Fields

data SallySystem Source #

A transition system declaration

Constructors

SallySystem 

Fields

data TrResult Source #

The result of translation, a specific form of the Sally AST.

Constructors

TrResult 

Fields

Instances

Eq TrResult Source # 
Show TrResult Source # 
Pretty TrResult Source #

TrResult requires a special printer since it is not an s-expression. The order of the vcat items is important because Sally is sensitive to names being declared before they are used in a model file.

Methods

pretty :: TrResult -> Doc #

prettyList :: [TrResult] -> Doc #