{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Telescope where

import Prelude hiding (null)

import Control.Monad

import Data.Bifunctor (first)
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 -> Context
flattenContext = Int -> Context -> Context -> Context
forall {a}. Subst a => Int -> [a] -> [a] -> [a]
loop Int
1 []
  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 dependeny 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 {a} {b} {a} {t} {t}.
Free a =>
(Int, b) -> (a, Dom' t (Type'' t a)) -> 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 a)) -> Bool
`comesBefore` (a
_, Dom' t (Type'' t a)
a) = Int
i Int -> a -> Bool
forall a. Free a => Int -> a -> Bool
`freeIn` Type'' t a -> a
forall t a. Type'' t a -> a
unEl (Dom' t (Type'' t a) -> Type'' t a
forall t e. Dom' t e -> e
unDom Dom' t (Type'' t a)
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 descending order.
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 descending order.
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. 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!
--     renaming _ (flipP perm) = [error, var 1, var 0]  -- The correct renaming!
--     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
flipP 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
allFreeVars 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 Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar Any -> IgnoreSorts -> Dom Type -> Any
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> Any
Any (Bool -> Any) -> (Int -> Bool) -> SingleVar Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> VarSet -> Bool
`VarSet.member` VarSet
work)) IgnoreSorts
IgnoreNot 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 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 a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- [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]
        -- Skip the construction of intermediate @IntSet@s in the check @ok@.
        -- ok  = (allFreeVars t `IntSet.intersection` IntSet.fromAscList [ 0 .. n-1 ])
        --       `IntSet.isSubsetOf` soFar
        good :: Int -> All
good Int
i = Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ (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 = All -> Bool
getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> All) -> IgnoreSorts -> Dom Type -> All
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Int -> All
good IgnoreSorts
IgnoreNot 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 a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- [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)         -- Γ  ⊢ flipP ρ : Γ'
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
rho)
  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
    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 $ allFreeVars 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
allFreeVars 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 -> [Int] -> [Int]
forall a. Eq a => a -> [a] -> [a]
List.delete Int
j ([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

    -- 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 -> [Int] -> Permutation
Perm Int
n ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$ [Int]
is    -- works on de Bruijn indices
    rho :: Permutation
rho   = Permutation -> Permutation
reverseP Permutation
perm  -- works on de Bruijn levels

    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'
    us :: [Pattern' DBPatVar]
us    = (Int -> Pattern' DBPatVar) -> [Int] -> [Pattern' DBPatVar]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Pattern' DBPatVar
-> (Int -> Pattern' DBPatVar) -> Maybe Int -> Pattern' DBPatVar
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pattern' DBPatVar
p1 Int -> Pattern' DBPatVar
forall a. DeBruijn a => Int -> a
deBruijnVar (Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
is)) [ Int
0 .. Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1 ]
    sigma :: PatternSubstitution
sigma = [Pattern' DBPatVar]
us [Pattern' DBPatVar] -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Int -> PatternSubstitution
forall a. Int -> Substitution' a
raiseS (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

    ts1 :: [Dom Type]
ts1   = Permutation -> [Dom Type] -> [Dom Type]
forall a. Permutation -> [a] -> [a]
permute Permutation
rho ([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
rho [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