module Steep
  module TypeInference
    # TypeEnv is the one-stop class to manage type of variables.
    #
    # ### Local variables primitive operations
    #
    # * Assigning to a local variable
    # * Adding local variable type enforcement
    # * Refine local variable types
    # * Resetting refinements
    #
    # ### Pure calls primitive operations
    #
    # * Adding pure calls
    # * Removing pure calls
    # * Refine pure call types
    # * Resetting pure call refinements
    #
    # ### Branch operations
    #
    # * Start branching with refinements
    # * Merge branches
    #
    #
    class TypeEnv
      include NodeHelper

      type local_variable_entry = [AST::Types::t, AST::Types::t?]

      attr_reader local_variable_types: Hash[Symbol, local_variable_entry]

      attr_reader pure_method_calls: Hash[Parser::AST::Node, [MethodCall::Typed, AST::Types::t?]]

      attr_reader instance_variable_types: Hash[Symbol, AST::Types::t]

      attr_reader global_types: Hash[Symbol, AST::Types::t]

      attr_reader constant_types: Hash[RBS::TypeName, AST::Types::t]

      attr_reader constant_env: ConstantEnv

      @pure_node_descendants: Hash[Parser::AST::Node, Set[Parser::AST::Node]]

      def initialize: (
          ConstantEnv,
          ?local_variable_types: Hash[Symbol, local_variable_entry],
          ?instance_variable_types: Hash[Symbol, AST::Types::t],
          ?global_types: Hash[Symbol, AST::Types::t],
          ?constant_types: Hash[RBS::TypeName, AST::Types::t],
          ?pure_method_calls: Hash[Parser::AST::Node, [MethodCall::Typed, AST::Types::t?]]
        ) -> void

      def update: (
          ?local_variable_types: Hash[Symbol, local_variable_entry],
          ?instance_variable_types: Hash[Symbol, AST::Types::t],
          ?global_types: Hash[Symbol, AST::Types::t],
          ?constant_types: Hash[RBS::TypeName, AST::Types::t],
          ?pure_method_calls: Hash[Parser::AST::Node, [MethodCall::Typed, AST::Types::t?]]
        ) -> TypeEnv

      def merge: (
          ?local_variable_types: Hash[Symbol, local_variable_entry],
          ?instance_variable_types: Hash[Symbol, AST::Types::t],
          ?global_types: Hash[Symbol, AST::Types::t],
          ?constant_types: Hash[RBS::TypeName, AST::Types::t],
          ?pure_method_calls: Hash[Parser::AST::Node, [MethodCall::Typed, AST::Types::t?]]
        ) -> TypeEnv

      # Returns type of `name`.
      #
      def []: (Symbol name) -> AST::Types::t?
            | (Parser::AST::Node node) -> AST::Types::t?

      # Tells the environment that local variables are updated.
      # Keeps their enforced types and invalidates related nodes.
      #
      def assign_local_variables: (Hash[Symbol, AST::Types::t]) -> TypeEnv

      # Tells the environment that the local variable is updated with it's enforced type.
      #
      # Invalidates related nodes.
      #
      def assign_local_variable: (Symbol name, AST::Types::t type, AST::Types::t? enforced_type) -> TypeEnv

      # Refines types of local variables and pure calls.
      #
      # * Receives types of updated local variables and pure calls.
      # * The local variable types will be
      #
      def refine_types: (?local_variable_types: Hash[Symbol, AST::Types::t], ?pure_call_types: Hash[Parser::AST::Node, AST::Types::t]) -> TypeEnv

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

      # Returns type of constant of `const_name`, or `const_name` under `mod_name`.
      #
      # Returns `nil` if no such constant found.
      #
      def constant: (Symbol const_name, bool toplevel) -> ConstantEnv::constant_tuple?
                  | (RBS::TypeName mod_name, Symbol const_name) -> ConstantEnv::constant_tuple?

      def annotated_constant: (RBS::TypeName) -> AST::Types::t?

      # _Pin_ the local variables if array is given.
      # When `nil` is given, all local variables are _pinned_.
      #
      def pin_local_variables: (Array[Symbol]? names) -> Hash[Symbol, local_variable_entry]

      # _Unpin_ the local variables if array is given.
      # When `nil` is given, all local variables are _unpinned_.
      #
      def unpin_local_variables: (Array[Symbol]? names) -> TypeEnv

      def to_s: () -> String

      # Apply the substitution to the type of local variables.
      #
      def subst: (Interface::Substitution) -> TypeEnv

      # Returns a `TypeEnv` such that:
      #
      # * All of the given environments are result of the type checking of branches from `self`,
      # * All of the branches meet at one point, with the returned `TypeEnv`
      #
      # See the example below:
      #
      # ```ruby
      # if foo()         # The original environment `self` is for after the evaluation of `foo()`
      #   a = bar()      # One environment `env1` can be given from after the evaluation of `bar()`
      # else
      #   b = baz()      # Another environment `env2` is from after the evaluation of `baz`
      # end
      #
      # ???              # How is the environment for here is `self.merge(env1, env2)`
      #                  # The environment has both optional types of `a` and `b`
      # ```
      #
      def join: (*TypeEnv) -> TypeEnv

      def add_pure_call: (Parser::AST::Node, MethodCall::Typed, AST::Types::t?) -> TypeEnv

      def replace_pure_call_type: (Parser::AST::Node, AST::Types::t) -> TypeEnv

      def invalidate_pure_node: (Parser::AST::Node) -> TypeEnv

      private

      def pure_node_invalidation: (Enumerable[Parser::AST::Node] invalidated_nodes) -> Hash[Parser::AST::Node, [MethodCall::Typed, AST::Types::t?]]

      def invalidated_pure_nodes: (Parser::AST::Node) -> Set[Parser::AST::Node]

      def local_variable_name?: (Symbol) -> bool

      def local_variable_name!: (Symbol) -> void

      def instance_variable_name?: (Symbol) -> bool

      def global_name?: (Symbol) -> bool
    end
  end
end