diff options
author | Rutger Broekhoff | 2025-07-07 21:52:08 +0200 |
---|---|---|
committer | Rutger Broekhoff | 2025-07-07 21:52:08 +0200 |
commit | ba61dfd69504ec6263a9dee9931d93adeb6f3142 (patch) | |
tree | d6c9b78e50eeab24e0c1c09ab45909a6ae3fd5db /lib/nix/elaborator.ml | |
download | verified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.tar.gz verified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.zip |
Initialize repository
Diffstat (limited to 'lib/nix/elaborator.ml')
-rw-r--r-- | lib/nix/elaborator.ml | 208 |
1 files changed, 208 insertions, 0 deletions
diff --git a/lib/nix/elaborator.ml b/lib/nix/elaborator.ml new file mode 100644 index 0000000..36ee0d4 --- /dev/null +++ b/lib/nix/elaborator.ml | |||
@@ -0,0 +1,208 @@ | |||
1 | open Core | ||
2 | open Types | ||
3 | |||
4 | (* The Nix elaborator does a few things: | ||
5 | - Attribute paths are transformed into a simple list of expressions: | ||
6 | + Simple identifiers are rewritten to string values | ||
7 | + Antiquotations are rewritten to their component expressions | ||
8 | + Anything else, that is not a string value, is rejected | ||
9 | and raises an exception | ||
10 | - In 'inherit (...) x1 ... xn', x1 ... xn are checked for 'reasonably' being | ||
11 | identifiers, i.e., being one of x, "x" and ${"x"}. | ||
12 | - Nested attribute paths are unfolded and attribute sets are merged where | ||
13 | possible. (Where we mean 'what Nix does' with 'where possible'; see the | ||
14 | comment at the respective function.) | ||
15 | - Paths are turned into strings and made absolute w.r.t. the current | ||
16 | working directory. | ||
17 | - Indented strings are converted to their 'normal' counterpart. *) | ||
18 | |||
19 | exception ElaborateError of string | ||
20 | |||
21 | type attr_set = recursivity * binding list | ||
22 | |||
23 | let set_expr (r, bs) = Val (AttSet (r, bs)) | ||
24 | let get_id = function Id x -> x | _ -> assert false | ||
25 | |||
26 | let rec update_bnd (bs : binding list) (x : string) ~(f : expr option -> expr) = | ||
27 | match bs with | ||
28 | | [] -> [ AttrPath ([ Val (Str (x, [])) ], f None) ] | ||
29 | | AttrPath ([ Val (Str (y, [])) ], e) :: s' when String.(x = y) -> | ||
30 | AttrPath ([ Val (Str (y, [])) ], f (Some e)) :: s' | ||
31 | | Inherit (_, ids) :: _ | ||
32 | when List.exists ids ~f:(fun e -> String.(get_id e = x)) -> | ||
33 | raise (ElaborateError "Cannot update inherit") | ||
34 | | bnd :: s' -> bnd :: update_bnd s' x ~f | ||
35 | |||
36 | let set_update_bnd (r, bs) x ~f = (r, update_bnd bs x ~f) | ||
37 | |||
38 | let rec has_bnd (bs : binding list) (x : string) : bool = | ||
39 | match bs with | ||
40 | | [] -> false | ||
41 | | AttrPath ([ Val (Str (y, [])) ], _) :: _ when String.(x = y) -> true | ||
42 | | Inherit (_, ids) :: _ | ||
43 | when List.exists ids ~f:(fun e -> String.(get_id e = x)) -> | ||
44 | true | ||
45 | | _ :: bs' -> has_bnd bs' x | ||
46 | |||
47 | let merge_bnds bs1 bs2 : binding list = | ||
48 | List.fold_left bs2 ~init:bs1 ~f:(fun bs1' b2 -> | ||
49 | match b2 with | ||
50 | | AttrPath ([ Val (Str (x, [])) ], e) -> | ||
51 | update_bnd bs1' x ~f:(function | ||
52 | | Some _ -> raise (ElaborateError "Duplicated attribute") | ||
53 | | None -> e) | ||
54 | | AttrPath ([ d ], e) -> AttrPath ([ d ], e) :: bs1' | ||
55 | | Inherit (md, xs) -> | ||
56 | if List.for_all xs ~f:(fun e -> not (has_bnd bs1' (get_id e))) then | ||
57 | Inherit (md, xs) :: bs1' | ||
58 | else raise (ElaborateError "Duplicated attribute") | ||
59 | | _ -> assert false) | ||
60 | |||
61 | (* This function intentionally clobbers recursivity, because that is the way | ||
62 | that Nix likes to handle attribute insertion. See | ||
63 | (1) https://github.com/NixOS/nix/issues/9020 | ||
64 | (2) https://github.com/NixOS/nix/issues/11268 | ||
65 | (3) https://github.com/NixOS/nix/pull/11294 *) | ||
66 | let rec insert (bs : binding list) (path : expr list) (e : expr) = | ||
67 | match path with | ||
68 | | [] -> raise (ElaborateError "Cannot insert attribute with empty path") | ||
69 | | [ Val (Str (x, [])) ] -> | ||
70 | update_bnd bs x ~f:(function | ||
71 | | None -> e | ||
72 | | Some (Val (AttSet (r1, bs1))) -> ( | ||
73 | match e with | ||
74 | | Val (AttSet (_, bs2)) -> set_expr (r1, merge_bnds bs1 bs2) | ||
75 | | _ -> raise (ElaborateError "Duplicated attribute")) | ||
76 | | _ -> raise (ElaborateError "Duplicated attribute")) | ||
77 | | Val (Str (x, [])) :: rest -> | ||
78 | update_bnd bs x ~f:(function | ||
79 | | Some (Val (AttSet (r, bs))) -> Val (AttSet (r, insert bs rest e)) | ||
80 | | Some _ -> raise (ElaborateError "Duplicated attribute") | ||
81 | | None -> Val (AttSet (Nonrec, insert [] rest e))) | ||
82 | | [ part ] -> AttrPath ([ part ], e) :: bs | ||
83 | | part :: rest -> | ||
84 | AttrPath ([ part ], Val (AttSet (Nonrec, insert [] rest e))) :: bs | ||
85 | |||
86 | let insert_inherit (bs : binding list) (from : expr option) (es : expr list) = | ||
87 | if List.for_all es ~f:(fun e -> not (has_bnd bs (get_id e))) then | ||
88 | Inherit (from, es) :: bs | ||
89 | else raise (ElaborateError "Duplicated attribute") | ||
90 | |||
91 | let simplify_path_component = function | ||
92 | | Id x -> Val (Str (x, [])) | ||
93 | | Val (Str (s, ess)) -> Val (Str (s, ess)) | ||
94 | | Aquote e -> e | ||
95 | | _ -> raise (ElaborateError "Unexpected path component") | ||
96 | |||
97 | let simplify_path = List.map ~f:simplify_path_component | ||
98 | |||
99 | let simplify_bnd_paths = | ||
100 | List.map ~f:(fun bnd -> | ||
101 | match bnd with | ||
102 | | AttrPath (path, e) -> AttrPath (simplify_path path, e) | ||
103 | | Inherit (me, xs) -> Inherit (me, xs)) | ||
104 | |||
105 | (* Law: concat_lines ∘ split_lines = id *) | ||
106 | |||
107 | let rec split_lines s = | ||
108 | match String.lsplit2 s ~on:'\n' with | ||
109 | | Some (s1, s2) -> s1 :: split_lines s2 | ||
110 | | None -> [ s ] | ||
111 | |||
112 | let rec concat_lines = function | ||
113 | | [] -> "" | ||
114 | | [ x ] -> x | ||
115 | | x :: xs -> x ^ "\n" ^ concat_lines xs | ||
116 | |||
117 | let map_tail ~f = function [] -> [] | x :: xs -> x :: List.map ~f xs | ||
118 | |||
119 | let unindent n s ~skip_first_line = | ||
120 | let map_op ~f = if skip_first_line then map_tail ~f else List.map ~f in | ||
121 | split_lines s | ||
122 | |> map_op ~f:(fun line -> | ||
123 | let expected_prefix = String.make n ' ' in | ||
124 | String.chop_prefix_if_exists ~prefix:expected_prefix line) | ||
125 | |> concat_lines | ||
126 | |||
127 | let is_spaces l = String.(strip l ~drop:(Char.( = ) ' ') |> is_empty) | ||
128 | |||
129 | let drop_first_empty_line s = | ||
130 | match String.lsplit2 s ~on:'\n' with | ||
131 | | Some (l, s') when is_spaces l -> s' | ||
132 | | _ -> s | ||
133 | |||
134 | let rec process ?(dir = None) = function | ||
135 | | BinaryOp (op, e1, e2) -> BinaryOp (op, process ~dir e1, process ~dir e2) | ||
136 | | UnaryOp (op, e) -> UnaryOp (op, process ~dir e) | ||
137 | | Cond (e1, e2, e3) -> Cond (process ~dir e1, process ~dir e2, process ~dir e3) | ||
138 | | With (e1, e2) -> With (process ~dir e1, process ~dir e2) | ||
139 | | Assert (e1, e2) -> Assert (process ~dir e1, process ~dir e2) | ||
140 | | Test (e1, es) -> | ||
141 | Test (process ~dir e1, List.(simplify_path es >>| process ~dir)) | ||
142 | | SetLet bs -> SetLet (process_bnds ~dir bs) | ||
143 | | Let (bs, e) -> Let (process_bnds ~dir bs, process ~dir e) | ||
144 | | Val v -> Val (process_val ~dir v) | ||
145 | | Id x -> Id x | ||
146 | | Select (e, es, me) -> | ||
147 | Select | ||
148 | ( process ~dir e, | ||
149 | List.(simplify_path es >>| process ~dir), | ||
150 | Option.(me >>| process ~dir) ) | ||
151 | | Apply (e1, e2) -> Apply (process ~dir e1, process ~dir e2) | ||
152 | | Aquote e -> Aquote (process ~dir e) | ||
153 | |||
154 | and process_val ~dir = function | ||
155 | | Str (s, ess) -> Str (s, List.(ess >>| fun (e, s) -> (process ~dir e, s))) | ||
156 | | IStr (n, s, ess) -> | ||
157 | let s' = drop_first_empty_line (unindent n s ~skip_first_line:false) | ||
158 | and ess' = | ||
159 | List.map ess ~f:(fun (e, s) -> | ||
160 | (process ~dir e, unindent n s ~skip_first_line:true)) | ||
161 | in | ||
162 | Str (s', ess') | ||
163 | | Lambda (p, e) -> Lambda (process_pattern ~dir p, process ~dir e) | ||
164 | | List es -> List List.(es >>| process ~dir) | ||
165 | | AttSet (r, bs) -> AttSet (r, process_bnds ~dir bs) | ||
166 | | Path p -> ( | ||
167 | if Filename.is_absolute p then Str (p, []) | ||
168 | else | ||
169 | match dir with | ||
170 | | Some dir when Filename.is_absolute dir -> | ||
171 | Str (Filename.concat dir p, []) | ||
172 | | Some _ -> | ||
173 | raise | ||
174 | (ElaborateError "Provided directory should be an absolute path") | ||
175 | | None -> raise (ElaborateError "Do not know how to resolve path")) | ||
176 | | v -> v | ||
177 | |||
178 | and process_bnds ~dir bs = | ||
179 | bs | ||
180 | |> List.map ~f:(function | ||
181 | | AttrPath (es, e) -> | ||
182 | AttrPath (List.(es >>| process ~dir), process ~dir e) | ||
183 | | Inherit (me, xs) -> | ||
184 | Inherit (Option.(me >>| process ~dir), process_inherit_ids xs)) | ||
185 | |> simplify_bnd_paths | ||
186 | |> List.fold ~init:[] ~f:(fun bs' bnd -> | ||
187 | match bnd with | ||
188 | | AttrPath (path, e) -> insert bs' path e | ||
189 | | Inherit (from, es) -> insert_inherit bs' from es) | ||
190 | |||
191 | and process_inherit_ids = | ||
192 | List.map ~f:(function | ||
193 | | Id x | Val (Str (x, [])) | Aquote (Val (Str (x, []))) -> Id x | ||
194 | | _ -> raise (ElaborateError "Unexpected expression in inherit")) | ||
195 | |||
196 | and process_pattern ~dir = function | ||
197 | | Alias x -> Alias x | ||
198 | | ParamSet (mx, (ps, k)) -> ParamSet (mx, (process_param_set ~dir mx ps, k)) | ||
199 | |||
200 | and process_param_set ~dir ?(seen = String.Set.empty) mx ps = | ||
201 | match ps with | ||
202 | | [] -> [] | ||
203 | | (y, me) :: ps' -> | ||
204 | if Set.mem seen y || Option.mem mx y ~equal:String.( = ) then | ||
205 | raise (ElaborateError "Duplicated function argument") | ||
206 | else | ||
207 | (y, Option.(me >>| process ~dir)) | ||
208 | :: process_param_set ~dir mx ps' ~seen:(Set.add seen y) | ||