run: Add %goals_final_check variable when evaluating tactics.

[goals.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 2d4e326..55a2b8d 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -61,7 +61,11 @@ let rec goal_runner env loc name args
          *)
         let pattern_still_needs_rebuild =
           try
-            Some (List.find (needs_rebuild env loc deps extra_deps) patterns)
+            let pattern =
+              List.find
+                (needs_rebuild ~final_check:true env loc deps extra_deps)
+                patterns in
+            Some pattern
           with
             Not_found -> None in
         match pattern_still_needs_rebuild with
@@ -73,7 +77,7 @@ let rec goal_runner env loc name args
   )
 
 (* Return whether the target (pattern) needs to be rebuilt. *)
-and needs_rebuild env loc deps extra_deps pattern =
+and needs_rebuild ?(final_check = false) env loc deps extra_deps pattern =
   Cmdline.debug "%a: testing if %a needs rebuild"
     Ast.string_loc loc Ast.string_pattern pattern;
 
@@ -105,6 +109,11 @@ and needs_rebuild env loc deps extra_deps pattern =
      (* Add some standard variables to the environment. *)
      let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
      let env =
+       (*let b = Ast.EConstant (Ast.noloc, Ast.CBool final_check) in*)
+       let b = Ast.EConstant (Ast.noloc,
+                              Ast.CString (if final_check then "1" else "")) in
+       Ast.Env.add "goals_final_check" b env in
+     let env =
        (* NB: extra_deps are not added to %^ *)
        match deps with
        | [] -> env