Class: TRuby::SMTTypeChecker

Inherits:
TypeChecker show all
Includes:
TRuby::SMT::DSL
Defined in:
lib/t_ruby/type_checker.rb

Overview

SMT-enhanced type checker with constraint solving

Instance Attribute Summary

Attributes inherited from TypeChecker

#errors, #hierarchy, #inferencer, #smt_solver, #use_smt, #warnings

Instance Method Summary collapse

Methods included from TRuby::SMT::DSL

#all, #any, #concrete, #has_property, #subtype, #type_equal, #type_var, #var

Methods inherited from TypeChecker

#check_assignment, #check_call, #check_function, #check_function_legacy, #check_interface, #check_method_with_smt, #check_operator, #check_program, #check_program_legacy, #check_property_access, #check_return, #check_statement, #diagnostics, #infer_param_type, #known_type?, #narrow_in_conditional, #register_alias, #register_function, #reset, #resolve_type, #subtype_with_smt?, #to_smt_type, #validate_type

Constructor Details

#initialize ⇒ SMTTypeChecker

Returns a new instance of SMTTypeChecker.



747
748
749
 
# File 'lib/t_ruby/type_checker.rb', line 747

def initialize
  super(use_smt: true)
end

Instance Method Details

#check_with_constraints(ir_program, &block) ⇒ Object

Add constraint-based type check



752
753
754
755
756
757
758
 
# File 'lib/t_ruby/type_checker.rb', line 752

def check_with_constraints(ir_program, &block)
  # Allow users to add custom constraints
  block.call(@smt_solver) if block_given?

  # Run standard type checking
  check_program(ir_program)
end

#inferred_type(var_name) ⇒ Object

Get inferred type for a variable



766
767
768
 
# File 'lib/t_ruby/type_checker.rb', line 766

def inferred_type(var_name)
  @smt_solver.infer(SMT::TypeVar.new(var_name))
end

#solve_constraints ⇒ Object

Solve current constraints and return solution



761
762
763
 
# File 'lib/t_ruby/type_checker.rb', line 761

def solve_constraints
  @smt_solver.solve
end