X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Fdeps.ml;h=0795cf813dd3e6062d7f347cc0e6b12f18100950;hb=156de1e0df4aace1a42957491118cc2174d70c6a;hp=6656e879339862b0f70a4ceeb9d42bac7b737a46;hpb=a70987f316ab4b948bf941ddea8fb6ccef09da4f;p=goals.git

diff --git a/src/deps.ml b/src/deps.ml
index 6656e87..0795cf8 100644
--- a/src/deps.ml
+++ b/src/deps.ml
@@ -28,7 +28,7 @@ type node =
 
 let string_of_node = function
   | Goal (_, _, _, _, _, _, debug_goal) -> debug_goal
-  | Exists (_, _, _, debug_tactic) -> debug_tactic
+  | Exists (_, _, _, debug_pred) -> debug_pred
 
 let compare_nodes n1 n2 =
   match n1, n2 with
@@ -182,7 +182,7 @@ and add_targets dag ?parent env roots =
   List.fold_left (fun dag root -> add_target dag ?parent env root) dag roots
 
 and add_target dag ?parent env = function
-  | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.ETacticDefn _ -> assert false
+  | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.EPredDefn _ -> assert false
 
   (* Call a goal or function. *)
   | Ast.ECall (loc, name, args) ->
@@ -198,13 +198,13 @@ and add_target dag ?parent env = function
            Ast.string_loc loc name
      )
 
-  (* Call a tactic. *)
-  | Ast.ETacticCtor (loc, name, args) ->
-     (* All parameters of tactics must be simple constant expressions
+  (* Call a predicate. *)
+  | Ast.EPredCtor (loc, name, args) ->
+     (* All parameters of predicates must be simple constant expressions
       * (strings, in future booleans, numbers, etc).
       *)
      let args = List.map (Eval.to_constant env) args in
-     add_tactic dag ?parent env loc name args
+     add_pred dag ?parent env loc name args
 
   (* If this is a goal then it's the same as calling goal().  If not
    * then look up the variable and substitute it.
@@ -225,13 +225,13 @@ and add_target dag ?parent env = function
   | Ast.EList (loc, exprs) ->
      add_targets dag ?parent env exprs
 
-  (* A string (with or without substitutions) implies *file(filename). *)
+  (* A string (with or without substitutions) implies is-file(filename). *)
   | Ast.ESubsts (loc, str) ->
      let str = Eval.substitute env loc str in
-     add_tactic dag ?parent env loc "*file" [Ast.CString str]
+     add_pred dag ?parent env loc "is-file" [Ast.CString str]
 
   | Ast.EConstant (loc, c) ->
-     add_tactic dag ?parent env loc "*file" [c]
+     add_pred dag ?parent env loc "is-file" [c]
 
 (* Add a goal by name. *)
 and add_goal dag ?parent env loc name args
@@ -269,16 +269,16 @@ and add_goal dag ?parent env loc name args
   (* Add all dependencies. *)
   add_targets dag ~parent:node env (deps @ extra_deps)
 
-(* Find the goal which matches the given tactic and add it.
+(* Find the goal which matches the given predicate and add it.
  * cargs is a list of parameters (all constants).
  *)
-and add_tactic dag ?parent env loc tactic cargs =
-  (* This is used to print the tactic in debug and error messages only. *)
-  let debug_tactic =
+and add_pred dag ?parent env loc pred cargs =
+  (* This is used to print the predicate in debug and error messages only. *)
+  let debug_pred =
     Ast.string_expr ()
-      (Ast.ETacticCtor (loc, tactic,
+      (Ast.EPredCtor (loc, pred,
                         List.map (fun c -> Ast.EConstant (loc, c)) cargs)) in
-  Cmdline.debug "%a: adding tactic %s" Ast.string_loc loc debug_tactic;
+  Cmdline.debug "%a: adding predicate %s" Ast.string_loc loc debug_pred;
 
   (* Find all goals in the environment.  Returns a list of (name, goal). *)
   let goals =
@@ -294,14 +294,14 @@ and add_tactic dag ?parent env loc tactic cargs =
       (List.map (fun (name, ((_, patterns, _, _) as goal)) ->
            List.map (fun pattern -> (pattern, name, goal)) patterns) goals) in
 
-  (* Find any patterns (ie. tactics) which match the one we
+  (* Find any patterns (ie. predicates) which match the one we
    * are searching for.  This returns a binding for the goal args,
    * so we end up with a list of (pattern, name, goal, args).
    *)
   let patterns : (Ast.pattern * Ast.id * Ast.goal * Ast.expr list) list =
     filter_map (
       fun (pattern, name, ((params, _, _, _) as goal)) ->
-        match matching_pattern env loc tactic cargs pattern params with
+        match matching_pattern env loc pred cargs pattern params with
         | None -> None
         | Some args -> Some (pattern, name, goal, args)
     ) patterns in
@@ -309,14 +309,14 @@ and add_tactic dag ?parent env loc tactic cargs =
   match patterns with
   | [] ->
      (* There's no matching goal, but we don't need one if
-      * the tactic doesn't need to be rebuilt.  So create a
-      * special Exists node which will be used to run the tactic
+      * the predicate doesn't need to be rebuilt.  So create a
+      * special Exists node which will be used to run the predicate
       * to see if the target needs to be rebuilt, and only fail
       * if it does need a rebuild.
       *)
      let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
-     let p = Ast.PTactic (loc, tactic, targs) in
-     let _, dag = add_node dag ?parent (Exists (env, loc, p, debug_tactic)) in
+     let p = Ast.PPred (loc, pred, targs) in
+     let _, dag = add_node dag ?parent (Exists (env, loc, p, debug_pred)) in
      dag
 
   | [_, name, goal, args] ->
@@ -355,23 +355,23 @@ and add_tactic dag ?parent env loc tactic cargs =
           (g, extra_deps)
 
        | _ :: _ ->
-          failwithf "%a: multiple goals found which match tactic %s, but more than one of these goals have {code} sections which is not allowed"
-            Ast.string_loc loc debug_tactic in
+          failwithf "%a: multiple goals found which match predicate %s, but more than one of these goals have {code} sections which is not allowed"
+            Ast.string_loc loc debug_pred in
 
      add_goal dag ?parent env loc name args goal extra_deps
 
-(* Test if pattern matches *tactic(cargs).  If it does
+(* Test if pattern matches is-predicate(cargs).  If it does
  * then we return Some args where args is the arguments that must
  * be passed to the matching goal.  The params parameter is
  * the names of the parameters of that goal.
  *)
-and matching_pattern env loc tactic cargs pattern params =
+and matching_pattern env loc pred cargs pattern params =
   match pattern with
-  | Ast.PTactic (loc, ttactic, targs)
-       when tactic <> ttactic ||
+  | Ast.PPred (loc, tpred, targs)
+       when pred <> tpred ||
             List.length cargs <> List.length targs ->
-     None (* Can't possibly match if tactic name or #args is different. *)
-  | Ast.PTactic (loc, ttactic, targs) ->
+     None (* Can't possibly match if predicate name or #args is different. *)
+  | Ast.PPred (loc, tpred, targs) ->
      (* Do the args match with a possible params binding? *)
      try Some (matching_params env loc params targs cargs)
      with Not_found -> None
@@ -481,10 +481,14 @@ type state = {
    * access we store a map node -> true.
    *)
   mutable complete : bool G.t;
+
+  (* List of nodes which failed. *)
+  mutable failed : bool G.t;
 }
 
 let new_state (dag, sorted_nodes) goal_runner exists_runner =
-  { dag; goal_runner; exists_runner; sorted_nodes; complete = G.empty }
+  { dag; goal_runner; exists_runner; sorted_nodes;
+    complete = G.empty; failed = G.empty }
 
 (* Called by [Jobs] when a node completes successfully.  We mark
  * it as done.
@@ -492,6 +496,13 @@ let new_state (dag, sorted_nodes) goal_runner exists_runner =
 let retire_job state node =
   state.complete <- G.add node true state.complete
 
+(* Called by [Jobs] when a node fails.  We mark the node as
+ * failed and ensure that anything that depends on it will
+ * also be marked as failed (and never returned by next_job).
+ *)
+let fail_job state node =
+  state.failed <- G.add node true state.failed
+
 let rec next_job state =
   (* Find the earliest node in the list which has all its
    * dependencies done.
@@ -499,25 +510,41 @@ let rec next_job state =
   let rec loop acc = function
     | [] ->
        if state.sorted_nodes = [] then Jobs.Complete else Jobs.Not_ready
-    | node :: nodes ->
-       if node_is_ready_to_run state node then (
-         state.sorted_nodes <- List.rev acc @ nodes;
-         match node with
-         | Goal (env, loc, name, args, goal, extra_deps, debug_goal) ->
-            Jobs.Job (node, fun () ->
-                            state.goal_runner env loc name args goal
-                              extra_deps debug_goal)
-         | Exists (env, loc, p, debug_tactic) ->
-            Jobs.Job (node, fun () ->
-                            state.exists_runner env loc p debug_tactic)
+    | node :: nodes when node_is_ready_to_run state node ->
+       (* Drop the node from the list of jobs and run it. *)
+       state.sorted_nodes <- List.rev acc @ nodes;
+       (match node with
+        | Goal (env, loc, name, args, goal, extra_deps, debug_goal) ->
+           Jobs.Job (node, fun () ->
+                           state.goal_runner env loc name args goal
+                             extra_deps debug_goal)
+        | Exists (env, loc, p, debug_pred) ->
+           Jobs.Job (node, fun () ->
+                           state.exists_runner env loc p debug_pred)
        )
-       else
-         loop (node :: acc) nodes
+    | node :: nodes when node_failed state node ->
+       (* Mark it as failed also, and drop it from the list of jobs. *)
+       fail_job state node;
+       state.sorted_nodes <- List.rev acc @ nodes;
+       loop acc nodes
+    | node :: nodes ->
+       (* All dependencies of this node are neither complete nor failed,
+        * continue down the list.
+        *)
+       loop (node :: acc) nodes
   in
   loop [] state.sorted_nodes
 
+(* All dependencies of this node are complete. *)
 and node_is_ready_to_run { dag; complete } node =
   let parents = try G.find node dag.edges with Not_found -> [] in
   List.for_all (fun p -> G.mem p complete) parents
 
+(* This node or any dependency of this node failed. *)
+and node_failed { dag; failed } node =
+  G.mem node failed || (
+    let parents = try G.find node dag.edges with Not_found -> [] in
+    List.exists (fun p -> G.mem p failed) parents
+  )
+
 let string_of_job  = string_of_node