working vm: parser, admission with totality checks, solver and repl

2 files changed, 83 insertions, 0 deletions

diff --git a/bin/dune b/bin/dune
new file mode 100644
index 0000000..1ad9289
--- /dev/null
+++ b/bin/dune
@@ -0,0 +1,4 @@
+(executable
+ (name main)
+ (public_name sol)
+ (libraries sol))
diff --git a/bin/main.ml b/bin/main.ml
new file mode 100644
index 0000000..09f96e1
--- /dev/null
+++ b/bin/main.ml
@@ -0,0 +1,79 @@
+(* The standalone Sol host: runs a program file, or a REPL.
+
+   This is the thin binary of decision 4: it links the library with
+   the standalone world and adds nothing else. *)
+
+let print_solutions solutions =
+  match solutions with
+  | [] -> print_endline "no."
+  | solutions ->
+      List.iter
+        (fun solution ->
+          match solution with
+          | [] -> print_endline "yes."
+          | bindings ->
+              let parts =
+                List.map
+                  (fun (variable, pattern) ->
+                    Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern)
+                  bindings
+              in
+              print_endline (String.concat ", " parts ^ "."))
+        solutions
+
+let run_statements statements =
+  match Sol.World.Standalone.load statements with
+  | Error error ->
+      Format.eprintf "%a@." Sol.World.pp_error error;
+      Error ()
+  | Ok (world, queries) ->
+      List.iter
+        (fun query ->
+          match Sol.Vm.Standalone.solve world query with
+          | Ok solutions -> print_solutions solutions
+          | Error error -> Format.eprintf "%a@." Sol.Vm.pp_error error)
+        queries;
+      Ok ()
+
+let run_file path =
+  let contents = In_channel.with_open_text path In_channel.input_all in
+  match Sol.Front.parse_string contents with
+  | Error message ->
+      prerr_endline message;
+      exit 1
+  | Ok statements -> (
+      match run_statements statements with Ok () -> () | Error () -> exit 1)
+
+let repl () =
+  print_endline "Sol. Statements accumulate; Query expression: ... runs.";
+  let rec loop history =
+    print_string "sol> ";
+    match In_channel.input_line stdin with
+    | None -> ()
+    | Some line when String.trim line = "" -> loop history
+    | Some line -> (
+        match Sol.Front.parse_string line with
+        | Error message ->
+            prerr_endline message;
+            loop history
+        | Ok statements -> (
+            let declarations =
+              List.filter
+                (function
+                  | Sol.Ast.Directive ("Query", _) -> false
+                  | _ -> true)
+                statements
+            in
+            match run_statements (history @ statements) with
+            | Ok () -> loop (history @ declarations)
+            | Error () -> loop history))
+  in
+  loop []
+
+let () =
+  match Sys.argv with
+  | [| _ |] -> repl ()
+  | [| _; path |] -> run_file path
+  | _ ->
+      prerr_endline "usage: sol [file.sol]";
+      exit 1