open Core

exception ImportError of string

type tree = { filename : string; deps : forest }
and forest = tree list

let provide (imports : (string * Extraction.coq_val) list) =
  let imports_set =
    Extraction.(
      VAttr
        (List.fold imports ~init:thunk_map_empty ~f:(fun attrs (filename, v) ->
             thunk_map_insert (Conv.chlist filename) (Forced v) attrs)))
  in
  let make_env =
    Extraction.(
      env_insert_abs (Conv.chlist "imports") (Forced imports_set) env_empty)
  in
  Extraction.(
    VClo
      ( Conv.chlist "path",
        make_env,
        EBinOp
          ( SelectAttrOp,
            EId (Conv.chlist "imports", None),
            EId (Conv.chlist "path", None) ) ))

let make_env (imports : (string * Extraction.coq_val) list) =
  Extraction.(
    env_insert_abs (Conv.chlist "import") (Forced (provide imports)) env_empty)

let rec import trees : (string * Extraction.coq_val) list =
  List.map trees ~f:(fun { filename; deps } ->
      let data = In_channel.read_all filename in
      Nix.parse ~filename data |> Nix.elaborate |> Nix2mininix.from_nix
      |> Builtins.apply_prelude
      |> Run.interp ~fuel:`Unlimited ~mode:`Shallow
           ~env:(make_env (import deps))
      |> function
      | Res (Some v) -> (filename, v)
      | Res None ->
          raise
            (ImportError
               (sprintf "Could not import %s: Failed to evaluate" filename))
      | NoFuel -> assert false)

let rec tree_map ~(f : string -> string) { filename; deps } =
  { filename = f filename; deps = forest_map ~f deps }

and forest_map ~(f : string -> string) trees = List.map ~f:(tree_map ~f) trees

(* [relative_to] must be an absolute path *)
let materialize forest ~relative_to : (string * Extraction.coq_val) list =
  forest_map forest ~f:(Filename.to_absolute_exn ~relative_to) |> import