content: 
  -- | Type checker for the Disciple Core language.
  --
  --   The functions in this module do not check for language fragment compliance.
  --   This needs to be done separately via "DDC.Core.Fragment".
  --
  module DDC.Core.Check
          ( -- * Configuration
            Config(..)
          , configOfProfile
  
            -- * Type checker trace
          , CheckTrace (..)
  
            -- * Checking Modules
          , Oracle
          , newOracleOfStore
          , checkModuleIO
          , reconModule
  
            -- * Checking Types
          , checkType,    checkTypeM
          , checkSpec
          , kindOfSpec
          , sortOfKind
  
            -- * Checking Expressions
          , Mode   (..)
          , Demand (..)
          , checkExpIO,   reconOfExp,     typeOfExp
  
            -- * Checking Witnesses
          , checkWitness, typeOfWitness
          , typeOfWiCon
  
            -- * Kinds of Constructors
          , takeSortOfKiCon
          , kindOfTwCon
          , kindOfTcCon
  
            -- * Annotations
          , AnTEC(..)
  
            -- * Error messages
          , Error         (..)
          , ErrorType     (..)
          , ErrorData     (..))
  where
  import DDC.Core.Check.Judge.Kind
  import DDC.Core.Check.Judge.Kind.TyCon
  import DDC.Core.Check.Judge.Module
  import DDC.Core.Check.Judge.Witness
  import DDC.Core.Check.Error
  import DDC.Core.Check.Exp
  import DDC.Core.Check.Context.Base
  import DDC.Core.Interface.Oracle
  import DDC.Core.Check.Base
  import qualified System.IO.Unsafe       as S
  
  
  -- | Check a type in the given universe with the given environment
  --   Returns the updated type and its classifier (a kind or sort),
  --   depeding on the universe of the type being checked.
  checkType  :: (Ord n, Show n, Pretty n)
             => Config n -> Universe -> Type n
             -> Either (Error a n) (Type n, Type n)
  
  checkType config uni tt
   = S.unsafePerformIO
   $ evalCheck (mempty, 0, 0)
   $ do   let ctx   = contextOfPrimEnvs
                          (configPrimKinds config)
                          (configPrimTypes config)
                          (configPrimDataDefs config)
  
          (t, k, _) <- checkTypeM config ctx uni tt Recon
          return (t, k)
  
  
  -- | Check a spec in the given environment, returning an error or its kind.
  checkSpec  :: (Ord n, Show n, Pretty n)
             => Config n -> Type n
             -> Either (Error a n) (Type n, Kind n)
  
  checkSpec config tt
   = S.unsafePerformIO
   $ evalCheck (mempty, 0, 0)
   $ do   let ctx   = contextOfPrimEnvs
                          (configPrimKinds config)
                          (configPrimTypes config)
                          (configPrimDataDefs config)
  
          (t, k, _) <- checkTypeM config ctx UniverseSpec tt Recon
          return (t, k)
  
  
  -- | Check a spec in an empty environment, returning an error or its kind.
  kindOfSpec
          :: (Ord n, Show n, Pretty n)
          => Config n -> Type n
          -> Either (Error a n) (Kind n)
  
  kindOfSpec config tt
   = S.unsafePerformIO
   $ evalCheck (mempty, 0, 0)
   $ do   (_, k, _) <- checkTypeM config emptyContext UniverseSpec tt Recon
          return k
  
  
  -- | Check a kind in an empty environment, returning an error or its sort.
  sortOfKind
          :: (Ord n, Show n, Pretty n)
          => Config n -> Kind n
          -> Either (Error a n) (Sort n)
  
  sortOfKind config tt
   = S.unsafePerformIO
   $ evalCheck (mempty, 0, 0)
   $ do   (_, s, _) <- checkTypeM config emptyContext UniverseKind tt Recon
          return s
  
  