Define *file() syntax for tactic constructors.
[goals.git] / 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
40 (* Start nonterminals. *)
41 %start <Ast.env> file
42 %start <Ast.expr> expr
43 %%
44
45 file:
46     | stmts EOF  { $1 }
47     ;
48
49 stmts:
50     | list(stmt)
51     { List.fold_left (
52         fun env (name, expr) -> Ast.StringMap.add name expr env
53       ) Ast.StringMap.empty $1
54     }
55     ;
56 stmt:
57     | option(goal_stmt) patterns COLON barelist option(CODE)
58     { let name, params =
59         match $1 with
60         | None ->
61            sprintf "_goal@%d" $startpos.pos_lnum, []
62         | Some x -> x in
63       name, Ast.EGoal ($loc, (params, $2, $4, $5))
64     }
65     | goal_stmt CODE
66     {
67       let name, params = $1 in
68       name, Ast.EGoal ($loc, (params, [], [], Some $2))
69     }
70     | LET ID EQUALS expr { $2, $4 }
71     ;
72
73 goal_stmt:
74     | GOAL ID option(param_decl) EQUALS
75     { $2, match $3 with None -> [] | Some ps -> ps }
76     ;
77 param_decl:
78     | LEFT_PAREN separated_list(COMMA, ID) RIGHT_PAREN { $2 }
79     ;
80
81 patterns:
82     | separated_list(COMMA, pattern) { $1 }
83     ;
84 pattern:
85     | STRING     { Ast.PTactic ($loc, "file", [$1]) }
86     | ID pattern_params { Ast.PTactic ($loc, $1, $2) }
87     | ID         { Ast.PVar ($loc, $1) }
88     ;
89 pattern_params:
90     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
91     ;
92 pattern_param:
93     | STRING     { $1 }
94     ;
95
96 expr:
97     | ID params  { Ast.ECall ($loc, $1, $2) }
98     | ID         { Ast.EVar ($loc, $1) }
99     | TACTIC params { Ast.ETactic ($loc, $1, $2) }
100     | STRING     { Ast.ESubsts ($loc, $1) }
101     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
102     ;
103 barelist:
104     | separated_list(COMMA, expr) { $1 }
105     ;
106 params:
107     | LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
108     ;