Language.Boogie.Util

Various properties and transformations of Boogie program elements

Types

type TypeBinding = Map Id Type

Mapping from type variables to types

typeSubst :: TypeBinding -> Type -> Type

typeSubst binding t : Substitute all free type variables in t according to binding; all variables in the domain of bindings are considered free if not explicitly bound

isFreeIn :: Id -> Type -> Bool

x isFreeIn t : does x occur as a free type variable in t? x must not be a name of a type constructor

unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding

unifier fv xs ys : most general unifier of xs and ys with shared free type variables fv

oneSidedUnifier :: [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding

oneSidedUnifier fv xs tv ys : Most general unifier of xs and ys, where only xs contain free variables (fv), while ys contain rigid type variables tv, which might clash with fv

boundUnifier :: [Id] -> [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding

boundUnifier fv bv1 xs bv2 ys : Most general unifier of xs and ys, where bv1 are bound type variables in xs and bv2 are bound type variables in ys, and fv are free type variables of the enclosing context

(<==>) :: Type -> Type -> Bool

Semantic equivalence on types (equality up to renaming of bound type variables)

Expressions

freeVarsTwoState :: Expression -> ([Id], [Id])

Free variables in an expression, referred to in current state and old state

freeVars :: Expression -> [Id]

Free variables in an expression, in current state

freeOldVars :: Expression -> [Id]

Free variables in an expression, in old state

type VarBinding = Map Id BareExpression

Mapping from variables to expressions

exprSubst :: VarBinding -> Expression -> Expression

exprSubst binding e : substitute all free variables in e according to binding; all variables in the domain of bindings are considered free if not explicitly bound

paramSubst :: PSig -> PDef -> Expression -> Expression

paramSubst sig def : Substitute parameter names from sig in an expression with their equivalents from def

Specs

preconditions :: [Contract] -> [SpecClause]

preconditions specs : all precondition clauses in specs

postconditions :: [Contract] -> [SpecClause]

postconditions specs : all postcondition clauses in specs

modifies :: [Contract] -> [Id]

modifies specs : all modifies clauses in specs

assumePreconditions :: PSig -> PSig

Make all preconditions in contracts free

Funstions and procedures

data FSig

Function signature

Constructors

FSig

Fields

fsigName :: Id

Function name

fsigTypeVars :: [Id]

Type variables

fsigArgTypes :: [Type]

Argument types

fsigRetType :: Type

Return type

data FDef

Function definition

Constructors

FDef

Fields

fdefArgs :: [Id]

Argument names (in the same order as fsigArgTypes in the corresponding signature)

fdefGuard :: Expression

Condition under which this definition applies

fdefBody :: Expression

Body

data PSig

Procedure signature

Constructors

PSig

Fields

psigName :: Id

Procedure name

psigTypeVars :: [Id]

Type variables

psigArgs :: [IdTypeWhere]

In-parameters

psigRets :: [IdTypeWhere]

Out-parameters

psigContracts :: [Contract]

Contracts

psigParams :: PSig -> [IdTypeWhere]

All parameters of a procedure signature

psigArgTypes :: PSig -> [Type]

Types of in-parameters of a procedure signature

psigRetTypes :: PSig -> [Type]

Types of out-parameters of a procedure signature

psigModifies :: PSig -> [Id]

Modifies clauses of a procedure signature

psigRequires :: PSig -> [SpecClause]

Preconditions of a procedure signature

psigEnsures :: PSig -> [SpecClause]

Postconditions of a procedure signature

data PDef

Procedure definition; a single procedure might have multiple definitions (one per body)

Constructors

PDef

Fields

pdefIns :: [Id]

In-parameter names (in the same order as psigArgs in the corresponding signature)

pdefOuts :: [Id]

Out-parameter names (in the same order as psigRets in the corresponding signature)

pdefParamsRenamed :: Bool

Are any parameter names in this definition different for the procedure signature? (used for optimizing parameter renaming, True is a safe default)

pdefBody :: BasicBody

Body

pdefPos :: SourcePos

Location of the (first line of the) procedure definition in the source

Code generation

num :: Integer -> Pos BareExpression

eneg :: Pos BareExpression -> Pos BareExpression

enot :: Pos BareExpression -> Pos BareExpression

(|+|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|-|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|*|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|/|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|%|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|!=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|<|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|<=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|>=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|&|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|||) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|=>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|<=>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

assume :: Pos BareExpression -> Pos BareStatement

Misc

interval :: Enum t => (t, t) -> [t]

interval (lo, hi) : Interval from lo to hi

fromRight :: Either a b -> b

Extract the element out of a Right and throw an error if its argument is Left

mapFst :: (t -> t1) -> (t, t2) -> (t1, t2)

mapSnd :: (t -> t2) -> (t1, t) -> (t1, t2)

mapBoth :: (t -> t1) -> (t, t) -> (t1, t1)

changeState :: (s -> t) -> (t -> s -> s) -> State t a -> State s a

Execute a computation with state of type t inside a computation with state of type s

withLocalState :: (s -> t) -> State t a -> State s a

withLocalState localState e : Execute e in current state modified by localState, and then restore current state