-- I1M 2009-10: Relación 19 (17 de marzo de 2010)
-- Departamento de Ciencias de la Computación e I.A.
-- Universidad de Sevilla
-- =====================================================================

-- ---------------------------------------------------------------------
-- Importación de librerías auxiliares                                --
-- ---------------------------------------------------------------------

import Test.QuickCheck 
import Control.Monad

-- ---------------------------------------------------------------------
-- Ejercicio 1. La definición de la composición de funciones es
--    (.) :: (b -> c) -> (a -> b) -> (a -> c)
--    (f . g) x = f (g x)
-- y la de aplicación de una función a los elementos de una lista es
--    map :: (a -> b) -> [a] -> [b]	Source
--    map _ []     = []
--    map f (x:xs) = f x : map f xs
-- Demostrar que para todo par de funciones f, g se tiene que
--    (map f). (map g) = map (f . g)
-- ---------------------------------------------------------------------

{-
 Demostración: Por extensionalidad, tenemos que demostrar que para todo
 lista xs se tiene que 
    ((map f). (map g)) xs = map (f . g) xs
 Lo demostraremos por inducción en xs.

-}

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que para todo función f y todo par de lista xs
-- e ys se tiene que
--    map f (xs ++ ys) = (map f xs) ++ (map f ys)
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Ejercicio 3. Demostrar que para todo función f 
--    (map f) . reverse = reverse . (map f)
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Nota. En los siguientes ejercicios se demostrarán propiedades de los
-- árboles binarios definidos como sigue 
--    data Arbol a = Hoja 
--                 | Nodo a (Arbol a) (Arbol a)
--                 deriving (Show, Eq)
-- En los ejemplos se usará el siguiente árbol
--    arbol = Nodo 9
--                   (Nodo 3 
--                         (Nodo 2 Hoja Hoja) 
--                         (Nodo 4 Hoja Hoja)) 
--                   (Nodo 7 Hoja Hoja)
-- ---------------------------------------------------------------------

data Arbol a = Hoja 
             | Nodo a (Arbol a) (Arbol a)
             deriving (Show, Eq)

arbol = Nodo 9
               (Nodo 3 
                     (Nodo 2 Hoja Hoja) 
                     (Nodo 4 Hoja Hoja)) 
               (Nodo 7 Hoja Hoja)

-- ---------------------------------------------------------------------
-- Ejercicio 4.1. Definir la función
--    maptree :: (a -> a) -> Arbol a -> Arbol a
-- tal que (maptree f x) es el árbol obtenido aplicándole a cada nodo de
-- x la función f. Por ejemplo,
--    *Main> arbol
--    Nodo 9 
--         (Nodo 3 
--               (Nodo 2 Hoja Hoja) 
--               (Nodo 4 Hoja Hoja)) 
--         (Nodo 7 Hoja Hoja)
--    *Main> maptree (2+) arbol
--    Nodo 11 
--         (Nodo 5 
--               (Nodo 4 Hoja Hoja) 
--               (Nodo 6 Hoja Hoja)) 
--         (Nodo 9 Hoja Hoja)
-- ---------------------------------------------------------------------

maptree :: (a -> a) -> Arbol a -> Arbol a
maptree = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4.2. La función
--    espejo :: Arbol a -> Arbol a
--    espejo Hoja         = Hoja
--    espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)
-- es tal que (espejo x) es la imagen especular del árbol x. Por ejemplo,
--    *Main> espejo arbol
--    Nodo 9 
--         (Nodo 7 Hoja Hoja) 
--         (Nodo 3 
--               (Nodo 4 Hoja Hoja) 
--               (Nodo 2 Hoja Hoja))
-- Comprobar con QuickCheck que 
--     (maptree (1+)) . espejo = espejo . (maptree (1+))
-- ---------------------------------------------------------------------

espejo :: Arbol a -> Arbol a
espejo Hoja         = Hoja
espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)

-- La propiedad es
prop_maptree_espejo :: Arbol Int -> Bool
prop_maptree_espejo x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 4.3. Demostrar por inducción que
--    (maptree f) . espejo = espejo . (maptree f)
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Ejercicio 4.5. La función
--    preorden :: Arbol a -> [a]
--    preorden Hoja         = []
--    preorden (Nodo x i d) = x : (preorden i ++ preorden d)
-- es tal que (preorden x) es la lista correspondiente al recorrido
-- preorden del árbol x; es decir, primero visita la raíz del árbol, a
-- continuación recorre el subárbol izquierdo y, finalmente, recorre el
-- subárbol derecho. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> preorden arbol
--    [9,3,2,4,7]
-- Comprobar con QuickCheck que
--    (map (1+)) . preorden = preorden . (maptree (1+)) 
-- ---------------------------------------------------------------------

preorden :: Arbol a -> [a]
preorden Hoja         = []
preorden (Nodo x i d) = x : (preorden i ++ preorden d)

-- La propiedad es
prop_map_preorden :: Arbol Int -> Bool
prop_map_preorden x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 4.6. Demostrar que
--    (map f) . preorden = preorden . (maptree f) 
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Funciones auxiliares                                               --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Nota. Para comprobar propiedades de árboles con QuickCheck se
-- utilizará el siguinete generador.
-- ---------------------------------------------------------------------

instance Arbitrary a => Arbitrary (Arbol a) where
  arbitrary = sized arbol
    where
      arbol 0       = return Hoja 
      arbol n | n>0 = oneof [return Hoja,
                             liftM3 Nodo arbitrary subarbol subarbol]
                      where subarbol = arbol (div n 2)
  coarbitrary = undefined