Class: ADSL::Parser::ASTEither

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_entity_classes_written_to ⇒ Object 



872
873
874
 
# File 'lib/adsl/parser/ast_nodes.rb', line 872

def list_entity_classes_written_to
  @blocks.map{ block.list_entity_classes_written_to }.flatten
end

#optimize ⇒ Object 



876
877
878
879
880
881
882
883
884
885
886
887
888
889
 
# File 'lib/adsl/parser/ast_nodes.rb', line 876

def optimize
  until_no_change super do |either|
    next either.optimize unless either.is_a?(ASTEither)
    next ASTDummyStmt.new if either.blocks.empty?
    next either.blocks.first if either.blocks.length == 1
    ASTEither.new(:blocks => either.blocks.map{ |block|
      if block.statements.length == 1 && block.statements.first.is_a?(ASTEither)
        block.statements.first.blocks
      else
        [block]
      end
    }.flatten(1).uniq)
  end
end

#to_adsl ⇒ Object 



891
892
893
 
# File 'lib/adsl/parser/ast_nodes.rb', line 891

def to_adsl
  "either #{ @blocks.map{ |b| "{\n#{ b.to_adsl.adsl_indent }}" }.join " or " }\n"
end

#typecheck_and_resolve(context) ⇒ Object 



839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
 
# File 'lib/adsl/parser/ast_nodes.rb', line 839

def typecheck_and_resolve(context)
  context.push_frame

  contexts = [context]
  (@blocks.length-1).times do
    contexts << context.dup
  end

  blocks = []
  @blocks.length.times do |i|
    blocks << @blocks[i].typecheck_and_resolve(contexts[i])
  end

  contexts.each do |c|
    c.pop_frame
  end

  either = ADSL::DS::DSEither.new :blocks => blocks

  lambdas = []

  ASTTypecheckResolveContext::context_vars_that_differ(*contexts).each do |var_name, vars|
    common_type = ADSL::DS::DSClass.common_supertype(vars.map(&:type))
    var = ADSL::DS::DSVariable.new :name => var_name, :type => common_type
    objset = ADSL::DS::DSEitherLambdaObjset.new :either => either, :vars => vars
    assignment = ADSL::DS::DSAssignment.new :var => var, :objset => objset
    context.redefine_var var, nil
    lambdas << assignment
  end

  return [ either, lambdas ]
end