View Source cure_guard_codegen (cure v0.1.0)

Guard Validation Code Generation

This module generates runtime validation code for dependent type guards. It translates guard constraints into executable BEAM code that validates values against dependent type requirements.

Features

  • Dependent Type Validation: Generate checks for dependent type constraints
  • Optimized Code: Efficient guard code with minimal runtime overhead
  • SMT Integration: Use SMT solver results to optimize guard checks
  • Error Reporting: Generate informative error messages for failed guards

Guard Types

Numeric Constraints 

Vector(T, n: Nat) when n > 0

Generates: Runtime check that n > 0

Refinement Types 

NonEmpty(T) = List(T, n) when n > 0

Generates: Length check for lists

Complex Constraints 

Matrix(T, rows: Nat, cols: Nat) when rows > 0 and cols > 0

Generates: Multiple validation checks

Code Generation Strategy

  1. Static Analysis: Use SMT solver to prove constraints at compile time
  2. Runtime Guards: Generate checks for constraints that can't be proven
  3. Optimization: Eliminate redundant checks through dataflow analysis
  4. Caching: Cache validation results for expensive computations

Summary

Types

expr()

Functions

clear_proof_cache()
compile_constraint(Constraint, Env)
generate_guard(Constraint, Env)
generate_guard(Constraint, Env, Opts)
generate_validation_function(TypeName, Params, Constraint)
optimize_guard(GuardAST, Env)

Types

expr()

-type expr() ::
          #literal_expr{value :: term(), location :: term()} |
          #identifier_expr{name :: term(), location :: term()} |
          #function_call_expr{function :: term(), args :: term(), location :: term()} |
          #match_expr{expr :: term(), patterns :: term(), location :: term()} |
          #let_expr{bindings :: term(), body :: term(), location :: term()} |
          #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} |
          #unary_op_expr{op :: term(), operand :: term(), location :: term()} |
          #list_expr{elements :: term(), location :: term()} |
          #tuple_expr{elements :: term(), location :: term()} |
          #record_expr{name :: term(), fields :: term(), location :: term()} |
          #field_access_expr{record :: term(), field :: term(), location :: term()} |
          #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} |
          #lambda_expr{params :: term(), body :: term(), location :: term()} |
          #fsm_spawn_expr{fsm_name :: term(),
                          init_args :: term(),
                          init_state :: term(),
                          location :: term()} |
          #fsm_send_expr{target :: term(), message :: term(), location :: term()} |
          #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} |
          #fsm_state_expr{location :: term()} |
          #qualified_call_expr{trait_name :: term(),
                               type_args :: term(),
                               method_name :: term(),
                               receiver :: term(),
                               args :: term(),
                               location :: term()}.

Functions

clear_proof_cache()

compile_constraint(Constraint, Env)

-spec compile_constraint(expr(), map()) -> {ok, erl_syntax:syntaxTree()} | {error, term()}.

generate_guard(Constraint, Env)

-spec generate_guard(expr(), map()) -> {ok, erl_syntax:syntaxTree()} | {error, term()}.

generate_guard(Constraint, Env, Opts)

-spec generate_guard(expr(), map(), map()) -> {ok, erl_syntax:syntaxTree()} | {error, term()}.

generate_validation_function(TypeName, Params, Constraint)

-spec generate_validation_function(atom(),
                                   [#param{name :: term(), type :: term(), location :: term()}],
                                   expr()) ->
                                      {ok, erl_syntax:syntaxTree()}.

optimize_guard(GuardAST, Env)

-spec optimize_guard(erl_syntax:syntaxTree(), map()) -> erl_syntax:syntaxTree().