{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Telescope.Path where

import Prelude hiding (null)

import Control.Applicative hiding (empty)
import Control.Monad (unless, guard)

import Data.Foldable (forM_, find)
import qualified Data.List as List
import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position

import Agda.TypeChecking.Free
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Size

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


-- | In an ambient context Γ, @telePiPath f Δ t bs@ builds a type that
-- can be @telViewPathBoundaryP'ed@ into (TelV Δ t, bs').
--   Γ.Δ ⊢ t
--   bs = [(i,u_i)]
--   Δ = Δ0,(i : I),Δ1
--   ∀ b ∈ {0,1}.  Γ.Δ0 | u_i .b : (telePiPath f Δ1 t bs)(i = b)
--   Γ ⊢ telePiPath f Δ t bs
telePiPath :: (Abs Type -> Abs Type) -> Telescope -> Type -> Boundary -> TCM Type
telePiPath reAbs tel t bs = do
  pp <- primPathP
  io <- primIOne
  let
    argN = Arg defaultArgInfo
    argH = Arg $ setHiding Hidden defaultArgInfo
    getLevel :: Abs Type -> TCM Level
    getLevel b = do
      s <- reduce $ getSort <$> b
      case s of
        NoAbs _ (Type l) -> return l
        Abs n (Type l) | NoOccurrence <- occurrence 0 s -> return $ noabsApp __IMPOSSIBLE__ (Abs n l)
        _ -> typeError . GenericError . show =<<
             (text "The type is non-fibrant or its sort depends on an interval variable" <+> prettyTCM (unAbs b))
             -- TODO better Type Error
    telePiPath :: [Int] -> Telescope -> TCM Type
    telePiPath []     EmptyTel          = pure $ t
    telePiPath (x:xs) (ExtendTel a tel)
      = case List.find (\ (t,_) -> t == var x) bs of
          Just (_,u) -> do
            -- assume a = 𝕀
            b <- b
            l <- getLevel b
            return $ El (Type l) $
              pp `apply` [ argH (Level l)
                         , argN (Lam defaultArgInfo (unEl <$> b))
                         , argN $ fst u
                         , argN $ snd u
                         ]
          Nothing    -> do
            b <- b
            return $ El (piSort (getSort a) (getSort <$> b)) (Pi a (reAbs b))
      where
        b  = traverse (telePiPath xs) tel
    telePiPath _     EmptyTel = __IMPOSSIBLE__
    telePiPath []    _        = __IMPOSSIBLE__
  telePiPath (downFrom (size tel)) tel


iApplyVars :: DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
iApplyVars ps = flip concatMap (map namedArg ps) $ \case
                             IApplyP _ t u x ->
                               [fromMaybe __IMPOSSIBLE__ (deBruijnView x)]
                             VarP{} -> []
                             ProjP{}-> []
                             LitP{} -> []
                             DotP{} -> []
                             DefP _ _ ps -> iApplyVars ps
                             ConP _ _ ps -> iApplyVars ps