Class: ADSL::Parser::ASTBlock

Inherits:
ASTNode show all
Defined in:
lib/adsl/parser/ast_nodes.rb

Instance Method Summary collapse

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(last_stmt = false) ⇒ Object 



659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
 
# File 'lib/adsl/parser/ast_nodes.rb', line 659

def optimize(last_stmt = false)
  until_no_change super() do |block|
    next block if block.statements.empty?

    statements = block.statements.map(&:optimize).map{ |stmt|
      stmt.is_a?(ASTBlock) ? stmt.statements : [stmt]
    }.flatten(1).reject{ |stmt|
      stmt.is_a?(ASTDummyStmt)
    }

    if last_stmt
      if statements.last.is_a?(ASTAssignment)
        if statements.last.objset.objset_has_side_effects?
          statements[-1] = ASTObjsetStmt.new(:objset => statements.last.objset)
        else
          statements.pop
        end
      elsif statements.last.is_a?(ASTEither)
        statements.last.blocks.map!{ |b| b.optimize true }
        statements[-1] = statements.last.optimize
      elsif statements.last.is_a?(ASTBlock)
        last = statements.pop.optimize true
        statements += last.statements
      end
    end

    ASTBlock.new(:statements => statements)
  end
end

#to_adsl ⇒ Object 



689
690
691
 
# File 'lib/adsl/parser/ast_nodes.rb', line 689

def to_adsl
  @statements.map(&:to_adsl).join
end

#typecheck_and_resolve(context, open_subcontext = true) ⇒ Object 



645
646
647
648
649
650
651
652
653
654
655
656
657
 
# File 'lib/adsl/parser/ast_nodes.rb', line 645

def typecheck_and_resolve(context, open_subcontext=true)
  context.push_frame if open_subcontext
  stmts = []
  @statements.each do |node|
    main_stmt = node.typecheck_and_resolve context
    stmts += context.pre_stmts
    stmts << main_stmt unless main_stmt.nil?
    context.pre_stmts = []
  end
  return ADSL::DS::DSBlock.new :statements => stmts.flatten
ensure
  context.pop_frame if open_subcontext
end