List.iter (run_target env) exprs
and run_target env = function
- | Ast.EGoalDefn _ | Ast.ETacticDefn _ -> assert false
+ | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.ETacticDefn _ -> assert false
- (* Call a goal. *)
- | Ast.ECallGoal (loc, name, args) ->
- let goal = Ast.getgoal env loc name in
- run_goal env loc name args goal
+ (* Call a goal or function. *)
+ | Ast.ECall (loc, name, args) ->
+ let expr = Ast.getvar env loc name in
+ (match expr with
+ | Ast.EGoalDefn (_, goal) ->
+ run_goal env loc name args goal []
+ | Ast.EFuncDefn (_, func) ->
+ let expr = Eval.call_function env loc name args func in
+ run_target env expr
+ | _ ->
+ failwithf "%a: tried to call ‘%s’ which is not a goal or a function"
+ Ast.string_loc loc name
+ )
(* Call a tactic. *)
| Ast.ETacticCtor (loc, name, args) ->
| Ast.EVar (loc, name) ->
let expr = Ast.getvar env loc name in
(match expr with
- | EGoalDefn (loc, ([], _, _, _)) ->
- run_target env (Ast.ECallGoal (loc, name, []))
+ | Ast.EGoalDefn (loc, ([], _, _, _)) ->
+ run_target env (Ast.ECall (loc, name, []))
| EGoalDefn _ ->
failwithf "%a: cannot call %s() since this goal has parameters"
Ast.string_loc loc name
run_tactic env loc "*file" [c]
(* Run a goal by name. *)
-and run_goal env loc name args (params, patterns, deps, code) =
- Cmdline.debug "%a: running goal %s %a"
- Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args));
+and run_goal env loc name args (params, patterns, deps, code) extra_deps =
+ (* This is used to print the goal in debug and error messages only. *)
+ let debug_goal =
+ sprintf "%s (%s)" name
+ (String.concat ", " (List.map (Ast.string_expr ()) args)) in
+ Cmdline.debug "%a: running goal %s" Ast.string_loc loc debug_goal;
(* This is the point where we evaluate the goal arguments. We must
* do this before creating the new environment, because variables
let params =
try List.combine params args
with Invalid_argument _ ->
- failwithf "%a: calling goal ‘%s’ with wrong number of arguments"
- Ast.string_loc loc name in
+ failwithf "%a: calling goal %s with wrong number of arguments, expecting %d args but got %d args"
+ Ast.string_loc loc debug_goal
+ (List.length params) (List.length args) in
List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
(* Check all dependencies have been updated. *)
- run_targets env deps;
+ run_targets env (deps @ extra_deps);
(* Check if any target (ie. pattern) needs to be rebuilt.
* As with make, a goal with no targets is always run.
*)
let rebuild =
- patterns = [] || List.exists (needs_rebuild env loc deps) patterns in
+ patterns = [] ||
+ List.exists (needs_rebuild env loc deps extra_deps) patterns in
if rebuild then (
(* Run the code (if any). *)
let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
let env =
+ (* NB: extra_deps are not added to %^ *)
match deps with
| [] -> env
| d :: _ -> Ast.Env.add "^" d env in
- let code = Eval.to_shell_script env loc code in
- let code = "set -e\nset -x\n\n" ^ code in
- let r = Sys.command code in
+ let r = Eval.run_code env loc code in
if r <> 0 then (
eprintf "*** goal ‘%s’ failed with exit code %d\n" name r;
exit 1
* run (else it's an error).
*)
let pattern_still_needs_rebuild =
- try Some (List.find (needs_rebuild env loc deps) patterns)
- with Not_found -> None in
+ try
+ Some (List.find (needs_rebuild env loc deps extra_deps) patterns)
+ with
+ Not_found -> None in
match pattern_still_needs_rebuild with
| None -> ()
| Some pattern ->
- failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a"
- Ast.string_loc loc
- name
- Ast.string_pattern pattern
+ failwithf "%a: goal %s ran successfully but it did not rebuild %a"
+ Ast.string_loc loc debug_goal Ast.string_pattern pattern
)
)
(* Return whether the target (pattern) needs to be rebuilt. *)
-and needs_rebuild env loc deps pattern =
+and needs_rebuild env loc deps extra_deps pattern =
Cmdline.debug "%a: testing if %a needs rebuild"
Ast.string_loc loc Ast.string_pattern pattern;
* should be called with env containing the goal params, this
* should substitute any parameters in the tactic arguments.
*)
- let targs = List.map (Ast.substitute env loc) targs in
+ let targs = List.map (Eval.substitute env loc) targs in
let targs =
List.map (fun targ ->
Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
(* Add some standard variables to the environment. *)
let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
let env =
+ (* NB: extra_deps are not added to %^ *)
match deps with
| [] -> env
| d :: _ -> Ast.Env.add "^" d env in
- let code = Eval.to_shell_script env loc code in
- let code = "set -e\nset -x\n\n" ^ code in
- let r = Sys.command code in
+ let r = Eval.run_code env loc code in
if r = 99 (* means "needs rebuild" *) then true
else if r = 0 (* means "doesn't need rebuild" *) then false
else (
* cargs is a list of parameters (all constants).
*)
and run_tactic env loc tactic cargs =
- Cmdline.debug "%a: running tactic %s" Ast.string_loc loc tactic;
+ (* This is used to print the tactic in debug and error messages only. *)
+ let debug_tactic =
+ Ast.string_expr ()
+ (Ast.ETacticCtor (loc, tactic,
+ List.map (fun c -> Ast.EConstant (loc, c)) cargs)) in
+ Cmdline.debug "%a: running tactic %s" Ast.string_loc loc debug_tactic;
(* Find all goals in the environment. Returns a list of (name, goal). *)
let goals =
*)
let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
let p = Ast.PTactic (loc, tactic, targs) in
- if needs_rebuild env loc [] p then (
- let t = Ast.ETacticCtor (loc, tactic,
- List.map (fun c -> Ast.EConstant (loc, c))
- cargs) in
- failwithf "%a: don't know how to build %a"
- Ast.string_loc loc Ast.string_expr t
- )
+ if needs_rebuild env loc [] [] p then
+ failwithf "%a: don't know how to build %s"
+ Ast.string_loc loc debug_tactic
+
+ | [_, name, goal, args] ->
+ (* Single goal matches, run it. *)
+ run_goal env loc name args goal []
| goals ->
- (* One or more goals match. We run them all (although if
- * one of them succeeds in rebuilding, it will cut short the rest).
+ (* Two or more goals match. Only one must have a CODE section,
+ * and we combine the dependencies into a "supergoal".
*)
- List.iter (
- fun (_, name, goal, args) ->
- run_goal env loc name args goal
- ) goals
+ let with_code, without_code =
+ List.partition (
+ fun (_, _, (_, _, _, code), _) -> code <> None
+ ) goals in
+
+ let (_, name, goal, args), extra_deps =
+ match with_code with
+ | [g] ->
+ let extra_deps =
+ List.flatten (
+ List.map (fun (_, _, (_, _, deps, _), _) -> deps) without_code
+ ) in
+ (g, extra_deps)
+
+ | [] ->
+ (* This is OK, it means we'll rebuild all dependencies
+ * but there is no code to run. Pick the first goal
+ * without code and the dependencies from the other goals.
+ *)
+ let g = List.hd without_code in
+ let extra_deps =
+ List.flatten (
+ List.map (fun (_, _, (_, _, deps, _), _) -> deps)
+ (List.tl without_code)
+ ) in
+ (g, extra_deps)
+
+ | _ :: _ ->
+ failwithf "%a: multiple goals found which match tactic %s, but more than one of these goals have {code} sections which is not allowed"
+ Ast.string_loc loc debug_tactic in
+
+ run_goal env loc name args goal extra_deps
(* Test if pattern matches *tactic(cargs). If it does
* then we return Some args where args is the arguments that must
git.annexia.org / goals.git / blobdiff