blob: 83ee71ad42d7d2b1cbee7f018c3d20be9ab226b7 (
plain)
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
|
open Logic
type context = (string * formula) list
type goalDesc = context * formula
type proof =
| Assumption of theorem
| ImpInsert of theorem * proof
| ImpErase of theorem * proof * proof
| Contradiction of theorem * proof
| Whole of goalDesc
type goal (* = TODO: tu wpisz swoją definicję *)
let qed pf =
(* TODO: zaimplementuj *)
failwith "not implemented"
let numGoals pf =
(* TODO: zaimplementuj *)
failwith "not implemented"
let goals pf =
(* TODO: zaimplementuj *)
failwith "not implemented"
let proof g f =
(* TODO: zaimplementuj *)
failwith "not implemented"
let goal pf =
(* TODO: zaimplementuj *)
failwith "not implemented"
let focus n pf =
(* TODO: zaimplementuj *)
failwith "not implemented"
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 ()
|
