{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Telescope where

import Prelude hiding (null)

import Control.Monad

import Data.Foldable (find)
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] -> Maybe Permutation
reorderTel [Dom Type]
tel = ((Int, Dom Type) -> (Int, Dom Type) -> Bool)
-> [(Int, Dom Type)] -> Maybe Permutation
forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (Int, Dom Type) -> (Int, Dom Type) -> Bool
forall {t} {b} {a} {t} {t}.
Free t =>
(Int, b) -> (a, Dom' t (Type'' t t)) -> Bool
comesBefore [(Int, Dom Type)]
tel'
  where
    tel' :: [(Int, Dom Type)]
tel' = [Int] -> [Dom Type] -> [(Int, Dom Type)]
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] -> Int
forall a. Sized a => a -> Int
size [Dom Type]
tel) [Dom Type]
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] -> Permutation
reorderTel_ [Dom Type]
tel = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Dom Type] -> Maybe Permutation
reorderTel [Dom Type]
tel)

-- | Unflatten: turns a flattened telescope into a proper telescope. Must be
--   properly ordered.
unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
unflattenTel :: [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [ArgName]
xs [Dom Type]
tel = Int -> [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel' ([Dom Type] -> Int
forall a. Sized a => a -> Int
size [Dom Type]
tel) [ArgName]
xs [Dom Type]
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] -> Tele (Dom Type)
unflattenTel' !Int
n [ArgName]
xs [Dom Type]
tel = case ([ArgName]
xs, [Dom Type]
tel) of
  ([],     [])      -> Tele (Dom Type)
forall a. Tele a
EmptyTel
  (ArgName
x : [ArgName]
xs, Dom Type
a : [Dom Type]
tel) -> Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a' (ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom Type)
tel')
    where
    tel' :: Tele (Dom Type)
tel' = Int -> [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [ArgName]
xs [Dom Type]
tel
    a' :: Dom Type
a'   = Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Dom Type))
rho Dom Type
a
    rho :: Substitution' Term
rho  = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$
           Int -> Term -> [Term]
forall a. Int -> a -> [a]
replicate Int
n ((CallStack -> Term) -> Term
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Term
impossibleTerm)
  ([],    Dom Type
_ : [Dom Type]
_) -> Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
  (ArgName
_ : [ArgName]
_, [])    -> Tele (Dom Type)
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) -> Tele (Dom Type)
renameTel []           Tele (Dom Type)
EmptyTel           = Tele (Dom Type)
forall a. Tele a
EmptyTel
renameTel (Maybe ArgName
Nothing:[Maybe ArgName]
xs) (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel') = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName] -> Tele (Dom Type) -> Tele (Dom Type)
renameTel [Maybe ArgName]
xs (Tele (Dom Type) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Abs (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom Type))
tel'
renameTel (Just ArgName
x :[Maybe ArgName]
xs) (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel') = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName] -> Tele (Dom Type) -> Tele (Dom Type)
renameTel [Maybe ArgName]
xs (Tele (Dom Type) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Abs (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Abs (Tele (Dom Type))
tel' { absName = x })
renameTel []           (ExtendTel Dom Type
_ Abs (Tele (Dom Type))
_   ) = Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
renameTel (Maybe ArgName
_      :[Maybe ArgName]
_ ) Tele (Dom Type)
EmptyTel           = Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

teleArgNames :: Telescope -> [Arg ArgName]
teleArgNames :: Tele (Dom Type) -> [Arg ArgName]
teleArgNames = Tele (Dom Type) -> [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) -> Tele (Dom Type) -> [NamedArg a]
tele2NamedArgs Tele (Dom Type)
tel0 Tele (Dom Type)
tel =
  [ ArgInfo -> Named_ a -> NamedArg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (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
argName) (ArgName -> Int -> a
forall a. DeBruijn a => ArgName -> Int -> a
deBruijnNamedVar ArgName
varName Int
i))
  | (Int
i, Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = (ArgName
argName,Type
_)}, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (ArgName
varName,Type
_)}) <- [Int]
-> [Dom (ArgName, Type)]
-> [Dom (ArgName, Type)]
-> [(Int, Dom (ArgName, Type), Dom (ArgName, Type))]
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)] -> Int
forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
l) [Dom (ArgName, Type)]
l0 [Dom (ArgName, Type)]
l ]
  where
  l :: [Dom (ArgName, Type)]
l  = Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel
  l0 :: [Dom (ArgName, Type)]
l0 = Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel0

-- | Split the telescope at the specified position.
splitTelescopeAt :: Int -> Telescope -> (Telescope,Telescope)
splitTelescopeAt :: Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt Int
n Tele (Dom Type)
tel
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0    = (Tele (Dom Type)
forall a. Tele a
EmptyTel, Tele (Dom Type)
tel)
  | Bool
otherwise = Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt' Int
n Tele (Dom Type)
tel
    where
      splitTelescopeAt' :: Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt' Int
_ Tele (Dom Type)
EmptyTel          = (Tele (Dom Type)
forall a. Tele a
EmptyTel,Tele (Dom Type)
forall a. Tele a
EmptyTel)
      splitTelescopeAt' Int
1 (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) = (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs (Tele (Dom Type))
tel Abs (Tele (Dom Type)) -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Tele (Dom Type)
forall a. Tele a
EmptyTel), Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom Type))
tel)
      splitTelescopeAt' Int
m (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) = (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs (Tele (Dom Type))
tel Abs (Tele (Dom Type)) -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Tele (Dom Type)
tel'), Tele (Dom Type)
tel'')
        where
          (Tele (Dom Type)
tel', Tele (Dom Type)
tel'') = Int -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
splitTelescopeAt (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type)))
-> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom Type))
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) -> Tele (Dom Type)
permuteTel Permutation
perm Tele (Dom Type)
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) -> [ArgName]
teleNames Tele (Dom Type)
tel
      types :: [Dom Type]
types = Permutation -> [Dom Type] -> [Dom Type]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Impossible -> Permutation -> [Dom Type] -> [Dom Type]
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm) ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
  in  [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [ArgName]
names [Dom Type]
types

-- | Like 'permuteTel', but start with a context.
--
permuteContext :: Permutation -> Context -> Telescope
permuteContext :: Permutation -> Context -> Tele (Dom Type)
permuteContext Permutation
perm Context
ctx = Permutation -> Tele (Dom Type) -> Tele (Dom Type)
permuteTel Permutation
perm (Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Context -> Tele (Dom Type)
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) -> VarSet -> VarSet
varDependencies Tele (Dom Type)
tel = VarSet -> VarSet
addLocks (VarSet -> VarSet) -> (VarSet -> VarSet) -> VarSet -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> VarSet -> VarSet
allDependencies Tele (Dom Type)
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) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
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) -> VarSet -> VarSet
allDependencies Tele (Dom Type)
tel VarSet
vs = VarSet -> [Dom Type] -> Int -> VarSet -> VarSet
loop VarSet
forall a. Null a => a
empty (Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenRevTel Tele (Dom Type)
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] -> Int -> VarSet -> VarSet
loop !VarSet
deps [Dom Type]
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] -> [Dom Type]
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]
telRev of
                [] ->
                  -- Ignore all deps outside the telescope
                  VarSet
deps
                (Dom Type
ti:[Dom Type]
telRev) ->
                  VarSet -> [Dom Type] -> Int -> VarSet -> VarSet
loop (Int -> VarSet -> VarSet
VarSet.insert Int
ix VarSet
deps) [Dom Type]
telRev Int
ix (VarSet -> VarSet -> VarSet
VarSet.union (Dom Type -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Dom Type
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) -> VarSet -> VarSet
varDependents Tele (Dom Type)
tel VarSet
vs =
  VarSet -> [Dom Type] -> Int -> VarSet -> VarSet
loop VarSet
forall a. Null a => a
empty (Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel) (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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] -> Int -> VarSet -> VarSet
loop !VarSet
deps [Dom Type]
tel Int
ix VarSet
work =
      case [Dom Type]
tel of
        [] -> VarSet
deps
        (Dom Type
ti:[Dom Type]
tel) ->
          if (Int -> Bool) -> Dom Type -> Bool
forall t. Free t => (Int -> Bool) -> t -> Bool
anyFreeVar (Int -> VarSet -> Bool
`VarSet.member` VarSet
work) Dom Type
ti then
            VarSet -> [Dom Type] -> Int -> VarSet -> VarSet
loop (Int -> VarSet -> VarSet
VarSet.insert Int
ix VarSet
deps) [Dom Type]
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] -> Int -> VarSet -> VarSet
loop VarSet
deps [Dom Type]
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)
firstPart  :: Telescope
  , SplitTel -> Tele (Dom Type)
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) -> SplitTel
splitTelescope VarSet
fv Tele (Dom Type)
tel = Tele (Dom Type) -> Tele (Dom Type) -> Permutation -> SplitTel
SplitTel Tele (Dom Type)
tel1 Tele (Dom Type)
tel2 Permutation
perm
  where
    names :: [ArgName]
names = Tele (Dom Type) -> [ArgName]
teleNames Tele (Dom Type)
tel
    ts0 :: [Dom Type]
ts0   = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
    n :: Int
n     = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel

    is :: VarSet
is    = Tele (Dom Type) -> VarSet -> VarSet
varDependencies Tele (Dom Type)
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]
ts1   = Impossible -> Permutation -> [Dom Type] -> [Dom Type]
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm) (Permutation -> [Dom Type] -> [Dom Type]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [Dom Type]
ts0)

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

    m :: Int
m     = VarSet -> Int
VarSet.size VarSet
is
    (Tele (Dom Type)
tel1, Tele (Dom Type)
tel2) = [Dom (ArgName, Type)] -> Tele (Dom Type)
telFromList ([Dom (ArgName, Type)] -> Tele (Dom Type))
-> ([Dom (ArgName, Type)] -> Tele (Dom Type))
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
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)] -> Tele (Dom Type)
telFromList (([Dom (ArgName, Type)], [Dom (ArgName, Type)])
 -> (Tele (Dom Type), Tele (Dom Type)))
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Int
-> [Dom (ArgName, Type)]
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m ([Dom (ArgName, Type)]
 -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
-> [Dom (ArgName, Type)]
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
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) -> Maybe SplitTel
splitTelescopeExact [Int]
is Tele (Dom Type)
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) -> Tele (Dom Type) -> Permutation -> SplitTel
SplitTel Tele (Dom Type)
tel1 Tele (Dom Type)
tel2 Permutation
perm
  where
    names :: [ArgName]
names = Tele (Dom Type) -> [ArgName]
teleNames Tele (Dom Type)
tel
    ts0 :: [Dom Type]
ts0   = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
    n :: Int
n     = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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
t = Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
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 -> Bool
forall t. Free t => (Int -> Bool) -> t -> Bool
allFreeVar Int -> Bool
good Dom Type
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]
ts1   = Impossible -> Permutation -> [Dom Type] -> [Dom Type]
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm) (Permutation -> [Dom Type] -> [Dom Type]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [Dom Type]
ts0)

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

    m :: Int
m     = [Int] -> Int
forall a. Sized a => a -> Int
size [Int]
is
    (Tele (Dom Type)
tel1, Tele (Dom Type)
tel2) = [Dom (ArgName, Type)] -> Tele (Dom Type)
telFromList ([Dom (ArgName, Type)] -> Tele (Dom Type))
-> ([Dom (ArgName, Type)] -> Tele (Dom Type))
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
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)] -> Tele (Dom Type)
telFromList (([Dom (ArgName, Type)], [Dom (ArgName, Type)])
 -> (Tele (Dom Type), Tele (Dom Type)))
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Int
-> [Dom (ArgName, Type)]
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m ([Dom (ArgName, Type)]
 -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
-> [Dom (ArgName, Type)]
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
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)
-> Int
-> Pattern' DBPatVar
-> Maybe (Tele (Dom Type), PatternSubstitution, Permutation)
instantiateTelescope Tele (Dom Type)
tel Int
k Pattern' DBPatVar
p = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok Maybe ()
-> (Tele (Dom Type), PatternSubstitution, Permutation)
-> Maybe (Tele (Dom Type), PatternSubstitution, Permutation)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (Tele (Dom Type)
tel', PatternSubstitution
sigma, Permutation -> Permutation
reverseP Permutation
perm)
  where
    names :: [ArgName]
names = Tele (Dom Type) -> [ArgName]
teleNames Tele (Dom Type)
tel
    ts0 :: [Dom Type]
ts0   = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
    n :: Int
n     = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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) -> VarSet -> VarSet
varDependencies Tele (Dom Type)
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) -> VarSet -> VarSet
varDependents Tele (Dom Type)
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]
ts1   = Permutation -> [Dom Type] -> [Dom Type]
forall a. Permutation -> [a] -> [a]
permute Permutation
permL' ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> [Dom Type] -> [Dom Type]
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma [Dom Type]
ts0
    tel' :: Tele (Dom Type)
tel'  = [ArgName] -> [Dom Type] -> Tele (Dom Type)
unflattenTel (Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
permL' [ArgName]
names) [Dom Type]
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)
-> Int
-> Tele (Dom Type)
-> ConHead
-> (Tele (Dom Type), PatternSubstitution)
expandTelescopeVar Tele (Dom Type)
gamma Int
k Tele (Dom Type)
delta ConHead
c = (Tele (Dom Type)
tel', PatternSubstitution
rho)
  where
    ([Dom (ArgName, Type)]
ts1,Dom (ArgName, Type)
xa:[Dom (ArgName, Type)]
ts2) = ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a. a -> Maybe a -> a
fromMaybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
 -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
-> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
-> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$
                    Int
-> [Dom (ArgName, Type)]
-> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
k ([Dom (ArgName, Type)]
 -> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)]))
-> [Dom (ArgName, Type)]
-> Maybe ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
gamma
    a :: Dom Type
a = Int -> Dom Type -> Dom Type
forall a. Subst a => Int -> a -> a
raise (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta) ((ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (ArgName, Type)
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)
conPType   = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
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) -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
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) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta)  -- Γ₁Δ ⊢ ρ₀ : Γ₁(x : D pars)
    rho :: PatternSubstitution
rho         = Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS ([Dom (ArgName, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (ArgName, Type)]
ts2) PatternSubstitution
rho0               -- Γ₁ΔΓ₂ρ₀ ⊢ ρ : Γ₁(x : D pars)Γ₂

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

    tel' :: Tele (Dom Type)
tel'        = Tele (Dom Type)
gamma1 Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` (Tele (Dom Type)
delta Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Tele (Dom Type)
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 -> m TelView
telView = Int -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> 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 -> m TelView
telViewUpTo Int
n Type
t = Int -> (Dom Type -> Bool) -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Int
n (Bool -> Dom Type -> Bool
forall a b. a -> b -> a
const Bool
True) Type
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 -> Bool) -> Type -> m TelView
telViewUpTo' Int
0 Dom Type -> Bool
p Type
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) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t
telViewUpTo' Int
n Dom Type -> Bool
p Type
t = do
  t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case unEl t of
    Pi Dom Type
a Abs Type
b | Dom Type -> Bool
p Dom Type
a ->
          -- Force the name to avoid retaining the rest of b.
      let !bn :: ArgName
bn = Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b in
      Dom Type -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom Type
a ArgName
bn (TelView -> TelView) -> m TelView -> m TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        Dom Type -> Abs Type -> (Type -> m TelView) -> m TelView
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a Abs Type
b ((Type -> m TelView) -> m TelView)
-> (Type -> m TelView) -> m TelView
forall a b. (a -> b) -> a -> b
$ \Type
b -> Int -> (Dom Type -> Bool) -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Dom Type -> Bool
p Type
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) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t

{-# INLINE telViewPath #-}
telViewPath :: PureTCM m => Type -> m TelView
telViewPath :: forall (m :: * -> *). PureTCM m => Type -> m TelView
telViewPath = Int -> Type -> m TelView
forall (m :: * -> *). PureTCM m => Int -> Type -> 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 -> m TelView
telViewUpToPath Int
n Type
t = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Type -> m TelView
forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
done Type
t else do
  Type -> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t m (Either (Dom Type, Abs Type) Type)
-> (Either (Dom Type, Abs Type) Type -> 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
a, Abs Type
b)          -> Dom Type -> Abs Type -> m TelView
recurse Dom Type
a Abs Type
b
    Right (El Sort' Term
_ (Pi Dom Type
a Abs Type
b)) -> Dom Type -> Abs Type -> m TelView
recurse Dom Type
a Abs Type
b
    Right Type
t               -> Type -> m TelView
forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
done Type
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 -> Abs Type -> m TelView
recurse Dom Type
a Abs Type
b = Dom Type -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b) (TelView -> TelView) -> m TelView -> m TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Type -> m TelView
forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
telViewUpToPath (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
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 -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
n Type
t = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Type -> m (TelView, Boundary)
forall {m :: * -> *} {b} {a}.
(Monad m, Null b) =>
a -> m (TelV a, b)
done Type
t else do
  Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi' Type
t m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> (Either ((Dom Type, Abs Type), (Term, Term)) Type
    -> 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
a, Abs Type
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 -> Abs Type -> m (TelView, Boundary)
recurse Dom Type
a Abs Type
b
    Right (El Sort' Term
_ (Pi Dom Type
a Abs Type
b)) -> Dom Type -> Abs Type -> m (TelView, Boundary)
recurse Dom Type
a Abs Type
b
    Right Type
t               -> Type -> m (TelView, Boundary)
forall {m :: * -> *} {b} {a}.
(Monad m, Null b) =>
a -> m (TelV a, b)
done Type
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 -> Abs Type -> m (TelView, Boundary)
recurse Dom Type
a Abs Type
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 -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
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
-> Abs Type
-> (Type -> m (TelView, Boundary))
-> m (TelView, Boundary)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a Abs Type
b ((Type -> m (TelView, Boundary)) -> m (TelView, Boundary))
-> (Type -> m (TelView, Boundary)) -> m (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ \Type
b -> Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type
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) =
      (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
$ (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, 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) -> Boundary -> Boundary
fullBoundary Tele (Dom Type)
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) -> Boundary -> [Elim]
forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' Int a -> [Elim' a]
teleElims Tele (Dom Type)
tel Boundary
bs
       l :: Int
l  = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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 -> m (TelView, Boundary)
telViewUpToPathBoundary Int
i Type
a = do
   (telv@(TelV tel b), bs) <- Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
i Type
a
   return (telv, fullBoundary tel bs)

{-# INLINE telViewPathBoundary #-}
telViewPathBoundary :: PureTCM m => Type -> m (TelView, Boundary)
telViewPathBoundary :: forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
telViewPathBoundary = Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> 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) -> Boundary' Int a -> [Elim' a]
teleElims Tele (Dom Type)
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) -> [Arg a]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel
teleElims Tele (Dom Type)
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) -> [Arg a]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
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 -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t = (((Dom Type, Abs Type), (Term, Term))
 -> Either (Dom Type, Abs Type) Type)
-> (Type -> Either (Dom Type, Abs Type) Type)
-> Either ((Dom Type, Abs Type), (Term, Term)) Type
-> Either (Dom Type, Abs Type) Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type
forall a b. a -> Either a b
Left ((Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type)
-> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
-> ((Dom Type, Abs Type), (Term, Term))
-> Either (Dom Type, Abs Type) Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
forall a b. (a, b) -> a
fst) Type -> Either (Dom Type, Abs Type) Type
forall a b. b -> Either a b
Right (Either ((Dom Type, Abs Type), (Term, Term)) Type
 -> Either (Dom Type, Abs Type) Type)
-> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m (Either (Dom Type, Abs Type) Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi' Type
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 -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi' Type
t = do
  m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
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 -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf = do
  view <- m (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  minterval  <- getTerm' builtinInterval
  return $ \case
    (Type -> 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, Abs Type), (Term, Term))
-> Either ((Dom Type, Abs Type), (Term, Term)) Type
forall a b. a -> Either a b
Left ( ( Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
intervalSort Term
interval
               , ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
name (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
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 -> Type
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
t    -> Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
forall a b. b -> Either a b
Right Type
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 -> m (Either (Dom Type, Abs Type) Type)
piOrPath Type
t = do
  (m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t) m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> (Either ((Dom Type, Abs Type), (Term, Term)) Type
    -> Either (Dom Type, Abs Type) Type)
-> m (Either (Dom Type, Abs Type) Type)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Left ((Dom Type, Abs Type)
p, (Term, Term)
_)           -> (Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type
forall a b. a -> Either a b
Left (Dom Type, Abs Type)
p
    Right (El Sort' Term
_ (Pi Dom Type
a Abs Type
b)) -> (Dom Type, Abs Type) -> Either (Dom Type, Abs Type) Type
forall a b. a -> Either a b
Left (Dom Type
a,Abs Type
b)
    Right Type
_               -> Type -> Either (Dom Type, Abs Type) Type
forall a b. b -> Either a b
Right Type
t

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

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

isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type))
isPath :: forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath Type
t = Type
-> (Dom Type -> Abs Type -> m (Maybe (Dom Type, Abs Type)))
-> (Type -> m (Maybe (Dom Type, Abs Type)))
-> m (Maybe (Dom Type, Abs Type))
forall (m :: * -> *) a.
PureTCM m =>
Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPath Type
t (\Dom Type
a Abs Type
b -> Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type)))
-> Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type))
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Type) -> Maybe (Dom Type, Abs Type)
forall a. a -> Maybe a
Just (Dom Type
a,Abs Type
b)) (m (Maybe (Dom Type, Abs Type))
-> Type -> m (Maybe (Dom Type, Abs Type))
forall a b. a -> b -> a
const (m (Maybe (Dom Type, Abs Type))
 -> Type -> m (Maybe (Dom Type, Abs Type)))
-> m (Maybe (Dom Type, Abs Type))
-> Type
-> m (Maybe (Dom Type, Abs Type))
forall a b. (a -> b) -> a -> b
$ Maybe (Dom Type, Abs Type) -> m (Maybe (Dom Type, Abs Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom Type, Abs Type)
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 -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPath Type
t Dom Type -> Abs Type -> m a
yes Type -> m a
no = Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
forall (m :: * -> *) a.
PureTCM m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPathB Type
t Dom Type -> Abs Type -> m a
yes ((Blocked Type -> m a) -> m a) -> (Blocked Type -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ Type -> m a
no (Type -> m a) -> (Blocked Type -> Type) -> Blocked Type -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocked Type -> Type
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
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPathB Type
t Dom Type -> Abs Type -> m a
yes Blocked Type -> m a
no = Type
-> (Blocker -> Type -> m a) -> (NotBlocked -> Type -> 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
t
  (\Blocker
b Type
t -> Blocked Type -> m a
no (Blocked Type -> m a) -> Blocked Type -> m a
forall a b. (a -> b) -> a -> b
$ Blocker -> Type -> Blocked Type
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b Type
t)
  (\NotBlocked
nb Type
t -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> (((Dom Type, Abs Type), (Term, Term)) -> m a)
-> (Type -> 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 -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t)
    ((Dom Type -> Abs Type -> m a) -> (Dom Type, Abs Type) -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> m a
yes ((Dom Type, Abs Type) -> m a)
-> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
-> ((Dom Type, Abs Type), (Term, Term))
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
forall a b. (a, b) -> a
fst)
    (Blocked Type -> m a
no (Blocked Type -> m a) -> (Type -> Blocked Type) -> Type -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotBlocked -> Type -> Blocked Type
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
-> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPathB = ((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
-> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
 -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
-> (Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
-> Type
-> (Blocked Type -> m a)
-> (Dom Type -> Abs Type -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
forall (m :: * -> *) a.
PureTCM m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> 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
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiOrPathB Type
t Dom Type -> Abs Type -> m a
yes Blocked Type -> m a
no = Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
forall (m :: * -> *) a.
MonadReduce m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiTypeB Type
t
  (\Dom Type
a Abs Type
b -> Dom Type -> Abs Type -> m a
yes Dom Type
a Abs Type
b)
  (\Blocked Type
bt -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> (((Dom Type, Abs Type), (Term, Term)) -> m a)
-> (Type -> 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 -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Blocked Type -> Type
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
bt))
    ((Dom Type -> Abs Type -> m a) -> (Dom Type, Abs Type) -> m a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> m a
yes ((Dom Type, Abs Type) -> m a)
-> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
-> ((Dom Type, Abs Type), (Term, Term))
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
forall a b. (a, b) -> a
fst)
    (Blocked Type -> m a
no (Blocked Type -> m a) -> (Type -> Blocked Type) -> Type -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Type
bt Blocked Type -> Type -> Blocked Type
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
-> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiOrPathB = ((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
-> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
 -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
-> (Type
    -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a)
-> Type
-> (Blocked Type -> m a)
-> (Dom Type -> Abs Type -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
forall (m :: * -> *) a.
PureTCM m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiOrPathB

telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns :: forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns = (forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a])
-> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
forall a.
DeBruijn a =>
(forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a])
-> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' Tele (Dom Type) -> [NamedArg a]
forall a. DeBruijn a => Tele (Dom Type) -> [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) -> [NamedArg a])
-> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
tel (Boundary []) = Tele (Dom Type) -> [NamedArg (Pattern' a)]
forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
tel
telePatterns' forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
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) -> [Arg (Named NamedName a)]
forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
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 -> m (Dom Type, Abs Type)
mustBePi Type
t = Type
-> (Type -> m (Dom Type, Abs Type))
-> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
-> m (Dom Type, Abs Type)
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
t Type -> m (Dom Type, Abs Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Dom Type -> Abs Type -> m (Dom Type, Abs Type))
 -> m (Dom Type, Abs Type))
-> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
-> m (Dom Type, Abs Type)
forall a b. (a -> b) -> a -> b
$ ((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
-> Dom Type -> Abs Type -> m (Dom Type, Abs Type)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
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 -> Abs Type -> m a) -> (Term -> m a) -> m a
ifPi Term
t Dom Type -> Abs Type -> m a
yes Term -> m a
no = Term
-> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
ifPiB Term
t Dom Type -> Abs Type -> 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 -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
ifPiB Term
t Dom Type -> Abs Type -> 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
a Abs Type
b -> Dom Type -> Abs Type -> m a
yes Dom Type
a Abs Type
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
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiTypeB (El Sort' Term
s Term
t) Dom Type -> Abs Type -> m a
yes Blocked Type -> m a
no = Term
-> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term
-> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
ifPiB Term
t Dom Type -> Abs Type -> m a
yes (\Blocked Term
bt -> Blocked Type -> m a
no (Blocked Type -> m a) -> Blocked Type -> m a
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Blocked Term -> Blocked Type
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 -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPiType (El Sort' Term
s Term
t) Dom Type -> Abs Type -> m a
yes Type -> m a
no = Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
ifPi Term
t Dom Type -> Abs Type -> m a
yes (Type -> m a
no (Type -> m a) -> (Term -> Type) -> Term -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort' Term -> Term -> Type
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 -> Abs Type -> m a) -> m a
ifNotPi = ((Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a)
-> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a)
 -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
-> (Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a)
-> Term
-> (Term -> m a)
-> (Dom Type -> Abs Type -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
forall (m :: * -> *) a.
MonadReduce m =>
Term -> (Dom Type -> Abs Type -> 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 -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType = ((Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a)
-> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a)
 -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a)
-> (Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a)
-> Type
-> (Type -> m a)
-> (Dom Type -> Abs Type -> m a)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Dom Type -> Abs Type -> m a) -> (Type -> 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 -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType Type
t Type -> tcm a
no Dom Type -> Abs Type -> tcm a
yes = do
  Type -> (Dom Type -> Abs Type -> tcm a) -> (Type -> tcm a) -> tcm a
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
ifPiType Type
t Dom Type -> Abs Type -> tcm a
yes (\ Type
t -> (((Dom Type, Abs Type), (Term, Term)) -> tcm a)
-> (Type -> tcm a)
-> Either ((Dom Type, Abs Type), (Term, Term)) Type
-> tcm a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Dom Type -> Abs Type -> tcm a) -> (Dom Type, Abs Type) -> tcm a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> tcm a
yes ((Dom Type, Abs Type) -> tcm a)
-> (((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type))
-> ((Dom Type, Abs Type), (Term, Term))
-> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dom Type, Abs Type), (Term, Term)) -> (Dom Type, Abs Type)
forall a b. (a, b) -> a
fst) (tcm a -> Type -> tcm a
forall a b. a -> b -> a
const (tcm a -> Type -> tcm a) -> tcm a -> Type -> tcm a
forall a b. (a -> b) -> a -> b
$ Type -> tcm a
no Type
t) (Either ((Dom Type, Abs Type), (Term, Term)) Type -> tcm a)
-> tcm (Either ((Dom Type, Abs Type), (Term, Term)) Type) -> tcm a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (tcm (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf tcm (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> tcm Type
-> tcm (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. tcm (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> tcm Type
forall a. a -> tcm a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t))

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

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

shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
shouldBePiOrPath :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type)
shouldBePiOrPath Type
t = Type
-> (Dom Type -> Abs Type -> m (Dom Type, Abs Type))
-> (Blocked Type -> m (Dom Type, Abs Type))
-> m (Dom Type, Abs Type)
forall (m :: * -> *) a.
PureTCM m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiOrPathB Type
t
  (((Dom Type, Abs Type) -> m (Dom Type, Abs Type))
-> Dom Type -> Abs Type -> m (Dom Type, Abs Type)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)
  (Blocked Type -> m Type
forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked (Blocked Type -> m Type)
-> (Type -> m (Dom Type, Abs Type))
-> Blocked Type
-> m (Dom Type, Abs Type)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    El Sort' Term
_ Dummy{} -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__, ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
"x" Type
HasCallStack => Type
__DUMMY_TYPE__)
    Type
t -> TypeError -> m (Dom Type, Abs Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m (Dom Type, Abs Type))
-> TypeError -> m (Dom Type, Abs Type)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
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 -> a -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
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 -> m Type
piApplyM' m Empty
err Type
t Term
v = Type
-> (Type -> m Type) -> (Dom Type -> Abs Type -> m Type) -> m Type
forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType Type
t (\Type
_ -> Empty -> Type
forall a. Empty -> a
absurd (Empty -> Type) -> m Empty -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Empty
err) {-else-} ((Dom Type -> Abs Type -> m Type) -> m Type)
-> (Dom Type -> Abs Type -> m Type) -> m Type
forall a b. (a -> b) -> a -> b
$ \ Dom Type
_ Abs Type
b -> Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
SubstArg Type
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 -> Arg a -> m Type
piApplyM' m Empty
err Type
t = m Empty -> Type -> a -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t (a -> m Type) -> (Arg a -> a) -> Arg a -> m Type
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 -> Named n a -> m Type
piApplyM' m Empty
err Type
t = m Empty -> Type -> a -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t (a -> m Type) -> (Named n a -> a) -> Named n a -> m Type
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 -> [a] -> m Type
piApplyM' m Empty
err Type
t = (m Type -> a -> m Type) -> m Type -> [a] -> m Type
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
mt a
v -> m Type
mt m Type -> (Type -> m Type) -> m Type
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type
t -> (m Empty -> Type -> a -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t a
v)) (Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t)


-- | Compute type arity

typeArity :: Type -> TCM Nat
typeArity :: Type -> TCM Int
typeArity Type
t = do
  TelV tel _ <- Type -> TCM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m TelView
telView Type
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) -> m b -> m b)
-> m b -> Tele (Dom Type) -> m b
foldrTelescopeM Dom (ArgName, Type) -> m b -> m b
f m b
b = Tele (Dom Type) -> m b
go
  where
    go :: Tele (Dom Type) -> m b
go Tele (Dom Type)
EmptyTel = m b
b
    go (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) =
      Dom (ArgName, Type) -> m b -> m b
f ((Abs (Tele (Dom Type)) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Tele (Dom Type))
tel,) (Type -> (ArgName, Type)) -> Dom Type -> Dom (ArgName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a) (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ Dom Type
-> Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> m b) -> m b
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
a Abs (Tele (Dom Type))
tel Tele (Dom Type) -> m b
go