View Source cure_guard_refinement (cure v0.7.0)

Guard-Based Type Refinement

This module implements Phase 3 of the guard support implementation: type system integration for guard constraints.

Features

Guard Constraint Extraction

Extract constraints from function guards and convert them to refinement type predicates:

def abs(x: Int): Int when x >= 0 = x
% Refines x's type to: Int when x >= 0

Flow-Sensitive Type Narrowing

Within a function body, parameters have their types refined based on the guard:

def process(x: Int) when x > 0 = 
    % Here, x has type: Int when x > 0 (i.e., Positive)
    requires_positive(x)

Cross-Clause Type Checking

Verify that all clauses of a multi-clause function have compatible return types:

def abs(x: Int): Int when x >= 0 = x
def abs(x: Int): Int when x < 0 = -x
% Return type unifies to: Int

Integration

This module integrates with:

cure_refinement_types - For creating refinement type predicates
cure_typechecker - For enhancing function clause type checking
cure_guard_optimizer - For guard simplification and SMT encoding
cure_smt_solver - For constraint verification

Implementation Approach

Extract Guard Constraints: Parse guard expressions to identify parameter constraints
Create Refinement Types: Convert guards to refinement type predicates
Narrow Parameter Types: Replace parameter types with refined versions in function body scope
Unify Return Types: Compute union type of all clause return types
Verify Consistency: Use SMT to check guards are consistent and complete

Summary

Types

expr()

type_expr()

Functions

apply_guard_refinements(Env, Params, Guard)

build_guard_disjunction/1

check_clause_compatibility(Clause1, Clause2)

check_guard_coverage(Clauses, Env)

compute_function_return_type(Clauses, Env)

create_refinement_from_guard(ParamName, BaseType, Constraints)

create_union_refinement_type(BaseType, Var, LeftConstraint, RightConstraint)

detect_unreachable_clauses(Clauses)

extract_disjunctive_branches/1

extract_guard_constraints/1

extract_param_constraints(ParamName, Guard)

find_counterexamples_smt(Guards, Env)

find_uncovered_cases(Clauses, Env)

identify_constrained_params(Guard)

is_disjunctive_constraint/1

narrow_param_types_in_body(Env, Params, Guard)

negate_comparison_op/1

negate_guard_expression/1

refine_param_type(ParamName, BaseType, Guard)

strengthen_environment(Env, ParamName, Constraint)

unify_clause_return_types(Clauses, 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()} |
          #vector_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()} |
          #forall_expr{variables :: term(), body :: term(), location :: term()} |
          #exists_expr{variables :: 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()} |
          #melquiades_send_expr{message :: term(), target :: term(), location :: term()} |
          #qualified_call_expr{trait_name :: term(),
                               type_args :: term(),
                               method_name :: term(),
                               receiver :: term(),
                               args :: term(),
                               location :: term()}.

type_expr()

-type type_expr() ::
          #primitive_type{name :: term(), location :: term()} |
          #dependent_type{name :: term(),
                          type_params :: term(),
                          value_params :: term(),
                          location :: term()} |
          #function_type{params :: term(), return_type :: term(), location :: term()} |
          #union_type{types :: term(), location :: term()} |
          #list_type{element_type :: term(), length :: term(), location :: term()} |
          #tuple_type{element_types :: term(), location :: term()} |
          #fsm_type{name :: term(), states :: term(), message_types :: term(), location :: term()} |
          #process_type{fsm_type :: term(), current_state :: term(), location :: term()} |
          #genserver_ref_type{variant :: term(), location :: term()}.

Functions

apply_guard_refinements(Env, Params, Guard)

-spec apply_guard_refinements(map(),
                              [#param{name :: term(), type :: term(), location :: term()}],
                              expr()) ->
                                 map().

build_guard_disjunction/1

check_clause_compatibility(Clause1, Clause2)

-spec check_clause_compatibility(#function_clause{params :: term(),
                                                  return_type :: term(),
                                                  constraint :: term(),
                                                  body :: term(),
                                                  location :: term()},
                                 #function_clause{params :: term(),
                                                  return_type :: term(),
                                                  constraint :: term(),
                                                  body :: term(),
                                                  location :: term()}) ->
                                    compatible | overlapping | unreachable.

check_guard_coverage(Clauses, Env)

-spec check_guard_coverage([#function_clause{params :: term(),
                                             return_type :: term(),
                                             constraint :: term(),
                                             body :: term(),
                                             location :: term()}],
                           map()) ->
                              complete | {incomplete, [term()]}.

compute_function_return_type(Clauses, Env)

-spec compute_function_return_type([#function_clause{params :: term(),
                                                     return_type :: term(),
                                                     constraint :: term(),
                                                     body :: term(),
                                                     location :: term()}],
                                   map()) ->
                                      {ok, type_expr()} | {error, term()}.

create_refinement_from_guard(ParamName, BaseType, Constraints)

-spec create_refinement_from_guard(atom(), type_expr(), [expr()]) -> type_expr().

create_union_refinement_type(BaseType, Var, LeftConstraint, RightConstraint)

-spec create_union_refinement_type(type_expr(), atom(), expr(), expr()) -> type_expr().

detect_unreachable_clauses(Clauses)

-spec detect_unreachable_clauses([#function_clause{params :: term(),
                                                   return_type :: term(),
                                                   constraint :: term(),
                                                   body :: term(),
                                                   location :: term()}]) ->
                                    [integer()].

extract_disjunctive_branches/1

-spec extract_disjunctive_branches(expr()) -> {expr(), expr()} | error.

extract_guard_constraints/1

-spec extract_guard_constraints(expr()) -> [{atom(), expr()}].

extract_param_constraints(ParamName, Guard)

-spec extract_param_constraints(atom(), expr()) -> [expr()].

find_counterexamples_smt(Guards, Env)

find_uncovered_cases(Clauses, Env)

-spec find_uncovered_cases([#function_clause{params :: term(),
                                             return_type :: term(),
                                             constraint :: term(),
                                             body :: term(),
                                             location :: term()}],
                           map()) ->
                              [term()].

identify_constrained_params(Guard)

-spec identify_constrained_params(expr()) -> [atom()].

is_disjunctive_constraint/1

-spec is_disjunctive_constraint(expr()) -> boolean().

narrow_param_types_in_body(Env, Params, Guard)

-spec narrow_param_types_in_body(map(),
                                 [#param{name :: term(), type :: term(), location :: term()}],
                                 expr()) ->
                                    map().

negate_comparison_op/1

negate_guard_expression/1

refine_param_type(ParamName, BaseType, Guard)

-spec refine_param_type(atom(), type_expr(), expr()) -> type_expr().

strengthen_environment(Env, ParamName, Constraint)

-spec strengthen_environment(map(), atom(), expr()) -> map().

unify_clause_return_types(Clauses, Env)

-spec unify_clause_return_types([#function_clause{params :: term(),
                                                  return_type :: term(),
                                                  constraint :: term(),
                                                  body :: term(),
                                                  location :: term()}],
                                map()) ->
                                   {ok, type_expr()} | {error, term()}.