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 goal_runner env loc name args
25 (params, patterns, deps, code) extra_deps debug_goal =
26 Cmdline.debug "%a: running goal %s" Ast.string_loc loc debug_goal;
28 (* Check if any target (ie. pattern) needs to be rebuilt.
29 * As with make, a goal with no targets is always run.
33 List.exists (needs_rebuild env loc deps extra_deps) patterns in
36 (* Run the code (if any). *)
38 | None -> () (* No { CODE } section. *)
41 (* Add some standard variables to the environment. *)
42 let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
43 let expr_of_pattern = function
44 | Ast.PTactic (loc, tactic, targs) ->
45 Ast.ETacticCtor (loc, tactic, List.map expr_of_substs targs)
47 let pexprs = List.map expr_of_pattern patterns in
48 let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
49 let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
51 (* NB: extra_deps are not added to %^ *)
54 | d :: _ -> Ast.Env.add "^" d env in
55 let r = Eval.run_code env loc code in
57 failwithf "%a: goal ‘%s’ failed with exit code %d"
58 Ast.string_loc loc debug_goal r;
60 (* Check all targets were updated after the code was
61 * run (else it's an error).
63 let pattern_still_needs_rebuild =
67 (needs_rebuild ~final_check:true env loc deps extra_deps)
72 match pattern_still_needs_rebuild with
75 failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a"
76 Ast.string_loc loc debug_goal Ast.string_pattern pattern
80 (* Return whether the target (pattern) needs to be rebuilt. *)
81 and needs_rebuild ?(final_check = false) env loc deps extra_deps pattern =
82 Cmdline.debug "%a: testing if %a needs rebuild"
83 Ast.string_loc loc Ast.string_pattern pattern;
86 | Ast.PTactic (loc, tactic, targs) ->
87 (* Look up the tactic. *)
88 let params, code = Ast.gettactic env loc tactic in
90 (* Resolve the targs down to constants. Since needs_rebuild
91 * should be called with env containing the goal params, this
92 * should substitute any parameters in the tactic arguments.
94 let targs = List.map (Eval.substitute env loc) targs in
97 Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
99 (* Create a new environment binding parameter names
104 try List.combine params targs
105 with Invalid_argument _ ->
106 failwithf "%a: calling tactic ‘%s’ with wrong number of arguments"
107 Ast.string_loc loc tactic in
108 List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
110 (* Add some standard variables to the environment. *)
111 let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
113 (*let b = Ast.EConstant (Ast.noloc, Ast.CBool final_check) in*)
114 let b = Ast.EConstant (Ast.noloc,
115 Ast.CString (if final_check then "1" else "")) in
116 Ast.Env.add "goals_final_check" b env in
118 (* NB: extra_deps are not added to %^ *)
121 | d :: _ -> Ast.Env.add "^" d env in
122 let r = Eval.run_code env loc code in
123 if r = 99 (* means "needs rebuild" *) then true
124 else if r = 0 (* means "doesn't need rebuild" *) then false
126 failwithf "%a: tactic ‘%s’ failed with exit code %d"
127 Ast.string_loc loc tactic r
129 and exists_runner env loc p debug_tactic =
130 Cmdline.debug "%a: running implicit existence rule for tactic %s"
131 Ast.string_loc loc debug_tactic;
133 if needs_rebuild env loc [] [] p then
134 failwithf "%a: don't know how to build ‘%s’"
135 Ast.string_loc loc debug_tactic