Initialize repository

1 files changed, 54 insertions, 0 deletions

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