# coding: utf-8 require 'forwardable' module TlaParserS # ****************************************************************** # # Manage context to parse TLA+ snippets # # # Builds context in three phases: # # 1) Initial context includes TLA+ standard definitions e.g. TRUE, FALSE # when context is created # 2) Global context includes snippets defining macros, procedures, # operators, and variables. Using pushContext/addContext # 3) During resolve phase push to context formal parameters, quantification # bind variables, variables in set constructor generator. Uses # pushContext/addContext methods internally from 'resolveDefine', # # # ****************************************************************** class Context extend Forwardable # for easy delegation attr_accessor :symbol_table attr_reader :options def_delegators :symbol_table, :currentContext, :dumpContext, :popContext, :entries, :symbols, :resolveModule # ------------------------------------------------------------------ # Logger PROGNAME = nil # progname for logger default class name include TlaParserS::Utils::MyLogger # mix logger # # TLA+ standar library symbols # GLOABLS = %w( TRUE FALSE ) # ------------------------------------------------------------------ # @!group Constructor & configs def initialize( options={} ) @options = options @logger = getLogger( PROGNAME, options ) @logger.info( "#{__method__} initialized" ) initContext end # @!endgroup # ------------------------------------------------------------------ # @!group Services to initialize def initContext @symbol_table = SymbolTable.new( options ) # # create context for standar library && add entries # @symbol_table.pushContext( nil ) # GLOABLS.each do |global| # entry = { # :context_type => "Init", # :context => "Global", # :symbol_type => "StandardLib", # :symbol_name => global, # } # @symbol_table.addEntry( entry ) # end return self end # Create new context in symbol table && add entries def initEntries( entries ) return unless entries && entries.any? # create new context pushContext # add entries entries.each do |entry| symbol_table.addEntry( entry ) end end # @!endgroup # Add more symbols to current context levell # def addContext( snippets, moduleName=nil ) symbol_table.addContext( snippets, moduleName ) return self end # Add one level to context & and add snipets there # # @param snippets [SyntaxNode] implementing 'symbol_definitions` method # def pushContext( snippets=nil, moduleName=nil ) warn "Method symbol_definitions not implemented on #{snippets}" if snippets && !snippets.respond_to?(:symbol_definitions) symbol_table.pushContext( snippets, moduleName ) return self end # Locate 'symbol' in context # # @param symbol [String] to resolve # # @return [Hash] with :symbol, :resolved properties def resolveSymbol( symbol ) resolved = symbol_table.resolveContext( symbol ) return resolvedSymbol( symbol, resolved ); # return { # :symbol => symbol, # :resolved => resolved, # } end # ------------------------------------------------------------------ # Resolver # Resolve symbol table entries in 'stmt' # # @param stmt [Statement] parse tree node for statement to resolve # @return see 'resolveExpression' private def resolveStatement( stmt, ret=[] ) stmt.traverse(ret) do |ret,node_type, node| @logger.debug( "#{__method__}: enter node_type=#{node_type}, #{node.text_value}ret=#{ret}." ) if @logger.debug? case node_type when "Statement" when "Skip" when "Return" when "Goto" when "Identifier" @logger.debug( "#{__method__}: Identifier node=#{node.inspect}" ) if @logger.debug? ret.concat( resolveExpression( node )) when "WithStatement" ret.concat( resolveExpression( node.with_expression )) ret.concat( resolveStatement( node.with_statement, ret )) when "Conditional" ret.concat( resolveExpression( node.condition )) @logger.debug( "#{__method__}: Conditional if_true=#{node.if_true.inspect}" ) if @logger.debug? ret.concat( resolveStatement( node.if_true, ret )) ret.concat( resolveStatement( node.if_not_true, ret )) if node.if_not_true when "Either" ret = node.choices.each { |s| resolveStatement( s, ret ) } when "Assert" ret.concat( resolveExpression( node.assertion )) when "Assignment" lvalue = node.lvalue @logger.debug( "#{__method__}: Assignment lvalue=#{lvalue.inspect}" ) if @logger.debug? ret.concat( resolveExpression( node.lvalue.expression ) ) ret.concat( resolveExpression( node.rvalue )) # lvalue = node.lvalue.node_value # @logger.debug( "#{__method__}: Assign lvalue=#{lvalue}" ) # # take just first variable # lvalue = lvalue.split( /[.\[]/ ).first # ret << resolvedSymbol( lvalue, symbol_table.resolveContext( lvalue )) # # resovel expression # ret.concat( resolveExpression( node.rvalue )) when "Print" @logger.debug( "#{__method__}: Print node=#{node.inspect}" ) if @logger.debug? sret = resolveExpression( node.print_expression ) @logger.debug( "#{__method__}: Print sret=#{sret}" ) if @logger.debug? ret = ret.concat( sret ) when "CompoundStatement" ret = node.statements.each { |s| resolveStatement( s, ret ) } # sret = [] # node.statements.each { |s| sret = resolveStatement( s, sret ) } # ret.concat( sret ) when "MacroCall" # resolve macro definition ret << resolvedSymbol( node.called, symbol_table.resolveContext( node.called ) ) # resolve actual parameters node.actual_parameters.each do |expr_node| eret = resolveExpression(expr_node ) @logger.debug "actual param eret=#{eret}" if @logger.debug? ret.concat( eret ) end # actual paramtere when "Call" # resolve procedure definition ret << resolvedSymbol( node.called, symbol_table.resolveContext( node.called ) ) # resolve actual parameters ret = node.actual_parameters.each do |expr_node| ret.concat( resolveExpression( expr_node )) end # actual paramtere else msg = "#{__method__}: Unknwon statement node type #{node_type} for node #{node.inspect}" @logger.error "#{__method__}:# {msg} )" raise ContextException, msg end @logger.debug( "#{__method__}: leave node_type=#{node_type} ret=#{ret}." ) if @logger.debug? ret end ret end # def resolveStatement( stmt ) # Resolve definitions with body (macro, procedure,operator # definition = callables), and variable definitions. # # @return [Hash:Array] of resolved entries, hash with {:symbol,:resolved} -properties # @see resolveExpression def resolveDefine( defineNode ) # @logger.debug "resolveDefine starting callable=#{defineNode.inspect}" if @logger.debug? ret = nil pushContext( defineNode ) # dumpContext if defineNode.respond_to?( :body_node ) then # macro, procedure, operatordef @logger.info( "#{__method__} start with resolveStatement for #{defineNode.body_node}" ) if defineNode.body_node.is_a?(SbuilderSexp::Expression) # operator ret = resolveExpression( defineNode.body_node ) else # macro, procedure ret = resolveStatement( defineNode.body_node ) end # resolve expressions initializing variable declarations if defineNode.respond_to?(:variable_declarations) sret = [] defineNode.variable_declarations.each do |variable_declaration| sret = sret.concat( resolveExpression( variable_declaration.init )) end # add resolved symbols from declaration init only if symbol # not already resolved sret.each do |s| ret << s unless ret.map { |r| r[:symbol] }.include?( s[:symbol]) end end # puts "sret found=#{sret}, ret=#{ret}" if sret.any? elsif defineNode.respond_to?( :init ) then @logger.info( "#{__method__} start with resolveExpression #{defineNode.init}" ) ret = resolveExpression( defineNode.init ) @logger.debug( "#{__method__} resolveExpression-->#{ret}" ) if @logger.debug? else msg = <<-EOS Unknown tree node object #{defineNode}. Should be 'Callabe' or 'VariableDef' EOS @logger.error( "#{__method__} #{msg}" ) raise ContextException.new msg end popContext() ret end # Resolve symbol table entries in 'expression' # # @param expression [Expression] parse tree node for exprresion to resolve # # @return [Hash:Array] {:symbol,:resolved} hashes, where :resolved is the result # of symbol table lookup def resolveExpression( expr ) ret = [] expr && expr.traverse do |m, node_type, enode, node_val | @logger.debug( "#{__method__} node_type=#{node_type}, node_val=#{node_val}" ) if @logger.debug? case node_type when "Identifier" ret << resolvedSymbol( node_val, symbol_table.resolveContext( node_val ) ) when "AdditiveExpression", "MultitiveExpression", "UnaryExpression", "ParenthesisExpression" when "PrimaryExpression" sret = [] # puts "PrimaryExpression: attribute_accessors=#{enode.attribute_accessors.join(',')}" enode.attribute_accessors && enode.attribute_accessors.each do |accessor| sret = sret.concat( resolveExpression( accessor )) end ret = ret.concat( sret ) when "FieldByValue" # ret << resolvedSymbol( node_val, symbol_table.resolveContext( node_val ) ) # expr = node.field_value_expression.traverse { |m, node_type, enode, node_val| m.concat( expression_value(node_type, enode, node_val )) } sret = resolveExpression( enode.field_value_expression ) ret = ret.concat( sret ) when "FieldByName" when "SequenceExpression" @logger.debug( "#{__method__} SequenceExpression: enode=#{enode.inspect}" ) if @logger.debug? sret = [] enode.tuples && enode.tuples.each do |tuple_expr| sret = sret.concat( resolveExpression( tuple_expr )) end ret = ret.concat( sret ) when "IfExpression" @logger.debug( "#{__method__} IfExpression: enode=#{enode.inspect}" ) if @logger.debug? sret = resolveExpression( enode.condition_node ) ret.concat( sret ) @logger.info( "#{__method__} IfExpression: condition-expr=#{sret}" ) sret = resolveExpression( enode.then_expression_node ) ret.concat( sret ) @logger.info( "#{__method__} IfExpression: then-expr=#{sret}" ) sret = [] sret = resolveExpression( enode.else_expression_node ) if enode.else_expression_node ret.concat( sret ) @logger.info( "#{__method__} IfExpression: els-expr=#{sret}" ) when "ChooseExpression" @logger.debug( "#{__method__} ChooseExpression: enode=#{enode.inspect}" ) if @logger.debug? @logger.debug( "#{__method__} ChooseExpression: enode.binds_node=#{enode.binds_node}" ) if @logger.debug? # bind node defines symbol table pushContext( enode ) choose_expression=enode.choose_expression @logger.debug( "#{__method__} ChooseExpression: choose_expression=#{choose_expression.inspect}" ) if @logger.debug? sret = resolveExpression( choose_expression ) @logger.info( "#{__method__} ChooseExpression: resolved sret=#{sret.map {|e| { e[:symbol] => e[:resolved] ? e[:resolved][:symbol_type]+':'+e[:resolved][:context] : nil} }}" ) ret = ret.concat( sret ) popContext() when "RecordDefinition" @logger.debug( "#{__method__} RecordDefinition: enode=#{enode.inspect}" ) if @logger.debug? sret = [] enode.record_fields.each do |record_field| sret = sret.concat( resolveExpression( record_field.element_expression )) end @logger.info( "#{__method__} RecordDefinition: resolved sret=#{sret.map {|e| { e[:symbol] => e[:resolved] ? e[:resolved][:symbol_type]+':'+e[:resolved][:context] : nil} }}" ) ret = ret.concat( sret ) when "RecordExcept" # resolve where base expression # id = enode.record_identifier # ret << resolvedSymbol( id, symbol_table.resolveContext( id ) ) bret = resolveExpression( enode.record_base ) ret = ret.concat( bret ) @logger.debug( "#{__method__} RecordExcept: record_base -->=#{bret}" ) if @logger.debug? sret = [] # resolve EXCEPT constructor field rvalue expression enode.record_field_definitions && enode.record_field_definitions.each do |field_definition| sret = sret.concat( resolveExpression( field_definition.rvalue_expression )) end ret = ret.concat( sret ) when "SetConstructor" sret = [] enode.set_elements && enode.set_elements.each do |set_element| sret = sret.concat( resolveExpression( set_element )) end ret = ret.concat( sret ) when "SetExpressionMap" @logger.debug( "#{__method__} SetExpressionMap: enode=#{enode.inspect}" ) if @logger.debug? # resolve set mapped sret = resolveExpression( enode.binds_node.bind_set ) ret = ret.concat( sret ) # resolve expression in set map pushContext( enode ) sret = resolveExpression( enode.set_expression ) @logger.debug( "#{__method__} SetExpressionMap: resolved sret=#{sret}" ) if @logger.debug? ret = ret.concat( sret ) when "FunctionExpression" @logger.debug( "#{__method__} FunctionExpression: enode=#{enode.inspect}" ) if @logger.debug? pushContext( enode ) sret = resolveExpression( enode.function_expression ) ret = ret.concat( sret ) popContext( ) when "SetExpression" @logger.debug( "#{__method__} SetExpression: enode=#{enode.inspect}" ) if @logger.debug? pushContext( enode ) sret = resolveExpression( enode.set_expression ) @logger.debug( "#{__method__} SetExpression: resolved sret=#{sret}" ) if @logger.debug? ret = ret.concat( sret ) popContext( ) when "OperatorExpression" @logger.debug( "#{__method__} OperatorExpression: enode=#{enode.inspect}" ) if @logger.debug? operator_name = enode.operator_name ret << resolvedSymbol( operator_name, symbol_table.resolveContext( operator_name ) ) sret = [] enode.arguments && enode.arguments.each do |argument_node| sret = sret.concat( resolveExpression( argument_node )) end @logger.info( "#{__method__} OperatorExpression: resolved sret=#{sret.map {|e| { e[:symbol] => e[:resolved] ? e[:resolved][:symbol_type]+':'+e[:resolved][:context] : nil} }}" ) ret = ret.concat( sret ) when "LetExpression" @logger.debug( "#{__method__} SetExpression: node.symbol_definitions=#{enode.symbol_definitions}" ) if @logger.debug? pushContext( enode ) # resolve let operator oret = resolveExpression( enode.operatorDef.body_node ) @logger.debug( "#{__method__} resolved oret=#{oret}" ) if @logger.debug? ret = ret.concat( oret ) # resolve let expression eret = resolveExpression( enode.letExpression ) @logger.debug( "#{__method__} resolved eret=#{eret}" ) if @logger.debug? ret = ret.concat( eret ) popContext( ) when "QuantifyExpression" @logger.debug( "#{__method__} SetExpression: node.symbol_definitions=#{enode.symbol_definitions}" ) if @logger.debug? pushContext( enode ) sret = resolveExpression( enode.binds_nodes.first.bind_set ) ret = ret.concat( sret ) @logger.debug( "#{__method__} resolved sret=#{sret}" ) if @logger.debug? @logger.debug( "#{__method__} SetExpression: #{enode.quantified_expression.inspect}" ) if @logger.debug? qret = resolveExpression( enode.quantified_expression ) @logger.debug( "#{__method__} resolved qret=#{qret}" ) if @logger.debug? ret = ret.concat( qret ) @logger.debug( "#{__method__} resolved ret=#{ret}" ) if @logger.debug? popContext( ) when "IntegerValue", "StringValue", "OriginalValue" else msg = "Unknwon expression node type #{node_type} with value #{node_val}" @logger.error( "#{__method__} #{msg}" ) raise ContextException.new msg end end ret end # def resolveExpression( expr ) private # @return [Hash] with {:symbol,:resolved} -properties def resolvedSymbol( identifier, resolved ) { :symbol => identifier, :resolved => resolved } end end # class end