====== Řešení ======
===== Řádný termín =====
  - Vytvor datovy typ na reprezenaciu lambda kalkulu a napis funkciu pre beta redukciu
  - Napis funkciu, ktora zo zoznamu urobi zoznam zoznamov (z [1,2,3] spravi %%[[%%1],[2],[3]]) a dokaz funkcnost pomocou map. Indukcny predpoklad sme mali vymysliet na mieste.
  - Napis funkciu, ktora otvori 2 zadane subory, v prvom skontroluje, ci obsahuje vyraz //a<sup>n</sup>b<sup>n</sup>b<sup>n</sup>//. Ak ano, do druheho suboru zapis //n//, ak nie, vypis na stdout "Error" a do druheho suboru zapis poziciu chyby. Boli zadane funkcie na pracu so subormi.

<file haskell reseniRadna.hs>
import System.IO

-- 1

data LC a
	= Var a
	| App (LC a) (LC a)
	| Abs a (LC a)
	deriving (Show, Eq, Read)

betared :: Eq a => (LC a) -> (LC a) -> (LC a)
betared (Abs a body) ex = subst [] body
	where
		fvex = fv ex
		subst bnds (Var v)
			| v /= a = Var v
			| foldr (||) False (map (\x -> x `elem` bnds) fvex) = error "Free variable occurs bound in the beta reduction"
			| True = ex
		subst bnds (App e1 e2) = App (subst bnds e1) (subst bnds e2)
		subst bnds abs@(Abs x ex) = if x == a then abs else Abs x (subst (x:bnds) ex)
betared _ _ = error "Just lambda-abstraction can be applied"

fv (Var x) = [x]
fv (App e1 e2) = fv e1 ++ fv e2
fv (Abs v body) = filter (/= v) $ fv body


-- 2

lister l = map' f l			-- /1
	where
		f x = [x]		-- /2

map' f (x:xs)	= f x : map' f xs	-- /3
map' _ _	= []			-- /4

{-

1)
Chci dokázat:
lister [] = []
====
	lister []
=|1	map' f  []
=|4	[]


2)
I.H.: lister as = ass

Chci dokázat:
lister (a:as) = [a] : ass
====
	lister (a:as)
=|1	map' f (a:as)
=|3	f a : map' f as
=|1	f a : lister as
=|IH	f a : ass
=|2	[a] : ass

Q.E.D.


2] vartiantní přístup
I.H.: lister as = [[a1], ..., [an]]

Chci dokázat:
lister (a:as) = [[a],[a1], ..., [an]]
===
	lister (a:as)
=|1	map' f (a:as)
=|3	f a : map' f as
=|1	f a : lister as
=|IH	f a : [[a1], ..., [an]]
=|2	[a] : [[a1], ..., [an]]
=|def(:)	[[a],[a1], ... , [an]]

Q.E.D.

-- pozn: bylo možno uvést i definici (:) a [], ale to je zbytečné
-- pozn2: uznal jsem i definici s lister [] = [] i když potom byly všechny důkazy na něm založené špatně
-}


-- 3

fabc fi fo = do
	hi <- openFile fi ReadMode
	ho <- openFile fo WriteMode
	ct <- hGetContents hi
	let (res, val) = proc ct
	hPutStr ho (show val)
	if res then return () else hPutStr stderr "Error"
	hClose ho
	hClose hi

proc l
	| las == lbs && lbs == lcs && (length nocs == 0) = (True, las)
	| True = (False, err)
	where
		(als, noas) = span (== 'a') l
		las = length als
		--
		(bs, nobs) = span (== 'b') noas
		lbs = length bs
		--
		(cs, nocs) = span (== 'c') nobs
		lcs = length cs
		--
		err
			| las == 0 = 1
			| las == lbs = if lcs > las then las + las + las + 1 else las + las + lcs + 1
			| True = if lbs > las then las + las + 1 else las + lbs + 1


-- span f l = (takeWhile f l, dropWhile f l)
-- pozor! takeWhile (=='a') a filter (=='a') není to samé!!!

-- EOF
</file>

  - Napis predikat ktory pre sachovnicu zadanych rozmerov a 2 zadanych pozicii urci pocet acyklickych grafov, ktore zacinaju v prvom bode, prejdu druhym a vratia sa znovu do prveho
  - ???
  - Napis predikat substr(Str,Sub), ktory urci, ci Sub je podretazcom Str

<file prolog reseniRadna.pl>
:- dynamic posx/2, sizeX/1, sizeY/1.


/* 1 */

numofp(X1, Y1, X1, Y1, XS, YS, 1)
	:-	XS > 1, YS > 1,
		retractall(sizeX(_)), retractall(sizeY(_)), assert(sizeX(XS)), assert(sizeY(YS)),
		testX(X1),
		testY(Y1),
		!.
numofp(X1, Y1, X2, Y2, XS, YS, NUM)
	:-	XS > 1, YS > 1,
		retractall(sizeX(_)), retractall(sizeY(_)), assert(sizeX(XS)), assert(sizeY(YS)),
		testX(X1), testX(X2),
		testY(Y1), testY(Y2),
		retractall(posx(_, _)),
		setof(RR, search(X1, Y1, X1, Y1, RR), RES),
		fltr(RES, (X2:Y2), RX), length(RX, NUM).


search(X, Y, X, Y, [(X:Y)])
	:-	posx(_, _), !.
search(X1, Y1, X2, Y2, [(X1:Y1)|P])
	:-	assert(posx(X1, Y1)),
		move(X1, Y1, XN, YN),
		(not(posx(XN, YN)); (X2 = XN, Y2 = YN)),
		search(XN, YN, X2, Y2, P).
search(X1, Y1, _, _, _)
	:-	posx(X1, Y1),
		retract(posx(X1, Y1)),
		!, fail.

fltr([L|LS], V, [L|LX]) :- member(V,L), !, fltr(LS, V, LX).
fltr([_|LS], V, LX) :- fltr(LS, V, LX).
fltr([], _, []).

move(X, Y, NX, NY) :-
	NX is X + 1,
	NY is Y + 2,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 1,
	NY is Y + 2,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X + 1,
	NY is Y - 2,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 1,
	NY is Y - 2,
	testX(NX),
	testY(NY).

move(X, Y, NX, NY) :-
	NX is X + 2,
	NY is Y + 1,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 2,
	NY is Y + 1,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X + 2,
	NY is Y - 1,
	testX(NX),
	testY(NY).
move(X, Y, NX, NY) :-
	NX is X - 2,
	NY is Y - 1,
	testX(NX),
	testY(NY).

testX(X) :- sizeX(XX), X >= 1, X =< XX.
testY(Y) :- sizeY(YY), Y >= 1, Y =< YY.

/* 2 */
mapst(Map, Key, Value) :- nonvar(Map), var(Value), nonvar(Key), Get =.. [Map, Key, Value], call(Get).
mapst(Map, Key, Value) :- nonvar(Map), nonvar(Value), nonvar(Key), insrt(Map, Key, Value).
mapst(Map, Key, Value) :- nonvar(Map), nonvar(Value), var(Key), Get =.. [Map, K, Value], setof(K, Get, Key).

insrt(Map, Key, _) :- Test =.. [Map, Key, _], call(Test), !, fail.
insrt(Map, Key, Val) :- Asrt =.. [Map, Key, Val], assert(Asrt).

/* !!!!!!!!!!!!! NNEEEEE!!!! !!!!!!!!!!!!!! */
/* 2 BRUTUS chyby !!!!!!!!!!! */

mapstx(Map, _, _) :- var(Map), !, fail.
mapstx(_, Key, Value) :- var(Key), var(Value), !, fail.
mapstx(Map, Key, Value) :- var(Value), P =.. [Map, Key, Value], call(P).
mapstx(Map, Key, Value) :- var(Key), P =.. [Map, K, Value], setof(K, P, Key).
mapstx(Map, Key, Value) :- P =.. [Map, Key, Value], call(P), !, fail.
mapstx(Map, Key, Value) :- P =.. [Map, Key, Value], assert(P).


/* 3 */

sbstr([], []).
sbstr(Str, SStr) :- appnd(_, SStr, L), appnd(L, _ ,Str).

appnd([], L2, L2).
appnd([H|T], L2, [H|AP]) :- appnd(T,L2,AP).


/* 3 alternativa */

sbstr2([], []).
sbstr2([_|_], []).
sbstr2([H|T1], [H|T2]) :- prfx(T1, T2).
sbstr2([_|T], X) :- sbstr2(T, X).

prfx(_, []).
prfx([H|T1], [H|T2]) :- prfx(T1,T2).


/* !!!!!!!!!!!!! NNEEEEE!!!! !!!!!!!!!!!!!! */
/* zkuste varianty pro sbstrx([1,2,3],X). */

sbstrx(Str, Sub) :- sstr(Str, Sub, Sub).

sstr([H1|T1], [H2|T2], S) :- (H1 = H2 -> sstr(T1, T2, S); sstr(T1, S, S)).
sstr(_, [], _).

/* ---------------------- Goedel ----------------------- */
/*

MODULE PRIME.
IMPORT Integers.

PREDICATE Prime : Integer.

Prime(prime) <- ~ SOME [x] (x > 1 & x < prime & prime Mod x = 0).

*/
/* ---------------------- Goedel ----------------------- */

/* EOF */
</file>

===== 1. opravný termín =====
  - eq v lambda kalkulu
  - unlister ''%%[[%%1], [2], [3]]'' -> ''[1, 2, 3]'' (nedefinovane chovani pro viceprvkove vnitrni seznamy) + dukaz
  - Zalamat text na dany pocet znaku na radek

<file haskell resOprava1.hs>
import IO

{- ------------ (1) ------------

lambda kalkul

LET True = λxy.x
LET False = λxy.y

LET eq = λab.iszero(a prev b) (iszero(b prev a)) False

Jelikoz cisla jsou definovana takto:

LET 0 = λfn.n
LET N = λfn.f^N n

neexistuje zaporne cislo!!! Tedy test musel byt obousmerny.
Tedy reseni s jednim smerem je na nic.

Pokus o rekurzi v definici odporuje primo lambda kalkulu.
Taky zadne body.

-}


{- ------------ (2) ------------ -}

unlister l = _foldr f [] l		-- 1
	where
		f [x] xs = x:xs		-- 2

_foldr _ a [] = a			-- 3
_foldr f a (x:xs) = f x (_foldr f a xs)	-- 4

{-
Pro []

unlister []
=|1	_foldr f [] []
=|3	[]


I.H.
unlister [[x1], ..., [xn]] = [x1, ..., xn]

Pro
	as = [[x1], ..., [xn]]
	a = [x0]

unlister (a:as)
=|1	_foldr f [] (a:as)
=|4	f a (_foldr f [] as)
=	f [x0] (_foldr f [] [[x1], ..., [xn]])
=|1	f [x0] (unlister [[x1], ..., [xn]])
=|IH	f [x0] [x1, ..., xn]
=|2	[x0, x1, ..., xn]

Q.E.D.
-}


{- znacne pracnejsi reseni s (++) -}

unlister' l = _foldr (++) [] l		-- 5

{-

Je nutne uvest definici (++) !!!!!

(++) [] ys = ys				-- 6
(++) (x:xs) ys = x:(xs ++ ys)		-- 7


Pro []

unlister' []
=|5	_foldr (++) [] []
=|3	[]


I.H.
unlister' [[x1], ..., [xn]] = [x1, ..., xn]

Pro
as = [[x1], ..., [xn]]
a = [x0]

unlister' (a:as)
=|5	_foldr (++) [] (a:as)
=|4	(++) a (_foldr (++) [] as)
=	(++) [x0] (_foldr (++) [] [[x1], ..., [xn]])
=|5	(++) [x0] (unlister' [[x1], ..., [xn]])
=|IH	(++) [x0] [x1, ..., xn]
=|7	x0 : ([] ++ [x1, ..., xn])
=|6	x0 : [x1, ..., xn]
=|:	[x0, x1, ..., xn]

-}


shrink n fi fo = do
	hi <- openFile fi ReadMode
	ho <- openFile fo WriteMode
	cont <- hGetContents hi
	hPutStr ho $ unlines $ concat $ map (shrinkP n) $ par $ lines cont
	hClose ho
	hClose hi

par ls
	| null rst = [concat p1]
	| null p1 = [concat nosp]
	| True = concat p1 : par rst
	where
		nosp = dropWhile (== []) ls
		(p1, rest) = span (/= []) nosp
		rst = dropWhile (== []) rest

shrinkP _ [] = []
shrinkP width cs
	| null wds = [cs, ""]
	| True = join (head wds) (tail wds)
	where
		wds = words cs
		join l (w:ws)
			| length l + 1 + length w > width = l : join w ws
			| True = join (l ++ (' ':w)) ws
		join l [] = [l, ""]


-- EOF
</file>

  - Najit vsechny cesty na sachovnici, ktere nejakym polickem projdou prave dvakrat
  - Nejaky strom
  - Otoci "slova" v seznamu (''[1, 2, 3, 0, 1, 2, 3]'' -> ''[3, 2, 1, 0, 3, 2, 1]'', 0 je "mezera")

<file prolog resOprava1.pl>
/* 1 */

:- dynamic ps/2, cycle/2.
:- dynamic sizeY/1, sizeX/1.

findall(X1, Y1, X2, Y2, SX, SY, RES) :-
	SX > 0, SY > 0,
	retractall(sizeX(_)), retractall(sizeY(_)),
	assert(sizeX(SX)), assert(sizeY(SY)),
	testP(X1, Y1), testP(X2, Y2),
	retractall(ps(_, _)), retractall(cycle(_, _)),
	setof(R, search(X1, Y1, X2, Y2, R), RES).

testP(X, Y) :-
	X > 0, Y > 0,
	sizeX(XX), X =< XX,
	sizeY(YY), Y =< YY.

search(X, Y, X, Y, [X:Y]) :- cycle(_, _), !.
search(X, Y, X, Y, _) :- not(cycle(_, _)), !, fail.
search(X, Y, XX, YY, [X:Y|R]) :-
	cycle(_, _),
	assert(ps(X, Y)),
	nxtStep(X, Y, NX, NY),
	not(ps(NX, NY)),
	search(NX, NY, XX, YY, R).
search(X, Y, XX, YY, [X:Y|R]) :-
	not(cycle(_, _)),
	assert(ps(X, Y)),
	nxtStep(X, Y, NX, NY),
	tryTwo(NX, NY),
	search(NX, NY, XX, YY, R).
search(X, Y, _, _, _) :-
	ps(X, Y), not(cycle(X, Y)),
	!, retract(ps(X, Y)),
	fail.

tryTwo(NX, NY) :-
	ps(NX, NY),
	assert(cycle(NX, NY)).
tryTwo(NX, NY) :-
	cycle(NX, NY),
	!, retract(cycle(NX, NY)),
	fail.
tryTwo(NX, NY) :-
	not(ps(NX, NY)).

nxtStep(X, Y, XX, Y) :-
	sizeX(SX), X < SX,
	XX is X + 1.
nxtStep(X, Y, XX, Y) :-
	XX is X - 1,
	XX > 0.
nxtStep(X, Y, X, YY) :-
	sizeY(SY), Y < SY,
	YY is Y + 1.
nxtStep(X, Y, X, YY) :-
	YY is Y - 1,
	YY > 0.

/* 2 */

emptyT(leaf).

insval(V, leaf, node(V, leaf, leaf)).
insval(V, node(W, L, R), node(W, LL, R)) :-
	V < W, insval(V, L, LL).
insval(V, node(W, L, R),node(W, L, RR)) :-
	V > W, insval(V, R, RR).
insval(V, node(V, L, R), node(V, L, R)).

l2t([], leaf).
l2t([H|T], R) :-
	l2t(T, TR),
	insval(H, TR, R).

t2l(leaf, []).
t2l(node(V, L, R), ResL) :-
	t2l(L, LL),
	t2l(R, RL),
	append(LL, [V|RL], ResL).

tree2list(T, L) :-
	var(T), var(L), !, fail.
tree2list(T, L) :-
	var(T), l2t(T, L).
tree2list(T, L) :-
	var(L), t2l(T, L).
tree2list(T, L) :-	/* tady to slo ruzne, nic neni 100% */
	nonvar(L), nonvar(T),
	t2l(T, LL), LL = L.

/* 3 */

/* takovy trochu Haskell v Prologu */

revin([], _, []).
revin([H|T], S, RES) :-
	words([H|T], S, WRDS),
	revall(WRDS, REV),
	unwords(REV, S, RES).

words([], _, []).
words([H|_], H, _) :-
	!, fail.	/* an error */
words([H|T], S, [[H|W]|WS]) :-
	inw(T, S, x(W, R)),
	words(R, S, WS).

inw([], _, x([], [])).
inw([H|T], H, x([], T)) :- !.
inw([H|T], S, x([H|W], R)) :-
	inw(T, S, x(W, R)).

revall([L|LS], [RL|RLS]) :-
	reverse(L, RL),
	revall(LS, RLS).
revall([], []).

unwords([], _, []).
unwords([L|LS], _, L) :-
	nll(LS), !.
unwords([L|LS], S, UR) :-
	append(L, [S], LSP),
	unwords(LS, S, UW),
	append(LSP, UW, UR).

nll([]).
nll([_|_]) :- !, fail.	/* je ale zbytecny */

/* brutus Prolog */
/* inspirace v pisemece, upraveno pro spravnou funkcnost */

revn([], _, []).
revn(Str, Spc, Res) :-
	not(member(Spc, Str)), !,
	reverse(Str, Res).
revn(Str, Spc, Res) :-
	append(L, [Spc|Rest], Str),
	not(member(Spc, L)), !,
	reverse(L, RL),
	revn(Rest, Spc, InRes),
	append(RL, [Spc|InRes], Res).

/*

member(H,[H|_]).
member(X,[_|T]) :- member(X,T).

*/

/* EOF */
</file>