module Steep
  module Subtyping
    class Check
      ABORT_LIMIT: Integer

      attr_reader builder: Interface::Builder

      attr_reader cache: Cache

      @assumptions: Set[Relation[untyped]]?

      @bounds: Array[Hash[Symbol, AST::Types::t?]]

      @self_type: AST::Types::t?

      @instance_type: AST::Types::t?

      @class_type: AST::Types::t?

      @constraints: Constraints?

      def initialize: (builder: Interface::Builder) -> void

      def factory: () -> AST::Types::Factory

      def with_context: [A] (self_type: AST::Types::t?, instance_type: AST::Types::t?, class_type: AST::Types::t?, constraints: Constraints?) { () -> A } -> A

      def self_type: () -> AST::Types::t

      def instance_type: () -> AST::Types::t

      def class_type: () -> AST::Types::t

      def constraints: () -> Constraints

      def push_variable_bounds: [A] (Array[Interface::TypeParam] | Hash[Symbol, AST::Types::t?] params) { () -> A } -> A

      def variable_upper_bound: (Symbol name) -> AST::Types::t?

      def variable_upper_bounds: () -> Hash[Symbol, AST::Types::t?]

      def push_assumption: [A] (Relation[untyped] relation) { () -> A } -> A

      def assumptions: () -> Set[Relation[untyped]]

      def each_ancestor: (RBS::DefinitionBuilder::AncestorBuilder::OneAncestors ancestors) { (RBS::Definition::Ancestor::t) -> void } -> void
                       | (RBS::DefinitionBuilder::AncestorBuilder::OneAncestors ancestors) -> Enumerator[RBS::Definition::Ancestor::t, void]

      type super_type = AST::Types::Name::Instance | AST::Types::Name::Interface | AST::Types::Name::Singleton

      def instance_super_types: (RBS::TypeName type_name, args: Array[AST::Types::t]) -> Array[super_type]

      def singleton_super_types: (RBS::TypeName type_name) -> Array[super_type]

      def check: (Relation[AST::Types::t] relation, constraints: Constraints, self_type: AST::Types::t?, instance_type: AST::Types::t?, class_type: AST::Types::t?) -> Result::t

      def check_type: (Relation[AST::Types::t] relation) -> Result::t

      def cache_bounds: (Relation[AST::Types::t] relation) -> Hash[Symbol, AST::Types::t?]

      def alias?: (AST::Types::t `type`) -> bool

      def cacheable?: (Relation[AST::Types::t] relation) -> bool

      def true_type?: (AST::Types::t `type`) -> bool

      def false_type?: (AST::Types::t `type`) -> bool

      include Result::Helper

      def check_type0: (Relation[AST::Types::t] relation) -> Result::t

      def definition_for_type: (AST::Types::t `type`) -> RBS::Definition

      # Returns true if given `type` is with one or more type arguments.
      #
      def arg_type?: (AST::Types::t `type`) -> bool

      type application_type = AST::Types::Name::Instance | AST::Types::Name::Interface | AST::Types::Name::Alias

      def check_type_arg: (Relation[application_type] relation) -> untyped

      def same_type?: (Relation[AST::Types::t] relation) -> bool

      def check_interface: (Relation[Interface::Shape] relation) -> Result::t

      def check_method: (Symbol name, Relation[Interface::Shape::Entry] relation) -> Result::t

      def check_generic_method_type: (Symbol name, Relation[Interface::MethodType] relation) -> Result::t

      def check_constraints: (Relation[untyped] relation, variables: Enumerable[Symbol], variance: VariableVariance) -> Result::t

      def check_method_type: (Symbol name, Relation[Interface::MethodType] relation) -> Result::t

      # Receives subtyping relation of blocks `b <: b'` where `b` and `b'` are expanded from
      # subtyping relation of two method types `(...) _b_ -> T <: (...) _b'_ -> S`.
      #
      # Returns `true` is the relation is satisfied immediately.
      # Returns a Relation when the given relation can be expanded to relation between Interface::Block.
      # Returns a failure otherwise.
      #
      def expand_block_given: (Symbol name, Relation[Interface::Block?] relation) -> (Relation[Interface::Block] | true | Result::Failure)

      # Receives a subtyping relation between self bindings `S <: S'` that is included in procs or blocks as:
      #
      # *             `^() [self: S] -> T <: ^() [self: S'] -> T`           (proc)
      # * `() { () [self: S'] -> T } -> T <: () { () [self: S] -> T } -> T` (block in method type)
      #
      def check_self_type_binding: (Relation[untyped], AST::Types::t? sub_self, AST::Types::t? super_self) -> Result::t?

      def check_function: (Symbol name, Relation[Interface::Function] relation) -> Result::t

      def check_method_params: (Symbol name, Relation[Interface::Function::Params] relation) -> Result::t

      # Returns `nil` when given two method_types are structually comparable.
      # Returns a failure otherwise.
      #
      def match_method_type_fails?: (Symbol name, Interface::MethodType method_type1, Interface::MethodType method_type2) -> (nil | Result::t)

      def match_params: (Symbol name, Relation[Interface::Function::Params] relation) -> (Array[[AST::Types::t, AST::Types::t]] | Result::t)

      def expand_alias: (AST::Types::t `type`) -> AST::Types::t

      # Returns the shortest type paths for one of the _unknown_ type variables.
      # Returns nil if there is no path.
      def hole_path: (AST::Types::t `type`, ?Array[AST::Types::t] path) -> Array[AST::Types::t]?

      def Relation: [T < Relation::_Subject] (T sub, T sup) -> Relation[T]
    end
  end
end