anchor.diff:        String.lowercase longname
     | None ->
         raise (Err (Util.format1 "not a valid FStar file: %s\n" f))
  +
  +type file_name = string
  +type module_name = string
  +type dependence =
  +    | PreferInterface of module_name
  +    | UseImplementation of module_name
  +type dependences = list<dependence>
  +let empty_dependences = []
  +type dependence_graph = //maps file names to the modules it depends on
  +     smap<(dependences * color)>
  +
  +let module_name_of_dep = function
  +    | PreferInterface m
  +    | UseImplementation m -> m
  +
  +let resolve_module_name (file_system_map:files_for_module_name) (key:module_name)
  +    : option<module_name>
  +    = match BU.smap_try_find file_system_map key with
  +      | Some (Some fn, _)
  +      | Some (_, Some fn) -> Some (lowercase_module_name fn)
  +      | _ -> None
  +
  +
  +let interface_of (file_system_map:files_for_module_name) (key:module_name)
  +    : option<file_name> =
  +    match BU.smap_try_find file_system_map key with
  +    | Some (Some iface, _) -> Some iface
  +    | _ -> None
  +
  +let implementation_of (file_system_map:files_for_module_name) (key:module_name)
  +    : option<file_name> =
  +    match BU.smap_try_find file_system_map key with
  +    | Some (_, Some impl) -> Some impl
  +    | _ -> None
  +
  +let has_interface (file_system_map:files_for_module_name) (key:module_name)
  +    : bool =
  +    Option.isSome (interface_of file_system_map key)
  +
  +let has_implementation (file_system_map:files_for_module_name) (key:module_name)
  +    : bool =
  +    Option.isSome (interface_of file_system_map key)
  +
  +//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) (deps:dependence_graph) (fn:file_name) : list<file_name> =
  +    match BU.smap_try_find deps fn with
  +    | None -> empty_dependences
  +    | Some (deps, _) ->
  +      let file_of_dep = function
  +        | PreferInterface key when has_interface file_system_map key ->
  +          Option.get <| interface_of file_system_map key
  +        | PreferInterface key
  +        | UseImplementation key ->
  +          Option.get <| implementation_of file_system_map key
  +     in
  +     List.map file_of_dep deps
  +
  +let add_dependence (deps:dependence_graph)
  +                   (from:file_name) (to_:file_name)
  +                  : unit =
  +    let key = lowercase_module_name from in
  +    let add_dep (d,color) to_ =
  +        if is_interface to_
  +        then (PreferInterface (lowercase_module_name to_)::d), color
  +        else (UseImplementation (lowercase_module_name to_)::d), color
  +    in
  +    match BU.smap_try_find deps key with
  +    | None ->
  +      BU.smap_add deps key (add_dep (empty_dependences, White) to_)
  +    | Some key_deps ->
  +      BU.smap_add deps key (add_dep key_deps to_)
  +
  +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 dep =
  +            Util.format2 " %s -> %s"
  +                (r k)
  +                (r (module_name_of_dep dep))
  +          in
  +          List.map print deps)
  +     (List.unique (smap_keys graph))) ^
  +    "\n}\n"
  +  )
   
   (** Enumerate all F* files in include directories.
       Return a list of pairs of long names and full paths. *)
  
positive.code:     | Open lid ->
          record_open false lid
      | ModuleAbbrev (ident, lid) ->
          add_dep (lowercase_join_longident lid true);
          record_module_alias ident lid
      | TopLevelLet (_, patterms) ->
          List.iter (fun (pat, t) -> collect_pattern pat; collect_term t) patterms
  
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 =
  