Safe Haskell | None |
---|
Type checker for Boogie 2
- typeCheckProgram :: Program -> Either [TypeError] Context
- exprType :: Context -> Expression -> Type
- resolve :: Context -> Type -> Type
- data TypeError = TypeError SourcePos Doc
- typeErrorsDoc :: [TypeError] -> Doc
- 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
- ctxTypeVars :: [Id]
- ctxIns :: Map Id Type
- ctxLocals :: Map Id Type
- ctxModifies :: [Id]
- ctxLabels :: [Id]
- ctxEncLabels :: [Id]
- ctxTwoState :: Bool
- ctxInLoop :: Bool
- ctxPos :: SourcePos
- ctxFreshTVCount :: Integer
- 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
- setLocals :: Map Id Type -> Context -> Context
- enterFunction :: FSig -> [Id] -> [Expression] -> Context -> Context
- enterProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Context -> Context
- enterQuantified :: [Id] -> [IdType] -> Context -> Context
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
Type error with a source position and a pretty-printed message
typeErrorsDoc :: [TypeError] -> DocSource
Pretty-printed list of type errors
Typing context
Typing 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] -> 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