Class: TlaParserS::Resolver

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

Defined Under Namespace

Classes: THash

Constant Summary collapse

PROGNAME =

Logger

nil

Constants included from Utils::MyLogger

Utils::MyLogger::LOGFILE

Instance Attribute Summary collapse

Construct && configure collapse

Initialize context & parse snippets collapse

Services to use after init & parse collapse

Internal methods for parsing collapse

implement module resolve collapse

private utilities collapse

Methods included from Utils::MyLogger

#getLogger, #logfile

Constructor Details

#initialize(options = {}) ⇒ Resolver

construct with ‘options’

Parameters:

  • options (Hash) (defaults to: {}) —

    to configure resolver

Options Hash (options):

  • :logfile (String) —

    name of file where to log to



55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
 
# File 'lib/semantics/resolver.rb', line 55

def initialize( options={} )
  
  @logger = getLogger( PROGNAME, options )
  @logger.info( "#{__method__} initialized parser-resolver version #{TlaParserS::version}" )

  @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 definition names in ‘snippets’ to ‘@directives’, and ‘moduleName’ to ‘@directive_modules’ if any of the ‘snippets’ contains ‘directive_definitions’

Parameters:

  • moduleName (String) —

    name of module where ‘snippets’ are parses

  • snippets (Snippets) —

    parsed snippts, respons to :directive_definitions



289
290
291
292
293
294
295
296
 
# File 'lib/semantics/resolver.rb', line 289

def addDirectives( snippets, moduleName )
  new_directives = snippets.directive_definitions
  
  @logger.debug( "#{__method__} moduleName=#{moduleName} -> new_directives=#{new_directives}" ) if @logger.debug?
  @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|String) —

    of module names to include

Returns:

  • (String:Array) —

    of entry points in ‘modules’



456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
 
# File 'lib/semantics/resolver.rb', line 456

def entryPointsForModules( modules )

  # ensure that it is an array 
  modules = modules.is_a?( Array ) ? modules : [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(',')}" ) if @logger.debug?
  return ret
end

#initContext(names) ⇒ Object

Build initial context (TLA+ reserved words, etc)

Parameters:

  • names (String:Array) —

    to put context



82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
 
# File 'lib/semantics/resolver.rb', line 82

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|File|String) —

    containg TLA+ snippets

  • blk (Block) —

    yields entry



105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
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
 
# File 'lib/semantics/resolver.rb', line 105

def initSnippets( entries, &blk )

  # Make it to an array
  entries = [ entries ] unless entries.is_a?( Array ) || entries.nil?

  @logger.info "#{__method__} starts in #{Dir.pwd}"

  # create global context
  context.pushContext

  # collect symbol definitions parsed
  parsedSnippets = []


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

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

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

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

      # String|File --> AST
      snippets = parseSnippets( entry, moduleName )
      yield( true, entry ) if blk
      @logger.debug( "#{__method__} #{moduleName}: snippets=#{snippets.inspect}" )          if @logger.debug?

      # collect an array of hashes with :node_type, :value, :true  -properties
      parsedSnippets += snippets.symbol_definitions

      # collect '@directives' and, '@directive_modules' if
      # snippets.directive_definitions because they should be 
      # included to entry points
      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

  @logger.info "#{__method__} finished"
  self
  parsedSnippets
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



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

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



399
400
401
402
403
404
405
406
 
# File 'lib/semantics/resolver.rb', line 399

def reportUnresolved( unresolvedSymbols )

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

end

#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



415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
 
# File 'lib/semantics/resolver.rb', line 415

def resolveEntryPoint( entryPoint )
  symbolTableEntry = context.resolveSymbol( entryPoint )
  @logger.debug( "#{__method__} symbolTableEntry #{entryPoint}-->#{symbolTableEntry}" ) if @logger.debug?
  if symbolTableEntry && symbolTableEntry[:resolved]
    # return from cache
    if symbolTableEntry[:cached]
      return symbolTableEntry[:cached]
    end
    tree = symbolTableEntry[:resolved][:tree]
    @logger.debug( "#{__method__} tree-->#{tree.inspect}" )       if @logger.debug?
    symbols = context.resolveDefine( tree )
    @logger.debug( "#{__method__} resolveDefine-->#{symbols.join('\n')}" ) if @logger.debug?
    symbolTableEntry[:cached] = symbols
    symbols
  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

#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



176
177
178
179
 
# File 'lib/semantics/resolver.rb', line 176

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.



317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
 
# File 'lib/semantics/resolver.rb', line 317

def resolveModulesDo( entryPoints, &blk )
  
  @logger.info( "#{__method__} resolveModules for entryPoint=#{entryPoints.join(',')}, symbol-table depth=#{context.symbol_table.depth}" )
  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 more in 'unResolved'
    break if unResolved.empty?
    # next to resolve
    entryPoint = unResolved.to_a.shift
    @logger.info( "#{__method__} next to resolve entryPoint #{entryPoint} " )
    # already resolved
    next if resolved.include?( entryPoint )

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

    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}" ) if @logger.debug?
    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}" ) if @logger.debug?
    
    # 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}" ) if @logger.debug?
    
    # 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

#sortModules(modules, &blk) ⇒ String:Array

Run topological sort on modules.

Parameters:

  • modules (String:Array) —

    names of modules to sort

Returns:

  • (String:Array) —

    of sorted modules



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
 
# File 'lib/semantics/resolver.rb', line 199

def sortModules( modules, &blk )
  
  @logger.info "#{__method__}: modulesstart=#{modules} - starts"
  
  sortteri =
    modules.
    #
    # map { |m| puts "m0=#{m}"; m }.
    #
    # Find symbols in module :m to array :s
    #
    # [{ :m=<module-name>, :s=>[<symbol definitions in module>]}, ...]
    #
    map { |m| { :m => m, :s=> context.resolveModule(m) } }.
    # map { |m| puts "m1[:s]=#{m[:s].map{ |s| s[:module] +':' + s[:symbol_name] } }"; m }.
    #
    # Resolver symbols in :s to array :r 
    #
    # At this point
    # [{ :m=<module-name>, :s=>[<symbol definitions in module>], :r=>[{:symbol=>"", :resolved>={} }]}, .... ]
    #
    map { |m| m[:r] = m[:s].map{ |s| resolveEntryPoint( s[:symbol_name] ) }.flatten; m }.
    # map { |m| puts "#{m[:m]}-> m2[:s]=#{m[:s].map{ |s| s[:module] +':' + s[:symbol_name] } }"; m }.        
    # map { |m| puts "#{m[:m]}-> m2[:r]=#{m[:r].map { |r| r[:symbol] + '->' + r[:resolved][:symbol_name] + '@' + (r[:resolved][:module] ||'-' )}}"; m }.
    #
    # Drop unresolved symbols from :r
    #
    map { |m| m[:r] = m[:r].reject { |r| r[:resolved].nil? }; m}.
    #
    # Add m[:d] array of module names (drop resolves, which do not
    # have module defined (correspoding to local references)
    #
    # [{ :m=<module-name>, :d=> [<resolved modules (filepaths?)>] :s=>[<symbol definitions in module>], :r=>[{:symbol=>"", :resolved>={} }]}, .... ]
    # 
    #
    map { |m| m[:d] = m[:r].select { |r| r[:resolved][:module]}.map { |r| r[:resolved][:module]}.uniq; m}.
    # map { |m| puts "m3=#{m[:m]}, :d=#{m[:d]}, [:s]=#{m[:s].map{ |s| s[:module] +':' + s[:symbol_name] } }"; m }.
    #
    # Reject modules, which do not define any snippets
    # 
    select { |m| m[:s].any? }.
    # map { |m| puts "m4=#{m[:m]}, :d=#{m[:d]}, [:s]=#{m[:s].map{ |s| s[:module] +':' + s[:symbol_name] } }"; m }.
    #
    # clear prefix path from modulename in m[:d] elements
    #
    map { |m| m[:d] = m[:d].map{ |d| modules.select { |mo| d.end_with?(mo)}.first }.select {|d| d }; m }.                
    # map { |m| puts "m5=#{m[:m]}, :d=#{m[:d]}"; m }.
    #
    #
    # Finally create a tsort hash
    #
    inject( THash.new ){ |t, m| t[m[:m]] = m[:d]; t }.
    #
    # And sort it
    #
    tsort
  
  sortteri
end