1 files changed, 116 insertions, 0 deletions
diff --git a/semestr-3/pf/lista5/proof/proof.ml b/semestr-3/pf/lista5/proof/proof.ml
new file mode 100644
index 0000000..3cde679
--- /dev/null
+++ b/semestr-3/pf/lista5/proof/proof.ml
@@ -0,0 +1,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 ()