diff options
Diffstat (limited to 'Semestr 3/pf/lista4')
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 Binary files differnew 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 Binary files differnew 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 Binary files differnew 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/_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 Binary files differnew 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 Binary files differnew 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 + |