-
El código completo de la clase:
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module Main where
data Lista a = N
| C a (Lista a)
deriving (Show)
infixr 5 `C`
{-@ lista1 :: Lista {v:Int | v >= 0} @-}
lista1 :: Lista Int
lista1 = 1 `C` 2 `C` 3 `C` N
{-@ lista2 :: Lista Nat @-}
lista2 :: Lista Int
lista2 = 1 `C` 2 `C` 3 `C` N
{-@ measure longitud @-}
longitud :: Lista a -> Int
longitud N = 0
longitud (_ `C` xs) = 1 + longitud xs
{-
N :: {v:Lista a | longitud v == 0}
C :: a -> xs:Lista a -> {v:Lista a | longitud v == 1 + longitud xs}
-}
{-
> head [1,2,3]
"This is a partial function, it throws an error on empty lists..."
> head []
*** Exception: Prelude.head: empty list
-}
{-
{-@ imposible :: {v:String | false} -> a @-}
imposible :: String -> a
imposible msj = error msj
-}
{-@ cabeza :: {v:Lista a | longitud v > 0} -> a @-}
cabeza :: Lista a -> a
cabeza (x `C` _) = x
cabeza N = error "Lista vacia"
{-
> [1] !! 4
*** Exception: Prelude.!!: index too large
> [] !! (-1)
*** Exception: Prelude.!!: negative index
-}
{-@ obtener :: xs:Lista a -> {i:Nat | longitud xs > i} -> a @-}
obtener :: Lista a -> Int -> a
obtener (x `C` _) 0 = x
obtener (_ `C` xs) i = obtener xs (i - 1)
obtener N _ = error "Lista vacia"
{-@ ack :: Nat -> Nat -> Nat / [m, n] @-}
ack :: Int -> Int -> Int
ack 0 n = n + 1
ack m 0 = ack (m - 1) 1
ack m n = ack (m - 1) (ack m (n - 1))
main :: IO ()
main = do
print (cabeza ((1 :: Int) `C` 2 `C` 3 `C` N))
--print (cabeza (N :: Lista Int))
print (obtener ((1 :: Int) `C` 2 `C` 3 `C` N) 2)
--print (obtener ((1 :: Int) `C` N) 4)