{-# 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.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 @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 <- forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getTerm' ArgName
builtinPathP
  Term
io <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
  let
    argN :: e -> Arg e
argN = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo
    argH :: e -> Arg e
argH = forall e. ArgInfo -> e -> Arg e
Arg forall a b. (a -> b) -> a -> b
$ 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 <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return Level
l
        Abs ArgName
n (Type Level
l) | Bool -> Bool
not (forall a. Free a => Int -> a -> Bool
freeIn Int
0 Abs Sort
s) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Impossible -> Abs a -> a
noabsApp forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. ArgName -> a -> Abs a
Abs ArgName
n Level
l)
        Abs Sort
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> TypeError
GenericError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
             (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"The type is non-fibrant or its sort depends on an interval variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (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          = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Type
t
    telePiPath (Int
x:[Int]
xs) (ExtendTel Dom Type
a Abs Telescope
tel)
      = case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (\ (Term
t,(Term, Term)
_) -> Term
t 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe Term
mpp
            let names :: [Arg ArgName]
names = Telescope -> [Arg ArgName]
teleArgNames forall a b. (a -> b) -> a -> b
$ 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
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Type Level
l) forall a b. (a -> b) -> a -> b
$
              Term
pp forall t. Apply t => t -> Args -> t
`apply` [ forall {e}. e -> Arg e
argH (Level -> Term
Level Level
l)
                         , forall {e}. e -> Arg e
argN (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b))
                         , forall {e}. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ [Arg ArgName] -> Term -> Term
lams [Arg ArgName]
names (forall a b. (a, b) -> a
fst (Term, Term)
u)
                         , forall {e}. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ [Arg ArgName] -> Term -> Term
lams [Arg ArgName]
names (forall a b. (a, b) -> b
snd (Term, Term)
u)
                         ]
          Maybe (Term, (Term, Term))
Nothing    -> do
            Abs Type
b <- TCMT IO (Abs Type)
b
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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  = 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 = forall a. HasCallStack => a
__IMPOSSIBLE__
    telePiPath []    Telescope
_        = forall a. HasCallStack => a
__IMPOSSIBLE__
  [Int] -> Telescope -> TCM Type
telePiPath (forall a. Integral a => a -> [a]
downFrom (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
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Int
40                  forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"tel  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Int
40 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.tel.path" Int
40 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"bndry" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 forall a. a -> a
id 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 = forall a. Impossible -> Int -> Substitution' a
strengthenS HasCallStack => Impossible
impossible Int
1 forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`
     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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
  forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (Dom Type
_, Abs Type
u) -> (forall a. Num a => a -> a -> a
+Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Int
arityPiPath (forall a. Abs a -> a
unAbs Abs Type
u)
    Right Type
_     -> 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 -> [ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Maybe Int
deBruijnView a
x ]
    VarP{}          -> []
    ProjP{}         -> []
    LitP{}          -> []
    DotP{}          -> []
    DefP PatternInfo
_ QName
_ [NamedArg (Pattern' a)]
ps     -> forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg (Pattern' a)]
ps
    ConP ConHead
_ ConPatternInfo
_ [NamedArg (Pattern' a)]
ps     -> forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg (Pattern' a)]
ps

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

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

-- | 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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getName' ArgName
builtinInterval) (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) forall a b. (a -> b) -> a -> b
$ \ QName
i -> do
  forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
t) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    Def QName
q [] -> QName
q forall a. Eq a => a -> a -> Bool
== QName
i
    Term
_        -> Bool
False