X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Frun.ml;h=3a042565c2c8bcd8184ecd5e16f915a141a8f2cf;hb=98b795ddf06271fa8018edcd0bd15960871828fd;hp=55a2b8d085607275e35aab77f757210450ffd7fb;hpb=109185686ffdc00520eba2b4c3a92f10a111fb60;p=goals.git

diff --git a/src/run.ml b/src/run.ml
index 55a2b8d..3a04256 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -41,8 +41,8 @@ let rec goal_runner env loc name args
         (* 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
@@ -54,7 +54,8 @@ let rec goal_runner env loc name args
           | 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).
@@ -71,7 +72,7 @@ let rec goal_runner env loc name args
         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
     )
   )
@@ -82,13 +83,13 @@ and needs_rebuild ?(final_check = false) env loc deps extra_deps 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 =
@@ -96,14 +97,14 @@ and needs_rebuild ?(final_check = false) env loc deps extra_deps pattern =
            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. *)
@@ -121,12 +122,17 @@ and needs_rebuild ?(final_check = false) env loc deps extra_deps pattern =
      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