Language.Boogie.TypeChecker

Type checker for Boogie 2

Checking programs

typeCheckProgram :: Program -> Either [TypeError] Context

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

exprType :: Context -> Expression -> Type

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

resolve :: Context -> Type -> Type

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

data TypeError

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

Constructors

TypeError SourcePos Doc

Instances

ErrorList TypeError

typeErrorsDoc :: [TypeError] -> Doc

Pretty-printed list of type errors

Typing context

data Context

Typing context

Constructors

Context

Fields

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 :: Context

Empty context

typeNames :: Context -> [Id]

Type constructors and synonyms

globalScope :: Context -> Map Id Type

Global variables and constants

localScope :: Context -> Map Id Type

Input parameters and local variables

mutableVars :: Context -> Map Id Type

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

allVars :: Context -> Map Id Type

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

allNames :: Context -> Map Id Type

All variables and constants (local-scope preferred)

funProcNames :: Context -> [Id]

Names of functions and procedures

funSig :: Id -> Context -> FSig

Function signature by name

procSig :: Id -> Context -> PSig

Procedure signature by name

setLocals :: Map Id Type -> Context -> Context

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

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 -> Context

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 -> Context

Local context of a quantified expression