Safe Haskell | None |
---|
Various properties and transformations of Boogie program elements
- type TypeBinding = Map Id Type
- typeSubst :: TypeBinding -> Type -> Type
- renameTypeVars :: [Id] -> [Id] -> TypeBinding -> TypeBinding
- fromTVNames :: [Id] -> [Id] -> TypeBinding
- isFreeIn :: Id -> Type -> Bool
- isTypeVar :: [Id] -> Id -> Bool
- unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding
- freshTVName :: Show a => a -> [Char]
- tupleType :: [Type] -> Type
- freeVarsTwoState :: Expression -> ([Id], [Id])
- freeVars :: Expression -> [Id]
- freeOldVars :: Expression -> [Id]
- type VarBinding = Map Id BareExpression
- exprSubst :: VarBinding -> Expression -> Expression
- paramSubst :: PSig -> PDef -> Expression -> Expression
- freeSelections :: Expression -> [(Id, [Expression])]
- applications :: Expression -> [(Id, [Expression])]
- preconditions :: [Contract] -> [SpecClause]
- postconditions :: [Contract] -> [SpecClause]
- modifies :: [Contract] -> [Id]
- assumePreconditions :: PSig -> PSig
- assumePostconditions :: PSig -> PSig
- data FSig = FSig {
- fsigName :: Id
- fsigTypeVars :: [Id]
- fsigArgTypes :: [Type]
- fsigRetType :: Type
- fsigType :: FSig -> Type
- fsigFromType :: Type -> FSig
- data FDef = FDef {
- fdefName :: Id
- fdefTV :: [Id]
- fdefArgs :: [IdType]
- fdefGuard :: Expression
- fdefBody :: Expression
- type ConstraintSet = ([FDef], [FDef])
- type AbstractStore = Map Id ConstraintSet
- asUnion :: AbstractStore -> AbstractStore -> AbstractStore
- data PSig = PSig {
- psigName :: Id
- psigTypeVars :: [Id]
- psigArgs :: [IdTypeWhere]
- psigRets :: [IdTypeWhere]
- psigContracts :: [Contract]
- psigParams :: PSig -> [IdTypeWhere]
- psigArgTypes :: PSig -> [Type]
- psigRetTypes :: PSig -> [Type]
- psigModifies :: PSig -> [Id]
- psigRequires :: PSig -> [SpecClause]
- psigEnsures :: PSig -> [SpecClause]
- psigType :: PSig -> Type
- data PDef = PDef {
- pdefIns :: [Id]
- pdefOuts :: [Id]
- pdefParamsRenamed :: Bool
- pdefBody :: BasicBody
- pdefConstraints :: AbstractStore
- pdefPos :: SourcePos
- pdefLocals :: PDef -> [Id]
- 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
- conjunction :: [Pos BareExpression] -> Pos BareExpression
- assume :: Pos BareExpression -> Pos BareStatement
- interval :: Enum t => (t, t) -> [t]
- fromRight :: Either a b -> b
- deleteAll :: Ord k => [k] -> Map k a -> Map k a
- restrictDomain :: Ord k => Set k -> Map k a -> Map k a
- removeDomain :: Ord k => Set k -> Map k a -> Map k a
- mapItwType :: (Type -> Type) -> IdTypeWhere -> IdTypeWhere
- anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool
- changeState :: Monad m => (s -> t) -> (t -> s -> s) -> StateT t m a -> StateT s m a
- withLocalState :: Monad m => (s -> t) -> StateT t m a -> StateT s m a
- internalError :: [Char] -> t
Types
type TypeBinding = Map Id TypeSource
Mapping from type variables to types
typeSubst :: TypeBinding -> Type -> TypeSource
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
renameTypeVars :: [Id] -> [Id] -> TypeBinding -> TypeBindingSource
renameTypeVars
tv newTV binding
: binding
with each occurrence of one of tv
replaced with corresponding newTV
(in both domain and range)
fromTVNames :: [Id] -> [Id] -> TypeBindingSource
fromTVNames
tvs tvs'
: type binding that replaces type variables tvs
with type variables tvs'
isTypeVar :: [Id] -> Id -> BoolSource
isTypeVar
contextTypeVars v
: Is v
either one of contextTypeVars
or a freash type variable generated by freshTVName
?
unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBindingSource
unifier
fv xs ys
: most general unifier of xs
and ys
with shared free type variables of the context fv
freshTVName :: Show a => a -> [Char]Source
'freshTVName n
: Fresh type variable with a unique identifier n
tupleType :: [Type] -> TypeSource
Internal tuple type constructor (used for representing procedure returns as a single type)
Expressions
freeVarsTwoState :: Expression -> ([Id], [Id])Source
Free variables in an expression, referred to in current state and old state
freeVars :: Expression -> [Id]Source
Free variables in an expression, in current state
freeOldVars :: Expression -> [Id]Source
Free variables in an expression, in old state
type VarBinding = Map Id BareExpressionSource
Mapping from variables to expressions
exprSubst :: VarBinding -> Expression -> ExpressionSource
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 -> ExpressionSource
paramSubst
sig def
:
Substitute parameter names from sig
in an expression with their equivalents from def
freeSelections :: Expression -> [(Id, [Expression])]Source
freeSelections
expr
: all map selections that occur in expr
, where the map is a free variable
applications :: Expression -> [(Id, [Expression])]Source
applications
expr
: all function applications that occur in expr
Specs
preconditions :: [Contract] -> [SpecClause]Source
preconditions
specs
: all precondition clauses in specs
postconditions :: [Contract] -> [SpecClause]Source
postconditions
specs
: all postcondition clauses in specs
assumePreconditions :: PSig -> PSigSource
Make all preconditions in contracts free
assumePostconditions :: PSig -> PSigSource
Make all postconditions in contracts free
Functions and procedures
Function signature
FSig | |
|
fsigFromType :: Type -> FSigSource
Map type as a function signature
Function definition
type ConstraintSet = ([FDef], [FDef])Source
Constraint set: contains a list of definitions and a list of constraints
type AbstractStore = Map Id ConstraintSetSource
Abstract store: maps names to their constraints
asUnion :: AbstractStore -> AbstractStore -> AbstractStoreSource
Union of abstract stores (values at the same key are concatenated)
Procedure signature
PSig | |
|
psigParams :: PSig -> [IdTypeWhere]Source
All parameters of a procedure signature
psigArgTypes :: PSig -> [Type]Source
Types of in-parameters of a procedure signature
psigRetTypes :: PSig -> [Type]Source
Types of out-parameters of a procedure signature
psigModifies :: PSig -> [Id]Source
Modifies clauses of a procedure signature
psigRequires :: PSig -> [SpecClause]Source
Preconditions of a procedure signature
psigEnsures :: PSig -> [SpecClause]Source
Postconditions of a procedure signature
Procedure definition; a single procedure might have multiple definitions (one per body)
PDef | |
|
pdefLocals :: PDef -> [Id]Source
All local names of a procedure definition
Code generation
num :: Integer -> Pos BareExpressionSource
Misc
deleteAll :: Ord k => [k] -> Map k a -> Map k aSource
deleteAll
keys m
: map m
with keys
removed from its domain
restrictDomain :: Ord k => Set k -> Map k a -> Map k aSource
restrictDomain
keys m
: map m
restricted on the set of keys keys
removeDomain :: Ord k => Set k -> Map k a -> Map k aSource
removeDomain
keys m
: map m
with the set of keys keys
removed from its domain
mapItwType :: (Type -> Type) -> IdTypeWhere -> IdTypeWhereSource
anyM :: Monad m => (a -> m Bool) -> [a] -> m BoolSource
Monadic version of any
(executes boolean-valued computation for all arguments in a list until the first True is found)
changeState :: Monad m => (s -> t) -> (t -> s -> s) -> StateT t m a -> StateT s m aSource
Execute a computation with state of type t
inside a computation with state of type s
withLocalState :: Monad m => (s -> t) -> StateT t m a -> StateT s m aSource
withLocalState
localState e
:
Execute e
in current state modified by localState
, and then restore current state
internalError :: [Char] -> tSource