module Steep
  module TypeInference
    class LogicTypeInterpreter
      class Result
        attr_reader env: TypeEnv

        attr_reader type: AST::Types::t

        attr_accessor unreachable: bool

        def initialize: (env: TypeEnv, type: AST::Types::t, unreachable: bool) -> void

        def update_env: () { () -> TypeEnv } -> Result

        def update_type: { () -> AST::Types::t } -> Result

        # Make the instance unreachable, and returns self
        #
        def unreachable!: () -> self
      end

      TRUE: AST::Types::Literal

      FALSE: AST::Types::Literal

      BOOL: AST::Types::Boolean

      BOT: AST::Types::Bot

      UNTYPED: AST::Types::Any

      attr_reader subtyping: Subtyping::Check

      attr_reader typing: Typing

      attr_reader factory (): AST::Types::Factory

      attr_reader config: Interface::Builder::Config

      def initialize: (subtyping: Subtyping::Check, typing: Typing, config: Interface::Builder::Config) -> void

      def eval: (env: TypeEnv, node: Parser::AST::Node) -> [Result, Result]

      def evaluate_node: (env: TypeEnv, node: Parser::AST::Node, ?type: AST::Types::t) -> [Result, Result]

      def evaluate_method_call: (env: TypeEnv, type: AST::Types::Logic::Base, receiver: Parser::AST::Node?, arguments: Array[Parser::AST::Node]) -> [Result, Result]?

      # Apply type refinement to `node` as `truthy_type` and `falsy_type`.
      #
      # This is done by top-down manner.
      #
      # Assignes given two types to the node when:
      #
      # * `node` is a `lvar`
      # * `node` is a `lvasgn`
      # * `node` is a _pure_ method call
      #
      def refine_node_type: (env: TypeEnv, node: Parser::AST::Node, truthy_type: AST::Types::t, falsy_type: AST::Types::t) -> [TypeEnv, TypeEnv]

      # Returns a pair of a node and set of local variable names.
      #
      # * The returned node is called _value node_ that is a node the value of given `node` can be taken from
      # * The local variable names are local variables that have the same value of the _value node_.
      #
      # ```ruby
      # a = 123   # `123` is the _value node_
      #           # :a is included in the set because `a` has the same value of _value node_
      #
      # c = b = a  # `a` is the _value node_, a set of { :b, :c } will be returned
      # ```
      #
      def decompose_value: (Parser::AST::Node node) -> [Parser::AST::Node, Set[Symbol]]

      private

      # Assign local variables included in the assignment node and masgn node
      #
      def evaluate_assignment: (Parser::AST::Node node, TypeEnv env, AST::Types::t rhs_type) -> TypeEnv

      def guess_type_from_method: (Parser::AST::Node node) -> (AST::Types::Logic::ReceiverIsArg | AST::Types::Logic::ReceiverIsNil | AST::Types::Logic::Not | AST::Types::Logic::ArgIsReceiver | nil)

      # Decompose to given type to truthy and falsy types.
      #
      # This directly corresponds to case-when syntax with literals:
      #
      # ```ruby
      # case x
      # when nil       # value_node == {nil}, arg_type = type_of({x})
      #   ...
      # when 123       # value_node == {nil}, arg_type = type_of({x})
      #   ...
      # end
      # ```
      #
      def literal_var_type_case_select: (Parser::AST::Node value_node, AST::Types::t arg_type) -> [Array[AST::Types::t], Array[AST::Types::t]]?

      def type_case_select: (AST::Types::t `type`, RBS::TypeName klass) -> [AST::Types::t?, AST::Types::t?]

      def type_case_select0: (AST::Types::t `type`, RBS::TypeName klass) -> [Array[AST::Types::t], Array[AST::Types::t]]

      def try_convert: (AST::Types::t, Symbol) -> AST::Types::t?

      def no_subtyping?: (sub_type: AST::Types::t, super_type: AST::Types::t) -> Subtyping::Result::t?

      def subtyping?: (sub_type: AST::Types::t, super_type: AST::Types::t) -> bool
    end
  end
end