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.



819
820
821
822
 
# File 'lib/t_ruby/smt_solver.rb', line 819

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

Instance Attribute Details

#solver ⇒ Object (readonly)

Returns the value of attribute solver.



817
818
819
 
# File 'lib/t_ruby/smt_solver.rb', line 817

def solver
  @solver
end

#type_env ⇒ Object (readonly)

Returns the value of attribute type_env.



817
818
819
 
# File 'lib/t_ruby/smt_solver.rb', line 817

def type_env
  @type_env
end

Instance Method Details

#infer_body(body_ir, expected_return) ⇒ Object

Generate constraints from method body



876
877
878
879
880
881
882
883
884
885
886
887
888
 
# File 'lib/t_ruby/smt_solver.rb', line 876

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



914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
 
# File 'lib/t_ruby/smt_solver.rb', line 914

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



825
826
827
828
829
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
 
# File 'lib/t_ruby/smt_solver.rb', line 825

def infer_method(method_ir)
  param_types = {}
  return_type = nil

  # Create type variables for parameters without annotations
  method_ir.params.each do |param|
    if param.type_annotation
      param_types[param.name] = type_from_ir(param.type_annotation)
    else
      param_types[param.name] = @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



891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
 
# File 'lib/t_ruby/smt_solver.rb', line 891

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