c59a555069a6052071ec87631c30f3992034b25f
[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 Utils
22 open Printf
23
24 (* There are several circular dependencies between the lexer
25  * (caused by includes) and eval.  These references break
26  * the circular dependencies.  They are initialized when
27  * the program starts, hence are never really None.
28  *)
29 let lexer_read = ref None
30 let eval_substitute = ref None
31
32 let find_on_include_path filename =
33   if not (Filename.is_implicit filename) then filename
34   else (
35     let rec loop = function
36       | [] -> filename
37       | inc :: incs ->
38          let path = inc // filename in
39          if Sys.file_exists path then path else loop incs
40     in
41     loop Cmdline.includes
42   )
43
44 let do_include env loc filename optflag file =
45   let eval_substitute =
46     match !eval_substitute with None -> assert false | Some f -> f in
47   let filename = eval_substitute env loc filename in
48   let filename = find_on_include_path filename in
49   if optflag && not (Sys.file_exists filename) then env
50   else (
51     let fp = open_in filename in
52     let lexbuf = Lexing.from_channel fp in
53     lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
54     let lexer_read =
55       match !lexer_read with None -> assert false | Some r -> r in
56     let env' = file lexer_read lexbuf in
57     close_in fp;
58     Ast.Env.merge env env'
59   )
60 %}
61
62 (* Tokens. *)
63 %token <Ast.substs> CODE
64 %token COLON
65 %token COMMA
66 %token EQUALS
67 %token EOF
68 %token EXPRESSION
69 %token FUNCTION
70 %token GOAL
71 %token <string> ID
72 %token INCLUDE
73 %token LEFT_ARRAY
74 %token LEFT_PAREN
75 %token LET
76 %token OPTINCLUDE
77 %token RETURNING
78 %token RIGHT_ARRAY
79 %token RIGHT_PAREN
80 %token SEMICOLON
81 %token <Ast.substs> STRING
82 %token STRING_KEYWORD
83 %token STRINGS
84 %token <string> TACTIC
85 %token TACTIC_KEYWORD
86
87 (* Start nonterminals. *)
88 %start <Ast.expr Ast.Env.t> file
89 %start <Ast.expr> expr
90 %%
91
92 file:
93     | stmts EOF  { $1 }
94     ;
95
96 stmts:
97     | (* none *) { Ast.Env.empty }
98     | stmts INCLUDE STRING option(SEMICOLON)
99     { do_include $1 $loc $3 false file }
100     | stmts OPTINCLUDE STRING option(SEMICOLON)
101     { do_include $1 $loc $3 true file }
102     | stmts stmt option(SEMICOLON)
103     { let name, expr = $2 in Ast.Env.add name expr $1 }
104     ;
105
106 stmt:
107     | option(goal_stmt) patterns COLON barelist option(CODE)
108     { let name, params =
109         match $1 with
110         | None ->
111            sprintf "_goal@%d" $startpos.pos_lnum, []
112         | Some x -> x in
113       name, Ast.EGoalDefn ($loc, (params, $2, $4, $5))
114     }
115     | goal_stmt CODE
116     {
117       let name, params = $1 in
118       name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
119     }
120     | FUNCTION ID params_decl return_decl EQUALS CODE
121     {
122       $2, Ast.EFuncDefn ($loc, ($3, $4, $6))
123     }
124     | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
125     {
126       $2, Ast.ETacticDefn ($loc, ($3, $5))
127     }
128     | LET ID EQUALS expr { $2, $4 }
129     ;
130
131 goal_stmt:
132     | GOAL ID option(params_decl) EQUALS
133     { $2, match $3 with None -> [] | Some ps -> ps }
134     ;
135 params_decl:
136     | LEFT_PAREN separated_list(COMMA, param_decl) RIGHT_PAREN { $2 }
137     ;
138 param_decl:
139     | ID         { $1 }
140 return_decl:
141     |            { RetExpr }
142     | RETURNING EXPRESSION { RetExpr }
143     | RETURNING STRINGS { RetStrings }
144     | RETURNING STRING_KEYWORD { RetString }
145
146 patterns:
147     | separated_list(COMMA, pattern) { $1 }
148     ;
149 pattern:
150     | STRING     { Ast.PTactic ($loc, "*file", [$1]) }
151     | TACTIC pattern_params { Ast.PTactic ($loc, $1, $2) }
152     ;
153 pattern_params:
154     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
155     ;
156 pattern_param:
157     | STRING     { $1 }
158     ;
159
160 expr:
161     | ID params  { Ast.ECall ($loc, $1, $2) }
162     | ID         { Ast.EVar ($loc, $1) }
163     | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
164     | STRING     { Ast.ESubsts ($loc, $1) }
165     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
166     ;
167 barelist:
168     | right_flexible_list(COMMA, expr) { $1 }
169     ;
170 params:
171     | LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
172     ;
173
174 (* http://gallium.inria.fr/blog/lr-lists/ *)
175 right_flexible_list(delim, X):
176     | (* nothing *) { [] }
177     | x = X { [x] }
178     | x = X delim xs = right_flexible_list(delim, X) { x :: xs }