Safe Haskell	Safe-Inferred

Language.Boogie.AST

Description

Abstract syntax tree for Boogie 2

Synopsis

Documentation

newtype Program Source

Program: a list of top-level declarations

Constructors

Program [Decl]

Instances

Eq Program
Show Program

data Type Source

Type

Constructors

BoolType
IntType
MapType [Id] [Type] Type
Instance Id [Type]

Instances

Eq Type
Show Type

nullaryType :: Id -> Type Source

nullaryType id : type denoted by id without arguments

noType :: Type Source

Dummy type used during type checking to denote error

data UnOp Source

Unary operators

Constructors

Neg
Not

Instances

Eq UnOp

data BinOp Source

Binary operators

Constructors

Plus
Minus
Times
Div
Mod
And
Or
Implies
Explies
Equiv
Eq
Neq
Lc
Ls
Leq
Gt
Geq

Instances

Eq BinOp

data QOp Source

Quantifiers

Constructors

Forall
Exists
Lambda

Instances

Eq QOp

type Expression = Pos BareExpression Source

Expression with a source position attached

data BareExpression Source

Expression

Constructors

FF	false
TT	true
Numeral Integer	`Numeral` `value`
Var Id	`Var` `name`
Application Id [Expression]	`Application` `f args`
MapSelection Expression [Expression]	`MapSelection` `map indexes`
MapUpdate Expression [Expression] Expression	`MapUpdate` `map indexes rhs`
Old Expression
IfExpr Expression Expression Expression	`IfExpr` `cond eThen eElse`
Coercion Expression Type
UnaryExpression UnOp Expression
BinaryExpression BinOp Expression Expression
Quantified QOp [Id] [IdType] Expression	`Quantified` `qop type_vars bound_vars expr`

Instances

Eq BareExpression
Show BareExpression

mapSelectExpr :: Pos BareExpression -> [Expression] -> Pos BareExpression Source

mapSelectExpr m args : map selection expression with position of m attached

data WildcardExpression Source

Wildcard or expression

Constructors

Wildcard
Expr Expression

Instances

Eq WildcardExpression

type Statement = Pos BareStatement Source

Statement with a source position attached

data BareStatement Source

Statement

Constructors

Predicate SpecClause	Predicate statement (assume or assert)
Havoc [Id]	`Havoc` `var_names`
Assign [(Id, [[Expression]])] [Expression]	`Assign` `var_map_selects rhss`
Call [Id] Id [Expression]	`Call` `lhss proc_name args`
CallForall Id [WildcardExpression]	`CallForall` `proc_name args`
If WildcardExpression Block (Maybe Block)	`If` `wild_or_expr then_block else_block`
While WildcardExpression [SpecClause] Block	`While` `wild_or_expr free_loop_inv loop_body`
Break (Maybe Id)	`Break` `label`
Return
Goto [Id]	`Goto` `labels`
Skip	only used at the end of a block

Instances

Eq BareStatement
Show BareStatement

type LStatement = Pos BareLStatement Source

Statement labeled by multiple labels with a source position attached

type BareLStatement = ([Id], Statement)Source

Statement labeled by multiple labels

type Block = [LStatement]Source

Statement block

singletonBlock :: Pos a -> [Pos ([a1], Pos a)]Source

Block consisting of a single non-labeled statement

type Body = ([[IdTypeWhere]], Block)Source

Procedure body: consists of local variable declarations and a statement block

type BasicBlock = (Id, [Statement])Source

Basic block is a list of statements labeled by a single label; the list contains no jump, if or while statements, except for the last statement, which can be a goto or return

type BasicBody = ([IdTypeWhere], Map Id [Statement])Source

Procedure body transformed to basic blocks: consists of local variable declarations and a set of basic blocks (represented as a map from their labels to statement lists)

data SpecType Source

Types of specification clauses

Constructors

Inline
Precondition
Postcondition
LoopInvariant
Where

Instances

Eq SpecType

data SpecClause Source

Specification clause

Constructors

SpecClause
Fields specType :: SpecType Source of the clause specFree :: Bool Is it free (assumption) or checked (assertions)? specExpr :: Expression Boolean expression

Instances

Eq SpecClause

data Contract Source

Procedure contract clause

Constructors

Requires Bool Expression	`Requires` `e free`
Modifies Bool [Id]	`Modifies` `var_names free`
Ensures Bool Expression	`Ensures` `e free`

Instances

Eq Contract

type Decl = Pos BareDecl Source

Top-level declaration with a source position attached

data BareDecl Source

Top-level declaration

Constructors

TypeDecl [NewType]
ConstantDecl Bool [Id] Type ParentInfo Bool	`ConstantDecl` `unique names type orderSpec complete`
FunctionDecl Id [Id] [FArg] FArg (Maybe Expression)	`FunctionDecl` `name type_args formals ret body`
AxiomDecl Expression
VarDecl [IdTypeWhere]
ProcedureDecl Id [Id] [IdTypeWhere] [IdTypeWhere] [Contract] (Maybe Body)	`ProcedureDecl` `name type_args formals rets contract body`
ImplementationDecl Id [Id] [IdType] [IdType] [Body]	`ImplementationDecl` `name type_args formals rets body`

Instances

Eq BareDecl
Show BareDecl

type Id = String Source

Identifier

data NewType Source

Definition of a type

Constructors

NewType
Fields tId :: Id tArgs :: [Id] tValue :: Maybe Type

Instances

Eq NewType

type IdType = (Id, Type)Source

Name declaration (identifier, type)

data IdTypeWhere Source

Name declaration with a where clause

Constructors

IdTypeWhere
Fields itwId :: Id itwType :: Type itwWhere :: Expression

Instances

Eq IdTypeWhere

noWhere :: IdTypeWhere -> (Id, Type)Source

Strip the where clause

type FArg = (Maybe Id, Type)Source

Formal argument of a function

dummyFArg :: [Char]Source

Argument name used for unnamed function arguments (does not matter, because it is never referred to from function's body)

type ParentEdge = (Bool, Id)Source

Parent edge of a constant declaration (uniqueness, parent name)

type ParentInfo = Maybe [ParentEdge]Source

Parent information in a constant declaration (Nothing means no information, while empty list means no parents)