--------------------------------------------------------------------------
-- |
-- Module      :  Typed.Type
-- Copyright   :  (c) Thanos Tsouanas 2010
-- License     :  BSD
-- Maintainer  :  thanos@sians.org
-- Stability   :  experimental
--
-- Types of the typed system.
--
--------------------------------------------------------------------------
module Typed.Type ( 
       -- * Data types
         Type(..)
       , Typing
       , Context
       -- * Supplamentary creators and extractors
       , baptize
       , dom
       , codom
       , context
       , arrowize
       , appType
       , ifType
       ) where
--------------------------------------------------------------------------
import Maybe    ( fromMaybe )
import Char     ( toUpper )
--------------------------------------------------------------------------


-- | Definition of types for this calculus.
data Type = TpUnit               -- ^ Unit type.
          | TpBool               -- ^ Boolean type.
          | TpNat                -- ^ Natural numbers type.
          | TpArrow Type Type    -- ^ Function type.
          | TpCustom String      -- ^ Custom-named type.
          | TpBap String         -- ^ Baptized type.
          | TpWrong String       -- ^ Wrong type, with an explanation of what went wrong.
          deriving (Eq, Show)

-- | A typing of a variable name to a type.
type Typing = (String, Type)

-- | A series of typings.
type Context = [Typing]


{- Helper typers and creators -}

-- | Make up a type name for the given variable.
baptize :: String -> Type
baptize = TpBap . map toUpper

-- | Return /just/ the domain of an arrow.
-- If the type has been made up, make up another one for its domain.
dom :: Type -> Maybe Type
dom (p1 `TpArrow` _)  = Just p1
dom (TpBap p)         = Just $ TpBap $ "dom(" ++ p ++ ")"
dom _                 = Nothing

-- | Return /just/ the codomain of an arrow.
-- If the type has been made up, make upanother one for its domain.
codom :: Type -> Maybe Type
codom (_ `TpArrow` p2)  = Just p2
codom (TpBap p)         = Just $ TpBap $ "codom(" ++ p ++ ")"
codom _                 = Nothing

-- | Type many variables at once with a single Type, returning a Context.
context :: [String] -> Type -> Context
context xs p  = map (\x -> (x,p)) xs

-- | Turn a list of types into an arrow by associating to the right.
-- (Something like foldr1 TpArrow types but returns Unit if empty.)
arrowize :: [Type] -> Type
arrowize []      = TpUnit
arrowize [p]     = p
arrowize ps      = foldr1 TpArrow ps

-- | Try to type two given types as an application.
appType :: Type -> Type -> Type
appType p1 p2 = case (dom p1) of
    Nothing            -> TpWrong $ show p1 ++ " is not arrow-ish"
    Just p1dom
        | p1dom /= p2  -> TpWrong $ "arrow " ++ show p1 ++ " should have domain " ++ show p2
        | otherwise    -> fromMaybe
                              (TpWrong $ "cannot infer the codomain of " ++ show p1)
                              (codom p1)

-- | Try to type three given types as a branching.
ifType :: Type -> Type -> Type -> Type
ifType p p1 p2
    | p /= TpBool  = TpWrong "predicate is not boolean"
    | p1 == p2     = p1
    | otherwise    = TpWrong $ "either " ++ show p1 ++ " or " ++ show p2