{-# OPTIONS_GHC -Wunused-imports #-}

module Mikan.TypeChecking.Telescope where

import Prelude hiding (null)

import Control.Monad

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

import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty ( Pretty )
import Mikan.Syntax.Internal

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

import Mikan.Utils.Either
import Mikan.Utils.Empty
import Mikan.Utils.Functor
import Mikan.Utils.Function
import Mikan.Utils.List
import Mikan.Utils.Null
import Mikan.Utils.Permutation
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.Utils.Tuple
import Mikan.Utils.VarSet (VarSet)
import Mikan.Utils.VarSet qualified as VarSet

import Mikan.Utils.Impossible
import Mikan.Utils.CallStack

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Take the first @n@ elements off of a telescope.
takeTelescope :: Int -> Telescope -> Telescope
takeTelescope :: Int -> Tele (Dom Type) -> Tele (Dom Type)
takeTelescope 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
  | Bool
otherwise = Int -> Tele (Dom Type) -> Tele (Dom Type)
forall {t} {a}. (Eq t, Num t) => t -> Tele a -> Tele a
loop Int
n Tele (Dom Type)
tel where
    loop :: t -> Tele a -> Tele a
loop t
_ Tele a
EmptyTel = Tele a
forall a. Tele a
EmptyTel
    loop t
0 Tele a
tel = Tele a
forall a. Tele a
EmptyTel
    loop t
n (ExtendTel a
a Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (t -> Tele a -> Tele a
loop (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Tele a -> Tele a) -> Abs (Tele a) -> Abs (Tele a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele a)
tel)

-- | Drop the last @n@ elements off of a telescope.
--
-- This is strict in the spine of the telescope.
dropEndTelescope :: Int -> Telescope -> Telescope
dropEndTelescope :: Int -> Tele (Dom Type) -> Tele (Dom Type)
dropEndTelescope 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
  | Bool
otherwise = (Int, Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a, b) -> b
snd ((Int, Tele (Dom Type)) -> Tele (Dom Type))
-> (Int, Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> (Int, Tele (Dom Type))
loop Tele (Dom Type)
tel where
      loop :: Tele (Dom Type) -> (Int, Tele (Dom Type))
loop Tele (Dom Type)
EmptyTel = (Int
n, Tele (Dom Type)
forall a. Tele a
EmptyTel)
      loop (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) =
        let (Int
k, Tele (Dom Type)
pfx) = Tele (Dom Type) -> (Int, Tele (Dom Type))
loop (Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Abs a -> a
unAbs Abs (Tele (Dom Type))
tel)
        in (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Bool
-> (Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type)
-> Tele (Dom Type)
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0) (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))
-> (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type)
-> Tele (Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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)
pfx)

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

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

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



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

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

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

    is :: VarSet
is    = VarSet -> VarSet -> VarSet
VarSet.union (Tele (Dom Type) -> VarSet -> VarSet
varDependencies Tele (Dom Type)
tel VarSet
fv) (Int -> Int -> VarSet
VarSet.range (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
n)
    isC :: VarSet
isC   = Int -> VarSet -> VarSet
VarSet.complement Int
n VarSet
is

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    j' :: Int
j'    = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Permutation -> Int -> Maybe Int
lookupRP Permutation
perm Int
j
    p1 :: Pattern' DBPatVar
p1    = Impossible -> Permutation -> Pattern' DBPatVar -> Pattern' DBPatVar
forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
HasCallStack => Impossible
impossible Permutation
perm' Pattern' DBPatVar
p -- Γ' ⊢ p1 : A'
    sigma :: PatternSubstitution
sigma = Int -> Pattern' DBPatVar -> PatternSubstitution
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
j' Pattern' DBPatVar
p1 PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Impossible -> Permutation -> PatternSubstitution
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible Permutation
perm -- Γ' ⊢ σ : Г

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

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

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

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

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


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

{-# INLINE telViewUpTo #-}
-- | @telViewUpTo n t@ takes off the first @n@ function types of @t@.
-- Takes off all if @n < 0@.
telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView
telViewUpTo :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m TelView
telViewUpTo Int
n Type
t =
  -- [TODO: Reed M, 09/05/2026]
  -- This does not get optimized very well on GHC 9.12 and below,
  -- as we can't SPECIALIZE away the (const True).
  Int -> (Dom Type -> Bool) -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Int
n (Bool -> Dom Type -> Bool
forall a b. a -> b -> a
const Bool
True) Type
t

{-# SPECIALIZE telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView #-}
-- | @telViewUpTo' n p t@ takes off $t$
--   the first @n@ (or arbitrary many if @n < 0@) function domains
--   as long as they satify @p@.
telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Int
0 Dom Type -> Bool
p Type
t = TelView -> m TelView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t
telViewUpTo' Int
n Dom Type -> Bool
p Type
t = do
  t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case unEl t of
    Pi Dom Type
a Abs Type
b | Dom Type -> Bool
p Dom Type
a ->
          -- Force the name to avoid retaining the rest of b.
      let !bn :: ArgName
bn = Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b in
      Dom Type -> ArgName -> TelView -> TelView
forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom Type
a ArgName
bn (TelView -> TelView) -> m TelView -> m TelView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        -- [TODO: Reed M, 09/05/2026]
        -- Using 'underAbstractionAbs' is horrible here, as we end up calling
        -- 'raise 1' @n@ times. Instead, we should fuse this into a loop that
        -- counts the number of @Abs@ binders we go under.
        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
b ->
          Int -> (Dom Type -> Bool) -> Type -> m TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Dom Type -> Bool
p Type
b
    Term
_ -> TelView -> m TelView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TelView -> m TelView) -> TelView -> m TelView
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Tele (Dom Type)
forall a. Tele a
EmptyTel Type
t

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

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

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

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

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

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

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

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

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

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

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


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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Decomposing a function type.

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

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

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

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

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

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

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

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

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

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

shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type, Boundary)
shouldBePiOrPath :: forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type, Boundary)
shouldBePiOrPath Type
t = do
  (TelV tel t', b) <- Int -> Type -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary Int
1 Type
t
  case tel of
    ExtendTel Dom Type
dom (Abs ArgName
nm Tele (Dom Type)
EmptyTel) -> (Dom Type, Abs Type, Boundary) -> m (Dom Type, Abs Type, Boundary)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dom Type
dom, ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
nm Type
t', Boundary
b)
    Tele (Dom Type)
_ -> TypeError -> m (Dom Type, Abs Type, Boundary)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m (Dom Type, Abs Type, Boundary))
-> TypeError -> m (Dom Type, Abs Type, Boundary)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
t

-- | Instantiate a 'Type' with a sequence of arguments, possibly
-- reducing if the type is not manifestly a 'Pi'.
--
-- This is a safe variant of 'piApply'.
piApplyM''
  :: forall m. (MonadReduce m, HasBuiltins m)
  => m Empty -- ^ How to proceed if the type cannot be reduced to a 'Pi' type
  -> Type    -- ^ The type to instantiate
  -> [Term]  -- ^ The arguments
  -> m Type
piApplyM'' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> [Term] -> m Type
piApplyM'' m Empty
err = Substitution' Term -> Type -> [Term] -> m Type
loop Substitution' Term
forall a. Substitution' a
idS where
  abort :: m Type
  abort :: m Type
abort = 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

  loop :: Substitution -> Type -> [Term] -> m Type
  loop :: Substitution' Term -> Type -> [Term] -> m Type
loop !Substitution' Term
rho !Type
t [] = Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
rho Type
t
  loop Substitution' Term
rho Type
t (Term
a:[Term]
as) = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    -- accumulate a substitution while we have manifest Pi types, so the
    -- body is traversed only once.
    Pi Dom Type
_ Abs Type
abs -> case Abs Type
abs of
      Abs   ArgName
_ Type
body -> Substitution' Term -> Type -> [Term] -> m Type
loop (Term
a Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` Substitution' Term
rho) Type
body [Term]
as
      NoAbs ArgName
_ Type
body -> Substitution' Term -> Type -> [Term] -> m Type
loop Substitution' Term
rho Type
body [Term]
as

    -- these can't become Pi types even after substitution, so we might
    -- as well abort early instead of applying the substitution
    Lam{}   -> m Type
abort
    Con{}   -> m Type
abort
    Lit{}   -> m Type
abort
    Sort{}  -> m Type
abort
    Level{} -> m Type
abort

    -- if we have to compute, apply the current accumulated substitution
    -- and restart the accumulator.
    Term
_ -> 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 (Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
rho Type
t)
      {- then -} (\Type
_   -> m Type
abort)
      {- else -} (\Dom Type
_ Abs Type
b -> Substitution' Term -> Type -> [Term] -> m Type
loop Substitution' Term
forall a. Substitution' a
idS (Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
SubstArg Type
a) [Term]
as)

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

-- | A class for things ('Arg', etc) that can be turned into a sequence
-- of arguments for 'piApplyM''.
class PiApplyArgs a where
  toPiArgs :: a -> [Term]

instance PiApplyArgs Term where
  toPiArgs :: Term -> [Term]
toPiArgs = Term -> [Term]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance PiApplyArgs a => PiApplyArgs (Arg a) where
  toPiArgs :: Arg a -> [Term]
toPiArgs = a -> [Term]
forall a. PiApplyArgs a => a -> [Term]
toPiArgs (a -> [Term]) -> (Arg a -> a) -> Arg a -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

instance PiApplyArgs a => PiApplyArgs (Named n a) where
  toPiArgs :: Named n a -> [Term]
toPiArgs = a -> [Term]
forall a. PiApplyArgs a => a -> [Term]
toPiArgs (a -> [Term]) -> (Named n a -> a) -> Named n a -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named n a -> a
forall name a. Named name a -> a
namedThing

instance PiApplyArgs a => PiApplyArgs [a] where
  toPiArgs :: [a] -> [Term]
toPiArgs = (a -> [Term]) -> [a] -> [Term]
forall a b. (a -> [b]) -> [a] -> [b]
concatMap' a -> [Term]
forall a. PiApplyArgs a => a -> [Term]
toPiArgs

-- | A version of 'piApplyM''' generalised over the arguments to
-- instantiate with.
piApplyM' :: (MonadReduce m, HasBuiltins m, PiApplyArgs a) => m Empty -> Type -> a -> m Type
piApplyM' :: forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
ty a
as = m Empty -> Type -> [Term] -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> [Term] -> m Type
piApplyM'' m Empty
err Type
ty ([Term] -> m Type) -> [Term] -> m Type
forall a b. (a -> b) -> a -> b
$! a -> [Term]
forall a. PiApplyArgs a => a -> [Term]
toPiArgs a
as
{-# INLINE piApplyM' #-}

-- | A version of 'piApplyM''' generalised over the arguments to
-- instantiate with, throwing an @'__IMPOSSIBLE__'@ error if there are
-- leftover arguments and the type can not be reduced to a 'Pi' type.
piApplyM :: (MonadReduce m, HasBuiltins m, PiApplyArgs a) => Type -> a -> m Type
piApplyM :: forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
Type -> a -> m Type
piApplyM = m Empty -> Type -> a -> m Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
{-# INLINE piApplyM #-}

-- | Compute type arity

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

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

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

---------------------------------------------------------------------------
-- * Teletypes
---------------------------------------------------------------------------

-- | Instantiate a 'Teletype' with some 'Args', attempting to produce a
-- 'Type'.
--
-- Takes continuations for whether we ran out of arguments with leftover
-- quantification, or out of quantifiers with leftover arguments. Note
-- that, unlike 'teleView', the 'Type' given to the "out of arguments"
-- continuation may include leading 'Pi's.
teleApply'
  :: Teletype                 -- ^ The teletype to instantiate.
  -> Args                     -- ^ The arguments.
  -> (Telescope -> Type -> a) -- ^ How to handle running out of arguments.
  -> (Type -> Args -> a)      -- ^ How to handle running out of quantifiers.
  -> a
teleApply' :: forall a.
Teletype
-> Args
-> (Tele (Dom Type) -> Type -> a)
-> (Type -> Args -> a)
-> a
teleApply' Teletype
tel Args
args Tele (Dom Type) -> Type -> a
okay Type -> Args -> a
fail =
  let
    -- like the piApplyM'' implementation, builds a substitution for the
    -- arguments instead of using absApp to avoid traversing the "core"
    -- multiple times.
    go :: Substitution' Term -> Args -> Teletype -> a
go !Substitution' Term
rho [] Teletype
tt = do
      let (!Tele (Dom Type)
tel, !Type
ty) = Teletype -> (Tele (Dom Type), Type)
unpackTeletype Teletype
tt
      Tele (Dom Type) -> Type -> a
okay (Substitution' (SubstArg (Tele (Dom Type)))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Tele (Dom Type)))
rho Tele (Dom Type)
tel) (Type -> a) -> Type -> a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Substitution' Term
rho) Type
ty
    go Substitution' Term
rho (Arg Term
a:Args
as) Teletype
tt = case Teletype
tt of
      ExtendTt Dom Type
_ Abs Teletype
b -> Substitution' Term -> Args -> Teletype -> a
go (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a Term -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
`consS` Substitution' Term
rho) Args
as (Abs Teletype -> Teletype
forall a. Subst a => Abs a -> a
absBody Abs Teletype
b)
      EmptyTt Type
ty   -> (Type -> Args -> a) -> Args -> Type -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Args -> a
fail (Arg Term
aArg Term -> Args -> Args
forall a. a -> [a] -> [a]
:Args
as) (Type -> a) -> Type -> a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
rho Type
ty
  in Substitution' Term -> Args -> Teletype -> a
go Substitution' Term
forall a. Substitution' a
idS Args
args Teletype
tel
{-# INLINE teleApply' #-}

-- | Instantiate a 'Teletype' with some 'Args', handling leftover
-- arguments by attempting reduction.
--
-- Leftover quantifiers are turned into /dependent/ binders (@'Abs'@),
-- as per @'telePi_'@.
teleApplyM
  :: forall m. (HasBuiltins m, MonadReduce m)
  => m Empty
  -- ^ How to error if there are leftover arguments and the "core" of
  -- the teletype does not compute to a function type.
  -> Teletype -- ^ The teletype to instantiate.
  -> Args     -- ^ The arguments.
  -> m Type
teleApplyM :: forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
m Empty -> Teletype -> Args -> m Type
teleApplyM m Empty
abort Teletype
tel Args
args = Teletype
-> Args
-> (Tele (Dom Type) -> Type -> m Type)
-> (Type -> Args -> m Type)
-> m Type
forall a.
Teletype
-> Args
-> (Tele (Dom Type) -> Type -> a)
-> (Type -> Args -> a)
-> a
teleApply' Teletype
tel Args
args (\Tele (Dom Type)
tel Type
ty -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$! Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
ty) (m Empty -> Type -> Args -> m Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
abort)
{-# INLINABLE teleApplyM #-}

-- | Instantiate a 'Teletype' with some 'Args'.
-- Leftover quantifiers are turned into /dependent/ binders (@'Abs'@),
-- as per @'telePi_'@.
--
-- __INVARIANT__: the length of the arguments must not exceed the
-- explicit quantification in the teletype. If this is not known, use
-- the monadic 'teleApplyM' instead.
teleApply :: HasCallStack => Teletype -> Args -> Type
teleApply :: HasCallStack => Teletype -> Args -> Type
teleApply Teletype
tel Args
args = Teletype
-> Args
-> (Tele (Dom Type) -> Type -> Type)
-> (Type -> Args -> Type)
-> Type
forall a.
Teletype
-> Args
-> (Tele (Dom Type) -> Type -> a)
-> (Type -> Args -> a)
-> a
teleApply' Teletype
tel Args
args Tele (Dom Type) -> Type -> Type
telePi_ \Type
_ Args
_ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__
{-# INLINABLE teleApply #-}

-- | View a 'Teletype' as a 'TelView', continuing into the "core" type
-- if necessary.
--
-- Unlike 'unpackTeletype', this function will also move quantification
-- in the "core" of the 'Teletype' into the 'Telescope' returned, as per
-- 'telView'.
teleView :: MonadReduce m => Teletype -> m TelView
teleView :: forall (m :: * -> *). MonadReduce m => Teletype -> m TelView
teleView Teletype
tty = ReduceM TelView -> m TelView
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce do
  let (!Tele (Dom Type)
tel, !Type
ty) = Teletype -> (Tele (Dom Type), Type)
unpackTeletype Teletype
tty
  Tele (Dom Type) -> ReduceM TelView -> ReduceM TelView
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel do
    TelV tel' ty <- Type -> ReduceM TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m TelView
telView Type
ty
    pure (TelV (tel `abstract` tel') ty)
{-# INLINE teleView #-}

-- | Quantify a 'Type' over a 'Telescope', producing a 'Teletype'.
--
-- If the type is a literal function type (as per 'telView''), these
-- extra quantifiers are also moved into the 'Teletype'.
teleType :: Telescope -> Type -> Teletype
teleType :: Tele (Dom Type) -> Type -> Teletype
teleType Tele (Dom Type)
tele Type
inty =
  let
    TelV Tele (Dom Type)
tele' Type
ty = Type -> TelView
telView' Type
inty

    loop :: Tele (Dom Type) -> Teletype
loop Tele (Dom Type)
EmptyTel        = Type -> Teletype
EmptyTt Type
ty
    loop (ExtendTel Dom Type
a Abs (Tele (Dom Type))
b) = Dom Type -> Abs Teletype -> Teletype
ExtendTt Dom Type
a (Abs Teletype -> Teletype) -> Abs Teletype -> Teletype
forall a b. (a -> b) -> a -> b
$! Tele (Dom Type) -> Teletype
loop (Tele (Dom Type) -> Teletype)
-> Abs (Tele (Dom Type)) -> Abs Teletype
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom Type))
b
  in Tele (Dom Type) -> Teletype
loop (Tele (Dom Type)
tele Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Tele (Dom Type)
tele')

-- | Add a binding to the front of a 'Teletype'.
teleCons :: Dom (ArgName, Type) -> Teletype -> Teletype
teleCons :: Dom (ArgName, Type) -> Teletype -> Teletype
teleCons Dom (ArgName, Type)
dom !Teletype
tt =
  let !nm :: ArgName
nm = (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type) -> ArgName) -> (ArgName, Type) -> ArgName
forall a b. (a -> b) -> a -> b
$ Dom (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom Dom (ArgName, Type)
dom
   in Dom Type -> Abs Teletype -> Teletype
ExtendTt ((ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type) -> Dom (ArgName, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (ArgName, Type)
dom) (ArgName -> Teletype -> Abs Teletype
forall a. ArgName -> a -> Abs a
Abs ArgName
nm Teletype
tt)
{-# INLINE teleCons #-}

-- | View a 'Teletype' as a 'TelView', continuing into the "core" type
-- if necessary, returning the expected boundaries of any path
-- encountered along the way; a 'Teletype' version of
-- 'telViewUpToPathBoundary'.
--
-- The 'Int' parameter, @n@, controls the number of quantifiers that may be
-- returned in the 'TelView'. This means that if @n@ is less than the
-- size of the teletype, any quantifiers will be moved into the /type/
-- part of the 'TelView'.
--
-- This function is lazy in the 'Boundary', so it can be used even if
-- computing the boundary is not necessary.
teleViewUpToPathBoundary :: PureTCM m => Int -> Teletype -> m (TelView, Boundary)
teleViewUpToPathBoundary :: forall (m :: * -> *).
PureTCM m =>
Int -> Teletype -> m (TelView, Boundary)
teleViewUpToPathBoundary !Int
n Teletype
tty = do
  let
    -- this is a slightly crazy traversal that accumulates a telescope
    -- extension (outside-in) to put the Teletype back together whenever
    -- we're exiting or deferring to the Type version.
    --
    -- doing it like this avoids iterated addContext for the Teletype
    -- prefix.

    loop :: (Tele (Dom Type) -> Tele (Dom Type))
-> Int -> Teletype -> f (TelView, Boundary)
loop !Tele (Dom Type) -> Tele (Dom Type)
tel Int
0 Teletype
tty = do
      let !ty :: Type
ty = HasCallStack => Teletype -> Args -> Type
Teletype -> Args -> Type
teleApply Teletype
tty []
      (TelView, Boundary) -> f (TelView, Boundary)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tele (Dom Type) -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV (Tele (Dom Type) -> Tele (Dom Type)
tel Tele (Dom Type)
forall a. Tele a
EmptyTel) Type
ty, [(Int, (Term, Term))] -> Boundary
forall x a. [(x, (a, a))] -> Boundary' x a
Boundary [])

    loop Tele (Dom Type) -> Tele (Dom Type)
tel Int
n Teletype
tty = case Teletype
tty of
      EmptyTt  Type
ty      -> do
        (TelV tel' ty, b) <- Tele (Dom Type) -> f (TelView, Boundary) -> f (TelView, Boundary)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (Tele (Dom Type) -> Tele (Dom Type)
tel Tele (Dom Type)
forall a. Tele a
EmptyTel) (f (TelView, Boundary) -> f (TelView, Boundary))
-> f (TelView, Boundary) -> f (TelView, Boundary)
forall a b. (a -> b) -> a -> b
$ Int -> Type -> f (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
n Type
ty
        pure (TelV (tel tel') ty, b)
      ExtendTt Dom Type
dom Abs Teletype
abs -> (Tele (Dom Type) -> Tele (Dom Type))
-> Int -> Teletype -> f (TelView, Boundary)
loop (Tele (Dom Type) -> Tele (Dom Type)
tel (Tele (Dom Type) -> Tele (Dom Type))
-> (Tele (Dom Type) -> Tele (Dom Type))
-> Tele (Dom Type)
-> Tele (Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
dom (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type)
-> Tele (Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs (Abs Teletype -> ArgName
forall a. Abs a -> ArgName
absName Abs Teletype
abs)) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs Teletype -> Teletype
forall a. Abs a -> a
unAbs Abs Teletype
abs)

  (v@(TelV !tel _), bndry) <- (Tele (Dom Type) -> Tele (Dom Type))
-> Int -> Teletype -> m (TelView, Boundary)
forall {f :: * -> *}.
PureTCM f =>
(Tele (Dom Type) -> Tele (Dom Type))
-> Int -> Teletype -> f (TelView, Boundary)
loop Tele (Dom Type) -> Tele (Dom Type)
forall a. a -> a
id Int
n Teletype
tty
  pure (v, fullBoundary tel bndry)
{-# SPECIALIZE teleViewUpToPathBoundary :: Int -> Teletype -> TCM (TelView, Boundary) #-}

teleViewUpToPath :: PureTCM m => Int -> Teletype -> m TelView
teleViewUpToPath :: forall (m :: * -> *). PureTCM m => Int -> Teletype -> m TelView
teleViewUpToPath Int
n Teletype
tty = (TelView, Boundary) -> TelView
forall a b. (a, b) -> a
fst ((TelView, Boundary) -> TelView)
-> m (TelView, Boundary) -> m TelView
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Int -> Teletype -> m (TelView, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Teletype -> m (TelView, Boundary)
teleViewUpToPathBoundary Int
n Teletype
tty
{-# INLINE teleViewUpToPath #-}