-
Notifications
You must be signed in to change notification settings - Fork 2
/
main.ml
183 lines (177 loc) · 7.01 KB
/
main.ml
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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
open Term
open Format
let verbose = ref false
let latex_output = ref None
let usage_msg =
"ipc_solver is a solver for intuitionistic propositional formulas.\n" ^
"\n" ^
"usage:"
let speclist = [
("--latex", Arg.String (fun path -> latex_output := Some path),
"Sets a path for latex output");
("--no-latex", Arg.Unit (fun _ -> latex_output := None),
"Cancels latex output");
("--verbose", Arg.Set verbose, "Enables verbose output");
("-v", Arg.Set verbose, "Enables verbose output")
]
let () =
Arg.parse speclist (fun _ -> ()) usage_msg;
let lexbuf = Lexing.from_channel stdin in
begin try
let tn = Parser.main Lexer.token lexbuf in
if !verbose then eprintf "Term is %a@." pp_print_pnterm tn;
let (t,env) = convert_name tn in
if !verbose then eprintf "Term is %a@." (pp_print_pterm env) t;
let solver_result = Solver.solve env.maxvar t in
let classical_result = begin match solver_result with
| Some _ -> Kripke.Irrefutable
| None -> Kripke.solve_n env 1 t end in
let kripke_result = begin match solver_result, classical_result with
| Some _, _ -> Kripke.Irrefutable
| _, Kripke.Irrefutable -> Kripke.solve env t
| _, r -> r end in
let message =
begin match solver_result, classical_result with
| Some _, _ -> "Provable."
| _, Kripke.Refutable _ -> "Not provable in intuitionistic logic; not provable in classical logic neither."
| _, Kripke.Irrefutable -> "Not provable in intuitionistic logic; provable in classical logic however."
| _, _ -> "Not provable in intuitionistic logic."
end in
Format.printf "%s@." message;
begin match !latex_output with
| Some latex_path ->
let f = open_out latex_path in
let ff = formatter_of_out_channel f in
fprintf ff "%s@." "\\documentclass[preview,varwidth=10000px,12pt]{standalone}";
fprintf ff "%s@." "\\usepackage{bussproofs}";
fprintf ff "%s@." "\\usepackage{color}";
fprintf ff "%s@." "\\usepackage{latexsym}";
fprintf ff "%s@." "\\usepackage{listings}";
fprintf ff "%s@." "\\begin{document}";
fprintf ff "%a:@.@." (pp_print_pterm_latex env 5) t;
fprintf ff "%s@.@." message;
begin match Solver.solve env.maxvar t with
| Some pr ->
if !verbose then eprintf "proof(LF, plain): %a@."
Lf_proof.pp_print_proofitem pr;
if !verbose then eprintf "proof(LF):@,%a@."
(Lf_proof.pp_print_proof env env.maxvar t) pr;
let npr = Nj_proof.convert_lf t pr in
if !verbose then eprintf "proof(NJ):@,%a@."
(Nj_proof.pp_print_lambda env) npr;
ignore (Nj_proof.nj_check_type [] npr);
let npr = Nj_proof.postproc_proof npr in
ignore (Nj_proof.nj_check_type [] npr);
if !verbose then eprintf "proof(NJ):@,%a@."
(Nj_proof.pp_print_lambda env) npr;
fprintf ff "%s@.@." "Proof tree (intuitionistic):";
fprintf ff "%a@." (Nj_proof.print_nj_latex env) npr
| None -> ()
end;
begin match kripke_result with
| Kripke.Refutable (n, accessibility, term_asgn) ->
if n == 1 then begin
fprintf ff "%s" "Counterexample: ";
for i = 0 to (env.maxvar-1) do
if i <> 0 then fprintf ff ", ";
fprintf ff "$%a = %d$"
(pp_print_pterm_latex_internal env 5) (PVar i)
(if (Hashtbl.find term_asgn (PVar i)).(0) then 1 else 0)
done;
fprintf ff "@.@."
end else begin
fprintf ff "%s" "Kripke counterexample: ";
fprintf ff "$\\mathcal{W} = \\{";
for j = 0 to (n-1) do
if j <> 0 then fprintf ff ", ";
fprintf ff "W_{%d}" j
done;
fprintf ff "\\}$, ";
for i = 0 to (n-1) do
for j = i+1 to (n-1) do
if accessibility.(i).(j) then begin
let ok = ref true in
for k = i+1 to (j-1) do
if accessibility.(i).(j) && accessibility.(j).(k) then
ok := false
done;
if !ok then fprintf ff "$(W_{%d} \\leadsto W_{%d})$, " i j
end
done
done;
for i = 0 to (env.maxvar-1) do
if i <> 0 then fprintf ff ", ";
fprintf ff "$%a = \\{"
(pp_print_pterm_latex_internal env 5) (PVar i);
let comma = ref false in
for j = 0 to (n-1) do
if (Hashtbl.find term_asgn (PVar i)).(j) then begin
if !comma then fprintf ff ", ";
fprintf ff "W_{%d}" j;
comma := true
end
done;
fprintf ff "\\}$"
done;
fprintf ff "@.@."
end;
fprintf ff "\\begin{tabular}{|r|l|}@.";
let visited = Hashtbl.create 771 in
let rec visit t =
if not (Hashtbl.mem visited t) then begin
Hashtbl.add visited t ();
begin match t with
| PVar _ -> ()
| PArrow (t0, t1) -> visit t0; visit t1
| POr (t0, t1) -> visit t0; visit t1
| PAnd (t0, t1) -> visit t0; visit t1
| PTop -> ()
| PBot -> ()
end;
fprintf ff "%a & " (pp_print_pterm_latex env 5) t;
if n == 1 then begin
fprintf ff "$%d$"
(if (Hashtbl.find term_asgn t).(0) then 1 else 0)
end else begin
fprintf ff "$\\{";
let comma = ref false in
for j = 0 to (n-1) do
if (Hashtbl.find term_asgn t).(j) then begin
if !comma then fprintf ff ", ";
fprintf ff "W_{%d}" j;
comma := true
end
done;
fprintf ff "\\}$"
end;
fprintf ff " \\\\"
end
in
for i = 0 to (env.maxvar-1) do
visit (PVar i)
done;
visit t;
fprintf ff "\\end{tabular}@.";
fprintf ff "@.@."
| _ -> ()
end;
fprintf ff "%s@." "\\end{document}";
close_out f
| None -> ()
end
with
| Parsing.Parse_error ->
Format.printf "Parse Error@.";
begin match !latex_output with
| Some latex_path ->
let f = open_out latex_path in
let ff = formatter_of_out_channel f in
fprintf ff "%s@." "%parse_error";
fprintf ff "%s@." "\\documentclass[preview,varwidth=4000px]{standalone}";
fprintf ff "%s@." "\\begin{document}";
fprintf ff "%s@." "Parse Error";
fprintf ff "%s@." "\\end{document}";
close_out f
| None -> ()
end
end