val topsort_aux (g: dep_graph') (root: string) (acc: list string & list string)
    : ML (list string & list string)
let rec topsort_aux (g:dep_graph') (root:string) (acc:list string & list string)
  : ML (list string & list string) =  //grey nodes & finished nodes

  let finish (acc:list string & list string) : ML (list string & list string) =
    let grey, finished = acc in
    List.filter (fun s -> s <> root) grey, root::finished in

  let all_edges_from_root = all_edges_from g root in
  if List.length all_edges_from_root = 0
  then finish acc
  else
    all_edges_from_root
    |> List.fold_left (fun (grey, finished) (_src, dst) ->
        if List.mem dst grey
        then raise (Error (Printf.sprintf "Cycle in the dependency graph (%s)"
               (List.fold_left (fun s m -> Printf.sprintf "%s <== %s" s m) dst grey)))
        else if List.mem dst finished then (grey, finished)
        else topsort_aux g dst (dst::grey, finished)) acc
    |> finish
val topsort_aux (g: dep_graph') (root: string) (acc: list string & list string)
    : ML (list string & list string)
let rec topsort_aux (g: dep_graph') (root: string) (acc: list string & list string)
    : ML (list string & list string) =
let finish (acc: list string & list string) : ML (list string & list string) =
  let grey, finished = acc in
  List.filter (fun s -> s <> root) grey, root :: finished
in
let all_edges_from_root = all_edges_from g root in
if List.length all_edges_from_root = 0
then finish acc
else
  all_edges_from_root |>
  List.fold_left (fun (grey, finished) (_src, dst) ->
        if List.mem dst grey
        then
          raise (Error
              (Printf.sprintf "Cycle in the dependency graph (%s)"
                  (List.fold_left (fun s m -> Printf.sprintf "%s <== %s" s m) dst grey)))
        else
          if List.mem dst finished
          then (grey, finished)
          else topsort_aux g dst (dst :: grey, finished))
    acc |>
  finish
Deps.fst.checked
prims.fst.checked ParserDriver.fsti.checked OS.fsti.checked Options.fsti.checked JSON.fsti.checked Hashtable.fsti.checked FStar.String.fsti.checked FStar.ST.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked Config.fst.checked Ast.fst.checked
Deps.fst
Deps.dep_graph' Prims.string FStar.Pervasives.Native.tuple2 Prims.list Prims.op_Equality Prims.int FStar.List.Tot.Base.length Deps.edge Prims.bool FStar.All.op_Bar_Greater FStar.List.fold_left FStar.Pervasives.Native.Mktuple2 FStar.List.Tot.Base.mem FStar.Exn.raise Prims.exn Ast.Error FStar.Printf.sprintf Deps.topsort_aux Prims.Cons Deps.all_edges_from FStar.List.filter Prims.op_disEquality
module Deps
open FStar.List.Tot
open FStar.IO
open FStar.All
open Ast

module H = Hashtable

type edge = string & string

type dep_graph' = list edge

type dep_graph = {
  graph: dep_graph';
  modules_with_entrypoint: list string;
  modules_with_static_assertions: list string;
  modules_with_output_types: list string;
  modules_with_out_exprs: list string;
  modules_with_extern_types: list string;
  modules_with_extern_functions: list string
}

let all_edges_from (g:dep_graph') (node:string) : Tot (list edge) =
  List.Tot.filter (fun (src, _dst) -> src = node) g

let dependencies graph modul =
  List.Tot.map snd (all_edges_from graph.graph modul)

let dep_exists dirname name =
  OS.file_exists (Options.get_file_name (OS.concat dirname name))

(*
 * root is already greyed
 *)
val topsort_aux (g: dep_graph') (root: string) (acc: list string & list string)
    : ML (list string & list string)
g: Deps.dep_graph' -> root: Prims.string -> acc: (Prims.list Prims.string * Prims.list Prims.string)
  -> FStar.All.ML (Prims.list Prims.string * Prims.list Prims.string)