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/extraction/dune | 56 ++++++++ lib/extraction/extraction.ml | 18 +++ lib/extraction/prelude.v | 52 +++++++ lib/mininix/builtins.ml | 77 +++++++++++ lib/mininix/builtins.nix | 302 +++++++++++++++++++++++++++++++++++++++++ lib/mininix/conv.ml | 96 +++++++++++++ lib/mininix/dune | 15 +++ lib/mininix/import.ml | 54 ++++++++ lib/mininix/mininix.ml | 13 ++ lib/mininix/mininix2nix.ml | 54 ++++++++ lib/mininix/nix2mininix.ml | 254 ++++++++++++++++++++++++++++++++++ lib/mininix/run.ml | 17 +++ lib/mininix/sexp.ml | 160 ++++++++++++++++++++++ lib/nix/dune | 15 +++ lib/nix/elaborator.ml | 208 ++++++++++++++++++++++++++++ lib/nix/lexer.mll | 315 +++++++++++++++++++++++++++++++++++++++++++ lib/nix/nix.ml | 20 +++ lib/nix/parser.mly | 310 ++++++++++++++++++++++++++++++++++++++++++ lib/nix/printer.ml | 176 ++++++++++++++++++++++++ lib/nix/tokens.ml | 64 +++++++++ lib/nix/types.ml | 112 +++++++++++++++ 21 files changed, 2388 insertions(+) create mode 100644 lib/extraction/dune create mode 100644 lib/extraction/extraction.ml create mode 100644 lib/extraction/prelude.v create mode 100644 lib/mininix/builtins.ml create mode 100644 lib/mininix/builtins.nix create mode 100644 lib/mininix/conv.ml create mode 100644 lib/mininix/dune create mode 100644 lib/mininix/import.ml create mode 100644 lib/mininix/mininix.ml create mode 100644 lib/mininix/mininix2nix.ml create mode 100644 lib/mininix/nix2mininix.ml create mode 100644 lib/mininix/run.ml create mode 100644 lib/mininix/sexp.ml create mode 100644 lib/nix/dune create mode 100644 lib/nix/elaborator.ml create mode 100644 lib/nix/lexer.mll create mode 100644 lib/nix/nix.ml create mode 100644 lib/nix/parser.mly create mode 100644 lib/nix/printer.ml create mode 100644 lib/nix/tokens.ml create mode 100644 lib/nix/types.ml (limited to 'lib') 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 @@ +(coq.extraction + (prelude prelude) + (extracted_modules + Ascii + BinInt + Bits + Decimal + prelude + gmap + Nat + PeanoNat + SpecFloat + ZArith_dec + base + BinNat + Bool + DecimalString + interp + numbers + pretty + Specif + Zbool + Basics + BinNums + countable + list0 + operational + res + String + Zpower + Binary + BinPosDef + Datatypes + fin_maps + List + option + Round + strings + BinarySingleNaN + BinPos + decidable + floats + mapset + orders + sorting + utils) + (flags + (-output-directory ".")) + (theories Flocq stdpp mininix)) + +(library + (name extraction) + (flags + (:standard -w -33)) + (instrumentation + (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 @@ +include Prelude +include Interp +include Operational +include Res + +(* Stuff that's not part of the paper. Still exposed because we sometimes want + to be able to create a natural number, float, process a list etc. *) +module Internal = struct + module BinNums = BinNums + module Datatypes = Datatypes + module List = List + + module Floats = struct + include Floats + include Binary + include SpecFloat + end +end 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 @@ +Require Import Coq.Numbers.DecimalString ExtrOcamlBasic ExtrOcamlString. +From stdpp Require Import strings stringmap gmap. +From mininix Require Import nix.interp. + +Definition attr_set_insert (x : string) (α : attr) (αs : gmap string attr) : gmap string attr := + <[x:=α]> αs. + +Definition attr_set_contains (x : string) (αs : gmap string attr) : bool := + bool_decide (x ∈ dom αs). + +Definition attr_set_fold {A} (f : string → attr → A → A) (init : A) (αs : gmap string attr) : A := + map_fold f init αs. + +Definition attr_set_empty : gmap string attr := ∅. + +Definition env_fold {A} (f : string → (kind * thunk) → A → A) (init : A) (E : env) : A := + map_fold f init E. + +Definition env_insert_abs (x : string) (t : thunk) (E : env) : env := + <[x:=(ABS,t)]> E. + +Definition thunk_map_fold {A} (f : string → thunk → A → A) (init : A) (bs : gmap string thunk) : A := + map_fold f init bs. + +Definition thunk_map_insert (x : string) (t : thunk) (bs : gmap string thunk) : gmap string thunk := + <[x:=t]> bs. + +Definition thunk_map_empty : gmap string thunk := ∅. + +Definition matcher := gmap string (option expr). + +Definition matcher_empty : matcher := ∅. + +Definition matcher_insert (x : string) (me : option expr) (ms : matcher) : matcher := + <[x:=me]> ms. + +Definition matcher_fold {A} (f : string → option expr → A → A) (init : A) (ms : matcher) : A := + map_fold f init ms. + +Definition env_empty : env := ∅. + +Definition string_of_Z (x : Z) : string := + NilZero.string_of_int (Z.to_int x). + +Definition string_to_Z (s : string) : option Z := + Z.of_int <$> NilZero.int_of_string s. + +Separate Extraction + attr_set_insert env_insert_abs matcher_insert thunk_map_insert + attr_set_contains attr_set_fold env_fold matcher_fold thunk_map_fold + env_empty attr_set_empty matcher_empty thunk_map_empty string_of_Z + 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 @@ +open Core +open Nix2mininix + +let minimal_prelude = + mn_attr + [ + ("true", `Nonrec, Extraction.ELit (Extraction.LitBool true)); + ("false", `Nonrec, Extraction.ELit (Extraction.LitBool false)); + ("null", `Nonrec, Extraction.ELit Extraction.LitNull); + ("seq", `Nonrec, mn_abs [ "e1"; "e2" ] (mn_seq (mn_id "e1") (mn_id "e2"))); + ( "deepSeq", + `Nonrec, + mn_abs [ "e1"; "e2" ] (mn_deep_seq (mn_id "e1") (mn_id "e2")) ); + ("typeOf", `Nonrec, mn_abs [ "e" ] (mn_type_of (mn_id "e"))); + ("functionArgs", `Nonrec, mn_abs [ "f" ] (mn_function_args (mn_id "f"))); + ( "bitAnd", + `Nonrec, + mn_abs [ "x"; "y" ] (mn_bit_and (mn_id "x") (mn_id "y")) ); + ("bitOr", `Nonrec, mn_abs [ "x"; "y" ] (mn_bit_or (mn_id "x") (mn_id "y"))); + ( "bitXor", + `Nonrec, + mn_abs [ "x"; "y" ] (mn_bit_xor (mn_id "x") (mn_id "y")) ); + ("ceil", `Nonrec, mn_abs [ "x" ] (mn_ceil (mn_id "x"))); + ("floor", `Nonrec, mn_abs [ "x" ] (mn_floor (mn_id "x"))); + ("__mn_nearestEven", `Nonrec, mn_abs [ "x" ] (mn_nearest_even (mn_id "x"))); + ( "__mn_singleton", + `Nonrec, + mn_abs [ "x"; "e" ] (mn_singleton_attr (mn_id "x") (mn_id "e")) ); + ( "__mn_attr_delete", + `Nonrec, + mn_abs [ "as"; "x" ] (mn_delete_attr (mn_id "as") (mn_id "x")) ); + ( "__mn_attr_has_prim", + `Nonrec, + mn_abs [ "d"; "e" ] (mn_has_attr (mn_id "d") (mn_id "e")) ); + ("__mn_attr_match", `Nonrec, mn_abs [ "as" ] (mn_attr_match (mn_id "as"))); + ("__mn_list_match", `Nonrec, mn_abs [ "xs" ] (mn_list_match (mn_id "xs"))); + ( "__mn_string_match", + `Nonrec, + mn_abs [ "s" ] (mn_string_match (mn_id "s")) ); + ] + +(* Watch out to not introduce constructs here that refer to themselves using + the mnbi_* functions in Nix2mininix - this can cause undesired loops. *) +let builtins_nix = + Nix.elaborate (Nix.parse ~filename:"" [%blob "builtins.nix"]) + +let builtins = + Extraction.ELetAttr + (Extraction.ABS, minimal_prelude, Nix2mininix.from_nix builtins_nix) + +let exported_builtins = + [ + "__mn_assert"; + "__mn_attr_has"; + "__mn_attr_insertNew"; + "__mn_attr_select"; + "__mn_attr_selectOr"; + "abort"; + "false"; + "head"; + "map"; + "null"; + "removeAttrs"; + "tail"; + "throw"; + "toString"; + "true"; + ] + +let apply_prelude e = + let bindings = + mn_attr + (("builtins", `Nonrec, builtins) + :: List.map exported_builtins ~f:(fun x -> + (x, `Rec, mn_select_attr (mn_id "builtins") (mn_str x)))) + in + 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 @@ +rec { + inherit true false null functionArgs typeOf seq deepSeq bitAnd bitOr bitXor floor ceil; # from the minimal prelude + + abort = _: null null; # we ignore the provided message + throw = abort; # same here + + head = xs: (__mn_list_match xs).head; + tail = xs: (__mn_list_match xs).tail; + + __mn_matchAttr = f: as: f (__mn_attr_match as); + __mn_matchList = f: xs: f (__mn_list_match xs); + __mn_matchString = f: s: f (__mn_string_match s); + + __mn_foldr = op: nul: + __mn_matchList ({ head, tail, empty }: + if empty then nul else op head (__mn_foldr op nul tail)); + + # foldl' should really be strict. But if we do that (using seq), the + # complexity of this function suddenly morphs from linear to + # exponential, which is way worse than not actually being strict. + foldl' = op: nul: + __mn_matchList + ({ head, tail, empty }: + if empty then nul else + let v = op nul head; in + seq v (foldl' op v tail)); + map = f: + __mn_matchList ({ head, tail, empty }: + if empty then [ ] else [ (f head) ] ++ map f tail); + elem = x: any (y: x == y); + elemAt = xs: n: assert n >= 0; + let go = xs: n: if n == 0 then head xs else go (tail xs) (n - 1); + in go xs n; + length = __mn_matchList ({ head, tail, empty }: + if empty then 0 else 1 + length tail); + sort = __mn_mergesort; + any = f: __mn_matchList ({ head, tail, empty }: !empty && (f head || any f tail)); + all = f: __mn_matchList ({ head, tail, empty }: !empty -> (f head && all f tail)); + concatLists = + __mn_matchList ({ head, tail, empty }: + if empty then [ ] else head ++ concatLists tail); + concatMap = f: xss: concatLists (map f xss); + concatStringsSep = sep: + __mn_matchList ({ head, tail, empty }: + if empty then "" else if tail == [ ] then head + else head + sep + concatStringsSep sep tail); + filter = f: + __mn_matchList ({ head, tail, empty }: + if empty then [ ] else (if f head then [ head ] else [ ]) ++ filter f tail); + groupBy = f: xs: + let update = x: acc: acc // { ${f x} = [ x ] ++ (acc.${f x} or [ ]); }; + in __mn_foldr update { } xs; + partition = f: groupBy (x: if f x then "right" else "wrong"); + + hasAttr = x: as: as ? ${x}; + getAttr = x: as: as.${x}; + attrNames = __mn_matchAttr ({ key, tail, empty, ... }: + if empty then [ ] else [ key ] ++ attrNames tail); + attrValues = __mn_matchAttr ({ head, tail, empty, ... }: + if empty then [ ] else [ head ] ++ attrValues tail); + mapAttrs = f: __mn_matchAttr ({ key, head, tail, empty }: + if empty then { } else + mapAttrs f tail // { ${key} = f key head; }); + removeAttrs = __mn_foldr (x: as': __mn_attr_delete as' x); + zipAttrsWith = f: ass: mapAttrs f (__mn_zipAttrs ass); + catAttrs = x: + __mn_matchList ({ head, tail, empty }: + if empty then [ ] + else (if head ? ${x} then [ head.${x} ] else [ ]) ++ catAttrs x tail); + listToAttrs = + __mn_foldr (attr: as': as' // { ${attr.name} = attr.value; }) { }; + intersectAttrs = e1: e2: + __mn_matchAttr + ({ key, head, tail, empty }: + if empty then { } else + (if e2 ? ${key} then { ${key} = e2.${key}; } else { }) // + intersectAttrs tail (__mn_attr_delete e2 key)) + e1; + + lessThan = x: y: x < y; # documentation is misleading, not only for numbers + add = x: y: x + y; + mul = x: y: x * y; + div = x: y: x / y; + sub = x: y: x - y; + genList = gen: n: + let + aux = off: if off >= n then [ ] else + [ (gen off) ] ++ aux (off + 1); + in + aux 0; + + __mn_genericClosure = { operator, seen, startSet }: + __mn_matchList + ({ head, tail, empty }: + if empty then [ ] else + if seen head.key + then __mn_genericClosure { inherit operator seen; startSet = tail; } + else [ head ] ++ __mn_genericClosure { + inherit operator; + seen = k: k == head.key || seen k; + startSet = tail ++ operator head; + }) + startSet; + genericClosure = { operator, startSet }: + __mn_genericClosure { inherit operator startSet; seen = _: false; }; + + isAttrs = e: typeOf e == "set"; + isBool = e: typeOf e == "bool"; + isFloat = e: typeOf e == "float"; + isFunction = e: typeOf e == "lambda"; + isInt = e: typeOf e == "int"; + isList = e: typeOf e == "list"; + isNull = e: typeOf e == "null"; + isString = e: typeOf e == "string"; + + toString = e: + if isAttrs e then + if e ? __toString then e.__toString e else e.outPath + else if isBool e then + if e then "1" else "" + else if isFloat e then + __mn_float_toString e + else if isInt e then + __mn_int_toString e + else if isList e then + concatStringsSep " " (map toString e) + else if isNull e then + "" + else if isString e then + e + else abort null; + + stringLength = + __mn_matchString ({ head, tail, empty }: + if empty then 0 else 1 + stringLength tail); + + substring = start: assert start >= 0; len: + __mn_matchString ({ head, tail, empty }: + if empty || len == 0 then "" else + if start > 0 + then substring (start - 1) len tail + else head + substring 0 (len - 1) tail); + + replaceStrings = from: to: s: + __mn_matchList + ({ head, tail, empty }: + let from = if empty then [ ] else [ head ] ++ tail; in + __mn_matchList + ({ head, tail, empty }: + let to = if empty then [ ] else [ head ] ++ tail; in + assert length from == length to; + __mn_strings_replace from to s) + to) + from; + + __mn_strings_replace = subsFrom: subsTo: s: + let go = __mn_strings_replace subsFrom subsTo; in + __mn_strings_replace_aux go subsFrom subsTo s; + + __mn_strings_replace_aux = go: subsFrom: subsTo: s: + __mn_matchList + ({ head, tail, empty }: + if empty + then + __mn_matchString + ({ head, tail, empty }: if empty then "" else head + go tail) + s + else + let subFrom = head; subsFrom' = tail; in + __mn_matchList + ({ head, tail, ... }: + let subTo = head; subsTo' = tail; in + if subFrom == "" + then + # We can only ask ourselves why, but it is so -- in Nix: + # replaceStrings ["" "a"] ["X" "_"] "asdf" ~> "XaXsXdXfX" + # and so we emulate this 'behavior' + subTo + __mn_matchString + ({ head, tail, empty }: + if empty then "" else head + go tail) + s + else + ({ ok, rest }: + if ok + then subTo + go rest + else __mn_strings_replace_aux go subsFrom' subsTo' s) + (__mn_string_chopPrefix subFrom s)) + subsTo) + subsFrom; + + __mn_string_chopPrefix = prefix: s: + __mn_matchString + ({ head, tail, empty }: + if empty then { ok = true; rest = s; } else + let prefix = head; prefix' = tail; in __mn_matchString + ({ head, tail, empty }: + if empty || prefix != head then { ok = false; rest = null; } else + __mn_string_chopPrefix prefix' tail) + s) + prefix; + + __mn_string_drop = n: s: + if n <= 0 then s else + __mn_matchString + ({ tail, empty, ... }: + if empty then "" else + __mn_string_drop (n - 1) tail) + s; + + __mn_float_toString = x: + let + sign = x < 0; + abs = __mn_abs x; + int = floor abs; + dec = __mn_nearestEven ((abs - int) * 1000000); + in + (if sign then "-" else "") + + __mn_int_toString int + "." + __mn_int_toString dec; + __mn_int_toString = x: (if x < 0 then "-" else "") + + ( + let d10 = __mn_quotRem (__mn_abs x) 10; in + (if d10.quot != 0 then toString d10.quot else "") + + (if d10.rem == 0 then "0" else + if d10.rem == 1 then "1" else + if d10.rem == 2 then "2" else + if d10.rem == 3 then "3" else + if d10.rem == 4 then "4" else + if d10.rem == 5 then "5" else + if d10.rem == 6 then "6" else + if d10.rem == 7 then "7" else + if d10.rem == 8 then "8" else + if d10.rem == 9 then "9" else + abort null) + ); + + __mn_quotRem = x: y: + let quot = x / y; in + { inherit quot; rem = x - quot * y; }; + __mn_abs = x: if x < 0 then -x else x; + + __mn_attr_insertNew = as: x: e: + if x == null then { } else + assert !(as ? ${x}); as // __mn_singleton x e; + __mn_attr_has_aux = d: e: + if typeOf d != "set" then false else __mn_attr_has_prim d e; + __mn_attr_has = e: + __mn_matchList ({ head, tail, empty }: + if empty then true else + if __mn_attr_has_aux e head then __mn_attr_has e.${head} tail + else false); + __mn_attr_select = e: + __mn_matchList ({ head, tail, empty }: + if empty then e + else __mn_attr_select e.${head} tail); + __mn_attr_selectOr = e: as: d: + if __mn_attr_has e as + then __mn_attr_select e as + else d; + __mn_assert = e1: e2: + if e1 then e2 else abort null; + + __mn_consAttrs = as: acc: + __mn_foldr + (x: acc: acc // { + ${x} = [ as.${x} ] ++ (acc.${x} or [ ]); + }) + acc + (attrNames as); + __mn_zipAttrs = __mn_foldr __mn_consAttrs { }; + + # Old merge sort algorithm, taken from GHC.Internal.Data.OldList. + __mn_mergesort = cmp: xs: __mn_mergesort' cmp (__mn_singletons xs); + __mn_singletons = map (x: [ x ]); + __mn_mergesort' = cmp: xs: + __mn_matchList + ({ head, tail, empty }: + if empty then [ ] else if tail == [ ] then head else + __mn_mergesort' cmp (__mn_mergePairs cmp xs)) + xs; + __mn_mergePairs = cmp: + __mn_matchList ({ head, tail, empty }: if empty then [ ] else + let xs' = head; in __mn_matchList + ({ head, tail, empty }: + if empty then [ xs' ] else + let ys' = head; xss' = tail; in + [ (__mn_merge cmp xs' ys') ] ++ __mn_mergePairs cmp xss') + tail); + __mn_merge = cmp: xs: ys: + __mn_matchList + ({ head, tail, empty }: + if empty then ys else + let x = head; xs' = tail; in + __mn_matchList + ({ head, tail, empty }: + if empty then xs else + let y = head; ys' = tail; in + if cmp y x + then [ y ] ++ __mn_merge cmp xs ys' # y < x, i.e., x > y + else [ x ] ++ __mn_merge cmp xs' ys) + ys) + xs; +} 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 @@ +open Core + +let _ = assert (Sys.word_size_in_bits = 64) +let chlist s = String.to_list s +let ( <> ) l1 l2 = not (List.equal Char.( = ) l1 l2) +let str = String.of_char_list +let prec = 53 +let emax = 1024 +let exp_bits = 11 +let saturated_exp = Int.shift_left 1 exp_bits - 1 + +let rec int_bits (x : int) : bool list = + if Int.(x < 0) then raise (Invalid_argument "Number must be nonnegative") + else if Int.(x = 0) then [] + else + let q = x /% 2 and r = x % 2 in + int_bits q @ [ r = 1 ] + +let int_to_positive (x : int) : Extraction.Internal.BinNums.positive = + if x <= 0 then raise (Invalid_argument "Number must be positive") + else + let bits = List.tl_exn (int_bits x) in + List.fold_left + ~f:(fun acc digit -> + if digit then Extraction.Internal.BinNums.Coq_xI acc + else Extraction.Internal.BinNums.Coq_xO acc) + ~init:Extraction.Internal.BinNums.Coq_xH bits + +let int_to_z (x : int) : Extraction.Internal.BinNums.coq_Z = + if x = 0 then Z0 + else if x < 0 then Zneg (int_to_positive (-x)) + else Zpos (int_to_positive x) + +let rec int63_of_positive (x : Extraction.Internal.BinNums.positive) : Int63.t = + let two = Int63.(succ one) in + match x with + | Coq_xH -> Int63.of_int_exn 1 + | Coq_xO x -> Int63.(two * int63_of_positive x) + | Coq_xI x -> Int63.((two * int63_of_positive x) + one) + +let int63_of_z (x : Extraction.Internal.BinNums.coq_Z) : Int63.t = + match x with + | Z0 -> Int63.zero + | Zpos x -> int63_of_positive x + | Zneg x -> Int63.neg (int63_of_positive x) + +let int63_to_positive x = Int63.to_int_exn x |> int_to_positive + +(* Conversions are the same as those in Coq's FloatOps. + See https://github.com/coq/coq/blob/master/theories/Floats/FloatOps.v *) + +let normfr_mantissa f = + let f = Float.abs f in + if Float.(f >= 0.5) && Float.(f < 1.) then Float.to_int (Float.ldexp f prec) + else 0 + +let float_to_flocq (x : float) : Extraction.Internal.Floats.float = + match Float.classify x with + | Zero -> Extraction.Internal.Floats.B754_zero (Float.ieee_negative x) + | Nan -> + Extraction.Internal.Floats.B754_nan + (Float.ieee_negative x, Float.ieee_mantissa x |> int63_to_positive) + | Infinite -> Extraction.Internal.Floats.B754_infinity (Float.ieee_negative x) + | Normal | Subnormal -> ( + let prec_z = int_to_z prec and emax_z = int_to_z emax in + let r, exp = Float.frexp x in + let e = int_to_z (exp - prec) and r' = int_to_z (normfr_mantissa r) in + let shr, e' = + Extraction.Internal.Floats.(shr_fexp prec_z emax_z r' e Coq_loc_Exact) + in + match shr.shr_m with + | Zpos p -> B754_finite (Float.is_negative x, p, e') + | Zneg _ | Z0 -> assert false) + +let float_from_flocq x : float = + match x with + | Extraction.Internal.Floats.B754_zero s -> + Float.create_ieee_exn ~negative:s ~mantissa:Int63.zero ~exponent:0 + | Extraction.Internal.Floats.B754_infinity s -> + if s then Float.neg_infinity else Float.infinity + | Extraction.Internal.Floats.B754_nan (s, m) -> + let m_int = int63_of_positive m in + Float.create_ieee_exn ~negative:s ~mantissa:m_int ~exponent:saturated_exp + | Extraction.Internal.Floats.B754_finite (s, m, e) -> + let pm = Float.of_int63 (int63_of_positive m) in + let f = Float.ldexp pm (Int63.to_int_exn (int63_of_z e)) in + if s then Float.neg f else f + +open struct + open Base_quickcheck + + let%expect_test "float conversion" = + Test.run_exn + (module Float) + ~f:(fun x -> [%test_eq: float] (float_from_flocq (float_to_flocq x)) x) +end 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 @@ +(library + (name mininix) + (inline_tests) + (preprocessor_deps + (file builtins.nix)) + (preprocess + (pps + ppx_blob + ppx_sexp_conv + ppx_expect + ppx_assert + base_quickcheck.ppx_quickcheck)) + (instrumentation + (backend bisect_ppx)) + (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 @@ +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 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 @@ +module Nix2mininix = Nix2mininix +module Mininix2nix = Mininix2nix +module Sexp = Sexp +module Import = Import + +let interp_tl ~fuel ~mode ?(imports = []) e = + Run.interp ~fuel ~mode ~env:(Import.make_env imports) e + +let apply_prelude = Builtins.apply_prelude + +let preprocess input ~filename = + input |> Nix.parse ~filename |> Nix.elaborate |> Nix2mininix.from_nix + |> 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 @@ +open Conv +open Core + +(* [or] is not a 'strong' keyword. That means that 'it depends' whether it is + identified as such. In the context of the left-hand side of an attribute, it + is not recognized as such. *) +let strong_keywords = + [ "with"; "rec"; "let"; "in"; "inherit"; "if"; "then"; "else"; "assert" ] + +let id_re = Str.regexp {|^[A-Za-z_]+[A-Za-z0-9'_-]*$|} + +let is_simple_id s = + Str.string_match id_re s 0 + && not (List.exists strong_keywords ~f:(String.( = ) s)) + +let thunk_map_to_map tm = + Extraction.thunk_map_fold + (fun k t -> Map.add_exn ~key:(String.of_char_list k) ~data:t) + (Map.empty (module String)) + tm + +let from_lit l = + match l with + | Extraction.LitString s -> Nix.Ast.Val (Nix.Ast.Str (str s, [])) + | Extraction.LitNull -> Nix.Ast.Id "null" + | Extraction.LitBool b -> Nix.Ast.Id (if b then "true" else "false") + | Extraction.LitNum x -> + Nix.Ast.Val + (match x with + | Extraction.NInt x -> Nix.Ast.Int (x |> Extraction.string_of_Z |> str) + | Extraction.NFloat x -> + Nix.Ast.Float (Printf.sprintf "%g" (float_from_flocq x))) + +let rec from_val = function + | Extraction.VClo _ | Extraction.VCloMatch _ -> Nix.Ast.Id "" + | Extraction.VLit l -> from_lit l + | Extraction.VAttr bs -> + let bs = + thunk_map_to_map bs + |> Map.to_alist ~key_order:`Increasing + |> List.map ~f:(fun (x, t) -> + let lhs = + if is_simple_id x then Nix.Ast.Id x + else Nix.Ast.Val (Nix.Ast.Str (x, [])) + in + Nix.Ast.AttrPath ([ lhs ], from_thunk t)) + in + Nix.Ast.Val (Nix.Ast.AttSet (Nix.Ast.Nonrec, bs)) + | Extraction.VList ts -> Nix.Ast.Val (Nix.Ast.List List.(ts >>| from_thunk)) + +and from_thunk = function + | Extraction.Thunk (_, ELit l) -> from_lit l + | Extraction.Thunk _ | Extraction.Indirect _ -> Nix.Ast.Id "" + | 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 @@ +open Conv +open Core + +exception FromNixError of string + +let try_insert_attr x e bs = + let x = chlist x in + if Extraction.attr_set_contains x bs then + raise (FromNixError "Attribute already exists") + else Extraction.attr_set_insert x e bs + +(* Shorthands, minor conversions *) + +let mn_singleton_set x e = + Extraction.( + EAttr (attr_set_insert (chlist x) (Attr (NONREC, e)) attr_set_empty)) + +let mn_abs args e = + List.fold_right args ~init:e ~f:(fun arg e' -> + Extraction.EAbs (chlist arg, e')) + +let mn_lit l = Extraction.ELit l +let mn_int x = mn_lit (Extraction.LitNum (Extraction.NInt x)) +let mn_float x = mn_lit (Extraction.LitNum (Extraction.NFloat x)) +let mn_bool b = mn_lit (Extraction.LitBool b) +let mn_true = mn_bool true +let mn_false = mn_bool false +let mn_str s = mn_lit (Extraction.LitString (chlist s)) +let mn_null = mn_lit Extraction.LitNull +let mn_id x = Extraction.EId (chlist x, None) +let mn_app e1 e2 = Extraction.EApp (e1, e2) +let mn_seq e1 e2 = Extraction.ESeq (Extraction.SHALLOW, e1, e2) +let mn_deep_seq e1 e2 = Extraction.ESeq (Extraction.DEEP, e1, e2) +let mn_list es = Extraction.EList es + +let mn_attr (bs : (string * [ `Rec | `Nonrec ] * Extraction.expr) list) = + Extraction.EAttr + (List.fold_left bs ~init:Extraction.attr_set_empty ~f:(fun bs' (x, r, e) -> + let r' = + match r with `Rec -> Extraction.REC | `Nonrec -> Extraction.NONREC + in + Extraction.attr_set_insert (chlist x) (Extraction.Attr (r', e)) bs')) + +let mn_with e1 e2 = Extraction.ELetAttr (Extraction.WITH, e1, e2) +let mn_binop op e1 e2 = Extraction.EBinOp (op, e1, e2) +let mn_add e1 e2 = mn_binop Extraction.AddOp e1 e2 +let mn_sub e1 e2 = mn_binop Extraction.SubOp e1 e2 +let mn_mul e1 e2 = mn_binop Extraction.MulOp e1 e2 +let mn_div e1 e2 = mn_binop Extraction.DivOp e1 e2 +let mn_bit_and e1 e2 = mn_binop Extraction.AndOp e1 e2 +let mn_bit_or e1 e2 = mn_binop Extraction.OrOp e1 e2 +let mn_bit_xor e1 e2 = mn_binop Extraction.XOrOp e1 e2 +let mn_lt e1 e2 = mn_binop Extraction.LtOp e1 e2 +let mn_eq e1 e2 = mn_binop Extraction.EqOp e1 e2 +let mn_if e1 e2 e3 = Extraction.EIf (e1, e2, e3) +let mn_delete_attr e1 e2 = mn_binop Extraction.DeleteAttrOp e1 e2 +let mn_has_attr e1 e2 = mn_binop Extraction.HasAttrOp e1 e2 +let mn_select_attr e1 e2 = mn_binop Extraction.SelectAttrOp e1 e2 + +let mn_singleton_attr e1 e2 = + mn_app (mn_binop Extraction.SingletonAttrOp e1 mn_null) e2 + +let mn_update_attr e1 e2 = mn_binop Extraction.UpdateAttrOp e1 e2 +let mn_type_of e = mn_binop Extraction.TypeOfOp e mn_null +let mn_function_args e = mn_binop Extraction.FunctionArgsOp e mn_null +let mn_list_append e1 e2 = mn_binop Extraction.AppendListOp e1 e2 +let mn_list_match e = mn_binop Extraction.MatchListOp e mn_null +let mn_string_match e = mn_binop Extraction.MatchStringOp e mn_null +let mn_attr_match e = mn_binop Extraction.MatchAttrOp e mn_null +let mn_ceil e = mn_binop (Extraction.RoundOp Ceil) e mn_null +let mn_nearest_even e = mn_binop (Extraction.RoundOp NearestEven) e mn_null +let mn_floor e = mn_binop (Extraction.RoundOp Floor) e mn_null + +(* Macros *) + +let mn_cast_bool e = mn_if e mn_true mn_false +let mn_or e1 e2 = mn_if e1 mn_true (mn_cast_bool e2) +let mn_and e1 e2 = mn_if e1 (mn_cast_bool e2) mn_false +let mn_impl e1 e2 = mn_if e1 (mn_cast_bool e2) mn_true +let mn_not e = mn_if e mn_false mn_true +let mn_negate e = mn_sub (mn_int Extraction.Internal.BinNums.Z0) e +let mn_neq e1 e2 = mn_not (mn_eq e2 e1) +let mn_gt e1 e2 = mn_lt e2 e1 +let mn_lte e1 e2 = mn_not (mn_gt e1 e2) +let mn_gte e1 e2 = mn_not (mn_lt e1 e2) + +(* Macros based on exported functions from the prelude *) + +let mnbi_assert e1 e2 = mn_app (mn_app (mn_id "__mn_assert") e1) e2 +let mnbi_has_attr e ds = mn_app (mn_app (mn_id "__mn_attr_has") e) (mn_list ds) +let mnbi_select e ds = mn_app (mn_app (mn_id "__mn_attr_select") e) (mn_list ds) + +let mnbi_select_or e1 ds e2 = + mn_app (mn_app (mn_app (mn_id "__mn_attr_selectOr") e1) (mn_list ds)) e2 + +let mnbi_insert_new e1 e2 e3 = + mn_app (mn_app (mn_app (mn_id "__mn_attr_insertNew") e1) e2) e3 + +let is_dynamic_binding (b : Nix.Ast.binding) = + match b with + | Nix.Ast.AttrPath ([ Nix.Ast.Val (Nix.Ast.Str (_, [])) ], _) + | Nix.Ast.Inherit _ -> + false + | Nix.Ast.AttrPath ([ _ ], _) -> true + | _ -> assert false + +let has_dynamic_bindings (bs : Nix.Ast.binding list) = + List.exists bs ~f:is_dynamic_binding + +(* Static bindings left, dynamic bindings right *) +let partition_dynamic (bs : Nix.Ast.binding list) : + Nix.Ast.binding list * Nix.Ast.binding list = + List.fold_left bs ~init:([], []) ~f:(fun (static, dynamic) b -> + if is_dynamic_binding b then (static, b :: dynamic) + else (b :: static, dynamic)) + +(* Precondition: e must be have been processed by the elaborator. *) +let rec from_nix e = + match e with + | Nix.Ast.BinaryOp (op, e1, e2) -> ( + let e1', e2' = (from_nix e1, from_nix e2) in + match op with + | Nix.Ast.Plus -> mn_add e1' e2' + | Nix.Ast.Minus -> mn_sub e1' e2' + | Nix.Ast.Mult -> mn_mul e1' e2' + | Nix.Ast.Div -> mn_div e1' e2' + | Nix.Ast.Gt -> mn_gt e1' e2' + | Nix.Ast.Lt -> mn_lt e1' e2' + | Nix.Ast.Lte -> mn_lte e1' e2' + | Nix.Ast.Gte -> mn_gte e1' e2' + | Nix.Ast.Eq -> mn_eq e1' e2' + | Nix.Ast.Neq -> mn_neq e1' e2' + | Nix.Ast.Or -> mn_or e1' e2' + | Nix.Ast.And -> mn_and e1' e2' + | Nix.Ast.Impl -> mn_impl e1' e2' + | Nix.Ast.Merge -> mn_update_attr e1' e2' + | Nix.Ast.Concat -> mn_list_append e1' e2') + | Nix.Ast.UnaryOp (op, e) -> ( + let e = from_nix e in + match op with Nix.Ast.Negate -> mn_negate e | Nix.Ast.Not -> mn_not e) + | Nix.Ast.Cond (e1, e2, e3) -> mn_if (from_nix e1) (from_nix e2) (from_nix e3) + | Nix.Ast.With (e1, e2) -> mn_with (from_nix e1) (from_nix e2) + | Nix.Ast.Assert (e1, e2) -> mnbi_assert (from_nix e1) (from_nix e2) + | Nix.Ast.Test (e, ds) -> mnbi_has_attr (from_nix e) List.(ds >>| from_nix) + | Nix.Ast.SetLet bs -> + from_nix + (Nix.Ast.Select + ( Nix.Ast.Val (Nix.Ast.AttSet (Nix.Ast.Rec, bs)), + [ Nix.Ast.Val (Nix.Ast.Str ("body", [])) ], + None )) + | Nix.Ast.Let (bs, e2) -> + if has_dynamic_bindings bs then + raise (FromNixError "Let bindings may not be dynamic"); + let e1 = from_nix (Nix.Ast.Val (Nix.Ast.AttSet (Nix.Ast.Rec, bs))) in + Extraction.ELetAttr (Extraction.ABS, e1, from_nix e2) + | Nix.Ast.Val v -> from_nix_val v + | Nix.Ast.Id x -> mn_id x + | Nix.Ast.Select (e, parts, md) -> ( + match md with + | Some d -> + mnbi_select_or (from_nix e) List.(parts >>| from_nix) (from_nix d) + | None -> ( + match parts with + | [ part ] -> mn_select_attr (from_nix e) (from_nix part) + | _ -> mnbi_select (from_nix e) List.(parts >>| from_nix))) + | Nix.Ast.Apply (e1, e2) -> mn_app (from_nix e1) (from_nix e2) + | Nix.Ast.Aquote _ -> + assert false (* should be gone after processing by elaborator *) + +and from_nix_val v = + match v with + | Str (s, parts) -> + let parts = List.(parts >>= fun (e, s) -> [ from_nix e; mn_str s ]) in + List.fold_left parts ~init:(mn_str s) ~f:mn_add + | IStr _ -> raise (FromNixError "Indented strings are not supported") + | Int n -> ( + match Extraction.string_to_Z (chlist n) with + | Some n -> mn_int n + | None -> raise (FromNixError "Bad integer literal")) + | Float n -> + let n = + try Float.of_string n + with Invalid_argument _ -> raise (FromNixError "Bad float literal") + in + if Float.(is_nan n || is_inf n) then + raise (FromNixError "Bad float literal") + else mn_float (float_to_flocq n) + | Path _ | SPath _ | HPath _ -> raise (FromNixError "Paths are not supported") + | Uri s -> mn_str s + | Lambda (Alias x, e) -> mn_abs [ x ] (from_nix e) + | Lambda (ParamSet (Some x, fs), e) -> + from_nix_val + (Lambda (Alias x, Apply (Val (Lambda (ParamSet (None, fs), e)), Id x))) + | Lambda (ParamSet (None, (fs, strictness)), e) -> + let ms = + List.fold_left fs ~init:Extraction.matcher_empty ~f:(fun ms (x, me) -> + Extraction.matcher_insert (chlist x) (Option.map ~f:from_nix me) ms) + in + Extraction.EAbsMatch + ( ms, + (match strictness with Loose -> false | Exact -> true), + from_nix e ) + | List es -> mn_list (List.map es ~f:from_nix) + | AttSet (recursivity, bs) -> + let static, dynamic = partition_dynamic bs + and recursivity' = + match recursivity with + | Nix.Ast.Rec -> Extraction.REC + | Nix.Ast.Nonrec -> Extraction.NONREC + in + + let set_no_dyn = + Extraction.EAttr + (List.fold_left static ~init:Extraction.attr_set_empty + ~f:(fun static' bnd -> + match bnd with + | Nix.Ast.AttrPath ([ Nix.Ast.Val (Nix.Ast.Str (x, [])) ], e) -> + try_insert_attr x + (Extraction.Attr (recursivity', from_nix e)) + static' + | Nix.Ast.Inherit (None, xs) -> + List.fold_left xs ~init:static' ~f:(fun static' x -> + match x with + | Id x -> + try_insert_attr x + (Extraction.Attr (Extraction.NONREC, mn_id x)) + static' + | _ -> assert false) + | Nix.Ast.Inherit (Some e, xs) -> + let e = from_nix e in + List.fold_left xs ~init:static' ~f:(fun static' x -> + match x with + | Id x -> + try_insert_attr x + (Extraction.Attr + (recursivity', mn_select_attr e (mn_str x))) + static' + | _ -> assert false) + | _ -> assert false)) + in + + List.fold_right dynamic ~init:set_no_dyn ~f:(fun bnd set -> + match bnd with + | Nix.Ast.AttrPath ([ d ], e) -> + mnbi_insert_new set + (match recursivity with + | Nix.Ast.Rec -> + Extraction.ELetAttr (Extraction.ABS, set_no_dyn, from_nix d) + | Nix.Ast.Nonrec -> from_nix d) + (match recursivity with + | Nix.Ast.Rec -> + Extraction.ELetAttr (Extraction.ABS, set_no_dyn, from_nix e) + | Nix.Ast.Nonrec -> from_nix e) + | _ -> 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 @@ +open Core + +(* The [n]th Church numeral *) +let rec church n f x = if n <= 0 then x else church (n - 1) f (f x) + +let limited = + church 2048 + (fun x -> Extraction.Internal.Datatypes.S x) + Extraction.Internal.Datatypes.O + +let rec infinity = Extraction.Internal.Datatypes.S infinity + +let interp ~fuel ~mode ~env e = + let mode : Extraction.mode = + match mode with `Shallow -> SHALLOW | `Deep -> DEEP + and fuel = match fuel with `Unlimited -> infinity | `Limited -> limited in + 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 @@ +open Conv +open Core +open Extraction + +exception ToSexpError of string + +let tag t l = Sexp.List (Sexp.Atom t :: l) + +let lit_to_sexp = function + | LitString s -> tag "LitString" [ Sexp.Atom (str s) ] + | LitNum (NInt n) -> + tag "LitNum" [ Sexp.Atom "INT"; Sexp.Atom (str (string_of_Z n)) ] + | LitNum (NFloat n) -> + tag "LitNum" + [ + Sexp.Atom "FLOAT"; + Sexp.Atom (Printf.sprintf "%g" (float_from_flocq n)); + ] + | LitBool b -> tag "LitBool" [ Sexp.Atom (Bool.to_string b) ] + | LitNull -> tag "LitNull" [] + +let option_to_sexp mv ~f = + match mv with Some v -> tag "Some" [ f v ] | None -> Sexp.Atom "None" + +let mode_to_sexp mode = + Sexp.Atom (match mode with SHALLOW -> "SHALLOW" | DEEP -> "DEEP") + +let rec_to_sexp r = Sexp.Atom (match r with REC -> "REC" | NONREC -> "NONREC") + +let binop_to_sexp op = + Sexp.Atom + (match op with + | UpdateAttrOp -> "UpdateAttrOp" + | AddOp -> "AddOp" + | SubOp -> "SubOp" + | MulOp -> "MulOp" + | DivOp -> "DivOp" + | AndOp -> "AndOp" + | OrOp -> "OrOp" + | XOrOp -> "XOrOp" + | RoundOp Ceil -> "Ceil" + | RoundOp NearestEven -> "NearestEven" + | RoundOp Floor -> "Floor" + | LtOp -> "LtOp" + | EqOp -> "EqOp" + | HasAttrOp -> "HasAttrOp" + | SelectAttrOp -> "SelectAttrOp" + | DeleteAttrOp -> "DeleteAttrOp" + | SingletonAttrOp -> "SingletonAttrOp" + | TypeOfOp -> "TypeOfOp" + | AppendListOp -> "AppendListOp" + | MatchAttrOp -> "MatchAttrOp" + | MatchListOp -> "MatchListOp" + | MatchStringOp -> "MatchStringOp" + | FunctionArgsOp -> "FunctionArgsOp") + +let kind_to_sexp k = Sexp.Atom (match k with ABS -> "ABS" | WITH -> "WITH") + +let rec expr_to_sexp = function + | ELit l -> tag "ELit" [ lit_to_sexp l ] + | EId (x, None) -> tag "EId" [ Sexp.Atom (str x) ] + | EId (x, Some (k, e)) -> + tag "EId" + [ Sexp.Atom (str x); tag "alt" [ kind_to_sexp k; expr_to_sexp e ] ] + | EAbs (x, e) -> tag "EAbs" [ Sexp.Atom (str x); expr_to_sexp e ] + | EAbsMatch (ms, strict, e) -> + tag "EAbsMatch" + [ + Sexp.Atom (if strict then "EXACT" else "LOOSE"); + tag "formals" + (matcher_fold + (fun x me se -> + Sexp.List + [ Sexp.Atom (str x); option_to_sexp me ~f:expr_to_sexp ] + :: se) + [] ms); + expr_to_sexp e; + ] + | EApp (e1, e2) -> tag "EApp" [ expr_to_sexp e1; expr_to_sexp e2 ] + | ELetAttr (k, e1, e2) -> + tag "ELetAttr" [ kind_to_sexp k; expr_to_sexp e1; expr_to_sexp e2 ] + | ESeq (mode, e1, e2) -> + tag "ESeq" [ mode_to_sexp mode; expr_to_sexp e1; expr_to_sexp e2 ] + | EAttr bs -> + tag "EAttr" + (attr_set_fold + (fun x (Attr (r, e)) se -> + Sexp.List [ Sexp.Atom (str x); rec_to_sexp r; expr_to_sexp e ] + :: se) + [] bs) + | EList es -> + tag "EList" + (Internal.List.fold_right (fun e se -> expr_to_sexp e :: se) [] es) + | EBinOp (op, e1, e2) -> + tag "EBinOp" [ binop_to_sexp op; expr_to_sexp e1; expr_to_sexp e2 ] + | EIf (e1, e2, e3) -> + tag "EIf" [ expr_to_sexp e1; expr_to_sexp e2; expr_to_sexp e3 ] + +let rec val_to_sexp = function + | VLit l -> tag "VLit" [ lit_to_sexp l ] + | VClo _ -> tag "VClo" [] + | VCloMatch _ -> tag "VCloMatch" [] + | VAttr bs -> + tag "VAttr" + (Extraction.thunk_map_fold + (fun x t bs' -> + Sexp.List [ Sexp.Atom (str x); thunk_to_sexp t ] :: bs') + [] bs) + | VList ts -> + tag "VList" + (Internal.List.fold_right (fun t st -> thunk_to_sexp t :: st) [] ts) + +and env_to_sexp env = + tag "Env" + (Extraction.env_fold + (fun x (k, t) envs -> + Sexp.List + [ + Sexp.Atom (str x); + Sexp.Atom + (match k with + | Extraction.ABS -> "ABS" + | Extraction.WITH -> "WITH"); + thunk_to_sexp t; + ] + :: envs) + [] env) + +and thunk_to_sexp = function + | Thunk _ -> tag "Thunk" [ Sexp.Atom "DELAYED" ] + | Indirect _ -> tag "Thunk" [ Sexp.Atom "INDIRECT" ] + | Forced v -> tag "Thunk" [ Sexp.Atom "FORCED"; val_to_sexp v ] + +let expr_res_to_sexp = function + | NoFuel -> Sexp.Atom "NoFuel" + | Res e -> tag "Res" [ option_to_sexp e ~f:expr_to_sexp ] + +let val_res_to_sexp = function + | NoFuel -> Sexp.Atom "NoFuel" + | Res e -> tag "Res" [ option_to_sexp e ~f:val_to_sexp ] + +let rec (sexp_of_import_tree : Import.tree -> Sexp.t) = function + | { filename; deps = [] } -> Sexp.Atom filename + | { filename; deps } -> + Sexp.List [ Sexp.Atom filename; sexp_of_import_forest deps ] + +and sexp_of_import_forest forest = + Sexp.List (Sexp.Atom "deps" :: List.map forest ~f:sexp_of_import_tree) + +exception OfSexpError of string + +let rec import_tree_of_sexp : Sexp.t -> Import.tree = function + | Sexp.Atom filename -> { filename; deps = [] } + | Sexp.List [ Sexp.Atom filename; deps ] -> + { filename; deps = import_forest_of_sexp deps } + | _ -> raise (OfSexpError "Could not parse import tree") + +and import_forest_of_sexp = function + | Sexp.List (Sexp.Atom "deps" :: deps) -> List.map ~f:import_tree_of_sexp deps + | _ -> 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 @@ +(menhir + (modules parser) + (flags "--dump" "--strict" "--external-tokens" "Tokens") + (infer true)) + +(ocamllex + (modules lexer)) + +(library + (name nix) + (preprocess + (pps ppx_sexp_conv)) + (instrumentation + (backend bisect_ppx)) + (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 @@ +open Core +open Types + +(* The Nix elaborator does a few things: + - Attribute paths are transformed into a simple list of expressions: + + Simple identifiers are rewritten to string values + + Antiquotations are rewritten to their component expressions + + Anything else, that is not a string value, is rejected + and raises an exception + - In 'inherit (...) x1 ... xn', x1 ... xn are checked for 'reasonably' being + identifiers, i.e., being one of x, "x" and ${"x"}. + - Nested attribute paths are unfolded and attribute sets are merged where + possible. (Where we mean 'what Nix does' with 'where possible'; see the + comment at the respective function.) + - Paths are turned into strings and made absolute w.r.t. the current + working directory. + - Indented strings are converted to their 'normal' counterpart. *) + +exception ElaborateError of string + +type attr_set = recursivity * binding list + +let set_expr (r, bs) = Val (AttSet (r, bs)) +let get_id = function Id x -> x | _ -> assert false + +let rec update_bnd (bs : binding list) (x : string) ~(f : expr option -> expr) = + match bs with + | [] -> [ AttrPath ([ Val (Str (x, [])) ], f None) ] + | AttrPath ([ Val (Str (y, [])) ], e) :: s' when String.(x = y) -> + AttrPath ([ Val (Str (y, [])) ], f (Some e)) :: s' + | Inherit (_, ids) :: _ + when List.exists ids ~f:(fun e -> String.(get_id e = x)) -> + raise (ElaborateError "Cannot update inherit") + | bnd :: s' -> bnd :: update_bnd s' x ~f + +let set_update_bnd (r, bs) x ~f = (r, update_bnd bs x ~f) + +let rec has_bnd (bs : binding list) (x : string) : bool = + match bs with + | [] -> false + | AttrPath ([ Val (Str (y, [])) ], _) :: _ when String.(x = y) -> true + | Inherit (_, ids) :: _ + when List.exists ids ~f:(fun e -> String.(get_id e = x)) -> + true + | _ :: bs' -> has_bnd bs' x + +let merge_bnds bs1 bs2 : binding list = + List.fold_left bs2 ~init:bs1 ~f:(fun bs1' b2 -> + match b2 with + | AttrPath ([ Val (Str (x, [])) ], e) -> + update_bnd bs1' x ~f:(function + | Some _ -> raise (ElaborateError "Duplicated attribute") + | None -> e) + | AttrPath ([ d ], e) -> AttrPath ([ d ], e) :: bs1' + | Inherit (md, xs) -> + if List.for_all xs ~f:(fun e -> not (has_bnd bs1' (get_id e))) then + Inherit (md, xs) :: bs1' + else raise (ElaborateError "Duplicated attribute") + | _ -> assert false) + +(* This function intentionally clobbers recursivity, because that is the way + that Nix likes to handle attribute insertion. See + (1) https://github.com/NixOS/nix/issues/9020 + (2) https://github.com/NixOS/nix/issues/11268 + (3) https://github.com/NixOS/nix/pull/11294 *) +let rec insert (bs : binding list) (path : expr list) (e : expr) = + match path with + | [] -> raise (ElaborateError "Cannot insert attribute with empty path") + | [ Val (Str (x, [])) ] -> + update_bnd bs x ~f:(function + | None -> e + | Some (Val (AttSet (r1, bs1))) -> ( + match e with + | Val (AttSet (_, bs2)) -> set_expr (r1, merge_bnds bs1 bs2) + | _ -> raise (ElaborateError "Duplicated attribute")) + | _ -> raise (ElaborateError "Duplicated attribute")) + | Val (Str (x, [])) :: rest -> + update_bnd bs x ~f:(function + | Some (Val (AttSet (r, bs))) -> Val (AttSet (r, insert bs rest e)) + | Some _ -> raise (ElaborateError "Duplicated attribute") + | None -> Val (AttSet (Nonrec, insert [] rest e))) + | [ part ] -> AttrPath ([ part ], e) :: bs + | part :: rest -> + AttrPath ([ part ], Val (AttSet (Nonrec, insert [] rest e))) :: bs + +let insert_inherit (bs : binding list) (from : expr option) (es : expr list) = + if List.for_all es ~f:(fun e -> not (has_bnd bs (get_id e))) then + Inherit (from, es) :: bs + else raise (ElaborateError "Duplicated attribute") + +let simplify_path_component = function + | Id x -> Val (Str (x, [])) + | Val (Str (s, ess)) -> Val (Str (s, ess)) + | Aquote e -> e + | _ -> raise (ElaborateError "Unexpected path component") + +let simplify_path = List.map ~f:simplify_path_component + +let simplify_bnd_paths = + List.map ~f:(fun bnd -> + match bnd with + | AttrPath (path, e) -> AttrPath (simplify_path path, e) + | Inherit (me, xs) -> Inherit (me, xs)) + +(* Law: concat_lines ∘ split_lines = id *) + +let rec split_lines s = + match String.lsplit2 s ~on:'\n' with + | Some (s1, s2) -> s1 :: split_lines s2 + | None -> [ s ] + +let rec concat_lines = function + | [] -> "" + | [ x ] -> x + | x :: xs -> x ^ "\n" ^ concat_lines xs + +let map_tail ~f = function [] -> [] | x :: xs -> x :: List.map ~f xs + +let unindent n s ~skip_first_line = + let map_op ~f = if skip_first_line then map_tail ~f else List.map ~f in + split_lines s + |> map_op ~f:(fun line -> + let expected_prefix = String.make n ' ' in + String.chop_prefix_if_exists ~prefix:expected_prefix line) + |> concat_lines + +let is_spaces l = String.(strip l ~drop:(Char.( = ) ' ') |> is_empty) + +let drop_first_empty_line s = + match String.lsplit2 s ~on:'\n' with + | Some (l, s') when is_spaces l -> s' + | _ -> s + +let rec process ?(dir = None) = function + | BinaryOp (op, e1, e2) -> BinaryOp (op, process ~dir e1, process ~dir e2) + | UnaryOp (op, e) -> UnaryOp (op, process ~dir e) + | Cond (e1, e2, e3) -> Cond (process ~dir e1, process ~dir e2, process ~dir e3) + | With (e1, e2) -> With (process ~dir e1, process ~dir e2) + | Assert (e1, e2) -> Assert (process ~dir e1, process ~dir e2) + | Test (e1, es) -> + Test (process ~dir e1, List.(simplify_path es >>| process ~dir)) + | SetLet bs -> SetLet (process_bnds ~dir bs) + | Let (bs, e) -> Let (process_bnds ~dir bs, process ~dir e) + | Val v -> Val (process_val ~dir v) + | Id x -> Id x + | Select (e, es, me) -> + Select + ( process ~dir e, + List.(simplify_path es >>| process ~dir), + Option.(me >>| process ~dir) ) + | Apply (e1, e2) -> Apply (process ~dir e1, process ~dir e2) + | Aquote e -> Aquote (process ~dir e) + +and process_val ~dir = function + | Str (s, ess) -> Str (s, List.(ess >>| fun (e, s) -> (process ~dir e, s))) + | IStr (n, s, ess) -> + let s' = drop_first_empty_line (unindent n s ~skip_first_line:false) + and ess' = + List.map ess ~f:(fun (e, s) -> + (process ~dir e, unindent n s ~skip_first_line:true)) + in + Str (s', ess') + | Lambda (p, e) -> Lambda (process_pattern ~dir p, process ~dir e) + | List es -> List List.(es >>| process ~dir) + | AttSet (r, bs) -> AttSet (r, process_bnds ~dir bs) + | Path p -> ( + if Filename.is_absolute p then Str (p, []) + else + match dir with + | Some dir when Filename.is_absolute dir -> + Str (Filename.concat dir p, []) + | Some _ -> + raise + (ElaborateError "Provided directory should be an absolute path") + | None -> raise (ElaborateError "Do not know how to resolve path")) + | v -> v + +and process_bnds ~dir bs = + bs + |> List.map ~f:(function + | AttrPath (es, e) -> + AttrPath (List.(es >>| process ~dir), process ~dir e) + | Inherit (me, xs) -> + Inherit (Option.(me >>| process ~dir), process_inherit_ids xs)) + |> simplify_bnd_paths + |> List.fold ~init:[] ~f:(fun bs' bnd -> + match bnd with + | AttrPath (path, e) -> insert bs' path e + | Inherit (from, es) -> insert_inherit bs' from es) + +and process_inherit_ids = + List.map ~f:(function + | Id x | Val (Str (x, [])) | Aquote (Val (Str (x, []))) -> Id x + | _ -> raise (ElaborateError "Unexpected expression in inherit")) + +and process_pattern ~dir = function + | Alias x -> Alias x + | ParamSet (mx, (ps, k)) -> ParamSet (mx, (process_param_set ~dir mx ps, k)) + +and process_param_set ~dir ?(seen = String.Set.empty) mx ps = + match ps with + | [] -> [] + | (y, me) :: ps' -> + if Set.mem seen y || Option.mem mx y ~equal:String.( = ) then + raise (ElaborateError "Duplicated function argument") + else + (y, Option.(me >>| process ~dir)) + :: 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 @@ +{ +open Core +open Tokens + +exception Error of string + +(* Types of curly braces. + AQUOTE corresponds to the braces for antiquotation, i.e. '${...}' + and SET to an attribute set '{...}'. + *) +type braces = + | AQUOTE + | SET + +let print_stack s = + let b = Buffer.create 100 in + Buffer.add_string b "[ "; + List.iter s ~f:(function + | AQUOTE -> Buffer.add_string b "AQUOTE; " + | SET -> Buffer.add_string b "SET; " + ); + Buffer.add_string b "]"; + Buffer.contents b + +let token_of_str state buf = + match state with + | `Start -> STR_START (Buffer.contents buf) + | `Mid -> STR_MID (Buffer.contents buf) + +let token_of_istr state buf = + match state with + | `Start -> ISTR_START (Buffer.contents buf) + | `Mid -> ISTR_MID (Buffer.contents buf) + +(* lookup table for one-character tokens *) +let char_table = Array.create ~len:94 EOF +let _ = + List.iter ~f:(fun (k, v) -> Array.set char_table ((int_of_char k) - 1) v) + [ + '.', SELECT; + '?', QMARK; + '!', NOT; + '=', ASSIGN; + '<', LT; + '>', GT; + '[', LBRACK; + ']', RBRACK; + '+', PLUS; + '-', MINUS; + '*', TIMES; + '/', SLASH; + '(', LPAREN; + ')', RPAREN; + ':', COLON; + ';', SEMICOLON; + ',', COMMA; + '@', AS + ] + +(* lookup table for two- and three-character tokens *) +let str_table = Hashtbl.create (module String) ~size:10 +let _ = + List.iter ~f:(fun (kwd, tok) -> Hashtbl.set str_table ~key:kwd ~data:tok) + [ + "//", MERGE; + "++", CONCAT; + "<=", LTE; + ">=", GTE; + "==", EQ; + "!=", NEQ; + "&&", AND; + "||", OR; + "->", IMPL; + "...", ELLIPSIS + ] + +(* lookup table for keywords *) +let keyword_table = Hashtbl.create (module String) ~size:10 +let _ = + List.iter ~f:(fun (kwd, tok) -> Hashtbl.set keyword_table ~key:kwd ~data:tok) + [ "with", WITH; + "rec", REC; + "let", LET; + "in", IN; + "inherit", INHERIT; + "if" , IF; + "then", THEN; + "else", ELSE; + "assert", ASSERT; + "or", ORDEF ] + +(* replace an escape sequence by the corresponding character(s) *) +let unescape = function + | "\\n" -> "\n" + | "\\r" -> "\r" + | "\\t" -> "\t" + | "\\\\" -> "\\" + | "\\${" -> "${" + | "''$" -> "$" + | "$$" -> "$" + | "'''" -> "''" + | "''\\t" -> "\t" + | "''\\r" -> "\r" + | "''\\n" -> "\n" + | x -> + failwith (Printf.sprintf "unescape unexpected arg %s" x) + +let collect_tokens lexer q lexbuf = + let stack = ref [] in + let queue = Stdlib.Queue.create () in + let rec go () = + match (try Some (Stdlib.Queue.take queue) with Stdlib.Queue.Empty -> None) with + | Some token -> + ( + match token, !stack with + | AQUOTE_CLOSE, [] -> + Stdlib.Queue.add AQUOTE_CLOSE q + | EOF, _ -> + Stdlib.Queue.add EOF q; + | _, _ -> + Stdlib.Queue.add token q; + go () + ) + | None -> + lexer queue stack lexbuf; + go () + in + Stdlib.Queue.add AQUOTE_OPEN q; + stack := [AQUOTE]; + lexer queue stack lexbuf; + go () + +(* utility functions *) +let print_position lexbuf = + let pos = Lexing.lexeme_start_p lexbuf in + Printf.sprintf "%s:%d:%d" pos.pos_fname + pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1) + + +let set_filename fname (lexbuf: Lexing.lexbuf) = + let pos = lexbuf.lex_curr_p in + lexbuf.lex_curr_p <- { pos with pos_fname = fname }; lexbuf + +} + +let nzdigit = ['1'-'9'] +let digit = nzdigit | '0' +let float = (nzdigit digit* '.' digit* | '0'? '.' digit+) (['E' 'e'] ['+' '-']? digit+)? +let alpha = ['a'-'z' 'A'-'Z'] +let alpha_digit = alpha | digit +let path_chr = alpha_digit | ['.' '_' '-' '+'] +let path = path_chr* ('/' path_chr+)+ +let spath = alpha_digit path_chr* ('/' path_chr+)* +let uri_chr = ['%' '/' '?' ':' '@' '&' '=' '+' '$' ',' '-' '_' '.' '!' '~' '*' '\''] +let scheme = alpha (alpha | ['+' '-' '.'])* +let uri = scheme ':' (alpha_digit | uri_chr)+ +let char_tokens = ['.' '?' '!' '=' '<' '>' '[' ']' '+' '-' '*' '/' '^' '(' ')' ':' ';' ',' '@'] + +rule get_tokens q s = parse +(* skip whitespeces *) +| [' ' '\t' '\r'] + { get_tokens q s lexbuf } +(* increase line count for new lines *) +| '\n' + { Lexing.new_line lexbuf; get_tokens q s lexbuf } +| char_tokens as c + { Stdlib.Queue.add (Array.get char_table ((int_of_char c) - 1)) q } +| ("//" | "++" | "<=" | ">=" | "==" | "!=" | "&&" | "||" | "->" | "...") as s + { Stdlib.Queue.add (Hashtbl.find_exn str_table s) q} +| digit+ as i + { Stdlib.Queue.add (INT i) q } +| float + { Stdlib.Queue.add (FLOAT (Lexing.lexeme lexbuf)) q } +| path + { Stdlib.Queue.add (PATH (Lexing.lexeme lexbuf)) q } +| '<' (spath as p) '>' + { Stdlib.Queue.add (SPATH p) q } +| '~' path as p + { Stdlib.Queue.add (HPATH p) q } +| uri + { Stdlib.Queue.add(URI (Lexing.lexeme lexbuf)) q } +(* keywords or identifiers *) +| ((alpha | '_')+ (alpha_digit | ['_' '\'' '-'])*) as id + { Stdlib.Queue.add (Hashtbl.find keyword_table id |> Option.value ~default:(ID id)) q} +(* comments *) +| '#' ([^ '\n']* as c) + { ignore c; get_tokens q s lexbuf} +| "/*" + { comment (Buffer.create 64) lexbuf; + get_tokens q s lexbuf + } +(* the following three tokens change the braces stack *) +| "${" + { Stdlib.Queue.add AQUOTE_OPEN q; s := AQUOTE :: !s } +| '{' + { Stdlib.Queue.add LBRACE q; s := SET :: !s } +| '}' + { + match !s with + | AQUOTE :: rest -> + Stdlib.Queue.add AQUOTE_CLOSE q; s := rest + | SET :: rest -> + Stdlib.Queue.add RBRACE q; s := rest + | _ -> + let pos = print_position lexbuf in + let err = Printf.sprintf "Unbalanced '}' at %s\n" pos in + raise (Error err) + } +(* a double-quoted string *) +| '"' + { string `Start (Buffer.create 64) q lexbuf } +(* an indented string *) +| "''" (' '+ as ws) + { istring `Start (Some (String.length ws)) (Buffer.create 64) q lexbuf } +| "''" + { istring `Start None (Buffer.create 64) q lexbuf } +(* End of input *) +| eof + { Stdlib.Queue.add EOF q } +(* any other character raises an exception *) +| _ + { + let pos = print_position lexbuf in + let tok = Lexing.lexeme lexbuf in + let err = Printf.sprintf "Unexpected character '%s' at %s\n" tok pos in + raise (Error err) + } + +(* Nix does not allow nested comments, but it is still handy to lex it + separately because we can properly increase line count. *) +and comment buf = parse + | '\n' + {Lexing.new_line lexbuf; Buffer.add_char buf '\n'; comment buf lexbuf} + | "*/" + { () } + | _ as c + { Buffer.add_char buf c; comment buf lexbuf } + +and string state buf q = parse + | '"' (* terminate when we hit '"' *) + { Stdlib.Queue.add (token_of_str state buf) q; Stdlib.Queue.add STR_END q } + | '\n' + { Lexing.new_line lexbuf; Buffer.add_char buf '\n'; string state buf q lexbuf } + | ("\\n" | "\\r" | "\\t" | "\\\\" | "\\${") as s + { Buffer.add_string buf (unescape s); string state buf q lexbuf } + | "\\" (_ as c) (* add the character verbatim *) + { Buffer.add_char buf c; string state buf q lexbuf } + | "${" (* collect all the tokens till we hit the matching '}' *) + { + Stdlib.Queue.add (token_of_str state buf) q; + collect_tokens get_tokens q lexbuf; + string `Mid (Buffer.create 64) q lexbuf + } + | _ as c (* otherwise just add the character to the buffer *) + { Buffer.add_char buf c; string state buf q lexbuf } + +and istring state imin buf q = parse + | ('\n' ' '* "''") + { + Lexing.new_line lexbuf; + Buffer.add_string buf "\n"; + let indent = match imin with | None -> 0 | Some i -> i in + Stdlib.Queue.add (token_of_istr state buf) q; + Stdlib.Queue.add (ISTR_END indent) q + } + | "''" + { + let indent = match imin with | None -> 0 | Some i -> i in + Stdlib.Queue.add (token_of_istr state buf) q; + Stdlib.Queue.add (ISTR_END indent) q + } + | ('\n' ' '* '\n') as s + { + Lexing.new_line lexbuf; + Lexing.new_line lexbuf; + Buffer.add_string buf s; + istring state imin buf q lexbuf + } + | ('\n' (' '* as ws)) as s + { + Lexing.new_line lexbuf; + Buffer.add_string buf s; + let ws_count = String.length ws in + match imin with + | None -> + istring state (Some ws_count) buf q lexbuf + | Some i -> + istring state (Some (min i ws_count)) buf q lexbuf + } + | ("''$" | "'''" | "''\\t" | "''\\r" | "''\\n") as s + { Buffer.add_string buf (unescape s); istring state imin buf q lexbuf } + | "''\\" (_ as c) + { Buffer.add_char buf c; istring state imin buf q lexbuf } + | "${" + { + Stdlib.Queue.add (token_of_istr state buf) q; + collect_tokens get_tokens q lexbuf; + istring `Mid imin (Buffer.create 64) q lexbuf + } + | _ as c + { Buffer.add_char buf c; istring state imin buf q lexbuf } +{ + +let rec next_token + (q: token Stdlib.Queue.t) + (s: braces list ref) + (lexbuf: Lexing.lexbuf) + : token = + match (try Some (Stdlib.Queue.take q) with | Stdlib.Queue.Empty -> None) with + | Some token -> + token + | None -> + get_tokens q s lexbuf; + next_token q s lexbuf +} 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 @@ +open Core +module Ast = Types +module Printer = Printer + +exception ParseError of string + +let parse ~filename (data : string) = + let lexbuf = Lexer.set_filename filename (Lexing.from_string data) + and q, s = (Stdlib.Queue.create (), ref []) in + try Parser.main (Lexer.next_token q s) lexbuf with + | Lexer.Error msg -> + let msg' = String.rstrip msg in + raise (ParseError (sprintf "Lexing error: %s" msg')) + | Parser.Error -> + let msg = sprintf "Parse error at %s" (Lexer.print_position lexbuf) in + raise (ParseError msg) + +let elaborate = Elaborator.process + +exception 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 @@ +/* Tokens with data */ +%token INT +%token FLOAT +/* A path */ +%token PATH +/* Search path, enclosed in <> */ +%token SPATH +/* Home path, starts with ~ */ +%token HPATH +%token URI +%token STR_START +%token STR_MID +%token STR_END +%token ISTR_START +%token ISTR_MID +%token ISTR_END +%token ID +/* Tokens that stand for themselves */ +%token SELECT "." +%token QMARK "?" +%token CONCAT "++" +%token NOT "!" +%token MERGE "//" +%token ASSIGN "=" +%token LT "<" +%token LTE "<=" +%token GT ">" +%token GTE ">=" +%token EQ "==" +%token NEQ "!=" +%token AND "&&" +%token OR "||" +%token IMPL "->" +%token AQUOTE_OPEN "${" +%token AQUOTE_CLOSE "}$" +%token LBRACE "{" +%token RBRACE "}" +%token LBRACK "[" +%token RBRACK "]" +%token PLUS "+" +%token MINUS "-" +%token TIMES "*" +%token SLASH "/" +%token LPAREN "(" +%token RPAREN ")" +%token COLON ":" +%token SEMICOLON ";" +%token COMMA "," +%token ELLIPSIS "..." +%token AS "@" +/* Keywords */ +%token WITH "with" +%token REC "rec" +%token LET "let" +%token IN "in" +%token INHERIT "inherit" +%token IF "if" +%token THEN "then" +%token ELSE "else" +%token ASSERT "assert" +%token ORDEF "or" + +/* End of input */ +%token EOF + +%{ + open Types +%} + +%start main + +%% + +main: +| e = expr0 EOF + { e } + +expr0: +| "if"; e1 = expr0; "then"; e2 = expr0; "else"; e3 = expr0 + { Cond (e1, e2, e3) } +| "with"; e1 = expr0; ";"; e2 = expr0 + { With (e1, e2) } +| "assert"; e1 = expr0; ";"; e2 = expr0 + { Assert (e1, e2) } +| "let"; xs = delimited("{", list(binding), "}") + { SetLet xs } +| "let"; xs = list(binding); "in"; e = expr0 + { Let (xs, e) } +| l = lambda + { Val l } +| e = expr1 + { e } + +/* Rules expr1-expr14 are almost direct translation of the operator + precedence table: + https://nixos.org/nix/manual/#sec-language-operators */ + +%inline binary_expr(Lhs, Op, Rhs): +| lhs = Lhs; op = Op; rhs = Rhs + { BinaryOp (op, lhs, rhs) } + +expr1: +| e = binary_expr(expr2, "->" {Impl}, expr1) +| e = expr2 + { e } + +expr2: +| e = binary_expr(expr2, "||" {Or}, expr3) +| e = expr3 + { e } + +expr3: +| e = binary_expr(expr3, "&&" {And}, expr4) +| e = expr4 + { e } + +%inline expr4_ops: +| "==" { Eq } +| "!=" { Neq } + +expr4: +| e = binary_expr(expr5, expr4_ops, expr5) +| e = expr5 + { e } + +%inline expr5_ops: +| "<" { Lt } +| ">" { Gt } +| "<=" { Lte } +| ">=" { Gte } + +expr5: +| e = binary_expr(expr6, expr5_ops, expr6) +| e = expr6 + { e } + +expr6: +| e = binary_expr(expr7, "//" {Merge}, expr6) +| e = expr7 + { e } + +expr7: +| e = preceded("!", expr7) + { UnaryOp (Not, e) } +| e = expr8 + { e } + +%inline expr8_ops: +| "+" { Plus } +| "-" { Minus } + +expr8: +| e = binary_expr(expr8, expr8_ops, expr9) +| e = expr9 + { e } + +%inline expr9_ops: +| "*" { Mult } +| "/" { Div } + +expr9: +| e = binary_expr(expr9, expr9_ops, expr10) +| e = expr10 + { e } + +expr10: +| e = binary_expr(expr11, "++" {Concat}, expr10) +| e = expr11 + { e } + +expr11: +| e = expr12 "?" p = attr_path + { Test (e, p) } +| e = expr12 + { e } + +expr12: +| e = preceded("-", expr13) + { UnaryOp (Negate, e) } +| e = expr13 + { e } + +expr13: +| f = expr13; arg = expr14 + { Apply (f, arg) } +| e = expr14 + { e } + +%inline selectable: +| s = set + { Val s } +| id = ID + { Id id } +| e = delimited("(", expr0, ")") + { e } + +expr14: +| e = selectable; "."; p = attr_path; o = option(preceded("or", expr14)) + { Select (e, p, o) } +| e = atomic_expr; "or" + { Apply (e, Id "or") } +| e = atomic_expr + { e } + +atomic_expr: +| id = ID + { Id id } +| v = value + { Val v } +| e = delimited("(", expr0, ")") + { e } + +attr_path: +| p = separated_nonempty_list(".", attr_path_component) + { p } + +attr_path_component: +| "or" + { Id "or" } +| id = ID + { Id id } +| e = delimited("${", expr0, "}$") + { Aquote e } +| s = str + { Val s } + +value: +| s = str + { s } +| s = istr + { s } +| i = INT + {Int i} +| f = FLOAT + { Float f } +| p = PATH + { Path p } +| sp = SPATH + { SPath sp } +| hp = HPATH + { HPath hp } +| uri = URI + { Uri uri } +| l = nixlist + { l } +| s = set + { s } + +%inline str_mid(X): +| xs = list(pair(delimited("${", expr0, "}$"), X)) { xs } + +/* Double-quoted string */ +str: +| start = STR_START; mids = str_mid(STR_MID); STR_END + { Str (start, mids) } + +/* Indented string */ +istr: +| start = ISTR_START; mids = str_mid(ISTR_MID); i = ISTR_END + { IStr (i, start, mids) } + +/* Lists and sets */ +nixlist: +| xs = delimited("[", list(expr14), "]") + { List xs } + +empty_set: +| "{"; "}" {} + +set: +| empty_set + { AttSet (Nonrec, []) } +| xs = delimited("{", nonempty_list(binding), "}") + { AttSet (Nonrec, xs) } +| xs = preceded("rec", delimited("{", list(binding), "}")) + { AttSet (Rec, xs) } + +binding: +| kv = terminated(separated_pair(attr_path, "=", expr0), ";") + { let (k, v) = kv in AttrPath (k, v) } +| xs = delimited("inherit", pair(option(delimited("(", expr0, ")")), list(attr_path_component)), ";") + { let (prefix, ids) = xs in Inherit (prefix, ids) } + +lambda: +| id = ID; "@"; p = param_set; ":"; e = expr0 + { Lambda (ParamSet (Some id, p), e) } +| p = param_set; "@"; id = ID; ":"; e = expr0 + { Lambda (ParamSet (Some id, p), e) } +| p = param_set; ":"; e = expr0 + { Lambda (ParamSet (None, p), e) } +| id = ID; ":"; e = expr0 + { Lambda (Alias id, e) } + +%inline param_set: +| empty_set + { ([], Exact) } +| "{"; "..."; "}" + { ([], Loose) } +| ps = delimited("{", pair(pair(params, ","?), boption("...")), "}") + { let ((ps, _), ellipsis) = ps in (ps, if ellipsis then Loose else Exact) } + +params: +| p = param + { [p] } +| ps = params; ","; p = param + { ps @ [p] } + +%inline param: +p = pair(ID, option(preceded("?", expr0))) + { 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 @@ +open Core +open Types +open PPrint + +let rec escape_chlist = function + | [] -> [] + | '$' :: '{' :: l' -> '\\' :: '$' :: '{' :: escape_chlist l' + | '\n' :: l' -> '\\' :: 'n' :: escape_chlist l' + | '\r' :: l' -> '\\' :: 'r' :: escape_chlist l' + | '\t' :: l' -> '\\' :: 't' :: escape_chlist l' + | '\\' :: l' -> '\\' :: '\\' :: escape_chlist l' + | '"' :: l' -> '\\' :: '"' :: escape_chlist l' + | c :: l' -> c :: escape_chlist l' + +let escape_string s = s |> String.to_list |> escape_chlist |> String.of_list +let out_width = ref 80 +let set_width i = out_width := i +let indent = ref 2 +let set_indent i = indent := i + +let rec doc_of_expr = function + | BinaryOp (op, lhs, rhs) -> + let lhs_doc = maybe_parens_bop op `Left lhs + and rhs_doc = maybe_parens_bop op `Right rhs in + infix !indent 1 (doc_of_bop op) lhs_doc rhs_doc + | UnaryOp (op, e) -> precede (doc_of_uop op) (maybe_parens (prec_of_uop op) e) + | Cond (e1, e2, e3) -> + surround !indent 1 + (soft_surround !indent 1 (string "if") (doc_of_expr e1) (string "then")) + (doc_of_expr e2) + (string "else" ^^ nest !indent (break 1 ^^ doc_of_expr e3)) + | With (e1, e2) -> + flow (break 1) [ string "with"; doc_of_expr e1 ^^ semi; doc_of_expr e2 ] + | Assert (e1, e2) -> + flow (break 1) [ string "assert"; doc_of_expr e1 ^^ semi; doc_of_expr e2 ] + | Test (e, path) -> + maybe_parens 4 e ^^ space ^^ string "?" + ^^ group (break 1 ^^ separate_map dot doc_of_expr path) + | SetLet bs -> + surround !indent 1 + (string "let " ^^ lbrace) + (group (separate_map (break 1) doc_of_binding bs)) + rbrace + | Let (bs, e) -> + surround !indent 1 (string "let") + (separate_map (break 1) doc_of_binding bs) + (prefix !indent 1 (string "in") (doc_of_expr e)) + | Val v -> doc_of_val v + | Id id -> string id + | Select (e, path, oe) -> + maybe_parens 1 e ^^ dot ^^ doc_of_attpath path + ^^ optional + (fun e -> + space ^^ string "or" ^^ nest !indent (break 1 ^^ maybe_parens 1 e)) + oe + | Apply (e1, e2) -> prefix !indent 1 (maybe_parens 2 e1) (maybe_parens 2 e2) + | Aquote e -> surround !indent 0 (string "${") (doc_of_expr e) (string "}") + +and maybe_parens lvl e = + if prec_of_expr e >= lvl then surround !indent 0 lparen (doc_of_expr e) rparen + else doc_of_expr e + +and maybe_parens_bop op (loc : [ `Left | `Right ]) e = + match (loc, assoc_of_bop op) with + | (`Left, Some Left | `Right, Some Right) + when prec_of_expr e >= prec_of_bop op -> + doc_of_expr e + | _, _ -> maybe_parens (prec_of_bop op) e + +and doc_of_attpath path = separate_map dot doc_of_expr path + +and doc_of_paramset (params, kind) = + let ps = + List.map ~f:doc_of_param params + @ if Poly.(kind = Loose) then [ string "..." ] else [] + in + surround !indent 0 lbrace (separate (comma ^^ break 1) ps) rbrace + +and doc_of_param (id, oe) = + string id ^^ optional (fun e -> qmark ^^ space ^^ doc_of_expr e) oe + +and doc_of_binding = function + | AttrPath (path, e) -> + doc_of_attpath path ^^ space ^^ equals ^^ space ^^ doc_of_expr e ^^ semi + | Inherit (oe, ids) -> + let id_docs = + List.map + ~f:(function + | Id x | Val (Str (x, [])) -> string x | _ -> assert false) + ids + in + let xs = + flow (break 1) + (match oe with + | Some e -> parens (doc_of_expr e) :: id_docs + | None -> id_docs) + in + soft_surround !indent 0 (string "inherit" ^^ space) xs semi + +and doc_of_bop = function + | Plus -> plus + | Minus -> minus + | Mult -> star + | Div -> slash + | Gt -> rangle + | Lt -> langle + | Lte -> string "<=" + | Gte -> string ">=" + | Eq -> string "==" + | Neq -> string "!=" + | Or -> string "||" + | And -> string "&&" + | Impl -> string "->" + | Merge -> string "//" + | Concat -> string "++" + +and doc_of_uop = function Negate -> minus | Not -> bang + +and doc_of_val = function + | Str (start, xs) -> + dquotes + (string (escape_string start) + ^^ concat + (List.map + ~f:(fun (e, s) -> + surround !indent 0 (string "${") (doc_of_expr e) + (string "}" ^^ string (escape_string s))) + xs)) + | IStr (i, start, xs) -> + let qq = string "''" in + let str s = + String.split ~on:'\n' s + |> List.map ~f:(fun s -> + let len = String.length s in + let s' = + if len >= i then String.sub s ~pos:i ~len:(len - i) else s + in + string s') + |> separate hardline + in + enclose qq qq + (str start + ^^ concat + (List.map + ~f:(fun (e, s) -> + enclose (string "${") rbrace (doc_of_expr e) ^^ str s) + xs)) + | Int x | Float x | Path x | SPath x | HPath x | Uri x -> string x + | Lambda (pattern, body) -> + let pat = + match pattern with + | Alias id -> string id + | ParamSet (None, ps) -> doc_of_paramset ps + | ParamSet (Some id, ps) -> + doc_of_paramset ps ^^ group (break 1 ^^ at ^^ break 1 ^^ string id) + in + flow (break 1) [ pat ^^ colon; doc_of_expr body ] + | List [] -> lbracket ^^ space ^^ rbracket + | List es -> + surround !indent 1 lbracket + (separate_map (break 1) (maybe_parens 2) es) + rbracket + | AttSet (Nonrec, []) -> lbrace ^^ space ^^ rbrace + | AttSet (Nonrec, bs) -> + surround !indent 1 lbrace + (group (separate_map (break 1) doc_of_binding bs)) + rbrace + | AttSet (Rec, bs) -> + string "rec" ^^ space ^^ doc_of_val (AttSet (Nonrec, bs)) + +let print chan expr = ToChannel.pretty 0.7 !out_width chan (doc_of_expr expr) + +let to_string expr = + let buf = Stdlib.Buffer.create 0 in + ToBuffer.pretty 0.7 !out_width buf (doc_of_expr expr); + 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 @@ +type token = + (* Tokens with data *) + | INT of string + | FLOAT of string + (* A path (starting with / or ./) *) + | PATH of string + (* Search path, enclosed in < and > *) + | SPATH of string + (* Home path, starting with ~/ *) + | HPATH of string + | URI of string + | STR_START of string + | STR_MID of string + | STR_END + | ISTR_START of string + | ISTR_MID of string + | ISTR_END of int + | ID of string + (* Tokens that stand for themselves *) + | SELECT + | QMARK + | CONCAT + | NOT + | MERGE + | ASSIGN + | LT + | LTE + | GT + | GTE + | EQ + | NEQ + | AND + | OR + | IMPL + | AQUOTE_OPEN + | AQUOTE_CLOSE + | LBRACE + | RBRACE + | LBRACK + | RBRACK + | PLUS + | MINUS + | TIMES + | SLASH + | LPAREN + | RPAREN + | COLON + | SEMICOLON + | COMMA + | ELLIPSIS + | AS + (* Keywords *) + | WITH + | REC + | LET + | IN + | INHERIT + | IF + | THEN + | ELSE + | ASSERT + | ORDEF + (* End of input *) + | 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 @@ +open Core + +(* Binary operators *) +type binary_op = + | Plus + | Minus + | Mult + | Div + | Gt + | Lt + | Lte + | Gte + | Eq + | Neq + | Or + | And + | Impl + | Merge + | Concat +[@@deriving sexp_of] + +(* Unary operators *) +type unary_op = Negate | Not [@@deriving sexp_of] + +(* The top-level expression type *) +type expr = + | BinaryOp of binary_op * expr * expr + | UnaryOp of unary_op * expr + | Cond of expr * expr * expr + | With of expr * expr + | Assert of expr * expr + | Test of expr * expr list + | SetLet of binding list + | Let of binding list * expr + | Val of value + | Id of id + | Select of expr * expr list * expr option + | Apply of expr * expr + | Aquote of expr +[@@deriving sexp_of] + +(* Possible values *) +and value = + (* Str is a string start, followed by arbitrary number of antiquotations and + strings that separate them *) + | Str of string * (expr * string) list + (* IStr is an indented string, so it has the extra integer component which + indicates the indentation *) + | IStr of int * string * (expr * string) list + | Int of string + | Float of string + | Path of string + | SPath of string + | HPath of string + | Uri of string + | Lambda of pattern * expr + | List of expr list + | AttSet of recursivity * binding list +[@@deriving sexp_of] + +(* Patterns in lambda definitions *) +and pattern = Alias of id | ParamSet of id option * param_set +[@@deriving sexp_of] + +and param_set = param list * match_kind [@@deriving sexp_of] +and param = id * expr option [@@deriving sexp_of] +and recursivity = Rec | Nonrec +and match_kind = Exact | Loose + +(* Bindings in attribute sets and let expressions *) +and binding = + (* The first expr should be attrpath, which is the same as in Select *) + | AttrPath of expr list * expr + | Inherit of expr option * expr list +[@@deriving sexp_of] + +(* Identifiers *) +and id = string + +(* Precedence levels of binary operators *) +let prec_of_bop = function + | Concat -> 5 + | Mult | Div -> 6 + | Plus | Minus -> 7 + | Merge -> 9 + | Gt | Lt | Lte | Gte -> 10 + | Eq | Neq -> 11 + | And -> 12 + | Or -> 13 + | Impl -> 14 + +type assoc = Left | Right + +let assoc_of_bop = function + | Mult | Div | Plus | Minus -> Some Left + | Concat | Merge | And | Or -> Some Right + | Gt | Lt | Lte | Gte | Eq | Neq | Impl -> None + +(* Precedence levels of unary operators *) +let prec_of_uop = function Negate -> 3 | Not -> 8 + +(* Precedence level of expressions + (assuming that the constituents have higher levels) *) +let prec_of_expr = function + | Val (Lambda _) -> 15 + | Val _ | Id _ | Aquote _ -> 0 + | BinaryOp (op, _, _) -> prec_of_bop op + | UnaryOp (op, _) -> prec_of_uop op + | Cond _ | With _ | Assert _ | Let _ | SetLet _ -> 15 + | Test _ -> 4 + | Select _ -> 1 + | Apply _ -> 2 -- cgit v1.2.3