build: Distribute src/.depend with tarball.
[goals.git] / src / deps.ml
1 (* Goalfile dependency DAG
2  * Copyright (C) 2020 Richard W.M. Jones
3  * Copyright (C) 2020 Red Hat Inc.
4  *
5  * This program is free software; you can redistribute it and/or modify
6  * it under the terms of the GNU General Public License as published by
7  * the Free Software Foundation; either version 2 of the License, or
8  * (at your option) any later version.
9  *
10  * This program is distributed in the hope that it will be useful,
11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13  * GNU General Public License for more details.
14  *
15  * You should have received a copy of the GNU General Public License along
16  * with this program; if not, write to the Free Software Foundation, Inc.,
17  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
18  *)
19
20 open Printf
21
22 open Utils
23
24 type node =
25   | Goal of Ast.env * Ast.loc * string * Ast.expr list *
26               Ast.goal * Ast.expr list * string
27   | Exists of Ast.env * Ast.loc * Ast.pattern * string
28
29 let string_of_node = function
30   | Goal (_, _, _, _, _, _, debug_goal) -> debug_goal
31   | Exists (_, _, _, debug_tactic) -> debug_tactic
32
33 let compare_nodes n1 n2 =
34   match n1, n2 with
35   | Goal _, Exists _ -> -1
36   | Exists _, Goal _ -> 1
37   | Exists (_, _, p1, _), Exists (_, _, p2, _) -> compare p1 p2
38   | Goal (_, _, n1, a1, _, _, _), Goal (_, _, n2, a2, _, _, _) ->
39      compare (n1, a1) (n2, a2)
40
41 module G = Map.Make (
42   struct
43     type t = node
44     let compare = compare_nodes
45   end
46 )
47
48 type dag = {
49   (* List of nodes. *)
50   nodes : node list;
51
52   (* Edges are stored as an adjacency list, which is a map from
53    * a parent node to a list of child nodes.  Note that as the
54    * graph does not need to be connected, there may be nodes
55    * in the list above which don't appear in this map.
56    *)
57   edges : node list G.t;
58 }
59
60 type t = dag * node list
61 (* The final type is a DAG and a topologically sorted list of nodes. *)
62
63 (* Creates a new DAG. *)
64 let rec new_dag () = { nodes = []; edges = G.empty }
65
66 (* This will create a new node, unless the node already exists.
67  * If the optional parent parameter is given then it also creates
68  * an edge from parent to the new (or existing) node.
69  *)
70 and add_node { nodes; edges } ?parent data =
71   let node, nodes =
72     try List.find (fun n -> compare_nodes n data = 0) nodes, nodes
73     with Not_found -> data, data :: nodes in
74   let edges =
75     match parent with
76     | None -> edges
77     | Some parent ->
78        let children = try G.find parent edges with Not_found -> [] in
79        if List.mem node children then edges
80        else G.add parent (node :: children) edges in
81   node, { nodes; edges }
82
83 (* This is Khan's algorithm. *)
84 and topological_sort dag =
85   let incoming_map = incoming_map dag in
86
87   (* Set of all nodes with no incoming edge. *)
88   let q = List.filter (fun node -> not (G.mem node incoming_map)) dag.nodes in
89
90   let rec loop dag acc im = function
91     | [] -> dag, acc
92     | node :: q ->
93        let acc = node :: acc in
94        let children = try G.find node dag.edges with Not_found -> [] in
95        let dag, q, im =
96          List.fold_left (
97            fun (dag, q, im) child ->
98              (* There's an arrow from node to child. *)
99              let dag =
100                { nodes =
101                    List.filter (fun n -> compare_nodes n node <> 0) dag.nodes;
102                  edges = remove_edge dag.edges node child } in
103              let im = remove_edge im child node in
104              let q = if not (G.mem child im) then child :: q else q in
105              (dag, q, im)
106          ) (dag, q, im) children in
107        loop dag acc im q
108   in
109   let dag, acc = loop dag [] incoming_map q in
110
111   if not (G.is_empty dag.edges) then
112     (* XXX More debugging to help out users!  I believe the remaining
113      * edges should demonstrate the cycle.
114      *)
115     failwithf "dependency graph contains cycles";
116
117   (* This builds the topological list in reverse order, but that's
118    * fine because that is the running order.
119    *)
120   acc
121
122 (* The dag structure has an adjacency list, which is a list of outgoing
123  * edges from each node.  But for a topological sort what we actually
124  * need is another list of incoming edges, so construct that first.
125  *
126  * Note this never returns a mapping node -> [].
127  *)
128 and incoming_map { edges } =
129   let im = ref G.empty in
130   G.iter (
131     fun parent children ->
132       List.iter (
133         fun c ->
134           (* There is an arrow from parent -> c. *)
135           let xs = try G.find c !im with Not_found -> [] in
136           im := G.add c (parent :: xs) !im
137       ) children
138   ) edges;
139   !im
140
141 (* Remove edge from parent to child returning a new edges map.
142  * Preserves the invariant that there is never a mapping node -> [].
143  *)
144 and remove_edge edges parent child =
145   try
146     let children = G.find parent edges in
147     let children =
148       List.filter (fun n -> compare_nodes n child <> 0) children in
149     if children = [] then
150       G.remove parent edges
151     else
152       G.add parent children edges
153   with
154     Not_found -> edges
155
156 and debug_dag { nodes; edges } =
157   eprintf "nodes:\n";
158   List.iter (fun node -> eprintf "  %s\n" (string_of_node node)) nodes;
159   eprintf "edges:\n";
160   G.iter (
161     fun parent children ->
162       eprintf "  %s ->" (string_of_node parent);
163       List.iter (fun c -> eprintf " %s" (string_of_node c)) children;
164       eprintf "\n"
165   ) edges
166
167 let rec create env roots =
168   let dag = new_dag () in
169   let dag = add_targets dag env roots in
170   if Cmdline.debug_flag () then debug_dag dag;
171   (* Make actually breaks cycles, but I'm not convinced that this
172    * is a good idea, so this function will fail if any cycle is
173    * found.  We may wish to revisit this decision in future.
174    *)
175   let sorted = topological_sort dag in
176   if Cmdline.debug_flag () then
177     eprintf "dependency order:\n  %s\n"
178       (String.concat " <- " (List.map string_of_node sorted));
179   dag, sorted
180
181 and add_targets dag ?parent env roots =
182   List.fold_left (fun dag root -> add_target dag ?parent env root) dag roots
183
184 and add_target dag ?parent env = function
185   | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.ETacticDefn _ -> assert false
186
187   (* Call a goal or function. *)
188   | Ast.ECall (loc, name, args) ->
189      let expr = Ast.getvar env loc name in
190      (match expr with
191       | Ast.EGoalDefn (_, goal) ->
192          add_goal dag ?parent env loc name args goal []
193       | Ast.EFuncDefn (_, func) ->
194          let expr = Eval.call_function env loc name args func in
195          add_target dag ?parent env expr
196       | _ ->
197          failwithf "%a: tried to call ā€˜%sā€™ which is not a goal or a function"
198            Ast.string_loc loc name
199      )
200
201   (* Call a tactic. *)
202   | Ast.ETacticCtor (loc, name, args) ->
203      (* All parameters of tactics must be simple constant expressions
204       * (strings, in future booleans, numbers, etc).
205       *)
206      let args = List.map (Eval.to_constant env) args in
207      add_tactic dag ?parent env loc name args
208
209   (* If this is a goal then it's the same as calling goal().  If not
210    * then look up the variable and substitute it.
211    *)
212   | Ast.EVar (loc, name) ->
213      let expr = Ast.getvar env loc name in
214      (match expr with
215       | Ast.EGoalDefn (loc, ([], _, _, _)) ->
216          add_target dag ?parent env (Ast.ECall (loc, name, []))
217       | EGoalDefn _ ->
218          failwithf "%a: cannot call %s() since this goal has parameters"
219            Ast.string_loc loc name
220       | _ ->
221          add_target dag ?parent env expr
222      )
223
224   (* Lists are inlined when found as a target. *)
225   | Ast.EList (loc, exprs) ->
226      add_targets dag ?parent env exprs
227
228   (* A string (with or without substitutions) implies *file(filename). *)
229   | Ast.ESubsts (loc, str) ->
230      let str = Eval.substitute env loc str in
231      add_tactic dag ?parent env loc "*file" [Ast.CString str]
232
233   | Ast.EConstant (loc, c) ->
234      add_tactic dag ?parent env loc "*file" [c]
235
236 (* Add a goal by name. *)
237 and add_goal dag ?parent env loc name args
238              ((params, patterns, deps, code) as goal)
239              extra_deps =
240   (* This is used to print the goal in debug and error messages only. *)
241   let debug_goal =
242     sprintf "%s (%s)" name
243       (String.concat ", " (List.map (Ast.string_expr ()) args)) in
244   Cmdline.debug "%a: adding goal %s" Ast.string_loc loc debug_goal;
245
246   (* This is the point where we evaluate the goal arguments.  We must
247    * do this before creating the new environment, because variables
248    * appearing in goal arguments don't refer to goal parameters.
249    *)
250   let args = List.map (Eval.evaluate_goal_arg env) args in
251
252   (* Create a new environment which maps the parameter names to
253    * the args.
254    *)
255   let env =
256     let params =
257       try List.combine params args
258       with Invalid_argument _ ->
259         failwithf "%a: calling goal %s with wrong number of arguments, expecting %d args but got %d args"
260           Ast.string_loc loc debug_goal
261           (List.length params) (List.length args) in
262     List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
263
264   (* Create the node. *)
265   let node, dag =
266     add_node dag ?parent (Goal (env, loc, name, args, goal,
267                                 extra_deps, debug_goal)) in
268
269   (* Add all dependencies. *)
270   add_targets dag ~parent:node env (deps @ extra_deps)
271
272 (* Find the goal which matches the given tactic and add it.
273  * cargs is a list of parameters (all constants).
274  *)
275 and add_tactic dag ?parent env loc tactic cargs =
276   (* This is used to print the tactic in debug and error messages only. *)
277   let debug_tactic =
278     Ast.string_expr ()
279       (Ast.ETacticCtor (loc, tactic,
280                         List.map (fun c -> Ast.EConstant (loc, c)) cargs)) in
281   Cmdline.debug "%a: adding tactic %s" Ast.string_loc loc debug_tactic;
282
283   (* Find all goals in the environment.  Returns a list of (name, goal). *)
284   let goals =
285     let env = Ast.Env.bindings env in
286     filter_map
287       (function
288        | name, Ast.EGoalDefn (loc, goal) -> Some (name, goal)
289        | _ -> None) env in
290
291   (* Find all patterns.  Returns a list of (pattern, name, goal). *)
292   let patterns : (Ast.pattern * Ast.id * Ast.goal) list =
293     List.flatten
294       (List.map (fun (name, ((_, patterns, _, _) as goal)) ->
295            List.map (fun pattern -> (pattern, name, goal)) patterns) goals) in
296
297   (* Find any patterns (ie. tactics) which match the one we
298    * are searching for.  This returns a binding for the goal args,
299    * so we end up with a list of (pattern, name, goal, args).
300    *)
301   let patterns : (Ast.pattern * Ast.id * Ast.goal * Ast.expr list) list =
302     filter_map (
303       fun (pattern, name, ((params, _, _, _) as goal)) ->
304         match matching_pattern env loc tactic cargs pattern params with
305         | None -> None
306         | Some args -> Some (pattern, name, goal, args)
307     ) patterns in
308
309   match patterns with
310   | [] ->
311      (* There's no matching goal, but we don't need one if
312       * the tactic doesn't need to be rebuilt.  So create a
313       * special Exists node which will be used to run the tactic
314       * to see if the target needs to be rebuilt, and only fail
315       * if it does need a rebuild.
316       *)
317      let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
318      let p = Ast.PTactic (loc, tactic, targs) in
319      let _, dag = add_node dag ?parent (Exists (env, loc, p, debug_tactic)) in
320      dag
321
322   | [_, name, goal, args] ->
323      (* Single goal matches. *)
324      add_goal dag ?parent env loc name args goal []
325
326   | goals ->
327      (* Two or more goals match.  Only one must have a CODE section,
328       * and we combine the dependencies into a "supergoal".
329       *)
330      let with_code, without_code =
331        List.partition (
332          fun (_, _, (_, _, _, code), _) -> code <> None
333        ) goals in
334
335      let (_, name, goal, args), extra_deps =
336        match with_code with
337        | [g] ->
338           let extra_deps =
339             List.flatten (
340               List.map (fun (_, _, (_, _, deps, _), _) -> deps) without_code
341             ) in
342           (g, extra_deps)
343
344        | [] ->
345           (* This is OK, it means we'll rebuild all dependencies
346            * but there is no code to run.  Pick the first goal
347            * without code and the dependencies from the other goals.
348            *)
349           let g = List.hd without_code in
350           let extra_deps =
351             List.flatten (
352               List.map (fun (_, _, (_, _, deps, _), _) -> deps)
353                 (List.tl without_code)
354             ) in
355           (g, extra_deps)
356
357        | _ :: _ ->
358           failwithf "%a: multiple goals found which match tactic %s, but more than one of these goals have {code} sections which is not allowed"
359             Ast.string_loc loc debug_tactic in
360
361      add_goal dag ?parent env loc name args goal extra_deps
362
363 (* Test if pattern matches *tactic(cargs).  If it does
364  * then we return Some args where args is the arguments that must
365  * be passed to the matching goal.  The params parameter is
366  * the names of the parameters of that goal.
367  *)
368 and matching_pattern env loc tactic cargs pattern params =
369   match pattern with
370   | Ast.PTactic (loc, ttactic, targs)
371        when tactic <> ttactic ||
372             List.length cargs <> List.length targs ->
373      None (* Can't possibly match if tactic name or #args is different. *)
374   | Ast.PTactic (loc, ttactic, targs) ->
375      (* Do the args match with a possible params binding? *)
376      try Some (matching_params env loc params targs cargs)
377      with Not_found -> None
378
379 (* Return a possible binding.  For example the goal is:
380  *   goal compile (name) = "%name.o": "%name.c" {}
381  * which means that params = ["name"] and targs = ["%name.o"].
382  *
383  * If we are called with cargs = ["file1.o"], we would
384  * return ["file1"].
385  *
386  * On non-matching this raises Not_found.
387  *)
388 and matching_params env loc params targs cargs =
389   (* This is going to record the resulting binding. *)
390   let res = ref Ast.Env.empty in
391   List.iter2 (matching_param env loc params res) targs cargs;
392
393   (* Rearrange the result into goal parameter order.  Also this
394    * checks that every parameter got a binding.
395    *)
396   let res = !res in
397   List.map (
398     (* Allow the Not_found exception to escape if no binding for this param. *)
399     fun param -> Ast.Env.find param res
400   ) params
401
402 (* If targ = "%name.o" and carg = "file.o" then this would set
403  * name => "file" in !res.  If they don't match, raises Not_found.
404  *)
405 and matching_param env loc params res targ carg =
406   match carg with
407   | Ast.CString carg ->
408      (* Substitute any non parameters in targ from the environment. *)
409      let targ =
410        List.map (
411          function
412          | Ast.SString _ as s -> s
413          | Ast.SVar name ->
414             if not (List.mem name params) then (
415               try
416                 let expr = Ast.getvar env loc name in
417                 match Eval.to_constant env expr with
418                 | Ast.CString s -> Ast.SString s
419               with Failure _ -> raise Not_found
420             )
421             else
422               Ast.SVar name
423        ) targ in
424
425      (* Do the actual pattern matching.  Any remaining SVar elements
426       * must refer to goal parameters.
427       *)
428      let carg = ref carg in
429      let rec loop = function
430        | [] ->
431           (* End of targ, we must have matched all of carg. *)
432           if !carg <> "" then raise Not_found
433        | Ast.SString s :: rest ->
434           (* Does this match the first part of !carg? *)
435           let clen = String.length !carg in
436           let slen = String.length s in
437           if slen > clen || s <> String.sub !carg 0 slen then
438             raise Not_found;
439           (* Yes, so continue after the matching prefix. *)
440           carg := String.sub !carg slen (clen-slen);
441           loop rest
442        | Ast.SVar name :: Ast.SString s :: rest ->
443           (* This is a goal parameter.  Find s later in !carg. *)
444           let i = string_find !carg s in
445           if i = -1 then raise Not_found;
446           (* Set the binding in !res. *)
447           let r = Ast.EConstant (Ast.noloc,
448                                  Ast.CString (String.sub !carg 0 i)) in
449           res := Ast.Env.add name r !res;
450           (* Continue after the match. *)
451           let skip = i + String.length s in
452           carg := String.sub !carg skip (String.length !carg - skip);
453           loop rest
454        | Ast.SVar name :: [] ->
455           (* Matches the whole remainder of the string. *)
456           let r = Ast.EConstant (Ast.noloc, Ast.CString !carg) in
457           res := Ast.Env.add name r !res
458        | Ast.SVar x :: Ast.SVar y :: _ ->
459           (* TODO! We cannot match a target like "%x%y". *)
460           assert false
461      in
462      loop targ
463
464 type goal_runner =
465   Ast.env -> Ast.loc -> string -> Ast.expr list -> Ast.goal ->
466   Ast.expr list -> string -> unit
467
468 type exists_runner = Ast.env -> Ast.loc -> Ast.pattern -> string -> unit
469
470 type state = {
471   dag : dag;
472   goal_runner : goal_runner;
473   exists_runner : exists_runner;
474
475   (* Topologically sorted in build order.  When nodes start running
476    * we take them off this list.
477    *)
478   mutable sorted_nodes : node list;
479
480   (* List of nodes which completed successfully.  Actually for fast
481    * access we store a map node -> true.
482    *)
483   mutable complete : bool G.t;
484 }
485
486 let new_state (dag, sorted_nodes) goal_runner exists_runner =
487   { dag; goal_runner; exists_runner; sorted_nodes; complete = G.empty }
488
489 (* Called by [Jobs] when a node completes successfully.  We mark
490  * it as done.
491  *)
492 let retire_job state node =
493   state.complete <- G.add node true state.complete
494
495 let rec next_job state =
496   (* Find the earliest node in the list which has all its
497    * dependencies done.
498    *)
499   let rec loop acc = function
500     | [] ->
501        if state.sorted_nodes = [] then Jobs.Complete else Jobs.Not_ready
502     | node :: nodes ->
503        if node_is_ready_to_run state node then (
504          state.sorted_nodes <- List.rev acc @ nodes;
505          match node with
506          | Goal (env, loc, name, args, goal, extra_deps, debug_goal) ->
507             Jobs.Job (node, fun () ->
508                             state.goal_runner env loc name args goal
509                               extra_deps debug_goal)
510          | Exists (env, loc, p, debug_tactic) ->
511             Jobs.Job (node, fun () ->
512                             state.exists_runner env loc p debug_tactic)
513        )
514        else
515          loop (node :: acc) nodes
516   in
517   loop [] state.sorted_nodes
518
519 and node_is_ready_to_run { dag; complete } node =
520   let parents = try G.find node dag.edges with Not_found -> [] in
521   List.for_all (fun p -> G.mem p complete) parents
522
523 let string_of_job  = string_of_node