-- | Abstract syntax tree for Boogie 2
module Language.Boogie.AST where
import Language.Boogie.Position
import Data.Map (Map)
{- Basic -}
-- | Program: a list of top-level declarations
newtype Program = Program [Decl]
deriving Eq
{- Types -}
-- | Type
data Type = BoolType | -- ^ bool
IntType | -- ^ int
MapType [Id] [Type] Type | -- 'MapType' @type_vars domains range@ : arrow type (used for maps, function and procedure signatures)
IdType Id [Type] -- 'IdType' @name args@: type denoted by an identifier (either type constructor, possibly with arguments, or a type variable)
deriving Eq -- syntactic equality
-- | 'nullaryType' @id@ : type denoted by @id@ without arguments
nullaryType id = IdType id []
-- | Dummy type used during type checking to denote error
noType = nullaryType "NoType"
{- Expressions -}
-- | Unary operators
data UnOp = Neg | Not
deriving Eq
-- | Binary operators
data BinOp = Plus | Minus | Times | Div | Mod | And | Or | Implies | Explies | Equiv | Eq | Neq | Lc | Ls | Leq | Gt | Geq
deriving Eq
-- | Quantifiers
data QOp = Forall | Exists | Lambda
deriving Eq
-- | Expression with a source position attached
type Expression = Pos BareExpression
-- | Expression
data BareExpression = 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@
deriving Eq -- syntactic equality
-- | 'mapSelectExpr' @m args@ : map selection expression with position of @m@ attached
mapSelectExpr m args = attachPos (position m) (MapSelection m args)
-- | Wildcard or expression
data WildcardExpression = Wildcard | Expr Expression
deriving Eq
{- Statements -}
-- | Statement with a source position attached
type Statement = Pos BareStatement
-- | Statement
data BareStatement = 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
deriving Eq -- syntactic equality
-- | Statement labeled by multiple labels with a source position attached
type LStatement = Pos BareLStatement
-- | Statement labeled by multiple labels
type BareLStatement = ([Id], Statement)
-- | Statement block
type Block = [LStatement]
-- | Block consisting of a single non-labeled statement
singletonBlock s = [attachPos (position s) ([], s)]
-- | Procedure body: consists of local variable declarations and a statement block
type Body = ([[IdTypeWhere]], Block)
-- | 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 BasicBlock = (Id, [Statement])
-- | 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)
type BasicBody = ([IdTypeWhere], Map Id [Statement])
{- Specs -}
-- | Types of specification clauses
data SpecType = Inline | Precondition | Postcondition | LoopInvariant | Where | Axiom
deriving Eq
-- | Specification clause
data SpecClause = SpecClause {
specType :: SpecType, -- ^ Source of the clause
specFree :: Bool, -- ^ Is it free (assumption) or checked (assertions)?
specExpr :: Expression -- ^ Boolean expression
} deriving Eq
-- | Procedure contract clause
data Contract = Requires Bool Expression | -- ^ 'Requires' @e free@
Modifies Bool [Id] | -- ^ 'Modifies' @var_names free@
Ensures Bool Expression -- ^ 'Ensures' @e free@
deriving Eq
{- Declarations -}
-- | Top-level declaration with a source position attached
type Decl = Pos BareDecl
-- | Top-level declaration
data BareDecl =
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@
deriving Eq
{- Misc -}
-- | Identifier
type Id = String
-- | Definition of a type
data NewType = NewType {
tId :: Id,
tArgs :: [Id],
tValue :: Maybe Type
} deriving Eq
-- | Name declaration (identifier, type)
type IdType = (Id, Type)
-- | Name declaration with a where clause
data IdTypeWhere = IdTypeWhere {
itwId :: Id,
itwType :: Type,
itwWhere :: Expression
} deriving Eq
-- | Strip the where clause
noWhere itw = (itwId itw, itwType itw)
-- | Formal argument of a function
type FArg = (Maybe Id, Type)
-- | Argument name used for unnamed function arguments
-- (does not matter, because it is never referred to from function's body)
dummyFArg = ""
-- | Parent edge of a constant declaration (uniqueness, parent name)
type ParentEdge = (Bool, Id)
-- | Parent information in a constant declaration
-- (Nothing means no information, while empty list means no parents)
type ParentInfo = Maybe [ParentEdge]