{-# LANGUAGE GADTs, 
             KindSignatures, 
             TypeFamilies, 
             RankNTypes,
             TypeOperators,
             MultiParamTypeClasses, 
             FunctionalDependencies,
             FlexibleInstances, 
             FlexibleContexts,
             UndecidableInstances, 
             AllowAmbiguousTypes #-}

import Prelude hiding (head,tail,map,foldr,zipWith,reverse)
import qualified Prelude as P
import qualified Data.List as L

-- | Nueva sintaxis

data Tree ::  * -> * where
   Leaf  :: Tree a 
   Node  :: Tree a -> a -> Tree a -> Tree a

-- | Expresiones
   
data Expr ::  * where
   Int     :: Int -> Expr 
   Bool    :: Bool -> Expr
   IsZero  :: Expr -> Expr
   Plus    :: Expr -> Expr -> Expr
   If      :: Expr -> Expr -> Expr -> Expr
   deriving Show

-- termino valido
e1 = If (IsZero (Plus (Int 0) (Int 1))) (Bool False) (Bool True)
e2 = If (Bool True) (Int 1) (Int 2)

-- terminos validos sintacticamente, pero no semanticamente
e3 = If (Int 0) (Bool False) (Bool True)
e4 = If (IsZero (Plus (Int 0) (Int 1))) (Bool False) (Int 3)

-- | Evaluador que mezcla tratamiento de errores con la evaluacion

data Val ::  * where
   VInt   :: Int   -> Val
   VBool  :: Bool  -> Val
   deriving Show

eval :: Expr -> Val
eval (Int n)       = VInt n
eval (Bool b)      = VBool b
eval (IsZero e)    = case eval e of
                       VInt n -> VBool (n == 0)
                       _      -> error "type error"
eval (Plus e1 e2)  = case (eval e1, eval e2) of
                       (VInt n1, VInt n2) -> VInt (n1 + n2)
                       _                  -> error "type error"
eval (If e1 e2 e3) = case eval e1 of
                       VBool b -> if b then eval e2 else eval e3
                       _       -> error "type error"

-- evaluacion ok
ev1 = eval e1
ev2 = eval e2
-- error de tipado
ev3 = eval e3
-- evaluacion ok a pesar de expresion mal formada
ev4 = eval e4

-- | Type checker

data EType = TInt | TBool
infixr 5 .::.
(.::.) :: Expr -> EType -> Bool 
(Int n)      .::. TInt  = True
(Bool b)     .::. TBool = True
(IsZero e)   .::. TBool = e .::. TInt
(Plus e1 e2) .::. TInt  = e1 .::. TInt && e2 .::. TInt
(If c e1 e2) .::. t     = c .::. TBool && e1 .::. t && e2 .::. t
_            .::. _     = False

wellTyped :: Expr -> Bool
wellTyped e = e .::. TInt || e .::. TBool

-- | Evaluador seguro (solo evalua si la expresion esta bien tipada)

safeEval :: Expr -> Val 
safeEval e | wellTyped e = seval e
           | otherwise   = error "type error"

seval :: Expr -> Val 
seval (Int n)      = VInt n
seval (Bool b)     = VBool b
seval (IsZero e)   = let VInt n = seval e
                     in VBool (n == 0)
seval (Plus e1 e2) = let VInt m = seval e1
                         VInt n = seval e2
                     in VInt (m + n)
seval (If c e1 e2) = let VBool b = seval c
                     in if b then seval e1 else seval e2 

-- | Expresiones empaquetadas (wrapped), phantom type

newtype WExpr a = E Expr 

instance Show a => Show (WExpr a) where
  show (E x) = show x

int    :: Int  -> WExpr Int
bool   :: Bool -> WExpr Bool
iszero :: WExpr Int -> WExpr Bool
plus   :: WExpr Int -> WExpr Int -> WExpr Int
ifc    :: WExpr Bool -> WExpr t -> WExpr t -> WExpr t

int n = E $ Int n
bool b = E $ Bool b
iszero (E e) = E $ IsZero e 
plus (E e1) (E e2) = E $ Plus e1 e2 
ifc (E c) (E e1) (E e2) = E $ If c e1 e2 


-- quisieramos un evaluador con un tipo de esta forma
weval :: WExpr t -> t 
weval (E e) = undefined

-- | GADT de expresiones + sistema de tipos

data Expr' :: * -> * where
   Int'    :: Int  -> Expr' Int 
   Bool'   :: Bool -> Expr' Bool
   IsZero' :: Expr' Int  -> Expr' Bool
   Plus'   :: Expr' Int  -> Expr' Int -> Expr' Int
   If'     :: Expr' Bool -> Expr' t -> Expr' t -> Expr' t

-- | Evaluador con GADTs (tagless)

eval' :: Expr' t -> t
eval' (Int' n)       = n
eval' (Bool' b)      = b
eval' (IsZero' e)    = eval' e == 0
eval' (Plus' e1 e2)  = eval' e1 + eval' e2
eval' (If' c e1 e2) = if eval' c then eval' e1 else eval' e2

-- terminos validos
ee1 = If' (IsZero' (Plus' (Int' 0) (Int' 1))) (Bool' False) (Bool' True)
ee2 = If' (Bool' True) (Int' 1) (Int' 2)

evv1 = eval' ee1
evv2 = eval' ee2

-- terminos invalidos (no tipan)
-- ee3 = If' (Int' 0) (Bool' False) (Bool' True)
-- ee4 = If' (IsZero' (Plus' (Int' 0) (Int' 1))) (Bool' False) (Int' 3)

-- | Signaturas requeridas en GADTs.

data X :: * -> * where
  C  :: Int -> X Int
  D  :: X a

-- signaturas validas para f
f :: X a -> [Int]
-- f :: X a -> [a]
f (C n) = [n]
f D     = []

g :: X a -> Int
-- g :: X Int -> Int
g (C n) = 1 + n
g D     = 0

-- | Extension del lenguaje

data Expr2 ::  * -> * where
   Int2     :: Int -> Expr2 Int 
   Bool2    :: Bool -> Expr2 Bool
   IsZero2  :: Expr2 Int -> Expr2 Bool
   Plus2    :: Expr2 Int -> Expr2 Int -> Expr2 Int
   If2      :: Expr2 Bool -> Expr2 a -> Expr2 a -> Expr2 a
   Pair2    :: Expr2 a -> Expr2 b -> Expr2 (a,b)
   Fst2     :: Expr2 (a,b) -> Expr2 a
   Snd2     :: Expr2 (a,b) -> Expr2 b

-- | Safe lists 

data Empty
data NonEmpty

data SafeList a b where
   NilS :: SafeList a Empty
   ConsS:: a -> SafeList a b -> SafeList a NonEmpty

safeHead :: SafeList a NonEmpty -> a
safeHead (ConsS x _) = x

-- safeTail :: SafeList a NonEmpty -> SafeList a ??
-- safeTail (ConsS _ xs) = xs

-- La siguiente definicion no la podemos tipar. Para poder tiparla debemos
-- debilitar la definicion de SafeList. 

-- silly False = NilS
-- silly True  = ConsS 1 NilS

-- | Vectores

data Zero
data Succ a

-- la intencion es usar tipos de la forma: Suc^n Zero

data Vec a n where
  Nil  :: Vec a Zero
  Cons :: a -> Vec a n -> Vec a (Succ n)

instance Show a => Show (Vec a n) where
  show xs = "<" ++ (concat . L.intersperse "," . L.map show . toList $ xs) ++ ">"

{-
instance Show a => Show (Vec a n) where
  show vs = show $ toList vs
-}

head :: Vec a (Succ n) -> a
head (Cons x xs) = x

tail :: Vec a (Succ n) -> Vec a n
tail (Cons x xs) = xs

map :: (a -> b) -> Vec a n -> Vec b n
map f   Nil        = Nil
map f  (Cons x xs) = Cons (f x) (map f xs)

zipWith :: (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n
zipWith f  Nil         Nil         = Nil
zipWith f  (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)
  
snoc :: Vec a n -> a -> Vec a (Succ n)
snoc  Nil         y = Cons y Nil
snoc  (Cons x xs) y = Cons x (snoc xs y)

reverse :: Vec a n -> Vec a n
reverse Nil         = Nil
reverse (Cons x xs) = snoc (reverse xs) x

-- | Codificacion de la suma a nivel de tipos como GADT.
-- | El GADT codica la relacion Sum m n s que relaciona
-- | dos naturales con la suma de ellos. Informalmente: Sum m n (m+n).

data Sum m n s where
  SumZero :: Sum Zero n n
  SumSucc :: Sum m n s -> Sum (Succ m) n (Succ s)

-- ejemplo
-- dos_mas_n :: Sum (Succ (Succ Zero)) n (Succ (Succ n))
dos_mas_n = SumSucc (SumSucc SumZero)
      
-- concatenacion de vectores  
appV :: Sum m n s -> Vec a m -> Vec a n -> Vec a s
appV SumZero      Nil          ys  = ys
appV (SumSucc p)  (Cons x xs)  ys  = Cons x (appV p xs ys)

-- ejemplo
app = appV dos_mas_n (Cons 1 (Cons 2 Nil)) (Cons 3 Nil)

-- usando una type family

infixr 5 :+:
type family (m :: *) :+: (n :: *) :: *
type instance Zero     :+: n = n
type instance (Succ m) :+: n = Succ (m :+: n)

infixr 5 .++.

(.++.) :: Vec a m -> Vec a n -> Vec a (m :+: n)
Nil       .++. ys  = ys
Cons x xs .++. ys  = Cons x (xs .++. ys)

-- ejemplo

app1 = (Cons 1 (Cons 2 Nil)) .++. (Cons 3 Nil)

-- | Conversion de vectores a listas

toList :: Vec a n -> [a]
toList Nil         = [ ]
toList (Cons x xs) = x : toList xs

-- | Conversion de listas a vectores

-- usando un tipo singleton para los naturales

data SNat n where
  Zero :: SNat Zero
  Succ :: SNat n -> SNat (Succ n)

snat2int :: SNat n -> Int
snat2int Zero     = 0
snat2int (Succ n) = 1 + snat2int n

instance Show (SNat n) where
  show sn = show $ snat2int sn  

s0 = Zero
s1 = Succ s0
s2 = Succ s1

fromListS :: SNat n -> [a] -> Vec a n
fromListS Zero      [ ]       = Nil
fromListS (Succ n)  (x : xs)  = Cons x (fromListS n xs)
fromListS _         _         = error "wrong length!"

-- usando un tipo existencial

data VecAny a where
  VecAny :: Vec a n -> VecAny a

instance Show a => Show (VecAny a) where
  show (VecAny xs) = show xs  

fromListE :: [a] -> VecAny a
fromListE []       =  VecAny Nil
fromListE (x : xs) =  case  fromListE xs of
                        VecAny ys -> VecAny (Cons x ys)

data VecAnyS a where
  VecAnyS :: SNat n -> Vec a n -> VecAnyS a

instance Show a => Show (VecAnyS a) where
  show (VecAnyS n xs) = show xs ++ "_" ++ show n 

fromListES :: [a] -> VecAnyS a
fromListES []       =  VecAnyS Zero Nil
fromListES (x : xs) =  case  fromListES xs of
                         VecAnyS n ys -> VecAnyS (Succ n) (Cons x ys)  

-- | Tipo igualdad

data Equal a b where
  Refl :: Equal a a

-- propiedad simetrica
sym :: Equal a b -> Equal b a
sym Refl = Refl

-- propiedad transitiva
trans :: Equal a b -> Equal b c -> Equal a c
trans Refl Refl = Refl

-- ejemplo
r :: Equal (Succ Zero :+: Succ Zero) (Succ (Succ Zero))
r = Refl

equalLength :: Vec a m -> Vec b n -> Maybe (Equal m n)
equalLength  Nil          Nil         = Just Refl
equalLength  (Cons _ xs)  (Cons _ ys) = case equalLength xs ys of
                                          Just Refl -> Just Refl
                                          Nothing   -> Nothing
equalLength  _            _           = Nothing

test :: Vec a m -> Vec b (Succ n) -> (a, b)
test v w =  case equalLength v w of
              Just Refl -> head (zipWith (,) v w)
    
-- | Reflexion de tipos

data Type t where
   RInt     :: Type Int 
   RChar    :: Type Char
   RList    :: Type a -> Type [a]
   RPair    :: Type a -> Type b -> Type (a,b)

-- ejemplo: comoresion de datos

data Bit = Cero | Uno

compressInt :: Int -> [Bit]
compressInt i = [Cero]

compressChar :: Char -> [Bit]
compressChar c = [Uno]

compress :: Type t -> t -> [Bit]
compress (RInt)        i         = compressInt i
compress (RChar)       c         = compressChar c
compress (RList ra)    [ ]       = Cero : [ ]
compress (RList ra)    (a : as)  = Uno : compress ra a 
                                        Prelude.++ compress (RList ra) as
compress (RPair ra rb) (a, b)    = compress ra a Prelude.++ compress rb b

-- Dynamics

data Dynamic where
  Dyn :: Type a -> a -> Dynamic

cast :: Dynamic -> Type t -> Maybe t
cast (Dyn ra a) rt =  case  tequal ra rt of
                        Just Refl   -> Just a
                        Nothing     -> Nothing


tequal :: Type t -> Type u -> Maybe (Equal t u)
tequal RInt          RInt          = Just Refl
tequal RChar         RChar         = Just Refl
tequal (RList ra)    (RList rb)    = case tequal ra rb of
                                       Just Refl -> Just Refl
                                       Nothing   -> Nothing
tequal (RPair ra rb) (RPair rc rd) = case tequal ra rc of
                                       Just Refl -> case tequal rb rd of
                                                      Just Refl -> Just Refl
                                                      Nothing   -> Nothing
                                       Nothing   -> Nothing
tequal _             _             = Nothing

-- ejemplo

addDyn :: Dynamic -> Dynamic -> Maybe Dynamic
addDyn x y = case (cast x RInt,cast y RInt) of
               (Just a,Just b) -> Just $ Dyn RInt (a+b)
               _               -> Nothing