class BoogieLanguage

prechigh
  left 'forall' 'exists'
  left 'old'
  nonassoc '[' ']'
  nonassoc '!'
  left '*' '/' '%'
  left '+' '-'
  left '++'
  left '==' '!=' '<' '>' '<=' '>=' '<:'
  left '&&'
  left '||'
  left '==>'
  left '<==>'
  left 'if' 'then' 'else'
  left ':'
  nonassoc '(' ')'
preclow

options no_result_var

token IDENTIFIER NUMBER BITVECTOR STRING BVTYPE
token PARSE_DECL PARSE_PARAM PARSE_SPEC PARSE_BLOCKS PARSE_STMT PARSE_EXPR PARSE_TYPE

rule

target:
  program
  | PARSE_DECL decl { val[1] }
  | PARSE_PARAM param_decl { val[1] }
  | PARSE_SPEC spec { val[1] }
  | PARSE_BLOCKS blocks { val[1] }
  | PARSE_STMT stmt { val[1] }
  | PARSE_EXPR expr { val[1] }
  | PARSE_TYPE type { val[1] }

name: IDENTIFIER { val[0] }
names: name { [val[0]] } | name ',' names { [val[0]] + val[2] }

ident: IDENTIFIER { {name: val[0]} }
ident_opt: { nil } | ident
idents: ident { [val[0]] } | ident ',' idents { [val[0]] + val[2] }
idents_opt: { [] } | idents

literal:
  bool_lit    { BooleanLiteral.new value: val[0] }
  | BITVECTOR  { BitvectorLiteral.new val[0] }
  | NUMBER     { IntegerLiteral.new value: val[0] }
bool_lit: 'true' { true } | 'false' { false }

string: STRING

type:
  type_atom
  | map_type
  | name tc_args { CustomType.new name: val[0], arguments: val[1] }

type_atom:
  'bool' { Type::Boolean }
  | 'int' { Type::Integer }
  | BVTYPE { BitvectorType.new width: val[0] }
  | '(' type ')' { val[1] }

map_type: type_args '[' types ']' type {
  MapType.new arguments: val[0], domain: val[2], range: val[4]
}

tc_args:
  { [] }
  | type_atom tc_args { [val[0]] + val[1] }
  | name tc_args { [(CustomType.new name: val[0], arguments: val[1])] }
  | map_type { [val[0]] }

types: type { [val[0]] } | type ',' types { [val[0]] + val[2] }

type_args: { [] } | '<' names '>' { val[1] }

expr: expr '<==>' expr  { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '==>' expr   { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '||' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '&&' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '==' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '!=' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '<' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '>' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '<=' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '>=' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '<:' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '++' expr    { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '+' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '-' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '*' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '/' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | expr '%' expr     { BinaryExpression.new lhs: val[0], op: val[1], rhs: val[2] }
    | '!' expr          { LogicalNegation.new expression: val[1] }
    | '-' expr          { ArithmeticNegation.new expression: val[1] }
    | expr '[' exprs ']' { MapSelect.new map: val[0], indexes: val[2] }
    | expr '[' exprs ':=' expr ']' { MapUpdate.new map: val[0], indexes: val[2], value: val[4] }
    | expr '[' NUMBER ':' NUMBER ']' { BitvectorExtract.new bitvector: val[0], msb: val[2], lsb: val[4] }
    | 'if' expr 'then' expr 'else' expr {
      IfExpression.new condition: val[1], then: val[3], else: val[5]
    }
    | '|' body '|' { CodeExpression.new body: val[1] }
    | literal
    | ident '(' exprs_opt ')' {
      id = FunctionIdentifier.new val[0]
      FunctionApplication.new function: id, arguments: val[2]
    }
    | ident { StorageIdentifier.new val[0] }
    | 'old' '(' expr ')' { OldExpression.new expression: val[2] }
    | '(' quantifier type_args param_decls '::' ants expr ')' {
      QuantifiedExpression.new quantifier: val[1], type_arguments: val[2],
        variables: val[3],
        attributes: val[5].select{|a| a.is_a?(Hash)},
        triggers: val[5].select{|es| es.is_a?(Array)}.map{|es| Trigger.new(expressions: es)},
        expression: val[6]
    }
    | '(' expr ')'  { val[1] }

exprs: expr { [val[0]] } | expr ',' exprs { [val[0]] + val[2] }
exprs_opt: { [] } | exprs

quantifier: 'forall' {'forall'} | 'exists' {'exists'}

attr: '{:' name enss_opt '}' { Attribute.new key: val[1].to_sym, values: val[2] }
attrs: { [] } | attr attrs { [val[0]] + val[1] }
trigger: '{' exprs '}' { val[1] }
ant: attr | trigger
ants: { [] } | ant ants { [val[0]] + val[1] }

ens: expr | string
enss: ens { [val[0]] } | ens ',' enss { [val[0]] + val[2] }
enss_opt: { [] } | enss

stmt:
  'assert' attrs expr ';' { AssertStatement.new attributes: val[1], expression: val[2], token: val[0] }
  | 'assume' attrs expr ';' { AssumeStatement.new attributes: val[1], expression: val[2], token: val[0] }
  | 'havoc' idents ';' {
    ids = val[1].map{|id| StorageIdentifier.new id}
    HavocStatement.new identifiers: ids, token: val[0]
  }
  | lhss ':=' exprs ';' { AssignStatement.new lhs: val[0], rhs: val[2] }
  | 'call' attrs call_lhs '(' exprs_opt ')' ';' {
    CallStatement.new attributes: val[1], assignments: val[2][:rets],
    procedure: val[2][:name], arguments: val[4], token: val[0]
  }
  | 'call' 'forall' ident '(' wc_exprs_opt ')' ';' {
    id = ProcedureIdentifier.new val[2]
    CallStatement.new assignments: nil, procedure: id, arguments: val[4],
    token: val[0]
  }
  | if_stmt
  | 'while' '(' wc_expr ')' loop_invs '{' blocks '}' {
    WhileStatement.new condition: val[2], invariants: val[4], blocks: val[6],
    token: val[0]
  }
  | 'break' ident_opt ';' {
    id = LabelIdentifier.new(val[1]) if val[1]
    BreakStatement.new identifier: id, token: val[0]
  }
  | 'return' ';' { ReturnStatement.new token: val[0] }
  | 'return' expr ';' { ReturnStatement.new expression: val[1], token: val[0] }
  | 'goto' idents ';' {
    ids = val[1].map{|id| LabelIdentifier.new id}
    GotoStatement.new identifiers: ids, token: val[0]
  }
stmts:
  stmt { [val[0]] }
  | stmt stmts { [val[0]] + val[1] }

call_lhs:
  ident { {name: ProcedureIdentifier.new(val[0]), rets: []} }
  | idents ':=' ident {
    ids = val[0].map{|id| StorageIdentifier.new id}
    id = ProcedureIdentifier.new val[2]
    {name: id, rets: ids}
  }

if_stmt: 'if' '(' wc_expr ')' '{' blocks '}' else_stmt { IfStatement.new condition: val[2], blocks: val[5], else: val[7], token: val[0] }
else_stmt: { nil } | 'else' '{' blocks '}' { val[2] } | 'else' if_stmt { val[1] }

lhs: ident selects {
  id = StorageIdentifier.new val[0]
  val[1].reduce(id){|m,x| MapSelect.new map: m, indexes: x}
}
lhss: lhs { [val[0]] } | lhs ',' lhss { [val[0]] + val[2] }

select: '[' exprs ']' { val[1] }
selects: { [] } | select selects { [val[0]] + val[1] }

wc_expr: expr | '*' { Expression::Wildcard }
wc_exprs: wc_expr { [val[0]] } | wc_expr ',' wc_exprs { [val[0]] + val[2] }
wc_exprs_opt: { [] } | wc_exprs

loop_inv: free_opt 'invariant' expr ';' { LoopInvariant.new free: val[0], expression: val[2] }
loop_invs: { [] } | loop_inv loop_invs { [val[0]] + val[1] }
free_opt: { false } | 'free' { true }

blocks:
  { [Block.new(names: [], statements: [])] }
  | name ':' blocks {
    bs = val[2]
    bs.first.prepend_children(:names,val[0])
    bs
  }
  | stmt blocks {
    bs = val[1]
    bs.unshift(Block.new(names: [], statements: [])) unless bs.first.names.empty?
    bs.first.prepend_children(:statements,val[0])
    bs
  }

body: '{' var_decls blocks '}' { Body.new locals: val[1], blocks: val[2] }

decl:
  type_decl
  | const_decl
  | func_decl
  | axiom_decl
  | var_decl
  | proc_decl
  | impl_decl
decls: { [] } | decl decls { [val[0]] + val[1] }

type_decl: 'type' attrs finite_opt name tc_params type_syn ';' {
  if val[5] && val[2]
    abort "Illegal declaration of type #{([val[3]] + val[4]) * " "}"
  end
  TypeDeclaration.new attributes: val[1], finite: val[2], name: val[3],
    arguments: val[4], type: val[5]
}
finite_opt: { false } | 'finite' { true }
tc_params: { [] } | name tc_params { [val[0]] + val[1] }
type_syn: { nil } | '=' type { val[1] }

const_decl: 'const' attrs unique_opt typed_ids order_spec ';' {
  ConstantDeclaration.new(val[3].merge({attributes: val[1], unique: val[2], order_spec: val[4]}))
}
unique_opt: { false } | 'unique' { true }
order_spec: parent_info complete_opt { [val[0],val[1]] }
parent_info: { nil } | '<:' parent_edges_opt { val[1] }
parent_edge: unique_opt ident {
  id = StorageIdentifier.new val[1]
  [val[0],id]
}
parent_edges: parent_edge { [val[0]] } | parent_edge ',' parent_edges { [val[0]] + val[2] }
parent_edges_opt: { [] } | parent_edges
complete_opt: { false } | 'complete' { true }

func_decl: 'function' attrs name type_args '(' fargs_opt ')' 'returns' '(' farg ')' fbody {
  FunctionDeclaration.new attributes: val[1], name: val[2],
    type_arguments: val[3], arguments: val[5], return: val[9], body: val[11]
}

farg:
  typed_ids { StorageDeclaration.new val[0] }
  | type { StorageDeclaration.new(names: [], type: val[0]) }

fargs:
  type { [{names: [], type: val[0]}] }
  | type ',' fargs {
    if val[2].first[:names].empty?
      [{names: [], type: val[0]}] + val[2]
    else
      val[2].first[:names].unshift(val[0])
      val[2]
    end
  }
  | type ':' fargs {
    # assert val[2].first[:names].empty?

    unless val[0].respond_to?(:name)
      raise ParseError, "parse error on value #{val[0]}: expecting name."
    end

    if val[2].first[:names].empty?
      val[2].first[:names].unshift(val[0])
      val[2]
    else
      [{names: [val[0]], type: val[2].first[:names].shift}] + val[2]
    end
  }
fargs_opt:
  { [] }
  | fargs {
    val[0].map do |x|
      x[:names].map!{|t| t.name}
      StorageDeclaration.new(x)
    end
  }
fbody: ';' { nil } | '{' expr '}' { val[1] }

axiom_decl: 'axiom' attrs expr ';' {
  AxiomDeclaration.new attributes: val[1], expression: val[2]
}

var_decl: 'var' attrs typed_ids_where ';' {
  VariableDeclaration.new(val[2].merge({attributes: val[1]}))
}
typed_ids: names ':' type { {names: val[0], type: val[2]} }
typed_ids_where: typed_ids where_clause { val[0].merge(val[1]) }
var_decls: { [] } | var_decl var_decls { [val[0]] + val[1] }
where_clause: { {} } | 'where' expr { {where: val[1]} }

proc_decl:
  'procedure' attrs name type_args '(' param_decls_opt ')' out_params pspec {
    ProcedureDeclaration.new attributes: val[1], name: val[2],
      type_arguments: val[3], parameters: val[5], returns: val[7],
      specifications: val[8][:specs], body: val[8][:body]
  }
out_params: { [] } | 'returns' '(' param_decls_opt ')' { val[2] }
pspec: ';' specs { {specs: val[1], body: nil} } | specs body { {specs: val[0], body: val[1]} }

param_decl: typed_ids_where { StorageDeclaration.new val[0] }
param_decls: param_decl { [val[0]] } | param_decl ',' param_decls { [val[0]] + val[2] }
param_decls_opt: { [] } | param_decls

spec:
  free_opt 'requires' attrs expr ';' {
    RequiresClause.new free: val[0], attributes: val[2], expression: val[3]
  }
  | free_opt 'modifies' attrs idents ';' {
    ids = val[3].map{|id| StorageIdentifier.new id}
    ModifiesClause.new free: val[0], attributes: val[2], identifiers: ids
  }
  | free_opt 'ensures' attrs expr ';' {
    EnsuresClause.new free: val[0], attributes: val[2], expression: val[3]
  }
specs: { [] } | spec specs { [val[0]] + val[1] }

impl_decl:
  'implementation' attrs name type_args '(' param_decls_opt ')' out_params body {
    ImplementationDeclaration.new attributes: val[1], name: val[2],
      type_arguments: val[3], parameters: val[5], returns: val[7],
      specifications: [], body: val[8]
  }

program: decls { Program.new declarations: val[0] }

end

—- header require_relative 'lexer.rex' require_relative 'ast/token' require_relative 'ast/program' require_relative 'ast/declaration' require_relative 'ast/specification' require_relative 'ast/statement' require_relative 'ast/expression' require_relative 'ast/type' include Bpl::AST

—- inner def parse(input)

scan_str(input)

end

def parse_special(str, kind)

scan_setup("$$PARSE_#{kind.upcase}$$ " + str)
do_parse

end

def parse_decl(str) parse_special(str, :decl) end def parse_param(str) parse_special(str, :param) end def parse_spec(str) parse_special(str, :spec) end def parse_blocks(str) parse_special(str, :blocks) end def parse_block(str) parse_special(str, :blocks).first end def parse_stmt(str) parse_special(str, :stmt) end def parse_expr(str) parse_special(str, :expr) end def parse_type(str) parse_special(str, :type) end

def parse_str(str)

case str
when /\b(type|const|function|axiom|var|procedure|implementation)\b/
  parse_decl(str)
when /\A\s*#{Bpl::IDENTIFIER}:.*;.*\s+#{Bpl::IDENTIFIER}:/m
  parse_blocks(str)
when /\A\s*#{Bpl::IDENTIFIER}:.*;/m
  parse_block(str)
when /\b(assert|assume|havoc|call|if|while|break|goto|return)\b|:=/
  parse_stmt(str)
when /\b(requires|ensures|modifies|invariant)\b/
  parse_spec(str)
when /[^<:]:[^:]/
  parse_param(str)
else
  parse_expr(str)
end

end

—- footer