{-# LANGUAGE ViewPatterns #-}

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.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 :: forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom a)
EmptyTel          = []
flattenTel (ExtendTel Dom a
a Abs (Tele (Dom a))
tel) = Int -> Dom a -> Dom a
forall a. Subst a => Int -> a -> a
raise (Abs (Tele (Dom a)) -> Int
forall a. Sized a => a -> Int
size Abs (Tele (Dom a))
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 = ((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 :: [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [String]
xs [Dom Type]
tel = Int -> [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel' ([Dom Type] -> Int
forall a. Sized a => a -> Int
size [Dom Type]
tel) [String]
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 -> [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel' !Int
n [String]
xs [Dom Type]
tel = case ([String]
xs, [Dom Type]
tel) of
  ([],     [])      -> Tele (Dom Type)
forall a. Tele a
EmptyTel
  (String
x : [String]
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' (String -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. String -> a -> Abs a
Abs String
x Tele (Dom Type)
tel')
    where
    tel' :: Tele (Dom Type)
tel' = Int -> [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [String]
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__
  (String
_ : [String]
_, [])    -> 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 String] -> Tele (Dom Type) -> Tele (Dom Type)
renameTel []           Tele (Dom Type)
EmptyTel           = Tele (Dom Type)
forall a. Tele a
EmptyTel
renameTel (Maybe String
Nothing:[Maybe String]
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 String] -> Tele (Dom Type) -> Tele (Dom Type)
renameTel [Maybe String]
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 String
x :[Maybe String]
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 String] -> Tele (Dom Type) -> Tele (Dom Type)
renameTel [Maybe String]
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 :: String
absName = String
x })
renameTel []           (ExtendTel Dom Type
_ Abs (Tele (Dom Type))
_   ) = Tele (Dom Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
renameTel (Maybe String
_      :[Maybe String]
_ ) 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) -> [String]
teleNames = (Dom (String, Type) -> String) -> [Dom (String, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String, Type) -> String
forall a b. (a, b) -> a
fst ((String, Type) -> String)
-> (Dom (String, Type) -> (String, Type))
-> Dom (String, Type)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (String, Type)] -> [String])
-> (Tele (Dom Type) -> [Dom (String, Type)])
-> Tele (Dom Type)
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList

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

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

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 (String, t) -> Dom a)
-> [Int] -> [Dom (String, t)] -> [Dom a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Dom (String, t)
dom -> Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar Int
i a -> Dom (String, 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 (String, t)
dom) (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [Dom (String, t)] -> Int
forall a. Sized a => a -> Int
size [Dom (String, t)]
l) [Dom (String, t)]
l
  where l :: [Dom (String, t)]
l = Tele (Dom t) -> [Dom (String, t)]
forall t. Tele (Dom t) -> [Dom (String, 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

-- | 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 String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName) -> Ranged String -> NamedName
forall a b. (a -> b) -> a -> b
$ String -> Ranged String
forall a. a -> Ranged a
unranged (String -> Ranged String) -> String -> Ranged String
forall a b. (a -> b) -> a -> b
$ String -> String
argNameToString String
argName) (String -> Int -> a
forall a. DeBruijn a => String -> Int -> a
debruijnNamedVar String
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 = (String
argName,Type
_)}, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (String
varName,Type
_)}) <- [Int]
-> [Dom (String, Type)]
-> [Dom (String, Type)]
-> [(Int, Dom (String, Type), Dom (String, 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 (String, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (String, Type)]
l) [Dom (String, Type)]
l0 [Dom (String, Type)]
l ]
  where
  l :: [Dom (String, Type)]
l  = Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel
  l0 :: [Dom (String, Type)]
l0 = Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, 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 :: [String]
names = Permutation -> [String] -> [String]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [String]
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  [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel [String]
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 :: Tele (Dom Type) -> IntSet -> IntSet
varDependencies Tele (Dom Type)
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
$ [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m) [Int]
locks
      where
        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, 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 :: Int
m = IntSet -> Int
IntSet.findMin IntSet
s
    n :: Int
n  = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
    ts :: [Dom Type]
ts = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel

    directDependencies :: Int -> IntSet
    directDependencies :: Int -> IntSet
directDependencies Int
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] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i)

    allDependencies :: IntSet -> IntSet -> IntSet
    allDependencies :: IntSet -> IntSet -> IntSet
allDependencies =
      (Int -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet
forall b. (Int -> b -> b) -> b -> IntSet -> b
IntSet.foldr ((Int -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet)
-> (Int -> IntSet -> IntSet) -> IntSet -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ \Int
j IntSet
soFar ->
        if Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n Bool -> Bool -> Bool
|| Int
j Int -> IntSet -> Bool
`IntSet.member` IntSet
soFar
        then IntSet
soFar
        else Int -> IntSet -> IntSet
IntSet.insert Int
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
$ Int -> IntSet
directDependencies Int
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 :: Tele (Dom Type) -> IntSet -> IntSet
varDependents Tele (Dom Type)
tel = IntSet -> IntSet
allDependents
  where
    n :: Int
n  = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
    ts :: [Dom Type]
ts = Tele (Dom Type) -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel

    directDependents :: IntSet -> IntSet
    directDependents :: IntSet -> IntSet
directDependents IntSet
is = [Int] -> IntSet
IntSet.fromList
      [ Int
j | Int
j <- Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n
          , let tj :: Dom Type
tj = Dom Type -> [Dom Type] -> Int -> Dom Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom Type
forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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) -> (Int -> Bool) -> SingleVar Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> 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 -> 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 :: IntSet -> Tele (Dom Type) -> SplitTel
splitTelescope IntSet
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 :: [String]
names = Tele (Dom Type) -> [String]
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 :: IntSet
is    = Tele (Dom Type) -> IntSet -> IntSet
varDependencies Tele (Dom Type)
tel IntSet
fv
    isC :: IntSet
isC   = [Int] -> IntSet
IntSet.fromList [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
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
$ IntSet -> [Int]
VarSet.toDescList IntSet
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ IntSet -> [Int]
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' :: Tele (Dom Type)
tel'  = [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel (Permutation -> [String] -> [String]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [String]
names) [Dom Type]
ts1

    m :: Int
m     = IntSet -> Int
forall a. Sized a => a -> Int
size IntSet
is
    (Tele (Dom Type)
tel1, Tele (Dom Type)
tel2) = [Dom (String, Type)] -> Tele (Dom Type)
telFromList ([Dom (String, Type)] -> Tele (Dom Type))
-> ([Dom (String, Type)] -> Tele (Dom Type))
-> ([Dom (String, Type)], [Dom (String, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- [Dom (String, Type)] -> Tele (Dom Type)
telFromList (([Dom (String, Type)], [Dom (String, Type)])
 -> (Tele (Dom Type), Tele (Dom Type)))
-> ([Dom (String, Type)], [Dom (String, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Int
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, 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 :: [String]
names = Tele (Dom Type) -> [String]
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'  = [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel (Permutation -> [String] -> [String]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [String]
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 (String, Type)] -> Tele (Dom Type)
telFromList ([Dom (String, Type)] -> Tele (Dom Type))
-> ([Dom (String, Type)] -> Tele (Dom Type))
-> ([Dom (String, Type)], [Dom (String, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- [Dom (String, Type)] -> Tele (Dom Type)
telFromList (([Dom (String, Type)], [Dom (String, Type)])
 -> (Tele (Dom Type), Tele (Dom Type)))
-> ([Dom (String, Type)], [Dom (String, Type)])
-> (Tele (Dom Type), Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Int
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m ([Dom (String, Type)]
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, 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 :: [String]
names = Tele (Dom Type) -> [String]
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 :: IntSet
is0   = Tele (Dom Type) -> IntSet -> IntSet
varDependencies Tele (Dom Type)
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   = Tele (Dom Type) -> IntSet -> IntSet
varDependents Tele (Dom Type)
tel (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Int -> IntSet
forall el coll. Singleton el coll => el -> coll
singleton Int
j
    -- lasti is the last (rightmost) variable of is0
    lasti :: Int
lasti = if IntSet -> Bool
forall a. Null a => a -> Bool
null IntSet
is0 then Int
n else IntSet -> Int
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)
    ([Int]
as,[Int]
bs) = (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Int -> IntSet -> Bool
`IntSet.member` IntSet
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 -> IntSet -> Bool
`IntSet.member` IntSet
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'  = [String] -> [Dom Type] -> Tele (Dom Type)
unflattenTel (Permutation -> [String] -> [String]
forall a. Permutation -> [a] -> [a]
permute Permutation
rho [String]
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 (String, Type)]
ts1,Dom (String, Type)
xa:[Dom (String, Type)]
ts2) = ([Dom (String, Type)], [Dom (String, Type)])
-> Maybe ([Dom (String, Type)], [Dom (String, Type)])
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a. a -> Maybe a -> a
fromMaybe ([Dom (String, Type)], [Dom (String, Type)])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([Dom (String, Type)], [Dom (String, Type)])
 -> ([Dom (String, Type)], [Dom (String, Type)]))
-> Maybe ([Dom (String, Type)], [Dom (String, Type)])
-> ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$
                    Int
-> [Dom (String, Type)]
-> Maybe ([Dom (String, Type)], [Dom (String, Type)])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
k ([Dom (String, Type)]
 -> Maybe ([Dom (String, Type)], [Dom (String, Type)]))
-> [Dom (String, Type)]
-> Maybe ([Dom (String, Type)], [Dom (String, Type)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, 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) ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type) -> Dom (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (String, 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 (String, Type)] -> Int
forall a. Sized a => a -> Int
size [Dom (String, Type)]
ts2) PatternSubstitution
rho0               -- Γ₁ΔΓ₂ρ₀ ⊢ ρ : Γ₁(x : D pars)Γ₂

    gamma1 :: Tele (Dom Type)
gamma1      = [Dom (String, Type)] -> Tele (Dom Type)
telFromList [Dom (String, 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 (String, Type)] -> Tele (Dom Type)
telFromList [Dom (String, 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')

-- | 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)

-- | @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

-- | @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
  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 ->
          -- Force the name to avoid retaining the rest of b.
      let !bn :: String
bn = Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b in
      Dom Type -> String -> TelView -> TelView
forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a String
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

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)

-- | @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 -> String -> TelView -> TelView
forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> String
forall a. Abs a -> String
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)

-- | [[ (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' :: 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 :: * -> *} {a} {a}. Monad m => a -> m (TelV a, [a])
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 {b} {a}.
Subst b =>
b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
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 :: * -> *} {a} {a}. Monad m => a -> m (TelV a, [a])
done Type
t
  where
    done :: a -> m (TelV a, [a])
done a
t      = (TelV a, [a]) -> m (TelV a, [a])
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, [])
    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 -> String -> TelView -> TelView
forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> String
forall a. Abs a -> String
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 :: 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, (Int -> Term
var (Int -> Term) -> Int -> Term
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 -> b -> b
forall a. Subst a => Int -> a -> a
raise (Tele (Dom a) -> Int
forall a. Sized a => a -> Int
size Tele (Dom a)
tel) b
xy) (Term, b) -> [(Term, b)] -> [(Term, b)]
forall a. a -> [a] -> [a]
: [(Term, b)]
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' Term]
es = Tele (Dom Type) -> Boundary -> [Elim' Term]
forall a.
DeBruijn a =>
Tele (Dom Type) -> Boundary' (a, 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 ((Term, (Term, Term)) -> (Term, (Term, Term)))
-> Boundary -> Boundary
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: Term
t@(Var Int
i []), (Term, Term)
xy) -> (Term
t, (Term, Term)
xy (Term, Term) -> [Elim' Term] -> (Term, Term)
forall t. Apply t => t -> [Elim' Term] -> t
`applyE` (Int -> [Elim' Term] -> [Elim' Term]
forall a. Int -> [a] -> [a]
drop (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 :: forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary Int
i Type
a = do
   (telv :: TelView
telv@(TelV Tele (Dom Type)
tel Type
b), Boundary
bs) <- Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
i Type
a
   (TelView, Boundary) -> m (TelView, Boundary)
forall a. a -> m a
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, Tele (Dom Type) -> Boundary -> Boundary
fullBoundary Tele (Dom Type)
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 :: forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP = Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary'

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

-- | 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

-- | 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

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
  Type -> PathView
view <- m (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  Maybe Term
minterval  <- String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getTerm' String
builtinInterval
  (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
-> m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
forall a. a -> m a
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
$ \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 :: String
name | Lam ArgInfo
_ (Abs String
n Term
_) <- Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a = String
n
               | Bool
otherwise = String
"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
               , String -> Type -> Abs Type
forall a. String -> a -> Abs a
Abs String
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 -> String -> TelView -> TelView
forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> String
forall a. Abs a -> String
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 = ((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))
-> (Type -> m (Either (Dom Type, Abs Type) Type))
-> Type
-> m (Maybe (Dom Type, Abs Type))
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Type -> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi

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 [] = 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
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
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 Int
i [],(Term, Term)
_) -> Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x
        (Term, (Term, Term))
_            -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__) Boundary
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 = 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 :: 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))


-- | 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__

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

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 Tele (Dom Type)
tel Type
_ <- Type -> TCM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m TelView
telView Type
t
  Int -> TCM Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
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 (Tele (Dom Type), OutputTypeName)
getOutputTypeName Type
t = do
  TelV Tele (Dom Type)
tel Type
t' <- Int -> (Dom Type -> Bool) -> Type -> TCM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' (-Int
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
  Term
-> (Blocker -> Term -> TCM (Tele (Dom Type), OutputTypeName))
-> (NotBlocked -> Term -> TCM (Tele (Dom Type), OutputTypeName))
-> TCM (Tele (Dom Type), 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
_ -> (Tele (Dom Type), OutputTypeName)
-> TCM (Tele (Dom Type), OutputTypeName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type)
tel , Blocker -> OutputTypeName
OutputTypeNameNotYetKnown Blocker
b)) ((NotBlocked -> Term -> TCM (Tele (Dom Type), OutputTypeName))
 -> TCM (Tele (Dom Type), OutputTypeName))
-> (NotBlocked -> Term -> TCM (Tele (Dom Type), OutputTypeName))
-> TCM (Tele (Dom Type), OutputTypeName)
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
v ->
    case Term
v of
      -- Possible base types:
      Def QName
n [Elim' Term]
_  -> (Tele (Dom Type), OutputTypeName)
-> TCM (Tele (Dom Type), OutputTypeName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type)
tel , QName -> OutputTypeName
OutputTypeName QName
n)
      Sort{}   -> (Tele (Dom Type), OutputTypeName)
-> TCM (Tele (Dom Type), OutputTypeName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type)
tel , OutputTypeName
NoOutputTypeName)
      Var Int
n [Elim' Term]
_  -> (Tele (Dom Type), OutputTypeName)
-> TCM (Tele (Dom Type), OutputTypeName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type)
tel , OutputTypeName
OutputTypeVar)
      Pi{}     -> (Tele (Dom Type), OutputTypeName)
-> TCM (Tele (Dom Type), OutputTypeName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type)
tel , OutputTypeName
OutputTypeVisiblePi)
      -- Not base types:
      Con{}    -> TCM (Tele (Dom Type), OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lam{}    -> TCM (Tele (Dom Type), OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit{}    -> TCM (Tele (Dom Type), OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Level{}  -> TCM (Tele (Dom Type), OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV{}  -> TCM (Tele (Dom Type), OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      DontCare{} -> TCM (Tele (Dom Type), OutputTypeName)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Dummy String
s [Elim' Term]
_ -> String -> TCM (Tele (Dom Type), OutputTypeName)
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
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
  (Tele (Dom Type)
tel , OutputTypeName
n) <- Type -> TCM (Tele (Dom Type), 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
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"There are instances whose type is still unsolved"
  InstanceTable -> TCM InstanceTable
forall a. a -> TCMT IO a
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