Class: ADSL::Parser::ASTForEach

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

#list_creations ⇒ Object 



819
820
821
 
# File 'lib/adsl/parser/ast_nodes.rb', line 819

def list_creations
  @block.list_creations
end

#optimize ⇒ Object 



823
824
825
826
827
828
829
 
# File 'lib/adsl/parser/ast_nodes.rb', line 823

def optimize
  optimized = super
  if optimized.block.statements.empty?
    return ASTObjsetStmt.new(:objset => optimized.objset).optimize
  end
  optimized
end

#to_adsl ⇒ Object 



831
832
833
 
# File 'lib/adsl/parser/ast_nodes.rb', line 831

def to_adsl
  "foreach #{ @var_name.text } : #{ @objset.to_adsl } {\n#{ @block.to_adsl.adsl_indent }}\n"
end

#typecheck_and_resolve(context) ⇒ Object 



766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
 
# File 'lib/adsl/parser/ast_nodes.rb', line 766

def typecheck_and_resolve(context)
  before_context = context.dup
  objset = @objset.typecheck_and_resolve context
  
  temp_iterator_objset = ASTDummyObjset.new :type => objset.type
  assignment = ASTAssignment.new :lineno => @lineno, :var_name => @var_name, :objset => temp_iterator_objset
  @block.statements = [assignment, @block.statements].flatten
  
  vars_written_to = Set[]
  vars_read = Set[]
  vars_read_before_being_written_to = Set[]
  context.on_var_write do |name|
    vars_written_to << name
  end
  context.on_var_read do |name|
    var_node, var = context.lookup_var name, false
    vars_read_before_being_written_to << name unless
        vars_written_to.include?(name) or vars_read_before_being_written_to.include? name
    vars_read << name unless vars_read.include? name
  end

  context.push_frame
  block = @block.typecheck_and_resolve context
  context.pop_frame

  vars_read_before_being_written_to.each do |var_name|
    vars_read_before_being_written_to.delete var_name unless vars_written_to.include? var_name
  end

  flat = true
  # flat = false unless vars_read_before_being_written_to.empty?

  if flat
    for_each = ADSL::DS::DSFlatForEach.new :objset => objset, :block => block
  else
    for_each = ADSL::DS::DSForEach.new :objset => objset, :block => block
  end

  vars_read_before_being_written_to.each do |var_name|
    before_var_node, before_var = before_context.lookup_var var_name, false
    inside_var_node, inside_var = context.lookup_var var_name, false
    lambda_objset = ADSL::DS::DSForEachPreLambdaObjset.new :for_each => for_each, :before_var => before_var, :inside_var => inside_var
    var = ADSL::DS::DSVariable.new :name => var_name, :type => before_var.type
    assignment = ADSL::DS::DSAssignment.new :var => var, :objset => lambda_objset
    block.replace before_var, var
    block.statements.unshift assignment
  end
  
  iterator_objset = ADSL::DS::DSForEachIteratorObjset.new :for_each => for_each
  block.replace temp_iterator_objset, iterator_objset
  return for_each
end