module TypesTerms where

import Syntax
import PrettyPrint


--------------------------------------------------------------------------------
-- Types
-- 

data Type
    = Type (T Type)
    | TyAll HsName Type
        deriving (Show, Eq)

mkTyVar n       = Type $ HsTyVar n
mkTyCon n       = Type $ HsTyCon n
mkTyApp t1 t2   = Type $ HsTyApp t1 t2
mkTyFun t1 t2   = Type $ HsTyFun t1 t2
mkTyTuple ts    = Type $ HsTyTuple ts
mkTyAll n t     = TyAll n t


instance Printable Type where
    ppi (Type t)    = ppi t
    ppi (TyAll n t) = text "forall" <+> ppi n <> text "." $$ nest 4 (ppi t)




isFun :: Type -> Bool
isFun (Type (HsTyFun _ _))      = True
isFun _                         = False


applyType :: Term -> Type -> Term
applyType (term, (TyAll a s)) t = (term, substType t a s) 
applyType _ _                   = error "applyType: to a non-forall type"


substType :: Type -> HsName -> Type -> Type
substType t v ty@(TyAll n x)
    | n == v    = ty
    | otherwise = mkTyAll n (substType t v x)
substType t v ty@(Type (HsTyVar n))
    | n == v    = t
    | otherwise = ty
substType t v (Type s) 
    = Type $ mapT (substType t v) s


--
--------------------------------------------------------------------------------



--------------------------------------------------------------------------------
-- Terms
--

type Term = (HsExp, Type)


dom :: Term -> Type
dom (_, Type (HsTyFun t _)) = t
dom _                       = error "dom: of a non-function term"


applyTerm :: Term -> Term -> Term
applyTerm (s, (Type (HsTyFun dom cdom))) (t, ty)
    | dom == ty     = (hsApp s t, cdom)
    | otherwise     = error $ "applyTerm: wrong types" ++ show dom ++ show ty
applyTerm _ _       = error "applyTerm: applying to non-function"


ppTerm (t,ty)   = ppi t <> text ":" <+> ppi ty

--
--------------------------------------------------------------------------------