aboutsummaryrefslogtreecommitdiffstats
path: root/bin
diff options
context:
space:
mode:
authorRutger Broekhoff2025-07-07 21:52:08 +0200
committerRutger Broekhoff2025-07-07 21:52:08 +0200
commitba61dfd69504ec6263a9dee9931d93adeb6f3142 (patch)
treed6c9b78e50eeab24e0c1c09ab45909a6ae3fd5db /bin
downloadverified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.tar.gz
verified-dyn-lang-interp-ba61dfd69504ec6263a9dee9931d93adeb6f3142.zip
Initialize repository
Diffstat (limited to 'bin')
-rw-r--r--bin/dune14
-rw-r--r--bin/main.ml26
-rw-r--r--bin/repl.ml52
-rw-r--r--bin/repl_cmd.ml178
-rw-r--r--bin/run.ml163
-rw-r--r--bin/settings.ml120
6 files changed, 553 insertions, 0 deletions
diff --git a/bin/dune b/bin/dune
new file mode 100644
index 0000000..2a56b29
--- /dev/null
+++ b/bin/dune
@@ -0,0 +1,14 @@
1(executable
2 (public_name mininix)
3 (name main)
4 (preprocess
5 (pps ppx_let))
6 (libraries
7 nix
8 core
9 core_unix.command_unix
10 linenoise
11 mininix
12 sexp_pretty
13 stdio
14 ppx_let))
diff --git a/bin/main.ml b/bin/main.ml
new file mode 100644
index 0000000..e4ca4b9
--- /dev/null
+++ b/bin/main.ml
@@ -0,0 +1,26 @@
1open Core
2
3let repl =
4 Command.basic ~summary:"run the Mininix REPL" (Command.Param.return Repl.run)
5
6let eval =
7 Command.basic ~summary:"run a Nix file"
8 (let%map_open.Command filename = anon ("FILENAME" %: string)
9 and strict = flag "strict" no_arg ~doc:"use deep evaluation strategy"
10 and importsdef =
11 flag "importsdef" (optional string) ~doc:"import tree definition file"
12 in
13 fun () ->
14 Settings.opts.eval_strategy := if strict then `Deep else `Shallow;
15 Settings.opts.imports_def_file := importsdef;
16 let ok =
17 if String.(filename = "-") then Run.eval_stdin ()
18 else Run.eval_file filename
19 in
20 if ok then exit 0 else exit 1)
21
22let main =
23 Command.group ~summary:"the Mininix interpreter"
24 [ ("repl", repl); ("eval", eval) ]
25
26let () = Command_unix.run main
diff --git a/bin/repl.ml b/bin/repl.ml
new file mode 100644
index 0000000..092c503
--- /dev/null
+++ b/bin/repl.ml
@@ -0,0 +1,52 @@
1open Core
2open Option.Let_syntax
3
4let ok = ref true
5let opts = Settings.opts
6
7let rec user_input cb =
8 let prompt = (if !ok then "[okay]" else "[fail]") ^ " (mini)nix> " in
9 try
10 match LNoise.linenoise prompt with
11 | None -> ()
12 | Some v ->
13 cb v;
14 user_input cb
15 with Sys_unix.Break ->
16 printf "\n%!";
17 user_input cb
18
19let split_cmd_prefix cmd =
20 let%bind cmd = String.chop_prefix ~prefix:":" cmd in
21 let cmd' = Repl_cmd.lstrip_space cmd in
22 let space = String.chop_suffix_exn cmd ~suffix:cmd' in
23 return (":" ^ space, cmd')
24
25let handle_cmd cmd =
26 let cmd = Repl_cmd.strip_space cmd in
27 (match split_cmd_prefix cmd with
28 | Some (_, cmd) -> ok := Repl_cmd.invoke cmd
29 | None ->
30 if String.(strip cmd <> "") then
31 ok := Run.eval_expr cmd ~origin:Interactive);
32 printf "\n%!"
33
34let run () =
35 LNoise.set_multiline true;
36 LNoise.history_load ~filename:"mininix_history" |> ignore;
37 LNoise.history_set ~max_length:500 |> ignore;
38 LNoise.set_hints_callback (fun line ->
39 let%bind _, cmd = split_cmd_prefix line in
40 let%bind hint = Repl_cmd.hint cmd in
41 return (hint, LNoise.Yellow, true));
42 LNoise.set_completion_callback (fun line_so_far completions ->
43 match split_cmd_prefix line_so_far with
44 | Some (prefix, cmd_so_far) ->
45 Repl_cmd.complete cmd_so_far
46 |> List.map ~f:(String.append prefix)
47 |> List.iter ~f:(LNoise.add_completion completions)
48 | None -> ());
49 user_input (fun from_user ->
50 LNoise.history_add from_user |> ignore;
51 LNoise.history_save ~filename:"mininix_history" |> ignore;
52 handle_cmd from_user)
diff --git a/bin/repl_cmd.ml b/bin/repl_cmd.ml
new file mode 100644
index 0000000..9ebeae7
--- /dev/null
+++ b/bin/repl_cmd.ml
@@ -0,0 +1,178 @@
1open Core
2open Option.Let_syntax
3
4let join_str_list ~sep = function
5 | [] -> ""
6 | s :: ss -> List.fold ss ~init:s ~f:(fun acc s -> acc ^ sep ^ s)
7
8type cmd = {
9 args : string;
10 opts : unit -> string list;
11 next : (string -> (string, cmd) Either.t) option;
12 call : string list -> bool;
13}
14
15let set_opt_cmd opt setting =
16 {
17 args = "<option value>";
18 opts = (fun () -> Settings.allowed_values setting);
19 next = None;
20 call =
21 (fun args ->
22 match Settings.set_to setting args with
23 | None -> true
24 | Some msg ->
25 printf "Failed to set option %s: %s\n%!" opt msg;
26 false);
27 }
28
29let set_cmd =
30 {
31 args = "<option name> <option value>";
32 opts = (fun () -> Map.keys Settings.settings);
33 next =
34 Some
35 (fun opt ->
36 match Map.find Settings.settings opt with
37 | Some setting -> Second (set_opt_cmd opt setting)
38 | None -> First (sprintf "Unknown option '%s'" opt));
39 call =
40 (fun _ ->
41 printf "Missing option argument value\n%!";
42 false);
43 }
44
45let settings_cmd =
46 {
47 args = "";
48 opts = (fun () -> []);
49 next = None;
50 call =
51 (function
52 | [] ->
53 Settings.print ();
54 true
55 | _ ->
56 printf "Expected no arguments\n%!";
57 false);
58 }
59
60let run_cmd =
61 {
62 args = "<filename>";
63 opts = (fun () -> []);
64 next = None;
65 call =
66 (function
67 | [ filename ] -> Run.eval_file filename
68 | _ ->
69 printf "Expected one argument (the filename)\n%!";
70 false);
71 }
72
73let quit_cmd =
74 { args = ""; opts = (fun () -> []); next = None; call = (fun _ -> exit 0) }
75
76let commands =
77 Map.of_alist_exn
78 (module String)
79 [
80 ("quit", quit_cmd);
81 ("set", set_cmd);
82 ("settings", settings_cmd);
83 ("run", run_cmd);
84 ]
85
86let root_cmd =
87 {
88 args = "<command>";
89 opts = (fun () -> Map.keys commands);
90 next =
91 Some
92 (fun cmd_name ->
93 match Map.find commands cmd_name with
94 | Some cmd -> Second cmd
95 | None ->
96 First
97 (sprintf "Unknown command '%s' (expected one of {%s})" cmd_name
98 (Map.keys commands |> join_str_list ~sep:", ")));
99 call =
100 (fun _ ->
101 printf "Missing command!\n%!";
102 false);
103 }
104
105let is_space = Char.( = ) ' '
106let strip_space = String.strip ~drop:is_space
107let lstrip_space = String.lstrip ~drop:is_space
108
109let clean_str_list ss =
110 ss |> List.map ~f:strip_space
111 |> List.filter ~f:(fun s -> not (String.is_empty s))
112
113let words s = s |> String.split ~on:' ' |> clean_str_list
114let unwords ss = clean_str_list ss |> join_str_list ~sep:" "
115
116let rec call cmd args =
117 match args with
118 | [] -> cmd.call []
119 | arg0 :: argn -> (
120 match cmd.next with
121 | None -> cmd.call args
122 | Some next -> (
123 match next arg0 with
124 | First msg ->
125 printf "%s\n%!" msg;
126 false
127 | Second cmd' -> call cmd' argn))
128
129let try_lsplit2_space s =
130 match String.lsplit2 s ~on:' ' with Some (l, r) -> (l, r) | None -> (s, "")
131
132let lsplit2_space' s =
133 let%bind l, r = String.lsplit2 s ~on:' ' in
134 (* s = l ^ " " ^ r *)
135 let r' = lstrip_space r in
136 let space = " " ^ String.chop_suffix_exn r ~suffix:r' in
137 (* s = l ^ space ^ r' *)
138 return (l, space, r')
139
140let rec completions cmd args =
141 (* cmd|<TAB> -> options
142 cmd|abc<TAB> -> options with prefix 'abc'
143 cmd|abc .*<TAB> -> subcommand 'abc' options, pass .* *)
144 if String.(args = "") then cmd.opts ()
145 else
146 match lsplit2_space' args with
147 | None -> cmd.opts () |> List.filter ~f:(String.is_prefix ~prefix:args)
148 | Some (arg0, space, argn) -> (
149 match cmd.next with
150 | None -> []
151 | Some next -> (
152 match next arg0 with
153 | First _ -> []
154 | Second cmd' ->
155 completions cmd' argn
156 |> List.map ~f:(String.append (arg0 ^ space))))
157
158let rec hints cmd args =
159 (* cmd: "" -> " <args>"
160 cmd: "<space>+" -> "<args>"
161 cmd: "<space>+<subcmd>" -> "<hints for subcmd>"
162 cmd: "<space>+<subcmd> .*" -> "<hints for subcmd with .*>" *)
163 if String.(args = "") then Some (" " ^ cmd.args)
164 else if String.(strip_space args = "") then Some cmd.args
165 else
166 let args = lstrip_space args in
167 let%bind next = cmd.next in
168 match lsplit2_space' args with
169 | None ->
170 let%bind cmd' = next args |> Either.Second.to_option in
171 hints cmd' ""
172 | Some (arg0, space, argn) ->
173 let%bind cmd' = next arg0 |> Either.Second.to_option in
174 hints cmd' (space ^ argn)
175
176let invoke cmd = call root_cmd (words cmd)
177let complete cmd = completions root_cmd cmd
178let hint cmd = hints root_cmd cmd
diff --git a/bin/run.ml b/bin/run.ml
new file mode 100644
index 0000000..f39997c
--- /dev/null
+++ b/bin/run.ml
@@ -0,0 +1,163 @@
1open Core
2
3let opts = Settings.opts
4
5module Origin = struct
6 type t = Filename of string | Stdin | Interactive
7
8 let to_string = function
9 | Filename name -> name
10 | Stdin -> "<stdin>"
11 | Interactive -> "<interactive>"
12end
13
14(* [dir] must be an absolute path *)
15let rec find_imports_file dir : (string, string) result =
16 let def_filename = Filename.concat dir "importdef.sexp" in
17 match Core_unix.access def_filename [ `Read ] with
18 | Ok () -> Ok def_filename
19 | Error (Core_unix.Unix_error (ENOENT, _, _))
20 | Error (Core_unix.Unix_error (EACCES, _, _)) ->
21 let parent = Filename.dirname dir in
22 if String.(parent = dir) then Error "Could not find importdef.sexp file"
23 else find_imports_file (Filename.dirname dir)
24 | Error _ -> Error "Could not find importdef.sexp file"
25
26let load_imports ~for_ =
27 let cwd = Core_unix.getcwd () in
28 let filename =
29 match !(opts.imports_def_file) with
30 | None -> (
31 let dir =
32 match for_ with
33 | Origin.Filename filename ->
34 Filename.to_absolute_exn
35 (Filename.dirname filename)
36 ~relative_to:cwd
37 | Origin.Stdin | Origin.Interactive -> cwd
38 in
39 match find_imports_file dir with
40 | Error _ ->
41 printf
42 "Note: no importdef.sexp was found / could be accessed; imports \
43 will not work\n\
44 %!";
45 None
46 | Ok filename ->
47 let relative =
48 if Filename.is_absolute filename then
49 Filename.of_absolute_exn filename ~relative_to:cwd
50 else filename
51 in
52 printf "Imports definition found at %s\n%!" relative;
53 Some filename)
54 | Some filename -> Some filename
55 in
56 match filename with
57 | None -> Ok []
58 | Some filename -> (
59 (* User-provided filenames may not be absolute *)
60 let filename_abs = Filename.to_absolute_exn filename ~relative_to:cwd in
61 try
62 Ok
63 (In_channel.read_all filename
64 |> Sexp.of_string |> Mininix.Sexp.import_forest_of_sexp
65 |> Mininix.Import.materialize
66 ~relative_to:(Filename.dirname filename_abs))
67 with Sys_error err -> Error ("Failed to read imports definition: " ^ err))
68
69let eval_expr_with_imports ~origin ~imports data =
70 let cwd = Core_unix.getcwd () in
71 let config = Sexp_pretty.Config.default
72 and formatter = Stdlib.Format.formatter_of_out_channel stdout in
73 try
74 if !(opts.print_input) then printf "==> Input Nix:\n%s\n\n%!" data;
75 let nexp = Nix.parse ~filename:(Origin.to_string origin) data in
76 if !(opts.print_parsed) then (
77 print_string "==> Parsed Nix:\n";
78 Nix.Printer.print stdout nexp;
79 printf "\n\n%!");
80 let nnexp =
81 Nix.elaborate
82 ~dir:
83 (Some
84 (match origin with
85 | Filename name ->
86 Filename.to_absolute_exn ~relative_to:cwd
87 (Filename.dirname name)
88 | Stdin | Interactive -> cwd))
89 nexp
90 in
91 if !(opts.print_elaborated) then (
92 print_string "==> Parsed, elaborated Nix:\n";
93 Nix.Printer.print stdout nnexp;
94 printf "\n\n%!");
95 if !(opts.print_nix_sexp) then (
96 let nsexp = Nix.Ast.sexp_of_expr nnexp in
97 print_string "==> Nix S-expr:\n";
98 Sexp_pretty.pp_formatter config formatter nsexp;
99 printf "\n%!");
100 let mnexp = Mininix.Nix2mininix.from_nix nnexp in
101 if !(opts.print_mininix_sexp) then (
102 let mnsexp = Mininix.Sexp.expr_to_sexp mnexp in
103 print_string "==> Mininix S-expr:\n";
104 Sexp_pretty.pp_formatter config formatter mnsexp;
105 printf "\n%!");
106 let mnwpexp = Mininix.apply_prelude mnexp in
107 if !(opts.print_mininix_sexp_w_prelude) then (
108 let mnwpsexp = Mininix.Sexp.expr_to_sexp mnwpexp in
109 print_string "==> Mininix S-expr (+ prelude):\n";
110 Sexp_pretty.pp_formatter config formatter mnwpsexp;
111 printf "\n%!");
112 let res =
113 Mininix.interp_tl ~fuel:!(opts.fuel_amount) ~mode:!(opts.eval_strategy)
114 ~imports mnwpexp
115 in
116 if !(opts.print_result_mininix_sexp) then (
117 let ressexp = Mininix.Sexp.val_res_to_sexp res in
118 print_string "==> Evaluation result (Mininix S-exp):\n";
119 Sexp_pretty.pp_formatter config formatter ressexp;
120 printf "\n%!");
121 match res with
122 | Res (Some v) ->
123 let nixv = Mininix.Mininix2nix.from_val v in
124 if !(opts.print_result_nix_sexp) then (
125 let nixvsexp = Nix.Ast.sexp_of_expr nixv in
126 print_string "==> Evaluation result (Nix S-exp):\n";
127 Sexp_pretty.pp_formatter config formatter nixvsexp;
128 printf "\n%!");
129 print_string "==> Evaluation result (Nix):\n";
130 Nix.Printer.print stdout nixv;
131 printf "\n%!";
132 true
133 | Res None ->
134 printf "Failed to evaluate\n%!";
135 false
136 | _ ->
137 printf "Ran out of fuel\n%!";
138 false
139 with
140 | Nix.ParseError msg ->
141 printf "Failed to parse: %s\n%!" msg;
142 false
143 | Nix.ElaborateError msg ->
144 printf "Elaboration failed: %s\n%!" msg;
145 false
146 | Mininix.Nix2mininix.FromNixError msg ->
147 printf "Failed to convert Nix to Mininix: %s\n%!" msg;
148 false
149
150let eval_expr ~origin data =
151 match load_imports ~for_:origin with
152 | Ok imports -> eval_expr_with_imports ~origin ~imports data
153 | Error msg ->
154 print_endline msg;
155 false
156
157let eval_ch ~origin ch = In_channel.input_all ch |> eval_expr ~origin
158
159let eval_file filename =
160 In_channel.with_file filename ~binary:true
161 ~f:(eval_ch ~origin:(Filename filename))
162
163let eval_stdin () = eval_ch In_channel.stdin ~origin:Stdin
diff --git a/bin/settings.ml b/bin/settings.ml
new file mode 100644
index 0000000..55699ee
--- /dev/null
+++ b/bin/settings.ml
@@ -0,0 +1,120 @@
1open Core
2
3type fuel_amount = [ `Limited | `Unlimited ]
4type eval_strategy = [ `Shallow | `Deep ]
5
6type options = {
7 eval_strategy : eval_strategy ref;
8 fuel_amount : fuel_amount ref;
9 imports_def_file : string option ref;
10 print_input : bool ref;
11 print_parsed : bool ref;
12 print_elaborated : bool ref;
13 print_nix_sexp : bool ref;
14 print_mininix_sexp : bool ref;
15 print_mininix_sexp_w_prelude : bool ref;
16 print_result_mininix_sexp : bool ref;
17 print_result_nix_sexp : bool ref;
18}
19
20let opts =
21 {
22 eval_strategy = ref `Deep;
23 fuel_amount = ref `Unlimited;
24 imports_def_file = ref None;
25 print_input = ref false;
26 print_parsed = ref false;
27 print_elaborated = ref false;
28 print_nix_sexp = ref false;
29 print_mininix_sexp = ref false;
30 print_mininix_sexp_w_prelude = ref false;
31 print_result_mininix_sexp = ref false;
32 print_result_nix_sexp = ref false;
33 }
34
35type 'a setter = 'a -> unit
36
37type setting =
38 | BoolSetting of bool ref
39 | EvalStrategySetting of eval_strategy ref
40 | FilenameOptionSetting of string option ref
41 | FuelAmountSetting of fuel_amount ref
42
43let allowed_values s =
44 match s with
45 | BoolSetting _ -> [ "true"; "false" ]
46 | EvalStrategySetting _ -> [ "shallow"; "deep" ]
47 | FilenameOptionSetting _ -> [ "none"; "some " ]
48 | FuelAmountSetting _ -> [ "limited"; "unlimited" ]
49
50let set_to s v =
51 match s with
52 | BoolSetting vref -> (
53 match v with
54 | [ "true" ] ->
55 vref := true;
56 None
57 | [ "false" ] ->
58 vref := false;
59 None
60 | _ -> Some "expected one argument: 'true' or 'false'")
61 | EvalStrategySetting vref -> (
62 match v with
63 | [ "shallow" ] ->
64 vref := `Shallow;
65 None
66 | [ "deep" ] ->
67 vref := `Deep;
68 None
69 | _ -> Some "expected one argument: 'shallow' or 'deep'")
70 | FilenameOptionSetting vref -> (
71 match v with
72 | [ "none" ] ->
73 vref := None;
74 None
75 | [ "some"; filename ] ->
76 vref := Some (String.strip filename);
77 None
78 | _ -> Some "expected 'none' or 'some <filename>'")
79 | FuelAmountSetting vref -> (
80 match v with
81 | [ "limited" ] ->
82 vref := `Limited;
83 None
84 | [ "unlimited" ] ->
85 vref := `Unlimited;
86 None
87 | _ -> Some "expected 'limited' or 'unlimited'")
88
89let to_string s =
90 match s with
91 | BoolSetting vref -> Bool.to_string !vref
92 | EvalStrategySetting vref -> (
93 match !vref with `Shallow -> "shallow" | `Deep -> "deep")
94 | FilenameOptionSetting vref -> (
95 match !vref with None -> "none" | Some v -> "some " ^ v)
96 | FuelAmountSetting vref -> (
97 match !vref with `Limited -> "limited" | `Unlimited -> "unlimited")
98
99let settings =
100 Map.of_alist_exn
101 (module String)
102 [
103 ("print_input", BoolSetting opts.print_input);
104 ("print_parsed", BoolSetting opts.print_parsed);
105 ("print_elaborated", BoolSetting opts.print_elaborated);
106 ("print_nix_sexp", BoolSetting opts.print_nix_sexp);
107 ("print_mininix_sexp", BoolSetting opts.print_mininix_sexp);
108 ( "print_mininix_sexp_w_prelude",
109 BoolSetting opts.print_mininix_sexp_w_prelude );
110 ("print_result_mininix_sexp", BoolSetting opts.print_result_mininix_sexp);
111 ("print_result_nix_sexp", BoolSetting opts.print_result_nix_sexp);
112 ("eval_strategy", EvalStrategySetting opts.eval_strategy);
113 ("fuel_amount", FuelAmountSetting opts.fuel_amount);
114 ("imports_def_file", FilenameOptionSetting opts.imports_def_file);
115 ]
116
117let print () =
118 printf "==> Settings:\n";
119 Map.iteri settings ~f:(fun ~key:name ~data:setting ->
120 printf " %s: %s\n" name (to_string setting))