Implement -include (optional include) command.

[goals.git] / src / eval.ml

diff --git a/src/eval.ml b/src/eval.ml
index af57213..1688b5f 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -25,24 +25,35 @@ let rec evaluate_targets env exprs =
   List.iter (evaluate_target env) exprs
 
 and evaluate_target env = function
-  | Ast.EGoal _ -> assert false
+  | Ast.EGoal _ | Ast.ETactic _ -> assert false
 
   (* Call a goal. *)
-  | Ast.ECall (loc, name, args) ->
+  | Ast.ECallGoal (loc, name, args) ->
      let goal = Ast.getgoal env loc name in
      run_goal env loc name args goal
 
-  | Ast.ETactic (loc, name, args) ->
+  (* Call a tactic. *)
+  | Ast.ECallTactic (loc, name, args) ->
      (* All parameters of tactics must be simple constant expressions
       * (strings, in future booleans, numbers, etc).
       *)
      let args = List.map (Ast.to_constant env) args in
      run_tactic env loc name args
 
-  (* Look up the variable and substitute it. *)
+  (* If this is a goal then it's the same as calling goal().  If not
+   * then look up the variable and substitute it.
+   *)
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
-     evaluate_target env expr
+     (match expr with
+      | EGoal (loc, ([], _, _, _)) ->
+         evaluate_target env (Ast.ECallGoal (loc, name, []))
+      | EGoal _ ->
+         failwithf "%a: cannot call %s() since this goal has parameters"
+           Ast.string_loc loc name
+      | _ ->
+         evaluate_target env expr
+     )
 
   (* Lists are inlined when found as a target. *)
   | Ast.EList (loc, exprs) ->
@@ -51,13 +62,16 @@ and evaluate_target env = function
   (* A string (with or without substitutions) implies *file(filename). *)
   | Ast.ESubsts (loc, str) ->
      let str = Ast.substitute env loc str in
-     run_tactic env loc "file" [Ast.CString str]
+     run_tactic env loc "*file" [Ast.CString str]
 
   | Ast.EConstant (loc, c) ->
-     run_tactic env loc "file" [c]
+     run_tactic env loc "*file" [c]
 
 (* Run a goal by name. *)
 and run_goal env loc name args (params, patterns, deps, code) =
+  Cmdline.debug "%a: running goal %s %a"
+    Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args));
+
   (* Create a new environment which maps the parameter names to
    * the args.
    *)
@@ -84,7 +98,7 @@ and run_goal env loc name args (params, patterns, deps, code) =
         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.ECallTactic (loc, tactic, 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
@@ -117,23 +131,56 @@ 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 deps pattern =
+  Cmdline.debug "%a: testing if %a needs rebuild"
+    Ast.string_loc loc Ast.string_pattern 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
+     (* Look up the tactic. *)
+     let params, code = Ast.gettactic env loc tactic 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.
       *)
-     assert (tactic = "file");
-     assert (List.length targs = 1);
-     let targ = List.hd targs in
-     not (Sys.file_exists targ)
+     let targs = List.map (Ast.substitute env loc) targs in
+     let targs =
+       List.map (fun targ ->
+           Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
+
+     (* Create a new environment binding parameter names
+      * to tactic 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
+       List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
+
+     (* Add some standard variables to the environment. *)
+     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 = 99 (* means "needs rebuild" *) then true
+     else if r = 0 (* means "doesn't need rebuild" *) then false
+     else (
+       eprintf "*** tactic ‘%s’ failed with exit code %d\n" tactic r;
+       exit 1
+     )
 
 (* Find the goal which matches the given tactic and run it.
  * cargs is a list of parameters (all constants).
  *)
 and run_tactic env loc tactic cargs =
+  Cmdline.debug "%a: running tactic %s" Ast.string_loc loc tactic;
+
   (* Find all goals in the environment.  Returns a list of (name, goal). *)
   let goals =
     let env = Ast.Env.bindings env in
@@ -171,9 +218,9 @@ and run_tactic env loc tactic cargs =
      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
+       let t = Ast.ECallTactic (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
      )