blob: ca1bfb540ca120ab2676b2f4c301fc831e6bca1d (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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
|
