{-# LANGUAGE InstanceSigs #-}
module Types where

import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.List ( intercalate )

import Terms ( Term )

-- Types
data Type
    = TypeVar String
    | BaseType String
    | Arrow Type Type
    deriving (Eq, Ord)
instance Show Type where
    show :: Type -> String
    show (TypeVar v) = v
    show (BaseType b) = b
    show (Arrow t1 t2) = go t1 ++ " -> " ++ show t2
        where
            go (Arrow t3 t4) = "(" ++ go t3 ++ " -> " ++ show t4 ++ ")"
            go t = show t

-- type variables occuring in type
typeVars :: Type -> [String]
typeVars (TypeVar v) = [v]
typeVars (BaseType _) = []
typeVars (Arrow t1 t2) = typeVars t1 ++ typeVars t2

-- substitute a type for a type variable
typeSubst :: Type -> String -> Type -> Type
typeSubst tp@(TypeVar x) y sp = if x == y then sp else tp
typeSubst tp@(BaseType _) _ _ = tp
typeSubst (Arrow tp1 tp2) y tp3 = Arrow (typeSubst tp1 y tp3) (typeSubst tp2 y tp3)

-- Contexts
type Context = Map String Type
showContext :: Context -> String
showContext ctx | Map.null ctx = ""
showContext ctx = "[" ++ intercalate ", " (map (\(name, tp) -> name ++ " : " ++ show tp) $ Map.toList ctx) ++ "]"
emptyContext :: Context
emptyContext = Map.empty

-- Term in Context
data TermInContext = TermInContext Context Term Type
instance Show TermInContext where
    show :: TermInContext -> String
    show (TermInContext ctx term tp) = showContext ctx ++ " |- " ++ show term ++ " : " ++ show tp