diff options
Diffstat (limited to 'Semestr 3/pf/lista4')
18 files changed, 0 insertions, 287 deletions
diff --git a/Semestr 3/pf/lista4/lista4.ml b/Semestr 3/pf/lista4/lista4.ml deleted file mode 100644 index 32ea4a6..0000000 --- a/Semestr 3/pf/lista4/lista4.ml +++ /dev/null @@ -1,92 +0,0 @@ -(* 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 deleted file mode 100644 index 3c0d215..0000000 --- a/Semestr 3/pf/lista4/logic/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -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 deleted file mode 100644 index 93dc2b7..0000000 --- a/Semestr 3/pf/lista4/logic/README +++ /dev/null @@ -1,27 +0,0 @@ -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 deleted file mode 100644 index 7609f41..0000000 --- a/Semestr 3/pf/lista4/logic/_build/_digests +++ /dev/null @@ -1,8 +0,0 @@ -"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 deleted file mode 100644 index 69d909d..0000000 --- a/Semestr 3/pf/lista4/logic/_build/_log +++ /dev/null @@ -1,12 +0,0 @@ -### 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 differdeleted file mode 100644 index 5fca9f1..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.cma +++ /dev/null diff --git a/Semestr 3/pf/lista4/logic/_build/logic.cmi b/Semestr 3/pf/lista4/logic/_build/logic.cmi Binary files differdeleted file mode 100644 index d9d951f..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.cmi +++ /dev/null diff --git a/Semestr 3/pf/lista4/logic/_build/logic.cmo b/Semestr 3/pf/lista4/logic/_build/logic.cmo Binary files differdeleted file mode 100644 index 4f60b90..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.cmo +++ /dev/null diff --git a/Semestr 3/pf/lista4/logic/_build/logic.ml b/Semestr 3/pf/lista4/logic/_build/logic.ml deleted file mode 100644 index bb72fc2..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.ml +++ /dev/null @@ -1,78 +0,0 @@ -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 deleted file mode 100644 index 5169b43..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.ml.depends +++ /dev/null @@ -1 +0,0 @@ -logic.ml: Format List diff --git a/Semestr 3/pf/lista4/logic/_build/logic.mli b/Semestr 3/pf/lista4/logic/_build/logic.mli deleted file mode 100644 index afbdc7d..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.mli +++ /dev/null @@ -1,44 +0,0 @@ -(** 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 deleted file mode 100644 index 3c54482..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.mli.depends +++ /dev/null @@ -1 +0,0 @@ -logic.mli: Format diff --git a/Semestr 3/pf/lista4/logic/_build/logic.mllib b/Semestr 3/pf/lista4/logic/_build/logic.mllib deleted file mode 100644 index 3732649..0000000 --- a/Semestr 3/pf/lista4/logic/_build/logic.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Logic - diff --git a/Semestr 3/pf/lista4/logic/_build/ocamlc.where b/Semestr 3/pf/lista4/logic/_build/ocamlc.where deleted file mode 100644 index 49511f0..0000000 --- a/Semestr 3/pf/lista4/logic/_build/ocamlc.where +++ /dev/null @@ -1 +0,0 @@ -/home/fmalinka/.opam/4.11.1/lib/ocaml diff --git a/Semestr 3/pf/lista4/logic/_tags b/Semestr 3/pf/lista4/logic/_tags deleted file mode 100644 index e69de29..0000000 --- a/Semestr 3/pf/lista4/logic/_tags +++ /dev/null diff --git a/Semestr 3/pf/lista4/logic/logic.cma b/Semestr 3/pf/lista4/logic/logic.cma Binary files differdeleted file mode 100644 index 5fca9f1..0000000 --- a/Semestr 3/pf/lista4/logic/logic.cma +++ /dev/null diff --git a/Semestr 3/pf/lista4/logic/logic.cmi b/Semestr 3/pf/lista4/logic/logic.cmi Binary files differdeleted file mode 100644 index d9d951f..0000000 --- a/Semestr 3/pf/lista4/logic/logic.cmi +++ /dev/null diff --git a/Semestr 3/pf/lista4/logic/logic.mllib b/Semestr 3/pf/lista4/logic/logic.mllib deleted file mode 100644 index 3732649..0000000 --- a/Semestr 3/pf/lista4/logic/logic.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Logic - |