-
Debes escribir la firma de LiquidHaskell a la función invertir demostrando que la operación de inversión preserva la altura del árbol original. Si tu implementación y tu firma son correctas, LiquidHaskell verificará que ej1 es válido.
-
Debes escribir la firma de LiquidHaskell para aplanar demostrando que la longitud de la lista resultante (len) es exactamente igual a la cantidad total de nodos del árbol (size).
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module Main where
{-@ measure len @-}
len :: [a] -> Int
len [] = 0
len (_:xs) = 1 + len xs
{-@ type ListN a N = {v:[a] | len v = N} @-}
data Tree a = Leaf | Node a (Tree a) (Tree a)
{-@ inline max' @-}
max' :: Int -> Int -> Int
max' a b = if a > b then a else b
{-@ measure altura @-}
altura :: Tree a -> Int
altura Leaf = 0
altura (Node _ l r) = 1 + max' (altura l) (altura r)
{-@ type TreeN a N = {v:Tree a | altura v = N} @-}
invertir :: Tree a -> Tree a
invertir Leaf = Leaf
invertir (Node x l r) = Node x (invertir r) (invertir l)
{-@ ej1 :: TreeN Nat 2 @-}
ej1 :: Tree Int
ej1 = invertir (Node 2 (Node 1 Leaf Leaf) (Node 3 Leaf Leaf))
{-@ measure size @-}
size :: Tree a -> Int
size Leaf = 0
size (Node _ l r) = 1 + size l + size r
aplanar :: Tree a -> [a]
aplanar Leaf = []
aplanar (Node x l r) = (aplanar l) ++ ([x] ++ (aplanar r))
{-@ ej2 :: ListN Nat 3 @-}
ej2 :: [Int]
ej2 = aplanar (Node 2 (Node 1 Leaf Leaf) (Node 3 Leaf Leaf))
main :: IO ()
main = print "Hola Mundo"