anchor.diff:    (* Util.print2 "Deps for %s: %s\n" filename (String.concat " " (!deps)); *)
     !deps, !mo_roots
   
  -type file_name = string
  -type module_name = string
  -type dependences = {
  -    interface_deps:list<module_name>;
  -    implementation_deps:list<module_name>
  -}
  -type dependence_graph = smap<(dependences * color)>
  -
  -let has_interface (file_system_map:files_for_module_name) key =
  -    match BU.smap_try_find file_system_map key with
  -    | Some (Some _, _) -> true
  -    | _ -> false
  -
  -let has_implementation (file_system_map:files_for_module_name) key =
  -    match BU.smap_try_find file_system_map key with
  -    | Some (_, Some _) -> true
  -    | _ -> false
  -
  -let completed_scan file_system_map graph key =
  -    if has_implementation file_system_map key
  -    then match BU.smap_try_find graph key with
  -         | Some ({implementation_deps = _::_}) -> true
  -         | _ -> false
  -    else if has_interface file_system_map key
  -    then match BU.smap_try_find graph key with
  -         | Some ({interface_deps = _::_}) -> true
  -         | _ -> false
  -    else failwith "Impossible: module does not exist"
  -
  -let dependences_of (file_system_map:files_for_module_name) (g:dependence_graph) (m:module_name) =
  -    match BU.smap_try_find g m with
  -    | None -> []
  -    | Some (deps, _) ->
  -      deps.interface_deps
  -      @List.filter (fun impl -> not (has_interface file_system_map impl)) deps.implementation_deps
  -
  -let print_graph (graph:dependence_graph) =
  -  Util.print_endline "A DOT-format graph has been dumped in the current directory as dep.graph";
  -  Util.print_endline "With GraphViz installed, try: fdp -Tpng -odep.png dep.graph";
  -  Util.print_endline "Hint: cat dep.graph | grep -v _ | grep -v prims";
  -  Util.write_file "dep.graph" (
  -    "digraph {\n" ^
  -    String.concat "\n" (List.collect
  -      (fun k ->
  -          let deps = fst (must (smap_try_find graph k)) in
  -          let r s = replace_char s '.' '_' in
  -          let print iface dep =
  -            Util.format3 " %s%s -> %s"
  -                (if iface then "interface_" else "")
  -                (r k)
  -                (r dep)
  -          in
  -          List.map (print true) deps.interface_deps
  -        @ List.map (print false) deps.implementation_deps)
  -     (List.unique (smap_keys graph))) ^
  -    "\n}\n"
  -  )
  -
   (** Collect the dependencies for a list of given files. *)
  -let collect (verify_mode: verify_mode) (filenames: list<string>) =
  +let collect (verify_mode: verify_mode) (filenames: list<file_name>)
  +    : list<file_name>
  +    * dependence_graph
  +    =
     (* The dependency graph; keys are lowercased module names, values = list of
      * lowercased module names this file depends on. *)
     let dep_graph : dependence_graph = smap_create 41 in
  +
   
     (* A bitmap that ensures every --verify_module X was matched by an existing X
      * in our dependency graph. *)
  
positive.code:       String.lowercase longname
    | None ->
        raise (Err (Util.format1 "not a valid FStar file: %s\n" f))
  
  (** Enumerate all F* files in include directories.
      Return a list of pairs of long names and full paths. *)
  
negative.code:  * list<string> //additional "roots" that should be scanned
                  //i.e. implementations of interfaces in the first list
  =
    let deps     : ref<(list<dependence>)> = BU.mk_ref [] in
    let mo_roots : ref<(list<dependence>)> = BU.mk_ref [] in
    let add_dep deps d =
      if not (List.existsML (fun d' -> d' = d) !deps) then
        deps := d :: !deps
    in
    let working_map = smap_copy original_map in
  
    let add_dependence_edge lid =
      let key = lowercase_join_longident lid true in
      match resolve_module_name working_map key with
      | Some module_name ->
        add_dep deps (PreferInterface module_name);
        if has_interface working_map module_name
        && has_implementation working_map module_name
        then add_dep mo_roots (UseImplementation module_name);
        true
      | _ ->
        false
    in
  
    let record_open_module let_open lid =
        if add_dependence_edge lid then true
        else let key = lowercase_join_longident lid true in
             let r = enter_namespace original_map working_map key in
             if not r //NS: this means that lid is a namespace?
             then if let_open then
                  raise (Errors.Error ("let-open only supported for modules, not namespaces", (range_of_lid lid)))
             else FStar.Errors.warn (range_of_lid lid)
                      (Util.format1 "No modules in namespace %s and no file with \
                                     that name either" (string_of_lid lid true));
             false
    in
  
    let record_open_namespace error_msg lid =
  