From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 lib/mininix/import.ml | 54 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100644 lib/mininix/import.ml

(limited to 'lib/mininix/import.ml')

diff --git a/lib/mininix/import.ml b/lib/mininix/import.ml
new file mode 100644
index 0000000..ca1bfb5
--- /dev/null
+++ b/lib/mininix/import.ml
@@ -0,0 +1,54 @@
+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
-- 
cgit v1.2.3