1 (* Goalfile Abstract Syntax Tree
2 * Copyright (C) 2019 Richard W.M. Jones
3 * Copyright (C) 2019 Red Hat Inc.
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.
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.
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.
24 let rec to_constant env = function
25 | Ast.EConstant (loc, c) -> c
28 let expr = Ast.getvar env loc name in
31 | ESubsts (loc, str) ->
32 CString (substitute env loc str)
35 failwithf "%a: list found where constant expression expected"
38 | ECall (loc, name, args) ->
39 let expr = Ast.getvar env loc name in
42 (* Goals don't return anything so they cannot be used in
43 * constant expressions. Use a function instead.
45 failwithf "%a: cannot use goal call ‘%s’ in shell expansion"
46 Ast.string_loc loc name
48 | EFuncDefn (loc, func) ->
49 to_constant env (call_function env loc name args func)
52 failwithf "%a: cannot use ‘%s’ in constant expression"
53 Ast.string_loc loc name
56 | ETacticCtor (loc, name, _) ->
57 failwithf "%a: cannot use tactic ‘%s’ in constant expression"
58 Ast.string_loc loc name
60 | EGoalDefn (loc, _) ->
61 failwithf "%a: cannot use goal in constant expression"
64 | EFuncDefn (loc, _) ->
65 failwithf "%a: cannot use function in constant expression"
68 | ETacticDefn (loc, _) ->
69 failwithf "%a: cannot use tactic in constant expression"
72 and substitute env loc substs =
73 let b = Buffer.create 13 in
76 | Ast.SString s -> Buffer.add_string b s
78 let expr = Ast.getvar env loc name in
79 match to_constant env expr with
80 | Ast.CString s -> Buffer.add_string b s
84 and to_shell_script env loc substs =
85 let b = Buffer.create 13 in
88 | Ast.SString s -> Buffer.add_string b s
90 let expr = Ast.getvar env loc name in
91 let s = expr_to_shell_string env expr in
96 and expr_to_shell_string env = function
97 | Ast.EConstant (loc, CString s) -> Filename.quote s
100 let expr = Ast.getvar env loc name in
101 expr_to_shell_string env expr
103 | ESubsts (loc, str) ->
104 Filename.quote (substitute env loc str)
106 | EList (loc, exprs) ->
107 let strs = List.map (expr_to_shell_string env) exprs in
108 (* These are shell quoted so we can just concat them with space. *)
109 String.concat " " strs
111 | ECall (loc, name, args) ->
112 let expr = Ast.getvar env loc name in
115 (* Goals don't return anything so they cannot be used in
116 * shell script expansions. Use a function instead.
118 failwithf "%a: cannot use goal call ‘%s’ in shell expansion"
119 Ast.string_loc loc name
121 | EFuncDefn (loc, func) ->
122 expr_to_shell_string env (call_function env loc name args func)
125 failwithf "%a: cannot call ‘%s’ which is not a function"
126 Ast.string_loc loc name
129 (* Tactics expand to the first parameter. *)
130 | ETacticCtor (loc, _, []) -> Filename.quote ""
131 | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
133 | EGoalDefn (loc, _) ->
134 failwithf "%a: cannot use goal in shell expansion"
137 | EFuncDefn (loc, _) ->
138 failwithf "%a: cannot use function in shell expansion"
141 | ETacticDefn (loc, _) ->
142 failwithf "%a: cannot use tactic in shell expansion"
145 and run_code ?(quiet = false) env loc code =
146 let code = to_shell_script env loc code in
148 "source " ^ Filename.quote Cmdline.prelude_sh_file ^ "\n" ^
150 (if not quiet then "set -x\n" else "") ^
154 let chan = Unix.open_process_in code in
155 let b = Buffer.create 1024 in
158 Buffer.add_string b (input_line chan);
159 Buffer.add_char b '\n'
161 with End_of_file -> ());
162 let st = Unix.close_process_in chan in
165 | Unix.WEXITED i -> i
166 | Unix.WSIGNALED i ->
167 failwithf "%a: killed by signal %d" Ast.string_loc loc i
169 failwithf "%a: stopped by signal %d" Ast.string_loc loc i in
172 and evaluate_goal_arg env = function
173 | Ast.EVar (loc, name) ->
174 let expr = Ast.getvar env loc name in
175 evaluate_goal_arg env expr
177 | ESubsts (loc, str) ->
178 let str = substitute env loc str in
179 Ast.EConstant (loc, Ast.CString str)
181 | EList (loc, exprs) ->
182 Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
184 | ETacticCtor (loc, name, exprs) ->
185 Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
187 | ECall (loc, name, args) ->
188 let expr = Ast.getvar env loc name in
191 (* Goals don't return anything so they cannot be used in
192 * goal args. Use a function instead.
194 failwithf "%a: cannot use goal call ‘%s’ in goal argument"
195 Ast.string_loc loc name
197 | EFuncDefn (loc, func) ->
198 call_function env loc name args func
201 failwithf "%a: cannot call ‘%s’ which is not a function"
202 Ast.string_loc loc name
208 | ETacticDefn _ as e -> e
210 (* Functions are only called from goal args or when substituting
211 * into a shell script or constant expression (this may change if we
212 * implement ‘:=’ assignment for variables). This evaluates a
213 * function by running the associated shell script and parsing
214 * the output as an expression, string or list of strings.
216 and call_function env loc name args (params, returning, code) =
217 (* This is used to print the function in debug and error messages only. *)
219 sprintf "%s (%s) returning %s" name
220 (String.concat ", " (List.map (Ast.string_expr ()) args))
221 (match returning with RetExpr -> "expression"
222 | RetString -> "string"
223 | RetStrings -> "strings") in
224 Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func;
226 (* Evaluate function args. Must be done before updating the environment. *)
227 let args = List.map (evaluate_goal_arg env) args in
229 (* Create a new environment which maps the parameter names to
234 try List.combine params args
235 with Invalid_argument _ ->
236 failwithf "%a: calling function %s with wrong number of arguments, expecting %d args but got %d args"
237 Ast.string_loc loc debug_func
238 (List.length params) (List.length args) in
239 List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
241 let r, b = run_code env loc code in
243 eprintf "*** function ‘%s’ failed with exit code %d\n" name r;
248 | RetExpr -> Parse.parse_expr (sprintf "function:%s" name) b
249 | RetString -> Ast.EConstant (loc, Ast.CString b)
251 (* run_code always adds \n after the final line, so when we
252 * read it back we will get a final empty string which we
253 * have to drop. XXX Probably better to preserve the lines
254 * read from the external command.
256 let strs = nsplit "\n" b in
257 let strs = List.rev strs in
258 let strs = match strs with "" :: xs -> xs | xs -> xs in
259 let strs = List.rev strs in
260 let strs = List.map (fun s -> Ast.EConstant (loc, Ast.CString s)) strs in