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
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) ->
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.
| 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
(* 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 =
(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
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] ->
(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
* 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.
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.
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
git.annexia.org / goals.git / blobdiff