Class: ADSL::Parser::ASTClass

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?, #optimize, #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

#to_adsl ⇒ Object 



322
323
324
325
 
# File 'lib/adsl/parser/ast_nodes.rb', line 322

def to_adsl
  par_name = @parent_name.nil? ? "" : "extends #{@parent_name.text} "
  "class #{ @name.text } #{ par_name }{\n#{ @relations.map(&:to_adsl).adsl_indent }}\n"
end

#typecheck_and_resolve(context) ⇒ Object 



286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
 
# File 'lib/adsl/parser/ast_nodes.rb', line 286

def typecheck_and_resolve(context)
  klass = context.classes[@name.text][1]
  @relations.each do |rel_node|
    rel = context.relations[@name.text][rel_node.name.text][1]
    klass.relations << rel
    
    if rel_node.cardinality[0] > rel_node.cardinality[1]
      raise ADSLError, "Invalid cardinality of relation #{klass.name}.#{rel_node.name.text} on line #{rel_node.cardinality[2]}: minimum cardinality #{rel_node.cardinality[0]} must not be greater than the maximum cardinality #{rel_node.cardinality[1]}"
    end
    if rel_node.cardinality[1] == 0
      raise ADSLError, "Invalid cardinality of relation #{klass.name}.#{rel_node.name.text} on line #{rel_node.cardinality[2]}: maximum cardinality #{rel_node.cardinality[1]} must be positive"
    end
    unless context.classes.include? rel_node.to_class_name.text
      raise ADSLError, "Unknown class name #{rel_node.to_class_name.text} in relation #{klass.name}.#{rel_node.name.text} on line #{rel_node.to_class_name.lineno}"
    end

    rel.to_class = context.classes[rel_node.to_class_name.text][1]
    rel.cardinality = rel_node.cardinality
    if rel_node.inverse_of_name
      target_class = context.classes[rel.to_class.name][1]
      inverse_of_node, inverse_of = context.relations[target_class.name][rel_node.inverse_of_name.text]

      while inverse_of_node.nil?
        inverse_of_node, inverse_of = context.relations[target_class.name][rel_node.inverse_of_name.text]
        target_class = target_class.parent
        raise ADSLError, "Unknown relation to which #{rel.from_class.name}.#{rel.name} relation is inverse to: #{rel.to_class.name}.#{rel_node.inverse_of_name.text} on line #{rel_node.inverse_of_name.lineno}" if target_class.nil?
      end

      if inverse_of_node.inverse_of_name
        raise ADSLError, "Relation #{rel.from_class.name}.#{rel.name} cannot be inverse to an inverse relation #{rel.to_class.name}.#{rel_node.inverse_of_name.text} on line #{rel_node.inverse_of_name.lineno}"
      end
      rel.inverse_of = inverse_of
    end
  end
end