Class: TRuby::SMT::TypeInferenceEngine

Inherits:
Object
  • Object
show all
Defined in:
lib/t_ruby/smt_solver.rb

Overview

Type Inference Engine using SMT

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ TypeInferenceEngine

Returns a new instance of TypeInferenceEngine.



824
825
826
827
 
# File 'lib/t_ruby/smt_solver.rb', line 824

def initialize
  @solver = ConstraintSolver.new
  @type_env = {} # Variable name -> Type
end

Instance Attribute Details

#solver ⇒ Object (readonly)

Returns the value of attribute solver.



822
823
824
 
# File 'lib/t_ruby/smt_solver.rb', line 822

def solver
  @solver
end

#type_env ⇒ Object (readonly)

Returns the value of attribute type_env.



822
823
824
 
# File 'lib/t_ruby/smt_solver.rb', line 822

def type_env
  @type_env
end

Instance Method Details

#infer_body(body_ir, expected_return) ⇒ Object

Generate constraints from method body



880
881
882
883
884
885
886
887
888
889
890
891
892
 
# File 'lib/t_ruby/smt_solver.rb', line 880

def infer_body(body_ir, expected_return)
  case body_ir
  when IR::Block
    body_ir.statements.each do |stmt|
      infer_statement(stmt, expected_return)
    end
  when IR::Return
    if body_ir.value
      value_type = infer_expression(body_ir.value)
      @solver.add_subtype(value_type, expected_return)
    end
  end
end

#infer_expression(expr) ⇒ Object

Infer expression type



918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
 
# File 'lib/t_ruby/smt_solver.rb', line 918

def infer_expression(expr)
  case expr
  when IR::Literal
    ConcreteType.new(literal_type(expr.literal_type))
  when IR::VariableRef
    @type_env[expr.name] || @solver.fresh_var("V_#{expr.name}")
  when IR::MethodCall
    infer_method_call(expr)
  when IR::BinaryOp
    infer_binary_op(expr)
  when IR::ArrayLiteral
    infer_array_literal(expr)
  else
    @solver.fresh_var("E")
  end
end

#infer_method(method_ir) ⇒ Object

Infer types for a method



830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
 
# File 'lib/t_ruby/smt_solver.rb', line 830

def infer_method(method_ir)
  param_types = {}

  # Create type variables for parameters without annotations
  method_ir.params.each do |param|
    param_types[param.name] = if param.type_annotation
                                type_from_ir(param.type_annotation)
                              else
                                @solver.fresh_var("P_#{param.name}")
                              end
    @type_env[param.name] = param_types[param.name]
  end

  # Create type variable for return type if not annotated
  return_type = if method_ir.return_type
                  type_from_ir(method_ir.return_type)
                else
                  @solver.fresh_var("R_#{method_ir.name}")
                end

  # Analyze body to generate constraints
  if method_ir.body
    infer_body(method_ir.body, return_type)
  end

  # Solve constraints
  result = @solver.solve

  if result[:success]
    # Build inferred signature
    inferred_params = param_types.transform_values do |type|
      resolve_type(type, result[:solution])
    end

    inferred_return = resolve_type(return_type, result[:solution])

    {
      success: true,
      params: inferred_params,
      return_type: inferred_return,
    }
  else
    {
      success: false,
      errors: result[:errors],
    }
  end
end

#infer_statement(stmt, expected_return) ⇒ Object

Infer statement



895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
 
# File 'lib/t_ruby/smt_solver.rb', line 895

def infer_statement(stmt, expected_return)
  case stmt
  when IR::Assignment
    value_type = infer_expression(stmt.value)
    @type_env[stmt.target] = value_type

    if stmt.type_annotation
      annotated = type_from_ir(stmt.type_annotation)
      @solver.add_subtype(value_type, annotated)
    end
  when IR::Return
    if stmt.value
      value_type = infer_expression(stmt.value)
      @solver.add_subtype(value_type, expected_return)
    end
  when IR::Conditional
    infer_expression(stmt.condition)
    infer_body(stmt.then_branch, expected_return) if stmt.then_branch
    infer_body(stmt.else_branch, expected_return) if stmt.else_branch
  end
end