13 files changed, 221 insertions, 0 deletions
diff --git a/semestr-3/pf/lista4/lista4.ml b/semestr-3/pf/lista4/lista4.ml
new file mode 100644
index 0000000..32ea4a6
--- /dev/null
+++ b/semestr-3/pf/lista4/lista4.ml
@@ -0,0 +1,92 @@
+(* Zadanie 1 *)
+
+type 'a btree = Leaf | Node of 'a btree * 'a * 'a btree
+
+let is_balanced bt = 
+  let rec check = function
+    | Leaf -> 0
+    | Node (rt, x, lt) -> 
+      let left_weight = check lt
+      in if left_weight == -1 then -1 else
+        let right_weight = check rt
+        in if right_weight == -1 then -1 else
+        if abs (left_weight - right_weight) <= 1 then left_weight + right_weight + 1 else -1
+  in if check bt == -1 then false else true
+
+let rec preorder = function
+  | Leaf -> []
+  | Node (lt, x, rt) ->
+    x :: ((preorder lt) @ (preorder rt)) 
+let bt = Node ((Node ((Node (Leaf, 3, Leaf)), 2, Leaf)), 
+               1, 
+               (Node (Node (Leaf, 5, Leaf), 4, Node (Leaf, 6, Leaf))))
+
+let reverse xs =
+  let rec iter res = function
+    | [] -> res
+    | hd :: tl -> (iter (hd :: res) tl) in
+  iter [] xs
+
+let halve xs =
+  let rec iter xs crawl sth = 
+    match crawl with
+      [] -> (sth, xs)
+    | [x] -> (sth, xs)
+    | st :: nd :: tl -> iter (List.tl xs) tl ((List.hd xs) :: sth) in
+  let sth, ndh = iter xs xs [] in
+  ((reverse sth), ndh)
+
+let rec bt_of_list = function
+  | [] -> Leaf
+  | x :: xs ->
+    let (sth, ndh) = (halve xs)
+    in Node (bt_of_list sth, x, bt_of_list ndh)
+
+
+(* Zadanie 2 *)
+
+type 'a place = PNil | Place of 'a list * 'a list
+
+let findNth xs n = 
+  let rec iter xs n = match xs, n with
+    | [], 0 -> PNil
+    | [], n -> failwith "n too big"
+    | xs, 0 -> Place ([], xs)
+    | x :: xs, n -> match (iter xs (n - 1)) with 
+      | PNil -> Place ([x], [])
+      | Place (bef, aft) -> Place (x :: bef, aft)
+  in match iter xs n with
+  | PNil -> PNil
+  | Place (bef, aft) -> Place (reverse bef, aft)
+
+let collapse = function
+  | PNil -> []
+  | Place (bef, aft) -> List.rev_append bef aft
+
+let add x = function
+  | PNil -> Place ([], [x])
+  | Place (bef, aft) -> Place (bef, x :: aft)
+
+let del = function
+  | PNil -> failwith "empty place"
+  | Place (_, []) -> failwith "nothing at this place"
+  | Place (bef, aft) -> Place (bef, List.tl aft)
+
+let next = function
+  | PNil -> failwith "empty place"
+  | Place (_, []) -> failwith "nothing next to this place"
+  | Place (bef, aft) -> let x = List.hd aft 
+    in Place (x :: bef, List.tl aft)
+
+let prev = function
+  | PNil -> failwith "empty place"
+  | Place ([], _) -> failwith "nothing next to this place"
+  | Place (bef, aft) -> let x = List.hd bef 
+    in Place (List.tl bef, x :: aft)
+
+
+(* Pierwszy element -- drzewo ukorzenione w aktualnym wierzcholku po usunieciu synow (czyli ojciec jest nowym synem) 
+   Drugi element -- prawe poddrzewo
+   Trzeci element -- lewe poddrzewo *)
+type 'a btplace = 'a btree * 'a btree * 'a btree
+
diff --git a/semestr-3/pf/lista4/logic/_build/logic.cma b/semestr-3/pf/lista4/logic/_build/logic.cma
new file mode 100644
index 0000000..5fca9f1
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.cma
diff --git a/semestr-3/pf/lista4/logic/_build/logic.cmi b/semestr-3/pf/lista4/logic/_build/logic.cmi
new file mode 100644
index 0000000..d9d951f
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.cmi
diff --git a/semestr-3/pf/lista4/logic/_build/logic.cmo b/semestr-3/pf/lista4/logic/_build/logic.cmo
new file mode 100644
index 0000000..4f60b90
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.cmo
diff --git a/semestr-3/pf/lista4/logic/_build/logic.ml b/semestr-3/pf/lista4/logic/_build/logic.ml
new file mode 100644
index 0000000..bb72fc2
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.ml
@@ -0,0 +1,78 @@
+type formula = False | Var of string | Imp of formula * formula
+
+let rec string_of_formula = function
+  | False -> "F"
+  | Var s -> s
+  | Imp (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")"
+(* match (f1, f2) with
+   | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
+   | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
+   | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
+   | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *)
+
+let pp_print_formula fmtr f =
+  Format.pp_print_string fmtr (string_of_formula f)
+
+type verdict = { assump : formula list; concl : formula }
+
+type theorem = 
+  | Assumption of verdict
+  | ImpInsert of verdict * theorem
+  | ImpErase of verdict * theorem * theorem
+  | Contradiction of verdict * theorem
+
+let get_verdict thm = match thm with
+  | Assumption f -> f
+  | ImpInsert (v, _) | ImpErase (v, _, _) | Contradiction (v, _) -> v
+
+let assumptions thm = (get_verdict thm).assump
+let consequence thm = (get_verdict thm).concl
+
+let pp_print_theorem fmtr thm =
+  let open Format in
+  pp_open_hvbox fmtr 2;
+  begin match assumptions thm with
+    | [] -> ()
+    | f :: fs ->
+      pp_print_formula fmtr f;
+      fs |> List.iter (fun f ->
+          pp_print_string fmtr ",";
+          pp_print_space fmtr ();
+          pp_print_formula fmtr f);
+      pp_print_space fmtr ()
+  end;
+  pp_open_hbox fmtr ();
+  pp_print_string fmtr "⊢";
+  pp_print_space fmtr ();
+  pp_print_formula fmtr (consequence thm);
+  pp_close_box fmtr ();
+  pp_close_box fmtr ()
+
+let by_assumption f =
+  Assumption { assump=[f]; concl=f }
+
+let imp_i f thm =
+  let premise = get_verdict thm
+  in ImpInsert ({assump=(List.filter ((<>) f) premise.assump); concl=(Imp (f, premise.concl))}, thm)
+
+let imp_e th1 th2 =
+  let premise1 = get_verdict th1 in 
+  let premise2 = get_verdict th2 in
+  match premise1.concl with
+  | False | Var _ -> failwith "th1 conclusion is not implication"
+  | Imp (phi, psi) -> if phi <> premise2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else  
+      ImpErase ({assump=(premise1.assump @ premise2.assump); concl=(psi)}, th1, th2)
+
+let bot_e f thm =
+  match get_verdict thm with
+  | {assump=ass; concl=False}-> (Contradiction ({assump=ass; concl=f}, thm))
+  | _ -> failwith "thm conclusion is not False"
+
+
+let taut = (imp_i (Var "p") (by_assumption (Var "p")))
+let taut2 = (imp_i (Var "p") (imp_i (Var "q") (by_assumption (Var "p"))))
+
+let imppqr = Imp (Imp (Var "p", Var "q"), Var "r")
+let imppq = Imp (Var "p", Var "q")
+let imppr = Imp (Var "p", Var "r")
+let taut3 = (imp_i (imppqr) (imp_i imppq (by_assumption imppr))) 
+\ No newline at end of file
diff --git a/semestr-3/pf/lista4/logic/_build/logic.ml.depends b/semestr-3/pf/lista4/logic/_build/logic.ml.depends
new file mode 100644
index 0000000..5169b43
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.ml.depends
@@ -0,0 +1 @@
+logic.ml: Format List
diff --git a/semestr-3/pf/lista4/logic/_build/logic.mli b/semestr-3/pf/lista4/logic/_build/logic.mli
new file mode 100644
index 0000000..afbdc7d
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.mli
@@ -0,0 +1,44 @@
+(** reprezentacja formuł *)
+type formula = False | Var of string | Imp of formula * formula
+
+val pp_print_formula : Format.formatter -> formula -> unit
+
+(** reprezentacja twierdzeń *)
+type theorem
+
+(** założenia twierdzenia *)
+val assumptions : theorem -> formula list
+(** teza twierdzeni *)
+val consequence : theorem -> formula
+
+val pp_print_theorem : Format.formatter -> theorem -> unit
+
+(** by_assumption f konstuuje następujący dowód
+
+    -------(Ax)
+    {f} ⊢ f  *)
+val by_assumption : formula -> theorem
+
+(** imp_i f thm konstuuje następujący dowód
+
+       thm
+      Γ ⊢ φ
+    ---------------(→I)
+    Γ \ {f} ⊢ f → φ *)
+val imp_i : formula -> theorem -> theorem
+
+(** imp_e thm1 thm2 konstuuje następujący dowód
+
+    thm1      thm2
+    Γ ⊢ φ → ψ    Δ ⊢ φ 
+    ------------------(→E)
+    Γ ∪ Δ ⊢ ψ *)
+val imp_e : theorem -> theorem -> theorem
+
+(** bot_e f thm konstruuje następujący dowód
+
+    thm
+    Γ ⊢ ⊥
+    -----(⊥E)
+    Γ ⊢ f *)
+val bot_e : formula -> theorem -> theorem
diff --git a/semestr-3/pf/lista4/logic/_build/logic.mli.depends b/semestr-3/pf/lista4/logic/_build/logic.mli.depends
new file mode 100644
index 0000000..3c54482
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.mli.depends
@@ -0,0 +1 @@
+logic.mli: Format
diff --git a/semestr-3/pf/lista4/logic/_build/logic.mllib b/semestr-3/pf/lista4/logic/_build/logic.mllib
new file mode 100644
index 0000000..3732649
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/logic.mllib
@@ -0,0 +1,2 @@
+Logic
+
diff --git a/semestr-3/pf/lista4/logic/_build/ocamlc.where b/semestr-3/pf/lista4/logic/_build/ocamlc.where
new file mode 100644
index 0000000..49511f0
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/_build/ocamlc.where
@@ -0,0 +1 @@
+/home/fmalinka/.opam/4.11.1/lib/ocaml
diff --git a/semestr-3/pf/lista4/logic/logic.cma b/semestr-3/pf/lista4/logic/logic.cma
new file mode 100644
index 0000000..5fca9f1
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/logic.cma
diff --git a/semestr-3/pf/lista4/logic/logic.cmi b/semestr-3/pf/lista4/logic/logic.cmi
new file mode 100644
index 0000000..d9d951f
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/logic.cmi
diff --git a/semestr-3/pf/lista4/logic/logic.mllib b/semestr-3/pf/lista4/logic/logic.mllib
new file mode 100644
index 0000000..3732649
--- /dev/null
+++ b/semestr-3/pf/lista4/logic/logic.mllib
@@ -0,0 +1,2 @@
+Logic
+