content: module Agda2Hs.Compile.TypeDefinition where
  
  import Control.Monad ( unless )
  
  import Data.Maybe ( fromMaybe )
  
  import Agda.Compiler.Backend
  
  import Agda.Syntax.Common ( namedArg )
  import Agda.Syntax.Internal
  import Agda.Syntax.Internal.Pattern
  
  import Agda.TypeChecking.Telescope ( mustBePi )
  
  import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
  import Agda.Utils.Monad
  
  import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTypeArgs )
  import Agda2Hs.Compile.Types
  import Agda2Hs.Compile.Utils
  import Agda2Hs.Compile.Var ( compileDBVar )
  import Agda.Syntax.Common.Pretty (prettyShow)
  import Agda.TypeChecking.Substitute
  
  import qualified Agda2Hs.Language.Haskell as Hs
  import Agda2Hs.Language.Haskell.Utils ( hsName )
  
  compileTypeDef :: Hs.Name () -> Definition -> C [Hs.Decl ()]
  compileTypeDef name (Defn {..}) = do
    unlessM (isTransparentFunction defName) $ checkValidTypeName name
    Clause{..} <- singleClause funClauses
    addContext (KeepNames clauseTel) $ do
      as <- compileTypePatternArgs defType namedClausePats
      let hd = foldl (Hs.DHApp ()) (Hs.DHead () name) as
      rhs <- compileType $ fromMaybe __IMPOSSIBLE__ clauseBody
      return [Hs.TypeDecl () hd rhs]
    where
      Function{..} = theDef
      singleClause = \case
        [cl] -> return cl
        _    -> agda2hsError "Not supported: type definition with several clauses"
  
  compileTypePatternArgs :: Type -> NAPs -> C [Hs.TyVarBind ()]
  compileTypePatternArgs ty naps = do
    aux <- compileTypeArgs ty $ fromMaybe __IMPOSSIBLE__ $ allApplyElims $ patternsToElims naps
    mapM assertIsTyVarBind aux
    where
      assertIsTyVarBind :: Hs.Type () -> C (Hs.TyVarBind ())
      assertIsTyVarBind = \case
        Hs.TyVar _ n -> pure $ Hs.UnkindedVar () n
        _ -> agda2hsError "Not supported: type definition by pattern matching"
  
  compileTypeArg :: DeBruijnPattern -> C (Hs.TyVarBind ())
  compileTypeArg p@(VarP o i) = do
    name <- hsName <$> compileDBVar (dbPatVarIndex i)
    checkValidTyVarName name
    return $ Hs.UnkindedVar () name
  compileTypeArg _ = agda2hsError "Not supported: type definition by pattern matching"
  