From: Richard W.M. Jones Date: Fri, 10 Jan 2020 08:42:41 +0000 (+0000) Subject: run: Add %goals_final_check variable when evaluating tactics. X-Git-Tag: v'0.2'~51 X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=109185686ffdc00520eba2b4c3a92f10a111fb60;p=goals.git run: Add %goals_final_check variable when evaluating tactics. This is true ("1") if this is the final check that the goal evaluation was successful. It allows tactics to behave differently when evaluating if we need a rebuild vs checking that the rebuild was successful. --- diff --git a/src/run.ml b/src/run.ml index 2d4e326..55a2b8d 100644 --- 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