{-# LANGUAGE CPP                      #-}
{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Primitive.Cubical where
import Prelude hiding (null, (!!))

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Internal

import Control.Monad
import Control.Monad.Reader
import Control.Monad.Trans ( lift )

import Agda.TypeChecking.Names
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin


import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope

import Agda.Utils.Except

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


-- | Tries to @primTransp@ a whole telescope of arguments, following the rule for Σ types.
--   If a type in the telescope does not support transp, @transpTel@ throws it as an exception.
transpTel :: Abs Telescope -- Γ ⊢ i.Δ
          -> Term          -- Γ ⊢ φ : F  -- i.Δ const on φ
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> ExceptT (Closure (Abs Type)) TCM Args      -- Γ ⊢ Δ[1]
transpTel delta phi args = do
  tTransp <- liftTCM primTrans
  imin <- liftTCM primIMin
  imax <- liftTCM primIMax
  ineg <- liftTCM primINeg
  let
    noTranspError t = lift . throwError =<< liftTCM (buildClosure t)
    bapp :: (Applicative m, Subst t a) => m (Abs a) -> m t -> m a
    bapp t u = lazyAbsApp <$> t <*> u
    gTransp (Just l) t phi a = pure tTransp <#> l <@> (Lam defaultArgInfo . fmap unEl <$> t) <@> phi <@> a
    gTransp Nothing  t phi a = do
      -- Γ ⊢ i.Ξ
      xi <- (open =<<) $ do
        bind "i" $ \ i -> do
          TelV xi _ <- (liftTCM . telView =<<) $ t `bapp` i
          return xi
      argnames <- do
        teleArgNames . unAbs <$> xi
      glamN argnames $ \ xi_args -> do
        b' <- bind "i" $ \ i -> do
          ti <- t `bapp` i
          xin <- bind "i" $ \ i -> xi `bapp` (pure ineg <@> i)
          xi_args <- xi_args
          ni <- pure ineg <@> i
          phi <- phi
          lift $ piApplyM ti =<< trFillTel xin phi xi_args ni
        axi <- do
          a <- a
          xif <- bind "i" $ \ i -> xi `bapp` (pure ineg <@> i)
          phi <- phi
          xi_args <- xi_args
          lift $ apply a <$> transpTel xif phi xi_args
        s <- reduce $ getSort (absBody b')
        case s of
          Type l -> do
            l <- open $ lam_i (Level l)
            b' <- open b'
            axi <- open axi
            gTransp (Just l) b' phi axi
          Inf    ->
            case 0 `freeIn` (raise 1 b' `lazyAbsApp` var 0) of
              False -> return axi
              True -> noTranspError b'
          _ -> noTranspError b'
    lam_i = Lam defaultArgInfo . Abs "i"
    go :: Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args
    go EmptyTel            _   []       = return []
    go (ExtendTel t delta) phi (a:args) = do
      -- Γ,i ⊢ t
      -- Γ,i ⊢ (x : t). delta
      -- Γ ⊢ a : t[0]
      s <- reduce $ getSort t
      -- Γ ⊢ b : t[1], Γ,i ⊢ b : t[i]
      (b,bf) <- runNamesT [] $ do
        l <- case s of
               Inf -> return Nothing
               Type l -> Just <$> open (lam_i (Level l))
               _ -> noTranspError (Abs "i" (unDom t))
        t <- open $ Abs "i" (unDom t)
        [phi,a] <- mapM open [phi, unArg a]
        b <- gTransp l t phi a
        bf <- bind "i" $ \ i -> do
                            gTransp ((<$> l) $ \ l -> lam "j" $ \ j -> l <@> (pure imin <@> i <@> j))
                                    (bind "j" $ \ j -> t `bapp` (pure imin <@> i <@> j))
                                    (pure imax <@> (pure ineg <@> i) <@> phi)
                                    a
        return (b, absBody bf)
      (:) (b <$ a) <$> go (lazyAbsApp delta bf) phi args
    go (ExtendTel t delta) phi []    = __IMPOSSIBLE__
    go EmptyTel            _   (_:_) = __IMPOSSIBLE__
  go (absBody delta) phi args

-- | Like @transpTel@ but performing a transpFill.
trFillTel :: Abs Telescope -- Γ ⊢ i.Δ
          -> Term
          -> Args          -- Γ ⊢ δ : Δ[0]
          -> Term          -- Γ ⊢ r : I
          -> ExceptT (Closure (Abs Type)) TCM Args      -- Γ ⊢ Δ[r]
trFillTel delta phi args r = do
  imin <- liftTCM primIMin
  imax <- liftTCM primIMax
  ineg <- liftTCM primINeg
  transpTel (Abs "j" $ raise 1 delta `lazyAbsApp` (imin `apply` (map argN [var 0, raise 1 r])))
            (imax `apply` [argN $ ineg `apply` [argN r], argN phi])
            args