{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Telescope where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Trans.Maybe (MaybeT)

import Data.Foldable
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
-- import Data.Monoid

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty ( Pretty )
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern ( patternToTerm )

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

import Agda.Utils.CallStack ( withCallerCallStack )
import Agda.Utils.Either
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible

-- | Flatten telescope: @(Γ : Tel) -> [Type Γ]@.
--
-- 'flattenTel' is lazy in both the spine and values of
-- the resulting list.
flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel :: forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom a)
tel = Int -> Tele (Dom a) -> [Dom a]
forall {a}. Subst a => Int -> Tele a -> [a]
loop (Tele (Dom a) -> Int
forall a. Sized a => a -> Int
size Tele (Dom a)
tel) Tele (Dom a)
tel
  where
    loop :: Int -> Tele a -> [a]
loop Int
ix Tele a
EmptyTel = []
    loop Int
ix (ExtendTel a
a (Abs ArgName
_ Tele a
tel)) = Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
ix a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> Tele a -> [a]
loop (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Tele a
tel
    loop Int
ix (ExtendTel a
a (NoAbs ArgName
_ Tele a
tel)) = Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
ix a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> Tele a -> [a]
loop Int
ix Tele a
tel
{-# SPECIALIZE flattenTel :: Telescope -> [Dom Type] #-}

-- | Flatten telescope: @(Γ : Tel) -> [Type Γ]@ into a reversed list.
--
-- 'flattenRevTel' is lazy in both the spine and values of
-- the resulting list.
flattenRevTel :: TermSubst a => Tele (Dom a) -> [Dom a]
flattenRevTel :: forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenRevTel Tele (Dom a)
tel = Int -> [Dom a] -> Tele (Dom a) -> [Dom a]
forall {a}. Subst a => Int -> [a] -> Tele a -> [a]
loop (Tele (Dom a) -> Int
forall a. Sized a => a -> Int
size Tele (Dom a)
tel) [] Tele (Dom a)
tel
  where
    loop :: Int -> [a] -> Tele a -> [a]
loop Int
ix [a]
acc Tele a
EmptyTel = [a]
acc
    loop Int
ix [a]
acc (ExtendTel a
a (Abs ArgName
_ Tele a
tel)) = Int -> [a] -> Tele a -> [a]
loop (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
ix a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc) Tele a
tel
    loop Int
ix [a]
acc (ExtendTel a
a (NoAbs ArgName
_ Tele a
tel)) = Int -> [a] -> Tele a -> [a]
loop Int
ix (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
ix a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc) Tele a
tel
{-# SPECIALIZE flattenRevTel :: Telescope -> [Dom Type] #-}

-- | Turn a context into a flat telescope: all entries live in the whole context.
-- @
--    (Γ : Context) -> [Type Γ]
-- @
flattenContext :: Context -> [ContextEntry]
flattenContext :: Context -> [ContextEntry]
flattenContext = Int -> [ContextEntry] -> [ContextEntry] -> [ContextEntry]
forall {a}. Subst a => Int -> [a] -> [a] -> [a]
loop Int
1 [] ([ContextEntry] -> [ContextEntry])
-> (Context -> [ContextEntry]) -> Context -> [ContextEntry]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [ContextEntry]
forall a. Context' a -> [a]
cxEntries
  where
    loop :: Int -> [a] -> [a] -> [a]
loop Int
n [a]
tel []       = [a]
tel
    loop Int
n [a]
tel (a
ce:[a]
ctx) = Int -> [a] -> [a] -> [a]
loop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
n a
ce a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
tel) [a]
ctx

-- | Order a flattened telescope in the correct dependency order: Γ ->
--   Permutation (Γ -> Γ~)
--
--   Since @reorderTel tel@ uses free variable analysis of type in @tel@,
--   the telescope should be 'normalise'd.
reorderTel :: [Dom Type] -> Maybe Permutation
reorderTel :: [Dom (Type'' Term Term)] -> Maybe Permutation
reorderTel [Dom (Type'' Term Term)]
tel = ((Int, Dom (Type'' Term Term))
 -> (Int, Dom (Type'' Term Term)) -> Bool)
-> [(Int, Dom (Type'' Term Term))] -> Maybe Permutation
forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (Int, Dom (Type'' Term Term))
-> (Int, Dom (Type'' Term Term)) -> Bool
forall {t} {b} {a} {t} {t}.
Free t =>
(Int, b) -> (a, Dom' t (Type'' t t)) -> Bool
comesBefore [(Int, Dom (Type'' Term Term))]
tel'
  where
    tel' :: [(Int, Dom (Type'' Term Term))]
tel' = [Int]
-> [Dom (Type'' Term Term)] -> [(Int, Dom (Type'' Term Term))]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [Dom (Type'' Term Term)] -> Int
forall a. Sized a => a -> Int
size [Dom (Type'' Term Term)]
tel) [Dom (Type'' Term Term)]
tel
    (Int
i, b
_) comesBefore :: (Int, b) -> (a, Dom' t (Type'' t t)) -> Bool
`comesBefore` (a
_, Dom' t (Type'' t t)
a) = Int
i Int -> t -> Bool
forall t. Free t => Int -> t -> Bool
`freeIn` Type'' t t -> t
forall t a. Type'' t a -> a
unEl (Dom' t (Type'' t t) -> Type'' t t
forall t e. Dom' t e -> e
unDom Dom' t (Type'' t t)
a) -- a tiny bit unsafe

reorderTel_ :: [Dom Type] -> Permutation
reorderTel_ :: [Dom (Type'' Term Term)] -> Permutation
reorderTel_ [Dom (Type'' Term Term)]
tel = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Dom (Type'' Term Term)] -> Maybe Permutation
reorderTel [Dom (Type'' Term Term)]
tel)

-- | Unflatten: turns a flattened telescope into a proper telescope. Must be
--   properly ordered.
unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
unflattenTel :: [ArgName]
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
unflattenTel [ArgName]
xs [Dom (Type'' Term Term)]
tel = Int
-> [ArgName]
-> [Dom (Type'' Term Term)]
-> Tele (Dom (Type'' Term Term))
unflattenTel' ([Dom (Type'' Term Term)] -> Int
forall a. Sized a => a -> Int
size [Dom (Type'' Term Term)]
tel) [ArgName]
xs [Dom (Type'' Term Term)]
tel

-- | A variant of 'unflattenTel' which takes the size of the last
-- argument as an argument.
unflattenTel' :: Int -> [ArgName] -> [Dom Type] -> Telescope
unflattenTel' :: Int
-> [ArgName]
-> [Dom (Type'' Term Term)]
-> Tele (Dom (Type'' Term Term))
unflattenTel' !Int
n [ArgName]
xs [Dom (Type'' Term Term)]
tel = case ([ArgName]
xs, [Dom (Type'' Term Term)]
tel) of
  ([],     [])      -> Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel
  (ArgName
x : [ArgName]
xs, Dom (Type'' Term Term)
a : [Dom (Type'' Term Term)]
tel) -> Dom (Type'' Term Term)
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom (Type'' Term Term)
a' (ArgName
-> Tele (Dom (Type'' Term Term))
-> Abs (Tele (Dom (Type'' Term Term)))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom (Type'' Term Term))
tel')
    where
    tel' :: Tele (Dom (Type'' Term Term))
tel' = Int
-> [ArgName]
-> [Dom (Type'' Term Term)]
-> Tele (Dom (Type'' Term Term))
unflattenTel' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [ArgName]
xs [Dom (Type'' Term Term)]
tel
    a' :: Dom (Type'' Term Term)
a'   = Substitution' (SubstArg (Dom (Type'' Term Term)))
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Dom (Type'' Term Term)))
rho Dom (Type'' Term Term)
a
    rho :: Substitution' Term
rho  = Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS ((CallStack -> Impossible) -> Impossible
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible) Int
n
  ([],    Dom (Type'' Term Term)
_ : [Dom (Type'' Term Term)]
_) -> Tele (Dom (Type'' Term Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
  (ArgName
_ : [ArgName]
_, [])    -> Tele (Dom (Type'' Term Term))
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Rename the variables in the telescope to the given names
--   Precondition: @size xs == size tel@.
renameTel :: [Maybe ArgName] -> Telescope -> Telescope
renameTel :: [Maybe ArgName]
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
renameTel []           Tele (Dom (Type'' Term Term))
EmptyTel           = Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel
renameTel (Maybe ArgName
Nothing:[Maybe ArgName]
xs) (ExtendTel Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel') = Dom (Type'' Term Term)
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom (Type'' Term Term)
a (Abs (Tele (Dom (Type'' Term Term)))
 -> Tele (Dom (Type'' Term Term)))
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName]
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
renameTel [Maybe ArgName]
xs (Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term)))
-> Abs (Tele (Dom (Type'' Term Term)))
-> Abs (Tele (Dom (Type'' Term Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom (Type'' Term Term)))
tel'
renameTel (Just ArgName
x :[Maybe ArgName]
xs) (ExtendTel Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel') = Dom (Type'' Term Term)
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom (Type'' Term Term)
a (Abs (Tele (Dom (Type'' Term Term)))
 -> Tele (Dom (Type'' Term Term)))
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName]
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
renameTel [Maybe ArgName]
xs (Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term)))
-> Abs (Tele (Dom (Type'' Term Term)))
-> Abs (Tele (Dom (Type'' Term Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Abs (Tele (Dom (Type'' Term Term)))
tel' { absName = x })
renameTel []           (ExtendTel Dom (Type'' Term Term)
_ Abs (Tele (Dom (Type'' Term Term)))
_   ) = Tele (Dom (Type'' Term Term))
forall a. HasCallStack => a
__IMPOSSIBLE__
renameTel (Maybe ArgName
_      :[Maybe ArgName]
_ ) Tele (Dom (Type'' Term Term))
EmptyTel           = Tele (Dom (Type'' Term Term))
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Get the suggested names from a telescope
teleNames :: Telescope -> [ArgName]
teleNames :: Tele (Dom (Type'' Term Term)) -> [ArgName]
teleNames = (Dom (ArgName, Type'' Term Term) -> ArgName)
-> [Dom (ArgName, Type'' Term Term)] -> [ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' ((ArgName, Type'' Term Term) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type'' Term Term) -> ArgName)
-> (Dom (ArgName, Type'' Term Term) -> (ArgName, Type'' Term Term))
-> Dom (ArgName, Type'' Term Term)
-> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type'' Term Term) -> (ArgName, Type'' Term Term)
forall t e. Dom' t e -> e
unDom) ([Dom (ArgName, Type'' Term Term)] -> [ArgName])
-> (Tele (Dom (Type'' Term Term))
    -> [Dom (ArgName, Type'' Term Term)])
-> Tele (Dom (Type'' Term Term))
-> [ArgName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom (Type'' Term Term)) -> [Dom (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList

teleArgNames :: Telescope -> [Arg ArgName]
teleArgNames :: Tele (Dom (Type'' Term Term)) -> [Arg ArgName]
teleArgNames = Tele (Dom (Type'' Term Term)) -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs

-- | Convert a telescope to a list of 'Arg' in left-to-right order:
--
--   @teleArgs ((a : A) (b : B a) {c : C}) = [a, b, {c}] = [2, 1, {0}]@
teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
teleArgs :: forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs = (Dom' Term a -> Arg a) -> [Dom' Term a] -> [Arg a]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term a -> Arg a
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term a] -> [Arg a])
-> (Tele (Dom t) -> [Dom' Term a]) -> Tele (Dom t) -> [Arg a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom t) -> [Dom' Term a]
forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
teleDoms

-- | Convert a telescope to a list of 'Dom' in left-to-right order:
--
--   @teleDoms ((a : A) (b : B a) {c : C}) = [a, b, {c}] = [2, 1, {0}]@
teleDoms :: (DeBruijn a) => Tele (Dom t) -> [Dom a]
teleDoms :: forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
teleDoms Tele (Dom t)
tel = (Int -> Dom (ArgName, t) -> Dom a)
-> [Int] -> [Dom (ArgName, t)] -> [Dom a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Dom (ArgName, t)
dom -> Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar Int
i a -> Dom (ArgName, t) -> Dom a
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (ArgName, t)
dom) (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [Dom (ArgName, t)] -> Int
forall a. Sized a => a -> Int
size [Dom (ArgName, t)]
l) [Dom (ArgName, t)]
l
  where l :: [Dom (ArgName, t)]
l = Tele (Dom t) -> [Dom (ArgName, t)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
tel

-- UNUSED
-- withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]
-- xs `withNamedArgsFromTel` tel =
--   [ Arg info (Named (Just $ Ranged empty $ argNameToString name) x)
--   | (x, Dom {domInfo = info, unDom = (name,_)}) <- zip xs l ]
--   where l = telToList tel

teleNamedArgs :: (DeBruijn a) => Tele (Dom t) -> [NamedArg a]
teleNamedArgs :: forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs = (Dom' Term a -> NamedArg a) -> [Dom' Term a] -> [NamedArg a]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term a -> NamedArg a
forall t a. Dom' t a -> NamedArg a
namedArgFromDom ([Dom' Term a] -> [NamedArg a])
-> (Tele (Dom t) -> [Dom' Term a]) -> Tele (Dom t) -> [NamedArg a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom t) -> [Dom' Term a]
forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
teleDoms

{-# INLINABLE tele2NamedArgs #-}
-- | A variant of `teleNamedArgs` which takes the argument names (and the argument info)
--   from the first telescope and the variable names from the second telescope.
--
--   Precondition: the two telescopes have the same length.
tele2NamedArgs :: (DeBruijn a) => Telescope -> Telescope -> [NamedArg a]
tele2NamedArgs :: forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term)) -> [NamedArg a]
tele2NamedArgs Tele (Dom (Type'' Term Term))
tel0 Tele (Dom (Type'' Term Term))
tel =
  [ ArgInfo -> Named_ a -> NamedArg a
forall e. ArgInfo -> e -> Arg e
Arg (Dom (ArgName, Type'' Term Term)
d1 Dom (ArgName, Type'' Term Term)
-> Getting ArgInfo (Dom (ArgName, Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom (ArgName, Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) (Maybe NamedName -> a -> Named_ a
forall name a. Maybe name -> a -> Named name a
Named (NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged ArgName -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
forall a b. (a -> b) -> a -> b
$ ArgName -> Ranged ArgName
forall a. a -> Ranged a
unranged (ArgName -> Ranged ArgName) -> ArgName -> Ranged ArgName
forall a b. (a -> b) -> a -> b
$ ArgName -> ArgName
argNameToString ((ArgName, Type'' Term Term) -> ArgName
forall a b. (a, b) -> a
fst (Dom (ArgName, Type'' Term Term) -> (ArgName, Type'' Term Term)
forall t e. Dom' t e -> e
unDom Dom (ArgName, Type'' Term Term)
d1)))
                             (ArgName -> Int -> a
forall a. DeBruijn a => ArgName -> Int -> a
deBruijnNamedVar ((ArgName, Type'' Term Term) -> ArgName
forall a b. (a, b) -> a
fst (Dom (ArgName, Type'' Term Term) -> (ArgName, Type'' Term Term)
forall t e. Dom' t e -> e
unDom Dom (ArgName, Type'' Term Term)
d2)) Int
i))
  | (Int
i, Dom (ArgName, Type'' Term Term)
d1, Dom (ArgName, Type'' Term Term)
d2) <- [Int]
-> [Dom (ArgName, Type'' Term Term)]
-> [Dom (ArgName, Type'' Term Term)]
-> [(Int, Dom (ArgName, Type'' Term Term),
     Dom (ArgName, Type'' Term Term))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [Dom (ArgName, Type'' Term Term)] -> Int
forall a. Sized a => a -> Int
size [Dom (ArgName, Type'' Term Term)]
l) [Dom (ArgName, Type'' Term Term)]
l0 [Dom (ArgName, Type'' Term Term)]
l ]
  where
  l :: [Dom (ArgName, Type'' Term Term)]
l  = Tele (Dom (Type'' Term Term)) -> [Dom (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom (Type'' Term Term))
tel
  l0 :: [Dom (ArgName, Type'' Term Term)]
l0 = Tele (Dom (Type'' Term Term)) -> [Dom (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom (Type'' Term Term))
tel0

-- | Split the telescope at the specified position.
splitTelescopeAt :: Int -> Telescope -> (Telescope,Telescope)
splitTelescopeAt :: Int
-> Tele (Dom (Type'' Term Term))
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
splitTelescopeAt Int
n Tele (Dom (Type'' Term Term))
tel
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0    = (Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel, Tele (Dom (Type'' Term Term))
tel)
  | Bool
otherwise = Int
-> Tele (Dom (Type'' Term Term))
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
splitTelescopeAt' Int
n Tele (Dom (Type'' Term Term))
tel
    where
      splitTelescopeAt' :: Int
-> Tele (Dom (Type'' Term Term))
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
splitTelescopeAt' Int
_ Tele (Dom (Type'' Term Term))
EmptyTel          = (Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel,Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel)
      splitTelescopeAt' Int
1 (ExtendTel Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel) = (Dom (Type'' Term Term)
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom (Type'' Term Term)
a (Abs (Tele (Dom (Type'' Term Term)))
tel Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
-> Abs (Tele (Dom (Type'' Term Term)))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel), Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom (Type'' Term Term)))
tel)
      splitTelescopeAt' Int
m (ExtendTel Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel) = (Dom (Type'' Term Term)
-> Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom (Type'' Term Term)
a (Abs (Tele (Dom (Type'' Term Term)))
tel Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
-> Abs (Tele (Dom (Type'' Term Term)))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Tele (Dom (Type'' Term Term))
tel'), Tele (Dom (Type'' Term Term))
tel'')
        where
          (Tele (Dom (Type'' Term Term))
tel', Tele (Dom (Type'' Term Term))
tel'') = Int
-> Tele (Dom (Type'' Term Term))
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
splitTelescopeAt (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Tele (Dom (Type'' Term Term))
 -> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term))))
-> Tele (Dom (Type'' Term Term))
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Abs (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom (Type'' Term Term)))
tel

-- | Permute telescope: permutes or drops the types in the telescope according
--   to the given permutation (on de Bruijn _levels_). Assumes that the permutation preserves the
--   dependencies in the telescope.
--
--   For example (Andreas, 2016-12-18, issue #2344):
--   @
--     tel                        = (A : Set) (X : _18 A) (i : Fin (_m_23 A X))
--     tel (de Bruijn)            = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0)
--     flattenTel tel             = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0) |- [ Set, _18 @2, Fin (_m_23 @2 @1) ]
--     perm                       = 0,1,2 -> 0,1  (picks the first two)
--     renaming _ perm            = [var 0, var 1, error]  -- THE WRONG RENAMING! (levels)
--     renaming _ (reverseP perm) = [error, var 0, var 1]  -- The correct renaming! (indices)
--     apply to flattened tel     = ... |- [ Set, _18 @1, Fin (_m_23 @1 @0) ]
--     permute perm it            = ... |- [ Set, _18 @1 ]
--     unflatten (de Bruijn)      = 1:Set, 0: _18 @0
--     unflatten                  = (A : Set) (X : _18 A)
--   @
permuteTel :: Permutation -> Telescope -> Telescope
permuteTel :: Permutation
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
permuteTel Permutation
perm Tele (Dom (Type'' Term Term))
tel =
  let names :: [ArgName]
names = Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm ([ArgName] -> [ArgName]) -> [ArgName] -> [ArgName]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [ArgName]
teleNames Tele (Dom (Type'' Term Term))
tel
      types :: [Dom (Type'' Term Term)]
types = Permutation -> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm ([Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)])
-> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a b. (a -> b) -> a -> b
$ Impossible
-> Permutation
-> [Dom (Type'' Term Term)]
-> [Dom (Type'' Term Term)]
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm) ([Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)])
-> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
tel
  in  [ArgName]
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
unflattenTel [ArgName]
names [Dom (Type'' Term Term)]
types

-- | Like 'permuteTel', but start with a context.
--
permuteContext :: Permutation -> Context -> Telescope
permuteContext :: Permutation -> Context -> Tele (Dom (Type'' Term Term))
permuteContext Permutation
perm Context
ctx = Permutation
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
permuteTel Permutation
perm (Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Context -> Tele (Dom (Type'' Term Term))
contextToTel Context
ctx

-- | Recursively computes dependencies of a set of variables in a given
--   telescope. Any dependencies outside of the telescope are ignored.
--
--   Note that 'varDependencies' considers a variable to depend on itself.
varDependencies :: Telescope -> VarSet -> VarSet
varDependencies :: Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
varDependencies Tele (Dom (Type'' Term Term))
tel = VarSet -> VarSet
addLocks (VarSet -> VarSet) -> (VarSet -> VarSet) -> VarSet -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
allDependencies Tele (Dom (Type'' Term Term))
tel
  where
    addLocks :: VarSet -> VarSet
    addLocks :: VarSet -> VarSet
addLocks VarSet
s =
      case VarSet -> Maybe Int
VarSet.lookupMin VarSet
s of
        Just Int
m ->
          let locks :: [Int]
locks = [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [ Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) | (Arg Term
a :: Arg Term) <- Tele (Dom (Type'' Term Term)) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom (Type'' Term Term))
tel, IsLock{} <- Lock -> [Lock]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Arg Term -> Lock
forall a. LensLock a => a -> Lock
getLock Arg Term
a)]
          -- 'teleArgs' returns indices in descending order, so both the
          -- 'takeWhile' and 'insertsDesc' are safe.
          in [Int] -> VarSet -> VarSet
VarSet.insertsDesc ((Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m) [Int]
locks) VarSet
s
        Maybe Int
Nothing ->
          VarSet
s

    allDependencies :: Telescope -> VarSet -> VarSet
    allDependencies :: Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
allDependencies Tele (Dom (Type'' Term Term))
tel VarSet
vs = VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop VarSet
forall a. Null a => a
empty (Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenRevTel Tele (Dom (Type'' Term Term))
tel) (-Int
1) VarSet
vs
      where
        -- Idea here is to keep a set @work@ of variables that we still need
        -- to get deps of. At each iteration, we skip backwards through the telescope
        -- and add its direct dependencies to the work set. This only checks dependencies
        -- of each variable once, as telescope elements can't depend on things later in the telescope.
        loop :: VarSet -> [Dom Type] -> Int -> VarSet -> VarSet
        loop :: VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop !VarSet
deps [Dom (Type'' Term Term)]
telRev Int
prevIx VarSet
work =
          case VarSet -> Maybe (Int, VarSet)
VarSet.minView VarSet
work of
            Maybe (Int, VarSet)
Nothing -> VarSet
deps
            Just (Int
ix, VarSet
work) ->
              case Int -> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. Int -> [a] -> [a]
drop (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
prevIx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Dom (Type'' Term Term)]
telRev of
                [] ->
                  -- Ignore all deps outside the telescope
                  VarSet
deps
                (Dom (Type'' Term Term)
ti:[Dom (Type'' Term Term)]
telRev) ->
                  VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop (Int -> VarSet -> VarSet
VarSet.insert Int
ix VarSet
deps) [Dom (Type'' Term Term)]
telRev Int
ix (VarSet -> VarSet -> VarSet
VarSet.union (Dom (Type'' Term Term) -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Dom (Type'' Term Term)
ti) VarSet
work)



-- | Computes the set of variables in a telescope whose type depend on
--   one of the variables in the given set (including recursive
--   dependencies). Any dependencies outside of the telescope are
--   ignored.
--
--   Unlike 'varDependencies', a variable is *not* considered to depend on itself.
varDependents :: Telescope -> VarSet -> VarSet
varDependents :: Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
varDependents Tele (Dom (Type'' Term Term))
tel VarSet
vs =
  VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop VarSet
forall a. Null a => a
empty (Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
tel) (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) VarSet
vs
  where
    -- Idea here is to keep a set @work@ of variables that we
    -- want to find dependents of. At each iteration, we walk forwards through
    -- the telescope and check if the each telescope contains any of the
    -- variables in the work set. If it does, we add that variable to the work
    -- and dependents set.
    loop :: VarSet -> [Dom Type] -> Int -> VarSet -> VarSet
    loop :: VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop !VarSet
deps [Dom (Type'' Term Term)]
tel Int
ix VarSet
work =
      case [Dom (Type'' Term Term)]
tel of
        [] -> VarSet
deps
        (Dom (Type'' Term Term)
ti:[Dom (Type'' Term Term)]
tel) ->
          if (Int -> Bool) -> Dom (Type'' Term Term) -> Bool
forall t. Free t => (Int -> Bool) -> t -> Bool
anyFreeVar (Int -> VarSet -> Bool
`VarSet.member` VarSet
work) Dom (Type'' Term Term)
ti then
            VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop (Int -> VarSet -> VarSet
VarSet.insert Int
ix VarSet
deps) [Dom (Type'' Term Term)]
tel (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> VarSet -> VarSet
VarSet.insert Int
ix VarSet
work)
          else
            VarSet -> [Dom (Type'' Term Term)] -> Int -> VarSet -> VarSet
loop VarSet
deps [Dom (Type'' Term Term)]
tel (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) VarSet
work

-- | A telescope split in two.
data SplitTel = SplitTel
  { SplitTel -> Tele (Dom (Type'' Term Term))
firstPart  :: Telescope
  , SplitTel -> Tele (Dom (Type'' Term Term))
secondPart :: Telescope
  , SplitTel -> Permutation
splitPerm  :: Permutation
    -- ^ The permutation (of de Bruijn _levels_) that takes us from the original telescope to
    --   @firstPart ++ secondPart@.
  }

-- | Split a telescope into the part that defines the given variables and the
--   part that doesn't.
--
--   See 'Agda.TypeChecking.Tests.prop_splitTelescope'.
splitTelescope
  :: VarSet     -- ^ A set of de Bruijn indices.
  -> Telescope  -- ^ Original telescope.
  -> SplitTel   -- ^ @firstPart@ mentions the given variables, @secondPart@ not.
splitTelescope :: VarSet -> Tele (Dom (Type'' Term Term)) -> SplitTel
splitTelescope VarSet
fv Tele (Dom (Type'' Term Term))
tel = Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term)) -> Permutation -> SplitTel
SplitTel Tele (Dom (Type'' Term Term))
tel1 Tele (Dom (Type'' Term Term))
tel2 Permutation
perm
  where
    names :: [ArgName]
names = Tele (Dom (Type'' Term Term)) -> [ArgName]
teleNames Tele (Dom (Type'' Term Term))
tel
    ts0 :: [Dom (Type'' Term Term)]
ts0   = Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
tel
    n :: Int
n     = Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
tel

    is :: VarSet
is    = Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
varDependencies Tele (Dom (Type'' Term Term))
tel VarSet
fv
    isC :: VarSet
isC   = Int -> VarSet -> VarSet
VarSet.complement Int
n VarSet
is

    perm :: Permutation
perm  = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$! (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$! VarSet -> [Int]
VarSet.toDescList VarSet
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++! VarSet -> [Int]
VarSet.toDescList VarSet
isC

    ts1 :: [Dom (Type'' Term Term)]
ts1   = Impossible
-> Permutation
-> [Dom (Type'' Term Term)]
-> [Dom (Type'' Term Term)]
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm) (Permutation -> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [Dom (Type'' Term Term)]
ts0)

    tel' :: Tele (Dom (Type'' Term Term))
tel'  = [ArgName]
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
unflattenTel (Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [ArgName]
names) [Dom (Type'' Term Term)]
ts1

    m :: Int
m     = VarSet -> Int
VarSet.size VarSet
is
    (Tele (Dom (Type'' Term Term))
tel1, Tele (Dom (Type'' Term Term))
tel2) = [Dom (ArgName, Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList ([Dom (ArgName, Type'' Term Term)]
 -> Tele (Dom (Type'' Term Term)))
-> ([Dom (ArgName, Type'' Term Term)]
    -> Tele (Dom (Type'' Term Term)))
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [Dom (ArgName, Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList (([Dom (ArgName, Type'' Term Term)],
  [Dom (ArgName, Type'' Term Term)])
 -> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term))))
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Int
-> [Dom (ArgName, Type'' Term Term)]
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
m ([Dom (ArgName, Type'' Term Term)]
 -> ([Dom (ArgName, Type'' Term Term)],
     [Dom (ArgName, Type'' Term Term)]))
-> [Dom (ArgName, Type'' Term Term)]
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom (Type'' Term Term))
tel'

-- | As splitTelescope, but fails if any additional variables or reordering
--   would be needed to make the first part well-typed.
splitTelescopeExact
  :: [Int]          -- ^ A list of de Bruijn indices
  -> Telescope      -- ^ The telescope to split
  -> Maybe SplitTel -- ^ @firstPart@ mentions the given variables in the given order,
                    --   @secondPart@ contains all other variables
splitTelescopeExact :: [Int] -> Tele (Dom (Type'' Term Term)) -> Maybe SplitTel
splitTelescopeExact [Int]
is Tele (Dom (Type'' Term Term))
tel = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok Maybe () -> SplitTel -> Maybe SplitTel
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term)) -> Permutation -> SplitTel
SplitTel Tele (Dom (Type'' Term Term))
tel1 Tele (Dom (Type'' Term Term))
tel2 Permutation
perm
  where
    names :: [ArgName]
names = Tele (Dom (Type'' Term Term)) -> [ArgName]
teleNames Tele (Dom (Type'' Term Term))
tel
    ts0 :: [Dom (Type'' Term Term)]
ts0   = Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
tel
    n :: Int
n     = Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
tel

    checkDependencies :: IntSet -> [Int] -> Bool
    checkDependencies :: IntSet -> [Int] -> Bool
checkDependencies IntSet
soFar []     = Bool
True
    checkDependencies IntSet
soFar (Int
j:[Int]
js) = Bool
ok Bool -> Bool -> Bool
&& IntSet -> [Int] -> Bool
checkDependencies (Int -> IntSet -> IntSet
IntSet.insert Int
j IntSet
soFar) [Int]
js
      where
        t :: Dom (Type'' Term Term)
t = Dom (Type'' Term Term)
-> [Dom (Type'' Term Term)] -> Int -> Dom (Type'' Term Term)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom (Type'' Term Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom (Type'' Term Term)]
ts0 (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j)  -- ts0[n-1-j]
        good :: Int -> Bool
good Int
i = (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) Bool -> Bool -> Bool
`implies` (Int
i Int -> IntSet -> Bool
`IntSet.member` IntSet
soFar) where implies :: Bool -> Bool -> Bool
implies = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
        ok :: Bool
ok = (Int -> Bool) -> Dom (Type'' Term Term) -> Bool
forall t. Free t => (Int -> Bool) -> t -> Bool
allFreeVar Int -> Bool
good Dom (Type'' Term Term)
t

    ok :: Bool
ok    = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) [Int]
is Bool -> Bool -> Bool
&& IntSet -> [Int] -> Bool
checkDependencies IntSet
IntSet.empty [Int]
is

    isC :: [Int]
isC   = Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Int]
is

    perm :: Permutation
perm  = Int -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int]
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++! [Int]
isC

    ts1 :: [Dom (Type'' Term Term)]
ts1   = Impossible
-> Permutation
-> [Dom (Type'' Term Term)]
-> [Dom (Type'' Term Term)]
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm) (Permutation -> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [Dom (Type'' Term Term)]
ts0)

    tel' :: Tele (Dom (Type'' Term Term))
tel'  = [ArgName]
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
unflattenTel (Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [ArgName]
names) [Dom (Type'' Term Term)]
ts1

    m :: Int
m     = [Int] -> Int
forall a. Sized a => a -> Int
size [Int]
is
    (Tele (Dom (Type'' Term Term))
tel1, Tele (Dom (Type'' Term Term))
tel2) = [Dom (ArgName, Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList ([Dom (ArgName, Type'' Term Term)]
 -> Tele (Dom (Type'' Term Term)))
-> ([Dom (ArgName, Type'' Term Term)]
    -> Tele (Dom (Type'' Term Term)))
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [Dom (ArgName, Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList (([Dom (ArgName, Type'' Term Term)],
  [Dom (ArgName, Type'' Term Term)])
 -> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term))))
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
-> (Tele (Dom (Type'' Term Term)), Tele (Dom (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Int
-> [Dom (ArgName, Type'' Term Term)]
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
m ([Dom (ArgName, Type'' Term Term)]
 -> ([Dom (ArgName, Type'' Term Term)],
     [Dom (ArgName, Type'' Term Term)]))
-> [Dom (ArgName, Type'' Term Term)]
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom (Type'' Term Term))
tel'

-- | Try to instantiate one variable in the telescope (given by its de Bruijn
--   level) with the given value, returning the new telescope and a
--   substitution to the old one. Returns Nothing if the given value depends
--   (directly or indirectly) on the variable.
instantiateTelescope
  :: Telescope -- ^ ⊢ Γ
  -> Int       -- ^ Γ ⊢ var k : A   de Bruijn _level_
  -> DeBruijnPattern -- ^ Γ ⊢ u : A
  -> Maybe (Telescope,           -- ⊢ Γ'
            PatternSubstitution, -- Γ' ⊢ σ : Γ
            Permutation)         -- reordering of Γ applied before instantiating
                                 -- (works on de Bruijn _levels_)
instantiateTelescope :: Tele (Dom (Type'' Term Term))
-> Int
-> Pattern' DBPatVar
-> Maybe
     (Tele (Dom (Type'' Term Term)), PatternSubstitution, Permutation)
instantiateTelescope Tele (Dom (Type'' Term Term))
tel Int
k Pattern' DBPatVar
p = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok Maybe ()
-> (Tele (Dom (Type'' Term Term)), PatternSubstitution,
    Permutation)
-> Maybe
     (Tele (Dom (Type'' Term Term)), PatternSubstitution, Permutation)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (Tele (Dom (Type'' Term Term))
tel', PatternSubstitution
sigma, Permutation -> Permutation
reverseP Permutation
perm)
  where
    names :: [ArgName]
names = Tele (Dom (Type'' Term Term)) -> [ArgName]
teleNames Tele (Dom (Type'' Term Term))
tel
    ts0 :: [Dom (Type'' Term Term)]
ts0   = Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
tel
    n :: Int
n     = Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
tel
    j :: Int
j     = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
k -- de Bruijn index
    u :: Term
u     = Pattern' DBPatVar -> Term
patternToTerm Pattern' DBPatVar
p

    -- Jesper, 2019-12-31: Previous implementation that does some
    -- unneccessary reordering but is otherwise correct (keep!)
    -- -- is0 is the part of Γ that is needed to type u
    -- is0   = varDependencies tel $ freeVarSet u
    -- -- is1 is the rest of Γ (minus the variable we are instantiating)
    -- is1   = IntSet.delete j $
    --           IntSet.fromAscList [ 0 .. n-1 ] `IntSet.difference` is0
    -- -- we work on de Bruijn indices, so later parts come first
    -- is    = IntSet.toAscList is1 ++! IntSet.toAscList is0

    -- -- if u depends on var j, we cannot instantiate
    -- ok    = not $ j `IntSet.member` is0

    -- is0 is the part of Γ that is needed to type u
    is0 :: VarSet
is0   = Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
varDependencies Tele (Dom (Type'' Term Term))
tel (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Term
u
    -- is1 is the part of Γ that depends on variable j
    is1 :: VarSet
is1   = Tele (Dom (Type'' Term Term)) -> VarSet -> VarSet
varDependents Tele (Dom (Type'' Term Term))
tel (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
j
    -- lasti is the last (rightmost) variable of is0
    lasti :: Int
lasti = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
n (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ VarSet -> Maybe Int
VarSet.lookupMin VarSet
is0
    -- we move each variable in is1 to the right until it comes after
    -- all variables in is0 (i.e. after lasti)
    ([Int]
as,[Int]
bs) = (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Int -> VarSet -> Bool
`VarSet.member` VarSet
is1) [ Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1 , Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2 .. Int
lasti ]
    is :: [Int]
is    = [Int] -> [Int]
forall a. [a] -> [a]
reverse ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int]
bs [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++! [Int]
as [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++! Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
lasti
    perm :: Permutation
perm  = Int -> [Int] -> Permutation
Perm Int
n [Int]
is -- works on de Bruijn indices

    -- if u depends on var j, we cannot instantiate
    ok :: Bool
ok    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int
j Int -> VarSet -> Bool
`VarSet.member` VarSet
is0

    perm' :: Permutation
perm'  = Int -> Permutation -> Permutation
deleteP Int
j Permutation
perm  -- works on de Bruijn indices
    permL' :: Permutation
permL' = Permutation -> Permutation
reverseP Permutation
perm'  -- works on de Bruijn levels

    j' :: Int
j'    = 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
$ Permutation -> Int -> Maybe Int
lookupRP Permutation
perm Int
j
    p1 :: Pattern' DBPatVar
p1    = Impossible -> Permutation -> Pattern' DBPatVar -> Pattern' DBPatVar
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible Permutation
perm' Pattern' DBPatVar
p -- Γ' ⊢ p1 : A'
    sigma :: PatternSubstitution
sigma = Int -> Pattern' DBPatVar -> PatternSubstitution
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
j' Pattern' DBPatVar
p1 PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Impossible -> Permutation -> PatternSubstitution
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible Permutation
perm -- Γ' ⊢ σ : Г

    ts1 :: [Dom (Type'' Term Term)]
ts1   = Permutation -> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. Permutation -> [a] -> [a]
permute Permutation
permL' ([Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)])
-> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a b. (a -> b) -> a -> b
$ PatternSubstitution
-> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma [Dom (Type'' Term Term)]
ts0
    tel' :: Tele (Dom (Type'' Term Term))
tel'  = [ArgName]
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
unflattenTel (Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
permL' [ArgName]
names) [Dom (Type'' Term Term)]
ts1 -- Γ'

-- | Try to eta-expand one variable in the telescope (given by its de Bruijn
--   level)
expandTelescopeVar
  :: Telescope  -- Γ = Γ₁(x : D pars)Γ₂
  -> Int        -- k = size Γ₁
  -> Telescope  -- Γ₁ ⊢ Δ
  -> ConHead    -- Γ₁ ⊢ c : Δ → D pars
  -> ( Telescope            -- Γ' = Γ₁ΔΓ₂[x ↦ c Δ]
     , PatternSubstitution) -- Γ' ⊢ ρ : Γ
expandTelescopeVar :: Tele (Dom (Type'' Term Term))
-> Int
-> Tele (Dom (Type'' Term Term))
-> ConHead
-> (Tele (Dom (Type'' Term Term)), PatternSubstitution)
expandTelescopeVar Tele (Dom (Type'' Term Term))
gamma Int
k Tele (Dom (Type'' Term Term))
delta ConHead
c = (Tele (Dom (Type'' Term Term))
tel', PatternSubstitution
rho)
  where
    ([Dom (ArgName, Type'' Term Term)]
ts1,Dom (ArgName, Type'' Term Term)
xa:[Dom (ArgName, Type'' Term Term)]
ts2) = ([Dom (ArgName, Type'' Term Term)],
 [Dom (ArgName, Type'' Term Term)])
-> Maybe
     ([Dom (ArgName, Type'' Term Term)],
      [Dom (ArgName, Type'' Term Term)])
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
forall a. a -> Maybe a -> a
fromMaybe ([Dom (ArgName, Type'' Term Term)],
 [Dom (ArgName, Type'' Term Term)])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe
   ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
 -> ([Dom (ArgName, Type'' Term Term)],
     [Dom (ArgName, Type'' Term Term)]))
-> Maybe
     ([Dom (ArgName, Type'' Term Term)],
      [Dom (ArgName, Type'' Term Term)])
-> ([Dom (ArgName, Type'' Term Term)],
    [Dom (ArgName, Type'' Term Term)])
forall a b. (a -> b) -> a -> b
$
                    Int
-> [Dom (ArgName, Type'' Term Term)]
-> Maybe
     ([Dom (ArgName, Type'' Term Term)],
      [Dom (ArgName, Type'' Term Term)])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
k ([Dom (ArgName, Type'' Term Term)]
 -> Maybe
      ([Dom (ArgName, Type'' Term Term)],
       [Dom (ArgName, Type'' Term Term)]))
-> [Dom (ArgName, Type'' Term Term)]
-> Maybe
     ([Dom (ArgName, Type'' Term Term)],
      [Dom (ArgName, Type'' Term Term)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom (Type'' Term Term))
gamma
    a :: Dom (Type'' Term Term)
a = Int -> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a. Subst a => Int -> a -> a
raise (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
delta) ((ArgName, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd ((ArgName, Type'' Term Term) -> Type'' Term Term)
-> Dom (ArgName, Type'' Term Term) -> Dom (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (ArgName, Type'' Term Term)
xa) -- Γ₁Δ ⊢ D pars

    cpi :: ConPatternInfo
cpi         = ConPatternInfo
      { conPInfo :: PatternInfo
conPInfo   = PatternInfo
defaultPatternInfo
      , conPRecord :: Bool
conPRecord = Bool
True
      , conPFallThrough :: Bool
conPFallThrough
                   = Bool
False
      , conPType :: Maybe (Arg (Type'' Term Term))
conPType   = Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a. a -> Maybe a
Just (Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term)))
-> Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term) -> Arg (Type'' Term Term)
forall t a. Dom' t a -> Arg a
argFromDom Dom (Type'' Term Term)
a
      , conPLazy :: Bool
conPLazy   = Bool
True
      }
    cargs :: [NamedArg (Pattern' DBPatVar)]
cargs       = (NamedArg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar))
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> [a] -> [b]
map' (Origin
-> NamedArg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom (Type'' Term Term))
delta
    cdelta :: Pattern' DBPatVar
cdelta      = ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi [NamedArg (Pattern' DBPatVar)]
cargs                    -- Γ₁Δ ⊢ c Δ : D pars
    rho0 :: PatternSubstitution
rho0        = Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Pattern' DBPatVar
cdelta (PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution -> PatternSubstitution
forall a b. (a -> b) -> a -> b
$ Int -> PatternSubstitution
forall a. Int -> Substitution' a
raiseS (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
delta)  -- Γ₁Δ ⊢ ρ₀ : Γ₁(x : D pars)
    rho :: PatternSubstitution
rho         = Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS ([Dom (ArgName, Type'' Term Term)] -> Int
forall a. Sized a => a -> Int
size [Dom (ArgName, Type'' Term Term)]
ts2) PatternSubstitution
rho0               -- Γ₁ΔΓ₂ρ₀ ⊢ ρ : Γ₁(x : D pars)Γ₂

    gamma1 :: Tele (Dom (Type'' Term Term))
gamma1      = [Dom (ArgName, Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList [Dom (ArgName, Type'' Term Term)]
ts1
    gamma2' :: Tele (Dom (Type'' Term Term))
gamma2'     = PatternSubstitution
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho0 (Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ [Dom (ArgName, Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
telFromList [Dom (ArgName, Type'' Term Term)]
ts2

    tel' :: Tele (Dom (Type'' Term Term))
tel'        = Tele (Dom (Type'' Term Term))
gamma1 Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
forall t. Abstract t => Tele (Dom (Type'' Term Term)) -> t -> t
`abstract` (Tele (Dom (Type'' Term Term))
delta Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term)) -> Tele (Dom (Type'' Term Term))
forall t. Abstract t => Tele (Dom (Type'' Term Term)) -> t -> t
`abstract` Tele (Dom (Type'' Term Term))
gamma2')


{-# INLINE telView #-}
-- | Gather leading Πs of a type in a telescope.
telView :: (MonadReduce m, MonadAddContext m) => Type -> m TelView
telView :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m TelView
telView = Int -> Type'' Term Term -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type'' Term Term -> m TelView
telViewUpTo (-Int
1)

{-# INLINE telViewUpTo #-}
-- | @telViewUpTo n t@ takes off the first @n@ function types of @t@.
-- Takes off all if @n < 0@.
telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView
telViewUpTo :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type'' Term Term -> m TelView
telViewUpTo Int
n Type'' Term Term
t = Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m TelView
telViewUpTo' Int
n (Bool -> Dom (Type'' Term Term) -> Bool
forall a b. a -> b -> a
const Bool
True) Type'' Term Term
t

{-# SPECIALIZE telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView #-}
-- | @telViewUpTo' n p t@ takes off $t$
--   the first @n@ (or arbitrary many if @n < 0@) function domains
--   as long as they satify @p@.
telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m TelView
telViewUpTo' Int
0 Dom (Type'' Term Term) -> Bool
p Type'' Term Term
t = TelView -> m TelView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> Type'' Term Term -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel Type'' Term Term
t
telViewUpTo' Int
n Dom (Type'' Term Term) -> Bool
p Type'' Term Term
t = do
  t <- Type'' Term Term -> m (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
t
  case unEl t of
    Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b | Dom (Type'' Term Term) -> Bool
p Dom (Type'' Term Term)
a ->
          -- Force the name to avoid retaining the rest of b.
      let !bn :: ArgName
bn = Abs (Type'' Term Term) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Type'' Term Term)
b in
      Dom (Type'' Term Term) -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom (Type'' Term Term)
a ArgName
bn (TelView -> TelView) -> m TelView -> m TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> (Type'' Term Term -> m TelView)
-> m TelView
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstractionAbs (Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall {t} {e}. Dom' t e -> Dom' t e
dropInvalidRew Dom (Type'' Term Term)
a) Abs (Type'' Term Term)
b ((Type'' Term Term -> m TelView) -> m TelView)
-> (Type'' Term Term -> m TelView) -> m TelView
forall a b. (a -> b) -> a -> b
$
          \Type'' Term Term
b -> Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m TelView
telViewUpTo' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Dom (Type'' Term Term) -> Bool
p Type'' Term Term
b
    Term
_ -> TelView -> m TelView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> Type'' Term Term -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel Type'' Term Term
t
  where
    -- We drop invalidated local rewrite rules
    -- Note that the returned telescope might still contain invalidated
    -- rewrite rules so adding the telescope to the context might fail
    dropInvalidRew :: Dom' t e -> Dom' t e
dropInvalidRew Dom' t e
a = if Dom' t e -> Bool
forall t e. Dom' t e -> Bool
invalidRew Dom' t e
a then Dom' t e
a Dom' t e -> (Dom' t e -> Dom' t e) -> Dom' t e
forall a b. a -> (a -> b) -> b
& (Maybe (RewDom' t) -> Identity (Maybe (RewDom' t)))
-> Dom' t e -> Identity (Dom' t e)
forall t e (f :: * -> *).
Functor f =>
(Maybe (RewDom' t) -> f (Maybe (RewDom' t)))
-> Dom' t e -> f (Dom' t e)
dRew ((Maybe (RewDom' t) -> Identity (Maybe (RewDom' t)))
 -> Dom' t e -> Identity (Dom' t e))
-> Maybe (RewDom' t) -> Dom' t e -> Dom' t e
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (RewDom' t)
forall a. Maybe a
Nothing else Dom' t e
a

-- | Returns Nothing if there are invalidated local rewrite rules present in
--   the telescope
safeTelViewUpTo' :: (MonadReduce m, MonadAddContext m)
  => Int -> (Dom Type -> Bool) -> Type -> MaybeT m TelView
safeTelViewUpTo' :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> MaybeT m TelView
safeTelViewUpTo' Int
n Dom (Type'' Term Term) -> Bool
p Type'' Term Term
t = do
  telv@(TelV tel _) <- Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> MaybeT m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m TelView
telViewUpTo' Int
n Dom (Type'' Term Term) -> Bool
p Type'' Term Term
t
  if any invalidRew tel then mzero else pure telv

{-# INLINE telViewPath #-}
telViewPath :: PureTCM m => Type -> m TelView
telViewPath :: forall (m :: * -> *). PureTCM m => Type'' Term Term -> m TelView
telViewPath = Int -> Type'' Term Term -> m TelView
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m TelView
telViewUpToPath (-Int
1)

{-# SPECIALIZE telViewUpToPath :: Int -> Type -> TCM TelView #-}
-- | @telViewUpToPath n t@ takes off @t@
--   the first @n@ (or arbitrary many if @n < 0@) function domains or Path types.
--
-- @telViewUpToPath n t = fst <$> telViewUpToPathBoundary' n t@
telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
telViewUpToPath :: forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m TelView
telViewUpToPath Int
n Type'' Term Term
t = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Type'' Term Term -> m TelView
forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
done Type'' Term Term
t else do
  Type'' Term Term
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
pathViewAsPi Type'' Term Term
t m (Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term))
     (Type'' Term Term))
-> (Either
      (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
    -> m TelView)
-> m TelView
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left  (Dom (Type'' Term Term)
a, Abs (Type'' Term Term)
b)          -> Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m TelView
recurse Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b
    Right (El Sort' Term
_ (Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b)) -> Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m TelView
recurse Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b
    Right Type'' Term Term
t               -> Type'' Term Term -> m TelView
forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
done Type'' Term Term
t
  where
    done :: a -> m (TelV a)
done a
t      = TelV a -> m (TelV a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TelV a -> m (TelV a)) -> TelV a -> m (TelV a)
forall a b. (a -> b) -> a -> b
$ Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom a)
forall a. Tele a
EmptyTel a
t
    recurse :: Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m TelView
recurse Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b = Dom (Type'' Term Term) -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom (Type'' Term Term)
a (Abs (Type'' Term Term) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Type'' Term Term)
b) (TelView -> TelView) -> m TelView -> m TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Type'' Term Term -> m TelView
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m TelView
telViewUpToPath (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
absBody Abs (Type'' Term Term)
b)

-- | Boundary conditions @[[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y]@.
-- For instance, if @p : Path A a b@, then @p i@ has boundary condition @(i,(a,b))@.
-- We call @i@ the /dimension/ and @(x,y)@ its /boundary/.
newtype Boundary' x a = Boundary { forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary :: [(x,(a,a))] }
  deriving (Int -> Boundary' x a -> ArgName -> ArgName
[Boundary' x a] -> ArgName -> ArgName
Boundary' x a -> ArgName
(Int -> Boundary' x a -> ArgName -> ArgName)
-> (Boundary' x a -> ArgName)
-> ([Boundary' x a] -> ArgName -> ArgName)
-> Show (Boundary' x a)
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
forall x a.
(Show x, Show a) =>
Int -> Boundary' x a -> ArgName -> ArgName
forall x a.
(Show x, Show a) =>
[Boundary' x a] -> ArgName -> ArgName
forall x a. (Show x, Show a) => Boundary' x a -> ArgName
$cshowsPrec :: forall x a.
(Show x, Show a) =>
Int -> Boundary' x a -> ArgName -> ArgName
showsPrec :: Int -> Boundary' x a -> ArgName -> ArgName
$cshow :: forall x a. (Show x, Show a) => Boundary' x a -> ArgName
show :: Boundary' x a -> ArgName
$cshowList :: forall x a.
(Show x, Show a) =>
[Boundary' x a] -> ArgName -> ArgName
showList :: [Boundary' x a] -> ArgName -> ArgName
Show, Boundary' x a
Boundary' x a -> Bool
Boundary' x a -> (Boundary' x a -> Bool) -> Null (Boundary' x a)
forall a. a -> (a -> Bool) -> Null a
forall x a. Boundary' x a
forall x a. Boundary' x a -> Bool
$cempty :: forall x a. Boundary' x a
empty :: Boundary' x a
$cnull :: forall x a. Boundary' x a -> Bool
null :: Boundary' x a -> Bool
Null)

-- | Usually, the dimensions of a boundary condition are interval /variables/,
-- represented by a de Bruijn index @Int@.
type Boundary = Boundary' Int Term

-- | Substitution formally creates dimensions that are interval /expressions/,
-- represented by a @Term@.
-- However, in practice these terms should be of the form @'var' i@.
type TmBoundary = Boundary' Term Term

-- | Turn dimension variables @i@ into dimension expressions @'var' i@.
tmBoundary :: Boundary' Int a -> Boundary' Term a
tmBoundary :: forall a. Boundary' Int a -> Boundary' Term a
tmBoundary = [(Term, (a, a))] -> Boundary' Term a
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary ([(Term, (a, a))] -> Boundary' Term a)
-> (Boundary' Int a -> [(Term, (a, a))])
-> Boundary' Int a
-> Boundary' Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, (a, a)) -> (Term, (a, a)))
-> [(Int, (a, a))] -> [(Term, (a, a))]
forall a b. (a -> b) -> [a] -> [b]
map' ((Int -> Term) -> (Int, (a, a)) -> (Term, (a, a))
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Int -> Term
var) ([(Int, (a, a))] -> [(Term, (a, a))])
-> (Boundary' Int a -> [(Int, (a, a))])
-> Boundary' Int a
-> [(Term, (a, a))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boundary' Int a -> [(Int, (a, a))]
forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary

-- | Turn dimension expressions into dimension variables.
-- Formally this is a partial operation, but should only be called when the precondition is met.
--
-- Precondition: the dimension terms in the boundary are all of the form @'var' i@.
varBoundary :: Boundary' Term a -> Boundary' Int a
varBoundary :: forall a. Boundary' Term a -> Boundary' Int a
varBoundary = [(Int, (a, a))] -> Boundary' Int a
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary ([(Int, (a, a))] -> Boundary' Int a)
-> (Boundary' Term a -> [(Int, (a, a))])
-> Boundary' Term a
-> Boundary' Int a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term, (a, a)) -> (Int, (a, a)))
-> [(Term, (a, a))] -> [(Int, (a, a))]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> Int) -> (Term, (a, a)) -> (Int, (a, a))
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Term -> Int
unVar) ([(Term, (a, a))] -> [(Int, (a, a))])
-> (Boundary' Term a -> [(Term, (a, a))])
-> Boundary' Term a
-> [(Int, (a, a))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boundary' Term a -> [(Term, (a, a))]
forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary
  where
    unVar :: Term -> Int
unVar (Var Int
i []) = Int
i
    unVar Term
_ = Int
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Substitution into a 'Boundary' a priori creates a 'TmBoundary' which we convert back via 'varBoundary'.
-- A priori, this is a partial operation.
instance Subst Boundary where
  type SubstArg Boundary = Term
  applySubst :: Substitution' (SubstArg Boundary) -> Boundary -> Boundary
applySubst Substitution' (SubstArg Boundary)
sub = Boundary' Term Term -> Boundary
forall a. Boundary' Term a -> Boundary' Int a
varBoundary (Boundary' Term Term -> Boundary)
-> (Boundary -> Boundary' Term Term) -> Boundary -> Boundary
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' (SubstArg (Boundary' Term Term))
-> Boundary' Term Term -> Boundary' Term Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Boundary)
Substitution' (SubstArg (Boundary' Term Term))
sub (Boundary' Term Term -> Boundary' Term Term)
-> (Boundary -> Boundary' Term Term)
-> Boundary
-> Boundary' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boundary -> Boundary' Term Term
forall a. Boundary' Int a -> Boundary' Term a
tmBoundary

instance Subst TmBoundary where
  type SubstArg TmBoundary = Term
  applySubst :: Substitution' (SubstArg (Boundary' Term Term))
-> Boundary' Term Term -> Boundary' Term Term
applySubst Substitution' (SubstArg (Boundary' Term Term))
sub = [(Term, (Term, Term))] -> Boundary' Term Term
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary ([(Term, (Term, Term))] -> Boundary' Term Term)
-> (Boundary' Term Term -> [(Term, (Term, Term))])
-> Boundary' Term Term
-> Boundary' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' (SubstArg [(Term, (Term, Term))])
-> [(Term, (Term, Term))] -> [(Term, (Term, Term))]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [(Term, (Term, Term))])
Substitution' (SubstArg (Boundary' Term Term))
sub ([(Term, (Term, Term))] -> [(Term, (Term, Term))])
-> (Boundary' Term Term -> [(Term, (Term, Term))])
-> Boundary' Term Term
-> [(Term, (Term, Term))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boundary' Term Term -> [(Term, (Term, Term))]
forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary

deriving instance (Pretty x, Pretty a) => Pretty (Boundary' x a)

{-# SPECIALIZE telViewUpToPathBoundary' :: Int -> Type -> TCM (TelView, Boundary) #-}
-- | Like 'telViewUpToPath' but also returns the 'Boundary' expected by the Path types encountered.
-- The boundary terms live in the telescope given by the 'TelView'.
-- Each point of the boundary has the type of the codomain of the Path type it got taken from, see 'fullBoundary'.
--
-- @
--  (TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary' n a
--  Input:  Δ ⊢ a
--  Output: Δ.Γ ⊢ b
--          Δ.Γ ⊢ T is the codomain of the PathP at variable i
--          Δ.Γ ⊢ i : I
--          Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
-- @
--
-- Useful to reconstruct IApplyP patterns after teleNamedArgs Γ.
--
telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' :: forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
n Type'' Term Term
t = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Type'' Term Term -> m (TelView, Boundary)
forall {m :: * -> *} {b} {a}.
(Monad m, Null b) =>
a -> m (TelV a, b)
done Type'' Term Term
t else do
  Type'' Term Term
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi' Type'' Term Term
t m (Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term))
-> (Either
      ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
      (Type'' Term Term)
    -> m (TelView, Boundary))
-> m (TelView, Boundary)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left ((Dom (Type'' Term Term)
a, Abs (Type'' Term Term)
b), (Term, Term)
xy)     -> (Term, Term) -> (TelView, Boundary) -> (TelView, Boundary)
forall {a} {a}.
Subst a =>
(a, a) -> (TelV a, Boundary' Int a) -> (TelV a, Boundary' Int a)
addEndPoints (Term, Term)
xy ((TelView, Boundary) -> (TelView, Boundary))
-> m (TelView, Boundary) -> m (TelView, Boundary)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (Type'' Term Term)
-> Abs (Type'' Term Term) -> m (TelView, Boundary)
recurse Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b
    Right (El Sort' Term
_ (Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b)) -> Dom (Type'' Term Term)
-> Abs (Type'' Term Term) -> m (TelView, Boundary)
recurse Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b
    Right Type'' Term Term
t               -> Type'' Term Term -> m (TelView, Boundary)
forall {m :: * -> *} {b} {a}.
(Monad m, Null b) =>
a -> m (TelV a, b)
done Type'' Term Term
t
  where
    done :: a -> m (TelV a, b)
done a
t      = (TelV a, b) -> m (TelV a, b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom a)
forall a. Tele a
EmptyTel a
t, b
forall a. Null a => a
empty)
    recurse :: Dom (Type'' Term Term)
-> Abs (Type'' Term Term) -> m (TelView, Boundary)
recurse Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b = (TelView -> TelView) -> (TelView, Boundary) -> (TelView, Boundary)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Dom (Type'' Term Term) -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom (Type'' Term Term)
a (Abs (Type'' Term Term) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Type'' Term Term)
b)) ((TelView, Boundary) -> (TelView, Boundary))
-> m (TelView, Boundary) -> m (TelView, Boundary)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> (Type'' Term Term -> m (TelView, Boundary))
-> m (TelView, Boundary)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b ((Type'' Term Term -> m (TelView, Boundary))
 -> m (TelView, Boundary))
-> (Type'' Term Term -> m (TelView, Boundary))
-> m (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ \Type'' Term Term
b -> Int -> Type'' Term Term -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m (TelView, Boundary)
telViewUpToPathBoundary' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type'' Term Term
b
    addEndPoints :: (a, a) -> (TelV a, Boundary' Int a) -> (TelV a, Boundary' Int a)
addEndPoints (a, a)
xy (telv :: TelV a
telv@(TelV Tele (Dom a)
tel a
_), Boundary [(Int, (a, a))]
cs) =
      let !s :: Int
s = Tele (Dom a) -> Int
forall a. Sized a => a -> Int
size Tele (Dom a)
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
      in (TelV a
telv, [(Int, (a, a))] -> Boundary' Int a
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary ([(Int, (a, a))] -> Boundary' Int a)
-> [(Int, (a, a))] -> Boundary' Int a
forall a b. (a -> b) -> a -> b
$ (Int
s, Int -> (a, a) -> (a, a)
forall a. Subst a => Int -> a -> a
raise (Tele (Dom a) -> Int
forall a. Sized a => a -> Int
size Tele (Dom a)
tel) (a, a)
xy) (Int, (a, a)) -> [(Int, (a, a))] -> [(Int, (a, a))]
forall a. a -> [a] -> [a]
: [(Int, (a, a))]
cs)


fullBoundary :: Telescope -> Boundary -> Boundary
fullBoundary :: Tele (Dom (Type'' Term Term)) -> Boundary -> Boundary
fullBoundary Tele (Dom (Type'' Term Term))
tel Boundary
bs =
      -- tel = Γ
      -- ΔΓ ⊢ b
      -- Δ ⊢ a = PiPath Γ bs b
      -- Δ.Γ ⊢ T is the codomain of the PathP at variable i
      -- Δ.Γ ⊢ i : I
      -- Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
      -- Δ.Γ | PiPath Γ bs A ⊢ teleElims tel bs : b
   let es :: [Elim]
es = Tele (Dom (Type'' Term Term)) -> Boundary -> [Elim]
forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> Boundary' Int a -> [Elim' a]
teleElims Tele (Dom (Type'' Term Term))
tel Boundary
bs
       l :: Int
l  = Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
tel
   in [(Int, (Term, Term))] -> Boundary
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary ([(Int, (Term, Term))] -> Boundary)
-> [(Int, (Term, Term))] -> Boundary
forall a b. (a -> b) -> a -> b
$ ((Int, (Term, Term)) -> (Int, (Term, Term)))
-> [(Int, (Term, Term))] -> [(Int, (Term, Term))]
forall a b. (a -> b) -> [a] -> [b]
map' (\ (Int
i, (Term, Term)
xy) -> (Int
i, (Term, Term)
xy (Term, Term) -> [Elim] -> (Term, Term)
forall t. Apply t => t -> [Elim] -> t
`applyE` (Int -> [Elim] -> [Elim]
forall a. Int -> [a] -> [a]
drop (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) [Elim]
es))) ([(Int, (Term, Term))] -> [(Int, (Term, Term))])
-> [(Int, (Term, Term))] -> [(Int, (Term, Term))]
forall a b. (a -> b) -> a -> b
$ Boundary -> [(Int, (Term, Term))]
forall x a. Boundary' x a -> [(x, (a, a))]
theBoundary Boundary
bs

{-# SPECIALIZE telViewUpToPathBoundary :: Int -> Type -> TCM (TelView, Boundary) #-}
-- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary n a@
--  Input:  Δ ⊢ a
--  Output: ΔΓ ⊢ b
--          ΔΓ ⊢ i : I
--          ΔΓ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : b
telViewUpToPathBoundary :: PureTCM m => Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary :: forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m (TelView, Boundary)
telViewUpToPathBoundary Int
i Type'' Term Term
a = do
   (telv@(TelV tel b), bs) <- Int -> Type'' Term Term -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
i Type'' Term Term
a
   return (telv, fullBoundary tel bs)

{-# INLINE telViewPathBoundary #-}
telViewPathBoundary :: PureTCM m => Type -> m (TelView, Boundary)
telViewPathBoundary :: forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m (TelView, Boundary)
telViewPathBoundary = Int -> Type'' Term Term -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m (TelView, Boundary)
telViewUpToPathBoundary' (-Int
1)


-- | @teleElimsB args bs = es@
--  Input:  Δ.Γ ⊢ args : Γ
--          Δ.Γ ⊢ T is the codomain of the PathP at variable i
--          Δ.Γ ⊢ i : I
--          Δ.Γ ⊢ bs = [ (i=0) -> t_i; (i=1) -> u_i ] : T
--  Output: Δ.Γ | PiPath Γ bs A ⊢ es : A
teleElims :: DeBruijn a => Telescope -> Boundary' Int a -> [Elim' a]
teleElims :: forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> Boundary' Int a -> [Elim' a]
teleElims Tele (Dom (Type'' Term Term))
tel (Boundary []) = (Arg a -> Elim' a) -> [Arg a] -> [Elim' a]
forall a b. (a -> b) -> [a] -> [b]
map' Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply ([Arg a] -> [Elim' a]) -> [Arg a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Arg a]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom (Type'' Term Term))
tel
teleElims Tele (Dom (Type'' Term Term))
tel (Boundary [(Int, (a, a))]
boundary) = (Arg a -> Elim' a) -> [Arg a] -> [Elim' a]
forall a b. (a -> b) -> [a] -> [b]
map' Arg a -> Elim' a
updateArg ([Arg a] -> [Elim' a]) -> [Arg a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Arg a]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom (Type'' Term Term))
tel
  where
    matchVar :: Int -> Maybe (a, a)
matchVar Int
i = (Int, (a, a)) -> (a, a)
forall a b. (a, b) -> b
snd ((Int, (a, a)) -> (a, a)) -> Maybe (Int, (a, a)) -> Maybe (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, (a, a)) -> Bool) -> [(Int, (a, a))] -> Maybe (Int, (a, a))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> ((Int, (a, a)) -> Int) -> (Int, (a, a)) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (a, a)) -> Int
forall a b. (a, b) -> a
fst) [(Int, (a, a))]
boundary
    updateArg :: Arg a -> Elim' a
updateArg a :: Arg a
a@(Arg ArgInfo
info a
p) =
      case a -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView a
p of
        Just Int
i | Just (a
t,a
u) <- Int -> Maybe (a, a)
matchVar Int
i -> a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
t a
u a
p
        Maybe Int
_                                 -> Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Arg a
a

{-# SPECIALIZE pathViewAsPi :: Type -> TCM (Either (Dom Type, Abs Type) Type) #-}
-- | Reduces 'Type'.
pathViewAsPi
  :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi :: forall (m :: * -> *).
PureTCM m =>
Type'' Term Term
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
pathViewAsPi Type'' Term Term
t = (((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
 -> Either
      (Dom (Type'' Term Term), Abs (Type'' Term Term))
      (Type'' Term Term))
-> (Type'' Term Term
    -> Either
         (Dom (Type'' Term Term), Abs (Type'' Term Term))
         (Type'' Term Term))
-> Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term)
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Dom (Type'' Term Term), Abs (Type'' Term Term))
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall a b. a -> Either a b
Left ((Dom (Type'' Term Term), Abs (Type'' Term Term))
 -> Either
      (Dom (Type'' Term Term), Abs (Type'' Term Term))
      (Type'' Term Term))
-> (((Dom (Type'' Term Term), Abs (Type'' Term Term)),
     (Term, Term))
    -> (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a, b) -> a
fst) Type'' Term Term
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall a b. b -> Either a b
Right (Either
   ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
   (Type'' Term Term)
 -> Either
      (Dom (Type'' Term Term), Abs (Type'' Term Term))
      (Type'' Term Term))
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi' Type'' Term Term
t

{-# SPECIALIZE pathViewAsPi' :: Type -> TCM (Either ((Dom Type, Abs Type), (Term,Term)) Type) #-}
-- | Reduces 'Type'.
pathViewAsPi'
  :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term,Term)) Type)
pathViewAsPi' :: forall (m :: * -> *).
PureTCM m =>
Type'' Term Term
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi' Type'' Term Term
t = do
  m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi'whnf m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> m (Type'' Term Term)
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type'' Term Term -> m (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
t

{-# SPECIALIZE pathViewAsPi'whnf :: TCM (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type) #-}
pathViewAsPi'whnf
  :: (HasBuiltins m)
  => m (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type)
pathViewAsPi'whnf :: forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi'whnf = do
  view <- m (Type'' Term Term -> PathView)
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term -> PathView)
pathView'
  minterval  <- getTerm' builtinInterval
  return $ \case
    (Type'' Term Term -> PathView
view -> PathType Sort' Term
s QName
l Arg Term
p Arg Term
a Arg Term
x Arg Term
y) | Just Term
interval <- Maybe Term
minterval ->
      let name :: ArgName
name | Lam ArgInfo
_ (Abs ArgName
n Term
_) <- Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a = ArgName
n
               | Bool
otherwise = ArgName
"i"
      in
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term)
forall a b. a -> Either a b
Left ( ( Type'' Term Term -> Dom (Type'' Term Term)
forall a. a -> Dom a
defaultDom (Type'' Term Term -> Dom (Type'' Term Term))
-> Type'' Term Term -> Dom (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
intervalSort Term
interval
               , ArgName -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. ArgName -> a -> Abs a
Abs ArgName
name (Type'' Term Term -> Abs (Type'' Term Term))
-> Type'' Term Term -> Abs (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort' Term -> Sort' Term
forall a. Subst a => Int -> a -> a
raise Int
1 Sort' Term
s) (Term -> Type'' Term Term) -> Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0]
               )
             , (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x, Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
y)
             )

    Type'' Term Term
t    -> Type'' Term Term
-> Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term)
forall a b. b -> Either a b
Right Type'' Term Term
t

-- | Returns @Left (a,b)@ in case the type is @Pi a b@ or @PathP b _ _@.
--   Assumes the 'Type' is in whnf.
piOrPath :: HasBuiltins m => Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath :: forall (m :: * -> *).
HasBuiltins m =>
Type'' Term Term
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
piOrPath Type'' Term Term
t = do
  (m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi'whnf m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> m (Type'' Term Term)
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type'' Term Term
t) m (Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term))
-> (Either
      ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
      (Type'' Term Term)
    -> Either
         (Dom (Type'' Term Term), Abs (Type'' Term Term))
         (Type'' Term Term))
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Left ((Dom (Type'' Term Term), Abs (Type'' Term Term))
p, (Term, Term)
_)           -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall a b. a -> Either a b
Left (Dom (Type'' Term Term), Abs (Type'' Term Term))
p
    Right (El Sort' Term
_ (Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b)) -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall a b. a -> Either a b
Left (Dom (Type'' Term Term)
a,Abs (Type'' Term Term)
b)
    Right Type'' Term Term
_               -> Type'' Term Term
-> Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
forall a b. b -> Either a b
Right Type'' Term Term
t

-- | Assumes 'Type' is in whnf.
telView'UpToPath :: Int -> Type -> TCM TelView
telView'UpToPath :: Int -> Type'' Term Term -> TCM TelView
telView'UpToPath Int
n Type'' Term Term
t = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then TCM TelView
done else do
  Type'' Term Term
-> TCMT
     IO
     (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
forall (m :: * -> *).
HasBuiltins m =>
Type'' Term Term
-> m (Either
        (Dom (Type'' Term Term), Abs (Type'' Term Term))
        (Type'' Term Term))
piOrPath Type'' Term Term
t TCMT
  IO
  (Either
     (Dom (Type'' Term Term), Abs (Type'' Term Term))
     (Type'' Term Term))
-> (Either
      (Dom (Type'' Term Term), Abs (Type'' Term Term)) (Type'' Term Term)
    -> TCM TelView)
-> TCM TelView
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'' Term Term)
a, Abs (Type'' Term Term)
b) -> Dom (Type'' Term Term) -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom (Type'' Term Term)
a (Abs (Type'' Term Term) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Type'' Term Term)
b) (TelView -> TelView) -> TCM TelView -> TCM TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Type'' Term Term -> TCM TelView
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m TelView
telViewUpToPath (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
absBody Abs (Type'' Term Term)
b)
    Right Type'' Term Term
_     -> TCM TelView
done
  where
    done :: TCM TelView
done = TelView -> TCM TelView
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> TCM TelView) -> TelView -> TCM TelView
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> Type'' Term Term -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel Type'' Term Term
t

telView'Path :: Type -> TCM TelView
telView'Path :: Type'' Term Term -> TCM TelView
telView'Path = Int -> Type'' Term Term -> TCM TelView
telView'UpToPath (-Int
1)

isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type))
isPath :: forall (m :: * -> *).
PureTCM m =>
Type'' Term Term
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
isPath Type'' Term Term
t = Type'' Term Term
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))))
-> (Type'' Term Term
    -> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))))
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Type'' Term Term -> m a)
-> m a
ifPath Type'' Term Term
t (\Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b -> Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))
 -> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))))
-> Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> Maybe a
Just (Dom (Type'' Term Term)
a,Abs (Type'' Term Term)
b)) (m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Type'' Term Term
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
forall a b. a -> b -> a
const (m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
 -> Type'' Term Term
 -> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))))
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Type'' Term Term
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. Maybe a
Nothing)

ifPath :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPath :: forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Type'' Term Term -> m a)
-> m a
ifPath Type'' Term Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Type'' Term Term -> m a
no = Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPathB Type'' Term Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes ((Blocked (Type'' Term Term) -> m a) -> m a)
-> (Blocked (Type'' Term Term) -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> m a
no (Type'' Term Term -> m a)
-> (Blocked (Type'' Term Term) -> Type'' Term Term)
-> Blocked (Type'' Term Term)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked (Type'' Term Term) -> Type'' Term Term
forall t a. Blocked' t a -> a
ignoreBlocking

{-# SPECIALIZE ifPathB :: Type -> (Dom Type -> Abs Type -> TCM a) -> (Blocked Type -> TCM a) -> TCM a #-}
ifPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPathB :: forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPathB Type'' Term Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Blocked (Type'' Term Term) -> m a
no = Type'' Term Term
-> (Blocker -> Type'' Term Term -> m a)
-> (NotBlocked -> Type'' Term Term -> m a)
-> m a
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
t
  (\Blocker
b Type'' Term Term
t -> Blocked (Type'' Term Term) -> m a
no (Blocked (Type'' Term Term) -> m a)
-> Blocked (Type'' Term Term) -> m a
forall a b. (a -> b) -> a -> b
$ Blocker -> Type'' Term Term -> Blocked (Type'' Term Term)
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b Type'' Term Term
t)
  (\NotBlocked
nb Type'' Term Term
t -> m (Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term))
-> (((Dom (Type'' Term Term), Abs (Type'' Term Term)),
     (Term, Term))
    -> m a)
-> (Type'' Term Term -> m a)
-> m a
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi'whnf m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> m (Type'' Term Term)
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type'' Term Term
t)
    ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term), Abs (Type'' Term Term)) -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes ((Dom (Type'' Term Term), Abs (Type'' Term Term)) -> m a)
-> (((Dom (Type'' Term Term), Abs (Type'' Term Term)),
     (Term, Term))
    -> (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a, b) -> a
fst)
    (Blocked (Type'' Term Term) -> m a
no (Blocked (Type'' Term Term) -> m a)
-> (Type'' Term Term -> Blocked (Type'' Term Term))
-> Type'' Term Term
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotBlocked -> Type'' Term Term -> Blocked (Type'' Term Term)
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
nb))

ifNotPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPathB :: forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Blocked (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
ifNotPathB = ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> (Blocked (Type'' Term Term) -> m a) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
  -> (Blocked (Type'' Term Term) -> m a) -> m a)
 -> (Blocked (Type'' Term Term) -> m a)
 -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> m a)
-> (Type'' Term Term
    -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
    -> (Blocked (Type'' Term Term) -> m a)
    -> m a)
-> Type'' Term Term
-> (Blocked (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPathB

ifPiOrPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiOrPathB :: forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiOrPathB Type'' Term Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Blocked (Type'' Term Term) -> m a
no = Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiTypeB Type'' Term Term
t
  (\Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b -> Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b)
  (\Blocked (Type'' Term Term)
bt -> m (Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term))
-> (((Dom (Type'' Term Term), Abs (Type'' Term Term)),
     (Term, Term))
    -> m a)
-> (Type'' Term Term -> m a)
-> m a
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi'whnf m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> m (Type'' Term Term)
-> m (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Blocked (Type'' Term Term) -> Type'' Term Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Type'' Term Term)
bt))
    ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term), Abs (Type'' Term Term)) -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes ((Dom (Type'' Term Term), Abs (Type'' Term Term)) -> m a)
-> (((Dom (Type'' Term Term), Abs (Type'' Term Term)),
     (Term, Term))
    -> (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a, b) -> a
fst)
    (Blocked (Type'' Term Term) -> m a
no (Blocked (Type'' Term Term) -> m a)
-> (Type'' Term Term -> Blocked (Type'' Term Term))
-> Type'' Term Term
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked (Type'' Term Term)
bt Blocked (Type'' Term Term)
-> Type'' Term Term -> Blocked (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>)))

ifNotPiOrPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiOrPathB :: forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Blocked (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
ifNotPiOrPathB = ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> (Blocked (Type'' Term Term) -> m a) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
  -> (Blocked (Type'' Term Term) -> m a) -> m a)
 -> (Blocked (Type'' Term Term) -> m a)
 -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> m a)
-> (Type'' Term Term
    -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
    -> (Blocked (Type'' Term Term) -> m a)
    -> m a)
-> Type'' Term Term
-> (Blocked (Type'' Term Term) -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiOrPathB

telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns :: forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term))
-> Boundary -> [NamedArg (Pattern' a)]
telePatterns = (forall a.
 DeBruijn a =>
 Tele (Dom (Type'' Term Term)) -> [NamedArg a])
-> Tele (Dom (Type'' Term Term))
-> Boundary
-> [NamedArg (Pattern' a)]
forall a.
DeBruijn a =>
(forall a.
 DeBruijn a =>
 Tele (Dom (Type'' Term Term)) -> [NamedArg a])
-> Tele (Dom (Type'' Term Term))
-> Boundary
-> [NamedArg (Pattern' a)]
telePatterns' Tele (Dom (Type'' Term Term)) -> [NamedArg a]
forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> [NamedArg a]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs

telePatterns' :: DeBruijn a =>
                (forall a. (DeBruijn a) => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' :: forall a.
DeBruijn a =>
(forall a.
 DeBruijn a =>
 Tele (Dom (Type'' Term Term)) -> [NamedArg a])
-> Tele (Dom (Type'' Term Term))
-> Boundary
-> [NamedArg (Pattern' a)]
telePatterns' forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> [NamedArg a]
f Tele (Dom (Type'' Term Term))
tel (Boundary []) = Tele (Dom (Type'' Term Term)) -> [NamedArg (Pattern' a)]
forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> [NamedArg a]
f Tele (Dom (Type'' Term Term))
tel
telePatterns' forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> [NamedArg a]
f Tele (Dom (Type'' Term Term))
tel (Boundary [(Int, (Term, Term))]
boundary) = [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
recurse ([Arg (Named NamedName a)] -> [NamedArg (Pattern' a)])
-> [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Arg (Named NamedName a)]
forall a.
DeBruijn a =>
Tele (Dom (Type'' Term Term)) -> [NamedArg a]
f Tele (Dom (Type'' Term Term))
tel
  where
    recurse :: [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
recurse = ((Arg (Named NamedName a) -> NamedArg (Pattern' a))
-> [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg (Named NamedName a) -> NamedArg (Pattern' a))
 -> [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)])
-> ((a -> Pattern' a)
    -> Arg (Named NamedName a) -> NamedArg (Pattern' a))
-> (a -> Pattern' a)
-> [Arg (Named NamedName a)]
-> [NamedArg (Pattern' a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName a -> Named NamedName (Pattern' a))
-> Arg (Named NamedName a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName a -> Named NamedName (Pattern' a))
 -> Arg (Named NamedName a) -> NamedArg (Pattern' a))
-> ((a -> Pattern' a)
    -> Named NamedName a -> Named NamedName (Pattern' a))
-> (a -> Pattern' a)
-> Arg (Named NamedName a)
-> NamedArg (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Pattern' a)
-> Named NamedName a -> Named NamedName (Pattern' a)
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) a -> Pattern' a
updateVar
    matchVar :: Int -> Maybe (Term, Term)
matchVar Int
i = (Int, (Term, Term)) -> (Term, Term)
forall a b. (a, b) -> b
snd ((Int, (Term, Term)) -> (Term, Term))
-> Maybe (Int, (Term, Term)) -> Maybe (Term, Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, (Term, Term)) -> Bool)
-> [(Int, (Term, Term))] -> Maybe (Int, (Term, Term))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool)
-> ((Int, (Term, Term)) -> Int) -> (Int, (Term, Term)) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Term, Term)) -> Int
forall a b. (a, b) -> a
fst) [(Int, (Term, Term))]
boundary
    updateVar :: a -> Pattern' a
updateVar a
x =
      case a -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView a
x of
        Just Int
i | Just (Term
t,Term
u) <- Int -> Maybe (Term, Term)
matchVar Int
i -> PatternInfo -> Term -> Term -> a -> Pattern' a
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
defaultPatternInfo Term
t Term
u a
x
        Maybe Int
_                                 -> PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo a
x

-- | Decomposing a function type.

mustBePi :: MonadReduce m => Type -> m (Dom Type, Abs Type)
mustBePi :: forall (m :: * -> *).
MonadReduce m =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
mustBePi Type'' Term Term
t = Type'' Term Term
-> (Type'' Term Term
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Type'' Term Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
ifNotPiType Type'' Term Term
t Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Dom (Type'' Term Term)
  -> Abs (Type'' Term Term)
  -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
 -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ ((Dom (Type'' Term Term), Abs (Type'' Term Term))
 -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- | If the given type is a @Pi@, pass its parts to the first continuation.
--   If not (or blocked), pass the reduced type to the second continuation.
ifPi :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
ifPi :: forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Term -> m a)
-> m a
ifPi Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Term -> m a
no = Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked Term -> m a)
-> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked Term -> m a)
-> m a
ifPiB Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes (Term -> m a
no (Term -> m a) -> (Blocked Term -> Term) -> Blocked Term -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking)

ifPiB :: (MonadReduce m) => Term -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
ifPiB :: forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked Term -> m a)
-> m a
ifPiB Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Blocked Term -> m a
no = Term
-> (Blocker -> Term -> m a) -> (NotBlocked -> Term -> m a) -> m a
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t
  (\Blocker
b Term
t -> Blocked Term -> m a
no (Blocked Term -> m a) -> Blocked Term -> m a
forall a b. (a -> b) -> a -> b
$ Blocker -> Term -> Blocked Term
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b Term
t) -- Pi type is never blocked
  (\NotBlocked
nb Term
t -> case Term
t of
    Pi Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b -> Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Dom (Type'' Term Term)
a Abs (Type'' Term Term)
b
    Term
_      -> Blocked Term -> m a
no (Blocked Term -> m a) -> Blocked Term -> m a
forall a b. (a -> b) -> a -> b
$ NotBlocked -> Term -> Blocked Term
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked
nb Term
t)

ifPiTypeB :: (MonadReduce m) => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiTypeB :: forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiTypeB (El Sort' Term
s Term
t) Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Blocked (Type'' Term Term) -> m a
no = Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked Term -> m a)
-> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked Term -> m a)
-> m a
ifPiB Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes (\Blocked Term
bt -> Blocked (Type'' Term Term) -> m a
no (Blocked (Type'' Term Term) -> m a)
-> Blocked (Type'' Term Term) -> m a
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type'' Term Term)
-> Blocked Term -> Blocked (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Blocked Term
bt)

-- | If the given type is a @Pi@, pass its parts to the first continuation.
--   If not (or blocked), pass the reduced type to the second continuation.
ifPiType :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPiType :: forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Type'' Term Term -> m a)
-> m a
ifPiType (El Sort' Term
s Term
t) Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes Type'' Term Term -> m a
no = Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Term -> m a)
-> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Term -> m a)
-> m a
ifPi Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a
yes (Type'' Term Term -> m a
no (Type'' Term Term -> m a)
-> (Term -> Type'' Term Term) -> Term -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s)

-- | If the given type is blocked or not a @Pi@, pass it reduced to the first continuation.
--   If it is a @Pi@, pass its parts to the second continuation.
ifNotPi :: MonadReduce m => Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPi :: forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
ifNotPi = ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> (Term -> m a) -> m a)
-> (Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
  -> (Term -> m a) -> m a)
 -> (Term -> m a)
 -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> m a)
-> (Term
    -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
    -> (Term -> m a)
    -> m a)
-> Term
-> (Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Term -> m a)
-> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Term -> m a)
-> m a
ifPi

-- | If the given type is blocked or not a @Pi@, pass it reduced to the first continuation.
--   If it is a @Pi@, pass its parts to the second continuation.
ifNotPiType :: MonadReduce m => Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType :: forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Type'' Term Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
ifNotPiType = ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> (Type'' Term Term -> m a) -> m a)
-> (Type'' Term Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
  -> (Type'' Term Term -> m a) -> m a)
 -> (Type'' Term Term -> m a)
 -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
 -> m a)
-> (Type'' Term Term
    -> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
    -> (Type'' Term Term -> m a)
    -> m a)
-> Type'' Term Term
-> (Type'' Term Term -> m a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Type'' Term Term -> m a)
-> m a
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Type'' Term Term -> m a)
-> m a
ifPiType

ifNotPiOrPathType :: (MonadReduce tcm, HasBuiltins tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType :: forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type'' Term Term
-> (Type'' Term Term -> tcm a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a)
-> tcm a
ifNotPiOrPathType Type'' Term Term
t Type'' Term Term -> tcm a
no Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a
yes = do
  Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a)
-> (Type'' Term Term -> tcm a)
-> tcm a
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Type'' Term Term -> m a)
-> m a
ifPiType Type'' Term Term
t Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a
yes (\ Type'' Term Term
t -> (((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
 -> tcm a)
-> (Type'' Term Term -> tcm a)
-> Either
     ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
     (Type'' Term Term)
-> tcm a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a)
-> (Dom (Type'' Term Term), Abs (Type'' Term Term)) -> tcm a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a
yes ((Dom (Type'' Term Term), Abs (Type'' Term Term)) -> tcm a)
-> (((Dom (Type'' Term Term), Abs (Type'' Term Term)),
     (Term, Term))
    -> (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
-> (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a, b) -> a
fst) (tcm a -> Type'' Term Term -> tcm a
forall a b. a -> b -> a
const (tcm a -> Type'' Term Term -> tcm a)
-> tcm a -> Type'' Term Term -> tcm a
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> tcm a
no Type'' Term Term
t) (Either
   ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
   (Type'' Term Term)
 -> tcm a)
-> tcm
     (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> tcm a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (tcm
  (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
pathViewAsPi'whnf tcm
  (Type'' Term Term
   -> Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
-> tcm (Type'' Term Term)
-> tcm
     (Either
        ((Dom (Type'' Term Term), Abs (Type'' Term Term)), (Term, Term))
        (Type'' Term Term))
forall a b. tcm (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type'' Term Term -> tcm (Type'' Term Term)
forall a. a -> tcm a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type'' Term Term
t))

shouldBePath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
shouldBePath :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
shouldBePath Type'' Term Term
t = Type'' Term Term
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> (Blocked (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPathB Type'' Term Term
t
  (((Dom (Type'' Term Term), Abs (Type'' Term Term))
 -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)
  (Blocked (Type'' Term Term) -> m (Type'' Term Term)
forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked (Blocked (Type'' Term Term) -> m (Type'' Term Term))
-> (Type'' Term Term
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Blocked (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    El Sort' Term
_ Dummy{} -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom (Type'' Term Term)
HasCallStack => Dom (Type'' Term Term)
__DUMMY_DOM__, ArgName -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. ArgName -> a -> Abs a
Abs ArgName
"x" Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__)
    Type'' Term Term
t -> TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBePath Type'' Term Term
t)

shouldBePi :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
shouldBePi :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
shouldBePi Type'' Term Term
t = Type'' Term Term
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> (Blocked (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiTypeB Type'' Term Term
t
  (((Dom (Type'' Term Term), Abs (Type'' Term Term))
 -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)
  (Blocked (Type'' Term Term) -> m (Type'' Term Term)
forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked (Blocked (Type'' Term Term) -> m (Type'' Term Term))
-> (Type'' Term Term
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Blocked (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    El Sort' Term
_ Dummy{} -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom (Type'' Term Term)
HasCallStack => Dom (Type'' Term Term)
__DUMMY_DOM__, ArgName -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. ArgName -> a -> Abs a
Abs ArgName
"x" Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__)
    Type'' Term Term
t -> TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBePi Type'' Term Term
t)

shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
shouldBePiOrPath :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type'' Term Term
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
shouldBePiOrPath Type'' Term Term
t = Type'' Term Term
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> (Blocked (Type'' Term Term)
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
PureTCM m =>
Type'' Term Term
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> (Blocked (Type'' Term Term) -> m a)
-> m a
ifPiOrPathB Type'' Term Term
t
  (((Dom (Type'' Term Term), Abs (Type'' Term Term))
 -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Dom (Type'' Term Term)
-> Abs (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)
  (Blocked (Type'' Term Term) -> m (Type'' Term Term)
forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked (Blocked (Type'' Term Term) -> m (Type'' Term Term))
-> (Type'' Term Term
    -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> Blocked (Type'' Term Term)
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    El Sort' Term
_ Dummy{} -> (Dom (Type'' Term Term), Abs (Type'' Term Term))
-> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom (Type'' Term Term)
HasCallStack => Dom (Type'' Term Term)
__DUMMY_DOM__, ArgName -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. ArgName -> a -> Abs a
Abs ArgName
"x" Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__)
    Type'' Term Term
t -> TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term)))
-> TypeError -> m (Dom (Type'' Term Term), Abs (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBePi Type'' Term Term
t) -- TODO: separate error

-- | A safe variant of 'piApply'.

class PiApplyM a where
  piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type

  piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type
  piApplyM = m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
piApplyM' m Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
  {-# INLINE piApplyM #-}

instance PiApplyM Term where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> Term -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t Term
v = Type'' Term Term
-> (Type'' Term Term -> m (Type'' Term Term))
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term) -> m (Type'' Term Term))
-> m (Type'' Term Term)
forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type'' Term Term
-> (Type'' Term Term -> tcm a)
-> (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> tcm a)
-> tcm a
ifNotPiOrPathType Type'' Term Term
t (\Type'' Term Term
_ -> Empty -> Type'' Term Term
forall a. Empty -> a
absurd (Empty -> Type'' Term Term) -> m Empty -> m (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Empty
err) {-else-} ((Dom (Type'' Term Term)
  -> Abs (Type'' Term Term) -> m (Type'' Term Term))
 -> m (Type'' Term Term))
-> (Dom (Type'' Term Term)
    -> Abs (Type'' Term Term) -> m (Type'' Term Term))
-> m (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ \ Dom (Type'' Term Term)
_ Abs (Type'' Term Term)
b -> Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> m (Type'' Term Term))
-> Type'' Term Term -> m (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Abs (Type'' Term Term)
-> SubstArg (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs (Type'' Term Term)
b Term
SubstArg (Type'' Term Term)
v
  {-# INLINABLE piApplyM' #-}

{-# SPECIALIZE piApplyM' :: TCM Empty -> Type -> Term -> TCM Type #-}

instance PiApplyM a => PiApplyM (Arg a) where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> Arg a -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t = m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t (a -> m (Type'' Term Term))
-> (Arg a -> a) -> Arg a -> m (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

instance PiApplyM a => PiApplyM (Named n a) where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> Named n a -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t = m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t (a -> m (Type'' Term Term))
-> (Named n a -> a) -> Named n a -> m (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named n a -> a
forall name a. Named name a -> a
namedThing

instance PiApplyM a => PiApplyM [a] where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> [a] -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t = (m (Type'' Term Term) -> a -> m (Type'' Term Term))
-> m (Type'' Term Term) -> [a] -> m (Type'' Term Term)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ m (Type'' Term Term)
mt a
v -> m (Type'' Term Term)
mt m (Type'' Term Term)
-> (Type'' Term Term -> m (Type'' Term Term))
-> m (Type'' Term Term)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type'' Term Term
t -> (m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
piApplyM' m Empty
err Type'' Term Term
t a
v)) (Type'' Term Term -> m (Type'' Term Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type'' Term Term
t)


-- | Compute type arity

typeArity :: Type -> TCM Nat
typeArity :: Type'' Term Term -> TCM Int
typeArity Type'' Term Term
t = do
  TelV tel _ <- Type'' Term Term -> TCM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m TelView
telView Type'' Term Term
t
  return (size tel)

-- | Fold a telescope into a monadic computation, adding variables to the
-- context at each step.

foldrTelescopeM
  :: MonadAddContext m
  => (Dom (ArgName, Type) -> m b -> m b)
  -> m b
  -> Telescope
  -> m b
foldrTelescopeM :: forall (m :: * -> *) b.
MonadAddContext m =>
(Dom (ArgName, Type'' Term Term) -> m b -> m b)
-> m b -> Tele (Dom (Type'' Term Term)) -> m b
foldrTelescopeM Dom (ArgName, Type'' Term Term) -> m b -> m b
f m b
b = Tele (Dom (Type'' Term Term)) -> m b
go
  where
    go :: Tele (Dom (Type'' Term Term)) -> m b
go Tele (Dom (Type'' Term Term))
EmptyTel = m b
b
    go (ExtendTel Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel) =
      Dom (ArgName, Type'' Term Term) -> m b -> m b
f ((Abs (Tele (Dom (Type'' Term Term))) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Tele (Dom (Type'' Term Term)))
tel,) (Type'' Term Term -> (ArgName, Type'' Term Term))
-> Dom (Type'' Term Term) -> Dom (ArgName, Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (Type'' Term Term)
a) (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term)
-> Abs (Tele (Dom (Type'' Term Term)))
-> (Tele (Dom (Type'' Term Term)) -> m b)
-> m b
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstraction Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel Tele (Dom (Type'' Term Term)) -> m b
go