module Momo.CoreTyping
  ( CoreTyping(..)
  ) where

import Control.Monad.Catch (MonadThrow)

import Momo.CoreSyntax (CoreSyntax)
import Momo.CoreSyntax qualified as Core
import Momo.Env (Env)
import Momo.Path (Path)

class CoreSyntax term => CoreTyping term where
  -- Typing
  typeTerm     :: MonadThrow m => Env term -> term -> m (Core.Val term)
  kindDefType  :: MonadThrow m => Env term -> Core.Def term -> m (Core.Kind term)
  checkValType :: MonadThrow m => Env term -> Core.Val term -> m ()
  checkKind    :: MonadThrow m => Env term -> Core.Kind term -> m ()

  -- Type matching
  valTypeMatch :: Env term -> Core.Val term -> Core.Val term -> Bool
  defTypeEquiv :: Env term -> Core.Kind term -> Core.Def term -> Core.Def term -> Bool
  kindMatch    :: Env term -> Core.Kind term -> Core.Kind term -> Bool

  deftypeOfPath :: Path -> Core.Kind term -> Core.Def term