| Copyright | (c) Henry J. Wylde, 2015 |
|---|---|
| License | BSD3 |
| Maintainer | public@hjwylde.com |
| Safe Haskell | None |
| Language | Haskell2010 |
Language.Qux.Annotated.TypeChecker
Description
Type checking functions to verify that a Program is type-safe.
These functions only verify that types are used correctly. They don't verify other properties such as definite assignment.
- type Check = ReaderT Context (Writer [TypeException])
- runCheck :: Check a -> Context -> (a, [TypeException])
- execCheck :: Check a -> Context -> [TypeException]
- data Context = Context {}
- context :: Program -> Context
- emptyContext :: Context
- type Locals = Map Id Type
- retrieve :: MonadReader Context m => Id -> StateT Locals m (Maybe [Type])
- check :: Program SourcePos -> [TypeException]
- checkProgram :: Program SourcePos -> Check ()
- checkDecl :: Decl SourcePos -> Check ()
- checkStmt :: Stmt SourcePos -> StateT Locals Check ()
- checkExpr :: Expr SourcePos -> StateT Locals Check Type
Environment
type Check = ReaderT Context (Writer [TypeException]) Source
A type that allows collecting errors while type checking a program.
Requires a Context for evaluation.
runCheck :: Check a -> Context -> (a, [TypeException]) Source
Runs the given check with the context.
execCheck :: Check a -> Context -> [TypeException] Source
Runs the given check with the context and extracts the exceptions.
Global context
Global context that holds function definition types.
emptyContext :: Context Source
An empty context.
Local context
type Locals = Map Id Type Source
Local context. This is a map of variable names to types (e.g., parameters).
retrieve :: MonadReader Context m => Id -> StateT Locals m (Maybe [Type]) Source
Retrieves the type of the given identifier. Preference is placed on local variables. A local variable type is a singleton list, while a function type is it's parameter types and return type.
Type checking
check :: Program SourcePos -> [TypeException] Source
Type checks the program, returning any errors that are found.
A result of [] indicates the program is well-typed.
checkProgram :: Program SourcePos -> Check () Source
Type checks a program.