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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
(* 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 } ->
(* A variable resolved to itself carries no information;
its constraints, if any, are in the residue. *)
let informative =
List.filter
(fun (variable, pattern) ->
not (Sol.Pattern.equal pattern (Sol.Pattern.Var variable)))
bindings
in
let parts =
List.map
(fun (variable, pattern) ->
Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern)
informative
@ 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 declarations statements =
List.filter
(function Sol.Ast.Directive ("Query", _) -> false | _ -> true)
statements
(* Feeding statements into the session: declarations accumulate,
queries answer immediately, and a failure changes nothing, so the
session only ever holds an admitted program. *)
let feed history statements =
match run_statements (history @ statements) with
| Ok () -> history @ declarations statements
| Error () -> history
let strip_quotes s =
let n = String.length s in
if n >= 2 && s.[0] = '"' && s.[n - 1] = '"' then String.sub s 1 (n - 2)
else s
let load_file history argument =
let path = strip_quotes argument in
match In_channel.with_open_text path In_channel.input_all with
| exception Sys_error message ->
prerr_endline message;
history
| contents -> (
match Sol.Front.parse_string contents with
| Error message ->
prerr_endline (path ^ ": " ^ message);
history
| Ok statements ->
let next = feed history statements in
if next != history then
Printf.printf "loaded %s: %d declarations, %d queries run.\n" path
(List.length (declarations statements))
(List.length statements - List.length (declarations statements));
next)
let repl () =
print_endline
"Sol. Statements accumulate; Query expression: ... runs; :help for commands.";
let rec loop history =
print_string "sol> ";
flush stdout;
match In_channel.input_line stdin with
| None -> ()
| Some line -> (
let line = String.trim line in
match String.index_opt line ' ' with
| _ when line = "" -> loop history
| _ when line = ":quit" -> ()
| _ when line = ":reset" ->
print_endline "session cleared.";
loop []
| _ when line = ":help" ->
print_endline
":load FILE bring a program into the session (atomic: a rejected file changes nothing)\n\
:reset clear the session\n\
:quit leave";
loop history
| Some i when String.sub line 0 i = ":load" ->
loop
(load_file history
(String.trim (String.sub line i (String.length line - i))))
| _ when String.length line > 0 && line.[0] = ':' ->
prerr_endline "unknown command; :help lists them.";
loop history
| _ -> (
match Sol.Front.parse_string line with
| Error message ->
prerr_endline message;
loop history
| Ok statements -> loop (feed history statements)))
in
loop []
let () =
match Sys.argv with
| [| _ |] -> repl ()
| [| _; "lsp" |] -> Lsp.run ()
| [| _; path |] -> run_file path
| _ ->
prerr_endline "usage: sol [file.sol | lsp]";
exit 1
|
