    {-# LANGUAGE CPP #-}

    module Agda.TypeChecking.Rules.Data where

    import Control.Applicative
    import Control.Monad
    import Control.Monad.Trans

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Internal
    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import qualified Agda.Syntax.Info as Info

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Polarity
    import Agda.TypeChecking.Free

    import Agda.TypeChecking.Rules.Term ( isType_ )

    import Agda.Interaction.Options

    import Agda.Utils.Monad
    import Agda.Utils.Size
    import Agda.Utils.Tuple

    #include "../../undefined.h"
    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Datatypes
    ---------------------------------------------------------------------------

    -- | Type check a datatype definition. Assumes that the type has already been
    --   checked.
    checkDataDef :: Info.DefInfo -> Induction -> QName -> [A.LamBinding] -> [A.Constructor] -> TCM ()
    checkDataDef i ind name ps cs =
        traceCall (CheckDataDef (getRange i) (qnameName name) ps cs) $ do -- TODO!! (qnameName)
    	let npars = size ps

    	-- Look up the type of the datatype.
    	t <- instantiateFull =<< typeOfConst name

    	-- The parameters are in scope when checking the constructors.
    	dataDef <- bindParameters ps t $ \tel t0 -> do

    	    -- Parameters are always hidden in constructors
    	    let tel' = hideTel tel

    	    -- The type we get from bindParameters is Θ -> s where Θ is the type of
    	    -- the indices. We count the number of indices and return s.
                (nofIxs, s) <- splitType =<< normalise t0

                when (any (`freeIn` s) [0..nofIxs - 1]) $ do
                  err <- fsep [ text "The sort of" <+> prettyTCM name
                              , text "cannot depend on its indices in the type"
                              , prettyTCM t0
                              ]
                  typeError $ GenericError $ show err

                s <- return $ raise (-nofIxs) s

                reportSDoc "tc.data.sort" 20 $ vcat
                  [ text "checking datatype" <+> prettyTCM name
                  , nest 2 $ vcat
                    [ text "type:   " <+> prettyTCM t0
                    , text "sort:   " <+> prettyTCM s
                    , text "indices:" <+> text (show nofIxs)
                    ]
                  ]

    	    -- Change the datatype from an axiom to a datatype with no constructors.
                let dataDef = Datatype { dataPars           = npars
                                       , dataIxs            = nofIxs
                                       , dataInduction      = ind
                                       , dataClause         = Nothing
                                       , dataCons           = []     -- Constructors are added later
    				   , dataSort           = s
                                       , dataHsType         = Nothing
                                       , dataAbstr          = Info.defAbstract i
                                       , dataPolarity       = []
                                       , dataArgOccurrences = []
                                       }

    	    escapeContext (size tel) $ do
    	      addConstant name ( Defn name t (defaultDisplayForm name) 0 dataDef )

    	    -- Check the types of the constructors
    	    mapM_ (checkConstructor name tel' nofIxs s ind) cs

    	    -- Return the data definition
    	    return dataDef

            let nofIxs = dataIxs dataDef
                s      = dataSort dataDef

    	-- If proof irrelevance is enabled we have to check that datatypes in
    	-- Prop contain at most one element.
    	do  proofIrr <- proofIrrelevance
    	    case (proofIrr, s, cs) of
    		(True, Prop, _:_:_) -> setCurrentRange (getRange $ map conName cs) $
                                            typeError PropMustBeSingleton
                      where conName (A.Axiom _ c _) = c
                            conName (A.ScopedDecl _ (d:_)) = conName d
                            conName _ = __IMPOSSIBLE__
    		_		    -> return ()

    	-- Add the datatype to the signature with its constructors. It was previously
    	-- added without them.
    	addConstant name (Defn name t (defaultDisplayForm name) 0 $
                                dataDef { dataCons = map cname cs }
    			 )
            computePolarity name
        where
    	cname (A.ScopedDecl _ [d]) = cname d
    	cname (A.Axiom _ x _)	   = x
    	cname _			   = __IMPOSSIBLE__ -- constructors are axioms

    	hideTel  EmptyTel		  = EmptyTel
    	hideTel (ExtendTel (Arg _ t) tel) = ExtendTel (Arg Hidden t) $ hideTel <$> tel

    	splitType (El _ (Pi _ b))  = ((+ 1) -*- id) <$> splitType (absBody b)
    	splitType (El _ (Fun _ b)) = ((+ 1) -*- raise 1) <$> splitType b
    	splitType (El _ (Sort s))  = return (0, s)
    	splitType (El _ t)	   = typeError $ DataMustEndInSort t

    -- | Type check a constructor declaration. Checks that the constructor targets
    --   the datatype and that it fits inside the declared sort.
    checkConstructor :: QName -> Telescope -> Nat -> Sort
                     -> Induction -- ^ Is the constructor inductive or coinductive?
                     -> A.Constructor -> TCM ()
    checkConstructor d tel nofIxs s ind (A.ScopedDecl scope [con]) = do
      setScope scope
      checkConstructor d tel nofIxs s ind con
    checkConstructor d tel nofIxs s ind con@(A.Axiom i c e) =
        traceCall (CheckConstructor d tel s con) $ do
    	t <- isType_ e
    	n <- size <$> getContextTelescope
    	reportSDoc "tc.data.con" 15 $ vcat
              [ sep [ text "checking that"
                    , nest 2 $ prettyTCM t
                    , text "ends in" <+> prettyTCM d
                    ]
    	  , nest 2 $ text "nofPars =" <+> text (show n)
              ]
    	constructs n t d
    	reportSDoc "tc.data.con" 15 $ sep
              [ text "checking that the type fits in"
              , nest 2 $ prettyTCM s
              ]
    	t `fitsIn` s
    	escapeContext (size tel)
    	    $ addConstant c
    	    $ Defn c (telePi tel t) (defaultDisplayForm c) 0
    	    $ Constructor (size tel) c d Nothing (Info.defAbstract i) ind
    checkConstructor _ _ _ _ _ _ = __IMPOSSIBLE__ -- constructors are axioms

    -- | Bind the parameters of a datatype. The bindings should be domain free.
    bindParameters :: [A.LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
    bindParameters [] a ret = ret EmptyTel a
    bindParameters (A.DomainFree h x : ps) (El _ (Pi (Arg h' a) b)) ret
        | h /= h'	=
    	__IMPOSSIBLE__
        | otherwise = addCtx x arg $ bindParameters ps (absBody b) $ \tel s ->
    		    ret (ExtendTel arg $ Abs (show x) tel) s
      where
        arg = Arg h a
    bindParameters (A.DomainFree h x : ps) (El _ (Fun (Arg h' a) b)) ret
        | h /= h'	=
    	__IMPOSSIBLE__
        | otherwise = addCtx x arg $ bindParameters ps (raise 1 b) $ \tel s ->
    		    ret (ExtendTel arg $ Abs (show x) tel) s
      where
        arg = Arg h a
    bindParameters _ _ _ = __IMPOSSIBLE__

    -- | Check that the arguments to a constructor fits inside the sort of the datatype.
    --   The first argument is the type of the constructor.
    fitsIn :: Type -> Sort -> TCM ()
    fitsIn t s = do
      t <- instantiateFull t
      s' <- instantiateFull (getSort t)
      reportSDoc "tc.data.fits" 10 $
        sep [ text "does" <+> prettyTCM t
            , text "of sort" <+> prettyTCM s'
            , text "fit in" <+> prettyTCM s <+> text "?"
            ]
      -- The line below would be simpler, but doesn't allow datatypes
      -- to be indexed by the universe level.
    --   noConstraints $ s' `leqSort` s
      case funView $ unEl t of
        FunV arg@(Arg h a) _ -> do
          let s' = getSort a
          cs <- s' `leqSort` s
          addConstraints cs
          x <- freshName_ (argName t)
          let v  = Arg h $ Var 0 []
              t' = piApply (raise 1 t) [v]
          addCtx x arg $ fitsIn t' (raise 1 s)
        _		     -> return ()

    -- | Check that a type constructs something of the given datatype. The first
    --   argument is the number of parameters to the datatype.
    --   TODO: what if there's a meta here?
    constructs :: Int -> Type -> QName -> TCM ()
    constructs nofPars t q = constrT 0 t
        where
    	constrT n (El s v) = constr n s v

    	constr n s v = do
    	    v <- reduce v
    	    case v of
    		Pi a b	-> underAbstraction a b $ \t ->
    			   constrT (n + 1) t
    		Fun _ b -> constrT n b
    		Def d vs
    		    | d == q -> checkParams n =<< reduce (take nofPars vs)
    						    -- we only check the parameters
    		_ -> bad $ El s v

    	bad t = typeError $ ShouldEndInApplicationOfTheDatatype t

    	checkParams n vs = zipWithM_ sameVar (map unArg vs) ps
    	    where
    		ps = reverse [ i | (i,Arg h _) <- zip [n..] vs ]

    		sameVar v i = do
    		    t <- typeOfBV i
    		    addConstraints =<< equalTerm t v (Var i [])

    -- | Force a type to be a specific datatype.
    forceData :: MonadTCM tcm => QName -> Type -> tcm Type
    forceData d (El s0 t) = liftTCM $ do
        t' <- reduce t
        d  <- canonicalName d
        case t' of
    	Def d' _
    	    | d == d'   -> return $ El s0 t'
    	    | otherwise	-> fail $ "wrong datatype " ++ show d ++ " != " ++ show d'
    	MetaV m vs	    -> do
    	    Defn _ t _ _ Datatype{dataSort = s} <- getConstInfo d
    	    ps <- newArgsMeta t
    	    noConstraints $ equalType (El s0 t') (El s (Def d ps)) -- TODO: too strict?
    	    reduce $ El s0 t'
    	_ -> typeError $ ShouldBeApplicationOf (El s0 t) d

    -- | Is the type coinductive? Returns 'Nothing' if the answer cannot
    -- be determined.

    isCoinductive :: MonadTCM tcm => Type -> tcm (Maybe Bool)
    isCoinductive t = do
      El _ t <- normalise t
      case t of
        Def q _ -> do
          def <- getConstInfo q
          case theDef def of
            Axiom       {} -> return (Just False)
            Function    {} -> return Nothing
            Datatype    { dataInduction = CoInductive } -> return (Just True)
            Datatype    { dataInduction = Inductive   } -> return (Just False)
            Record      {} -> return (Just False)
            Constructor {} -> __IMPOSSIBLE__
            Primitive   {} -> __IMPOSSIBLE__
        Var   {} -> return Nothing
        Lam   {} -> __IMPOSSIBLE__
        Lit   {} -> __IMPOSSIBLE__
        Con   {} -> __IMPOSSIBLE__
        Pi    {} -> return (Just False)
        Fun   {} -> return (Just False)
        Sort  {} -> return (Just False)
        MetaV {} -> return Nothing