{-# 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
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
l) -> Level -> TCM Level
forall (m :: * -> *) a. Monad m => a -> m a
return Level
l
        Abs ArgName
n (Type Level
l) | Bool -> Bool
not (Nat -> Abs Sort -> Bool
forall a. Free a => Nat -> a -> Bool
freeIn Nat
0 Abs Sort
s) -> Level -> TCM Level
forall (m :: * -> *) a. Monad m => a -> m a
return (Level -> TCM Level) -> Level -> TCM Level
forall a b. (a -> b) -> a -> b
$ Impossible -> Abs Level -> Level
forall a. Subst a => Impossible -> Abs a -> a
noabsApp Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (ArgName -> Level -> Abs Level
forall a. ArgName -> a -> Abs a
Abs ArgName
n Level
l)
        Abs Sort
_ -> TypeError -> TCM Level
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Level) -> (Doc -> TypeError) -> Doc -> TCM Level
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) -> TCMT IO Doc -> TCM Level
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 :: [Nat] -> 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 (Nat
x:[Nat]
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
== Nat -> Term
var Nat
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
l <- Abs Type -> TCM Level
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 -> Sort
forall t. Level' t -> Sort' t
Type Level
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
Level Level
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 ([Nat] -> Telescope -> TCM Type
telePiPath [Nat]
xs) Abs Telescope
tel
    telePiPath [Nat]
_     Telescope
EmptyTel = TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
    telePiPath []    Telescope
_        = TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
  [Nat] -> Telescope -> TCM Type
telePiPath (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Telescope -> Nat
forall a. Sized a => a -> Nat
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 -> [(Nat, (Term, Term))] -> TCM Type
telePiPath_ Telescope
tel Type
t [(Nat, (Term, Term))]
bndry = do
  ArgName -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Nat
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 -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Nat
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 -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Nat -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Nat
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
<+> [(Nat, (Term, Term))] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Nat, (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 [(Nat -> Term
var Nat
i, (Term, Term)
u) | (Nat
i , (Term, Term)
u) <- [(Nat, (Term, Term))]
bndry]
 where
   argsLam :: t (Arg ArgName) -> Term -> Term
argsLam t (Arg ArgName)
args Term
tm = Impossible -> Nat -> Substitution' Term
forall a. Impossible -> Nat -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible Nat
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 Nat
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) -> (Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+Nat
1) (Nat -> Nat) -> TCM Nat -> TCM Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Nat
arityPiPath (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
u)
    Right Type
_ -> Nat -> TCM Nat
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0

iApplyVars :: DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
iApplyVars :: [NamedArg (Pattern' a)] -> [Nat]
iApplyVars [NamedArg (Pattern' a)]
ps = ((Pattern' a -> [Nat]) -> [Pattern' a] -> [Nat])
-> [Pattern' a] -> (Pattern' a -> [Nat]) -> [Nat]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Pattern' a -> [Nat]) -> [Pattern' a] -> [Nat]
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 -> [Nat]) -> [Nat]) -> (Pattern' a -> [Nat]) -> [Nat]
forall a b. (a -> b) -> a -> b
$ \case
                             IApplyP PatternInfo
_ Term
t Term
u a
x ->
                               [Nat -> Maybe Nat -> Nat
forall a. a -> Maybe a -> a
fromMaybe Nat
forall a. HasCallStack => a
__IMPOSSIBLE__ (a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView a
x)]
                             VarP{} -> []
                             ProjP{}-> []
                             LitP{} -> []
                             DotP{} -> []
                             DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps -> [NamedArg (Pattern' a)] -> [Nat]
forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [Nat]
iApplyVars [NamedArg (Pattern' a)]
ps
                             ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps -> [NamedArg (Pattern' a)] -> [Nat]
forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [Nat]
iApplyVars [NamedArg (Pattern' a)]
ps

isInterval :: (MonadTCM m, MonadReduce m) => Type -> m Bool
isInterval :: 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