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 evaluate_goal_arg env = function
146 | Ast.EVar (loc, name) ->
147 let expr = Ast.getvar env loc name in
148 evaluate_goal_arg env expr
150 | ESubsts (loc, str) ->
151 let str = substitute env loc str in
152 Ast.EConstant (loc, Ast.CString str)
154 | EList (loc, exprs) ->
155 Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
157 | ETacticCtor (loc, name, exprs) ->
158 Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
160 | ECall (loc, name, args) ->
161 let expr = Ast.getvar env loc name in
164 (* Goals don't return anything so they cannot be used in
165 * goal args. Use a function instead.
167 failwithf "%a: cannot use goal call ‘%s’ in goal argument"
168 Ast.string_loc loc name
170 | EFuncDefn (loc, func) ->
171 call_function env loc name args func
174 failwithf "%a: cannot call ‘%s’ which is not a function"
175 Ast.string_loc loc name
181 | ETacticDefn _ as e -> e
183 (* Functions are only called from goal args or when substituting
184 * into a shell script or constant expression (this may change if we
185 * implement ‘:=’ assignment for variables). This evaluates a
186 * function by running the associated shell script and parsing
187 * the output as an expression.
189 and call_function env loc name args (params, code) =
190 (* This is used to print the function in debug and error messages only. *)
192 sprintf "%s (%s)" name
193 (String.concat ", " (List.map (Ast.string_expr ()) args)) in
194 Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func;
196 (* Evaluate function args. Must be done before updating the environment. *)
197 let args = List.map (evaluate_goal_arg env) args in
199 (* Create a new environment which maps the parameter names to
204 try List.combine params args
205 with Invalid_argument _ ->
206 failwithf "%a: calling function %s with wrong number of arguments, expecting %d args but got %d args"
207 Ast.string_loc loc debug_func
208 (List.length params) (List.length args) in
209 List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
212 let code = to_shell_script env loc code in
213 let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in
215 let chan = Unix.open_process_in code in
216 let b = Buffer.create 1024 in
219 Buffer.add_string b (input_line chan);
220 Buffer.add_char b '\n'
222 with End_of_file -> ());
223 let st = Unix.close_process_in chan in
225 | Unix.WEXITED 0 -> ()
227 eprintf "*** function ‘%s’ failed with exit code %d\n" name i
228 | Unix.WSIGNALED i ->
229 eprintf "*** function ‘%s’ killed by signal %d\n" name i
231 eprintf "*** function ‘%s’ stopped by signal %d\n" name i
234 Parse.parse_expr (sprintf "function:%s" name) (Buffer.contents b)