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/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 ++++++++++++++++++++++++ 10 files changed, 1042 insertions(+) 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 (limited to 'lib/mininix') 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") -- cgit v1.2.3