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
|
open Logic
type context = (string * formula) list
type goalDesc = context * formula
type proof =
| Whole of goalDesc
| Leaf of theorem
| ImpInsert of theorem * proof
| ImpErase of theorem * proof * proof
| Contradiction of theorem * proof
type goal = Goal of (goalDesc list) * (goalDesc list) * proof
let rec numGoals pf =
match pf with
| Whole _ -> 1
| Leaf _ -> 0
| ImpInsert (_, pf) | Contradiction (_, pf) -> numGoals pf
| ImpErase (_, pf1, pf2) -> (numGoals pf1) + (numGoals pf2)
let qed pf =
if (numGoals pf) <> 0 then failwith "proof not finished" else
match pf with
| Whole _ -> failwith "proof not finished"
| Leaf thm | ImpInsert (thm, _) | ImpErase (thm, _, _) | Contradiction (thm, _) -> thm
let rec goals pf =
match pf with
| Whole gd -> [gd]
| Leaf _ -> []
| ImpInsert (_, pf) | Contradiction (_, pf) -> goals pf
| ImpErase (_, pf1, pf2) -> (goals pf1) @ (goals pf2)
let proof g f =
Whole (g, f)
let goal (Goal (bef, aft, pf)) =
if aft == [] then failwith "Goal is empty" else (List.hd aft)
let focus n pf =
let add_goal (Goal (bef, aft, pf)) gl =
Goal (bef, gl::aft, pf)
in let goal = List.fold_left add_goal (Goal ([], [], pf)) (goals pf) in
let unfocus gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let next gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let prev gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let intro name gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let apply f gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let apply_thm thm gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let apply_assm name gl =
(* TODO: zaimplementuj *)
failwith "not implemented"
let pp_print_proof fmtr pf =
let ngoals = numGoals pf
and goals = goals pf
in if ngoals = 0
then Format.pp_print_string fmtr "No more subgoals"
else begin
Format.pp_open_vbox fmtr (-100);
Format.pp_open_hbox fmtr ();
Format.pp_print_string fmtr "There are";
Format.pp_print_space fmtr ();
Format.pp_print_int fmtr ngoals;
Format.pp_print_space fmtr ();
Format.pp_print_string fmtr "subgoals:";
Format.pp_close_box fmtr ();
Format.pp_print_cut fmtr ();
goals |> List.iteri (fun n (_, f) ->
Format.pp_print_cut fmtr ();
Format.pp_open_hbox fmtr ();
Format.pp_print_int fmtr (n + 1);
Format.pp_print_string fmtr ":";
Format.pp_print_space fmtr ();
pp_print_formula fmtr f;
Format.pp_close_box fmtr ());
Format.pp_close_box fmtr ()
end
let pp_print_goal fmtr gl =
let (g, f) = goal gl
in
Format.pp_open_vbox fmtr (-100);
g |> List.iter (fun (name, f) ->
Format.pp_print_cut fmtr ();
Format.pp_open_hbox fmtr ();
Format.pp_print_string fmtr name;
Format.pp_print_string fmtr ":";
Format.pp_print_space fmtr ();
pp_print_formula fmtr f;
Format.pp_close_box fmtr ());
Format.pp_print_cut fmtr ();
Format.pp_print_string fmtr (String.make 40 '=');
Format.pp_print_cut fmtr ();
pp_print_formula fmtr f;
Format.pp_close_box fmtr ()
|
