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.
22 let rec to_constant env = function
23 | Ast.EConstant (loc, c) -> c
26 let expr = Ast.getvar env loc name in
29 | ESubsts (loc, str) ->
30 CString (substitute env loc str)
33 failwithf "%a: list found where constant expression expected"
36 | ECallGoal (loc, name, _) ->
37 failwithf "%a: cannot use goal ‘%s’ in constant expression"
38 Ast.string_loc loc name
40 | ETacticCtor (loc, name, _) ->
41 failwithf "%a: cannot use tactic ‘%s’ in constant expression"
42 Ast.string_loc loc name
44 | EGoalDefn (loc, _) ->
45 failwithf "%a: cannot use goal in constant expression"
48 | ETacticDefn (loc, _) ->
49 failwithf "%a: cannot use tactic in constant expression"
52 and substitute env loc substs =
53 let b = Buffer.create 13 in
56 | Ast.SString s -> Buffer.add_string b s
58 let expr = Ast.getvar env loc name in
59 match to_constant env expr with
60 | Ast.CString s -> Buffer.add_string b s
64 let rec to_shell_script env loc substs =
65 let b = Buffer.create 13 in
68 | Ast.SString s -> Buffer.add_string b s
70 let expr = Ast.getvar env loc name in
71 let s = expr_to_shell_string env expr in
76 and expr_to_shell_string env = function
77 | Ast.EConstant (loc, CString s) -> Filename.quote s
80 let expr = Ast.getvar env loc name in
81 expr_to_shell_string env expr
83 | ESubsts (loc, str) ->
84 Filename.quote (substitute env loc str)
86 | EList (loc, exprs) ->
87 let strs = List.map (expr_to_shell_string env) exprs in
88 (* These are shell quoted so we can just concat them with space. *)
89 String.concat " " strs
91 | ECallGoal (loc, name, _) ->
92 failwithf "%a: cannot use goal ‘%s’ in shell expansion"
93 Ast.string_loc loc name
95 (* Tactics expand to the first parameter. *)
96 | ETacticCtor (loc, _, []) -> Filename.quote ""
97 | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
99 | EGoalDefn (loc, _) ->
100 failwithf "%a: cannot use goal in shell expansion"
103 | ETacticDefn (loc, _) ->
104 failwithf "%a: cannot use tactic in shell expansion"
107 let rec evaluate_goal_arg env = function
108 | Ast.EVar (loc, name) ->
109 let expr = Ast.getvar env loc name in
110 evaluate_goal_arg env expr
112 | ESubsts (loc, str) ->
113 let str = Ast.substitute env loc str in
114 Ast.EConstant (loc, Ast.CString str)
116 | EList (loc, exprs) ->
117 Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
119 | ETacticCtor (loc, name, exprs) ->
120 Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
122 | ECallGoal (loc, name, _) ->
123 (* Goals don't return anything so they cannot be used in
124 * goal args. Use a function instead.
126 failwithf "%a: cannot use goal ‘%s’ in goal argument"
127 Ast.string_loc loc name
131 | ETacticDefn _ as e -> e