Class: TlaParserS::Resolver

Inherits:
Object
  • Object
show all
Includes:
Utils::MyLogger
Defined in:
lib/semantics/resolver.rb

Constant Summary collapse

PROGNAME =

Logger

"resolver"

Constants included from Utils::MyLogger

Utils::MyLogger::LOGFILE

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Utils::MyLogger

#getLogger, #logfile

Constructor Details

#initialize(options = {}) ⇒ Resolver

constructore



45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
 
# File 'lib/semantics/resolver.rb', line 45

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

Instance Attribute Details

#context ⇒ Object (readonly)

Returns the value of attribute context.



7
8
9
 
# File 'lib/semantics/resolver.rb', line 7

def context
  @context
end

#directive_modules ⇒ Object (readonly)

String:Array

of names

for INVARIANTS and ASSUMPTIONS



22
23
24
 
# File 'lib/semantics/resolver.rb', line 22

def directive_modules
  @directive_modules
end

#directives ⇒ Object (readonly)

Returns the value of attribute directives.



18
19
20
 
# File 'lib/semantics/resolver.rb', line 18

def directives
  @directives
end

#parser ⇒ Object (readonly)

Returns the value of attribute parser.



12
13
14
 
# File 'lib/semantics/resolver.rb', line 12

def parser
  @parser
end

#report_unresolved ⇒ Object (readonly)

true if warn on unresolves



16
17
18
 
# File 'lib/semantics/resolver.rb', line 16

def report_unresolved
  @report_unresolved
end

Instance Method Details

#addDirectives(snippets, moduleName) ⇒ Object

Add of definition names in ‘snippets’ to ‘@directives’, and ‘moduleName’ to ‘@directive_modules’ if any ‘snippets’ contained ‘directive_definitions’

Parameters:

  • moduleName (String) —

    name of module where ‘snippets’ are parses

  • snippets (Snippets) —

    parsed snippts, respons to :directive_definitions



85
86
87
88
89
90
91
92
 
# File 'lib/semantics/resolver.rb', line 85

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

#entryPointsForModules(modules) ⇒ String:Array

return list of definitions in ‘modules’

Parameters:

  • modules (String:Array) —

    of module names to include

Returns:

  • (String:Array) —

    of entry points in the module



313
314
315
316
317
318
319
320
321
322
323
324
325
 
# File 'lib/semantics/resolver.rb', line 313

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

#initContext(names) ⇒ Object

Build initial context (TLA+ reserved words, etc)

Parameters:

  • names (String:Array) —

    to put context



97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
 
# File 'lib/semantics/resolver.rb', line 97

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

#initSnippets(entries, &blk) ⇒ Object

Load TLA+ snippets from file (or strings in unit test), and build global context to use in resolving.

Parameters:

  • entries (File:Array | String:Array) —

    containg TLA+ snippets

  • blk (Block) —

    yields entry



123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
 
# File 'lib/semantics/resolver.rb', line 123

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

#parseSnippets(entry, moduleName) ⇒ Snippets

Parse entry ie. file or possibly a string

Parameters:

  • entry (File|String) —

    to parse

  • moduleName (String) —

    identifying ‘entry’ for error messages

Returns:

  • (Snippets) —

    parsed syntax tree node



68
69
70
71
72
73
74
75
76
77
 
# File 'lib/semantics/resolver.rb', line 68

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

#reportUnresolved(unresolvedSymbols) ⇒ Object

Ouptput to stderr if ‘unresolvedSymbols.any

Parameters:

  • unresolvedSymbols (Hash:Array) —

    of :symbol,:entry of unresolved symbols



271
272
273
274
275
276
277
278
 
# File 'lib/semantics/resolver.rb', line 271

def reportUnresolved( unresolvedSymbols )

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

#resolveEntryPoint(entryPoint) ⇒ Hash:Array

Return Hash:Array of symbols resolved in ‘entryPoint’. First locates ‘entryPoint’ syntax tree in ‘context’, and then use ‘resolveDefine’ to resolve entries.

Parameters:

  • entryPoint (String) —

    name entry point to resolve

Returns:

  • (Hash:Array) —

    identifier in entry points



287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
 
# File 'lib/semantics/resolver.rb', line 287

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 = "    Unknown entrypoint '\#{entryPoint}'\n\n    Known entry points: \#{context.entries.join(',')}\n    EOS\n    @logger.error( \"\#{__method__} \#{msg}\" )        \n    raise ResolverException.new msg\n  end\n\n  return [ symbolTableEntry ] +  symbols\n\nend\n"

#resolveModules(entryPoints, &blk) ⇒ String:Array

Find modules 1) containing TLA+ snippets reachable from ‘entryPoints’, 2) modules reachabable for directive defintision, and 3) modules containing directive definitions

Parameters:

  • entryPoints (String:Array) —

    TLA+ definition names to implement

Returns:

  • (String:Array) —

    names of modules needed in implementation



172
173
174
175
 
# File 'lib/semantics/resolver.rb', line 172

def resolveModules( entryPoints, &blk )
  definitionModules = resolveModulesDo( entryPoints + directives, &blk )
  return definitionModules + directive_modules
end

#resolveModulesDo(entryPoints, &blk) {|"start", entryPoints| ... } ⇒ String:Arrays

Find modules containing TLA+ snippets needed to implement code for ‘entryPoints’. Notice: A module may include additional entrypoint, which must also be satisfied.

‘resolved’, ‘unresolved’, and String:Array list of symbols.

Parameters:

  • entryPoints (String:Array) —

    TLA+ definition names to implement

  • blk (Proc) —

    called with (key, String:Array), where key in

Yields:

  • ("start", entryPoints)

Returns:

  • (String:Arrays) —

    of module names needed in implementation.



190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
 
# File 'lib/semantics/resolver.rb', line 190

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