X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Feval.ml;h=46455f7a21aa3eb699201937727b2d2719c0ab69;hb=c261da4d0efea4d86131abbbc2912edfa863995e;hp=c6cbda1380fd14439a7a8df201d02410fed7e186;hpb=e019d14d15d5caa90892f4c21d8424dbc95067ae;p=goals.git

diff --git a/src/eval.ml b/src/eval.ml
index c6cbda1..46455f7 100644
--- 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
+        let code = "set -e\nset -x\n\n" ^ code in
+        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,11 +118,12 @@ 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 =
+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 (Ast.substitute env loc) targs in
+     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
       *)
@@ -141,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