src/parser.mly

   1 (* Goalfile parser
   2  * Copyright (C) 2019 Richard W.M. Jones
   3  * Copyright (C) 2019 Red Hat Inc.
   4  *
   5  * This program is free software; you can redistribute it and/or modify
   6  * it under the terms of the GNU General Public License as published by
   7  * the Free Software Foundation; either version 2 of the License, or
   8  * (at your option) any later version.
   9  *
  10  * This program is distributed in the hope that it will be useful,
  11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13  * GNU General Public License for more details.
  14  *
  15  * You should have received a copy of the GNU General Public License along
  16  * with this program; if not, write to the Free Software Foundation, Inc.,
  17  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  18  *)
  19
  20 %{
  21 open Printf
  22 %}
  23
  24 (* Tokens. *)
  25 %token <Ast.substs> CODE
  26 %token COLON
  27 %token COMMA
  28 %token EQUALS
  29 %token EOF
  30 %token GOAL
  31 %token <string> ID
  32 %token LEFT_ARRAY
  33 %token LEFT_PAREN
  34 %token LET
  35 %token RIGHT_ARRAY
  36 %token RIGHT_PAREN
  37 %token <Ast.substs> STRING
  38 %token <string> TACTIC
  39 %token TACTIC_KEYWORD
  40
  41 (* Start nonterminals. *)
  42 %start <Ast.env> file
  43 %start <Ast.expr> expr
  44 %%
  45
  46 file:
  47     | stmts EOF  { $1 }
  48     ;
  49
  50 stmts:
  51     | list(stmt)
  52     { List.fold_left (
  53         fun env (name, expr) -> Ast.Env.add name expr env
  54       ) Ast.Env.empty $1
  55     }
  56     ;
  57 stmt:
  58     | option(goal_stmt) patterns COLON barelist option(CODE)
  59     { let name, params =
  60         match $1 with
  61         | None ->
  62            sprintf "_goal@%d" $startpos.pos_lnum, []
  63         | Some x -> x in
  64       name, Ast.EGoal ($loc, (params, $2, $4, $5))
  65     }
  66     | goal_stmt CODE
  67     {
  68       let name, params = $1 in
  69       name, Ast.EGoal ($loc, (params, [], [], Some $2))
  70     }
  71     | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
  72     {
  73       $2, Ast.ETactic ($loc, ($3, $5))
  74     }
  75     | LET ID EQUALS expr { $2, $4 }
  76     ;
  77
  78 goal_stmt:
  79     | GOAL ID option(params_decl) EQUALS
  80     { $2, match $3 with None -> [] | Some ps -> ps }
  81     ;
  82 params_decl:
  83     | LEFT_PAREN separated_list(COMMA, param_decl) RIGHT_PAREN { $2 }
  84     ;
  85 param_decl:
  86     | ID         { $1 }
  87
  88 patterns:
  89     | separated_list(COMMA, pattern) { $1 }
  90     ;
  91 pattern:
  92     | STRING     { Ast.PTactic ($loc, "*file", [$1]) }
  93     | ID pattern_params { Ast.PTactic ($loc, $1, $2) }
  94     ;
  95 pattern_params:
  96     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
  97     ;
  98 pattern_param:
  99     | STRING     { $1 }
 100     ;
 101
 102 expr:
 103     | ID params  { Ast.ECallGoal ($loc, $1, $2) }
 104     | ID         { Ast.EVar ($loc, $1) }
 105     | TACTIC params { Ast.ECallTactic ($loc, $1, $2) }
 106     | STRING     { Ast.ESubsts ($loc, $1) }
 107     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
 108     ;
 109 barelist:
 110     | separated_list(COMMA, expr) { $1 }
 111     ;
 112 params:
 113     | LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
 114     ;