{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Telescope.Path where

import Prelude hiding (null)

import qualified Data.List as List
import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal

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.Maybe
import Agda.Utils.Size

import Agda.Utils.Impossible


-- | In an ambient context Γ, @telePiPath f lams Δ t bs@ builds a type that
-- can be @'telViewPathBoundary'@ed into (TelV Δ t, bs').
--   Γ.Δ ⊢ t
--   bs = [(i,u_i)]
--   Δ = Δ0,(i : I),Δ1
--   ∀ b ∈ {0,1}.  Γ.Δ0 | lams Δ1 (u_i .b) : (telePiPath f Δ1 t bs)(i = b) -- kinda: see lams
--   Γ ⊢ telePiPath f Δ t bs
telePiPath :: (Abs Type -> Abs Type) -> ([Arg ArgName] -> Term -> Term) -> Telescope -> Type -> Boundary -> TCM Type
telePiPath :: (Abs Type -> Abs Type)
-> ([Arg ArgName] -> Term -> Term)
-> Telescope
-> Type
-> Boundary
-> TCM Type
telePiPath = \ Abs Type -> Abs Type
reAbs [Arg ArgName] -> Term -> Term
lams Telescope
tel Type
t (Boundary [(Int, (Term, Term))]
bs) -> do
  pathP <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> TCMT IO (Maybe Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> TCMT IO (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' BuiltinId
builtinPathP
  let
    loop :: [Int] -> Telescope -> TCM Type
    loop []     Telescope
EmptyTel          = Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    loop (Int
x:[Int]
xs) (ExtendTel Dom Type
a Abs Telescope
tel) = do
        b <- (Telescope -> TCM Type) -> Abs Telescope -> TCMT IO (Abs Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
traverse ([Int] -> Telescope -> TCM Type
loop [Int]
xs) Abs Telescope
tel
        case List.find ((x ==) . fst) bs of
          -- Create a Path type.
          Just (Int
_,(Term
u0,Term
u1)) -> do
            let names :: [Arg ArgName]
names = Telescope -> [Arg ArgName]
teleArgNames (Telescope -> [Arg ArgName]) -> Telescope -> [Arg ArgName]
forall a b. (a -> b) -> a -> b
$ Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel
            -- assume a = 𝕀
            l <- Abs Type -> TCM Level
getLevel Abs Type
b
            return $ El (Type l) $
              pathP `apply`
                [ argH (Level l)
                , argN (Lam defaultArgInfo (unEl <$> b))
                , argN $ lams names u0
                , argN $ lams names u1
                ]
          Maybe (Int, (Term, Term))
Nothing    -> do
            -- Create a Π type.
            Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
a Abs Type
b) (Dom Type -> Abs Type -> Term
Pi Dom Type
a (Abs Type -> Abs Type
reAbs Abs Type
b))
    loop (Int
_:[Int]
_) Telescope
EmptyTel    = TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
    loop []    ExtendTel{} = TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
  loop (downFrom (size tel)) tel
  where
    argN :: e -> Arg e
argN = ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo
    argH :: e -> Arg e
argH = ArgInfo -> e -> Arg e
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> e -> Arg e) -> ArgInfo -> e -> Arg e
forall a b. (a -> b) -> a -> b
$ Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo
    getLevel :: Abs Type -> TCM Level
    getLevel :: Abs Type -> TCM Level
getLevel Abs Type
b = do
      s <- Abs Sort -> TCMT IO (Abs Sort)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Abs Sort -> TCMT IO (Abs Sort)) -> Abs Sort -> TCMT IO (Abs Sort)
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> Abs Type -> Abs Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b
      -- 'reAbs' ensures that 'Abs' correctly indicates an occurrence of the bound variable.
      case reAbs s of
        NoAbs ArgName
_ (Type Level
l) -> Level -> TCM Level
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
l
        Abs Sort
_ -> TypeError -> TCM Level
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Level) -> TypeError -> TCM Level
forall a b. (a -> b) -> a -> b
$ Abs Type -> TypeError
PathAbstractionFailed Abs Type
b
          -- Andreas, 2025-04-17, not impossible after all, see issue #7803.
          --
          -- Previously: 2024-10-07, issue #7413
          -- Andrea writes in https://github.com/agda/agda/issues/7413#issuecomment-2396146135
          --
          -- I believe this is actually impossible at the moment
          -- unless generalized Path types were implemented while I wasn't looking:
          --
          -- telePathPi only does this check if there's a boundary,
          -- which should only be introduced by a PathP copattern,
          -- which then should ensure the result type is in Type lvl
          -- for some lvl that does not depend on on the interval
          -- variable of the path.

-- | @telePiPath_ Δ t [(i,u)]@
--   Δ ⊢ t
--   i ∈ Δ
--   Δ ⊢ u_b : t  for  b ∈ {0,1}
telePiPath_ :: Telescope -> Type -> Boundary -> TCM Type
telePiPath_ :: Telescope -> Type -> Boundary -> TCM Type
telePiPath_ Telescope
tel Type
t Boundary
bndry = do
  ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Int
40                  (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"tel  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
  ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
  ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"bndry" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Boundary -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Boundary
bndry

  (Abs Type -> Abs Type)
-> ([Arg ArgName] -> Term -> Term)
-> Telescope
-> Type
-> Boundary
-> TCM Type
telePiPath Abs Type -> Abs Type
forall a. a -> a
id [Arg ArgName] -> Term -> Term
forall {t :: * -> *}. Foldable t => t (Arg ArgName) -> Term -> Term
argsLam Telescope
tel Type
t Boundary
bndry
 where
   argsLam :: t (Arg ArgName) -> Term -> Term
argsLam t (Arg ArgName)
args Term
tm = Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible Int
1 Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
     (Arg ArgName -> Term -> Term) -> Term -> t (Arg ArgName) -> Term
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Arg{argInfo :: forall e. Arg e -> ArgInfo
argInfo = ArgInfo
ai, unArg :: forall e. Arg e -> e
unArg = ArgName
x} -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
x) Term
tm t (Arg ArgName)
args

-- | arity of the type, including both Pi and Path.
--   Does not reduce the type.
arityPiPath :: Type -> TCM Int
arityPiPath :: Type -> TCM Int
arityPiPath Type
t = do
  Type -> TCMT IO (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath Type
t TCMT IO (Either (Dom Type, Abs Type) Type)
-> (Either (Dom Type, Abs Type) Type -> TCM Int) -> TCM Int
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (Dom Type
_, Abs Type
u) -> (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Int) -> TCM Int -> TCM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Int
arityPiPath (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
u)
    Right Type
_     -> Int -> TCM Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0

-- | Collect the interval copattern variables as list of de Bruijn indices.
class IApplyVars p where
  iApplyVars :: p -> [Int]

instance DeBruijn a => IApplyVars (Pattern' a) where
  iApplyVars :: Pattern' a -> [Int]
iApplyVars = \case
    IApplyP PatternInfo
_ Term
t Term
u a
x -> [ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ a -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView a
x ]
    VarP{}          -> []
    ProjP{}         -> []
    LitP{}          -> []
    DotP{}          -> []
    DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps     -> [NamedArg (Pattern' a)] -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg (Pattern' a)]
ps
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps     -> [NamedArg (Pattern' a)] -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg (Pattern' a)]
ps

instance IApplyVars p => IApplyVars (NamedArg p) where
  iApplyVars :: NamedArg p -> [Int]
iApplyVars = p -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars (p -> [Int]) -> (NamedArg p -> p) -> NamedArg p -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg p -> p
forall a. NamedArg a -> a
namedArg

instance IApplyVars p => IApplyVars [p] where
  iApplyVars :: [p] -> [Int]
iApplyVars = (p -> [Int]) -> [p] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap p -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars

{-# SPECIALIZE isInterval :: Type -> TCM Bool #-}
-- | Check whether a type is the built-in interval type.
isInterval :: (MonadTCM m, MonadReduce m) => Type -> m Bool
isInterval :: forall (m :: * -> *). (MonadTCM m, MonadReduce m) => Type -> m Bool
isInterval Type
t = TCM Bool -> m Bool
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> m Bool) -> TCM Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
  TCMT IO (Maybe QName)
-> TCM Bool -> (QName -> TCM Bool) -> TCM Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' BuiltinId
builtinInterval) (Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) ((QName -> TCM Bool) -> TCM Bool)
-> (QName -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \ QName
i -> do
  Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) TCMT IO Term -> (Term -> Bool) -> TCM Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Def QName
q [] -> QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
i
    Term
_        -> Bool
False