Improvements to --dep graph

mk/generic.mk

@@ -109,6 +109,14 @@ $(DEPSTEM): $(DEPSTEM).touch
 depend: $(DEPSTEM)
 include $(DEPSTEM)
 
+depgraph: $(DEPSTEM).pdf
+$(DEPSTEM).pdf: $(DEPSTEM) .force
+	$(call msg, "DEPEND GRAPH", $(SRC))
+	$(FSTAR) --dep graph $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $(DEPSTEM).graph
+	$(FSTAR_ROOT)/.scripts/simpl_graph.py $(DEPSTEM).graph > $(DEPSTEM).simpl
+	dot -Tpdf -o $@ $(DEPSTEM).simpl
+	echo "Wrote $@"
+
 all-checked: $(ALL_CHECKED_FILES)
 
 all-ml: $(ALL_ML_FILES)

src/basic/FStarC.Compiler.Util.fsti

@@ -213,7 +213,7 @@ val get_file_extension: string -> string
 val is_path_absolute: string -> bool
 val join_paths: string -> string -> string
 val normalize_file_path: string -> string
-val basename: string -> string
+val basename: string -> string (* name of file without directory *)
 val dirname : string -> string
 val getcwd: unit -> string
 val readdir: string -> list string

src/basic/FStarC.StringBuffer.fsti

@@ -27,7 +27,7 @@ type t
 // sb |> add "hello" |> add " world" |> add "!"
 
 
-val create : FStarC.BigInt.t -> t
+val create : int -> t
 val add: string -> t -> t
 val contents: t -> string
 val clear: t -> t

src/parser/FStarC.Parser.Dep.fst

@@ -22,11 +22,10 @@
 *)
 module FStarC.Parser.Dep
 
-open FStar.Pervasives
+open FStarC
+open FStarC.Compiler
 open FStarC.Compiler.Effect   //for ref, failwith etc
 open FStarC.Compiler.List
-open FStar open FStarC
-open FStarC.Compiler
 open FStarC.Parser
 open FStarC.Parser.AST
 open FStarC.Compiler.Util
@@ -425,28 +424,30 @@ let dependences_of (file_system_map:files_for_module_name)
       List.map (file_of_dep file_system_map all_cmd_line_files) deps
       |> List.filter (fun k -> k <> fn) (* skip current module, cf #451 *)
 
-let print_graph (outc : out_channel) (fn : string) (graph:dependence_graph) =
+let print_graph (outc : out_channel) (fn : string) (graph:dependence_graph)
+  (file_system_map:files_for_module_name)
+  (cmd_lined_files:list file_name)
+ : unit
+ =
   if not (Options.silent ()) then begin
     Util.print1 "A DOT-format graph has been dumped in the current directory as `%s`\n" fn;
     Util.print1 "With GraphViz installed, try: fdp -Tpng -odep.png %s\n" fn;
     Util.print1 "Hint: cat %s | grep -v _ | grep -v prims\n" fn
   end;
-  let s =
-    "digraph {\n" ^
-    String.concat "\n" (List.collect
-      (fun k ->
-          let deps = (must (deps_try_find graph k)).edges in
-          let r s = replace_char s '.' '_' in
-          let print dep =
-            Util.format2 "  \"%s\" -> \"%s\""
-                (r (lowercase_module_name k))
-                (r (module_name_of_dep dep))
-          in
-          List.map print deps)
-     (List.unique (deps_keys graph))) ^
-    "\n}\n"
-  in
-  fprint outc "%s" [s]
+  let sb = FStarC.StringBuffer.create 10000 in
+  let pr str = ignore <| FStarC.StringBuffer.add str sb in
+  pr "digraph {\n";
+  List.unique (deps_keys graph) |> List.iter (fun k ->
+    let deps = (must (deps_try_find graph k)).edges in
+    List.iter (fun dep ->
+      let l = basename k in
+      let r = basename <| file_of_dep file_system_map cmd_lined_files dep in
+      if not <| Options.should_be_already_cached (module_name_of_dep dep) then
+        pr (Util.format2 "  \"%s\" -> \"%s\"\n" l r)
+    ) deps
+  );
+  pr "}\n";
+  fprint outc "%s" [FStarC.StringBuffer.contents sb]
 
 let safe_readdir_for_include (d:string) : list string =
   try readdir d
@@ -806,7 +807,7 @@ let collect_one
   if data_from_cache |> is_some then begin  //we found the parsing data in the checked file
     let deps, has_inline_for_extraction, mo_roots = from_parsing_data (data_from_cache |> must) original_map filename in
     if !dbg then
-      BU.print2 "Reading the parsing data for %s from its checked file .. found [%s]\n" filename (show deps);
+      BU.print2 "Reading the parsing data for %s from its checked file .. found %s\n" filename (show deps);
     data_from_cache |> must,
     deps, has_inline_for_extraction, mo_roots
   end
@@ -1530,12 +1531,12 @@ let collect (all_cmd_line_files: list file_name)
   profile (fun () -> List.iter discover_one all_cmd_line_files) "FStarC.Parser.Dep.discover";
 
   (* At this point, dep_graph has all the (immediate) dependency graph of all the files. *)
-  let cycle_detected dep_graph cycle filename =
+  let cycle_detected (dep_graph:dependence_graph) cycle filename =
       Util.print1 "The cycle contains a subset of the modules in:\n%s \n" (String.concat "\n`used by` " cycle);
 
       (* Write the graph to a file for the user to see. *)
       let fn = "dep.graph" in
-      with_file_outchannel fn (fun outc -> print_graph outc fn dep_graph);
+      with_file_outchannel fn (fun outc -> print_graph outc fn dep_graph file_system_map all_cmd_line_files);
 
       print_string "\n";
       raise_error0 Errors.Fatal_CyclicDependence [
@@ -1597,7 +1598,7 @@ let collect (all_cmd_line_files: list file_name)
             | _ -> [x]) in
         match node.color with
         | Gray ->
-           cycle_detected dep_graph cycle filename
+          cycle_detected dep_graph cycle filename
         | Black ->
             (* If the element has been visited already, then the map contains all its
              * dependencies. Otherwise, the map only contains its direct dependencies. *)
@@ -1762,7 +1763,7 @@ let print_full (outc : out_channel) (deps:deps) : unit =
         aux all_extracted_modules;
         List.rev !order
     in
-    let sb = FStarC.StringBuffer.create (FStarC.BigInt.of_int_fs 10000) in
+    let sb = FStarC.StringBuffer.create 10000 in
     let pr str = ignore <| FStarC.StringBuffer.add str sb in
     let print_entry target first_dep all_deps =
         pr target;
@@ -2060,7 +2061,7 @@ let do_print (outc : out_channel) (fn : string) deps : unit =
       pref ();
       profile (fun () -> print_full outc deps) "FStarC.Parser.Deps.print_full_deps"
   | Some "graph" ->
-      print_graph outc fn deps.dep_graph
+      print_graph outc fn deps.dep_graph deps.file_system_map deps.cmd_line_files
   | Some "raw" ->
       print_raw outc deps
   | Some _ ->