Class: ADSL::Parser::ASTAction

Inherits:

ASTNode

• Object
• ASTNode
• ADSL::Parser::ASTAction

Defined in:

lib/adsl/parser/ast_nodes.rb

Instance Method Summary

• #optimize ⇒ Object
• #pre_optimize_adsl_ast_size ⇒ Object
• #prepend_global_variables_by_signatures(*regexes) ⇒ Object
• #to_adsl ⇒ Object
• #typecheck_and_resolve(context) ⇒ Object

Methods inherited from ASTNode

#==, #adsl_ast, #adsl_ast_size, #block_replace, #dup, #hash, is_formula?, is_objset?, is_statement?, node_type, #objset_has_side_effects?, #preorder_traverse

Methods included from Verification::FormulaGenerators

#[], #and, #binary_op, #binary_op_with_any_number_of_params, #equiv, #exists, #false, #forall, #handle_quantifier, #implies, #in_formula_builder, #not, #or, #true

Methods included from Verification::Utils

#classname_for_classname, #infer_classname_from_varname, #t

Instance Method Details

#optimize ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 571

def optimize
  copy = dup
  copy.instance_variable_set :@pre_optimize_adsl_ast_size, copy.adsl_ast_size

  copy.block = until_no_change(copy.block) do |block|
    block = block.optimize(true)

    variables_read = []
    block.preorder_traverse do |node|
      next unless node.is_a? ASTVariable
      variables_read << node.var_name.text
    end
    block.block_replace do |node|
      next unless node.is_a? ASTAssignment
      next if node.var_name.nil? || variables_read.include?(node.var_name.text)
      ASTObjsetStmt.new :objset => node.objset
    end

    next block if block.statements.length != 1

    if block.statements.first.is_a? ASTEither
      either = block.statements.first
      either = ASTEither.new(:blocks => either.blocks.reject{ |subblock| subblock.statements.empty? })
      if either.blocks.length == 0
        ASTBlock.new(:statements => [])
      elsif either.blocks.length == 1
        either.blocks.first
      else
        ASTBlock.new(:statements => [either])
      end
    else
      block
    end
  end

  copy
end

#pre_optimize_adsl_ast_size ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 609

def pre_optimize_adsl_ast_size
  @pre_optimize_adsl_ast_size || adsl_ast_size
end

#prepend_global_variables_by_signatures(*regexes) ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 613

def prepend_global_variables_by_signatures(*regexes)
  variable_names = []
  preorder_traverse do |node|
    next unless node.is_a? ASTVariable
    name = node.var_name.text
    variable_names << name if regexes.map{ |r| r =~ name ? true : false }.include? true
  end
  variable_names.each do |name|
    @block.statements.unshift ASTAssignment.new(
      :var_name => ASTIdent.new(:text => name),
      :objset => ASTEmptyObjset.new
    )
  end
end

#to_adsl ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 628

def to_adsl
  args = []
  @arg_cardinalities.length.times do |index|
    card = @arg_cardinalities[index]
    type = @arg_types[index].text
    name = @arg_names[index].text

    card_str = card[1] == Float::INFINITY ? "#{card[0]}+" : "#{card[0]}..#{card[1]}"
    args << "#{card_str} #{type} #{name}"
  end
  "action #{@name.text}(#{ args.join ', ' }) {\n#{ @block.to_adsl.adsl_indent }}\n"
end

#typecheck_and_resolve(context) ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 535

def typecheck_and_resolve(context)
  old_action_node, old_action = context.actions[@name.text]
  raise ADSLError, "Duplicate action name #{@name.text} on line #{@name.lineno}; first definition on line #{old_action_node.name.lineno}" unless old_action.nil?
  arguments = []
  cardinalities = []
  block = nil
  context.in_stack_frame do
    @arg_names.length.times do |i|
      cardinality = @arg_cardinalities[i]
      if cardinality[0] > cardinality[1]
        raise ADSLError, "Invalid cardinality of argument #{@arg_names[i].text} of action #{@name.text} on line #{cardinality[2]}: minimum cardinality #{cardinality[0]} must not be greater than the maximum cardinality #{cardinality[1]}"
      end
      if cardinality[1] == 0
        raise ADSLError, "Invalid cardinality of relation #{@arg_names[i].text} of action #{@name.text} on line #{cardinality[2]}: maximum cardinality #{cardinality[1]} must be positive"
      end
      cardinality = cardinality.first 2

      klass_node, klass = context.classes[@arg_types[i].text]
      raise ADSLError, "Unknown class #{@arg_types[i].text} on line #{@arg_types[i].lineno}" if klass.nil?
      var = ADSL::DS::DSVariable.new :name => @arg_names[i].text, :type => klass
      context.define_var var, @arg_types[i]
      arguments << var
      cardinalities << cardinality
    end
    block = @block.typecheck_and_resolve context, false
  end
  action = ADSL::DS::DSAction.new :name => @name.text, :args => arguments, :cardinalities => cardinalities, :block => block
  context.actions[action.name] = [self, action]
  return action
rescue Exception => e
  #pp @block
  new_ex = e.exception("#{e.message} in action #{@name.text}")
  new_ex.set_backtrace e.backtrace
  raise new_ex
end