Safe Haskell | Safe-Inferred |
---|
Type checker for Boogie 2
- checkProgram :: Program -> Checked Context
- exprType :: Context -> Expression -> Type
- resolve :: Context -> Type -> Type
- data TypeError = TypeError SourcePos Doc
- typeErrorsDoc :: [TypeError] -> Doc
- type Checked a = Either [TypeError] a
- data Context = Context {
- ctxTypeConstructors :: Map Id Int
- ctxTypeSynonyms :: Map Id ([Id], Type)
- ctxGlobals :: Map Id Type
- ctxConstants :: Map Id Type
- ctxFunctions :: Map Id FSig
- ctxProcedures :: Map Id PSig
- ctxWhere :: Map Id Expression
- ctxTypeVars :: [Id]
- ctxIns :: Map Id Type
- ctxLocals :: Map Id Type
- ctxModifies :: [Id]
- ctxLabels :: [Id]
- ctxEncLabels :: [Id]
- ctxTwoState :: Bool
- ctxInLoop :: Bool
- ctxPos :: SourcePos
- emptyContext :: Context
- typeNames :: Context -> [Id]
- globalScope :: Context -> Map Id Type
- localScope :: Context -> Map Id Type
- mutableVars :: Context -> Map Id Type
- allVars :: Context -> Map Id Type
- allNames :: Context -> Map Id Type
- funProcNames :: Context -> [Id]
- funSig :: Id -> Context -> FSig
- procSig :: Id -> Context -> PSig
- setGlobals :: Context -> Map Id Type -> Context
- setIns :: Context -> Map Id Type -> Context
- setLocals :: Context -> Map Id Type -> Context
- setConstants :: Context -> Map Id Type -> Context
- enterFunction :: FSig -> [Id] -> [Expression] -> Maybe Type -> Context -> Context
- enterProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Context -> Context
- enterQuantified :: [Id] -> [IdType] -> Context -> Context
Checking programs
checkProgram :: Program -> Checked ContextSource
checkProgram
p
: Check program p
and return the type information in the global part of the context
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
Type error with a source position and a pretty-printed message
typeErrorsDoc :: [TypeError] -> DocSource
Pretty-printed list of type errors
Typechecking context
Typechecking context
Context | |
|
Empty context
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)
funProcNames :: Context -> [Id]Source
Names of functions and procedures
enterFunction :: FSig -> [Id] -> [Expression] -> Maybe Type -> 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