{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE ViewPatterns #-}

module Agda.TypeChecking.Telescope where

import Prelude hiding (null)

import Control.Monad

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

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

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

import Agda.Utils.CallStack ( withCallerCallStack )
import Agda.Utils.Either
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible

-- | Flatten telescope: (Γ : Tel) -> [Type Γ]
flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel :: forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom a)
EmptyTel          = []
flattenTel (ExtendTel Dom a
a Abs (Tele (Dom a))
tel) = forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Abs (Tele (Dom a))
tel forall a. Num a => a -> a -> a
+ Int
1) Dom a
a forall a. a -> [a] -> [a]
: forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom a))
tel)

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

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

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

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

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

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

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

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

teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
teleArgs :: forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
teleDoms

teleDoms :: (DeBruijn a) => Tele (Dom t) -> [Dom a]
teleDoms :: forall a t. DeBruijn a => Tele (Dom t) -> [Dom a]
teleDoms Tele (Dom t)
tel = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i Dom (String, t)
dom -> forall a. DeBruijn a => Int -> a
deBruijnVar Int
i forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom (String, t)
dom) (forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size [Dom (String, t)]
l) [Dom (String, t)]
l
  where l :: [Dom (String, t)]
l = forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom t)
tel

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

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

-- | A variant of `teleNamedArgs` which takes the argument names (and the argument info)
--   from the first telescope and the variable names from the second telescope.
--
--   Precondition: the two telescopes have the same length.
tele2NamedArgs :: (DeBruijn a) => Telescope -> Telescope -> [NamedArg a]
tele2NamedArgs :: forall a.
DeBruijn a =>
Tele (Dom Type) -> Tele (Dom Type) -> [NamedArg a]
tele2NamedArgs Tele (Dom Type)
tel0 Tele (Dom Type)
tel =
  [ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged forall a b. (a -> b) -> a -> b
$ String -> String
argNameToString String
argName) (forall a. DeBruijn a => String -> Int -> a
debruijnNamedVar String
varName Int
i))
  | (Int
i, Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = (String
argName,Type
_)}, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (String
varName,Type
_)}) <- forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size [Dom (String, Type)]
l) [Dom (String, Type)]
l0 [Dom (String, Type)]
l ]
  where
  l :: [Dom (String, Type)]
l  = forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel
  l0 :: [Dom (String, Type)]
l0 = forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel0

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

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

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

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

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

-- | Computes the set of variables in a telescope whose type depend on
--   one of the variables in the given set (including recursive
--   dependencies). Any dependencies outside of the telescope are
--   ignored.
varDependents :: Telescope -> IntSet -> IntSet
varDependents :: Tele (Dom Type) -> IntSet -> IntSet
varDependents Tele (Dom Type)
tel = IntSet -> IntSet
allDependents
  where
    n :: Int
n  = forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
    ts :: [Dom Type]
ts = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel

    directDependents :: IntSet -> IntSet
    directDependents :: IntSet -> IntSet
directDependents IntSet
is = [Int] -> IntSet
IntSet.fromList
      [ Int
j | Int
j <- forall a. Integral a => a -> [a]
downFrom Int
n
          , let tj :: Dom Type
tj = forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts (Int
nforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
j)
          , Any -> Bool
getAny forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> Any
Any forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> IntSet -> Bool
`IntSet.member` IntSet
is)) IgnoreSorts
IgnoreNot Dom Type
tj
          ]

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

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

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

    is :: IntSet
is    = Tele (Dom Type) -> IntSet -> IntSet
varDependencies Tele (Dom Type)
tel IntSet
fv
    isC :: IntSet
isC   = [Int] -> IntSet
IntSet.fromList [Int
0..(Int
nforall a. Num a => a -> a -> a
-Int
1)] IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is

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

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

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

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

-- | As splitTelescope, but fails if any additional variables or reordering
--   would be needed to make the first part well-typed.
splitTelescopeExact
  :: [Int]          -- ^ A list of de Bruijn indices
  -> Telescope      -- ^ The telescope to split
  -> Maybe SplitTel -- ^ @firstPart@ mentions the given variables in the given order,
                    --   @secondPart@ contains all other variables
splitTelescopeExact :: [Int] -> Tele (Dom Type) -> Maybe SplitTel
splitTelescopeExact [Int]
is Tele (Dom Type)
tel = forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Tele (Dom Type) -> Tele (Dom Type) -> Permutation -> SplitTel
SplitTel Tele (Dom Type)
tel1 Tele (Dom Type)
tel2 Permutation
perm
  where
    names :: [String]
names = Tele (Dom Type) -> [String]
teleNames Tele (Dom Type)
tel
    ts0 :: [Dom Type]
ts0   = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
    n :: Int
n     = 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   = forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom Type]
ts0 (Int
nforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
j)  -- ts0[n-1-j]
        -- Skip the construction of intermediate @IntSet@s in the check @ok@.
        -- ok  = (allFreeVars t `IntSet.intersection` IntSet.fromAscList [ 0 .. n-1 ])
        --       `IntSet.isSubsetOf` soFar
        good :: Int -> All
good Int
i = Bool -> All
All forall a b. (a -> b) -> a -> b
$ (Int
i 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 = forall a. Ord a => a -> a -> Bool
(<=)
        ok :: Bool
ok = All -> Bool
getAll forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree Int -> All
good IgnoreSorts
IgnoreNot Dom Type
t

    ok :: Bool
ok    = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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   = forall a. Integral a => a -> [a]
downFrom Int
n forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Int]
is

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

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

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

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

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

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

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

    -- is0 is the part of Γ that is needed to type u
    is0 :: IntSet
is0   = Tele (Dom Type) -> IntSet -> IntSet
varDependencies Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall t. Free t => t -> IntSet
allFreeVars Term
u
    -- is1 is the part of Γ that depends on variable j
    is1 :: IntSet
is1   = Tele (Dom Type) -> IntSet -> IntSet
varDependents Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton Int
j
    -- lasti is the last (rightmost) variable of is0
    lasti :: Int
lasti = if forall a. Null a => a -> Bool
null IntSet
is0 then Int
n else IntSet -> Int
IntSet.findMin IntSet
is0
    -- we move each variable in is1 to the right until it comes after
    -- all variables in is0 (i.e. after lasti)
    ([Int]
as,[Int]
bs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Int -> IntSet -> Bool
`IntSet.member` IntSet
is1) [ Int
nforall a. Num a => a -> a -> a
-Int
1 , Int
nforall a. Num a => a -> a -> a
-Int
2 .. Int
lasti ]
    is :: [Int]
is    = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Eq a => a -> [a] -> [a]
List.delete Int
j forall a b. (a -> b) -> a -> b
$ [Int]
bs forall a. [a] -> [a] -> [a]
++ [Int]
as forall a. [a] -> [a] -> [a]
++ forall a. Integral a => a -> [a]
downFrom Int
lasti

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

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

    p1 :: Pattern' DBPatVar
p1    = forall a. Subst a => Impossible -> Permutation -> a -> a
renameP HasCallStack => Impossible
impossible Permutation
perm Pattern' DBPatVar
p -- Γ' ⊢ p1 : A'
    us :: [Pattern' DBPatVar]
us    = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pattern' DBPatVar
p1 forall a. DeBruijn a => Int -> a
deBruijnVar (forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
is)) [ Int
0 .. Int
nforall a. Num a => a -> a -> a
-Int
1 ]
    sigma :: PatternSubstitution
sigma = [Pattern' DBPatVar]
us forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Int -> Substitution' a
raiseS (Int
nforall a. Num a => a -> a -> a
-Int
1)

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

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

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

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

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

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

-- | @telViewUpTo n t@ takes off the first @n@ function types of @t@.
-- Takes off all if @n < 0@.
telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView
telViewUpTo :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m TelView
telViewUpTo Int
n Type
t = forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Int
n (forall a b. a -> b -> a
const Bool
True) Type
t

-- | @telViewUpTo' n p t@ takes off $t$
--   the first @n@ (or arbitrary many if @n < 0@) function domains
--   as long as they satify @p@.
telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' Int
0 Dom Type -> Bool
p Type
t = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Tele (Dom a) -> a -> TelV a
TelV forall a. Tele a
EmptyTel Type
t
telViewUpTo' Int
n Dom Type -> Bool
p Type
t = do
  Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  case forall t a. Type'' t a -> a
unEl Type
t of
    Pi Dom Type
a Abs Type
b | Dom Type -> Bool
p Dom Type
a ->
          -- Force the name to avoid retaining the rest of b.
      let !bn :: String
bn = forall a. Abs a -> String
absName Abs Type
b in
      forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a String
bn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ \Type
b -> forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m TelView
telViewUpTo' (Int
n forall a. Num a => a -> a -> a
- Int
1) Dom Type -> Bool
p Type
b
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Tele (Dom a) -> a -> TelV a
TelV forall a. Tele a
EmptyTel Type
t

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

-- | @telViewUpToPath n t@ takes off $t$
--   the first @n@ (or arbitrary many if @n < 0@) function domains or Path types.
--
-- @telViewUpToPath n t = fst <$> telViewUpToPathBoundary'n t@
telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
telViewUpToPath :: forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
telViewUpToPath Int
n Type
t = if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
done Type
t else do
  forall (m :: * -> *).
PureTCM m =>
Type -> m (Either (Dom Type, Abs Type) Type)
pathViewAsPi Type
t 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               -> forall {m :: * -> *} {a}. Monad m => a -> m (TelV a)
done Type
t
  where
    done :: a -> m (TelV a)
done a
t      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Tele (Dom a) -> a -> TelV a
TelV forall a. Tele a
EmptyTel a
t
    recurse :: Dom Type -> Abs Type -> m TelView
recurse Dom Type
a Abs Type
b = forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (forall a. Abs a -> String
absName Abs Type
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
telViewUpToPath (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Type
b)

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

-- | Like @telViewUpToPath@ but also returns the @Boundary@ expected
-- by the Path types encountered. The boundary terms live in the
-- telescope given by the @TelView@.
-- Each point of the boundary has the type of the codomain of the Path type it got taken from, see @fullBoundary@.
telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' :: forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' Int
n Type
t = if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then forall {m :: * -> *} {a} {a}. Monad m => a -> m (TelV a, [a])
done Type
t else do
  forall (m :: * -> *).
PureTCM m =>
Type -> m (Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi' Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left ((Dom Type
a, Abs Type
b), (Term, Term)
xy)     -> forall {b} {a}.
Subst b =>
b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
addEndPoints (Term, Term)
xy 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               -> forall {m :: * -> *} {a} {a}. Monad m => a -> m (TelV a, [a])
done Type
t
  where
    done :: a -> m (TelV a, [a])
done a
t      = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Tele (Dom a) -> a -> TelV a
TelV forall a. Tele a
EmptyTel a
t, [])
    recurse :: Dom Type -> Abs Type -> m (TelView, Boundary)
recurse Dom Type
a Abs Type
b = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (forall a. Abs a -> String
absName Abs Type
b)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
a Abs Type
b forall a b. (a -> b) -> a -> b
$ \Type
b -> forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary' (Int
n forall a. Num a => a -> a -> a
- Int
1) Type
b
    addEndPoints :: b -> (TelV a, [(Term, b)]) -> (TelV a, [(Term, b)])
addEndPoints b
xy (telv :: TelV a
telv@(TelV Tele (Dom a)
tel a
_), [(Term, b)]
cs) =
      (TelV a
telv, (Int -> Term
var forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Tele (Dom a)
tel forall a. Num a => a -> a -> a
- Int
1, forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Tele (Dom a)
tel) b
xy) forall a. a -> [a] -> [a]
: [(Term, b)]
cs)


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

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

-- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundaryP n a@
--  Input:  Δ ⊢ a
--  Output: Δ.Γ ⊢ b
--          Δ.Γ ⊢ T is the codomain of the PathP at variable i
--          Δ.Γ ⊢ i : I
--          Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
-- Useful to reconstruct IApplyP patterns after teleNamedArgs Γ.
telViewUpToPathBoundaryP :: PureTCM m => Int -> Type -> m (TelView,Boundary)
telViewUpToPathBoundaryP :: forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP = forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundary'

telViewPathBoundaryP :: PureTCM m => Type -> m (TelView,Boundary)
telViewPathBoundaryP :: forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
telViewPathBoundaryP = forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP (-Int
1)


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

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

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

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

    Type
t    -> 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
  (forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    Left ((Dom Type, Abs Type)
p, (Term, Term)
_)           -> forall a b. a -> Either a b
Left (Dom Type, Abs Type)
p
    Right (El Sort' Term
_ (Pi Dom Type
a Abs Type
b)) -> forall a b. a -> Either a b
Left (Dom Type
a,Abs Type
b)
    Right 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 forall a. Eq a => a -> a -> Bool
== Int
0 then TCM TelView
done else do
  forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (Dom Type
a, Abs Type
b) -> forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (forall a. Abs a -> String
absName Abs Type
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => Int -> Type -> m TelView
telViewUpToPath (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Type
b)
    Right Type
_     -> TCM TelView
done
  where
    done :: TCM TelView
done = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Tele (Dom a) -> a -> TelV a
TelV 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 = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Dom Type
a,Abs Type
b)) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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 forall a b. (a -> b) -> a -> b
$ Type -> m a
no forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking

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 = 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 forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b Type
t)
  (\NotBlocked
nb Type
t -> forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t)
    (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> m a
yes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
    (Blocked Type -> m a
no forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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 -> forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t a. Blocked' t a -> a
ignoreBlocking Blocked Type
bt))
    (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> m a
yes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
    (Blocked Type -> m a
no forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Type
bt 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =>
(forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a])
-> Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' 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 [] = forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
tel
telePatterns' forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
tel Boundary
boundary = [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
recurse forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
f Tele (Dom Type)
tel
  where
    recurse :: [Arg (Named NamedName a)] -> [NamedArg (Pattern' a)]
recurse = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) a -> Pattern' a
updateVar
    matchVar :: Int -> Maybe (Term, Term)
matchVar Int
x =
      forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\case
        (Var Int
i [],(Term, Term)
_) -> Int
i forall a. Eq a => a -> a -> Bool
== Int
x
        (Term, (Term, Term))
_            -> forall a. HasCallStack => a
__IMPOSSIBLE__) Boundary
boundary
    updateVar :: a -> Pattern' a
updateVar a
x =
      case 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 -> forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
defaultPatternInfo Term
t Term
u a
x
        Maybe Int
_                                 -> 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 = forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
t forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a b c. ((a, b) -> c) -> a -> b -> c
curry 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 = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s 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 = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
  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 -> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> tcm a
yes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Type -> tcm a
no Type
t) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (m :: * -> *).
HasBuiltins m =>
m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
pathViewAsPi'whnf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall (m :: * -> *) a.
PureTCM m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPathB Type
t
  (forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall (m :: * -> *) a. Monad m => a -> m a
return)
  (forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    El Sort' Term
_ Dummy{} -> forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => Dom Type
__DUMMY_DOM__, forall a. String -> a -> Abs a
Abs String
"x" HasCallStack => Type
__DUMMY_TYPE__)
    Type
t -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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 = forall (m :: * -> *) a.
MonadReduce m =>
Type
-> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
ifPiTypeB Type
t
  (forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall (m :: * -> *) a. Monad m => a -> m a
return)
  (forall (m :: * -> *) a. MonadBlock m => Blocked a -> m a
fromBlocked forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
    El Sort' Term
_ Dummy{} -> forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => Dom Type
__DUMMY_DOM__, forall a. String -> a -> Abs a
Abs String
"x" HasCallStack => Type
__DUMMY_TYPE__)
    Type
t -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
t)

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

-- | A safe variant of 'piApply'.

class PiApplyM a where
  piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type

  piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type
  piApplyM = forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' forall a. HasCallStack => a
__IMPOSSIBLE__

instance PiApplyM Term where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Term -> m Type
piApplyM' m Empty
err Type
t Term
v = forall (tcm :: * -> *) a.
(MonadReduce tcm, HasBuiltins tcm) =>
Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
ifNotPiOrPathType Type
t (\Type
_ -> forall a. Empty -> a
absurd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Empty
err) {-else-} forall a b. (a -> b) -> a -> b
$ \ Dom Type
_ Abs Type
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
v

instance PiApplyM a => PiApplyM (Arg a) where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Arg a -> m Type
piApplyM' m Empty
err Type
t = forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg

instance PiApplyM a => PiApplyM (Named n a) where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> Named n a -> m Type
piApplyM' m Empty
err Type
t = forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing

instance PiApplyM a => PiApplyM [a] where
  piApplyM' :: forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> [a] -> m Type
piApplyM' m Empty
err Type
t = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m Type
mt a
v -> m Type
mt forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type
t -> (forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type -> a -> m Type
piApplyM' m Empty
err Type
t a
v)) (forall (m :: * -> *) a. Monad m => a -> m a
return Type
t)


-- | Compute type arity

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

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

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

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


-- | Register the definition with the given type as an instance.
--   Issue warnings if instance is unusable.
addTypedInstance ::
     QName  -- ^ Name of instance.
  -> Type   -- ^ Type of instance.
  -> TCM ()
addTypedInstance :: QName -> Type -> TCM ()
addTypedInstance = Bool -> QName -> Type -> TCM ()
addTypedInstance' Bool
True

-- | Register the definition with the given type as an instance.
addTypedInstance' ::
     Bool   -- ^ Should we print warnings for unusable instance declarations?
  -> QName  -- ^ Name of instance.
  -> Type   -- ^ Type of instance.
  -> TCM ()
addTypedInstance' :: Bool -> QName -> Type -> TCM ()
addTypedInstance' Bool
w QName
x Type
t = do
  (Tele (Dom Type)
tel , OutputTypeName
n) <- Type -> TCM (Tele (Dom Type), OutputTypeName)
getOutputTypeName Type
t
  case OutputTypeName
n of
    OutputTypeName QName
n            -> QName -> QName -> TCM ()
addNamedInstance QName
x QName
n
    OutputTypeNameNotYetKnown{} -> QName -> TCM ()
addUnknownInstance QName
x
    OutputTypeName
NoOutputTypeName            -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
w forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ Warning
WrongInstanceDeclaration
    OutputTypeName
OutputTypeVar               -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
w forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ Warning
WrongInstanceDeclaration
    OutputTypeName
OutputTypeVisiblePi         -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
w forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> Warning
InstanceWithExplicitArg QName
x

resolveUnknownInstanceDefs :: TCM ()
resolveUnknownInstanceDefs :: TCM ()
resolveUnknownInstanceDefs = do
  Set QName
anonInstanceDefs <- TCM (Set QName)
getAnonInstanceDefs
  TCM ()
clearAnonInstanceDefs
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Set QName
anonInstanceDefs forall a b. (a -> b) -> a -> b
$ \ QName
n -> do
    -- Andreas, 2022-12-04, issue #6380:
    -- Do not warn about unusable instances here.
    Bool -> QName -> Type -> TCM ()
addTypedInstance' Bool
False QName
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
n

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