language-boogie-0.2: Interpreter and language infrastructure for Boogie.

Safe HaskellNone




Type checker for Boogie 2


Checking programs

typeCheckProgram :: Program -> Either [TypeError] ContextSource

Check program and return type errors if present, and the global typing context otherwise

exprType :: Context -> Expression -> TypeSource

exprType c expr : Type of expr in context c; fails if expr contains type errors.

resolve :: Context -> Type -> TypeSource

resolve c t : type t with all type synonyms resolved according to binding in c

data TypeError Source

Type error with a source position and a pretty-printed message


TypeError SourcePos Doc 


typeErrorsDoc :: [TypeError] -> DocSource

Pretty-printed list of type errors

Typing context

data Context Source

Typing context




ctxTypeConstructors :: Map Id Int

type constructor arity

ctxTypeSynonyms :: Map Id ([Id], Type)

type synonym values

ctxGlobals :: Map Id Type

global variable types (type synonyms resolved)

ctxConstants :: Map Id Type

constant types (type synonyms resolved)

ctxFunctions :: Map Id FSig

function signatures (type synonyms resolved)

ctxProcedures :: Map Id PSig

procedure signatures (type synonyms resolved) Local:

ctxTypeVars :: [Id]

free type variables

ctxIns :: Map Id Type

input parameter types

ctxLocals :: Map Id Type

local variable types

ctxModifies :: [Id]

variables in the modifies clause of the enclosing procedure

ctxLabels :: [Id]

all labels of the enclosing procedure body

ctxEncLabels :: [Id]

labels of all enclosing statements

ctxTwoState :: Bool

is the context two-state? (procedure body or postcondition)

ctxInLoop :: Bool

is context inside a loop body?

ctxPos :: SourcePos

position in the source code Persistent context (not specific to any node, never gets restored):

ctxFreshTVCount :: Integer

number of fresh type variables already generated

emptyContext :: ContextSource

Empty context

typeNames :: Context -> [Id]Source

Type constructors and synonyms

globalScope :: Context -> Map Id TypeSource

Global variables and constants

localScope :: Context -> Map Id TypeSource

Input parameters and local variables

mutableVars :: Context -> Map Id TypeSource

All variables that can be assigned to (local variables and global variables)

allVars :: Context -> Map Id TypeSource

All variables that can have where clauses (everything except constants)

allNames :: Context -> Map Id TypeSource

All variables and constants (local-scope preferred)

funProcNames :: Context -> [Id]Source

Names of functions and procedures

funSig :: Id -> Context -> FSigSource

Function signature by name

procSig :: Id -> Context -> PSigSource

Procedure signature by name

enterFunction :: FSig -> [Id] -> [Expression] -> Context -> ContextSource

enterFunction sig formals actuals mRetType c : Local context of function sig with formal arguments formals and actual arguments actuals in a context where the return type is exprected to be mRetType (if known)

enterProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Context -> ContextSource

enterProcedure sig def actuals lhss c : Local context of procedure sig with definition def and actual arguments actuals in a call with left-hand sides lhss

enterQuantified :: [Id] -> [IdType] -> Context -> ContextSource

Local context of a quantified expression