aboutsummaryrefslogtreecommitdiff
path: root/Semestr 3/pf/lista4
diff options
context:
space:
mode:
authorFranciszek Malinka <franciszek.malinka@gmail.com>2021-02-25 14:42:55 +0100
committerFranciszek Malinka <franciszek.malinka@gmail.com>2021-02-25 14:42:55 +0100
commit9477dbe667f250ecd23f8fc0d56b942191526421 (patch)
treea4b50c9a726f415f835f5311c11c5d66e95f688c /Semestr 3/pf/lista4
parent1968c1e590077bd51844eacfac722d7963848cb8 (diff)
Stare semestry, niepoukladane
Diffstat (limited to 'Semestr 3/pf/lista4')
-rw-r--r--Semestr 3/pf/lista4/lista4.ml92
-rw-r--r--Semestr 3/pf/lista4/logic/Makefile19
-rw-r--r--Semestr 3/pf/lista4/logic/README27
-rw-r--r--Semestr 3/pf/lista4/logic/_build/_digests8
-rw-r--r--Semestr 3/pf/lista4/logic/_build/_log12
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.cmabin0 -> 3109 bytes
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.cmibin0 -> 1513 bytes
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.cmobin0 -> 3102 bytes
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.ml78
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.ml.depends1
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.mli44
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.mli.depends1
-rw-r--r--Semestr 3/pf/lista4/logic/_build/logic.mllib2
-rw-r--r--Semestr 3/pf/lista4/logic/_build/ocamlc.where1
-rw-r--r--Semestr 3/pf/lista4/logic/_tags0
-rw-r--r--Semestr 3/pf/lista4/logic/logic.cmabin0 -> 3109 bytes
-rw-r--r--Semestr 3/pf/lista4/logic/logic.cmibin0 -> 1513 bytes
-rw-r--r--Semestr 3/pf/lista4/logic/logic.mllib2
18 files changed, 287 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/Makefile b/Semestr 3/pf/lista4/logic/Makefile
new file mode 100644
index 0000000..3c0d215
--- /dev/null
+++ b/Semestr 3/pf/lista4/logic/Makefile
@@ -0,0 +1,19 @@
+SOURCES = logic.ml logic.mli logic.mllib
+CMFILES = logic.cma logic.cmi
+.PHONY: all clean build
+
+all: logic.cma logic.cmi
+
+build: $(SOURCES)
+ rm -f $(CMFILES)
+ ocamlbuild logic.cma
+
+logic.cma: build
+ cp _build/$@ $@
+
+logic.cmi: build
+ cp _build/$@ $@
+
+clean:
+ rm -f $(CMFILES)
+ ocamlbuild -clean
diff --git a/Semestr 3/pf/lista4/logic/README b/Semestr 3/pf/lista4/logic/README
new file mode 100644
index 0000000..93dc2b7
--- /dev/null
+++ b/Semestr 3/pf/lista4/logic/README
@@ -0,0 +1,27 @@
+Szablon do listy 4 z Programowania funkcyjnego w grupach mabi, mbu, ppo i efes.
+
+Zarówno plik README, jak i źródła wykorzystują kodowanie znaków UTF-8.
+Jeśli nie wyświetlają się one dobrze na Twoim komputerze, zadbaj o to,
+by Twój edytor używał kodowania znaków UTF-8. Jeśli Twój edytor tego
+nie potrafi, zmień edytor.
+
+Pliki logic.mli, logic.ml, proof.mli, proof.ml definiują bibliotekę,
+którą łatwo skompilować poleceniem
+
+$ make
+
+Żeby moduły definiowane przez tą bibliotekę były widoczne w interpreterze,
+należy przekazać plik logic.cma jako parametr do interpretera:
+
+$ utop logic.cma
+
+Jeśli masz problemy ze skompilowaniem biblioteki, możesz zawsze skompilować ją
+ręcznie, choć nie jest to najwygodniejsza metoda:
+
+$ ocamlc -c logic.mli
+$ ocamlc -c logic.ml
+$ ocamlc -c proof.mli
+$ ocamlc -c proof.ml
+$ ocamlc -a -o logic.cma logic.cmo proof.cmo
+
+Pamiętaj, że po każdej zmianie należy przekompilować bibliotekę.
diff --git a/Semestr 3/pf/lista4/logic/_build/_digests b/Semestr 3/pf/lista4/logic/_build/_digests
new file mode 100644
index 0000000..7609f41
--- /dev/null
+++ b/Semestr 3/pf/lista4/logic/_build/_digests
@@ -0,0 +1,8 @@
+"Rule: ocaml: mllib & cmo* -> cma (%=logic )": "\233\003\206\234O\218\186\169\012\143\026\230\137vT\179"
+"Rule: ocaml dependencies ml (%=logic )": "\253\229 \217\176a\202\182\197\148\232\251\185q\138\n"
+"Resource: /mnt/c/Users/franc/Documents/pf/lista4/logic/logic.mli": "\144T\172\t\250\250\t\020qGU\157\247\251M\b"
+"Resource: /mnt/c/Users/franc/Documents/pf/lista4/logic/logic.ml": "[u \139\192\022|\201<\229\173\026\237\206K\022"
+"Rule: ocaml: ml & cmi -> cmo (%=logic )": "gr\213\221\155;\233\179\2497\006V\165\210\t\232"
+"Rule: ocaml: mli -> cmi (%=logic )": "\170\192\216\b\023\138!\200EW\017\002\179\007fC"
+"Rule: ocaml dependencies mli (%=logic )": "|\128\193\029\172\176V6EV\145\157\148J\007\232"
+"Resource: /mnt/c/Users/franc/Documents/pf/lista4/logic/logic.mllib": ">\208|K\146\191E\166@\251\011\165a\167\209I"
diff --git a/Semestr 3/pf/lista4/logic/_build/_log b/Semestr 3/pf/lista4/logic/_build/_log
new file mode 100644
index 0000000..69d909d
--- /dev/null
+++ b/Semestr 3/pf/lista4/logic/_build/_log
@@ -0,0 +1,12 @@
+### Starting build.
+# Target: logic.mli.depends, tags: { extension:mli, file:logic.mli, ocaml, ocamldep, quiet, traverse }
+/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules logic.mli > logic.mli.depends # cached
+# Target: logic.cmi, tags: { byte, compile, extension:mli, file:logic.mli, interf, ocaml, quiet, traverse }
+/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o logic.cmi logic.mli # cached
+# Target: logic.ml.depends, tags: { extension:ml, file:logic.ml, ocaml, ocamldep, quiet, traverse }
+/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules logic.ml > logic.ml.depends
+# Target: logic.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:logic.cmo, file:logic.ml, implem, ocaml, quiet, traverse }
+/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o logic.cmo logic.ml
+# Target: logic.cma, tags: { byte, extension:cma, file:logic.cma, library, link, ocaml, quiet, traverse }
+/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -a logic.cmo -o logic.cma
+# Compilation successful.
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
Binary files differ
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
Binary files differ
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
Binary files differ
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/_tags b/Semestr 3/pf/lista4/logic/_tags
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/Semestr 3/pf/lista4/logic/_tags
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
Binary files differ
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
Binary files differ
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
+