--------------------------------------------------------------------------
-- |
-- Module      :  Typed.TypeSystem
-- Copyright   :  (c) Thanos Tsouanas 2010
-- License     :  BSD
-- Maintainer  :  thanos@sians.org
-- Stability   :  experimental
--
-- Type system of the typed system.
--
--------------------------------------------------------------------------
module Typed.TypeSystem ( typeOf ) where
--------------------------------------------------------------------------
import Typed.Term    ( Term(..) )
import Typed.Type    ( Type(..), Context, baptize, ifType, appType )
import Maybe         ( fromMaybe )
--------------------------------------------------------------------------


-- | Tries to type the given 'Term', w.r.t. the given 'Context'.
typeOf :: Context -> Term -> Type
typeOf ctx term = case term of

    -- unit
    TmUnit                     -> TpUnit

    -- booleans
    TmTrue                     -> TpBool
    TmFalse                    -> TpBool
    TmIsZero t
      | typeOf ctx t == TpNat  -> TpBool
      | otherwise              -> TpWrong "only numbers can be tested for zeroness"

    -- arithmetic
    TmZero                     -> TpNat
    TmSucc t
      | typeOf ctx t == TpNat  -> TpNat
      | otherwise              -> TpWrong "can only apply succ to numbers"
    TmPred t
      | typeOf ctx t == TpNat  -> TpNat
      | otherwise              -> TpWrong "can only apply pred to numbers"

    -- lambda calculus
    TmVar x                    -> fromMaybe (baptize x) (lookup x ctx)
    TmAbs r@(_,p) t            -> p `TpArrow` (typeOf (r:ctx) t)
    t1 `TmApp` t2              -> appType p1 p2   where [p1,p2]    = map (typeOf ctx) [t1,t2]
    TmIf t t1 t2               -> ifType p p1 p2  where [p,p1,p2]  = map (typeOf ctx) [t,t1,t2]

    -- special
    TmLoop                     -> TpWrong "BOTTOM"
    _________________________  -> TpWrong $ "cannot type term " ++ show term