pts type checker

TypeChecker.hs

-- TypeChecker.hs ---
-- Copyright (C) 2018 Hussein Ait-Lahcen
-- Author: Hussein Ait-Lahcen <[email protected]>
-- This program is free software; you can redistribute it and/or
-- modify it under the terms of the GNU General Public License
-- as published by the Free Software Foundation; either version 3
-- of the License, or (at your option) any later version.
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
-- You should have received a copy of the GNU General Public License
-- along with this program. If not, see <http://www.gnu.org/licenses/>.
{-# LANGUAGE FlexibleContexts #-}

module Kudos.TypeChecker
  ( justice
  , typecheck
  ) where

import           Control.Lens
import           Control.Monad.Error.Lens
import           Control.Monad.Except
import           Control.Monad.Reader
import           Data.Functor
import           Data.HashMap.Strict      as H
import           Data.Text                as T

import           Kudos.Config
import           Kudos.Error
import           Kudos.Normalizer
import           Kudos.Syntax             as S

import           Debug.Trace

justice :: System -> System -> Bool
justice (SPi n l r) (SPi n' l' r') =
  justice l l' && justice r (substitute n' 0 (SVar n 0) (shift n 0 r'))
justice (SLam n l r) (SLam n' l' r') =
  justice l l' && justice r (substitute n' 0 (SVar n 0) (shift n 0 r'))
justice (SApp f x) (SApp f' x') = justice f f' && justice x x'
justice (SVar n i) (SVar n' i') = n == n' && i == i'
justice (SStar u) (SStar u') = u == u'
justice _ _ = False

liftUniverse :: Universe -> Universe
liftUniverse = (+ 1)

typeUniverse :: Universe
typeUniverse = 1

kindUniverse :: Universe
kindUniverse = liftUniverse typeUniverse

injectBinding :: HasBindings t => Identifier -> S.Index -> System -> t -> t
injectBinding n i s = bindings %~ Bindings . H.insert (n, i) s . unBindings

typecheck ::
     ( HasConfiguration env
     , HasEnvironment env
     , HasBindings env
     , AsTypeError err
     , MonadReader env m
     , MonadError err m
     , Show env
     )
  => System
  -> m System
typecheck (SStar u) = pure $ SStar $ liftUniverse u
typecheck (SVar n i) = do
  binds <- view bindings
  case H.lookup (n, i) (unBindings binds) of
    Just s  -> pure s
    Nothing -> throwing _UnknowBinding (n, binds)
typecheck (SLam n l r) = do
  l' <- typecheck l
  case l' of
    (SStar _) -> do
      r' <- local (injectBinding n 0 $ normalize l) (typecheck r)
      pure $ SPi n l r'
    _ -> throwing _InvalidAbstraction l'
typecheck (SPi n l r) = do
  l' <- normalize <$> typecheck l
  r' <- normalize <$> local (injectBinding n 0 (normalize l)) (typecheck r)
  case (l', r') of
    (SStar u, SStar v) -> do
      h <- view hierarchy
      case h of
        Predicative   -> pure $ SStar $ max u v
        Impredicative -> pure $ SStar v
    _ -> throwing _InvalidProduct (l, r)
typecheck (SApp f x) = do
  f' <- normalize <$> typecheck f
  case f' of
    (SPi n l r) -> do
      x' <- typecheck x
      if justice l x'
        then pure $ normalize $ substitute n 0 x r
        else throwing _Unfairness (normalize l, normalize x')
    _ -> throwing _InvalidApplication (f', x)