class ADSLParser
prechigh left '==' '!=' noassoc NOT left '<=>' left '<=' '=>' left and or preclow token class extends inverseof action foreach either or create delete subset oneof allof invariant forall exists in empty true false not and equal equiv implies IDENT start adslspec
rule
adslspec: root_elems { return ASTSpec.new :lineno => lineno, :classes => val[0][0], :actions => val[0][1], :invariants => val[0][2] } root_elems: class_decl root_elems { val[1][0].unshift val[0]; return val[1] } | action_decl root_elems { val[1][1].unshift val[0]; return val[1] } | invariant_decl root_elems { val[1][2].unshift val[0]; return val[1] } | { return [[], [], []] } class_decl: class IDENT '{' rel_decls '}' { return ASTClass.new :lineno => val[0], :name => val[1], :relations => val[3] } | class IDENT extends IDENT '{' rel_decls '}' { return ASTClass.new :lineno => val[0], :name => val[1], :parent_name => val[3], :relations => val[5] } rel_decls: rel_decls rel_decl { val[0] << val[1]; return val[0] } | { return [] } rel_decl: cardinality IDENT IDENT inverse_suffix { return ASTRelation.new :lineno => val[0][2], :cardinality => val[0].first(2), :to_class_name => val[1], :name => val[2], :inverse_of_name => val[3] } cardinality: card_number { return [val[0][0], val[0][0], val[0][1]] } | card_number '..' card_number { return [val[0][0], val[2][0], val[0][1]] } | card_number '+' { return [val[0][0], 1.0/0.0, val[0][1]] } card_number: '0' { return [0, lineno] } | '1' { return [1, lineno] } inverse_suffix: inverseof IDENT { return val[1] } | { return nil } action_decl: action IDENT '(' action_args ')' block { return ASTAction.new(:lineno => val[0], :name => val[1], :arg_cardinalities => val[3][0], :arg_types => val[3][1], :arg_names => val[3][2], :block => val[5]) } action_args: additional_args cardinality IDENT IDENT { val[0][0] << val[1]; val[0][1] << val[2]; val[0][2] << val[3]; return val[0] } | { return [[], [], []] } additional_args: additional_args cardinality IDENT IDENT ',' { val[0][0] << val[1]; val[0][1] << val[2]; val[0][2] << val[3]; return val[0] } | { return [[], [], []] } block: '{' statements '}' { return ASTBlock.new :lineno => val[0], :statements => val[1] } statements: statement statements { val[1].unshift val[0]; return val[1] } | { return [] } statement: IDENT '=' objset { return ASTAssignment.new :lineno => val[0].lineno, :var_name => val[0], :objset => val[2] } | create_objset { return ASTObjsetStmt.new :lineno => val[0].lineno, :objset => val[0] } | delete objset { return ASTDeleteObj.new :lineno => val[0], :objset => val[1] } | objset '.' IDENT '+=' objset { return ASTCreateTup.new :lineno => val[0].lineno, :objset1 => val[0], :rel_name => val[2], :objset2 => val[4] } | objset '.' IDENT '-=' objset { return ASTDeleteTup.new :lineno => val[0].lineno, :objset1 => val[0], :rel_name => val[2], :objset2 => val[4] } | objset '.' IDENT '=' objset { return ASTSetTup.new :lineno => val[0].lineno, :objset1 => val[0], :rel_name => val[2], :objset2 => val[4] } | foreach IDENT ':' objset block { return ASTForEach.new :lineno => val[0], :var_name => val[1], :objset => val[3], :block => val[4] } | either block or eitherblocks { val[3].unshift val[1]; return ASTEither.new :lineno => val[0], :blocks => val[3] } eitherblocks: eitherblocks or block { val[0] << val[2]; return val[0] } | block { return [val[0]] } create_objset: create '(' IDENT ')' { return ASTCreateObjset.new :lineno => val[0], :class_name => val[2] } objset: IDENT { return ASTVariable.new :lineno => val[0].lineno, :var_name => val[0] } | subset '(' objset ')' { return ASTSubset.new :lineno => val[0], :objset => val[2] } | oneof '(' objset ')' { return ASTOneOf.new :lineno => val[0], :objset => val[2] } | allof '(' IDENT ')' { return ASTAllOf.new :lineno => val[0], :class_name => val[2] } | create_objset { return val[0] } | create '(' objset '.' IDENT ')' { return ASTDereferenceBuild.new :lineno => val[0].lineno, :objset => val[2], :rel_name => val[4] } | objset '.' IDENT { return ASTDereference.new :lineno => val[0].lineno, :objset => val[0], :rel_name => val[2] } | empty { return ASTEmptyObjset.new :lineno => val[0] } invariant_objset: IDENT { return ASTVariable.new :lineno => val[0].lineno, :var_name => val[0] } | subset '(' objset ')' { return ASTSubset.new :lineno => val[0], :objset => val[2] } | allof '(' IDENT ')' { return ASTAllOf.new :lineno => val[0], :class_name => val[2] } | invariant_objset '.' IDENT { return ASTDereference.new :lineno => val[0].lineno, :objset => val[0], :rel_name => val[2] } | empty { return ASTEmptyObjset.new :lineno => val[0] } invariant_decl: invariant formula { return ASTInvariant.new :lineno => val[0], :name => nil, :formula => val[1] } | invariant IDENT ':' formula { return ASTInvariant.new :lineno => val[0], :name => val[1], :formula => val[3] } formula: forall '(' quantifier_parameters_with_commas ':' formula ')' { return ASTForAll.new :lineno => val[0], :vars => val[2], :subformula => val[4] } | exists '(' quantifier_parameters_with_commas optional_formula ')' { return ASTExists.new :lineno => val[0], :vars => val[2], :subformula => val[3] } | not formula { return ASTNot.new :lineno => val[0], :subformula => val[1] } =NOT | formula and formula { return ASTAnd.new :lineno => val[0].lineno, :subformulae => [val[0], val[2]] } | formula or formula { return ASTOr.new :lineno => val[0].lineno, :subformulae => [val[0], val[2]] } | formula '<=>' formula { return ASTEquiv.new :lineno => val[0].lineno, :subformulae => [val[0], val[2]] } | formula '=>' formula { return ASTImplies.new :lineno => val[0].lineno, :subformula1 => val[0], :subformula2 => val[2] } | formula '<=' formula { return ASTImplies.new :lineno => val[0].lineno, :subformula1 => val[2], :subformula2 => val[0] } | '(' formula ')' { return val[1] } | equiv '(' formula ',' formula additional_formulae ')' { return ASTEquiv.new :lineno => val[0], :subformulae => [val[2], val[4]] + val[5] } | implies '(' formula ',' formula ')' { return ASTImplies.new :lineno => val[0], :subformula1 => val[2], :subformula2 => val[4] } | invariant_objset '==' invariant_objset { return ASTEqual.new :lineno => val[0].lineno, :objsets => [val[0], val[2]] } | invariant_objset '!=' invariant_objset { return ASTNot.new(:lineno => val[0].lineno, :subformula => ASTEqual.new(:lineno => val[0].lineno, :objsets => [val[0], val[2]])) } | equal '(' invariant_objset ',' invariant_objset additional_invariant_objsets ')' { return ASTEqual.new :lineno => val[0], :objsets => [val[2], val[4]] + val[5] } | invariant_objset in invariant_objset { return ASTIn.new :lineno => val[0].lineno, :objset1 => val[0], :objset2 => val[2] } | true { return ASTBoolean.new :lineno => val[0], :bool_value => true } | false { return ASTBoolean.new :lineno => val[0], :bool_value => false } | empty '(' invariant_objset ')' { return ASTEmpty.new :lineno => val[0], :objset => val[2] } quantifier_parameters_with_commas: quantifier_parameters_with_commas ',' quantifier_parameter { val[0] << val[2]; return val[0] } | quantifier_parameter { return [val[0]] } quantifier_parameter: IDENT IDENT { return [val[1], ASTAllOf.new(:lineno => val[0].lineno, :class_name => val[0]), val[0].lineno] } | IDENT in objset { return [val[0], val[2], val[0].lineno] } optional_formula: ':' formula { return val[1] } | { return nil } additional_formulae: additional_formulae ',' formula { val[0] << val[2]; return val[0] } | { return [] } additional_invariant_objsets: additional_invariant_objsets ',' invariant_objset { val[0] << val[2]; return val[0] } | { return [] }
end
—- header
require ‘adsl/parser/adsl_parser.rex’ require ‘adsl/fol/first_order_logic’
module ADSL
module Parser
—- inner
# generated by racc
def generate_ast(str) scan str # do_parse end def parse(str) generate_ast(str).typecheck_and_resolve end
—- footer
end
end