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 evaluate_targets env exprs =
23 List.iter (evaluate_target env) exprs
25 and evaluate_target env = function
26 | Ast.EGoal _ -> assert false
29 | Ast.ECall (loc, name, args) ->
31 try Ast.StringMap.find name env
33 failwithf "%a: goal ‘%s’ not found" Ast.string_loc loc name in
36 | Ast.EGoal (loc, goal) -> goal
38 failwithf "%a: tried to call ‘%s’ which is not a goal"
39 Ast.string_loc loc name in
40 run_goal loc env name args goal
42 | Ast.ETactic (loc, name, args) ->
43 (* All parameters of tactics must be simple expressions (strings,
44 * in future booleans, numbers, etc).
46 let args = List.map (simplify env) args in
47 run_goal_for_tactic loc env name args
49 (* Look up the variable and substitute it. *)
50 | Ast.EVar (loc, name) ->
52 try Ast.StringMap.find name env
54 failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
55 evaluate_target env expr
57 (* Lists are inlined when found as a target. *)
58 | Ast.EList (loc, exprs) ->
59 evaluate_targets env exprs
61 (* A string (with or without substitutions) implies *file(filename). *)
62 | Ast.ESubsts (loc, str) ->
63 let str = substitute loc env str in
64 run_goal_for_tactic loc env "file" [Ast.CString str]
66 | Ast.EConstant (loc, c) ->
67 run_goal_for_tactic loc env "file" [c]
69 (* Find the goal which matches the given tactic and run it.
70 * Params is a list of constants.
72 and run_goal_for_tactic loc env tactic const_args =
73 (* Search across all goals for a matching tactic. *)
75 let env = Ast.StringMap.bindings env in
77 (function (name, Ast.EGoal (loc, goal)) -> Some (name, goal) | _ -> None)
80 (* If there are multiple goals matching, this must choose
81 * the most recently defined (XXX).
85 (fun (_, (_, patterns, _, _)) ->
86 List.exists (matching_pattern loc env tactic const_args) patterns)
90 failwithf "%a: don't know how to build %s %s"
94 (List.map (function Ast.CString s -> s) const_args)) in
96 let args = [] (* XXX calculate free variables *) in
97 run_goal loc env name args goal
99 (* XXX This only does exact matches at the moment. *)
100 and matching_pattern loc env tactic const_args = function
101 | Ast.PTactic (loc, constructor, params)
102 when tactic = constructor &&
103 List.length const_args = List.length params ->
104 (* Try to simplify the parameters of this pattern down
105 * to constants, but don't fail here if we can't do this.
108 let params = List.map (substitute loc env) params in
109 let params = List.map (fun s -> Ast.CString s) params in
111 with Failure _ -> false
114 | Ast.PTactic _ -> false
116 | Ast.PVar (loc, name) -> assert false
118 NOT IMPLEMENTED - we need variables to contain constructors!
120 let expr = Ast.StringMap.find name env in
121 let expr = simplify env expr in
122 with Not_found -> false
126 (* Run a named goal. *)
127 and run_goal loc env name args (params, patterns, deps, code) =
128 (* Substitute the args for the parameters in the environment. *)
130 try List.combine params args
131 with Invalid_argument _ ->
132 failwithf "%a: calling goal ‘%s’ with wrong number of arguments"
133 Ast.string_loc loc name in
135 List.fold_left (fun env (k, v) -> Ast.StringMap.add k v env)
138 (* Evaluate the dependencies first. *)
139 evaluate_targets env deps;
141 (* Check if any target needs to be updated. *)
144 (* Run the code (if any). *)
148 let code = substitute loc env code in
149 Printf.printf "running : %s\n" code
152 (* Check all targets were updated (else it's an error). *)
155 (* Take any expression and simplify it down to a constant.
156 * If the expression cannot be simplified then this throws
159 and simplify env = function
160 | Ast.EConstant (loc, c) -> c
162 | Ast.EVar (loc, name) ->
164 try Ast.StringMap.find name env
166 failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
169 | Ast.ESubsts (loc, str) ->
170 Ast.CString (substitute loc env str)
172 | Ast.EList (loc, _) ->
173 failwithf "%a: list found where constant expression expected"
176 | Ast.ECall (loc, name, _) ->
177 failwithf "%a: cannot use goal ‘%s’ in constant expression"
178 Ast.string_loc loc name
180 | Ast.ETactic (loc, name, _) ->
181 failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
182 Ast.string_loc loc name
184 | Ast.EGoal (loc, _) ->
185 failwithf "%a: cannot use goal in constant expression"
188 (* Take a substitution list and try to turn it into a simple
189 * string by evaluating every variable. If not possible this
190 * throws an error. Returns a string.
192 and substitute loc env substs =
193 let b = Buffer.create 13 in
196 | Ast.SString s -> Buffer.add_string b s
199 try Ast.StringMap.find name env
201 failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
202 match simplify env expr with
203 | Ast.CString s -> Buffer.add_string b s