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 substituting
187 * the output into an EList.
189 * XXX In future allow functions to be annotated with a return type.
191 and call_function env loc name args (params, code) =
192 (* This is used to print the function in debug and error messages only. *)
194 sprintf "%s (%s)" name
195 (String.concat ", " (List.map (Ast.string_expr ()) args)) in
196 Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func;
198 (* Evaluate function args. Must be done before updating the environment. *)
199 let args = List.map (evaluate_goal_arg env) args in
201 (* Create a new environment which maps the parameter names to
206 try List.combine params args
207 with Invalid_argument _ ->
208 failwithf "%a: calling function %s with wrong number of arguments, expecting %d args but got %d args"
209 Ast.string_loc loc debug_func
210 (List.length params) (List.length args) in
211 List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
214 let code = to_shell_script env loc code in
215 let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in
217 let chan = Unix.open_process_in code in
218 let lines = ref [] in
219 (try while true do lines := input_line chan :: !lines done
220 with End_of_file -> ());
221 let lines = List.rev !lines in
222 let st = Unix.close_process_in chan in
224 | Unix.WEXITED 0 -> ()
226 eprintf "*** function ‘%s’ failed with exit code %d\n" name i
227 | Unix.WSIGNALED i ->
228 eprintf "*** function ‘%s’ killed by signal %d\n" name i
230 eprintf "*** function ‘%s’ stopped by signal %d\n" name i
233 Ast.EList (Ast.noloc,
234 (List.map (fun line ->
235 Ast.EConstant (Ast.noloc, Ast.CString line))