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