content: 
  module DDC.Core.Check.Judge.DataDefs
          (checkDataDefs)
  where
  import DDC.Core.Check.Config
  import DDC.Core.Check.Error
  import DDC.Type.DataDef
  import DDC.Type.Exp.Simple
  import DDC.Data.Pretty
  import Data.Maybe
  import DDC.Core.Env.EnvT                (EnvT)
  import Data.Set                         (Set)
  import qualified DDC.Type.Env           as Env
  import qualified Data.Set               as Set
  import qualified Data.Map               as Map
  
  
  -------------------------------------------------------------------------------
  -- | Check some data type definitions.
  --   TODO: we're not kind checking the data type declarations.
  checkDataDefs
          :: (Ord n, Show n, Pretty n)
          => Config n
          -> EnvT   n
          -> [DataDef n]
          -> ([ErrorData n], [DataDef n])
  
  checkDataDefs config env defs
   = let
          -- Primitive type constructors.
          primTypeCtors
                  = Set.fromList
                  $ Map.keys $ Env.envMap   $ configPrimKinds config
  
          -- Primitive data type constructors
          primDataTypeCtors
                  = Set.fromList
                  $ Map.keys $ dataDefsTypes $ configPrimDataDefs config
  
          -- Primitive data constructors
          primDataCtors
                  = Set.fromList
                  $ Map.keys $ dataDefsCtors $ configPrimDataDefs config
  
     in   checkDataDefs' env
                  (Set.union primTypeCtors primDataTypeCtors)
                  primDataCtors
                  [] []
                  defs
  
  
  checkDataDefs'
          :: (Ord n, Show n, Pretty n)
          => EnvT n               -- ^ Type equations.
          -> Set n                -- ^ Names of existing data types.
          -> Set n                -- ^ Names of existing data constructor.
          -> [ErrorData n]        -- ^ Errors found so far.
          -> [DataDef n]          -- ^ Checked data defs.
          -> [DataDef n]          -- ^ Data defs still to check.
          -> ([ErrorData n], [DataDef n])
  
  checkDataDefs' env nsTypes nsCtors errs dsChecked ds
   -- We've checked all the defs.
   | []   <- ds
   = (reverse errs, reverse dsChecked)
  
   -- Keep checking defs.
   | d : ds' <- ds
   = case checkDataDef env nsTypes nsCtors d of
  
      -- There are errors in this def.
      Left errs'
       -> checkDataDefs' env
                  (Set.insert (dataDefTypeName d) nsTypes)
                  (Set.fromList $ fromMaybe [] $ dataCtorNamesOfDataDef d)
                  (errs ++ errs') dsChecked ds'
  
      -- This def is ok.
      Right d'
       -> checkDataDefs' env
                  (Set.insert (dataDefTypeName d') nsTypes)
                  (Set.fromList $ fromMaybe [] $ dataCtorNamesOfDataDef d)
                  errs (d' : dsChecked) ds'
  
   | otherwise
   = error "ddc-core.checkDataDefs: bogus warning suppression"
  
  
  -- DataDef --------------------------------------------------------------------
  -- | Check a data type definition.
  checkDataDef
          :: (Ord n, Show n, Pretty n)
          => EnvT n               -- ^ Environment of types.
          -> Set n                -- ^ Names of existing data types.
          -> Set n                -- ^ Names of existing data constructors.
          -> DataDef n            -- ^ Data type definition to check.
          -> Either [ErrorData n] (DataDef n)
  
  checkDataDef env nsTypes nsCtors def
  
   -- Check the data type name is not already defined.
   | Set.member (dataDefTypeName def) nsTypes
   = Left [ErrorDataDupTypeName (dataDefTypeName def)]
  
   -- No data constructors to check.
   | Nothing      <- dataDefCtors def
   = Right def
  
   -- Check the data constructors.
   | Just ctors   <- dataDefCtors def
   = case checkDataCtors env nsCtors [] def [] ctors of
          Left errs       -> Left errs
          Right ctors'    -> Right $ def { dataDefCtors = Just ctors' }
  
   | otherwise
   = error "ddc-core.checkDataDef: bogus warning suppression"
  
  
  -- Ctors ----------------------------------------------------------------------
  -- | Check the data constructor definitions from a single data type.
  checkDataCtors
          :: (Ord n, Show n, Pretty n)
          => EnvT n               -- ^ Environment of types
          -> Set n                -- ^ Names of existing data constructors.
          -> [ErrorData n]        -- ^ Errors found so far.
          -> DataDef n            -- ^ The DataDef these constructors relate to.
          -> [DataCtor  n]        -- ^ Checked constructor defs.
          -> [DataCtor  n]        -- ^ Constructor defs still to check.
          -> Either [ErrorData n] [DataCtor n]
  
  checkDataCtors env nsCtors errs def csChecked cs
   -- We've checked all the constructors and there were no errors.
   | []   <- cs, []   <- errs
   = Right (reverse csChecked)
  
   -- We've checked all the constructors and there were errors with some of them.
   | []   <- cs
   = Left  (reverse errs)
  
   -- Keep checking constructors.
   | c : cs' <- cs
   = case checkDataCtor env nsCtors def c of
          Left  err -> checkDataCtors env
                          (Set.insert (dataCtorName c) nsCtors)
                          (err : errs) def csChecked cs'
  
          Right c'  -> checkDataCtors env
                          (Set.insert (dataCtorName c') nsCtors)
                          errs         def (c' : csChecked) cs'
  
   | otherwise
   = error "ddc-core.checkDataCtors: bogus warning suppression"
  
  
  -- Ctor -----------------------------------------------------------------------
  -- | Check a single data constructor definition.
  checkDataCtor
          :: (Ord n, Show n, Pretty n)
          => EnvT n               -- ^ Environment of types.
          -> Set n                -- ^ Names of existing data constructors.
          -> DataDef  n           -- ^ Def of data type for this constructor.
          -> DataCtor n           -- ^ Data constructor to check.
          -> Either (ErrorData n) (DataCtor n)
  
  checkDataCtor env nsCtors def ctor
  
   -- Check the constructor name is not already defined.
   | Set.member (dataCtorName ctor) nsCtors
   = Left $ ErrorDataDupCtorName (dataCtorName ctor)
  
   -- Check that the constructor produces a value of the associated data type.
   | not $ equivT env (dataTypeOfDataDef def) (dataCtorResultType ctor)
   = Left $ ErrorDataWrongResult
                  (dataCtorName ctor)
                  (dataCtorResultType ctor) (dataTypeOfDataDef def)
  
   -- This constructor looks ok.
   | otherwise
   = Right ctor
  
  