require 'set'

module TlaParserS

  class Resolver

    attr_reader :context                   # TlaParserS::Context
                                           # create context to resolve
                                           # references


    attr_reader :parser                    # TlaParserS::Parser to
                                           # parse TLA+ source code


    attr_reader :report_unresolved         # true if warn on unresolves

    attr_reader  :directives               # [String:Array] of names
                                           # for INVARIANTS and
                                           # ASSUMPTIONS

    attr_reader :directive_modules         # array of module names containing
                                           # directives
    
    # ******************************************************************
    # Load TLA+ snippets from file (or strings in unit test), and build
    # global context to use in resolving.
    #
    # constructor:
    # #initContext: add initContext
    # #initSnippets: parse TLA+ snippets to context
    # #resolveModules: resolve modules
    #
    # ******************************************************************
    

    # ------------------------------------------------------------------
    # Logger
    
    PROGNAME = "resolver"                  # progname for logger
    include TlaParserS::Utils::MyLogger    # mix logger

    # ------------------------------------------------------------------
    # constructore
    def initialize( options={} )
      
      @logger = getLogger( PROGNAME, options )
      @logger.info( "#{__method__} initialized" )

      @report_unresolved = options[:report_unresolved]


      @context = TlaParserS::Context.new( options )
      @parser  = TlaParserS::Parser.new( options )

      # initiall no directives
      @directives = []

      # initially no directive modules
      @directive_modules = []
    end

    # Parse entry ie. file or possibly a string
    #
    # @param entry [File|String] to parse
    # @param moduleName [String] identifying 'entry' for error messages
    # @return [Snippets] parsed syntax tree node 
    def parseSnippets( entry, moduleName )
        begin
          parser.parse( entry )
        rescue ParseException => ee
          msg = "Parsing '#{moduleName}' results to error \n\n#{ee.message}"
          @logger.error( "#{__method__} #{msg}" )        
          raise ParseException.new( ee ), msg, ee.backtrace
        end
          
    end

    # Add of definition names in 'snippets' to '@directives', and
    # 'moduleName' to '@directive_modules' if any 'snippets' contained
    # 'directive_definitions'
    #
    # @param moduleName [String] name of module where 'snippets' are parses
    # @param snippets [Snippets] parsed snippts, respons to :directive_definitions
    def addDirectives( snippets, moduleName )
      new_directives = snippets.directive_definitions
      
      @logger.debug( "#{__method__} moduleName=#{moduleName} -> new_directives=#{new_directives}" )
      @directives = directives + new_directives

      @directive_modules << moduleName if new_directives && new_directives.any?
    end

    # Build initial context (TLA+ reserved words, etc)
    #
    # @param names [String:Array] to put context
    def initContext( names )
      
      # create global context
      context.initEntries(
        names.map do |name|
          {
          :context_type => 'initalContext', 
          :context => "initalContext",
          :symbol_type => "initalContext",
          :symbol_name => name
          }
        end
      )

      
    end


    # ------------------------------------------------------------------
    # Load TLA+ snippets from file (or strings in unit test), and
    # build global context to use in resolving.
    #
    # @param entries [ File:Array | String:Array] containg TLA+ snippets
    #
    # @param blk [Block] yields entry 
    
    def initSnippets( entries, &blk )

      # create global context
      context.pushContext

      # iterate
      entries && entries.each_with_index do |entry,i|

        # skip directories
        # next if entry.is_a?( File ) && File.directory?( entry )
        next if File.directory?( entry )        

        # meaningfull modulename
        moduleName = entry.is_a?( File ) ? entry.path : "entries[#{i}]"

        @logger.info( "#{__method__} entry=#{entry}" )
        begin

          # String|File --> AST
          snippets = parseSnippets( entry, moduleName )
          yield( true, entry ) if blk

          # collect directive defitions
          addDirectives( snippets, moduleName )

          # add to contex tree nodes, which respond to
          # 'symbol_definitions'
          context.addContext( snippets, moduleName )
          
        rescue TlaParserS::ParseException => e

          # quit if no block - or block decides to quit
          if !blk ||  !yield( false, entry, e ) then
            raise e
          end
        end

      end

      self
    end

    # ------------------------------------------------------------------
    # Find modules 1) containing TLA+ snippets reachable from
    # 'entryPoints', 2) modules reachabable for directive defintision,
    # and 3) modules containing directive definitions
    #
    # @param entryPoints [String:Array] TLA+ definition names to implement
    # @return [String:Array] names of modules needed in implementation
    def resolveModules( entryPoints, &blk )
      definitionModules = resolveModulesDo( entryPoints + directives, &blk )
      return definitionModules + directive_modules
    end
    

    # ------------------------------------------------------------------
    # Find modules containing TLA+ snippets needed to implement code
    # for 'entryPoints'.  Notice: A module may include additional
    # entrypoint, which must also be satisfied.
    #
    # @param entryPoints [String:Array] TLA+ definition names to implement
    #
    # @param blk [Proc] called with (key, String:Array), where key \in
    # {'start', 'resolved', 'unresolved'}, and String:Array list of
    # symbols.
    # 
    # @return [String:Arrays] of module names needed in implementation.
    def resolveModulesDo( entryPoints, &blk )
      
      @logger.info( "#{__method__} resolveModules for entryPoint=#{entryPoints.join(',')}" )
      yield( "start", entryPoints ) if blk

      # collected during processing
      moduleNames = [].to_set

      # collect here
      unresolvedSymbols = []

      unResolved = entryPoints.to_set
      resolved = [].to_set

      while TRUE do

        # done - if no mode 'unResolved'
        break if unResolved.empty?
        # next to resolve
        entryPoint = unResolved.to_a.shift
        @logger.info( "#{__method__} next to resolve entryPoint #{entryPoint} " )              
        next if resolved.include?( entryPoint )

        # array of hashes how entry point is resolved
        resolvedSymbols = resolveEntryPoint( entryPoint )
        @logger.info( "#{__method__} entryPoint #{entryPoint} ->resolvedSymbols=#{resolvedSymbols}" )      

        resolvedModules =                  # array of mod.names
          resolvedSymbols.                 # { :symbol=>, :resolved=> }
          select { |e| e[:resolved] }.     # successfully resolved
          map { |e| e[:resolved] }.        # discard :symbol =>.. :resolved => ...
          select { |s| s[:module] }.       # defines module ie. not
                                           # TLA+ standar module, nor
                                           # local context
          map { |s| s[:module]  }          # extract moduleName

        
        @logger.debug( "#{__method__} resolvedModules=#{resolvedModules}" )
        newModules = resolvedModules.select { |m| !moduleNames.include?( m ) }

        # collect unresolved
        unresolvedSymbols +=
          resolvedSymbols.                 # { :symbol=>, :resolved=> }
          select { |r| r[:resolved].nil? }.# unresolved
          map{ |r|
          {
            :symbol => r[:symbol],
            :entry => entryPoint  }}       # add entry point causing error

        # return list of definitions (ie. newEntryPoint) in 'modules'
        newEntryPoints = entryPointsForModules( newModules )
        @logger.debug( "#{__method__} newEntryPoints=#{newEntryPoints}" )
        
        # one more resolved: move it to resolved
        unResolved = unResolved.delete( entryPoint )
        resolved = resolved.add( entryPoint )

        # still to resolve: unResolved + newEntryPoints - resolved
        unResolved = unResolved.union( newEntryPoints.to_set ).subtract( resolved )
        @logger.debug( "#{__method__} unResolved=#{unResolved}" )
        
        # collect modules
        moduleNames = moduleNames.union( newModules.to_set )
        
      end # looop for ever

      # warn on output unresolved - if option set
      reportUnresolved( unresolvedSymbols ) if report_unresolved
      yield( "resolved", resolved.to_a ) if blk        
      yield( "unresolved", unresolvedSymbols ) if blk  

      @logger.info( "#{__method__} resolve-result ->#{moduleNames.to_a}" )      
      # set --> array
      moduleNames.to_a
      
    end # resolveModules

    # Ouptput to stderr if 'unresolvedSymbols.any
    #
    # @param unresolvedSymbols [Hash:Array] of {:symbol,:entry} of unresolved symbols
    # 
    def reportUnresolved( unresolvedSymbols )

      warn <<-EOS if unresolvedSymbols.any?
      Unresolved symbols:
      -- #{unresolvedSymbols.map{ |u| 'Symbol \'' + u[:symbol] + '\' in entry \'' +  u[:entry] + '\''}.join("\n  -- ")} 
      EOS

    end

    # Return Hash:Array of symbols resolved in 'entryPoint'. First
    # locates 'entryPoint' syntax tree in 'context', and then
    # use 'resolveDefine' to resolve entries.
    #
    # @param entryPoint [String] name entry point to resolve
    #
    # @return [Hash:Array] identifier in entry points
    def resolveEntryPoint( entryPoint )
      symbolTableEntry = context.resolveSymbol( entryPoint )
      @logger.debug( "#{__method__} symbolTableEntry #{entryPoint}-->#{symbolTableEntry}" )
      if symbolTableEntry && symbolTableEntry[:resolved]
        tree = symbolTableEntry[:resolved][:tree]
        @logger.debug( "#{__method__} tree-->#{tree.inspect}" )      
        symbols = context.resolveDefine( tree )
        @logger.debug( "#{__method__} resolveDefine-->#{symbols.join('\n')}" )
      else
        msg = <<-EOS  
        Unknown entrypoint '#{entryPoint}'

        Known entry points: #{context.entries.join(',')}
        EOS
        @logger.error( "#{__method__} #{msg}" )        
        raise ResolverException.new msg
      end

      return [ symbolTableEntry ] +  symbols

    end

    # return list of definitions in 'modules'
    #
    # @param modules [String:Array] of module names to include
    # @return [String:Array] of entry points in the module
    def entryPointsForModules( modules )

      moduleSymbols = []
      modules.each do |moduleName|
        # resolve module entry poinsts
        moduleEntries = context.resolveModule( moduleName )
        
        moduleSymbols = moduleSymbols + moduleEntries
      end
      ret = moduleSymbols.map { |s| s[:symbol_name] }
      @logger.debug( "#{__method__} modules=#{modules.join(',')}-->ret=#{ret.join(',')}" )
      return ret
    end
    
  end

end