module Agda.TypeChecking.Telescope where

import Prelude hiding (null)

import Control.Monad

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

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

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

import Agda.Utils.CallStack ( withCallerCallStack )
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 :: TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel :: Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom a)
EmptyTel          = []
flattenTel (ExtendTel Dom a
a Abs (Tele (Dom a))
tel) = Nat -> Dom a -> Dom a
forall a. Subst a => Nat -> a -> a
raise (Abs (Tele (Dom a)) -> Nat
forall a. Sized a => a -> Nat
size Abs (Tele (Dom a))
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) Dom a
a Dom a -> [Dom a] -> [Dom a]
forall a. a -> [a] -> [a]
: Tele (Dom a) -> [Dom a]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom a))
tel)

{-# SPECIALIZE flattenTel :: Telescope -> [Dom Type] #-}

-- | 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 = ((Nat, Dom Type) -> (Nat, Dom Type) -> Bool)
-> [(Nat, Dom Type)] -> Maybe Permutation
forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
topoSort (Nat, Dom Type) -> (Nat, Dom Type) -> Bool
forall a b a t t.
Free a =>
(Nat, b) -> (a, Dom' t (Type'' t a)) -> Bool
comesBefore [(Nat, Dom Type)]
tel'
  where
    tel' :: [(Nat, Dom Type)]
tel' = [Nat] -> [Dom Type] -> [(Nat, Dom Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat -> [Nat]) -> Nat -> [Nat]
forall a b. (a -> b) -> a -> b
$ [Dom Type] -> Nat
forall a. Sized a => a -> Nat
size [Dom Type]
tel) [Dom Type]
tel
    (Nat
i, b
_) comesBefore :: (Nat, b) -> (a, Dom' t (Type'' t a)) -> Bool
`comesBefore` (a
_, Dom' t (Type'' t a)
a) = Nat
i Nat -> a -> Bool
forall a. Free a => Nat -> 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] -> Telescope
unflattenTel []   []            = Telescope
forall a. Tele a
EmptyTel
unflattenTel (ArgName
x : [ArgName]
xs) (Dom Type
a : [Dom Type]
tel) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a' (ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs ArgName
x Telescope
tel')
  where
    tel' :: Telescope
tel' = [ArgName] -> [Dom Type] -> Telescope
unflattenTel [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 (Nat -> Term -> [Term]
forall a. Nat -> a -> [a]
replicate ([Dom Type] -> Nat
forall a. Sized a => a -> Nat
size [Dom Type]
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) ((CallStack -> Term) -> Term
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Term
impossibleTerm))
unflattenTel [] (Dom Type
_ : [Dom Type]
_) = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
unflattenTel (ArgName
_ : [ArgName]
_) [] = Telescope
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] -> Telescope -> Telescope
renameTel []           Telescope
EmptyTel           = Telescope
forall a. Tele a
EmptyTel
renameTel (Maybe ArgName
Nothing:[Maybe ArgName]
xs) (ExtendTel Dom Type
a Abs Telescope
tel') = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName] -> Telescope -> Telescope
renameTel [Maybe ArgName]
xs (Telescope -> Telescope) -> Abs Telescope -> Abs Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Telescope
tel'
renameTel (Just ArgName
x :[Maybe ArgName]
xs) (ExtendTel Dom Type
a Abs Telescope
tel') = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName] -> Telescope -> Telescope
renameTel [Maybe ArgName]
xs (Telescope -> Telescope) -> Abs Telescope -> Abs Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Abs Telescope
tel' { absName :: ArgName
absName = ArgName
x })
renameTel []           (ExtendTel Dom Type
_ Abs Telescope
_   ) = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
renameTel (Maybe ArgName
_      :[Maybe ArgName]
_ ) Telescope
EmptyTel           = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__

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

teleArgNames :: Telescope -> [Arg ArgName]
teleArgNames :: Telescope -> [Arg ArgName]
teleArgNames = (Dom' Term (ArgName, Type) -> Arg ArgName)
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term ArgName -> Arg ArgName
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term ArgName -> Arg ArgName)
-> (Dom' Term (ArgName, Type) -> Dom' Term ArgName)
-> Dom' Term (ArgName, Type)
-> Arg ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ArgName, Type) -> ArgName)
-> Dom' Term (ArgName, Type) -> Dom' Term ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst) ([Dom' Term (ArgName, Type)] -> [Arg ArgName])
-> (Telescope -> [Dom' Term (ArgName, Type)])
-> Telescope
-> [Arg ArgName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList

teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
teleArgs :: 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

teleDoms :: (DeBruijn a) => Tele (Dom t) -> [Dom a]
teleDoms :: Tele (Dom t) -> [Dom a]
teleDoms Tele (Dom t)
tel = (Nat -> Dom' Term (ArgName, t) -> Dom a)
-> [Nat] -> [Dom' Term (ArgName, t)] -> [Dom a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Nat
i Dom' Term (ArgName, t)
dom -> Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
i a -> Dom' Term (ArgName, t) -> Dom a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom' Term (ArgName, t)
dom) (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat -> [Nat]) -> Nat -> [Nat]
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, t)] -> Nat
forall a. Sized a => a -> Nat
size [Dom' Term (ArgName, t)]
l) [Dom' Term (ArgName, t)]
l
  where l :: [Dom' Term (ArgName, t)]
l = Tele (Dom t) -> [Dom' Term (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) => Telescope -> [NamedArg a]
teleNamedArgs :: Telescope -> [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])
-> (Telescope -> [Dom' Term a]) -> Telescope -> [NamedArg a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Dom' Term a]
forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
teleDoms

-- | 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 :: Telescope -> Telescope -> [NamedArg a]
tele2NamedArgs Telescope
tel0 Telescope
tel =
  [ ArgInfo -> Named (WithOrigin (Ranged ArgName)) a -> NamedArg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Maybe (WithOrigin (Ranged ArgName))
-> a -> Named (WithOrigin (Ranged ArgName)) a
forall name a. Maybe name -> a -> Named name a
Named (WithOrigin (Ranged ArgName) -> Maybe (WithOrigin (Ranged ArgName))
forall a. a -> Maybe a
Just (WithOrigin (Ranged ArgName)
 -> Maybe (WithOrigin (Ranged ArgName)))
-> WithOrigin (Ranged ArgName)
-> Maybe (WithOrigin (Ranged ArgName))
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged ArgName -> WithOrigin (Ranged ArgName)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged ArgName -> WithOrigin (Ranged ArgName))
-> Ranged ArgName -> WithOrigin (Ranged ArgName)
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 -> Nat -> a
forall a. DeBruijn a => ArgName -> Nat -> a
debruijnNamedVar ArgName
varName Nat
i))
  | (Nat
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
_)}) <- [Nat]
-> [Dom' Term (ArgName, Type)]
-> [Dom' Term (ArgName, Type)]
-> [(Nat, Dom' Term (ArgName, Type), Dom' Term (ArgName, Type))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat -> [Nat]) -> Nat -> [Nat]
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)] -> Nat
forall a. Sized a => a -> Nat
size [Dom' Term (ArgName, Type)]
l) [Dom' Term (ArgName, Type)]
l0 [Dom' Term (ArgName, Type)]
l ]
  where
  l :: [Dom' Term (ArgName, Type)]
l  = Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
  l0 :: [Dom' Term (ArgName, Type)]
l0 = Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0

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

-- | Recursively computes dependencies of a set of variables in a given
--   telescope. Any dependencies outside of the telescope are ignored.
varDependencies :: Telescope -> IntSet -> IntSet
varDependencies :: Telescope -> IntSet -> IntSet
varDependencies Telescope
tel = IntSet -> IntSet
addLocks (IntSet -> IntSet) -> (IntSet -> IntSet) -> IntSet -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> IntSet -> IntSet
allDependencies IntSet
IntSet.empty
  where
    addLocks :: IntSet -> IntSet
addLocks IntSet
s | IntSet -> Bool
IntSet.null IntSet
s = IntSet
s
               | Bool
otherwise = IntSet -> IntSet -> IntSet
IntSet.union IntSet
s (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ [Nat] -> IntSet
IntSet.fromList ([Nat] -> IntSet) -> [Nat] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Nat -> Bool) -> [Nat] -> [Nat]
forall a. (a -> Bool) -> [a] -> [a]
filter (Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
m) [Nat]
locks
      where
        locks :: [Nat]
locks = [Maybe Nat] -> [Nat]
forall a. [Maybe a] -> [a]
catMaybes [ Term -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) | (Arg Term
a :: Arg Term) <- Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel, Arg Term -> Lock
forall a. LensLock a => a -> Lock
getLock Arg Term
a Lock -> Lock -> Bool
forall a. Eq a => a -> a -> Bool
== Lock
IsLock]
        m :: Nat
m = IntSet -> Nat
IntSet.findMin IntSet
s
    n :: Nat
n  = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel
    ts :: [Dom Type]
ts = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel

    directDependencies :: Int -> IntSet
    directDependencies :: Nat -> IntSet
directDependencies Nat
i = Dom Type -> IntSet
forall t. Free t => t -> IntSet
allFreeVars (Dom Type -> IntSet) -> Dom Type -> IntSet
forall a b. (a -> b) -> a -> b
$ Dom Type -> [Dom Type] -> Nat -> Dom Type
forall a. a -> [a] -> Nat -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
i)

    allDependencies :: IntSet -> IntSet -> IntSet
    allDependencies :: IntSet -> IntSet -> IntSet
allDependencies =
      (Nat -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet
forall b. (Nat -> b -> b) -> b -> IntSet -> b
IntSet.foldr ((Nat -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet)
-> (Nat -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ \Nat
j IntSet
soFar ->
        if Nat
j Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
n Bool -> Bool -> Bool
|| Nat
j Nat -> IntSet -> Bool
`IntSet.member` IntSet
soFar
        then IntSet
soFar
        else Nat -> IntSet -> IntSet
IntSet.insert Nat
j (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> IntSet
allDependencies IntSet
soFar (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Nat -> IntSet
directDependencies Nat
j

-- | 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.
varDependents :: Telescope -> IntSet -> IntSet
varDependents :: Telescope -> IntSet -> IntSet
varDependents Telescope
tel = IntSet -> IntSet
allDependents
  where
    n :: Nat
n  = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel
    ts :: [Dom Type]
ts = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel

    directDependents :: IntSet -> IntSet
    directDependents :: IntSet -> IntSet
directDependents IntSet
is = [Nat] -> IntSet
IntSet.fromList
      [ Nat
j | Nat
j <- Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n
          , let tj :: Dom Type
tj = Dom Type -> [Dom Type] -> Nat -> Dom Type
forall a. a -> [a] -> Nat -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
j)
          , 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) -> (Nat -> Bool) -> SingleVar Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat -> IntSet -> Bool
`IntSet.member` IntSet
is)) IgnoreSorts
IgnoreNot Dom Type
tj
          ]

    allDependents :: IntSet -> IntSet
    allDependents :: IntSet -> IntSet
allDependents IntSet
is
     | IntSet -> Bool
forall a. Null a => a -> Bool
null IntSet
new  = IntSet
forall a. Null a => a
empty
     | Bool
otherwise = IntSet
new IntSet -> IntSet -> IntSet
`IntSet.union` IntSet -> IntSet
allDependents IntSet
new
      where new :: IntSet
new = IntSet -> IntSet
directDependents IntSet
is

-- | A telescope split in two.
data SplitTel = SplitTel
  { SplitTel -> Telescope
firstPart  :: Telescope
  , SplitTel -> Telescope
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 :: IntSet -> Telescope -> SplitTel
splitTelescope IntSet
fv Telescope
tel = Telescope -> Telescope -> Permutation -> SplitTel
SplitTel Telescope
tel1 Telescope
tel2 Permutation
perm
  where
    names :: [ArgName]
names = Telescope -> [ArgName]
teleNames Telescope
tel
    ts0 :: [Dom Type]
ts0   = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
    n :: Nat
n     = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel

    is :: IntSet
is    = Telescope -> IntSet -> IntSet
varDependencies Telescope
tel IntSet
fv
    isC :: IntSet
isC   = [Nat] -> IntSet
IntSet.fromList [Nat
0..(Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1)] IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is

    perm :: Permutation
perm  = Nat -> [Nat] -> Permutation
Perm Nat
n ([Nat] -> Permutation) -> [Nat] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Nat -> Nat) -> [Nat] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-) ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ IntSet -> [Nat]
VarSet.toDescList IntSet
is [Nat] -> [Nat] -> [Nat]
forall a. [a] -> [a] -> [a]
++ IntSet -> [Nat]
VarSet.toDescList IntSet
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' :: Telescope
tel'  = [ArgName] -> [Dom Type] -> Telescope
unflattenTel (Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [ArgName]
names) [Dom Type]
ts1

    m :: Nat
m     = IntSet -> Nat
forall a. Sized a => a -> Nat
size IntSet
is
    (Telescope
tel1, Telescope
tel2) = [Dom' Term (ArgName, Type)] -> Telescope
telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
-> ([Dom' Term (ArgName, Type)] -> Telescope)
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> (Telescope, Telescope)
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- [Dom' Term (ArgName, Type)] -> Telescope
telFromList (([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
 -> (Telescope, Telescope))
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> (Telescope, Telescope)
forall a b. (a -> b) -> a -> b
$ Nat
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
m ([Dom' Term (ArgName, Type)]
 -> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)]))
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
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 :: [Nat] -> Telescope -> Maybe SplitTel
splitTelescopeExact [Nat]
is Telescope
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
$> Telescope -> Telescope -> Permutation -> SplitTel
SplitTel Telescope
tel1 Telescope
tel2 Permutation
perm
  where
    names :: [ArgName]
names = Telescope -> [ArgName]
teleNames Telescope
tel
    ts0 :: [Dom Type]
ts0   = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
    n :: Nat
n     = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel

    checkDependencies :: IntSet -> [Int] -> Bool
    checkDependencies :: IntSet -> [Nat] -> Bool
checkDependencies IntSet
soFar []     = Bool
True
    checkDependencies IntSet
soFar (Nat
j:[Nat]
js) = Bool
ok Bool -> Bool -> Bool
&& IntSet -> [Nat] -> Bool
checkDependencies (Nat -> IntSet -> IntSet
IntSet.insert Nat
j IntSet
soFar) [Nat]
js
      where
        t :: Dom Type
t   = Dom Type -> [Dom Type] -> Nat -> Dom Type
forall a. a -> [a] -> Nat -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts0 (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
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 :: Nat -> All
good Nat
i = Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ (Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n) Bool -> Bool -> Bool
`implies` (Nat
i Nat -> 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
$ (Nat -> All) -> IgnoreSorts -> Dom Type -> All
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Nat -> All
good IgnoreSorts
IgnoreNot Dom Type
t

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

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

    perm :: Permutation
perm  = Nat -> [Nat] -> Permutation
Perm Nat
n ([Nat] -> Permutation) -> [Nat] -> Permutation
forall a b. (a -> b) -> a -> b
$ (Nat -> Nat) -> [Nat] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-) ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ [Nat]
is [Nat] -> [Nat] -> [Nat]
forall a. [a] -> [a] -> [a]
++ [Nat]
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' :: Telescope
tel'  = [ArgName] -> [Dom Type] -> Telescope
unflattenTel (Permutation -> [ArgName] -> [ArgName]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [ArgName]
names) [Dom Type]
ts1

    m :: Nat
m     = [Nat] -> Nat
forall a. Sized a => a -> Nat
size [Nat]
is
    (Telescope
tel1, Telescope
tel2) = [Dom' Term (ArgName, Type)] -> Telescope
telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
-> ([Dom' Term (ArgName, Type)] -> Telescope)
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> (Telescope, Telescope)
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- [Dom' Term (ArgName, Type)] -> Telescope
telFromList (([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
 -> (Telescope, Telescope))
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> (Telescope, Telescope)
forall a b. (a -> b) -> a -> b
$ Nat
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
m ([Dom' Term (ArgName, Type)]
 -> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)]))
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
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 :: Telescope
-> Nat
-> DeBruijnPattern
-> Maybe (Telescope, PatternSubstitution, Permutation)
instantiateTelescope Telescope
tel Nat
k DeBruijnPattern
p = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok Maybe ()
-> (Telescope, PatternSubstitution, Permutation)
-> Maybe (Telescope, PatternSubstitution, Permutation)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (Telescope
tel', PatternSubstitution
sigma, Permutation
rho)
  where
    names :: [ArgName]
names = Telescope -> [ArgName]
teleNames Telescope
tel
    ts0 :: [Dom Type]
ts0   = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
    n :: Nat
n     = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel
    j :: Nat
j     = Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
k
    u :: Term
u     = DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
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 :: IntSet
is0   = Telescope -> IntSet -> IntSet
varDependencies Telescope
tel (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Term -> IntSet
forall t. Free t => t -> IntSet
allFreeVars Term
u
    -- is1 is the part of Γ that depends on variable j
    is1 :: IntSet
is1   = Telescope -> IntSet -> IntSet
varDependents Telescope
tel (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Nat -> IntSet
forall el coll. Singleton el coll => el -> coll
singleton Nat
j
    -- lasti is the last (rightmost) variable of is0
    lasti :: Nat
lasti = if IntSet -> Bool
forall a. Null a => a -> Bool
null IntSet
is0 then Nat
n else IntSet -> Nat
IntSet.findMin IntSet
is0
    -- we move each variable in is1 to the right until it comes after
    -- all variables in is0 (i.e. after lasti)
    ([Nat]
as,[Nat]
bs) = (Nat -> Bool) -> [Nat] -> ([Nat], [Nat])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Nat -> IntSet -> Bool
`IntSet.member` IntSet
is1) [ Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1 , Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
2 .. Nat
lasti ]
    is :: [Nat]
is    = [Nat] -> [Nat]
forall a. [a] -> [a]
reverse ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat] -> [Nat]
forall a. Eq a => a -> [a] -> [a]
List.delete Nat
j ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ [Nat]
bs [Nat] -> [Nat] -> [Nat]
forall a. [a] -> [a] -> [a]
++ [Nat]
as [Nat] -> [Nat] -> [Nat]
forall a. [a] -> [a] -> [a]
++ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
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
$ Nat
j Nat -> IntSet -> Bool
`IntSet.member` IntSet
is0

    perm :: Permutation
perm  = Nat -> [Nat] -> Permutation
Perm Nat
n ([Nat] -> Permutation) -> [Nat] -> Permutation
forall a b. (a -> b) -> a -> b
$ [Nat]
is    -- works on de Bruijn indices
    rho :: Permutation
rho   = Permutation -> Permutation
reverseP Permutation
perm  -- works on de Bruijn levels

    p1 :: DeBruijnPattern
p1    = Impossible -> Permutation -> DeBruijnPattern -> DeBruijnPattern
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible Permutation
perm DeBruijnPattern
p -- Γ' ⊢ p1 : A'
    us :: [DeBruijnPattern]
us    = (Nat -> DeBruijnPattern) -> [Nat] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (\Nat
i -> DeBruijnPattern
-> (Nat -> DeBruijnPattern) -> Maybe Nat -> DeBruijnPattern
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DeBruijnPattern
p1 Nat -> DeBruijnPattern
forall a. DeBruijn a => Nat -> a
deBruijnVar (Nat -> [Nat] -> Maybe Nat
forall a. Eq a => a -> [a] -> Maybe Nat
List.elemIndex Nat
i [Nat]
is)) [ Nat
0 .. Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1 ]
    sigma :: PatternSubstitution
sigma = [DeBruijnPattern]
us [DeBruijnPattern] -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Nat -> PatternSubstitution
forall a. Nat -> Substitution' a
raiseS (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
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' :: Telescope
tel'  = [ArgName] -> [Dom Type] -> Telescope
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 :: Telescope
-> Nat -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
expandTelescopeVar Telescope
gamma Nat
k Telescope
delta ConHead
c = (Telescope
tel', PatternSubstitution
rho)
  where
    ([Dom' Term (ArgName, Type)]
ts1,Dom' Term (ArgName, Type)
xa:[Dom' Term (ArgName, Type)]
ts2) = ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> Maybe ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a. a -> Maybe a -> a
fromMaybe ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
 -> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)]))
-> Maybe ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$
                    Nat
-> [Dom' Term (ArgName, Type)]
-> Maybe ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Nat
k ([Dom' Term (ArgName, Type)]
 -> Maybe
      ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)]))
-> [Dom' Term (ArgName, Type)]
-> Maybe ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma
    a :: Dom Type
a = Nat -> Dom Type -> Dom Type
forall a. Subst a => Nat -> a -> a
raise (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
delta) ((ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type) -> Dom' Term (ArgName, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (ArgName, Type)
xa) -- Γ₁Δ ⊢ D pars

    cpi :: ConPatternInfo
cpi         = ConPatternInfo :: PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
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 DeBruijnPattern]
cargs       = (NamedArg DeBruijnPattern -> NamedArg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> NamedArg DeBruijnPattern -> NamedArg DeBruijnPattern
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
delta
    cdelta :: DeBruijnPattern
cdelta      = ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
cargs                    -- Γ₁Δ ⊢ c Δ : D pars
    rho0 :: PatternSubstitution
rho0        = DeBruijnPattern -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
cdelta (PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution -> PatternSubstitution
forall a b. (a -> b) -> a -> b
$ Nat -> PatternSubstitution
forall a. Nat -> Substitution' a
raiseS (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
delta)  -- Γ₁Δ ⊢ ρ₀ : Γ₁(x : D pars)
    rho :: PatternSubstitution
rho         = Nat -> PatternSubstitution -> PatternSubstitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS ([Dom' Term (ArgName, Type)] -> Nat
forall a. Sized a => a -> Nat
size [Dom' Term (ArgName, Type)]
ts2) PatternSubstitution
rho0               -- Γ₁ΔΓ₂ρ₀ ⊢ ρ : Γ₁(x : D pars)Γ₂

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

    tel' :: Telescope
tel'        = Telescope
gamma1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` (Telescope
delta Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma2')

-- | Gather leading Πs of a type in a telescope.
telView :: (MonadReduce m, MonadAddContext m) => Type -> m TelView
telView :: Type -> m TelView
telView = Nat -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> Type -> m TelView
telViewUpTo (-Nat
1)

-- | @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 :: Nat -> Type -> m TelView
telViewUpTo Nat
n Type
t = Nat -> (Dom Type -> Bool) -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Nat
n (Bool -> Dom Type -> Bool
forall a b. a -> b -> a
const Bool
True) Type
t

-- | @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' :: Nat -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Nat
0 Dom Type -> Bool
p Type
t = TelView -> m TelView
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
telViewUpTo' Nat
n Dom Type -> Bool
p Type
t = do
  Type
t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Pi Dom Type
a Abs Type
b | Dom Type -> Bool
p Dom Type
a -> 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
<$> 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 -> Nat -> (Dom Type -> Bool) -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Dom Type -> Bool
p Type
b
    Term
_            -> TelView -> m TelView
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
  where
    absV :: Dom a -> ArgName -> TelV a -> TelV a
absV Dom a
a ArgName
x (TelV Tele (Dom a)
tel a
t) = Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom a
a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom a)
tel)) a
t

telViewPath :: PureTCM m => Type -> m TelView
telViewPath :: Type -> m TelView
telViewPath = Nat -> Type -> m TelView
forall (m :: * -> *). PureTCM m => Nat -> Type -> m TelView
telViewUpToPath (-Nat
1)

-- | @telViewUpToPath n t@ takes off $t$
--   the first @n@ (or arbitrary many if @n < 0@) function domains or Path types.
telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
telViewUpToPath :: Nat -> Type -> m TelView
telViewUpToPath Nat
0 Type
t = TelView -> m TelView
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
telViewUpToPath Nat
n Type
t = do
  Either (Dom Type, Abs Type) Type
vt <- Type -> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi (Type -> m (Either (Dom Type, Abs Type) Type))
-> Type -> m (Either (Dom Type, Abs Type) Type)
forall a b. (a -> b) -> a -> b
$ Type
t
  case Either (Dom Type, Abs Type) Type
vt of
    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) -> m TelView -> m TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> Type -> m TelView
forall (m :: * -> *). PureTCM m => Nat -> Type -> m TelView
telViewUpToPath (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right (El Sort' Term
_ Term
t) | Pi Dom Type
a Abs Type
b <- Term
t
                   -> 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
<$> Nat -> Type -> m TelView
forall (m :: * -> *). PureTCM m => Nat -> Type -> m TelView
telViewUpToPath (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right Type
t        -> TelView -> m TelView
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
  where
    absV :: Dom a -> ArgName -> TelV a -> TelV a
absV Dom a
a ArgName
x (TelV Tele (Dom a)
tel a
t) = Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom a
a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom a)
tel)) a
t

-- | [[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y]
type Boundary = Boundary' (Term,Term)
type Boundary' a = [(Term,a)]

-- | 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@.
telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView,Boundary)
telViewUpToPathBoundary' :: Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' Nat
0 Type
t = (TelView, Boundary) -> m (TelView, Boundary)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TelView, Boundary) -> m (TelView, Boundary))
-> (TelView, Boundary) -> m (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ (Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t,[])
telViewUpToPathBoundary' Nat
n Type
t = do
  Either ((Dom Type, Abs Type), (Term, Term)) Type
vt <- 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 -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type))
-> Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. (a -> b) -> a -> b
$ Type
t
  case Either ((Dom Type, Abs Type), (Term, Term)) Type
vt of
    Left ((Dom Type
a,Abs Type
b),(Term, Term)
xy) -> (Term, Term) -> (TelView, Boundary) -> (TelView, Boundary)
forall b a.
Subst b =>
b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
addEndPoints (Term, Term)
xy ((TelView, Boundary) -> (TelView, Boundary))
-> ((TelView, Boundary) -> (TelView, Boundary))
-> (TelView, Boundary)
-> (TelView, Boundary)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> ArgName -> (TelView, Boundary) -> (TelView, Boundary)
forall a b. Dom a -> ArgName -> (TelV a, b) -> (TelV a, b)
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
<$> Nat -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right (El Sort' Term
_ Term
t) | Pi Dom Type
a Abs Type
b <- Term
t
                   -> Dom Type -> ArgName -> (TelView, Boundary) -> (TelView, Boundary)
forall a b. Dom a -> ArgName -> (TelV a, b) -> (TelV a, b)
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
<$> Nat -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right Type
t        -> (TelView, Boundary) -> m (TelView, Boundary)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TelView, Boundary) -> m (TelView, Boundary))
-> (TelView, Boundary) -> m (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ (Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t,[])
  where
    absV :: Dom a -> ArgName -> (TelV a, b) -> (TelV a, b)
absV Dom a
a ArgName
x (TelV Tele (Dom a)
tel a
t, b
cs) = (Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom a
a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom a)
tel)) a
t, b
cs)
    addEndPoints :: b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
addEndPoints b
xy (telv :: TelV a
telv@(TelV Tele (Dom a)
tel a
_),[(Term, b)]
cs) = (TelV a
telv, (Nat -> Term
var (Nat -> Term) -> Nat -> Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom a) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom a)
tel Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1, b
xyInTel)(Term, b) -> [(Term, b)] -> [(Term, b)]
forall a. a -> [a] -> [a]
:[(Term, b)]
cs)
      where
       xyInTel :: b
xyInTel = Nat -> b -> b
forall a. Subst a => Nat -> a -> a
raise (Tele (Dom a) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom a)
tel) b
xy


fullBoundary :: Telescope -> Boundary -> Boundary
fullBoundary :: Telescope -> Boundary -> Boundary
fullBoundary Telescope
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' Term]
es = Telescope -> Boundary -> [Elim' Term]
forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
teleElims Telescope
tel Boundary
bs
       l :: Nat
l  = Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel
   in ((Term, (Term, Term)) -> (Term, (Term, Term)))
-> Boundary -> Boundary
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: Term
t@(Var Nat
i []), (Term, Term)
xy) -> (Term
t, (Term, Term)
xy (Term, Term) -> [Elim' Term] -> (Term, Term)
forall t. Apply t => t -> [Elim' Term] -> t
`applyE` (Nat -> [Elim' Term] -> [Elim' Term]
forall a. Nat -> [a] -> [a]
drop (Nat
l Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
i) [Elim' Term]
es))) Boundary
bs

-- | @(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 :: Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary Nat
i Type
a = do
   (telv :: TelView
telv@(TelV Telescope
tel Type
b), Boundary
bs) <- Nat -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' Nat
i Type
a
   (TelView, Boundary) -> m (TelView, Boundary)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TelView, Boundary) -> m (TelView, Boundary))
-> (TelView, Boundary) -> m (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ (TelView
telv, Telescope -> Boundary -> Boundary
fullBoundary Telescope
tel Boundary
bs)

-- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundaryP 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 Γ.
telViewUpToPathBoundaryP :: PureTCM m => Int -> Type -> m (TelView,Boundary)
telViewUpToPathBoundaryP :: Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP = Nat -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary'

telViewPathBoundaryP :: PureTCM m => Type -> m (TelView,Boundary)
telViewPathBoundaryP :: Type -> m (TelView, Boundary)
telViewPathBoundaryP = Nat -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP (-Nat
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' (a,a) -> [Elim' a]
teleElims :: Telescope -> Boundary' (a, a) -> [Elim' a]
teleElims Telescope
tel [] = (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
$ Telescope -> [Arg a]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
teleElims Telescope
tel Boundary' (a, a)
boundary = [Arg a] -> [Elim' a]
recurse (Telescope -> [Arg a]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel)
  where
    recurse :: [Arg a] -> [Elim' a]
recurse = (Arg a -> Elim' a) -> [Arg a] -> [Elim' a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg a -> Elim' a
updateArg
    matchVar :: Nat -> Maybe (a, a)
matchVar Nat
x =
      (Term, (a, a)) -> (a, a)
forall a b. (a, b) -> b
snd ((Term, (a, a)) -> (a, a)) -> Maybe (Term, (a, a)) -> Maybe (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term, (a, a)) -> Bool)
-> Boundary' (a, a) -> Maybe (Term, (a, a))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\case
        (Var Nat
i [],(a, a)
_) -> Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
x
        (Term, (a, a))
_            -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__) Boundary' (a, a)
boundary
    updateArg :: Arg a -> Elim' a
updateArg a :: Arg a
a@(Arg ArgInfo
info a
p) =
      case a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView a
p of
        Just Nat
i | Just (a
t,a
u) <- Nat -> Maybe (a, a)
matchVar Nat
i -> a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
t a
u a
p
        Maybe Nat
_                                 -> Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply Arg a
a

pathViewAsPi
  :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi :: 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

pathViewAsPi'
  :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term,Term)) Type)
pathViewAsPi' :: 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 (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

pathViewAsPi'whnf
  :: (HasBuiltins m)
  => m (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type)
pathViewAsPi'whnf :: m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf = do
  Type -> PathView
view <- m (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  Maybe Term
minterval  <- ArgName -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
getBuiltin' ArgName
builtinInterval
  (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
 -> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type))
-> (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a b. (a -> b) -> a -> b
$ \ Type
t -> case Type -> PathView
view Type
t of
    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"
          i :: Type
i = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel Integer
0) Term
interval
      in
        ((Dom Type, Abs Type), (Term, Term))
-> Either ((Dom Type, Abs Type), (Term, Term)) Type
forall a b. a -> Either a b
Left (((Dom Type, Abs Type), (Term, Term))
 -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> ((Dom Type, Abs Type), (Term, Term))
-> Either ((Dom Type, Abs Type), (Term, Term)) Type
forall a b. (a -> b) -> a -> b
$ ((Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type
i, 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 (Nat -> Sort' Term -> Sort' Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 Sort' Term
s) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
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
$ Nat -> Term
var Nat
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))

    PathView
_    -> 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 :: Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath Type
t = do
  Either ((Dom Type, Abs Type), (Term, Term)) Type
t <- 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  case Either ((Dom Type, Abs Type), (Term, Term)) Type
t of
    Left ((Dom Type, Abs Type)
p,(Term, Term)
_) -> Either (Dom Type, Abs Type) Type
-> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Dom Type, Abs Type) Type
 -> m (Either (Dom Type, Abs Type) Type))
-> Either (Dom Type, Abs Type) Type
-> m (Either (Dom Type, Abs Type) Type)
forall a b. (a -> b) -> a -> b
$ (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)) -> Either (Dom Type, Abs Type) Type
-> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Dom Type, Abs Type) Type
 -> m (Either (Dom Type, Abs Type) Type))
-> Either (Dom Type, Abs Type) Type
-> m (Either (Dom Type, Abs Type) Type)
forall a b. (a -> b) -> a -> 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
t -> Either (Dom Type, Abs Type) Type
-> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Dom Type, Abs Type) Type
 -> m (Either (Dom Type, Abs Type) Type))
-> Either (Dom Type, Abs Type) Type
-> m (Either (Dom Type, Abs Type) Type)
forall a b. (a -> b) -> a -> b
$ Type -> Either (Dom Type, Abs Type) Type
forall a b. b -> Either a b
Right Type
t

telView'UpToPath :: Int -> Type -> TCM TelView
telView'UpToPath :: Nat -> Type -> TCM TelView
telView'UpToPath Nat
0 Type
t = TelView -> TCM TelView
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> TCM TelView) -> TelView -> TCM TelView
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
telView'UpToPath Nat
n Type
t = do
  Either ((Dom Type, Abs Type), (Term, Term)) Type
vt <- TCMT IO (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 TCMT IO (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> TCMT IO Type
-> TCMT IO (Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> TCMT IO Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
  case Either ((Dom Type, Abs Type), (Term, Term)) Type
vt of
    Left ((Dom Type
a,Abs Type
b),(Term, Term)
_)     -> 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
<$> Nat -> Type -> TCM TelView
forall (m :: * -> *). PureTCM m => Nat -> Type -> m TelView
telViewUpToPath (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right (El Sort' Term
_ Term
t) | Pi Dom Type
a Abs Type
b <- Term
t
                   -> 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
<$> Nat -> Type -> TCM TelView
forall (m :: * -> *). PureTCM m => Nat -> Type -> m TelView
telViewUpToPath (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right Type
t        -> TelView -> TCM TelView
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> TCM TelView) -> TelView -> TCM TelView
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
  where
    absV :: Dom a -> ArgName -> TelV a -> TelV a
absV Dom a
a ArgName
x (TelV Tele (Dom a)
tel a
t) = Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom a
a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom a)
tel)) a
t

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

isPath
  :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type))
isPath :: Type -> m (Maybe (Dom Type, Abs Type))
isPath Type
t = ((Dom Type, Abs Type) -> Maybe (Dom Type, Abs Type))
-> (Type -> Maybe (Dom Type, Abs Type))
-> Either (Dom Type, Abs Type) Type
-> Maybe (Dom Type, Abs Type)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Dom Type, Abs Type) -> Maybe (Dom Type, Abs Type)
forall a. a -> Maybe a
Just (Maybe (Dom Type, Abs Type) -> Type -> Maybe (Dom Type, Abs Type)
forall a b. a -> b -> a
const Maybe (Dom Type, Abs Type)
forall a. Maybe a
Nothing) (Either (Dom Type, Abs Type) Type -> Maybe (Dom Type, Abs Type))
-> m (Either (Dom Type, Abs Type) Type)
-> m (Maybe (Dom Type, Abs Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t

telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns :: Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns = (forall a. DeBruijn a => Telescope -> [NamedArg a])
-> Telescope -> Boundary -> [NamedArg (Pattern' a)]
forall a.
DeBruijn a =>
(forall a. DeBruijn a => Telescope -> [NamedArg a])
-> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs

telePatterns' :: DeBruijn a =>
                (forall a. (DeBruijn a) => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' :: (forall a. DeBruijn a => Telescope -> [NamedArg a])
-> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' forall a. DeBruijn a => Telescope -> [NamedArg a]
f Telescope
tel [] = Telescope -> [NamedArg (Pattern' a)]
forall a. DeBruijn a => Telescope -> [NamedArg a]
f Telescope
tel
telePatterns' forall a. DeBruijn a => Telescope -> [NamedArg a]
f Telescope
tel Boundary
boundary = [Arg (Named (WithOrigin (Ranged ArgName)) a)]
-> [NamedArg (Pattern' a)]
recurse ([Arg (Named (WithOrigin (Ranged ArgName)) a)]
 -> [NamedArg (Pattern' a)])
-> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
-> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
forall a. DeBruijn a => Telescope -> [NamedArg a]
f Telescope
tel
  where
    recurse :: [Arg (Named (WithOrigin (Ranged ArgName)) a)]
-> [NamedArg (Pattern' a)]
recurse = ((Arg (Named (WithOrigin (Ranged ArgName)) a)
 -> NamedArg (Pattern' a))
-> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
-> [NamedArg (Pattern' a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg (Named (WithOrigin (Ranged ArgName)) a)
  -> NamedArg (Pattern' a))
 -> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
 -> [NamedArg (Pattern' a)])
-> ((a -> Pattern' a)
    -> Arg (Named (WithOrigin (Ranged ArgName)) a)
    -> NamedArg (Pattern' a))
-> (a -> Pattern' a)
-> [Arg (Named (WithOrigin (Ranged ArgName)) a)]
-> [NamedArg (Pattern' a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named (WithOrigin (Ranged ArgName)) a
 -> Named (WithOrigin (Ranged ArgName)) (Pattern' a))
-> Arg (Named (WithOrigin (Ranged ArgName)) a)
-> NamedArg (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named (WithOrigin (Ranged ArgName)) a
  -> Named (WithOrigin (Ranged ArgName)) (Pattern' a))
 -> Arg (Named (WithOrigin (Ranged ArgName)) a)
 -> NamedArg (Pattern' a))
-> ((a -> Pattern' a)
    -> Named (WithOrigin (Ranged ArgName)) a
    -> Named (WithOrigin (Ranged ArgName)) (Pattern' a))
-> (a -> Pattern' a)
-> Arg (Named (WithOrigin (Ranged ArgName)) a)
-> NamedArg (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Pattern' a)
-> Named (WithOrigin (Ranged ArgName)) a
-> Named (WithOrigin (Ranged ArgName)) (Pattern' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) a -> Pattern' a
updateVar
    matchVar :: Nat -> Maybe (Term, Term)
matchVar Nat
x =
      (Term, (Term, Term)) -> (Term, Term)
forall a b. (a, b) -> b
snd ((Term, (Term, Term)) -> (Term, Term))
-> Maybe (Term, (Term, Term)) -> Maybe (Term, Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term, (Term, Term)) -> Bool)
-> Boundary -> Maybe (Term, (Term, Term))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\case
        (Var Nat
i [],(Term, Term)
_) -> Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
x
        (Term, (Term, Term))
_            -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__) Boundary
boundary
    updateVar :: a -> Pattern' a
updateVar a
x =
      case a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView a
x of
        Just Nat
i | Just (Term
t,Term
u) <- Nat -> Maybe (Term, Term)
matchVar Nat
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 Nat
_                                 -> 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 :: 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 (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 :: 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 = do
  Term
t <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce 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
_      -> Term -> m a
no Term
t

-- | 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 :: 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 :: 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 :: 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 :: 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> tcm Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t))


-- | 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
piApplyM' m Empty
forall a. HasCallStack => a
__IMPOSSIBLE__

instance PiApplyM Term where
  piApplyM' :: 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 (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

instance PiApplyM a => PiApplyM (Arg a) where
  piApplyM' :: 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
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' :: 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
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' :: m Empty -> Type -> [a] -> m Type
piApplyM' m Empty
err Type
t = (m Type -> a -> m Type) -> m Type -> [a] -> m Type
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 (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
piApplyM' m Empty
err Type
t a
v)) (Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t)


-- | Compute type arity

typeArity :: Type -> TCM Nat
typeArity :: Type -> TCM Nat
typeArity Type
t = do
  TelV Telescope
tel Type
_ <- Type -> TCM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m TelView
telView Type
t
  Nat -> TCM Nat
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel)

---------------------------------------------------------------------------
-- * Instance definitions
---------------------------------------------------------------------------

data OutputTypeName
  = OutputTypeName QName
  | OutputTypeVar
  | OutputTypeVisiblePi
  | OutputTypeNameNotYetKnown Blocker
  | NoOutputTypeName

-- | Strips all hidden and instance Pi's and return the argument
--   telescope and head definition name, if possible.
getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName)
getOutputTypeName :: Type -> TCM (Telescope, OutputTypeName)
getOutputTypeName Type
t = do
  TelV Telescope
tel Type
t' <- Nat -> (Dom Type -> Bool) -> Type -> TCM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' (-Nat
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
  Term
-> (Blocker -> Term -> TCM (Telescope, OutputTypeName))
-> (NotBlocked -> Term -> TCM (Telescope, OutputTypeName))
-> TCM (Telescope, OutputTypeName)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t') (\ Blocker
b Term
_ -> (Telescope, OutputTypeName) -> TCM (Telescope, OutputTypeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel , Blocker -> OutputTypeName
OutputTypeNameNotYetKnown Blocker
b)) ((NotBlocked -> Term -> TCM (Telescope, OutputTypeName))
 -> TCM (Telescope, OutputTypeName))
-> (NotBlocked -> Term -> TCM (Telescope, OutputTypeName))
-> TCM (Telescope, OutputTypeName)
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
v ->
    case Term
v of
      -- Possible base types:
      Def QName
n [Elim' Term]
_  -> (Telescope, OutputTypeName) -> TCM (Telescope, OutputTypeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel , QName -> OutputTypeName
OutputTypeName QName
n)
      Sort{}   -> (Telescope, OutputTypeName) -> TCM (Telescope, OutputTypeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel , OutputTypeName
NoOutputTypeName)
      Var Nat
n [Elim' Term]
_  -> (Telescope, OutputTypeName) -> TCM (Telescope, OutputTypeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel , OutputTypeName
OutputTypeVar)
      Pi{}     -> (Telescope, OutputTypeName) -> TCM (Telescope, OutputTypeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
tel , OutputTypeName
OutputTypeVisiblePi)
      -- Not base types:
      Con{}    -> TCM (Telescope, OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lam{}    -> TCM (Telescope, OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit{}    -> TCM (Telescope, OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Level{}  -> TCM (Telescope, OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV{}  -> TCM (Telescope, OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      DontCare{} -> TCM (Telescope, OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Dummy ArgName
s [Elim' Term]
_ -> ArgName -> TCM (Telescope, OutputTypeName)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
ArgName -> m a
__IMPOSSIBLE_VERBOSE__ ArgName
s

-- | Register the definition with the given type as an instance
addTypedInstance :: QName -> Type -> TCM ()
addTypedInstance :: QName -> Type -> TCM ()
addTypedInstance QName
x Type
t = do
  (Telescope
tel , OutputTypeName
n) <- Type -> TCM (Telescope, OutputTypeName)
getOutputTypeName Type
t
  case OutputTypeName
n of
    OutputTypeName QName
n -> QName -> QName -> TCM ()
addNamedInstance QName
x QName
n
    OutputTypeNameNotYetKnown{} -> QName -> TCM ()
addUnknownInstance QName
x
    OutputTypeName
NoOutputTypeName -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning
WrongInstanceDeclaration
    OutputTypeName
OutputTypeVar -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning
WrongInstanceDeclaration
    OutputTypeName
OutputTypeVisiblePi -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Warning
InstanceWithExplicitArg QName
x

resolveUnknownInstanceDefs :: TCM ()
resolveUnknownInstanceDefs :: TCM ()
resolveUnknownInstanceDefs = do
  Set QName
anonInstanceDefs <- TCM (Set QName)
getAnonInstanceDefs
  TCM ()
clearAnonInstanceDefs
  Set QName -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set QName
anonInstanceDefs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
n -> QName -> Type -> TCM ()
addTypedInstance QName
n (Type -> TCM ()) -> TCMT IO Type -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Type
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
n

-- | Try to solve the instance definitions whose type is not yet known, report
--   an error if it doesn't work and return the instance table otherwise.
getInstanceDefs :: TCM InstanceTable
getInstanceDefs :: TCM InstanceTable
getInstanceDefs = do
  TCM ()
resolveUnknownInstanceDefs
  TempInstanceTable
insts <- TCM TempInstanceTable
getAllInstanceDefs
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set QName -> Bool
forall a. Null a => a -> Bool
null (Set QName -> Bool) -> Set QName -> Bool
forall a b. (a -> b) -> a -> b
$ TempInstanceTable -> Set QName
forall a b. (a, b) -> b
snd TempInstanceTable
insts) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"There are instances whose type is still unsolved"
  InstanceTable -> TCM InstanceTable
forall (m :: * -> *) a. Monad m => a -> m a
return (InstanceTable -> TCM InstanceTable)
-> InstanceTable -> TCM InstanceTable
forall a b. (a -> b) -> a -> b
$ TempInstanceTable -> InstanceTable
forall a b. (a, b) -> a
fst TempInstanceTable
insts