Actually run goal code.

[goals.git] / src / eval.ml

diff --git a/src/eval.ml b/src/eval.ml
index 260cbd9..9fc6e5c 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -17,6 +17,8 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
+open Printf
+
 open Utils
 
 let rec evaluate_targets env exprs =
@@ -71,21 +73,40 @@ and run_goal env loc name args (params, patterns, deps, code) =
   evaluate_targets env deps;
 
   (* Check if any target (ie. pattern) needs to be rebuilt. *)
-  let rebuild =
-    List.exists (needs_rebuild env loc name deps) patterns in
+  let rebuild = List.exists (needs_rebuild env loc deps) patterns in
 
   if rebuild then (
     (* Run the code (if any). *)
     (match code with
      | None -> ()
      | Some code ->
-        let code = Ast.substitute env loc code in
-        Printf.printf "running : %s\n" code
+        (* 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.ETactic (loc, tactic, List.map expr_of_substs targs)
+          | Ast.PVar (loc, name) ->
+             Ast.EVar (loc, name)
+        in
+        let pexprs = List.map expr_of_pattern patterns in
+        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 =
+          match deps with
+          | [] -> env
+          | d :: _ -> Ast.Env.add "^" d env in
+        let code = Ast.to_shell_script env loc code in
+        printf "%s\n%!" (trim code);
+        let r = Sys.command code in
+        if r <> 0 then (
+          eprintf "*** goal ‘%s’ failed with exit code %d\n" name r;
+          exit 1
+        )
     );
 
     (* Check all targets were updated (else it's an error). *)
     let pattern_still_needs_rebuild =
-      try Some (List.find (needs_rebuild env loc name deps) patterns)
+      try Some (List.find (needs_rebuild env loc deps) patterns)
       with Not_found -> None in
     match pattern_still_needs_rebuild with
     | None -> ()
@@ -97,8 +118,20 @@ and run_goal env loc name args (params, patterns, deps, code) =
   )
 
 (* Return whether the target (pattern) needs to be rebuilt. *)
-and needs_rebuild env loc name deps pattern =
-  false (* XXX *)
+and needs_rebuild env loc deps pattern =
+  match pattern with
+  | Ast.PTactic (loc, tactic, targs) ->
+     (* Resolve the targs down to constants. *)
+     let targs = List.map ((* XXX Ast.to_shell_script *)
+                            Ast.substitute env loc) targs in
+     (* XXX Look up the tactic.
+      * We would do that, but for now hard code the *file tactic. XXX
+      *)
+     assert (tactic = "file");
+     assert (List.length targs = 1);
+     let targ = List.hd targs in
+     not (Sys.file_exists targ)
+  | Ast.PVar _ -> assert false (* XXX not implemented *)
 
 (* Find the goal which matches the given tactic and run it.
  * cargs is a list of parameters (all constants).
@@ -130,23 +163,30 @@ and run_tactic env loc tactic cargs =
         | Some args -> Some (pattern, name, goal, args)
     ) patterns in
 
-  let _, name, goal, args =
-    match patterns with
-    | [p] -> p
-    | [] ->
+  match patterns with
+  | [_, name, goal, args] ->
+     run_goal env loc name args goal
+
+  | [] ->
+     (* There's no matching goal, but we don't need one if
+      * the tactic doesn't need to be rebuilt.
+      *)
+     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.ETactic (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 there are multiple matching goals, then assuming the goals
-        * are different we must pick the one which was defined last in
-        * the file.  However we don't do that right now. XXX
-        *)
-       assert false (* TODO! *) in
-
-  run_goal env loc name args goal
+     )
+
+  | _ ->
+     (* If there are multiple matching goals, then assuming the goals
+      * are different we must pick the one which was defined last in
+      * the file.  However we don't do that right now. XXX
+      *)
+     assert false (* TODO! *)
 
 (* Test if pattern matches *tactic(cargs).  If it does
  * then we return Some args where args is the arguments that must