(* Add some standard variables to the environment. *)
let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
let expr_of_pattern = function
- | Ast.PTactic (loc, tactic, targs) ->
- Ast.ETacticCtor (loc, tactic, List.map expr_of_substs targs)
+ | Ast.PPred (loc, pred, targs) ->
+ Ast.EPredCtor (loc, pred, List.map expr_of_substs targs)
in
let pexprs = List.map expr_of_pattern patterns in
let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
| d :: _ -> Ast.Env.add "^" d env in
let r = Eval.run_code env loc code in
if r <> 0 then
- failwithf "goal ‘%s’ failed with exit code %d" name r;
+ failwithf "%a: goal ‘%s’ failed with exit code %d"
+ Ast.string_loc loc debug_goal r;
(* Check all targets were updated after the code was
* run (else it's an error).
match pattern_still_needs_rebuild with
| None -> ()
| Some pattern ->
- failwithf "%a: goal %s ran successfully but it did not rebuild %a"
+ failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a"
Ast.string_loc loc debug_goal Ast.string_pattern pattern
)
)
Ast.string_loc loc Ast.string_pattern pattern;
match pattern with
- | Ast.PTactic (loc, tactic, targs) ->
- (* Look up the tactic. *)
- let params, code = Ast.gettactic env loc tactic in
+ | Ast.PPred (loc, pred, targs) ->
+ (* Look up the predicate. *)
+ let params, code = Ast.getpred env loc pred in
(* Resolve the targs down to constants. Since needs_rebuild
* should be called with env containing the goal params, this
- * should substitute any parameters in the tactic arguments.
+ * should substitute any parameters in the predicate arguments.
*)
let targs = List.map (Eval.substitute env loc) targs in
let targs =
Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
(* Create a new environment binding parameter names
- * to tactic args.
+ * to predicate args.
*)
let env =
let params =
try List.combine params targs
with Invalid_argument _ ->
- failwithf "%a: calling tactic ‘%s’ with wrong number of arguments"
- Ast.string_loc loc tactic in
+ failwithf "%a: calling predicate ‘%s’ with wrong number of arguments"
+ Ast.string_loc loc pred in
List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
(* Add some standard variables to the environment. *)
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
- failwithf "tactic ‘%s’ failed with exit code %d" tactic r
+ else (
+ let targs = List.map (Ast.string_expr ()) targs in
+ let targs = String.concat ", " targs in
+ failwithf "%a: predicate ‘%s (%s)’ failed with exit code %d"
+ Ast.string_loc loc pred targs r
+ )
-and exists_runner env loc p debug_tactic =
- Cmdline.debug "%a: running implicit existence rule for tactic %s"
- Ast.string_loc loc debug_tactic;
+and exists_runner env loc p debug_pred =
+ Cmdline.debug "%a: running implicit existence rule for predicate %s"
+ Ast.string_loc loc debug_pred;
if needs_rebuild env loc [] [] p then
- failwithf "%a: don't know how to build %s" Ast.string_loc loc debug_tactic
+ failwithf "%a: don't know how to build ‘%s’"
+ Ast.string_loc loc debug_pred