View Source cure_typechecker (cure v0.1.0)
Cure Programming Language - Type Checker
The type checker module provides high-level type checking functionality for Cure programs. It works with parsed AST nodes and implements comprehensive static type analysis including dependent type verification, constraint solving, and type inference.
Features
Comprehensive Type Checking
- Program-Level Analysis: Full program type checking with module support
- Function Type Checking: Parameter and return type verification
- Expression Type Inference: Bottom-up type inference for all expressions
- Dependent Type Support: Verification of dependent type constraints
Module System Support
- Module Scoping: Proper scoping of types and functions within modules
- Export Verification: Ensures exported functions exist and have correct types
- Import Resolution: Type-safe import of functions and types from other modules
- Two-Pass Processing: Collects signatures before checking bodies
Advanced Type Features
- Generic Functions: Full support for parametric polymorphism
- Constraint Solving: Integration with SMT-based constraint solving
- FSM Type Checking: Verification of finite state machine definitions
- Erlang Interop: Type checking for Erlang function interfaces
Error Reporting
- Detailed Error Messages: Precise error locations with helpful descriptions
- Warning System: Non-fatal issues that may indicate problems
- Error Recovery: Continues checking after errors to find more issues
- Structured Results: Machine-readable error and warning information
Type Checking Process
1. Environment Setup
Env = cure_typechecker:builtin_env(), % Built-in types and functions
R esult = cure_typechecker:check_program(AST).2. Module Processing
- Signature Collection: First pass collects all function signatures
- Body Checking: Second pass verifies function bodies against signatures
- Export Validation: Ensures all exported items are properly typed
3. Function Analysis
- Parameter Processing: Converts parameter types to environment bindings
- Constraint Checking: Verifies function constraints are boolean expressions
- Body Inference: Infers body type and checks against declared return type
- Generic Resolution: Resolves type parameters and constraints
Usage Examples
Program Type Checking
AST = cure_parser:parse_file("example.cure"),
Result = cure_typechecker:check_program(AST),
case Result#typecheck_result.success of
true ->
cure_utils:debug("Type checking successful~n");
false ->
Errors = Result#typecheck_result.errors,
cure_utils:debug("Type errors: ~p~n", [Errors])
end.Function Type Checking
FuncAST = #function_def{name = add, params = Params, body = Body, ...},
{ok, Env, Result} = cure_typechecker:check_function(FuncAST).Expression Type Inference
{ok, Type} = cure_typechecker:check_expression(ExprAST, Environment).Type Checking Results
Returns structured results with:
- Success Flag: Overall type checking success/failure
- Inferred Types: Types inferred for expressions and functions
- Error List: Detailed error information with locations
- Warnings: Non-fatal issues found during checking
Built-in Environment
Provides built-in types and functions:
- Primitive Types: Int, Float, String, Bool, Atom
- Type Constructors: List, Tuple, Map, Vector
- Standard Functions: Arithmetic, logical, and utility functions
- FSM Operations: Built-in FSM manipulati on functions
Integration
This module integrates with:
- cure_types: Core type system operations
- cure_parser: Processes parsed AST nodes
- cure_smt_solver: Constraint solving for dependent types
- cure_type_optimizer: Provides type information for optimizations
Error Categories
- Type Mismatches: Incompatible type assignments or operations
- Undefined Variables: References to unbound variables
- Constraint Violations: Failed dependent type constraints
- Export Errors: Missing or incorrectly typed exported functions
- Import Errors: Invalid module imports or type mismatches
Performance
- Two-Pass Efficiency: Minimizes redundant type checking
- Incremental Checking: Supports incremental compilation scenarios
- Constraint Caching: Reuses constraint solving results where possible
- Environment Sharing: Efficient environment management
Thread Safety
The type checker is stateless and thread-safe. Multiple type checking operations can run concurrently on different ASTs.
Summary
Functions
Type checks an entire Cure program.
Functions
Type checks an entire Cure program.
Performs comprehensive type checking of all top-level items in the program including modules, functions, FSMs, and type definitions.
Arguments
AST- List of top-level AST items from the parser
Returns
typecheck_result()- Complete type checking results including:success- Boolean indicating overall success/failuretype- Program type (usually undefined for programs)errors- List of type checking errors foundwarnings- List of warnings found
Example
AST = cure_parser:parse_file("example.cure"),
Result = cure_typechecker:check_program(AST),
case Result#typecheck_result.success of
true ->
cure_utils:debug("Program type checks successfully~n");
false ->
lists:foreach(fun(Error) ->
cure_utils:debug("Error: ~s~n", [Error#typecheck_error.message])
end, Result#typecheck_result.errors)
end.Features
- Built-in Environment: Uses standard built-in types and functions
- Error Recovery: Continues checking after errors to find more issues
- Two-Pass Processing: Collects signatures before checking implementations".