aboutsummaryrefslogtreecommitdiffstats
path: root/lib
diff options
context:
space:
mode:
authorRutger Broekhoff2025-07-07 21:52:08 +0200
committerRutger Broekhoff2025-07-07 21:52:08 +0200
commitba61dfd69504ec6263a9dee9931d93adeb6f3142 (patch)
treed6c9b78e50eeab24e0c1c09ab45909a6ae3fd5db /lib
downloadverified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.tar.gz
verified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.zip
Initialize repository
Diffstat (limited to 'lib')
-rw-r--r--lib/extraction/dune56
-rw-r--r--lib/extraction/extraction.ml18
-rw-r--r--lib/extraction/prelude.v52
-rw-r--r--lib/mininix/builtins.ml77
-rw-r--r--lib/mininix/builtins.nix302
-rw-r--r--lib/mininix/conv.ml96
-rw-r--r--lib/mininix/dune15
-rw-r--r--lib/mininix/import.ml54
-rw-r--r--lib/mininix/mininix.ml13
-rw-r--r--lib/mininix/mininix2nix.ml54
-rw-r--r--lib/mininix/nix2mininix.ml254
-rw-r--r--lib/mininix/run.ml17
-rw-r--r--lib/mininix/sexp.ml160
-rw-r--r--lib/nix/dune15
-rw-r--r--lib/nix/elaborator.ml208
-rw-r--r--lib/nix/lexer.mll315
-rw-r--r--lib/nix/nix.ml20
-rw-r--r--lib/nix/parser.mly310
-rw-r--r--lib/nix/printer.ml176
-rw-r--r--lib/nix/tokens.ml64
-rw-r--r--lib/nix/types.ml112
21 files changed, 2388 insertions, 0 deletions
diff --git a/lib/extraction/dune b/lib/extraction/dune
new file mode 100644
index 0000000..b56caf9
--- /dev/null
+++ b/lib/extraction/dune
@@ -0,0 +1,56 @@
1(coq.extraction
2 (prelude prelude)
3 (extracted_modules
4 Ascii
5 BinInt
6 Bits
7 Decimal
8 prelude
9 gmap
10 Nat
11 PeanoNat
12 SpecFloat
13 ZArith_dec
14 base
15 BinNat
16 Bool
17 DecimalString
18 interp
19 numbers
20 pretty
21 Specif
22 Zbool
23 Basics
24 BinNums
25 countable
26 list0
27 operational
28 res
29 String
30 Zpower
31 Binary
32 BinPosDef
33 Datatypes
34 fin_maps
35 List
36 option
37 Round
38 strings
39 BinarySingleNaN
40 BinPos
41 decidable
42 floats
43 mapset
44 orders
45 sorting
46 utils)
47 (flags
48 (-output-directory "."))
49 (theories Flocq stdpp mininix))
50
51(library
52 (name extraction)
53 (flags
54 (:standard -w -33))
55 (instrumentation
56 (backend bisect_ppx)))
diff --git a/lib/extraction/extraction.ml b/lib/extraction/extraction.ml
new file mode 100644
index 0000000..a737700
--- /dev/null
+++ b/lib/extraction/extraction.ml
@@ -0,0 +1,18 @@
1include Prelude
2include Interp
3include Operational
4include Res
5
6(* Stuff that's not part of the paper. Still exposed because we sometimes want
7 to be able to create a natural number, float, process a list etc. *)
8module Internal = struct
9 module BinNums = BinNums
10 module Datatypes = Datatypes
11 module List = List
12
13 module Floats = struct
14 include Floats
15 include Binary
16 include SpecFloat
17 end
18end
diff --git a/lib/extraction/prelude.v b/lib/extraction/prelude.v
new file mode 100644
index 0000000..ef35bcb
--- /dev/null
+++ b/lib/extraction/prelude.v
@@ -0,0 +1,52 @@
1Require Import Coq.Numbers.DecimalString ExtrOcamlBasic ExtrOcamlString.
2From stdpp Require Import strings stringmap gmap.
3From mininix Require Import nix.interp.
4
5Definition attr_set_insert (x : string) (α : attr) (αs : gmap string attr) : gmap string attr :=
6 <[x:=α]> αs.
7
8Definition attr_set_contains (x : string) (αs : gmap string attr) : bool :=
9 bool_decide (x ∈ dom αs).
10
11Definition attr_set_fold {A} (f : string → attr → A → A) (init : A) (αs : gmap string attr) : A :=
12 map_fold f init αs.
13
14Definition attr_set_empty : gmap string attr := ∅.
15
16Definition env_fold {A} (f : string → (kind * thunk) → A → A) (init : A) (E : env) : A :=
17 map_fold f init E.
18
19Definition env_insert_abs (x : string) (t : thunk) (E : env) : env :=
20 <[x:=(ABS,t)]> E.
21
22Definition thunk_map_fold {A} (f : string → thunk → A → A) (init : A) (bs : gmap string thunk) : A :=
23 map_fold f init bs.
24
25Definition thunk_map_insert (x : string) (t : thunk) (bs : gmap string thunk) : gmap string thunk :=
26 <[x:=t]> bs.
27
28Definition thunk_map_empty : gmap string thunk := ∅.
29
30Definition matcher := gmap string (option expr).
31
32Definition matcher_empty : matcher := ∅.
33
34Definition matcher_insert (x : string) (me : option expr) (ms : matcher) : matcher :=
35 <[x:=me]> ms.
36
37Definition matcher_fold {A} (f : string → option expr → A → A) (init : A) (ms : matcher) : A :=
38 map_fold f init ms.
39
40Definition env_empty : env := ∅.
41
42Definition string_of_Z (x : Z) : string :=
43 NilZero.string_of_int (Z.to_int x).
44
45Definition string_to_Z (s : string) : option Z :=
46 Z.of_int <$> NilZero.int_of_string s.
47
48Separate Extraction
49 attr_set_insert env_insert_abs matcher_insert thunk_map_insert
50 attr_set_contains attr_set_fold env_fold matcher_fold thunk_map_fold
51 env_empty attr_set_empty matcher_empty thunk_map_empty string_of_Z
52 string_to_Z interp' forallb.
diff --git a/lib/mininix/builtins.ml b/lib/mininix/builtins.ml
new file mode 100644
index 0000000..0809668
--- /dev/null
+++ b/lib/mininix/builtins.ml
@@ -0,0 +1,77 @@
1open Core
2open Nix2mininix
3
4let minimal_prelude =
5 mn_attr
6 [
7 ("true", `Nonrec, Extraction.ELit (Extraction.LitBool true));
8 ("false", `Nonrec, Extraction.ELit (Extraction.LitBool false));
9 ("null", `Nonrec, Extraction.ELit Extraction.LitNull);
10 ("seq", `Nonrec, mn_abs [ "e1"; "e2" ] (mn_seq (mn_id "e1") (mn_id "e2")));
11 ( "deepSeq",
12 `Nonrec,
13 mn_abs [ "e1"; "e2" ] (mn_deep_seq (mn_id "e1") (mn_id "e2")) );
14 ("typeOf", `Nonrec, mn_abs [ "e" ] (mn_type_of (mn_id "e")));
15 ("functionArgs", `Nonrec, mn_abs [ "f" ] (mn_function_args (mn_id "f")));
16 ( "bitAnd",
17 `Nonrec,
18 mn_abs [ "x"; "y" ] (mn_bit_and (mn_id "x") (mn_id "y")) );
19 ("bitOr", `Nonrec, mn_abs [ "x"; "y" ] (mn_bit_or (mn_id "x") (mn_id "y")));
20 ( "bitXor",
21 `Nonrec,
22 mn_abs [ "x"; "y" ] (mn_bit_xor (mn_id "x") (mn_id "y")) );
23 ("ceil", `Nonrec, mn_abs [ "x" ] (mn_ceil (mn_id "x")));
24 ("floor", `Nonrec, mn_abs [ "x" ] (mn_floor (mn_id "x")));
25 ("__mn_nearestEven", `Nonrec, mn_abs [ "x" ] (mn_nearest_even (mn_id "x")));
26 ( "__mn_singleton",
27 `Nonrec,
28 mn_abs [ "x"; "e" ] (mn_singleton_attr (mn_id "x") (mn_id "e")) );
29 ( "__mn_attr_delete",
30 `Nonrec,
31 mn_abs [ "as"; "x" ] (mn_delete_attr (mn_id "as") (mn_id "x")) );
32 ( "__mn_attr_has_prim",
33 `Nonrec,
34 mn_abs [ "d"; "e" ] (mn_has_attr (mn_id "d") (mn_id "e")) );
35 ("__mn_attr_match", `Nonrec, mn_abs [ "as" ] (mn_attr_match (mn_id "as")));
36 ("__mn_list_match", `Nonrec, mn_abs [ "xs" ] (mn_list_match (mn_id "xs")));
37 ( "__mn_string_match",
38 `Nonrec,
39 mn_abs [ "s" ] (mn_string_match (mn_id "s")) );
40 ]
41
42(* Watch out to not introduce constructs here that refer to themselves using
43 the mnbi_* functions in Nix2mininix - this can cause undesired loops. *)
44let builtins_nix =
45 Nix.elaborate (Nix.parse ~filename:"<builtins>" [%blob "builtins.nix"])
46
47let builtins =
48 Extraction.ELetAttr
49 (Extraction.ABS, minimal_prelude, Nix2mininix.from_nix builtins_nix)
50
51let exported_builtins =
52 [
53 "__mn_assert";
54 "__mn_attr_has";
55 "__mn_attr_insertNew";
56 "__mn_attr_select";
57 "__mn_attr_selectOr";
58 "abort";
59 "false";
60 "head";
61 "map";
62 "null";
63 "removeAttrs";
64 "tail";
65 "throw";
66 "toString";
67 "true";
68 ]
69
70let apply_prelude e =
71 let bindings =
72 mn_attr
73 (("builtins", `Nonrec, builtins)
74 :: List.map exported_builtins ~f:(fun x ->
75 (x, `Rec, mn_select_attr (mn_id "builtins") (mn_str x))))
76 in
77 Extraction.ELetAttr (Extraction.ABS, bindings, e)
diff --git a/lib/mininix/builtins.nix b/lib/mininix/builtins.nix
new file mode 100644
index 0000000..9c7ed32
--- /dev/null
+++ b/lib/mininix/builtins.nix
@@ -0,0 +1,302 @@
1rec {
2 inherit true false null functionArgs typeOf seq deepSeq bitAnd bitOr bitXor floor ceil; # from the minimal prelude
3
4 abort = _: null null; # we ignore the provided message
5 throw = abort; # same here
6
7 head = xs: (__mn_list_match xs).head;
8 tail = xs: (__mn_list_match xs).tail;
9
10 __mn_matchAttr = f: as: f (__mn_attr_match as);
11 __mn_matchList = f: xs: f (__mn_list_match xs);
12 __mn_matchString = f: s: f (__mn_string_match s);
13
14 __mn_foldr = op: nul:
15 __mn_matchList ({ head, tail, empty }:
16 if empty then nul else op head (__mn_foldr op nul tail));
17
18 # foldl' should really be strict. But if we do that (using seq), the
19 # complexity of this function suddenly morphs from linear to
20 # exponential, which is way worse than not actually being strict.
21 foldl' = op: nul:
22 __mn_matchList
23 ({ head, tail, empty }:
24 if empty then nul else
25 let v = op nul head; in
26 seq v (foldl' op v tail));
27 map = f:
28 __mn_matchList ({ head, tail, empty }:
29 if empty then [ ] else [ (f head) ] ++ map f tail);
30 elem = x: any (y: x == y);
31 elemAt = xs: n: assert n >= 0;
32 let go = xs: n: if n == 0 then head xs else go (tail xs) (n - 1);
33 in go xs n;
34 length = __mn_matchList ({ head, tail, empty }:
35 if empty then 0 else 1 + length tail);
36 sort = __mn_mergesort;
37 any = f: __mn_matchList ({ head, tail, empty }: !empty && (f head || any f tail));
38 all = f: __mn_matchList ({ head, tail, empty }: !empty -> (f head && all f tail));
39 concatLists =
40 __mn_matchList ({ head, tail, empty }:
41 if empty then [ ] else head ++ concatLists tail);
42 concatMap = f: xss: concatLists (map f xss);
43 concatStringsSep = sep:
44 __mn_matchList ({ head, tail, empty }:
45 if empty then "" else if tail == [ ] then head
46 else head + sep + concatStringsSep sep tail);
47 filter = f:
48 __mn_matchList ({ head, tail, empty }:
49 if empty then [ ] else (if f head then [ head ] else [ ]) ++ filter f tail);
50 groupBy = f: xs:
51 let update = x: acc: acc // { ${f x} = [ x ] ++ (acc.${f x} or [ ]); };
52 in __mn_foldr update { } xs;
53 partition = f: groupBy (x: if f x then "right" else "wrong");
54
55 hasAttr = x: as: as ? ${x};
56 getAttr = x: as: as.${x};
57 attrNames = __mn_matchAttr ({ key, tail, empty, ... }:
58 if empty then [ ] else [ key ] ++ attrNames tail);
59 attrValues = __mn_matchAttr ({ head, tail, empty, ... }:
60 if empty then [ ] else [ head ] ++ attrValues tail);
61 mapAttrs = f: __mn_matchAttr ({ key, head, tail, empty }:
62 if empty then { } else
63 mapAttrs f tail // { ${key} = f key head; });
64 removeAttrs = __mn_foldr (x: as': __mn_attr_delete as' x);
65 zipAttrsWith = f: ass: mapAttrs f (__mn_zipAttrs ass);
66 catAttrs = x:
67 __mn_matchList ({ head, tail, empty }:
68 if empty then [ ]
69 else (if head ? ${x} then [ head.${x} ] else [ ]) ++ catAttrs x tail);
70 listToAttrs =
71 __mn_foldr (attr: as': as' // { ${attr.name} = attr.value; }) { };
72 intersectAttrs = e1: e2:
73 __mn_matchAttr
74 ({ key, head, tail, empty }:
75 if empty then { } else
76 (if e2 ? ${key} then { ${key} = e2.${key}; } else { }) //
77 intersectAttrs tail (__mn_attr_delete e2 key))
78 e1;
79
80 lessThan = x: y: x < y; # documentation is misleading, not only for numbers
81 add = x: y: x + y;
82 mul = x: y: x * y;
83 div = x: y: x / y;
84 sub = x: y: x - y;
85 genList = gen: n:
86 let
87 aux = off: if off >= n then [ ] else
88 [ (gen off) ] ++ aux (off + 1);
89 in
90 aux 0;
91
92 __mn_genericClosure = { operator, seen, startSet }:
93 __mn_matchList
94 ({ head, tail, empty }:
95 if empty then [ ] else
96 if seen head.key
97 then __mn_genericClosure { inherit operator seen; startSet = tail; }
98 else [ head ] ++ __mn_genericClosure {
99 inherit operator;
100 seen = k: k == head.key || seen k;
101 startSet = tail ++ operator head;
102 })
103 startSet;
104 genericClosure = { operator, startSet }:
105 __mn_genericClosure { inherit operator startSet; seen = _: false; };
106
107 isAttrs = e: typeOf e == "set";
108 isBool = e: typeOf e == "bool";
109 isFloat = e: typeOf e == "float";
110 isFunction = e: typeOf e == "lambda";
111 isInt = e: typeOf e == "int";
112 isList = e: typeOf e == "list";
113 isNull = e: typeOf e == "null";
114 isString = e: typeOf e == "string";
115
116 toString = e:
117 if isAttrs e then
118 if e ? __toString then e.__toString e else e.outPath
119 else if isBool e then
120 if e then "1" else ""
121 else if isFloat e then
122 __mn_float_toString e
123 else if isInt e then
124 __mn_int_toString e
125 else if isList e then
126 concatStringsSep " " (map toString e)
127 else if isNull e then
128 ""
129 else if isString e then
130 e
131 else abort null;
132
133 stringLength =
134 __mn_matchString ({ head, tail, empty }:
135 if empty then 0 else 1 + stringLength tail);
136
137 substring = start: assert start >= 0; len:
138 __mn_matchString ({ head, tail, empty }:
139 if empty || len == 0 then "" else
140 if start > 0
141 then substring (start - 1) len tail
142 else head + substring 0 (len - 1) tail);
143
144 replaceStrings = from: to: s:
145 __mn_matchList
146 ({ head, tail, empty }:
147 let from = if empty then [ ] else [ head ] ++ tail; in
148 __mn_matchList
149 ({ head, tail, empty }:
150 let to = if empty then [ ] else [ head ] ++ tail; in
151 assert length from == length to;
152 __mn_strings_replace from to s)
153 to)
154 from;
155
156 __mn_strings_replace = subsFrom: subsTo: s:
157 let go = __mn_strings_replace subsFrom subsTo; in
158 __mn_strings_replace_aux go subsFrom subsTo s;
159
160 __mn_strings_replace_aux = go: subsFrom: subsTo: s:
161 __mn_matchList
162 ({ head, tail, empty }:
163 if empty
164 then
165 __mn_matchString
166 ({ head, tail, empty }: if empty then "" else head + go tail)
167 s
168 else
169 let subFrom = head; subsFrom' = tail; in
170 __mn_matchList
171 ({ head, tail, ... }:
172 let subTo = head; subsTo' = tail; in
173 if subFrom == ""
174 then
175 # We can only ask ourselves why, but it is so -- in Nix:
176 # replaceStrings ["" "a"] ["X" "_"] "asdf" ~> "XaXsXdXfX"
177 # and so we emulate this 'behavior'
178 subTo + __mn_matchString
179 ({ head, tail, empty }:
180 if empty then "" else head + go tail)
181 s
182 else
183 ({ ok, rest }:
184 if ok
185 then subTo + go rest
186 else __mn_strings_replace_aux go subsFrom' subsTo' s)
187 (__mn_string_chopPrefix subFrom s))
188 subsTo)
189 subsFrom;
190
191 __mn_string_chopPrefix = prefix: s:
192 __mn_matchString
193 ({ head, tail, empty }:
194 if empty then { ok = true; rest = s; } else
195 let prefix = head; prefix' = tail; in __mn_matchString
196 ({ head, tail, empty }:
197 if empty || prefix != head then { ok = false; rest = null; } else
198 __mn_string_chopPrefix prefix' tail)
199 s)
200 prefix;
201
202 __mn_string_drop = n: s:
203 if n <= 0 then s else
204 __mn_matchString
205 ({ tail, empty, ... }:
206 if empty then "" else
207 __mn_string_drop (n - 1) tail)
208 s;
209
210 __mn_float_toString = x:
211 let
212 sign = x < 0;
213 abs = __mn_abs x;
214 int = floor abs;
215 dec = __mn_nearestEven ((abs - int) * 1000000);
216 in
217 (if sign then "-" else "") +
218 __mn_int_toString int + "." + __mn_int_toString dec;
219 __mn_int_toString = x: (if x < 0 then "-" else "") +
220 (
221 let d10 = __mn_quotRem (__mn_abs x) 10; in
222 (if d10.quot != 0 then toString d10.quot else "") +
223 (if d10.rem == 0 then "0" else
224 if d10.rem == 1 then "1" else
225 if d10.rem == 2 then "2" else
226 if d10.rem == 3 then "3" else
227 if d10.rem == 4 then "4" else
228 if d10.rem == 5 then "5" else
229 if d10.rem == 6 then "6" else
230 if d10.rem == 7 then "7" else
231 if d10.rem == 8 then "8" else
232 if d10.rem == 9 then "9" else
233 abort null)
234 );
235
236 __mn_quotRem = x: y:
237 let quot = x / y; in
238 { inherit quot; rem = x - quot * y; };
239 __mn_abs = x: if x < 0 then -x else x;
240
241 __mn_attr_insertNew = as: x: e:
242 if x == null then { } else
243 assert !(as ? ${x}); as // __mn_singleton x e;
244 __mn_attr_has_aux = d: e:
245 if typeOf d != "set" then false else __mn_attr_has_prim d e;
246 __mn_attr_has = e:
247 __mn_matchList ({ head, tail, empty }:
248 if empty then true else
249 if __mn_attr_has_aux e head then __mn_attr_has e.${head} tail
250 else false);
251 __mn_attr_select = e:
252 __mn_matchList ({ head, tail, empty }:
253 if empty then e
254 else __mn_attr_select e.${head} tail);
255 __mn_attr_selectOr = e: as: d:
256 if __mn_attr_has e as
257 then __mn_attr_select e as
258 else d;
259 __mn_assert = e1: e2:
260 if e1 then e2 else abort null;
261
262 __mn_consAttrs = as: acc:
263 __mn_foldr
264 (x: acc: acc // {
265 ${x} = [ as.${x} ] ++ (acc.${x} or [ ]);
266 })
267 acc
268 (attrNames as);
269 __mn_zipAttrs = __mn_foldr __mn_consAttrs { };
270
271 # Old merge sort algorithm, taken from GHC.Internal.Data.OldList.
272 __mn_mergesort = cmp: xs: __mn_mergesort' cmp (__mn_singletons xs);
273 __mn_singletons = map (x: [ x ]);
274 __mn_mergesort' = cmp: xs:
275 __mn_matchList
276 ({ head, tail, empty }:
277 if empty then [ ] else if tail == [ ] then head else
278 __mn_mergesort' cmp (__mn_mergePairs cmp xs))
279 xs;
280 __mn_mergePairs = cmp:
281 __mn_matchList ({ head, tail, empty }: if empty then [ ] else
282 let xs' = head; in __mn_matchList
283 ({ head, tail, empty }:
284 if empty then [ xs' ] else
285 let ys' = head; xss' = tail; in
286 [ (__mn_merge cmp xs' ys') ] ++ __mn_mergePairs cmp xss')
287 tail);
288 __mn_merge = cmp: xs: ys:
289 __mn_matchList
290 ({ head, tail, empty }:
291 if empty then ys else
292 let x = head; xs' = tail; in
293 __mn_matchList
294 ({ head, tail, empty }:
295 if empty then xs else
296 let y = head; ys' = tail; in
297 if cmp y x
298 then [ y ] ++ __mn_merge cmp xs ys' # y < x, i.e., x > y
299 else [ x ] ++ __mn_merge cmp xs' ys)
300 ys)
301 xs;
302}
diff --git a/lib/mininix/conv.ml b/lib/mininix/conv.ml
new file mode 100644
index 0000000..8062099
--- /dev/null
+++ b/lib/mininix/conv.ml
@@ -0,0 +1,96 @@
1open Core
2
3let _ = assert (Sys.word_size_in_bits = 64)
4let chlist s = String.to_list s
5let ( <> ) l1 l2 = not (List.equal Char.( = ) l1 l2)
6let str = String.of_char_list
7let prec = 53
8let emax = 1024
9let exp_bits = 11
10let saturated_exp = Int.shift_left 1 exp_bits - 1
11
12let rec int_bits (x : int) : bool list =
13 if Int.(x < 0) then raise (Invalid_argument "Number must be nonnegative")
14 else if Int.(x = 0) then []
15 else
16 let q = x /% 2 and r = x % 2 in
17 int_bits q @ [ r = 1 ]
18
19let int_to_positive (x : int) : Extraction.Internal.BinNums.positive =
20 if x <= 0 then raise (Invalid_argument "Number must be positive")
21 else
22 let bits = List.tl_exn (int_bits x) in
23 List.fold_left
24 ~f:(fun acc digit ->
25 if digit then Extraction.Internal.BinNums.Coq_xI acc
26 else Extraction.Internal.BinNums.Coq_xO acc)
27 ~init:Extraction.Internal.BinNums.Coq_xH bits
28
29let int_to_z (x : int) : Extraction.Internal.BinNums.coq_Z =
30 if x = 0 then Z0
31 else if x < 0 then Zneg (int_to_positive (-x))
32 else Zpos (int_to_positive x)
33
34let rec int63_of_positive (x : Extraction.Internal.BinNums.positive) : Int63.t =
35 let two = Int63.(succ one) in
36 match x with
37 | Coq_xH -> Int63.of_int_exn 1
38 | Coq_xO x -> Int63.(two * int63_of_positive x)
39 | Coq_xI x -> Int63.((two * int63_of_positive x) + one)
40
41let int63_of_z (x : Extraction.Internal.BinNums.coq_Z) : Int63.t =
42 match x with
43 | Z0 -> Int63.zero
44 | Zpos x -> int63_of_positive x
45 | Zneg x -> Int63.neg (int63_of_positive x)
46
47let int63_to_positive x = Int63.to_int_exn x |> int_to_positive
48
49(* Conversions are the same as those in Coq's FloatOps.
50 See https://github.com/coq/coq/blob/master/theories/Floats/FloatOps.v *)
51
52let normfr_mantissa f =
53 let f = Float.abs f in
54 if Float.(f >= 0.5) && Float.(f < 1.) then Float.to_int (Float.ldexp f prec)
55 else 0
56
57let float_to_flocq (x : float) : Extraction.Internal.Floats.float =
58 match Float.classify x with
59 | Zero -> Extraction.Internal.Floats.B754_zero (Float.ieee_negative x)
60 | Nan ->
61 Extraction.Internal.Floats.B754_nan
62 (Float.ieee_negative x, Float.ieee_mantissa x |> int63_to_positive)
63 | Infinite -> Extraction.Internal.Floats.B754_infinity (Float.ieee_negative x)
64 | Normal | Subnormal -> (
65 let prec_z = int_to_z prec and emax_z = int_to_z emax in
66 let r, exp = Float.frexp x in
67 let e = int_to_z (exp - prec) and r' = int_to_z (normfr_mantissa r) in
68 let shr, e' =
69 Extraction.Internal.Floats.(shr_fexp prec_z emax_z r' e Coq_loc_Exact)
70 in
71 match shr.shr_m with
72 | Zpos p -> B754_finite (Float.is_negative x, p, e')
73 | Zneg _ | Z0 -> assert false)
74
75let float_from_flocq x : float =
76 match x with
77 | Extraction.Internal.Floats.B754_zero s ->
78 Float.create_ieee_exn ~negative:s ~mantissa:Int63.zero ~exponent:0
79 | Extraction.Internal.Floats.B754_infinity s ->
80 if s then Float.neg_infinity else Float.infinity
81 | Extraction.Internal.Floats.B754_nan (s, m) ->
82 let m_int = int63_of_positive m in
83 Float.create_ieee_exn ~negative:s ~mantissa:m_int ~exponent:saturated_exp
84 | Extraction.Internal.Floats.B754_finite (s, m, e) ->
85 let pm = Float.of_int63 (int63_of_positive m) in
86 let f = Float.ldexp pm (Int63.to_int_exn (int63_of_z e)) in
87 if s then Float.neg f else f
88
89open struct
90 open Base_quickcheck
91
92 let%expect_test "float conversion" =
93 Test.run_exn
94 (module Float)
95 ~f:(fun x -> [%test_eq: float] (float_from_flocq (float_to_flocq x)) x)
96end
diff --git a/lib/mininix/dune b/lib/mininix/dune
new file mode 100644
index 0000000..aabbf45
--- /dev/null
+++ b/lib/mininix/dune
@@ -0,0 +1,15 @@
1(library
2 (name mininix)
3 (inline_tests)
4 (preprocessor_deps
5 (file builtins.nix))
6 (preprocess
7 (pps
8 ppx_blob
9 ppx_sexp_conv
10 ppx_expect
11 ppx_assert
12 base_quickcheck.ppx_quickcheck))
13 (instrumentation
14 (backend bisect_ppx))
15 (libraries core extraction nix ppx_blob ppx_sexp_conv))
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 @@
1open Core
2
3exception ImportError of string
4
5type tree = { filename : string; deps : forest }
6and forest = tree list
7
8let provide (imports : (string * Extraction.coq_val) list) =
9 let imports_set =
10 Extraction.(
11 VAttr
12 (List.fold imports ~init:thunk_map_empty ~f:(fun attrs (filename, v) ->
13 thunk_map_insert (Conv.chlist filename) (Forced v) attrs)))
14 in
15 let make_env =
16 Extraction.(
17 env_insert_abs (Conv.chlist "imports") (Forced imports_set) env_empty)
18 in
19 Extraction.(
20 VClo
21 ( Conv.chlist "path",
22 make_env,
23 EBinOp
24 ( SelectAttrOp,
25 EId (Conv.chlist "imports", None),
26 EId (Conv.chlist "path", None) ) ))
27
28let make_env (imports : (string * Extraction.coq_val) list) =
29 Extraction.(
30 env_insert_abs (Conv.chlist "import") (Forced (provide imports)) env_empty)
31
32let rec import trees : (string * Extraction.coq_val) list =
33 List.map trees ~f:(fun { filename; deps } ->
34 let data = In_channel.read_all filename in
35 Nix.parse ~filename data |> Nix.elaborate |> Nix2mininix.from_nix
36 |> Builtins.apply_prelude
37 |> Run.interp ~fuel:`Unlimited ~mode:`Shallow
38 ~env:(make_env (import deps))
39 |> function
40 | Res (Some v) -> (filename, v)
41 | Res None ->
42 raise
43 (ImportError
44 (sprintf "Could not import %s: Failed to evaluate" filename))
45 | NoFuel -> assert false)
46
47let rec tree_map ~(f : string -> string) { filename; deps } =
48 { filename = f filename; deps = forest_map ~f deps }
49
50and forest_map ~(f : string -> string) trees = List.map ~f:(tree_map ~f) trees
51
52(* [relative_to] must be an absolute path *)
53let materialize forest ~relative_to : (string * Extraction.coq_val) list =
54 forest_map forest ~f:(Filename.to_absolute_exn ~relative_to) |> import
diff --git a/lib/mininix/mininix.ml b/lib/mininix/mininix.ml
new file mode 100644
index 0000000..b121619
--- /dev/null
+++ b/lib/mininix/mininix.ml
@@ -0,0 +1,13 @@
1module Nix2mininix = Nix2mininix
2module Mininix2nix = Mininix2nix
3module Sexp = Sexp
4module Import = Import
5
6let interp_tl ~fuel ~mode ?(imports = []) e =
7 Run.interp ~fuel ~mode ~env:(Import.make_env imports) e
8
9let apply_prelude = Builtins.apply_prelude
10
11let preprocess input ~filename =
12 input |> Nix.parse ~filename |> Nix.elaborate |> Nix2mininix.from_nix
13 |> Builtins.apply_prelude
diff --git a/lib/mininix/mininix2nix.ml b/lib/mininix/mininix2nix.ml
new file mode 100644
index 0000000..efbc42a
--- /dev/null
+++ b/lib/mininix/mininix2nix.ml
@@ -0,0 +1,54 @@
1open Conv
2open Core
3
4(* [or] is not a 'strong' keyword. That means that 'it depends' whether it is
5 identified as such. In the context of the left-hand side of an attribute, it
6 is not recognized as such. *)
7let strong_keywords =
8 [ "with"; "rec"; "let"; "in"; "inherit"; "if"; "then"; "else"; "assert" ]
9
10let id_re = Str.regexp {|^[A-Za-z_]+[A-Za-z0-9'_-]*$|}
11
12let is_simple_id s =
13 Str.string_match id_re s 0
14 && not (List.exists strong_keywords ~f:(String.( = ) s))
15
16let thunk_map_to_map tm =
17 Extraction.thunk_map_fold
18 (fun k t -> Map.add_exn ~key:(String.of_char_list k) ~data:t)
19 (Map.empty (module String))
20 tm
21
22let from_lit l =
23 match l with
24 | Extraction.LitString s -> Nix.Ast.Val (Nix.Ast.Str (str s, []))
25 | Extraction.LitNull -> Nix.Ast.Id "null"
26 | Extraction.LitBool b -> Nix.Ast.Id (if b then "true" else "false")
27 | Extraction.LitNum x ->
28 Nix.Ast.Val
29 (match x with
30 | Extraction.NInt x -> Nix.Ast.Int (x |> Extraction.string_of_Z |> str)
31 | Extraction.NFloat x ->
32 Nix.Ast.Float (Printf.sprintf "%g" (float_from_flocq x)))
33
34let rec from_val = function
35 | Extraction.VClo _ | Extraction.VCloMatch _ -> Nix.Ast.Id "<CODE>"
36 | Extraction.VLit l -> from_lit l
37 | Extraction.VAttr bs ->
38 let bs =
39 thunk_map_to_map bs
40 |> Map.to_alist ~key_order:`Increasing
41 |> List.map ~f:(fun (x, t) ->
42 let lhs =
43 if is_simple_id x then Nix.Ast.Id x
44 else Nix.Ast.Val (Nix.Ast.Str (x, []))
45 in
46 Nix.Ast.AttrPath ([ lhs ], from_thunk t))
47 in
48 Nix.Ast.Val (Nix.Ast.AttSet (Nix.Ast.Nonrec, bs))
49 | Extraction.VList ts -> Nix.Ast.Val (Nix.Ast.List List.(ts >>| from_thunk))
50
51and from_thunk = function
52 | Extraction.Thunk (_, ELit l) -> from_lit l
53 | Extraction.Thunk _ | Extraction.Indirect _ -> Nix.Ast.Id "<CODE>"
54 | Extraction.Forced v -> from_val v
diff --git a/lib/mininix/nix2mininix.ml b/lib/mininix/nix2mininix.ml
new file mode 100644
index 0000000..cfd4fa3
--- /dev/null
+++ b/lib/mininix/nix2mininix.ml
@@ -0,0 +1,254 @@
1open Conv
2open Core
3
4exception FromNixError of string
5
6let try_insert_attr x e bs =
7 let x = chlist x in
8 if Extraction.attr_set_contains x bs then
9 raise (FromNixError "Attribute already exists")
10 else Extraction.attr_set_insert x e bs
11
12(* Shorthands, minor conversions *)
13
14let mn_singleton_set x e =
15 Extraction.(
16 EAttr (attr_set_insert (chlist x) (Attr (NONREC, e)) attr_set_empty))
17
18let mn_abs args e =
19 List.fold_right args ~init:e ~f:(fun arg e' ->
20 Extraction.EAbs (chlist arg, e'))
21
22let mn_lit l = Extraction.ELit l
23let mn_int x = mn_lit (Extraction.LitNum (Extraction.NInt x))
24let mn_float x = mn_lit (Extraction.LitNum (Extraction.NFloat x))
25let mn_bool b = mn_lit (Extraction.LitBool b)
26let mn_true = mn_bool true
27let mn_false = mn_bool false
28let mn_str s = mn_lit (Extraction.LitString (chlist s))
29let mn_null = mn_lit Extraction.LitNull
30let mn_id x = Extraction.EId (chlist x, None)
31let mn_app e1 e2 = Extraction.EApp (e1, e2)
32let mn_seq e1 e2 = Extraction.ESeq (Extraction.SHALLOW, e1, e2)
33let mn_deep_seq e1 e2 = Extraction.ESeq (Extraction.DEEP, e1, e2)
34let mn_list es = Extraction.EList es
35
36let mn_attr (bs : (string * [ `Rec | `Nonrec ] * Extraction.expr) list) =
37 Extraction.EAttr
38 (List.fold_left bs ~init:Extraction.attr_set_empty ~f:(fun bs' (x, r, e) ->
39 let r' =
40 match r with `Rec -> Extraction.REC | `Nonrec -> Extraction.NONREC
41 in
42 Extraction.attr_set_insert (chlist x) (Extraction.Attr (r', e)) bs'))
43
44let mn_with e1 e2 = Extraction.ELetAttr (Extraction.WITH, e1, e2)
45let mn_binop op e1 e2 = Extraction.EBinOp (op, e1, e2)
46let mn_add e1 e2 = mn_binop Extraction.AddOp e1 e2
47let mn_sub e1 e2 = mn_binop Extraction.SubOp e1 e2
48let mn_mul e1 e2 = mn_binop Extraction.MulOp e1 e2
49let mn_div e1 e2 = mn_binop Extraction.DivOp e1 e2
50let mn_bit_and e1 e2 = mn_binop Extraction.AndOp e1 e2
51let mn_bit_or e1 e2 = mn_binop Extraction.OrOp e1 e2
52let mn_bit_xor e1 e2 = mn_binop Extraction.XOrOp e1 e2
53let mn_lt e1 e2 = mn_binop Extraction.LtOp e1 e2
54let mn_eq e1 e2 = mn_binop Extraction.EqOp e1 e2
55let mn_if e1 e2 e3 = Extraction.EIf (e1, e2, e3)
56let mn_delete_attr e1 e2 = mn_binop Extraction.DeleteAttrOp e1 e2
57let mn_has_attr e1 e2 = mn_binop Extraction.HasAttrOp e1 e2
58let mn_select_attr e1 e2 = mn_binop Extraction.SelectAttrOp e1 e2
59
60let mn_singleton_attr e1 e2 =
61 mn_app (mn_binop Extraction.SingletonAttrOp e1 mn_null) e2
62
63let mn_update_attr e1 e2 = mn_binop Extraction.UpdateAttrOp e1 e2
64let mn_type_of e = mn_binop Extraction.TypeOfOp e mn_null
65let mn_function_args e = mn_binop Extraction.FunctionArgsOp e mn_null
66let mn_list_append e1 e2 = mn_binop Extraction.AppendListOp e1 e2
67let mn_list_match e = mn_binop Extraction.MatchListOp e mn_null
68let mn_string_match e = mn_binop Extraction.MatchStringOp e mn_null
69let mn_attr_match e = mn_binop Extraction.MatchAttrOp e mn_null
70let mn_ceil e = mn_binop (Extraction.RoundOp Ceil) e mn_null
71let mn_nearest_even e = mn_binop (Extraction.RoundOp NearestEven) e mn_null
72let mn_floor e = mn_binop (Extraction.RoundOp Floor) e mn_null
73
74(* Macros *)
75
76let mn_cast_bool e = mn_if e mn_true mn_false
77let mn_or e1 e2 = mn_if e1 mn_true (mn_cast_bool e2)
78let mn_and e1 e2 = mn_if e1 (mn_cast_bool e2) mn_false
79let mn_impl e1 e2 = mn_if e1 (mn_cast_bool e2) mn_true
80let mn_not e = mn_if e mn_false mn_true
81let mn_negate e = mn_sub (mn_int Extraction.Internal.BinNums.Z0) e
82let mn_neq e1 e2 = mn_not (mn_eq e2 e1)
83let mn_gt e1 e2 = mn_lt e2 e1
84let mn_lte e1 e2 = mn_not (mn_gt e1 e2)
85let mn_gte e1 e2 = mn_not (mn_lt e1 e2)
86
87(* Macros based on exported functions from the prelude *)
88
89let mnbi_assert e1 e2 = mn_app (mn_app (mn_id "__mn_assert") e1) e2
90let mnbi_has_attr e ds = mn_app (mn_app (mn_id "__mn_attr_has") e) (mn_list ds)
91let mnbi_select e ds = mn_app (mn_app (mn_id "__mn_attr_select") e) (mn_list ds)
92
93let mnbi_select_or e1 ds e2 =
94 mn_app (mn_app (mn_app (mn_id "__mn_attr_selectOr") e1) (mn_list ds)) e2
95
96let mnbi_insert_new e1 e2 e3 =
97 mn_app (mn_app (mn_app (mn_id "__mn_attr_insertNew") e1) e2) e3
98
99let is_dynamic_binding (b : Nix.Ast.binding) =
100 match b with
101 | Nix.Ast.AttrPath ([ Nix.Ast.Val (Nix.Ast.Str (_, [])) ], _)
102 | Nix.Ast.Inherit _ ->
103 false
104 | Nix.Ast.AttrPath ([ _ ], _) -> true
105 | _ -> assert false
106
107let has_dynamic_bindings (bs : Nix.Ast.binding list) =
108 List.exists bs ~f:is_dynamic_binding
109
110(* Static bindings left, dynamic bindings right *)
111let partition_dynamic (bs : Nix.Ast.binding list) :
112 Nix.Ast.binding list * Nix.Ast.binding list =
113 List.fold_left bs ~init:([], []) ~f:(fun (static, dynamic) b ->
114 if is_dynamic_binding b then (static, b :: dynamic)
115 else (b :: static, dynamic))
116
117(* Precondition: e must be have been processed by the elaborator. *)
118let rec from_nix e =
119 match e with
120 | Nix.Ast.BinaryOp (op, e1, e2) -> (
121 let e1', e2' = (from_nix e1, from_nix e2) in
122 match op with
123 | Nix.Ast.Plus -> mn_add e1' e2'
124 | Nix.Ast.Minus -> mn_sub e1' e2'
125 | Nix.Ast.Mult -> mn_mul e1' e2'
126 | Nix.Ast.Div -> mn_div e1' e2'
127 | Nix.Ast.Gt -> mn_gt e1' e2'
128 | Nix.Ast.Lt -> mn_lt e1' e2'
129 | Nix.Ast.Lte -> mn_lte e1' e2'
130 | Nix.Ast.Gte -> mn_gte e1' e2'
131 | Nix.Ast.Eq -> mn_eq e1' e2'
132 | Nix.Ast.Neq -> mn_neq e1' e2'
133 | Nix.Ast.Or -> mn_or e1' e2'
134 | Nix.Ast.And -> mn_and e1' e2'
135 | Nix.Ast.Impl -> mn_impl e1' e2'
136 | Nix.Ast.Merge -> mn_update_attr e1' e2'
137 | Nix.Ast.Concat -> mn_list_append e1' e2')
138 | Nix.Ast.UnaryOp (op, e) -> (
139 let e = from_nix e in
140 match op with Nix.Ast.Negate -> mn_negate e | Nix.Ast.Not -> mn_not e)
141 | Nix.Ast.Cond (e1, e2, e3) -> mn_if (from_nix e1) (from_nix e2) (from_nix e3)
142 | Nix.Ast.With (e1, e2) -> mn_with (from_nix e1) (from_nix e2)
143 | Nix.Ast.Assert (e1, e2) -> mnbi_assert (from_nix e1) (from_nix e2)
144 | Nix.Ast.Test (e, ds) -> mnbi_has_attr (from_nix e) List.(ds >>| from_nix)
145 | Nix.Ast.SetLet bs ->
146 from_nix
147 (Nix.Ast.Select
148 ( Nix.Ast.Val (Nix.Ast.AttSet (Nix.Ast.Rec, bs)),
149 [ Nix.Ast.Val (Nix.Ast.Str ("body", [])) ],
150 None ))
151 | Nix.Ast.Let (bs, e2) ->
152 if has_dynamic_bindings bs then
153 raise (FromNixError "Let bindings may not be dynamic");
154 let e1 = from_nix (Nix.Ast.Val (Nix.Ast.AttSet (Nix.Ast.Rec, bs))) in
155 Extraction.ELetAttr (Extraction.ABS, e1, from_nix e2)
156 | Nix.Ast.Val v -> from_nix_val v
157 | Nix.Ast.Id x -> mn_id x
158 | Nix.Ast.Select (e, parts, md) -> (
159 match md with
160 | Some d ->
161 mnbi_select_or (from_nix e) List.(parts >>| from_nix) (from_nix d)
162 | None -> (
163 match parts with
164 | [ part ] -> mn_select_attr (from_nix e) (from_nix part)
165 | _ -> mnbi_select (from_nix e) List.(parts >>| from_nix)))
166 | Nix.Ast.Apply (e1, e2) -> mn_app (from_nix e1) (from_nix e2)
167 | Nix.Ast.Aquote _ ->
168 assert false (* should be gone after processing by elaborator *)
169
170and from_nix_val v =
171 match v with
172 | Str (s, parts) ->
173 let parts = List.(parts >>= fun (e, s) -> [ from_nix e; mn_str s ]) in
174 List.fold_left parts ~init:(mn_str s) ~f:mn_add
175 | IStr _ -> raise (FromNixError "Indented strings are not supported")
176 | Int n -> (
177 match Extraction.string_to_Z (chlist n) with
178 | Some n -> mn_int n
179 | None -> raise (FromNixError "Bad integer literal"))
180 | Float n ->
181 let n =
182 try Float.of_string n
183 with Invalid_argument _ -> raise (FromNixError "Bad float literal")
184 in
185 if Float.(is_nan n || is_inf n) then
186 raise (FromNixError "Bad float literal")
187 else mn_float (float_to_flocq n)
188 | Path _ | SPath _ | HPath _ -> raise (FromNixError "Paths are not supported")
189 | Uri s -> mn_str s
190 | Lambda (Alias x, e) -> mn_abs [ x ] (from_nix e)
191 | Lambda (ParamSet (Some x, fs), e) ->
192 from_nix_val
193 (Lambda (Alias x, Apply (Val (Lambda (ParamSet (None, fs), e)), Id x)))
194 | Lambda (ParamSet (None, (fs, strictness)), e) ->
195 let ms =
196 List.fold_left fs ~init:Extraction.matcher_empty ~f:(fun ms (x, me) ->
197 Extraction.matcher_insert (chlist x) (Option.map ~f:from_nix me) ms)
198 in
199 Extraction.EAbsMatch
200 ( ms,
201 (match strictness with Loose -> false | Exact -> true),
202 from_nix e )
203 | List es -> mn_list (List.map es ~f:from_nix)
204 | AttSet (recursivity, bs) ->
205 let static, dynamic = partition_dynamic bs
206 and recursivity' =
207 match recursivity with
208 | Nix.Ast.Rec -> Extraction.REC
209 | Nix.Ast.Nonrec -> Extraction.NONREC
210 in
211
212 let set_no_dyn =
213 Extraction.EAttr
214 (List.fold_left static ~init:Extraction.attr_set_empty
215 ~f:(fun static' bnd ->
216 match bnd with
217 | Nix.Ast.AttrPath ([ Nix.Ast.Val (Nix.Ast.Str (x, [])) ], e) ->
218 try_insert_attr x
219 (Extraction.Attr (recursivity', from_nix e))
220 static'
221 | Nix.Ast.Inherit (None, xs) ->
222 List.fold_left xs ~init:static' ~f:(fun static' x ->
223 match x with
224 | Id x ->
225 try_insert_attr x
226 (Extraction.Attr (Extraction.NONREC, mn_id x))
227 static'
228 | _ -> assert false)
229 | Nix.Ast.Inherit (Some e, xs) ->
230 let e = from_nix e in
231 List.fold_left xs ~init:static' ~f:(fun static' x ->
232 match x with
233 | Id x ->
234 try_insert_attr x
235 (Extraction.Attr
236 (recursivity', mn_select_attr e (mn_str x)))
237 static'
238 | _ -> assert false)
239 | _ -> assert false))
240 in
241
242 List.fold_right dynamic ~init:set_no_dyn ~f:(fun bnd set ->
243 match bnd with
244 | Nix.Ast.AttrPath ([ d ], e) ->
245 mnbi_insert_new set
246 (match recursivity with
247 | Nix.Ast.Rec ->
248 Extraction.ELetAttr (Extraction.ABS, set_no_dyn, from_nix d)
249 | Nix.Ast.Nonrec -> from_nix d)
250 (match recursivity with
251 | Nix.Ast.Rec ->
252 Extraction.ELetAttr (Extraction.ABS, set_no_dyn, from_nix e)
253 | Nix.Ast.Nonrec -> from_nix e)
254 | _ -> assert false)
diff --git a/lib/mininix/run.ml b/lib/mininix/run.ml
new file mode 100644
index 0000000..f33bace
--- /dev/null
+++ b/lib/mininix/run.ml
@@ -0,0 +1,17 @@
1open Core
2
3(* The [n]th Church numeral *)
4let rec church n f x = if n <= 0 then x else church (n - 1) f (f x)
5
6let limited =
7 church 2048
8 (fun x -> Extraction.Internal.Datatypes.S x)
9 Extraction.Internal.Datatypes.O
10
11let rec infinity = Extraction.Internal.Datatypes.S infinity
12
13let interp ~fuel ~mode ~env e =
14 let mode : Extraction.mode =
15 match mode with `Shallow -> SHALLOW | `Deep -> DEEP
16 and fuel = match fuel with `Unlimited -> infinity | `Limited -> limited in
17 Extraction.interp' fuel mode env e
diff --git a/lib/mininix/sexp.ml b/lib/mininix/sexp.ml
new file mode 100644
index 0000000..95da655
--- /dev/null
+++ b/lib/mininix/sexp.ml
@@ -0,0 +1,160 @@
1open Conv
2open Core
3open Extraction
4
5exception ToSexpError of string
6
7let tag t l = Sexp.List (Sexp.Atom t :: l)
8
9let lit_to_sexp = function
10 | LitString s -> tag "LitString" [ Sexp.Atom (str s) ]
11 | LitNum (NInt n) ->
12 tag "LitNum" [ Sexp.Atom "INT"; Sexp.Atom (str (string_of_Z n)) ]
13 | LitNum (NFloat n) ->
14 tag "LitNum"
15 [
16 Sexp.Atom "FLOAT";
17 Sexp.Atom (Printf.sprintf "%g" (float_from_flocq n));
18 ]
19 | LitBool b -> tag "LitBool" [ Sexp.Atom (Bool.to_string b) ]
20 | LitNull -> tag "LitNull" []
21
22let option_to_sexp mv ~f =
23 match mv with Some v -> tag "Some" [ f v ] | None -> Sexp.Atom "None"
24
25let mode_to_sexp mode =
26 Sexp.Atom (match mode with SHALLOW -> "SHALLOW" | DEEP -> "DEEP")
27
28let rec_to_sexp r = Sexp.Atom (match r with REC -> "REC" | NONREC -> "NONREC")
29
30let binop_to_sexp op =
31 Sexp.Atom
32 (match op with
33 | UpdateAttrOp -> "UpdateAttrOp"
34 | AddOp -> "AddOp"
35 | SubOp -> "SubOp"
36 | MulOp -> "MulOp"
37 | DivOp -> "DivOp"
38 | AndOp -> "AndOp"
39 | OrOp -> "OrOp"
40 | XOrOp -> "XOrOp"
41 | RoundOp Ceil -> "Ceil"
42 | RoundOp NearestEven -> "NearestEven"
43 | RoundOp Floor -> "Floor"
44 | LtOp -> "LtOp"
45 | EqOp -> "EqOp"
46 | HasAttrOp -> "HasAttrOp"
47 | SelectAttrOp -> "SelectAttrOp"
48 | DeleteAttrOp -> "DeleteAttrOp"
49 | SingletonAttrOp -> "SingletonAttrOp"
50 | TypeOfOp -> "TypeOfOp"
51 | AppendListOp -> "AppendListOp"
52 | MatchAttrOp -> "MatchAttrOp"
53 | MatchListOp -> "MatchListOp"
54 | MatchStringOp -> "MatchStringOp"
55 | FunctionArgsOp -> "FunctionArgsOp")
56
57let kind_to_sexp k = Sexp.Atom (match k with ABS -> "ABS" | WITH -> "WITH")
58
59let rec expr_to_sexp = function
60 | ELit l -> tag "ELit" [ lit_to_sexp l ]
61 | EId (x, None) -> tag "EId" [ Sexp.Atom (str x) ]
62 | EId (x, Some (k, e)) ->
63 tag "EId"
64 [ Sexp.Atom (str x); tag "alt" [ kind_to_sexp k; expr_to_sexp e ] ]
65 | EAbs (x, e) -> tag "EAbs" [ Sexp.Atom (str x); expr_to_sexp e ]
66 | EAbsMatch (ms, strict, e) ->
67 tag "EAbsMatch"
68 [
69 Sexp.Atom (if strict then "EXACT" else "LOOSE");
70 tag "formals"
71 (matcher_fold
72 (fun x me se ->
73 Sexp.List
74 [ Sexp.Atom (str x); option_to_sexp me ~f:expr_to_sexp ]
75 :: se)
76 [] ms);
77 expr_to_sexp e;
78 ]
79 | EApp (e1, e2) -> tag "EApp" [ expr_to_sexp e1; expr_to_sexp e2 ]
80 | ELetAttr (k, e1, e2) ->
81 tag "ELetAttr" [ kind_to_sexp k; expr_to_sexp e1; expr_to_sexp e2 ]
82 | ESeq (mode, e1, e2) ->
83 tag "ESeq" [ mode_to_sexp mode; expr_to_sexp e1; expr_to_sexp e2 ]
84 | EAttr bs ->
85 tag "EAttr"
86 (attr_set_fold
87 (fun x (Attr (r, e)) se ->
88 Sexp.List [ Sexp.Atom (str x); rec_to_sexp r; expr_to_sexp e ]
89 :: se)
90 [] bs)
91 | EList es ->
92 tag "EList"
93 (Internal.List.fold_right (fun e se -> expr_to_sexp e :: se) [] es)
94 | EBinOp (op, e1, e2) ->
95 tag "EBinOp" [ binop_to_sexp op; expr_to_sexp e1; expr_to_sexp e2 ]
96 | EIf (e1, e2, e3) ->
97 tag "EIf" [ expr_to_sexp e1; expr_to_sexp e2; expr_to_sexp e3 ]
98
99let rec val_to_sexp = function
100 | VLit l -> tag "VLit" [ lit_to_sexp l ]
101 | VClo _ -> tag "VClo" []
102 | VCloMatch _ -> tag "VCloMatch" []
103 | VAttr bs ->
104 tag "VAttr"
105 (Extraction.thunk_map_fold
106 (fun x t bs' ->
107 Sexp.List [ Sexp.Atom (str x); thunk_to_sexp t ] :: bs')
108 [] bs)
109 | VList ts ->
110 tag "VList"
111 (Internal.List.fold_right (fun t st -> thunk_to_sexp t :: st) [] ts)
112
113and env_to_sexp env =
114 tag "Env"
115 (Extraction.env_fold
116 (fun x (k, t) envs ->
117 Sexp.List
118 [
119 Sexp.Atom (str x);
120 Sexp.Atom
121 (match k with
122 | Extraction.ABS -> "ABS"
123 | Extraction.WITH -> "WITH");
124 thunk_to_sexp t;
125 ]
126 :: envs)
127 [] env)
128
129and thunk_to_sexp = function
130 | Thunk _ -> tag "Thunk" [ Sexp.Atom "DELAYED" ]
131 | Indirect _ -> tag "Thunk" [ Sexp.Atom "INDIRECT" ]
132 | Forced v -> tag "Thunk" [ Sexp.Atom "FORCED"; val_to_sexp v ]
133
134let expr_res_to_sexp = function
135 | NoFuel -> Sexp.Atom "NoFuel"
136 | Res e -> tag "Res" [ option_to_sexp e ~f:expr_to_sexp ]
137
138let val_res_to_sexp = function
139 | NoFuel -> Sexp.Atom "NoFuel"
140 | Res e -> tag "Res" [ option_to_sexp e ~f:val_to_sexp ]
141
142let rec (sexp_of_import_tree : Import.tree -> Sexp.t) = function
143 | { filename; deps = [] } -> Sexp.Atom filename
144 | { filename; deps } ->
145 Sexp.List [ Sexp.Atom filename; sexp_of_import_forest deps ]
146
147and sexp_of_import_forest forest =
148 Sexp.List (Sexp.Atom "deps" :: List.map forest ~f:sexp_of_import_tree)
149
150exception OfSexpError of string
151
152let rec import_tree_of_sexp : Sexp.t -> Import.tree = function
153 | Sexp.Atom filename -> { filename; deps = [] }
154 | Sexp.List [ Sexp.Atom filename; deps ] ->
155 { filename; deps = import_forest_of_sexp deps }
156 | _ -> raise (OfSexpError "Could not parse import tree")
157
158and import_forest_of_sexp = function
159 | Sexp.List (Sexp.Atom "deps" :: deps) -> List.map ~f:import_tree_of_sexp deps
160 | _ -> raise (OfSexpError "Could not parse import forest")
diff --git a/lib/nix/dune b/lib/nix/dune
new file mode 100644
index 0000000..3954c8a
--- /dev/null
+++ b/lib/nix/dune
@@ -0,0 +1,15 @@
1(menhir
2 (modules parser)
3 (flags "--dump" "--strict" "--external-tokens" "Tokens")
4 (infer true))
5
6(ocamllex
7 (modules lexer))
8
9(library
10 (name nix)
11 (preprocess
12 (pps ppx_sexp_conv))
13 (instrumentation
14 (backend bisect_ppx))
15 (libraries core core_unix core_unix.filename_unix pprint ppx_sexp_conv str))
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 @@
1open Core
2open 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
19exception ElaborateError of string
20
21type attr_set = recursivity * binding list
22
23let set_expr (r, bs) = Val (AttSet (r, bs))
24let get_id = function Id x -> x | _ -> assert false
25
26let 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
36let set_update_bnd (r, bs) x ~f = (r, update_bnd bs x ~f)
37
38let 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
47let 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 *)
66let 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
86let 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
91let 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
97let simplify_path = List.map ~f:simplify_path_component
98
99let 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
107let rec split_lines s =
108 match String.lsplit2 s ~on:'\n' with
109 | Some (s1, s2) -> s1 :: split_lines s2
110 | None -> [ s ]
111
112let rec concat_lines = function
113 | [] -> ""
114 | [ x ] -> x
115 | x :: xs -> x ^ "\n" ^ concat_lines xs
116
117let map_tail ~f = function [] -> [] | x :: xs -> x :: List.map ~f xs
118
119let 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
127let is_spaces l = String.(strip l ~drop:(Char.( = ) ' ') |> is_empty)
128
129let 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
134let 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
154and 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
178and 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
191and 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
196and process_pattern ~dir = function
197 | Alias x -> Alias x
198 | ParamSet (mx, (ps, k)) -> ParamSet (mx, (process_param_set ~dir mx ps, k))
199
200and 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)
diff --git a/lib/nix/lexer.mll b/lib/nix/lexer.mll
new file mode 100644
index 0000000..023d888
--- /dev/null
+++ b/lib/nix/lexer.mll
@@ -0,0 +1,315 @@
1{
2open Core
3open Tokens
4
5exception Error of string
6
7(* Types of curly braces.
8 AQUOTE corresponds to the braces for antiquotation, i.e. '${...}'
9 and SET to an attribute set '{...}'.
10 *)
11type braces =
12 | AQUOTE
13 | SET
14
15let print_stack s =
16 let b = Buffer.create 100 in
17 Buffer.add_string b "[ ";
18 List.iter s ~f:(function
19 | AQUOTE -> Buffer.add_string b "AQUOTE; "
20 | SET -> Buffer.add_string b "SET; "
21 );
22 Buffer.add_string b "]";
23 Buffer.contents b
24
25let token_of_str state buf =
26 match state with
27 | `Start -> STR_START (Buffer.contents buf)
28 | `Mid -> STR_MID (Buffer.contents buf)
29
30let token_of_istr state buf =
31 match state with
32 | `Start -> ISTR_START (Buffer.contents buf)
33 | `Mid -> ISTR_MID (Buffer.contents buf)
34
35(* lookup table for one-character tokens *)
36let char_table = Array.create ~len:94 EOF
37let _ =
38 List.iter ~f:(fun (k, v) -> Array.set char_table ((int_of_char k) - 1) v)
39 [
40 '.', SELECT;
41 '?', QMARK;
42 '!', NOT;
43 '=', ASSIGN;
44 '<', LT;
45 '>', GT;
46 '[', LBRACK;
47 ']', RBRACK;
48 '+', PLUS;
49 '-', MINUS;
50 '*', TIMES;
51 '/', SLASH;
52 '(', LPAREN;
53 ')', RPAREN;
54 ':', COLON;
55 ';', SEMICOLON;
56 ',', COMMA;
57 '@', AS
58 ]
59
60(* lookup table for two- and three-character tokens *)
61let str_table = Hashtbl.create (module String) ~size:10
62let _ =
63 List.iter ~f:(fun (kwd, tok) -> Hashtbl.set str_table ~key:kwd ~data:tok)
64 [
65 "//", MERGE;
66 "++", CONCAT;
67 "<=", LTE;
68 ">=", GTE;
69 "==", EQ;
70 "!=", NEQ;
71 "&&", AND;
72 "||", OR;
73 "->", IMPL;
74 "...", ELLIPSIS
75 ]
76
77(* lookup table for keywords *)
78let keyword_table = Hashtbl.create (module String) ~size:10
79let _ =
80 List.iter ~f:(fun (kwd, tok) -> Hashtbl.set keyword_table ~key:kwd ~data:tok)
81 [ "with", WITH;
82 "rec", REC;
83 "let", LET;
84 "in", IN;
85 "inherit", INHERIT;
86 "if" , IF;
87 "then", THEN;
88 "else", ELSE;
89 "assert", ASSERT;
90 "or", ORDEF ]
91
92(* replace an escape sequence by the corresponding character(s) *)
93let unescape = function
94 | "\\n" -> "\n"
95 | "\\r" -> "\r"
96 | "\\t" -> "\t"
97 | "\\\\" -> "\\"
98 | "\\${" -> "${"
99 | "''$" -> "$"
100 | "$$" -> "$"
101 | "'''" -> "''"
102 | "''\\t" -> "\t"
103 | "''\\r" -> "\r"
104 | "''\\n" -> "\n"
105 | x ->
106 failwith (Printf.sprintf "unescape unexpected arg %s" x)
107
108let collect_tokens lexer q lexbuf =
109 let stack = ref [] in
110 let queue = Stdlib.Queue.create () in
111 let rec go () =
112 match (try Some (Stdlib.Queue.take queue) with Stdlib.Queue.Empty -> None) with
113 | Some token ->
114 (
115 match token, !stack with
116 | AQUOTE_CLOSE, [] ->
117 Stdlib.Queue.add AQUOTE_CLOSE q
118 | EOF, _ ->
119 Stdlib.Queue.add EOF q;
120 | _, _ ->
121 Stdlib.Queue.add token q;
122 go ()
123 )
124 | None ->
125 lexer queue stack lexbuf;
126 go ()
127 in
128 Stdlib.Queue.add AQUOTE_OPEN q;
129 stack := [AQUOTE];
130 lexer queue stack lexbuf;
131 go ()
132
133(* utility functions *)
134let print_position lexbuf =
135 let pos = Lexing.lexeme_start_p lexbuf in
136 Printf.sprintf "%s:%d:%d" pos.pos_fname
137 pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1)
138
139
140let set_filename fname (lexbuf: Lexing.lexbuf) =
141 let pos = lexbuf.lex_curr_p in
142 lexbuf.lex_curr_p <- { pos with pos_fname = fname }; lexbuf
143
144}
145
146let nzdigit = ['1'-'9']
147let digit = nzdigit | '0'
148let float = (nzdigit digit* '.' digit* | '0'? '.' digit+) (['E' 'e'] ['+' '-']? digit+)?
149let alpha = ['a'-'z' 'A'-'Z']
150let alpha_digit = alpha | digit
151let path_chr = alpha_digit | ['.' '_' '-' '+']
152let path = path_chr* ('/' path_chr+)+
153let spath = alpha_digit path_chr* ('/' path_chr+)*
154let uri_chr = ['%' '/' '?' ':' '@' '&' '=' '+' '$' ',' '-' '_' '.' '!' '~' '*' '\'']
155let scheme = alpha (alpha | ['+' '-' '.'])*
156let uri = scheme ':' (alpha_digit | uri_chr)+
157let char_tokens = ['.' '?' '!' '=' '<' '>' '[' ']' '+' '-' '*' '/' '^' '(' ')' ':' ';' ',' '@']
158
159rule get_tokens q s = parse
160(* skip whitespeces *)
161| [' ' '\t' '\r']
162 { get_tokens q s lexbuf }
163(* increase line count for new lines *)
164| '\n'
165 { Lexing.new_line lexbuf; get_tokens q s lexbuf }
166| char_tokens as c
167 { Stdlib.Queue.add (Array.get char_table ((int_of_char c) - 1)) q }
168| ("//" | "++" | "<=" | ">=" | "==" | "!=" | "&&" | "||" | "->" | "...") as s
169 { Stdlib.Queue.add (Hashtbl.find_exn str_table s) q}
170| digit+ as i
171 { Stdlib.Queue.add (INT i) q }
172| float
173 { Stdlib.Queue.add (FLOAT (Lexing.lexeme lexbuf)) q }
174| path
175 { Stdlib.Queue.add (PATH (Lexing.lexeme lexbuf)) q }
176| '<' (spath as p) '>'
177 { Stdlib.Queue.add (SPATH p) q }
178| '~' path as p
179 { Stdlib.Queue.add (HPATH p) q }
180| uri
181 { Stdlib.Queue.add(URI (Lexing.lexeme lexbuf)) q }
182(* keywords or identifiers *)
183| ((alpha | '_')+ (alpha_digit | ['_' '\'' '-'])*) as id
184 { Stdlib.Queue.add (Hashtbl.find keyword_table id |> Option.value ~default:(ID id)) q}
185(* comments *)
186| '#' ([^ '\n']* as c)
187 { ignore c; get_tokens q s lexbuf}
188| "/*"
189 { comment (Buffer.create 64) lexbuf;
190 get_tokens q s lexbuf
191 }
192(* the following three tokens change the braces stack *)
193| "${"
194 { Stdlib.Queue.add AQUOTE_OPEN q; s := AQUOTE :: !s }
195| '{'
196 { Stdlib.Queue.add LBRACE q; s := SET :: !s }
197| '}'
198 {
199 match !s with
200 | AQUOTE :: rest ->
201 Stdlib.Queue.add AQUOTE_CLOSE q; s := rest
202 | SET :: rest ->
203 Stdlib.Queue.add RBRACE q; s := rest
204 | _ ->
205 let pos = print_position lexbuf in
206 let err = Printf.sprintf "Unbalanced '}' at %s\n" pos in
207 raise (Error err)
208 }
209(* a double-quoted string *)
210| '"'
211 { string `Start (Buffer.create 64) q lexbuf }
212(* an indented string *)
213| "''" (' '+ as ws)
214 { istring `Start (Some (String.length ws)) (Buffer.create 64) q lexbuf }
215| "''"
216 { istring `Start None (Buffer.create 64) q lexbuf }
217(* End of input *)
218| eof
219 { Stdlib.Queue.add EOF q }
220(* any other character raises an exception *)
221| _
222 {
223 let pos = print_position lexbuf in
224 let tok = Lexing.lexeme lexbuf in
225 let err = Printf.sprintf "Unexpected character '%s' at %s\n" tok pos in
226 raise (Error err)
227 }
228
229(* Nix does not allow nested comments, but it is still handy to lex it
230 separately because we can properly increase line count. *)
231and comment buf = parse
232 | '\n'
233 {Lexing.new_line lexbuf; Buffer.add_char buf '\n'; comment buf lexbuf}
234 | "*/"
235 { () }
236 | _ as c
237 { Buffer.add_char buf c; comment buf lexbuf }
238
239and string state buf q = parse
240 | '"' (* terminate when we hit '"' *)
241 { Stdlib.Queue.add (token_of_str state buf) q; Stdlib.Queue.add STR_END q }
242 | '\n'
243 { Lexing.new_line lexbuf; Buffer.add_char buf '\n'; string state buf q lexbuf }
244 | ("\\n" | "\\r" | "\\t" | "\\\\" | "\\${") as s
245 { Buffer.add_string buf (unescape s); string state buf q lexbuf }
246 | "\\" (_ as c) (* add the character verbatim *)
247 { Buffer.add_char buf c; string state buf q lexbuf }
248 | "${" (* collect all the tokens till we hit the matching '}' *)
249 {
250 Stdlib.Queue.add (token_of_str state buf) q;
251 collect_tokens get_tokens q lexbuf;
252 string `Mid (Buffer.create 64) q lexbuf
253 }
254 | _ as c (* otherwise just add the character to the buffer *)
255 { Buffer.add_char buf c; string state buf q lexbuf }
256
257and istring state imin buf q = parse
258 | ('\n' ' '* "''")
259 {
260 Lexing.new_line lexbuf;
261 Buffer.add_string buf "\n";
262 let indent = match imin with | None -> 0 | Some i -> i in
263 Stdlib.Queue.add (token_of_istr state buf) q;
264 Stdlib.Queue.add (ISTR_END indent) q
265 }
266 | "''"
267 {
268 let indent = match imin with | None -> 0 | Some i -> i in
269 Stdlib.Queue.add (token_of_istr state buf) q;
270 Stdlib.Queue.add (ISTR_END indent) q
271 }
272 | ('\n' ' '* '\n') as s
273 {
274 Lexing.new_line lexbuf;
275 Lexing.new_line lexbuf;
276 Buffer.add_string buf s;
277 istring state imin buf q lexbuf
278 }
279 | ('\n' (' '* as ws)) as s
280 {
281 Lexing.new_line lexbuf;
282 Buffer.add_string buf s;
283 let ws_count = String.length ws in
284 match imin with
285 | None ->
286 istring state (Some ws_count) buf q lexbuf
287 | Some i ->
288 istring state (Some (min i ws_count)) buf q lexbuf
289 }
290 | ("''$" | "'''" | "''\\t" | "''\\r" | "''\\n") as s
291 { Buffer.add_string buf (unescape s); istring state imin buf q lexbuf }
292 | "''\\" (_ as c)
293 { Buffer.add_char buf c; istring state imin buf q lexbuf }
294 | "${"
295 {
296 Stdlib.Queue.add (token_of_istr state buf) q;
297 collect_tokens get_tokens q lexbuf;
298 istring `Mid imin (Buffer.create 64) q lexbuf
299 }
300 | _ as c
301 { Buffer.add_char buf c; istring state imin buf q lexbuf }
302{
303
304let rec next_token
305 (q: token Stdlib.Queue.t)
306 (s: braces list ref)
307 (lexbuf: Lexing.lexbuf)
308 : token =
309 match (try Some (Stdlib.Queue.take q) with | Stdlib.Queue.Empty -> None) with
310 | Some token ->
311 token
312 | None ->
313 get_tokens q s lexbuf;
314 next_token q s lexbuf
315}
diff --git a/lib/nix/nix.ml b/lib/nix/nix.ml
new file mode 100644
index 0000000..39dc94c
--- /dev/null
+++ b/lib/nix/nix.ml
@@ -0,0 +1,20 @@
1open Core
2module Ast = Types
3module Printer = Printer
4
5exception ParseError of string
6
7let parse ~filename (data : string) =
8 let lexbuf = Lexer.set_filename filename (Lexing.from_string data)
9 and q, s = (Stdlib.Queue.create (), ref []) in
10 try Parser.main (Lexer.next_token q s) lexbuf with
11 | Lexer.Error msg ->
12 let msg' = String.rstrip msg in
13 raise (ParseError (sprintf "Lexing error: %s" msg'))
14 | Parser.Error ->
15 let msg = sprintf "Parse error at %s" (Lexer.print_position lexbuf) in
16 raise (ParseError msg)
17
18let elaborate = Elaborator.process
19
20exception ElaborateError = Elaborator.ElaborateError
diff --git a/lib/nix/parser.mly b/lib/nix/parser.mly
new file mode 100644
index 0000000..dc1638d
--- /dev/null
+++ b/lib/nix/parser.mly
@@ -0,0 +1,310 @@
1/* Tokens with data */
2%token <string> INT
3%token <string> FLOAT
4/* A path */
5%token <string> PATH
6/* Search path, enclosed in <> */
7%token <string> SPATH
8/* Home path, starts with ~ */
9%token <string> HPATH
10%token <string> URI
11%token <string> STR_START
12%token <string> STR_MID
13%token STR_END
14%token <string> ISTR_START
15%token <string> ISTR_MID
16%token <int> ISTR_END
17%token <string> ID
18/* Tokens that stand for themselves */
19%token SELECT "."
20%token QMARK "?"
21%token CONCAT "++"
22%token NOT "!"
23%token MERGE "//"
24%token ASSIGN "="
25%token LT "<"
26%token LTE "<="
27%token GT ">"
28%token GTE ">="
29%token EQ "=="
30%token NEQ "!="
31%token AND "&&"
32%token OR "||"
33%token IMPL "->"
34%token AQUOTE_OPEN "${"
35%token AQUOTE_CLOSE "}$"
36%token LBRACE "{"
37%token RBRACE "}"
38%token LBRACK "["
39%token RBRACK "]"
40%token PLUS "+"
41%token MINUS "-"
42%token TIMES "*"
43%token SLASH "/"
44%token LPAREN "("
45%token RPAREN ")"
46%token COLON ":"
47%token SEMICOLON ";"
48%token COMMA ","
49%token ELLIPSIS "..."
50%token AS "@"
51/* Keywords */
52%token WITH "with"
53%token REC "rec"
54%token LET "let"
55%token IN "in"
56%token INHERIT "inherit"
57%token IF "if"
58%token THEN "then"
59%token ELSE "else"
60%token ASSERT "assert"
61%token ORDEF "or"
62
63/* End of input */
64%token EOF
65
66%{
67 open Types
68%}
69
70%start <Types.expr> main
71
72%%
73
74main:
75| e = expr0 EOF
76 { e }
77
78expr0:
79| "if"; e1 = expr0; "then"; e2 = expr0; "else"; e3 = expr0
80 { Cond (e1, e2, e3) }
81| "with"; e1 = expr0; ";"; e2 = expr0
82 { With (e1, e2) }
83| "assert"; e1 = expr0; ";"; e2 = expr0
84 { Assert (e1, e2) }
85| "let"; xs = delimited("{", list(binding), "}")
86 { SetLet xs }
87| "let"; xs = list(binding); "in"; e = expr0
88 { Let (xs, e) }
89| l = lambda
90 { Val l }
91| e = expr1
92 { e }
93
94/* Rules expr1-expr14 are almost direct translation of the operator
95 precedence table:
96 https://nixos.org/nix/manual/#sec-language-operators */
97
98%inline binary_expr(Lhs, Op, Rhs):
99| lhs = Lhs; op = Op; rhs = Rhs
100 { BinaryOp (op, lhs, rhs) }
101
102expr1:
103| e = binary_expr(expr2, "->" {Impl}, expr1)
104| e = expr2
105 { e }
106
107expr2:
108| e = binary_expr(expr2, "||" {Or}, expr3)
109| e = expr3
110 { e }
111
112expr3:
113| e = binary_expr(expr3, "&&" {And}, expr4)
114| e = expr4
115 { e }
116
117%inline expr4_ops:
118| "==" { Eq }
119| "!=" { Neq }
120
121expr4:
122| e = binary_expr(expr5, expr4_ops, expr5)
123| e = expr5
124 { e }
125
126%inline expr5_ops:
127| "<" { Lt }
128| ">" { Gt }
129| "<=" { Lte }
130| ">=" { Gte }
131
132expr5:
133| e = binary_expr(expr6, expr5_ops, expr6)
134| e = expr6
135 { e }
136
137expr6:
138| e = binary_expr(expr7, "//" {Merge}, expr6)
139| e = expr7
140 { e }
141
142expr7:
143| e = preceded("!", expr7)
144 { UnaryOp (Not, e) }
145| e = expr8
146 { e }
147
148%inline expr8_ops:
149| "+" { Plus }
150| "-" { Minus }
151
152expr8:
153| e = binary_expr(expr8, expr8_ops, expr9)
154| e = expr9
155 { e }
156
157%inline expr9_ops:
158| "*" { Mult }
159| "/" { Div }
160
161expr9:
162| e = binary_expr(expr9, expr9_ops, expr10)
163| e = expr10
164 { e }
165
166expr10:
167| e = binary_expr(expr11, "++" {Concat}, expr10)
168| e = expr11
169 { e }
170
171expr11:
172| e = expr12 "?" p = attr_path
173 { Test (e, p) }
174| e = expr12
175 { e }
176
177expr12:
178| e = preceded("-", expr13)
179 { UnaryOp (Negate, e) }
180| e = expr13
181 { e }
182
183expr13:
184| f = expr13; arg = expr14
185 { Apply (f, arg) }
186| e = expr14
187 { e }
188
189%inline selectable:
190| s = set
191 { Val s }
192| id = ID
193 { Id id }
194| e = delimited("(", expr0, ")")
195 { e }
196
197expr14:
198| e = selectable; "."; p = attr_path; o = option(preceded("or", expr14))
199 { Select (e, p, o) }
200| e = atomic_expr; "or"
201 { Apply (e, Id "or") }
202| e = atomic_expr
203 { e }
204
205atomic_expr:
206| id = ID
207 { Id id }
208| v = value
209 { Val v }
210| e = delimited("(", expr0, ")")
211 { e }
212
213attr_path:
214| p = separated_nonempty_list(".", attr_path_component)
215 { p }
216
217attr_path_component:
218| "or"
219 { Id "or" }
220| id = ID
221 { Id id }
222| e = delimited("${", expr0, "}$")
223 { Aquote e }
224| s = str
225 { Val s }
226
227value:
228| s = str
229 { s }
230| s = istr
231 { s }
232| i = INT
233 {Int i}
234| f = FLOAT
235 { Float f }
236| p = PATH
237 { Path p }
238| sp = SPATH
239 { SPath sp }
240| hp = HPATH
241 { HPath hp }
242| uri = URI
243 { Uri uri }
244| l = nixlist
245 { l }
246| s = set
247 { s }
248
249%inline str_mid(X):
250| xs = list(pair(delimited("${", expr0, "}$"), X)) { xs }
251
252/* Double-quoted string */
253str:
254| start = STR_START; mids = str_mid(STR_MID); STR_END
255 { Str (start, mids) }
256
257/* Indented string */
258istr:
259| start = ISTR_START; mids = str_mid(ISTR_MID); i = ISTR_END
260 { IStr (i, start, mids) }
261
262/* Lists and sets */
263nixlist:
264| xs = delimited("[", list(expr14), "]")
265 { List xs }
266
267empty_set:
268| "{"; "}" {}
269
270set:
271| empty_set
272 { AttSet (Nonrec, []) }
273| xs = delimited("{", nonempty_list(binding), "}")
274 { AttSet (Nonrec, xs) }
275| xs = preceded("rec", delimited("{", list(binding), "}"))
276 { AttSet (Rec, xs) }
277
278binding:
279| kv = terminated(separated_pair(attr_path, "=", expr0), ";")
280 { let (k, v) = kv in AttrPath (k, v) }
281| xs = delimited("inherit", pair(option(delimited("(", expr0, ")")), list(attr_path_component)), ";")
282 { let (prefix, ids) = xs in Inherit (prefix, ids) }
283
284lambda:
285| id = ID; "@"; p = param_set; ":"; e = expr0
286 { Lambda (ParamSet (Some id, p), e) }
287| p = param_set; "@"; id = ID; ":"; e = expr0
288 { Lambda (ParamSet (Some id, p), e) }
289| p = param_set; ":"; e = expr0
290 { Lambda (ParamSet (None, p), e) }
291| id = ID; ":"; e = expr0
292 { Lambda (Alias id, e) }
293
294%inline param_set:
295| empty_set
296 { ([], Exact) }
297| "{"; "..."; "}"
298 { ([], Loose) }
299| ps = delimited("{", pair(pair(params, ","?), boption("...")), "}")
300 { let ((ps, _), ellipsis) = ps in (ps, if ellipsis then Loose else Exact) }
301
302params:
303| p = param
304 { [p] }
305| ps = params; ","; p = param
306 { ps @ [p] }
307
308%inline param:
309p = pair(ID, option(preceded("?", expr0)))
310 { p }
diff --git a/lib/nix/printer.ml b/lib/nix/printer.ml
new file mode 100644
index 0000000..57e81f4
--- /dev/null
+++ b/lib/nix/printer.ml
@@ -0,0 +1,176 @@
1open Core
2open Types
3open PPrint
4
5let rec escape_chlist = function
6 | [] -> []
7 | '$' :: '{' :: l' -> '\\' :: '$' :: '{' :: escape_chlist l'
8 | '\n' :: l' -> '\\' :: 'n' :: escape_chlist l'
9 | '\r' :: l' -> '\\' :: 'r' :: escape_chlist l'
10 | '\t' :: l' -> '\\' :: 't' :: escape_chlist l'
11 | '\\' :: l' -> '\\' :: '\\' :: escape_chlist l'
12 | '"' :: l' -> '\\' :: '"' :: escape_chlist l'
13 | c :: l' -> c :: escape_chlist l'
14
15let escape_string s = s |> String.to_list |> escape_chlist |> String.of_list
16let out_width = ref 80
17let set_width i = out_width := i
18let indent = ref 2
19let set_indent i = indent := i
20
21let rec doc_of_expr = function
22 | BinaryOp (op, lhs, rhs) ->
23 let lhs_doc = maybe_parens_bop op `Left lhs
24 and rhs_doc = maybe_parens_bop op `Right rhs in
25 infix !indent 1 (doc_of_bop op) lhs_doc rhs_doc
26 | UnaryOp (op, e) -> precede (doc_of_uop op) (maybe_parens (prec_of_uop op) e)
27 | Cond (e1, e2, e3) ->
28 surround !indent 1
29 (soft_surround !indent 1 (string "if") (doc_of_expr e1) (string "then"))
30 (doc_of_expr e2)
31 (string "else" ^^ nest !indent (break 1 ^^ doc_of_expr e3))
32 | With (e1, e2) ->
33 flow (break 1) [ string "with"; doc_of_expr e1 ^^ semi; doc_of_expr e2 ]
34 | Assert (e1, e2) ->
35 flow (break 1) [ string "assert"; doc_of_expr e1 ^^ semi; doc_of_expr e2 ]
36 | Test (e, path) ->
37 maybe_parens 4 e ^^ space ^^ string "?"
38 ^^ group (break 1 ^^ separate_map dot doc_of_expr path)
39 | SetLet bs ->
40 surround !indent 1
41 (string "let " ^^ lbrace)
42 (group (separate_map (break 1) doc_of_binding bs))
43 rbrace
44 | Let (bs, e) ->
45 surround !indent 1 (string "let")
46 (separate_map (break 1) doc_of_binding bs)
47 (prefix !indent 1 (string "in") (doc_of_expr e))
48 | Val v -> doc_of_val v
49 | Id id -> string id
50 | Select (e, path, oe) ->
51 maybe_parens 1 e ^^ dot ^^ doc_of_attpath path
52 ^^ optional
53 (fun e ->
54 space ^^ string "or" ^^ nest !indent (break 1 ^^ maybe_parens 1 e))
55 oe
56 | Apply (e1, e2) -> prefix !indent 1 (maybe_parens 2 e1) (maybe_parens 2 e2)
57 | Aquote e -> surround !indent 0 (string "${") (doc_of_expr e) (string "}")
58
59and maybe_parens lvl e =
60 if prec_of_expr e >= lvl then surround !indent 0 lparen (doc_of_expr e) rparen
61 else doc_of_expr e
62
63and maybe_parens_bop op (loc : [ `Left | `Right ]) e =
64 match (loc, assoc_of_bop op) with
65 | (`Left, Some Left | `Right, Some Right)
66 when prec_of_expr e >= prec_of_bop op ->
67 doc_of_expr e
68 | _, _ -> maybe_parens (prec_of_bop op) e
69
70and doc_of_attpath path = separate_map dot doc_of_expr path
71
72and doc_of_paramset (params, kind) =
73 let ps =
74 List.map ~f:doc_of_param params
75 @ if Poly.(kind = Loose) then [ string "..." ] else []
76 in
77 surround !indent 0 lbrace (separate (comma ^^ break 1) ps) rbrace
78
79and doc_of_param (id, oe) =
80 string id ^^ optional (fun e -> qmark ^^ space ^^ doc_of_expr e) oe
81
82and doc_of_binding = function
83 | AttrPath (path, e) ->
84 doc_of_attpath path ^^ space ^^ equals ^^ space ^^ doc_of_expr e ^^ semi
85 | Inherit (oe, ids) ->
86 let id_docs =
87 List.map
88 ~f:(function
89 | Id x | Val (Str (x, [])) -> string x | _ -> assert false)
90 ids
91 in
92 let xs =
93 flow (break 1)
94 (match oe with
95 | Some e -> parens (doc_of_expr e) :: id_docs
96 | None -> id_docs)
97 in
98 soft_surround !indent 0 (string "inherit" ^^ space) xs semi
99
100and doc_of_bop = function
101 | Plus -> plus
102 | Minus -> minus
103 | Mult -> star
104 | Div -> slash
105 | Gt -> rangle
106 | Lt -> langle
107 | Lte -> string "<="
108 | Gte -> string ">="
109 | Eq -> string "=="
110 | Neq -> string "!="
111 | Or -> string "||"
112 | And -> string "&&"
113 | Impl -> string "->"
114 | Merge -> string "//"
115 | Concat -> string "++"
116
117and doc_of_uop = function Negate -> minus | Not -> bang
118
119and doc_of_val = function
120 | Str (start, xs) ->
121 dquotes
122 (string (escape_string start)
123 ^^ concat
124 (List.map
125 ~f:(fun (e, s) ->
126 surround !indent 0 (string "${") (doc_of_expr e)
127 (string "}" ^^ string (escape_string s)))
128 xs))
129 | IStr (i, start, xs) ->
130 let qq = string "''" in
131 let str s =
132 String.split ~on:'\n' s
133 |> List.map ~f:(fun s ->
134 let len = String.length s in
135 let s' =
136 if len >= i then String.sub s ~pos:i ~len:(len - i) else s
137 in
138 string s')
139 |> separate hardline
140 in
141 enclose qq qq
142 (str start
143 ^^ concat
144 (List.map
145 ~f:(fun (e, s) ->
146 enclose (string "${") rbrace (doc_of_expr e) ^^ str s)
147 xs))
148 | Int x | Float x | Path x | SPath x | HPath x | Uri x -> string x
149 | Lambda (pattern, body) ->
150 let pat =
151 match pattern with
152 | Alias id -> string id
153 | ParamSet (None, ps) -> doc_of_paramset ps
154 | ParamSet (Some id, ps) ->
155 doc_of_paramset ps ^^ group (break 1 ^^ at ^^ break 1 ^^ string id)
156 in
157 flow (break 1) [ pat ^^ colon; doc_of_expr body ]
158 | List [] -> lbracket ^^ space ^^ rbracket
159 | List es ->
160 surround !indent 1 lbracket
161 (separate_map (break 1) (maybe_parens 2) es)
162 rbracket
163 | AttSet (Nonrec, []) -> lbrace ^^ space ^^ rbrace
164 | AttSet (Nonrec, bs) ->
165 surround !indent 1 lbrace
166 (group (separate_map (break 1) doc_of_binding bs))
167 rbrace
168 | AttSet (Rec, bs) ->
169 string "rec" ^^ space ^^ doc_of_val (AttSet (Nonrec, bs))
170
171let print chan expr = ToChannel.pretty 0.7 !out_width chan (doc_of_expr expr)
172
173let to_string expr =
174 let buf = Stdlib.Buffer.create 0 in
175 ToBuffer.pretty 0.7 !out_width buf (doc_of_expr expr);
176 Stdlib.Buffer.contents buf
diff --git a/lib/nix/tokens.ml b/lib/nix/tokens.ml
new file mode 100644
index 0000000..4891d48
--- /dev/null
+++ b/lib/nix/tokens.ml
@@ -0,0 +1,64 @@
1type token =
2 (* Tokens with data *)
3 | INT of string
4 | FLOAT of string
5 (* A path (starting with / or ./) *)
6 | PATH of string
7 (* Search path, enclosed in < and > *)
8 | SPATH of string
9 (* Home path, starting with ~/ *)
10 | HPATH of string
11 | URI of string
12 | STR_START of string
13 | STR_MID of string
14 | STR_END
15 | ISTR_START of string
16 | ISTR_MID of string
17 | ISTR_END of int
18 | ID of string
19 (* Tokens that stand for themselves *)
20 | SELECT
21 | QMARK
22 | CONCAT
23 | NOT
24 | MERGE
25 | ASSIGN
26 | LT
27 | LTE
28 | GT
29 | GTE
30 | EQ
31 | NEQ
32 | AND
33 | OR
34 | IMPL
35 | AQUOTE_OPEN
36 | AQUOTE_CLOSE
37 | LBRACE
38 | RBRACE
39 | LBRACK
40 | RBRACK
41 | PLUS
42 | MINUS
43 | TIMES
44 | SLASH
45 | LPAREN
46 | RPAREN
47 | COLON
48 | SEMICOLON
49 | COMMA
50 | ELLIPSIS
51 | AS
52 (* Keywords *)
53 | WITH
54 | REC
55 | LET
56 | IN
57 | INHERIT
58 | IF
59 | THEN
60 | ELSE
61 | ASSERT
62 | ORDEF
63 (* End of input *)
64 | EOF
diff --git a/lib/nix/types.ml b/lib/nix/types.ml
new file mode 100644
index 0000000..8245406
--- /dev/null
+++ b/lib/nix/types.ml
@@ -0,0 +1,112 @@
1open Core
2
3(* Binary operators *)
4type binary_op =
5 | Plus
6 | Minus
7 | Mult
8 | Div
9 | Gt
10 | Lt
11 | Lte
12 | Gte
13 | Eq
14 | Neq
15 | Or
16 | And
17 | Impl
18 | Merge
19 | Concat
20[@@deriving sexp_of]
21
22(* Unary operators *)
23type unary_op = Negate | Not [@@deriving sexp_of]
24
25(* The top-level expression type *)
26type expr =
27 | BinaryOp of binary_op * expr * expr
28 | UnaryOp of unary_op * expr
29 | Cond of expr * expr * expr
30 | With of expr * expr
31 | Assert of expr * expr
32 | Test of expr * expr list
33 | SetLet of binding list
34 | Let of binding list * expr
35 | Val of value
36 | Id of id
37 | Select of expr * expr list * expr option
38 | Apply of expr * expr
39 | Aquote of expr
40[@@deriving sexp_of]
41
42(* Possible values *)
43and value =
44 (* Str is a string start, followed by arbitrary number of antiquotations and
45 strings that separate them *)
46 | Str of string * (expr * string) list
47 (* IStr is an indented string, so it has the extra integer component which
48 indicates the indentation *)
49 | IStr of int * string * (expr * string) list
50 | Int of string
51 | Float of string
52 | Path of string
53 | SPath of string
54 | HPath of string
55 | Uri of string
56 | Lambda of pattern * expr
57 | List of expr list
58 | AttSet of recursivity * binding list
59[@@deriving sexp_of]
60
61(* Patterns in lambda definitions *)
62and pattern = Alias of id | ParamSet of id option * param_set
63[@@deriving sexp_of]
64
65and param_set = param list * match_kind [@@deriving sexp_of]
66and param = id * expr option [@@deriving sexp_of]
67and recursivity = Rec | Nonrec
68and match_kind = Exact | Loose
69
70(* Bindings in attribute sets and let expressions *)
71and binding =
72 (* The first expr should be attrpath, which is the same as in Select *)
73 | AttrPath of expr list * expr
74 | Inherit of expr option * expr list
75[@@deriving sexp_of]
76
77(* Identifiers *)
78and id = string
79
80(* Precedence levels of binary operators *)
81let prec_of_bop = function
82 | Concat -> 5
83 | Mult | Div -> 6
84 | Plus | Minus -> 7
85 | Merge -> 9
86 | Gt | Lt | Lte | Gte -> 10
87 | Eq | Neq -> 11
88 | And -> 12
89 | Or -> 13
90 | Impl -> 14
91
92type assoc = Left | Right
93
94let assoc_of_bop = function
95 | Mult | Div | Plus | Minus -> Some Left
96 | Concat | Merge | And | Or -> Some Right
97 | Gt | Lt | Lte | Gte | Eq | Neq | Impl -> None
98
99(* Precedence levels of unary operators *)
100let prec_of_uop = function Negate -> 3 | Not -> 8
101
102(* Precedence level of expressions
103 (assuming that the constituents have higher levels) *)
104let prec_of_expr = function
105 | Val (Lambda _) -> 15
106 | Val _ | Id _ | Aquote _ -> 0
107 | BinaryOp (op, _, _) -> prec_of_bop op
108 | UnaryOp (op, _) -> prec_of_uop op
109 | Cond _ | With _ | Assert _ | Let _ | SetLet _ -> 15
110 | Test _ -> 4
111 | Select _ -> 1
112 | Apply _ -> 2
generated by cgit v1.2.3 (git 2.49.0) at 2025-10-13 20:42:43 +0000