blob: eb212d2cbfc3362fdd77c212b97cf8d15db2e64b (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
(* 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 { Sol.Vm.bindings; residue } ->
let parts =
List.map
(fun (variable, pattern) ->
Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern)
bindings
@ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue
in
match parts with
| [] -> print_endline "yes."
| parts -> print_endline (String.concat ", " parts ^ "."))
solutions
let run_statements statements =
match Sol.Program.load statements with
| Error error ->
Format.eprintf "%a@." Sol.Program.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> ";
flush stdout;
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 ()
| [| _; "lsp" |] -> Lsp.run ()
| [| _; path |] -> run_file path
| _ ->
prerr_endline "usage: sol [file.sol | lsp]";
exit 1
|
