    {-# 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.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.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 @telViewPathBoundaryP'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
    bs = do
      Maybe Term
    mpp <- ArgName -> TCMT IO (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
    getTerm' ArgName
    builtinPathP
      Term
    io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
      let
        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' Term)
    getLevel Abs Type
    b = do
          Abs Sort
    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
          case Abs Sort
    s of
            NoAbs ArgName
    _ (Type Level' Term
    l) -> Level' Term -> TCM (Level' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Level' Term
    l
            Abs ArgName
    n (Type Level' Term
    l) | Bool -> Bool
    not (Int -> Abs Sort -> Bool
    forall a. Free a => Int -> a -> Bool
    freeIn Int
    0 Abs Sort
    s) -> Level' Term -> TCM (Level' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Level' Term -> TCM (Level' Term))
    -> Level' Term -> TCM (Level' Term)
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Abs (Level' Term) -> Level' Term
    forall a. Subst a => Impossible -> Abs a -> a
    noabsApp Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (ArgName -> Level' Term -> Abs (Level' Term)
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    n Level' Term
    l)
            Abs Sort
    _ -> TypeError -> TCM (Level' Term)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM (Level' Term))
    -> (Doc -> TypeError) -> Doc -> TCM (Level' Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgName -> TypeError
    GenericError (ArgName -> TypeError) -> (Doc -> ArgName) -> Doc -> TypeError
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> ArgName
    forall a. Show a => a -> ArgName
    show (Doc -> TCM (Level' Term)) -> TCMT IO Doc -> TCM (Level' Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                 (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    "The type is non-fibrant or its sort depends on an interval variable" 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
    prettyTCM (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b))
                 -- TODO better Type Error
        telePiPath :: [Int] -> Telescope -> TCM Type
        telePiPath :: [Int] -> Telescope -> TCM Type
    telePiPath []     Telescope
    EmptyTel          = Type -> TCM Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type -> TCM Type) -> Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Type
    t
        telePiPath (Int
    x:[Int]
    xs) (ExtendTel Dom Type
    a Abs Telescope
    tel)
          = case ((Term, (Term, Term)) -> Bool)
    -> Boundary -> Maybe (Term, (Term, Term))
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find (\ (Term
    t,(Term, Term)
    _) -> Term
    t Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Term
    var Int
    x) Boundary
    bs of
              Just (Term
    _,(Term, Term)
    u) -> do
                let pp :: Term
    pp = Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Maybe Term
    mpp
                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 = 𝕀
                Abs Type
    b <- TCMT IO (Abs Type)
    b
                Level' Term
    l <- Abs Type -> TCM (Level' Term)
    getLevel Abs Type
    b
                Type -> TCM Type
    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 (Level' Term -> Sort
    forall t. Level' t -> Sort' t
    Type Level' Term
    l) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $
                  Term
    pp Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ Term -> Arg Term
    forall {e}. e -> Arg e
    argH (Level' Term -> Term
    Level Level' Term
    l)
                             , Term -> Arg Term
    forall {e}. e -> Arg e
    argN (ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Abs Type -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Type
    b))
                             , Term -> Arg Term
    forall {e}. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ [Arg ArgName] -> Term -> Term
    lams [Arg ArgName]
    names ((Term, Term) -> Term
    forall a b. (a, b) -> a
    fst (Term, Term)
    u)
                             , Term -> Arg Term
    forall {e}. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ [Arg ArgName] -> Term -> Term
    lams [Arg ArgName]
    names ((Term, Term) -> Term
    forall a b. (a, b) -> b
    snd (Term, Term)
    u)
                             ]
              Maybe (Term, (Term, Term))
    Nothing    -> do
                Abs Type
    b <- TCMT IO (Abs Type)
    b
                Type -> TCM Type
    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))
          where
            b :: TCMT IO (Abs Type)
    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)
    traverse ([Int] -> Telescope -> TCM Type
    telePiPath [Int]
    xs) Abs Telescope
    tel
        telePiPath [Int]
    _     Telescope
    EmptyTel = TCM Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        telePiPath []    Telescope
    _        = TCM Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      [Int] -> Telescope -> TCM Type
    telePiPath (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel)) Telescope
    tel

    -- | @telePiPath_ Δ t [(i,u)]@
    --   Δ ⊢ t
    --   i ∈ Δ
    --   Δ ⊢ u_b : t  for  b ∈ {0,1}
    telePiPath_ :: Telescope -> Type -> [(Int,(Term,Term))] -> TCM Type
    telePiPath_ :: Telescope -> Type -> [(Int, (Term, Term))] -> TCM Type
    telePiPath_ Telescope
    tel Type
    t [(Int, (Term, Term))]
    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
    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
    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
    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
    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
    <+> [(Int, (Term, Term))] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [(Int, (Term, Term))]
    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 [(Int -> Term
    var Int
    i, (Term, Term)
    u) | (Int
    i , (Term, Term)
    u) <- [(Int, (Term, Term))]
    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 (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
      Either (Dom Type, Abs Type) Type
    t' <- Type -> TCMT IO (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    piOrPath Type
    t
      case Either (Dom Type, Abs Type) Type
    t' of
        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 (m :: * -> *) a. Monad m => a -> m a
    return Int
    0

    iApplyVars :: DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
    iApplyVars :: forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
    iApplyVars [NamedArg (Pattern' a)]
    ps = ((Pattern' a -> [Int]) -> [Pattern' a] -> [Int])
    -> [Pattern' a] -> (Pattern' a -> [Int]) -> [Int]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Pattern' a -> [Int]) -> [Pattern' a] -> [Int]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((NamedArg (Pattern' a) -> Pattern' a)
    -> [NamedArg (Pattern' a)] -> [Pattern' a]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' a) -> Pattern' a
    forall a. NamedArg a -> a
    namedArg [NamedArg (Pattern' a)]
    ps) ((Pattern' a -> [Int]) -> [Int]) -> (Pattern' a -> [Int]) -> [Int]
    forall a b. (a -> b) -> a -> b
    $ \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__ (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 a. DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
    iApplyVars [NamedArg (Pattern' a)]
    ps
                                 ConP ConHead
    _ ConPatternInfo
    _ [NamedArg (Pattern' a)]
    ps -> [NamedArg (Pattern' a)] -> [Int]
    forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
    iApplyVars [NamedArg (Pattern' a)]
    ps

    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 (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
      Maybe QName
    mi <- ArgName -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
    getName' ArgName
    builtinInterval
      Maybe QName -> TCM Bool -> (QName -> TCM Bool) -> TCM Bool
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe QName
    mi (Bool -> TCM Bool
    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
    t <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t
      case Term
    t of
        Def QName
    q [] -> Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCM Bool) -> Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    i
        Term
    _        -> Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCM Bool) -> Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    False