{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE RecordWildCards #-}

-- | This module contains the definition of hereditary substitution
-- and application operating on internal syntax which is in β-normal
-- form (β including projection reductions).
--
-- Further, it contains auxiliary functions which rely on substitution
-- but not on reduction.

module Mikan.TypeChecking.Substitute
  ( module Mikan.TypeChecking.Substitute
  , module Mikan.TypeChecking.Substitute.Class
  , module Mikan.TypeChecking.Substitute.DeBruijn
  , Substitution'(..), Substitution
  ) where

import Prelude hiding ( zip, zipWith )

import Data.Coerce
import Data.Function (on)
import Data.List qualified as List
import Data.Map (Map)
import Data.Map.Strict qualified as MapS
import Data.Maybe
import Data.HashMap.Strict (HashMap)

import Debug.Trace (trace)

import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Position
import Mikan.Syntax.Internal
import Mikan.Syntax.Abstract qualified as A

import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Monad.Options
import Mikan.TypeChecking.Free as Free
import Mikan.TypeChecking.CompiledClause
import Mikan.TypeChecking.Positivity.Occurrence as Occ

import Mikan.TypeChecking.Substitute.Class
import Mikan.TypeChecking.Substitute.DeBruijn

import Mikan.Utils.Either
import Mikan.Utils.Empty
import Mikan.Utils.Function (applyUnless, ($$!))
import Mikan.Utils.Functor
import Mikan.Utils.Impossible
import Mikan.Utils.List
import Mikan.Utils.List1 (List1, pattern (:|))
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe.Strict qualified as Strict
import Mikan.Utils.Monad
import Mikan.Utils.Permutation
import Mikan.Utils.Size
import Mikan.Utils.Tuple


{-# INLINE applyTermE #-}
-- | Apply @Elims@ while using the given function to report ill-typed
--   redexes.
--   Recursive calls for @applyE@ and @applySubst@ happen at type @t@ to
--   propagate the same strategy to subtrees.
applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t)
           => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE :: forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE Empty -> Term -> Elims -> Term
err' = \t
m Elims
es -> case Elims
es of
  [] -> t
m
  Elims
es -> Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$
    case t -> Term
forall a b. Coercible a b => a -> b
coerce t
m of
      Var Int
i Elims
es'   -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
      Def QName
f Elims
es'   -> QName -> Elims -> Elims -> Term
defApp QName
f Elims
es' Elims
es  -- remove projection redexes
      Con ConHead
c ConInfo
ci Elims
args -> forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
err' ConHead
c ConInfo
ci Elims
args Elims
es
      Lam ArgInfo
_ Abs Term
b     ->
        case Elims
es of
          Apply Arg Term
a : Elims
es0      -> Abs t -> SubstArg t -> t
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs Term -> Abs t
forall a b. Coercible a b => a -> b
coerce Abs Term
b :: Abs t) (Term -> SubstArg t
forall a b. Coercible a b => a -> b
coerce (Term -> SubstArg t) -> Term -> SubstArg t
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) t -> Elims -> Term
forall a. Coercible t a => a -> Elims -> Term
`app` Elims
es0
          IApply Term
_ Term
_ Term
a : Elims
es0 -> Abs t -> SubstArg t -> t
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp (Abs Term -> Abs t
forall a b. Coercible a b => a -> b
coerce Abs Term
b :: Abs t) (Term -> t
forall a b. Coercible a b => a -> b
coerce Term
a)         t -> Elims -> Term
forall a. Coercible t a => a -> Elims -> Term
`app` Elims
es0
          Elims
_                  -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV MetaId
x Elims
es' -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
      Lit{}       -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
      Level{}     -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
      Pi Dom Type
_ Abs Type
_      -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
      Sort Sort
s      -> Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Sort
s Sort -> Elims -> Sort
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
      Dummy DummyTermKind
s Elims
es' -> DummyTermKind -> Elims -> Term
Dummy DummyTermKind
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
      DontCare Term
mv -> Term -> Term
dontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
mv Term -> Elims -> Term
forall a. Coercible t a => a -> Elims -> Term
`app` Elims
es  -- Andreas, 2011-10-02
        -- need to go under DontCare, since "with" might resurrect irrelevant term
   where
     {-# INLINE app #-}
     app :: Coercible t a => a -> Elims -> Term
     app :: forall a. Coercible t a => a -> Elims -> Term
app a
u Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ (a -> t
forall a b. Coercible a b => a -> b
coerce a
u :: t) t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
     err :: Empty -> Term
err Empty
e = Empty -> Term -> Elims -> Term
err' Empty
e (t -> Term
forall a b. Coercible a b => a -> b
coerce t
m) Elims
es

instance Apply Term where
  applyE :: Term -> Elims -> Term
applyE = (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term
forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE Empty -> Term -> Elims -> Term
forall a. Empty -> a
absurd

instance Apply BraveTerm where
  applyE :: BraveTerm -> Elims -> BraveTerm
applyE = (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm
forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE (\ Empty
_ Term
t Elims
es ->  DummyTermKind -> Elims -> Term
Dummy (Term -> DummyTermKind
DummyBrave Term
t) Elims
es)

{-# INLINE canProject #-}
-- | If @v@ is a record or constructed value, @canProject f v@
--   returns its field @f@.
canProject :: QName -> Term -> Maybe (Arg Term)
canProject :: QName -> Term -> Maybe (Arg Term)
canProject QName
f Term
v =
  case Term
v of
    -- Andreas, 2022-06-10, issue #5922: also unfold data projections
    -- (not just record projections).
    (Con (ConHead QName
_ DataOrRecord
_ Induction
_ [QName]
fs) ConInfo
_ Elims
vs) -> do
      i <- QName -> [QName] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex QName
f [QName]
fs
      isApplyElim =<< listToMaybe (drop i vs)
    Term
_ -> Maybe (Arg Term)
forall a. Maybe a
Nothing

{-# INLINE conApp #-}
-- | Eliminate a constructed term.
conApp :: forall t. (Coercible t Term, Apply t)
       => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp :: forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp Empty -> Term -> Elims -> Term
fallback ch :: ConHead
ch@(ConHead QName
c DataOrRecord
_ Induction
_ [QName]
fs) ConInfo
ci Elims
args Elims
topEs = Elims -> Term
go Elims
topEs where

  -- print a message when we can't project "f" field
  {-# INLINE traceProjFailure #-}
  traceProjFailure :: forall a. QName -> a -> a
  traceProjFailure :: forall a. QName -> a -> a
traceProjFailure QName
f a
err = QName -> QName -> [QName] -> Elims -> Elims -> a -> a
forall {a} {a} {a} {a} {a}.
(Pretty a, Pretty a, Pretty a, Pretty a) =>
a -> a -> [a] -> [Elim' a] -> [Elim' a] -> a -> a
go QName
c QName
f [QName]
fs Elims
args Elims
topEs a
err where
    {-# NOINLINE go #-} -- Noinline because we don't want GHC to lift thunks out from the definition.
                        -- And we abstract over all free vars because we don't want GHC to make a closure
                        -- for go.
    go :: a -> a -> [a] -> [Elim' a] -> [Elim' a] -> a -> a
go a
c a
f [a]
fs [Elim' a]
args [Elim' a]
es a
err =
      let argsBeforeProj :: [Elim' a]
argsBeforeProj = (Elim' a -> Bool) -> [Elim' a] -> [Elim' a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile' (\case Proj{} -> Bool
False; Elim' a
_ -> Bool
True) ([Elim' a]
args [Elim' a] -> [Elim' a] -> [Elim' a]
forall a. [a] -> [a] -> [a]
++! [Elim' a]
es)
      in [Char] -> a -> a
forall a. [Char] -> a -> a
trace ([[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char]
"conApp: constructor ", a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
c
        , [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
" with fields" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (a -> [Char]) -> [a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++!) ([Char] -> [Char]) -> (a -> [Char]) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) [a]
fs
        , [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
" and args"    [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Elim' a -> [Char]) -> [Elim' a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++!) ([Char] -> [Char]) -> (Elim' a -> [Char]) -> Elim' a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) [Elim' a]
argsBeforeProj
        , [Char]
" projected by ", a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
f
        ]) a
err

  stuck :: Empty -> Term
  stuck :: Empty -> Term
stuck Empty
err = Empty -> Term -> Elims -> Term
fallback Empty
err (ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args) Elims
topEs

  go :: Elims -> Term
  go :: Elims -> Term
go = \case
    []            -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
topEs
    Apply{}  : Elims
es -> Elims -> Term
go Elims
es
    IApply{} : Elims
es -> Elims -> Term
go Elims
es
    Proj ProjOrigin
o QName
f : Elims
es -> [QName] -> Elims -> Term
lookupProj [QName]
fs Elims
args where

      fieldNotFound :: Term
      fieldNotFound :: Term
fieldNotFound = QName -> Term -> Term
forall a. QName -> a -> a
traceProjFailure QName
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term
stuck Empty
forall a. HasCallStack => a
__IMPOSSIBLE__

      -- attempt to return a projected term
      project :: QName -> Arg Term -> Term
      project :: QName -> Arg Term -> Term
project QName
fld Arg Term
a =
        let v :: Term
v = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a in t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
applyE (Term -> t
forall a b. Coercible a b => a -> b
coerce Term
v :: t) Elims
es)

      -- try to look up the projection
      lookupProj :: [QName] -> Elims -> Term
      lookupProj :: [QName] -> Elims -> Term
lookupProj (QName
fld:[QName]
fs) (Elim' Term
a:Elims
args)
        | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
fld = case Elim' Term
a of
            Proj{}       -> QName -> Term -> Term
forall a. QName -> a -> a
traceProjFailure QName
f Term
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Con args never contains Proj
            Apply Arg Term
a      -> QName -> Arg Term -> Term
project QName
fld Arg Term
a
            IApply Term
_ Term
_ Term
a -> QName -> Arg Term -> Term
project QName
fld (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
a)
        | Bool
otherwise = [QName] -> Elims -> Term
lookupProj [QName]
fs Elims
args
      lookupProj [QName]
fs [] = [QName] -> Elims -> Term
lookupFromElims [QName]
fs Elims
topEs -- field is not in the constructor args
      lookupProj [] Elims
_  = Term
fieldNotFound

      -- try to look up the projection from the newly supplied Elims
      lookupFromElims :: [QName] -> Elims -> Term
      lookupFromElims :: [QName] -> Elims -> Term
lookupFromElims (QName
fld:[QName]
fs) (Elim' Term
a:Elims
es)
        | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
fld = case Elim' Term
a of
            Proj{}       -> Term
fieldNotFound -- this happens when we project an under-applied constructor,
                                          -- so the projection is at the index where the field should be
            Apply Arg Term
a      -> QName -> Arg Term -> Term
project QName
fld Arg Term
a
            IApply Term
_ Term
_ Term
a -> QName -> Arg Term -> Term
project QName
fld (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
a)
        | Bool
otherwise = [QName] -> Elims -> Term
lookupFromElims [QName]
fs Elims
es
      lookupFromElims [QName]
_ Elims
_ = Term
fieldNotFound

  -- -- Andreas, 2016-07-20 futile attempt to magically fix ProjOrigin
  --     fallback = v
  -- in  if not $ null es then applyE v es else
  --     -- If we have no more eliminations, we can return v
  --     if o == ProjSystem then fallback else
  --       -- If the result is a projected term with ProjSystem,
  --       -- we can can restore it to ProjOrigin o.
  --       -- Otherwise, we get unpleasant printing with eta-expanded record metas.
  --     caseMaybe (hasElims v) fallback $ \ (hd, es0) ->
  --       caseMaybe (initLast es0) fallback $ \ (es1, e2) ->
  --         case e2 of
  --           -- We want to replace this ProjSystem by o.
  --           Proj ProjSystem q -> hd (es1 ++ [Proj o q])
  --             -- Andreas, 2016-07-21 for the whole testsuite
  --             -- this case was never triggered!
  --           _ -> fallback

-- | @defApp f us vs@ applies @Def f us@ to further arguments @vs@,
--   eliminating top projection redexes.
--   If @us@ is not empty, we cannot have a projection redex, since
--   the record argument is the first one.
defApp :: QName -> Elims -> Elims -> Term
defApp :: QName -> Elims -> Elims -> Term
defApp QName
f [] (Apply Arg Term
a : Elims
es) | Just Arg Term
v <- QName -> Term -> Maybe (Arg Term)
canProject QName
f (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
  = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
defApp QName
f Elims
es0 Elims
es = QName -> Elims -> Term
Def QName
f (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Elims
es0 Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es

-- Andreas, 2016-01-19: In connection with debugging issue #1783,
-- I consider the Apply instance for Type harmful, as piApply is not
-- safe if the type is not sufficiently reduced.
-- (piApply is not in the monad and hence cannot unfold type synonyms).
--
-- Without apply for types, one has to at least use piApply and be
-- aware of doing something which has a precondition
-- (type sufficiently reduced).
--
-- By grepping for piApply, one can quickly get an overview over
-- potentially harmful uses.
--
-- In general, piApplyM is preferable over piApply since it is more robust
-- and fails earlier than piApply, which may only fail at serialization time,
-- when all thunks are forced.

-- REMOVED:
-- instance Apply Type where
--   apply = piApply
--   -- Maybe an @applyE@ instance would be useful here as well.
--   -- A record type could be applied to a projection name
--   -- to yield the field type.
--   -- However, this works only in the monad where we can
--   -- look up the fields of a record type.

instance Apply Sort where
  applyE :: Sort -> Elims -> Sort
applyE Sort
s [] = Sort
s
  applyE Sort
s Elims
es = case Sort
s of
    MetaS MetaId
x Elims
es' -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> Elims -> Sort
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
    DefS  QName
d Elims
es' -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS  QName
d (Elims -> Sort) -> Elims -> Sort
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
    Sort
_ -> Sort
forall a. HasCallStack => a
__IMPOSSIBLE__

-- @applyE@ does not make sense for telecopes, definitions, clauses etc.

instance TermSubst a => Apply (Tele a) where
  apply :: Tele a -> Args -> Tele a
apply Tele a
tel               []       = Tele a
tel
  apply Tele a
EmptyTel          Args
_        = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
  apply (ExtendTel a
_ Abs (Tele a)
tel) (Arg Term
t : Args
ts) = Abs (Tele a) -> SubstArg (Tele a) -> Tele a
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs (Tele a)
tel (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
t) Tele a -> Args -> Tele a
forall t. Apply t => t -> Args -> t
`apply` Args
ts

  applyE :: Tele a -> Elims -> Tele a
applyE Tele a
t Elims
es = Tele a -> Args -> Tele a
forall t. Apply t => t -> Args -> t
apply Tele a
t (Args -> Tele a) -> Args -> Tele a
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply Definition where
  apply :: Definition -> Args -> Definition
apply (Defn ArgInfo
info QName
x Type
t [Polarity]
pol [Occurrence]
occ [Maybe Name]
gpars [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe InstanceInfo
inst Maybe QName
copy Bool
nc Bool
inj Bool
copat Blocked_
blk Bool
hasm Defn
d) Args
args =
    ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe InstanceInfo
-> Maybe QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Bool
-> Defn
-> Definition
Defn ArgInfo
info QName
x (Type -> Args -> Type
piApply Type
t Args
args) ([Polarity] -> Args -> [Polarity]
forall t. Apply t => t -> Args -> t
apply [Polarity]
pol Args
args) ([Occurrence] -> Args -> [Occurrence]
forall t. Apply t => t -> Args -> t
apply [Occurrence]
occ Args
args) (Int -> [Maybe Name] -> [Maybe Name]
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Maybe Name]
gpars)
         [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe InstanceInfo
inst Maybe QName
copy Bool
nc Bool
inj Bool
copat Blocked_
blk Bool
hasm (Defn -> Args -> Defn
forall t. Apply t => t -> Args -> t
apply Defn
d Args
args)

  applyE :: Definition -> Elims -> Definition
applyE Definition
t Elims
es = Definition -> Args -> Definition
forall t. Apply t => t -> Args -> t
apply Definition
t (Args -> Definition) -> Args -> Definition
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance {-# OVERLAPPING #-} Apply [Occ.Occurrence] where
  apply :: [Occurrence] -> Args -> [Occurrence]
apply [Occurrence]
occ Args
args = Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Occurrence]
occ
  applyE :: [Occurrence] -> Elims -> [Occurrence]
applyE [Occurrence]
t Elims
es = [Occurrence] -> Args -> [Occurrence]
forall t. Apply t => t -> Args -> t
apply [Occurrence]
t (Args -> [Occurrence]) -> Args -> [Occurrence]
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance {-# OVERLAPPING #-} Apply [Polarity] where
  apply :: [Polarity] -> Args -> [Polarity]
apply [Polarity]
pol Args
args = Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Polarity]
pol
  applyE :: [Polarity] -> Elims -> [Polarity]
applyE [Polarity]
t Elims
es = [Polarity] -> Args -> [Polarity]
forall t. Apply t => t -> Args -> t
apply [Polarity]
t (Args -> [Polarity]) -> Args -> [Polarity]
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply NumGeneralizableArgs where
  apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs
apply (SomeGeneralizableArgs Int
n) Args
args = Int -> NumGeneralizableArgs
SomeGeneralizableArgs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args)
  applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs
applyE NumGeneralizableArgs
t Elims
es = NumGeneralizableArgs -> Args -> NumGeneralizableArgs
forall t. Apply t => t -> Args -> t
apply NumGeneralizableArgs
t (Args -> NumGeneralizableArgs) -> Args -> NumGeneralizableArgs
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

-- | Make sure we only drop variable patterns.
instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where
  apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]
apply [NamedArg (Pattern' a)]
ps Args
args = Int -> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall {t} {x}.
(Eq t, Num t) =>
t -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [NamedArg (Pattern' a)]
ps where
    loop :: t -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop t
0 [NamedArg (Pattern' x)]
ps = [NamedArg (Pattern' x)]
ps
    loop t
n [] = [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    loop t
n (NamedArg (Pattern' x)
p : [NamedArg (Pattern' x)]
ps) = let recurse :: [NamedArg (Pattern' x)]
recurse = t -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [NamedArg (Pattern' x)]
ps in
      case NamedArg (Pattern' x) -> Pattern' x
forall a. NamedArg a -> a
namedArg NamedArg (Pattern' x)
p of
        VarP{}    -> [NamedArg (Pattern' x)]
recurse
        IApplyP{} -> [NamedArg (Pattern' x)]
recurse
        DotP{}  -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
        LitP{}  -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
        ConP{}  -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
        DefP{}  -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
        ProjP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
        MaskP{} -> [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__

  applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)]
applyE [NamedArg (Pattern' a)]
t Elims
es = [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)]
forall t. Apply t => t -> Args -> t
apply [NamedArg (Pattern' a)]
t (Args -> [NamedArg (Pattern' a)])
-> Args -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply Projection where
  apply :: Projection -> Args -> Projection
apply Projection
p Args
args = Projection
p
    { projIndex = projIndex p - size args
    , projLams  = projLams p `apply` args
    }
  applyE :: Projection -> Elims -> Projection
applyE Projection
t Elims
es = Projection -> Args -> Projection
forall t. Apply t => t -> Args -> t
apply Projection
t (Args -> Projection) -> Args -> Projection
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply ProjLams where
  apply :: ProjLams -> Args -> ProjLams
apply (ProjLams [Arg ArgName]
lams) Args
args = [Arg ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$ Int -> [Arg ArgName] -> [Arg ArgName]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Arg ArgName]
lams
  applyE :: ProjLams -> Elims -> ProjLams
applyE ProjLams
t Elims
es = ProjLams -> Args -> ProjLams
forall t. Apply t => t -> Args -> t
apply ProjLams
t (Args -> ProjLams) -> Args -> ProjLams
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply Defn where
  apply :: Defn -> Args -> Defn
apply Defn
d [] = Defn
d
  apply Defn
d Args
args = case Defn
d of
    Axiom{} -> Defn
d
    DataOrRecSig Int
n -> Int -> Defn
DataOrRecSig (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args)
    GeneralizableVar NumGeneralizableArgs
gv -> NumGeneralizableArgs -> Defn
GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
forall a b. (a -> b) -> a -> b
$ NumGeneralizableArgs -> Args -> NumGeneralizableArgs
forall t. Apply t => t -> Args -> t
apply NumGeneralizableArgs
gv Args
args
    AbstractDefn Defn
d -> Defn -> Defn
AbstractDefn (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Defn -> Args -> Defn
forall t. Apply t => t -> Args -> t
apply Defn
d Args
args
    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
inv
            , funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
            , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
_ } ->
      Defn
d { funClauses    = apply cs args
        , funCompiled   = apply cc args
        , funCovering   = apply cov args
        , funInv        = apply inv args
        , funExtLam     = modifySystem (`apply` args) <$> extLam
        }

    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
inv
            , funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
            , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right p0 :: Projection
p0@Projection{ projIndex :: Projection -> Int
projIndex = Int
n0 } } ->
      case Projection
p0 Projection -> Args -> Projection
forall t. Apply t => t -> Args -> t
`apply` Args
args of
        p :: Projection
p@Projection{ projIndex :: Projection -> Int
projIndex = Int
n }
          -- case: applied only to parameters
          | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     -> Defn
d { funProjection = Right p }
          -- case: applied also to record value (and possibly more)
          | Bool
otherwise ->
              Defn
d { funClauses        = apply cs args'
                , funCompiled       = apply cc args'
                , funCovering       = apply cov args'
                , funInv            = apply inv args'
                , funProjection     = if n == 0 && isVar0 then Right p else Left MaybeProjection
                , funExtLam         = modifySystem (\ System
_ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) <$> extLam
                }
              where
                args' :: Args
args' = Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop Int
n0 Args
args
                -- if n == 0 then n0 <= length args (which is at least 1) so we can drop all but one
                isVar0 :: Bool
isVar0 = case (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> [Term]) -> Args -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop (Int
n0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Args
args of [Var Int
0 []] -> Bool
True; [Term]
_ -> Bool
False

    Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
      Defn
d { dataPars = np - size args
        , dataClause     = apply cl args
        }
    Record{ recPars :: Defn -> Int
recPars = Int
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Telescope
recTel = Telescope
tel
          {-, recArgOccurrences = occ-} } ->
      Defn
d { recPars = np - size args
        , recClause = apply cl args, recTel = apply tel args
--        , recArgOccurrences = List.drop (length args) occ
        }
    Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
      Defn
d { conPars = np - size args }
    Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
      Defn
d { primClauses = apply cs args }
    PrimitiveSort{} -> Defn
d

  applyE :: Defn -> Elims -> Defn
applyE Defn
t Elims
es = Defn -> Args -> Defn
forall t. Apply t => t -> Args -> t
apply Defn
t (Args -> Defn) -> Args -> Defn
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply PrimFun where
  apply :: PrimFun -> Args -> PrimFun
apply (PrimFun QName
x Int
ar [Occurrence]
occs Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) Args
args =
    QName
-> Int
-> [Occurrence]
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) (Int -> [Occurrence] -> [Occurrence]
forall a. Int -> [a] -> [a]
drop Int
n [Occurrence]
occs) ((Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \ Args
vs -> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$! Args
args Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++! Args
vs
    where
    n :: Int
n = Args -> Int
forall a. Sized a => a -> Int
size Args
args
  applyE :: PrimFun -> Elims -> PrimFun
applyE PrimFun
t Elims
es = PrimFun -> Args -> PrimFun
forall t. Apply t => t -> Args -> t
apply PrimFun
t (Args -> PrimFun) -> Args -> PrimFun
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply Clause where
    -- This one is a little bit tricksy after the parameter refinement change.
    -- It is assumed that we only apply a clause to "parameters", i.e.
    -- arguments introduced by lambda lifting. The problem is that these aren't
    -- necessarily the first elements of the clause telescope.
    apply :: Clause -> Args -> Clause
apply cls :: Clause
cls@(Clause Range
rl Range
rf Telescope
tel [NamedArg DeBruijnPattern]
ps Maybe Term
b Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) Args
args
      | Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg DeBruijnPattern]
ps = Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
      | Bool
otherwise =
      Range
-> Range
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf
             Telescope
tel'
             (Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
Substitution' (SubstArg [NamedArg DeBruijnPattern])
rhoP ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [NamedArg DeBruijnPattern]
ps)
             (Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Maybe Term))
rho Maybe Term
b)
             (Substitution' (SubstArg (Maybe (Arg Type)))
-> Maybe (Arg Type) -> Maybe (Arg Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Maybe (Arg Type)))
rho Maybe (Arg Type)
t)
             Catchall
catchall
             ClauseRecursive
recursive
             Maybe Bool
unreachable
             ExpandedEllipsis
ell
             Maybe ModuleName
wm
      where
        -- We have
        --  Γ ⊢ args, for some outer context Γ
        --  Δ ⊢ ps,   where Δ is the clause telescope (tel)
        rargs :: [Term]
rargs = (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg (Args -> [Term]) -> Args -> [Term]
forall a b. (a -> b) -> a -> b
$ Args -> Args
forall a. [a] -> [a]
reverse Args
args
        rps :: [NamedArg DeBruijnPattern]
rps   = [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a]
reverse ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
take' (Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [NamedArg DeBruijnPattern]
ps
        n :: Int
n     = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel

        -- This is the new telescope. Created by substituting the args into the
        -- appropriate places in the old telescope. We know where those are by
        -- looking at the deBruijn indices of the patterns.
        tel' :: Telescope
tel' = Int
-> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel Int
n Telescope
tel [NamedArg DeBruijnPattern]
rps [Term]
rargs

        -- We then have to create a substitution from the old telescope to the
        -- new telescope that we can apply to dot patterns and the clause body.
        rhoP :: PatternSubstitution
        rhoP :: PatternSubstitution
rhoP = (Term -> DeBruijnPattern)
-> Int
-> [NamedArg DeBruijnPattern]
-> [Term]
-> PatternSubstitution
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Int
n [NamedArg DeBruijnPattern]
rps [Term]
rargs
        rho :: Substitution' Term
rho  = (Term -> Term)
-> Int
-> [NamedArg DeBruijnPattern]
-> [Term]
-> Substitution' Term
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> Term
forall a. a -> a
id   Int
n [NamedArg DeBruijnPattern]
rps [Term]
rargs

        substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
        substP :: Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i Term
v = Int
-> SubstArg [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern]
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
i (Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Term
v)

        -- Building the substitution from the old telescope to the new. The
        -- interesting case is when we have a variable pattern:
        --  We need Δ′ ⊢ ρ : Δ
        --  where Δ′ = newTel Δ (xⁱ : ps) (v : vs)
        --           = newTel Δ[xⁱ:=v] ps[xⁱ:=v'] vs
        --  Note that we need v' = raise (|Δ| - 1) v, to make Γ ⊢ v valid in
        --  ΓΔ[xⁱ:=v].
        --  A recursive call ρ′ = mkSub (substP i v' ps) vs gets us
        --    Δ′ ⊢ ρ′ : Δ[xⁱ:=v]
        --  so we just need Δ[xⁱ:=v] ⊢ σ : Δ and then ρ = ρ′ ∘ σ.
        --  That's achieved by σ = singletonS i v'.
        mkSub :: EndoSubst a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
        mkSub :: forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
_ Int
_ [] [] = Substitution' a
forall a. Substitution' a
idS
        mkSub Term -> a
tm Int
n (NamedArg DeBruijnPattern
p : [NamedArg DeBruijnPattern]
ps) (Term
v : [Term]
vs) =
          case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
            VarP PatternInfo
_ (DBPatVar ArgName
_ Int
i) -> (Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i Term
v' [NamedArg DeBruijnPattern]
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> a -> Substitution' a
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
i (Term -> a
tm Term
v')
              where v' :: Term
v' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v
            DotP{}  -> (Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n [NamedArg DeBruijnPattern]
ps [Term]
vs
            ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps' -> ((Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n ([NamedArg DeBruijnPattern] -> [Term] -> Substitution' a)
-> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a b. (a -> b) -> a -> b
$! ([NamedArg DeBruijnPattern]
ps' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++! [NamedArg DeBruijnPattern]
ps)) ([Term] -> Substitution' a) -> [Term] -> Substitution' a
forall a b. (a -> b) -> a -> b
$! (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
vs)
            DefP{}  -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
            LitP{}  -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
            ProjP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
            MaskP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
            IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar ArgName
_ Int
i) -> (Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
forall a.
EndoSubst a =>
(Term -> a)
-> Int -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i Term
v' [NamedArg DeBruijnPattern]
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> a -> Substitution' a
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
i (Term -> a
tm Term
v')
              where v' :: Term
v' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v
        mkSub Term -> a
_ Int
_ [NamedArg DeBruijnPattern]
_ [Term]
_ = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- The parameter patterns 'ps' are all variables or dot patterns, or eta
        -- expanded record patterns (issue #2550). If they are variables they
        -- can appear anywhere in the clause telescope. This function
        -- constructs the new telescope with 'vs' substituted for 'ps'.
        -- Example:
        --    tel = (x : A) (y : B) (z : C) (w : D)
        --    ps  = y@3 w@0
        --    vs  = u v
        --    newTel tel ps vs = (x : A) (z : C[u/y])
        newTel :: Nat -> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
        newTel :: Int
-> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel Int
n Telescope
tel [] [] = Telescope
tel
        newTel Int
n Telescope
tel (NamedArg DeBruijnPattern
p : [NamedArg DeBruijnPattern]
ps) (Term
v : [Term]
vs) =
          case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
            VarP PatternInfo
_ (DBPatVar ArgName
_ Int
i) -> Int
-> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> SubstArg (Dom Type) -> Telescope -> Telescope
forall {t} {a}.
(Eq t, Num t, Subst a, Subst (SubstArg a)) =>
t -> SubstArg a -> Tele a -> Tele a
subTel (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
SubstArg (Dom Type)
v Telescope
tel) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v) [NamedArg DeBruijnPattern]
ps) [Term]
vs
            DotP{}              -> Int
-> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel Int
n Telescope
tel [NamedArg DeBruijnPattern]
ps [Term]
vs
            ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps'        -> (Int
-> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel Int
n Telescope
tel ([NamedArg DeBruijnPattern] -> [Term] -> Telescope)
-> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
forall a b. (a -> b) -> a -> b
$! [NamedArg DeBruijnPattern]
ps' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++! [NamedArg DeBruijnPattern]
ps) ([Term] -> Telescope) -> [Term] -> Telescope
forall a b. (a -> b) -> a -> b
$! (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
vs)
            DefP{}  -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
            LitP{}  -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
            ProjP{} -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
            MaskP{} -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
            IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar ArgName
_ Int
i) -> Int
-> Telescope -> [NamedArg DeBruijnPattern] -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> SubstArg (Dom Type) -> Telescope -> Telescope
forall {t} {a}.
(Eq t, Num t, Subst a, Subst (SubstArg a)) =>
t -> SubstArg a -> Tele a -> Tele a
subTel (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
SubstArg (Dom Type)
v Telescope
tel) (Int
-> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
substP Int
i (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v) [NamedArg DeBruijnPattern]
ps) [Term]
vs
        newTel Int
_ Telescope
tel [NamedArg DeBruijnPattern]
_ [Term]
_ = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__

        projections :: ConHead -> Term -> [Term]
        projections :: ConHead -> Term -> [Term]
projections ConHead
c Term
v = [ -- #4528: We might have bogus terms here when printing a clause that
                            --        cannot be taken. To mitigate the problem we use a Def instead
                            --        a Proj elim for data constructors, which at least stops conApp
                            --        from crashing. See #4989 for not printing bogus terms at all.
                            case ConHead -> DataOrRecord
conDataRecord ConHead
c of
                              DataOrRecord
IsData     -> QName -> Elims -> Elims -> Term
defApp QName
f [] [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v)]
                                              -- Andreas, 2022-06-10, issue #5922.
                                              -- This was @Def f [Apply (Arg ai v)]@, but are we sure
                                              -- that @v@ isn't a matching @Con@?  The testcase for
                                              -- #5922 does not require this precaution,
                                              -- but I sleep better this way...
                              IsRecord{} -> Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
                          | QName
f <- ConHead -> [QName]
conFields ConHead
c ]

        -- subTel i v (Δ₁ (xᵢ : A) Δ₂) = Δ₁ Δ₂[xᵢ = v]
        subTel :: t -> SubstArg a -> Tele a -> Tele a
subTel t
i SubstArg a
v Tele a
EmptyTel = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
        subTel t
0 SubstArg a
v (ExtendTel a
_ Abs (Tele a)
tel) = Abs (Tele a) -> SubstArg (Tele a) -> Tele a
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs (Tele a)
tel SubstArg a
SubstArg (Tele a)
v
        subTel t
i SubstArg a
v (ExtendTel a
a Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel a
a (Abs (Tele a) -> Tele a) -> Abs (Tele a) -> Tele a
forall a b. (a -> b) -> a -> b
$ t -> SubstArg a -> Tele a -> Tele a
subTel (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Int -> SubstArg a -> SubstArg a
forall a. Subst a => Int -> a -> a
raise Int
1 SubstArg a
v) (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

    applyE :: Clause -> Elims -> Clause
applyE Clause
t Elims
es = Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
apply Clause
t (Args -> Clause) -> Args -> Clause
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply CompiledClauses where
  apply :: CompiledClauses -> Args -> CompiledClauses
apply CompiledClauses
cc Args
args = case CompiledClauses
cc of
    Fail [Arg ArgName]
hs -> [Arg ArgName] -> CompiledClauses
forall a. [Arg ArgName] -> CompiledClauses' a
Fail (Int -> [Arg ArgName] -> [Arg ArgName]
forall a. Int -> [a] -> [a]
drop Int
len [Arg ArgName]
hs)
    Done Int
no ClauseRecursive
mr [Arg ArgName]
hs Term
t
      | [Arg ArgName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg ArgName]
hs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len ->
         let sub :: Substitution' Term
sub = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$! ((Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var [Int
0..[Arg ArgName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg ArgName]
hs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg Args
args)
         in  Int -> ClauseRecursive -> [Arg ArgName] -> Term -> CompiledClauses
forall a.
Int -> ClauseRecursive -> [Arg ArgName] -> a -> CompiledClauses' a
Done Int
no ClauseRecursive
mr (Int -> [Arg ArgName] -> [Arg ArgName]
forall a. Int -> [a] -> [a]
List.drop Int
len [Arg ArgName]
hs) (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
sub Term
t
      | Bool
otherwise -> CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__
    Case Arg Int
n Case CompiledClauses
bs
      | Arg Int -> Int
forall e. Arg e -> e
unArg Arg Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Arg Int
n Arg Int -> (Int -> Int) -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Int
m -> Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len) (Case CompiledClauses -> Args -> Case CompiledClauses
forall t. Apply t => t -> Args -> t
apply Case CompiledClauses
bs Args
args)
      | Bool
otherwise -> CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__
    where
      len :: Int
len = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args
  applyE :: CompiledClauses -> Elims -> CompiledClauses
applyE CompiledClauses
t Elims
es = CompiledClauses -> Args -> CompiledClauses
forall t. Apply t => t -> Args -> t
apply CompiledClauses
t (Args -> CompiledClauses) -> Args -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply ExtLamInfo where
  apply :: ExtLamInfo -> Args -> ExtLamInfo
apply (ExtLamInfo ModuleName
m Bool
b Maybe System
sys) Args
args = ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
m Bool
b (Maybe System -> Args -> Maybe System
forall t. Apply t => t -> Args -> t
apply Maybe System
sys Args
args)
  applyE :: ExtLamInfo -> Elims -> ExtLamInfo
applyE ExtLamInfo
t Elims
es = ExtLamInfo -> Args -> ExtLamInfo
forall t. Apply t => t -> Args -> t
apply ExtLamInfo
t (Args -> ExtLamInfo) -> Args -> ExtLamInfo
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply System where
  -- We assume we apply a system only to arguments introduced by
  -- lambda lifting.
  apply :: System -> Args -> System
apply (System Telescope
tel [(Face, Term)]
sys) Args
args
      = if Int
nargs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
ntel then System
forall a. HasCallStack => a
__IMPOSSIBLE__
        else Telescope -> [(Face, Term)] -> System
System Telescope
newTel (((Face, Term) -> (Face, Term)) -> [(Face, Term)] -> [(Face, Term)]
forall a b. (a -> b) -> [a] -> [b]
map'' (((Term, Bool) -> (Term, Bool)) -> Face -> Face
forall a b. (a -> b) -> [a] -> [b]
map'' (Term -> Term
f (Term -> Term) -> (Bool -> Bool) -> (Term, Bool) -> (Term, Bool)
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')
*** Bool -> Bool
forall a. a -> a
id) (Face -> Face) -> (Term -> Term) -> (Face, Term) -> (Face, Term)
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')
*** Term -> Term
f) [(Face, Term)]
sys)

    where
      f :: Term -> Term
f = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
sigma
      nargs :: Int
nargs = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args
      ntel :: Int
ntel = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
      newTel :: Telescope
newTel = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
args
      -- newTel ⊢ σ : tel
      sigma :: Substitution' Term
sigma = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
ntel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nargs) ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map'' Arg Term -> Term
forall e. Arg e -> e
unArg Args
args))

  applyE :: System -> Elims -> System
applyE System
t Elims
es = System -> Args -> System
forall t. Apply t => t -> Args -> t
apply System
t (Args -> System) -> Args -> System
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply a => Apply (WithArity a) where
  apply :: WithArity a -> Args -> WithArity a
apply  (WithArity Int
n a
a) Args
args = Int -> a -> WithArity a
forall c. Int -> c -> WithArity c
WithArity Int
n (a -> WithArity a) -> a -> WithArity a
forall a b. (a -> b) -> a -> b
$ a -> Args -> a
forall t. Apply t => t -> Args -> t
apply  a
a Args
args
  applyE :: WithArity a -> Elims -> WithArity a
applyE (WithArity Int
n a
a) Elims
es   = Int -> a -> WithArity a
forall c. Int -> c -> WithArity c
WithArity Int
n (a -> WithArity a) -> a -> WithArity a
forall a b. (a -> b) -> a -> b
$ a -> Elims -> a
forall t. Apply t => t -> Elims -> t
applyE a
a Elims
es

instance Apply a => Apply (Case a) where
  apply :: Case a -> Args -> Case a
apply (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) Args
args =
    Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop (Map QName (WithArity a) -> Args -> Map QName (WithArity a)
forall t. Apply t => t -> Args -> t
apply Map QName (WithArity a)
cs Args
args) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (WithArity a -> Args -> WithArity a
forall t. Apply t => t -> Args -> t
`apply` Args
args) ((ConHead, WithArity a) -> (ConHead, WithArity a))
-> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConHead, WithArity a)
eta) (Map Literal a -> Args -> Map Literal a
forall t. Apply t => t -> Args -> t
apply Map Literal a
ls Args
args) (Maybe a -> Args -> Maybe a
forall t. Apply t => t -> Args -> t
apply Maybe a
m Args
args) Maybe Bool
b Bool
lz
  applyE :: Case a -> Elims -> Case a
applyE (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) Elims
es =
    Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop (Map QName (WithArity a) -> Elims -> Map QName (WithArity a)
forall t. Apply t => t -> Elims -> t
applyE Map QName (WithArity a)
cs Elims
es) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (WithArity a -> Elims -> WithArity a
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) ((ConHead, WithArity a) -> (ConHead, WithArity a))
-> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConHead, WithArity a)
eta)(Map Literal a -> Elims -> Map Literal a
forall t. Apply t => t -> Elims -> t
applyE Map Literal a
ls Elims
es) (Maybe a -> Elims -> Maybe a
forall t. Apply t => t -> Elims -> t
applyE Maybe a
m Elims
es) Maybe Bool
b Bool
lz

instance Apply FunctionInverse where
  apply :: FunctionInverse -> Args -> FunctionInverse
apply FunctionInverse
NotInjective  Args
args = FunctionInverse
forall c. FunctionInverse' c
NotInjective
  apply (Inverse InversionMap Clause
inv) Args
args = InversionMap Clause -> FunctionInverse
forall c. InversionMap c -> FunctionInverse' c
Inverse (InversionMap Clause -> FunctionInverse)
-> InversionMap Clause -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ InversionMap Clause -> Args -> InversionMap Clause
forall t. Apply t => t -> Args -> t
apply InversionMap Clause
inv Args
args

  applyE :: FunctionInverse -> Elims -> FunctionInverse
applyE FunctionInverse
t Elims
es = FunctionInverse -> Args -> FunctionInverse
forall t. Apply t => t -> Args -> t
apply FunctionInverse
t (Args -> FunctionInverse) -> Args -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Apply DisplayTerm where
  apply :: DisplayTerm -> Args -> DisplayTerm
apply (DTerm' Term
v Elims
es)      Args
args = Term -> Elims -> DisplayTerm
DTerm' Term
v       (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)
  apply (DDot' Term
v Elims
es)       Args
args = Term -> Elims -> DisplayTerm
DDot' Term
v        (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)
  apply (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs)     Args
args = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci      ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Arg DisplayTerm]
vs [Arg DisplayTerm] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Arg DisplayTerm) -> Args -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
args)
  apply (DDef QName
c [Elim' DisplayTerm]
es)        Args
args = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c         ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Elim' DisplayTerm]
es [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' DisplayTerm) -> Args -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
args)
  apply (DWithApp DisplayTerm
v List1 DisplayTerm
ws Elims
es) Args
args = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp DisplayTerm
v List1 DisplayTerm
ws  (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)

  applyE :: DisplayTerm -> Elims -> DisplayTerm
applyE (DTerm' Term
v Elims
es')      Elims
es = Term -> Elims -> DisplayTerm
DTerm' Term
v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
  applyE (DDot' Term
v Elims
es')       Elims
es = Term -> Elims -> DisplayTerm
DDot' Term
v (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es
  applyE (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs)      Elims
es = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Arg DisplayTerm]
vs [Arg DisplayTerm] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall a. [a] -> [a] -> [a]
++! (Arg Term -> Arg DisplayTerm) -> Args -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
ws
    where ws :: Args
ws = Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
  applyE (DDef QName
c [Elim' DisplayTerm]
es')        Elims
es = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! [Elim' DisplayTerm]
es' [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++! (Elim' Term -> Elim' DisplayTerm) -> Elims -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> DisplayTerm) -> Elim' Term -> Elim' DisplayTerm
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es
  applyE (DWithApp DisplayTerm
v List1 DisplayTerm
ws Elims
es') Elims
es = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp DisplayTerm
v List1 DisplayTerm
ws (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
es

instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where
  apply :: [t] -> Args -> [t]
apply  [t]
ts Args
args = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map'' (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) [t]
ts
  applyE :: [t] -> Elims -> [t]
applyE [t]
ts Elims
es   = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map'' (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) [t]
ts

instance Apply t => Apply (Blocked t) where
  apply :: Blocked t -> Args -> Blocked t
apply  Blocked t
b Args
args = (t -> t) -> Blocked t -> Blocked t
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) Blocked t
b
  applyE :: Blocked t -> Elims -> Blocked t
applyE Blocked t
b Elims
es   = (t -> t) -> Blocked t -> Blocked t
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Blocked t
b

instance Apply t => Apply (Maybe t) where
  apply :: Maybe t -> Args -> Maybe t
apply  Maybe t
x Args
args = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) Maybe t
x
  applyE :: Maybe t -> Elims -> Maybe t
applyE Maybe t
x Elims
es   = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Maybe t
x

instance Apply t => Apply (Strict.Maybe t) where
  apply :: Maybe t -> Args -> Maybe t
apply  Maybe t
x Args
args = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Args -> t
forall t. Apply t => t -> Args -> t
`apply` Args
args) Maybe t
x
  applyE :: Maybe t -> Elims -> Maybe t
applyE Maybe t
x Elims
es   = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Maybe t
x

instance Apply v => Apply (Map k v) where
  apply :: Map k v -> Args -> Map k v
apply  Map k v
x Args
args = (v -> v) -> Map k v -> Map k v
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Args -> v
forall t. Apply t => t -> Args -> t
`apply` Args
args) Map k v
x
  applyE :: Map k v -> Elims -> Map k v
applyE Map k v
x Elims
es   = (v -> v) -> Map k v -> Map k v
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Elims -> v
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) Map k v
x

instance Apply v => Apply (HashMap k v) where
  apply :: HashMap k v -> Args -> HashMap k v
apply  HashMap k v
x Args
args = (v -> v) -> HashMap k v -> HashMap k v
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Args -> v
forall t. Apply t => t -> Args -> t
`apply` Args
args) HashMap k v
x
  applyE :: HashMap k v -> Elims -> HashMap k v
applyE HashMap k v
x Elims
es   = (v -> v) -> HashMap k v -> HashMap k v
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> Elims -> v
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es) HashMap k v
x

instance (Apply a, Apply b) => Apply (a,b) where
  apply :: (a, b) -> Args -> (a, b)
apply  (a
x,b
y) Args
args = (a -> Args -> a
forall t. Apply t => t -> Args -> t
apply  a
x Args
args, b -> Args -> b
forall t. Apply t => t -> Args -> t
apply  b
y Args
args)
  applyE :: (a, b) -> Elims -> (a, b)
applyE (a
x,b
y) Elims
es   = (a -> Elims -> a
forall t. Apply t => t -> Elims -> t
applyE a
x Elims
es  , b -> Elims -> b
forall t. Apply t => t -> Elims -> t
applyE b
y Elims
es  )

instance (Apply a, Apply b, Apply c) => Apply (a,b,c) where
  apply :: (a, b, c) -> Args -> (a, b, c)
apply  (a
x,b
y,c
z) Args
args = (a -> Args -> a
forall t. Apply t => t -> Args -> t
apply  a
x Args
args, b -> Args -> b
forall t. Apply t => t -> Args -> t
apply  b
y Args
args, c -> Args -> c
forall t. Apply t => t -> Args -> t
apply  c
z Args
args)
  applyE :: (a, b, c) -> Elims -> (a, b, c)
applyE (a
x,b
y,c
z) Elims
es   = (a -> Elims -> a
forall t. Apply t => t -> Elims -> t
applyE a
x Elims
es  , b -> Elims -> b
forall t. Apply t => t -> Elims -> t
applyE b
y Elims
es  , c -> Elims -> c
forall t. Apply t => t -> Elims -> t
applyE c
z Elims
es  )

instance DoDrop a => Apply (Drop a) where
  apply :: Drop a -> Args -> Drop a
apply Drop a
x Args
args = Int -> Drop a -> Drop a
forall a. DoDrop a => Int -> Drop a -> Drop a
dropMore (Args -> Int
forall a. Sized a => a -> Int
size Args
args) Drop a
x
  applyE :: Drop a -> Elims -> Drop a
applyE Drop a
t Elims
es = Drop a -> Args -> Drop a
forall t. Apply t => t -> Args -> t
apply Drop a
t (Args -> Drop a) -> Args -> Drop a
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance DoDrop a => Abstract (Drop a) where
  abstract :: Telescope -> Drop a -> Drop a
abstract Telescope
tel Drop a
x = Int -> Drop a -> Drop a
forall a. DoDrop a => Int -> Drop a -> Drop a
unDrop (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Drop a
x

instance Apply Permutation where
  -- The permutation must start with [0..m - 1]
  apply :: Permutation -> Args -> Permutation
apply (Perm Int
n [Int]
xs) Args
args = Int -> [Int] -> Permutation
Perm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$! (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
m) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop Int
m [Int]
xs
    where
      m :: Int
m = Args -> Int
forall a. Sized a => a -> Int
size Args
args

  applyE :: Permutation -> Elims -> Permutation
applyE Permutation
t Elims
es = Permutation -> Args -> Permutation
forall t. Apply t => t -> Args -> t
apply Permutation
t (Args -> Permutation) -> Args -> Permutation
forall a b. (a -> b) -> a -> b
$ Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es

instance Abstract Permutation where
  abstract :: Telescope -> Permutation -> Permutation
abstract Telescope
tel (Perm Int
n [Int]
xs) = Int -> [Int] -> Permutation
Perm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) ([Int] -> Permutation) -> [Int] -> Permutation
forall a b. (a -> b) -> a -> b
$! [Int
0..Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++! ((Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) [Int]
xs)
    where
      m :: Int
m = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel

-- | @(x:A)->B(x) `piApply` [u] = B(u)@
--
--   Precondition: The type must contain the right number of pis without
--   having to perform any reduction.
--
--   @piApply@ is potentially unsafe, the monadic 'piApplyM' is preferable.
piApply :: Type -> Args -> Type
piApply :: Type -> Args -> Type
piApply = Substitution' Term -> Type -> Args -> Type
loop Substitution' Term
forall a. Substitution' a
idS where
  loop :: Substitution' Term -> Type -> Args -> Type
loop !Substitution' Term
rho !Type
t [] = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
rho Type
t

  -- manifest pi-type: accumulate substitution
  loop Substitution' Term
rho (El Sort
_ (Pi  Dom Type
_ Abs Type
b)) (Arg Term
a:Args
args) = case Abs Type
b of
    NoAbs ArgName
_ Type
b -> Substitution' Term -> Type -> Args -> Type
loop Substitution' Term
rho Type
b Args
args
    Abs   ArgName
_ Type
b -> Substitution' Term -> Type -> Args -> Type
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a Term -> Substitution' Term -> Substitution' Term
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' Term
rho) Type
b Args
args

  -- not a manifest pi-type: if we have a nontrivial substitution, could
  -- become a pi type after substitution; force the substitution and
  -- reset the accumulator.
  --
  -- otherwise, it's a violation of the invariant.
  loop Substitution' Term
rho Type
t (Arg Term
a:Args
args) = case Substitution' Term
rho of
    Substitution' Term
IdS -> [Char] -> Type -> Type
forall a. [Char] -> a -> a
trace ([Char]
"piApply t = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
"\n  args = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Args -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Args
args) Type
forall a. HasCallStack => a
__IMPOSSIBLE__
    Substitution' Term
_   -> Substitution' Term -> Type -> Args -> Type
loop Substitution' Term
forall a. Substitution' a
idS (Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
rho Type
t) (Arg Term
aArg Term -> Args -> Args
forall a. a -> [a] -> [a]
:Args
args)

---------------------------------------------------------------------------
-- * Abstraction
---------------------------------------------------------------------------

-- | Abstract over a telescope in a term, producing lambdas.
-- Dumb abstraction: Always produces 'Abs', never 'NoAbs'.
--
-- The implementation is sound because 'Telescope' does not use
-- 'NoAbs'.
instance Abstract Term where
  abstract :: Telescope -> Term -> Term
abstract = (Term -> Telescope -> Term) -> Telescope -> Term -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term -> Telescope -> Term
loop where
    {-# INLINABLE loop #-}

    loop :: Term -> Telescope -> Term
    loop :: Term -> Telescope -> Term
loop Term
t Telescope
EmptyTel          = Term
t
    loop Term
t (ExtendTel Dom Type
u Abs Telescope
tel) = ArgInfo -> Abs Term -> Term
Lam (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
u) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$! Term -> Telescope -> Term
loop Term
t (Telescope -> Term) -> Abs Telescope -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Telescope
tel

instance Abstract Type where
  abstract :: Telescope -> Type -> Type
abstract = Telescope -> Type -> Type
telePi_

instance Abstract Telescope where
  Telescope
EmptyTel           abstract :: Telescope -> Telescope -> Telescope
`abstract` Telescope
tel = Telescope
tel
  ExtendTel Dom Type
arg Abs Telescope
xtel `abstract` Telescope
tel = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
arg (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Abs Telescope
xtel Abs Telescope -> (Telescope -> Telescope) -> Abs Telescope
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
tel)

instance Abstract Definition where
  abstract :: Telescope -> Definition -> Definition
abstract Telescope
tel defn :: Definition
defn@Defn{Bool
[Maybe Name]
[Occurrence]
[Polarity]
[LocalDisplayForm]
Maybe QName
Maybe InstanceInfo
CompiledRepresentation
ArgInfo
QName
Blocked_
Type
Defn
MutualId
defArgInfo :: ArgInfo
defName :: QName
defType :: Type
defPolarity :: [Polarity]
defArgOccurrences :: [Occurrence]
defGeneralizedParams :: [Maybe Name]
defDisplay :: [LocalDisplayForm]
defMutual :: MutualId
defCompiledRep :: CompiledRepresentation
defInstance :: Maybe InstanceInfo
defCopy :: Maybe QName
defNoCompilation :: Bool
defInjective :: Bool
defCopatternLHS :: Bool
defBlocked :: Blocked_
defMightContainMetas :: Bool
theDef :: Defn
defArgInfo :: Definition -> ArgInfo
defArgOccurrences :: Definition -> [Occurrence]
defBlocked :: Definition -> Blocked_
defCompiledRep :: Definition -> CompiledRepresentation
defCopatternLHS :: Definition -> Bool
defCopy :: Definition -> Maybe QName
defDisplay :: Definition -> [LocalDisplayForm]
defGeneralizedParams :: Definition -> [Maybe Name]
defInjective :: Definition -> Bool
defInstance :: Definition -> Maybe InstanceInfo
defMightContainMetas :: Definition -> Bool
defMutual :: Definition -> MutualId
defName :: Definition -> QName
defNoCompilation :: Definition -> Bool
defPolarity :: Definition -> [Polarity]
defType :: Definition -> Type
theDef :: Definition -> Defn
..} = Definition
defn
    { defType              = abstract tel defType
    , defPolarity          = abstract tel defPolarity
    , defArgOccurrences    = abstract tel defArgOccurrences
    , defGeneralizedParams = replicate' (size tel) Nothing ++! defGeneralizedParams
    , theDef               = abstract tel theDef
    }

instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where
  abstract :: Telescope -> [Occurrence] -> [Occurrence]
abstract Telescope
tel []  = []
  abstract Telescope
tel [Occurrence]
occ = Int -> Occurrence -> [Occurrence]
forall a. Int -> a -> [a]
replicate' (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Occurrence
Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++! [Occurrence]
occ -- TODO: check occurrence

instance {-# OVERLAPPING #-} Abstract [Polarity] where
  abstract :: Telescope -> [Polarity] -> [Polarity]
abstract Telescope
tel []  = []
  abstract Telescope
tel [Polarity]
pol = Int -> Polarity -> [Polarity]
forall a. Int -> a -> [a]
replicate' (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Polarity
Invariant [Polarity] -> [Polarity] -> [Polarity]
forall a. [a] -> [a] -> [a]
++! [Polarity]
pol -- TODO: check polarity

instance Abstract NumGeneralizableArgs where
  abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
abstract Telescope
tel (SomeGeneralizableArgs Int
n) = Int -> NumGeneralizableArgs
SomeGeneralizableArgs (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)

instance Abstract Projection where
  abstract :: Telescope -> Projection -> Projection
abstract Telescope
tel Projection
p = Projection
p
    { projIndex = size tel + projIndex p
    , projLams  = abstract tel $ projLams p
    }

instance Abstract ProjLams where
  abstract :: Telescope -> ProjLams -> ProjLams
abstract Telescope
tel (ProjLams [Arg ArgName]
lams) = [Arg ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$!
    ((Dom' Term (ArgName, Type) -> Arg ArgName)
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' (\ !Dom' Term (ArgName, Type)
dom -> Dom' Term ArgName -> Arg ArgName
forall t a. Dom' t a -> Arg a
argFromDom ((ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type) -> ArgName)
-> Dom' Term (ArgName, Type) -> Dom' Term ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (ArgName, Type)
dom)) (Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel)) [Arg ArgName] -> [Arg ArgName] -> [Arg ArgName]
forall a. [a] -> [a] -> [a]
++! [Arg ArgName]
lams

instance Abstract System where
  abstract :: Telescope -> System -> System
abstract Telescope
tel (System Telescope
tel1 [(Face, Term)]
sys) = Telescope -> [(Face, Term)] -> System
System (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel1) [(Face, Term)]
sys

instance Abstract Defn where
  abstract :: Telescope -> Defn -> Defn
abstract Telescope
tel Defn
d = case Defn
d of
    Axiom{} -> Defn
d
    DataOrRecSig Int
n -> Int -> Defn
DataOrRecSig (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
    GeneralizableVar NumGeneralizableArgs
gv -> NumGeneralizableArgs -> Defn
GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
forall a b. (a -> b) -> a -> b
$ Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel NumGeneralizableArgs
gv
    AbstractDefn Defn
d -> Defn -> Defn
AbstractDefn (Defn -> Defn) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Telescope -> Defn -> Defn
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Defn
d
    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
inv
            , funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
            , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
_  } ->
      Defn
d { funClauses  = abstract tel cs
        , funCompiled = abstract tel cc
        , funCovering = abstract tel cov
        , funInv      = abstract tel inv
        , funExtLam   = modifySystem (abstract tel) <$> extLam
        }
    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
inv
            , funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
            , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p } ->
      -- Andreas, 2015-05-11 if projection was applied to Var 0
      -- then abstract over last element of tel (the others are params).
      if Projection -> Int
projIndex Projection
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then
        Defn
d { funProjection = Right $ abstract tel p
          , funClauses    = map' (abstractClause EmptyTel) cs
          }
      else
        Defn
d { funProjection = Right $ abstract tel p
          , funClauses    = map' (abstractClause tel1) cs
          , funCompiled   = abstract tel1 cc
          , funCovering   = abstract tel1 cov
          , funInv        = abstract tel1 inv
          , funExtLam     = modifySystem (\ System
_ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) <$> extLam
          }
        where
          tel1 :: Telescope
tel1 = [Dom' Term (ArgName, Type)] -> Telescope
telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
-> [Dom' Term (ArgName, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. Int -> [a] -> [a]
drop (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
          -- #5128: clause telescopes should be abstracted over the full telescope, regardless of
          --        projection shenanigans.
          abstractClause :: Telescope -> Clause -> Clause
abstractClause Telescope
tel1 Clause
c = (Telescope -> Clause -> Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 Clause
c) { clauseTel = abstract tel $ clauseTel c }

    Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
      Defn
d { dataPars       = np + size tel
        , dataClause     = abstract tel cl
        }
    Record{ recPars :: Defn -> Int
recPars = Int
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recTel :: Defn -> Telescope
recTel = Telescope
tel' } ->
      Defn
d { recPars    = np + size tel
        , recClause  = abstract tel cl
        , recTel     = abstract tel tel'
        }
    Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
      Defn
d { conPars = np + size tel }
    Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
      Defn
d { primClauses = abstract tel cs }
    PrimitiveSort{} -> Defn
d

instance Abstract PrimFun where
    abstract :: Telescope -> PrimFun -> PrimFun
abstract Telescope
tel (PrimFun QName
x Int
ar [Occurrence]
occs Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) =
      QName
-> Int
-> [Occurrence]
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) (Int -> Occurrence -> [Occurrence]
forall a. Int -> a -> [a]
replicate' Int
n Occurrence
Mixed [Occurrence] -> [Occurrence] -> [Occurrence]
forall a. [a] -> [a] -> [a]
++! [Occurrence]
occs) ((Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
 -> PrimFun)
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
forall a b. (a -> b) -> a -> b
$ \Args
ts ->
        Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
forall a b. (a -> b) -> a -> b
$ Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop Int
n Args
ts
        where n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel

instance Abstract Clause where
  abstract :: Telescope -> Clause -> Clause
abstract Telescope
tel (Clause Range
rl Range
rf Telescope
tel' [NamedArg DeBruijnPattern]
ps Maybe Term
b Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
    Range
-> Range
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel')
           (Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars Int
m Telescope
tel [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++! [NamedArg DeBruijnPattern]
ps)
           Maybe Term
b
           Maybe (Arg Type)
t -- nothing to do for t, since it lives under the telescope
           Catchall
catchall
           ClauseRecursive
recursive
           Maybe Bool
unreachable
           ExpandedEllipsis
ell
           Maybe ModuleName
wm
      where m :: Int
m = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel'

instance Abstract CompiledClauses where
  abstract :: Telescope -> CompiledClauses -> CompiledClauses
abstract Telescope
tel CompiledClauses
cc = case CompiledClauses
cc of
      Fail [Arg ArgName]
xs         -> [Arg ArgName] -> CompiledClauses
forall a. [Arg ArgName] -> CompiledClauses' a
Fail ([Arg ArgName]
hs [Arg ArgName] -> [Arg ArgName] -> [Arg ArgName]
forall a. [a] -> [a] -> [a]
++! [Arg ArgName]
xs)
      Done Int
no ClauseRecursive
mr [Arg ArgName]
xs Term
t -> Int -> ClauseRecursive -> [Arg ArgName] -> Term -> CompiledClauses
forall a.
Int -> ClauseRecursive -> [Arg ArgName] -> a -> CompiledClauses' a
Done Int
no ClauseRecursive
mr ([Arg ArgName]
hs [Arg ArgName] -> [Arg ArgName] -> [Arg ArgName]
forall a. [a] -> [a] -> [a]
++! [Arg ArgName]
xs) Term
t
      Case Arg Int
n Case CompiledClauses
bs       -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Arg Int
n Arg Int -> (Int -> Int) -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Int
i -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) (Telescope -> Case CompiledClauses -> Case CompiledClauses
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Case CompiledClauses
bs)
    where
      hs :: [Arg ArgName]
hs = (Dom' Term (ArgName, Type) -> Arg ArgName)
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom' Term ArgName -> Arg ArgName
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term ArgName -> Arg ArgName)
-> (Dom' Term (ArgName, Type) -> Dom' Term ArgName)
-> Dom' Term (ArgName, Type)
-> Arg ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ArgName, Type) -> ArgName)
-> Dom' Term (ArgName, Type) -> Dom' Term ArgName
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst) ([Dom' Term (ArgName, Type)] -> [Arg ArgName])
-> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel

instance Abstract a => Abstract (WithArity a) where
  abstract :: Telescope -> WithArity a -> WithArity a
abstract Telescope
tel (WithArity Int
n a
a) = Int -> a -> WithArity a
forall c. Int -> c -> WithArity c
WithArity Int
n (a -> WithArity a) -> a -> WithArity a
forall a b. (a -> b) -> a -> b
$ Telescope -> a -> a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel a
a

instance Abstract a => Abstract (Case a) where
  abstract :: Telescope -> Case a -> Case a
abstract Telescope
tel (Branches Bool
cop Map QName (WithArity a)
cs Maybe (ConHead, WithArity a)
eta Map Literal a
ls Maybe a
m Maybe Bool
b Bool
lz) =
    Bool
-> Map QName (WithArity a)
-> Maybe (ConHead, WithArity a)
-> Map Literal a
-> Maybe a
-> Maybe Bool
-> Bool
-> Case a
forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop (Telescope -> Map QName (WithArity a) -> Map QName (WithArity a)
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Map QName (WithArity a)
cs) ((WithArity a -> WithArity a)
-> (ConHead, WithArity a) -> (ConHead, WithArity a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Telescope -> WithArity a -> WithArity a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) ((ConHead, WithArity a) -> (ConHead, WithArity a))
-> Maybe (ConHead, WithArity a) -> Maybe (ConHead, WithArity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ConHead, WithArity a)
eta)
                 (Telescope -> Map Literal a -> Map Literal a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Map Literal a
ls) (Telescope -> Maybe a -> Maybe a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe a
m) Maybe Bool
b Bool
lz

telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telVars Int
m = (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) ([NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern])
-> (Telescope -> [NamedArg DeBruijnPattern])
-> Telescope
-> [Arg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars Int
m)

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars Int
m Telescope
EmptyTel             = []
namedTelVars Int
m (ExtendTel !Dom Type
dom Abs Telescope
tel) =
  let !rest :: [NamedArg DeBruijnPattern]
rest = Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel) in
  let !this :: NamedArg DeBruijnPattern
this = ArgInfo
-> Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) (Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern)
-> Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! (Int -> ArgName -> Named NamedName DeBruijnPattern
namedDBVarP (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (ArgName -> Named NamedName DeBruijnPattern)
-> ArgName -> Named NamedName DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Abs Telescope -> ArgName
forall a. Abs a -> ArgName
absName Abs Telescope
tel) in
  NamedArg DeBruijnPattern
this NamedArg DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. a -> [a] -> [a]
: [NamedArg DeBruijnPattern]
rest

instance Abstract FunctionInverse where
  abstract :: Telescope -> FunctionInverse -> FunctionInverse
abstract Telescope
tel FunctionInverse
NotInjective  = FunctionInverse
forall c. FunctionInverse' c
NotInjective
  abstract Telescope
tel (Inverse InversionMap Clause
inv) = InversionMap Clause -> FunctionInverse
forall c. InversionMap c -> FunctionInverse' c
Inverse (InversionMap Clause -> FunctionInverse)
-> InversionMap Clause -> FunctionInverse
forall a b. (a -> b) -> a -> b
$ Telescope -> InversionMap Clause -> InversionMap Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel InversionMap Clause
inv

instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where
  abstract :: Telescope -> [t] -> [t]
abstract Telescope
tel = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map'' (Telescope -> t -> t
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel)

instance Abstract t => Abstract (Maybe t) where
  abstract :: Telescope -> Maybe t -> Maybe t
abstract Telescope
tel Maybe t
x = (t -> t) -> Maybe t -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> t -> t
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) Maybe t
x

instance Abstract v => Abstract (Map k v) where
  abstract :: Telescope -> Map k v -> Map k v
abstract Telescope
tel Map k v
m = (v -> v) -> Map k v -> Map k v
forall a b. (a -> b) -> Map k a -> Map k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> v -> v
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) Map k v
m

instance Abstract v => Abstract (HashMap k v) where
  abstract :: Telescope -> HashMap k v -> HashMap k v
abstract Telescope
tel HashMap k v
m = (v -> v) -> HashMap k v -> HashMap k v
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Telescope -> v -> v
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) HashMap k v
m

---------------------------------------------------------------------------
-- * Substitution and shifting\/weakening\/strengthening
---------------------------------------------------------------------------

-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renaming _ π) : Term Γ -> Term Δ@
--   Assumes that π works on de Bruijn _indices_.
renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a
renaming :: forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
err Permutation
p = Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
err [Maybe a]
gamma (Substitution' a -> Substitution' a)
-> Substitution' a -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS (Int -> Substitution' a) -> Int -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Permutation -> Int
forall a. Sized a => a -> Int
size Permutation
p
  where
    gamma :: [Maybe a]
    gamma :: [Maybe a]
gamma = Permutation -> (Int -> a) -> [Maybe a]
forall a b. InversePermute a b => Permutation -> a -> b
inversePermute Permutation
p (Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar :: Int -> a)
    -- gamma = safePermute (invertP (-1) p) $ map deBruijnVar [0..]

-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renamingR π) : Term Δ -> Term Γ@
--   Assumes that π works on de Bruijn _levels_.
renamingR :: DeBruijn a => Permutation -> Substitution' a
renamingR :: forall a. DeBruijn a => Permutation -> Substitution' a
renamingR p :: Permutation
p@(Perm Int
n [Int]
is) = [a]
xs [a] -> Substitution' a -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS Int
n
  where
  xs :: [a]
xs = (Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map' (\Int
i -> Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i)) ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
is)

  -- The list xs used to be defined in the following way:
  --
  --   permute (reverseP p) (map deBruijnVar [0..])
  --
  -- We have that
  --
  --     permute (reverseP p) (map deBruijnVar [0..])
  --   = permute (Perm n $ map ((n - 1) -) $ reverse is)
  --       (map deBruijnVar [0..])
  --   = map (map deBruijnVar [0..] !!)
  --       (map ((n - 1) -) $ reverse is)
  --   = map deBruijnVar (map ((n - 1) -) $ reverse is)
  --   = map (\i -> deBruijnVar (n - 1 - i)) (reverse is).
  --
  -- The latter code is linear in the length of is (if deBruijnVar
  -- takes constant time), while the time complexity of the former
  -- code depends on the value of the largest index in is.

-- | The permutation should permute the corresponding context. (as de Bruijn _indices_)
renameP :: Subst a => Impossible -> Permutation -> a -> a
renameP :: forall a. Subst a => Impossible -> Permutation -> a -> a
renameP Impossible
err Permutation
p = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> Permutation -> Substitution' (SubstArg a)
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
err Permutation
p)

instance EndoSubst a => Subst (Substitution' a) where
  type SubstArg (Substitution' a) = a
  applySubst :: Substitution' (SubstArg (Substitution' a))
-> Substitution' a -> Substitution' a
applySubst Substitution' (SubstArg (Substitution' a))
rho Substitution' a
sgm = Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
Substitution' (SubstArg (Substitution' a))
rho Substitution' a
sgm

{-# INLINE applySubstTerm #-}
applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
applySubstTerm :: forall t.
(Coercible t Term, EndoSubst t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm Substitution' t
IdS t
t = t
t
applySubstTerm Substitution' t
rho t
t    = Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$ case t -> Term
forall a b. Coercible a b => a -> b
coerce t
t of
    Var Int
i Elims
es    -> let !t :: t
t = Substitution' t -> Int -> t
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' t
rho Int
i in t -> Term
forall a b. Coercible a b => a -> b
coerce (t
t t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es)
    Lam ArgInfo
h Abs Term
m     -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$! forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Abs t) Substitution' t
rho Abs Term
m
    Def QName
f Elims
es    -> QName -> Elims -> Elims -> Term
defApp QName
f [] (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es
    Con ConHead
c ConInfo
ci Elims
vs -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
vs
    MetaV MetaId
x Elims
es  -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es
    Lit Literal
l       -> Literal -> Term
Lit Literal
l
    Level Level
l     -> Level -> Term
levelTm (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Level' t) Substitution' t
rho Level
l
    Pi Dom Type
a Abs Type
b      -> Dom Type -> Abs Type -> Term
Pi (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Dom' t (Type'' t t)) Substitution' t
rho Dom Type
a) (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Abs (Type'' t t)) Substitution' t
rho Abs Type
b)
    -- Pi a b      -> Pi (subPiDom rho a) (subPiCod rho b)
    Sort Sort
s      -> Sort -> Term
Sort (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @(Sort' t) Substitution' t
rho Sort
s)
    DontCare Term
mv -> Term -> Term
dontCare (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
mv)
    Dummy DummyTermKind
s Elims
es  -> DummyTermKind -> Elims -> Term
Dummy DummyTermKind
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
es
 where
   sub :: forall a b. (Coercible b a, SubstWith t a) => Substitution' t -> b -> b
   sub :: forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub Substitution' t
rho b
t = a -> b
forall a b. Coercible a b => a -> b
coerce (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' t
Substitution' (SubstArg a)
rho (b -> a
forall a b. Coercible a b => a -> b
coerce b
t :: a)); {-# INLINE sub #-}

   {- András, 2026-03-17: when substituting a term, we don't want to create any thunks until we hit the *next*
      inductive layer of terms.
      But apparently, not for Pi, currently! Forcing Pi seems to cost some checking time in stdlib.
      Below's some commented-out definitions for stricter Pi substitution.
   -}

   -- subPiDom :: Substitution' t -> Dom Type -> Dom Type
   -- subPiDom rho (Dom i n f t (El s a)) =
   --   let !i' = setFreeVariables unknownFreeVariables i in
   --   Dom i' n f $$! (sub @(Maybe t) rho t) $$! (El $$! sub @(Sort' t) rho s $$! sub @t rho a)

   -- subPiCod :: Substitution' t -> Abs Type -> Abs Type
   -- subPiCod rho (Abs x (El s a)) =
   --   let !rho' = liftS 1 rho in
   --   Abs x $$! (El $$! sub @(Sort' t) rho' s $$! sub @t rho' a)
   -- subPiCod rho (NoAbs x (El s a)) =
   --   NoAbs x $! (El $$! sub @(Sort' t) rho s $$! sub @t rho a)

   subE :: Substitution' t -> Elims -> Elims
   subE :: Substitution' t -> Elims -> Elims
subE Substitution' t
rho []     = []
   subE Substitution' t
rho (Elim' Term
a:Elims
as) = case Elim' Term
a of
     Apply (Arg ArgInfo
i Term
t) ->
       let !i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
               | Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i
       in (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i' (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
t))Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
as
     p :: Elim' Term
p@Proj{}        -> (Elim' Term
p Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
as
     IApply Term
l Term
r Term
t    -> (Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
l) (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
r) (forall a b.
(Coercible b a, SubstWith t a) =>
Substitution' t -> b -> b
sub @t Substitution' t
rho Term
t)Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:) (Elims -> Elims) -> Elims -> Elims
forall a b. (a -> b) -> a -> b
$! Substitution' t -> Elims -> Elims
subE Substitution' t
rho Elims
as

instance Subst Term where
  type SubstArg Term = Term
  applySubst :: Substitution' (SubstArg Term) -> Term -> Term
applySubst = Substitution' Term -> Term -> Term
Substitution' (SubstArg Term) -> Term -> Term
forall t.
(Coercible t Term, EndoSubst t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm

-- András 2023-09-25: we can only put this here, because at the original definition site there's no Subst Term instance.
{-# SPECIALIZE weakenLookupS :: Nat -> Substitution' Term -> Nat -> Term #-}
{-# SPECIALIZE lookupS :: Substitution' Term -> Nat -> Term #-}
{-# SPECIALIZE isNoAbs :: Abs Term -> Maybe Term #-}

instance Subst BraveTerm where
  type SubstArg BraveTerm = BraveTerm
  applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
applySubst = Substitution' BraveTerm -> BraveTerm -> BraveTerm
Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm
forall t.
(Coercible t Term, EndoSubst t, Apply t) =>
Substitution' t -> t -> t
applySubstTerm

instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) where
  type SubstArg (Type'' a b) = SubstArg a
  applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b
applySubst Substitution' (SubstArg (Type'' a b))
rho (El Sort' a
s b
t) = Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
Substitution' (SubstArg (Type'' a b))
rho Sort' a
s Sort' a -> b -> Type'' a b
forall t a. Sort' t -> a -> Type'' t a
`El` Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (Type'' a b))
rho b
t

instance Subst a => Subst (Sort' a) where
  type SubstArg (Sort' a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
applySubst Substitution' (SubstArg (Sort' a))
rho = \case
    Univ Univ
u Level' a
n       -> Univ -> Level' a -> Sort' a
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Level' a))
Substitution' (SubstArg (Sort' a))
rho Level' a
n
    Inf Univ
u Integer
n        -> Univ -> Integer -> Sort' a
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
    Sort' a
LevelUniv      -> Sort' a
forall t. Sort' t
LevelUniv
    Sort' a
IntervalUniv   -> Sort' a
forall t. Sort' t
IntervalUniv
    Sort' a
CofUniv        -> Sort' a
forall t. Sort' t
CofUniv
    PiSort Dom' a a
a Sort' a
s1 Abs (Sort' a)
s2 -> ((Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a)
-> Dom' a a -> Sort' a -> Abs (Sort' a) -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Dom' a a)) -> Dom' a a -> Dom' a a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Dom' a a))
Substitution' (SubstArg (Sort' a))
rho Dom' a a
a) (Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s1)) (Abs (Sort' a) -> Sort' a) -> Abs (Sort' a) -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Abs (Sort' a)))
-> Abs (Sort' a) -> Abs (Sort' a)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Abs (Sort' a)))
Substitution' (SubstArg (Sort' a))
rho Abs (Sort' a)
s2
    FunSort Sort' a
s1 Sort' a
s2  -> Sort' a -> Sort' a -> Sort' a
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s1) (Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s2)
    UnivSort Sort' a
s     -> Sort' a -> Sort' a
forall t. Sort' t -> Sort' t
UnivSort (Sort' a -> Sort' a) -> Sort' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho Sort' a
s
    MetaS MetaId
x [Elim' a]
es     -> MetaId -> [Elim' a] -> Sort' a
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
Substitution' (SubstArg (Sort' a))
rho [Elim' a]
es
    DefS QName
d [Elim' a]
es      -> QName -> [Elim' a] -> Sort' a
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d ([Elim' a] -> Sort' a) -> [Elim' a] -> Sort' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
Substitution' (SubstArg (Sort' a))
rho [Elim' a]
es
    s :: Sort' a
s@DummyS{}     -> Sort' a
s
    where
      subE :: Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
      subE :: Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho []     = []
      subE Substitution' (SubstArg a)
rho (Elim' a
a:[Elim' a]
as) = case Elim' a
a of
        Apply (Arg ArgInfo
i a
t) ->
          let !i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
                  | Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i
          in (Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i' (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
t))Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
:) ([Elim' a] -> [Elim' a]) -> [Elim' a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [Elim' a]
as
        p :: Elim' a
p@Proj{}        -> (Elim' a
p Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
:) ([Elim' a] -> [Elim' a]) -> [Elim' a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [Elim' a]
as
        IApply a
l a
r a
t    -> (a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
l) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
r) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
t)Elim' a -> [Elim' a] -> [Elim' a]
forall a. a -> [a] -> [a]
:)
                           ([Elim' a] -> [Elim' a]) -> [Elim' a] -> [Elim' a]
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [Elim' a] -> [Elim' a]
subE Substitution' (SubstArg a)
rho [Elim' a]
as

instance Subst a => Subst (Level' a) where
  type SubstArg (Level' a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a
applySubst Substitution' (SubstArg (Level' a))
rho (Max Integer
n [PlusLevel' a]
as) = Integer -> [PlusLevel' a] -> Level' a
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' a] -> Level' a) -> [PlusLevel' a] -> Level' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> [PlusLevel' a] -> [PlusLevel' a]
forall {a}.
Subst a =>
Substitution' (SubstArg a) -> [PlusLevel' a] -> [PlusLevel' a]
go Substitution' (SubstArg a)
Substitution' (SubstArg (Level' a))
rho [PlusLevel' a]
as where
    go :: Substitution' (SubstArg a) -> [PlusLevel' a] -> [PlusLevel' a]
go Substitution' (SubstArg a)
rho []              = []
    go Substitution' (SubstArg a)
rho (Plus Integer
x a
y : [PlusLevel' a]
as) = (:) (PlusLevel' a -> [PlusLevel' a] -> [PlusLevel' a])
-> PlusLevel' a -> [PlusLevel' a] -> [PlusLevel' a]
forall a b. (a -> b) -> a -> b
$$! (Integer -> a -> PlusLevel' a
forall t. Integer -> t -> PlusLevel' t
Plus Integer
x (a -> PlusLevel' a) -> a -> PlusLevel' a
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
rho a
y) ([PlusLevel' a] -> [PlusLevel' a])
-> [PlusLevel' a] -> [PlusLevel' a]
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg a) -> [PlusLevel' a] -> [PlusLevel' a]
go Substitution' (SubstArg a)
rho [PlusLevel' a]
as

instance Subst a => Subst (PlusLevel' a) where
  type SubstArg (PlusLevel' a) = SubstArg a
  applySubst :: Substitution' (SubstArg (PlusLevel' a))
-> PlusLevel' a -> PlusLevel' a
applySubst Substitution' (SubstArg (PlusLevel' a))
rho (Plus Integer
n a
l) = Integer -> a -> PlusLevel' a
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (a -> PlusLevel' a) -> a -> PlusLevel' a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (PlusLevel' a))
rho a
l

instance Subst Name where
  type SubstArg Name = Term
  applySubst :: Substitution' (SubstArg Name) -> Name -> Name
applySubst Substitution' (SubstArg Name)
rho = Name -> Name
forall a. a -> a
id

instance Subst ConPatternInfo where
  type SubstArg ConPatternInfo = Term
  applySubst :: Substitution' (SubstArg ConPatternInfo)
-> ConPatternInfo -> ConPatternInfo
applySubst Substitution' (SubstArg ConPatternInfo)
rho ConPatternInfo
i = ConPatternInfo
i{ conPType = applySubst rho $ conPType i }

instance Subst Pattern where
  type SubstArg Pattern = Term
  applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern
applySubst Substitution' (SubstArg Pattern)
rho = \case
    ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
ps    -> ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c (Substitution' (SubstArg ConPatternInfo)
-> ConPatternInfo -> ConPatternInfo
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg ConPatternInfo)
Substitution' (SubstArg Pattern)
rho ConPatternInfo
mt) ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg Pattern])
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg Pattern])
Substitution' (SubstArg Pattern)
rho [NamedArg Pattern]
ps
    DefP PatternInfo
o QName
q [NamedArg Pattern]
ps     -> PatternInfo -> QName -> [NamedArg Pattern] -> Pattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg Pattern])
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg Pattern])
Substitution' (SubstArg Pattern)
rho [NamedArg Pattern]
ps
    DotP PatternInfo
o Term
t        -> PatternInfo -> Term -> Pattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
o (Term -> Pattern) -> Term -> Pattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg Pattern)
rho Term
t
    MaskP Pattern
p         -> Pattern -> Pattern
forall x. Pattern' x -> Pattern' x
MaskP (Substitution' (SubstArg Pattern) -> Pattern -> Pattern
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Pattern)
rho Pattern
p)
    p :: Pattern
p@(VarP PatternInfo
_o ArgName
_x)  -> Pattern
p
    p :: Pattern
p@(LitP PatternInfo
_o Literal
_l)  -> Pattern
p
    p :: Pattern
p@(ProjP ProjOrigin
_o QName
_x) -> Pattern
p
    IApplyP PatternInfo
o Term
t Term
u ArgName
x -> PatternInfo -> Term -> Term -> ArgName -> Pattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg Pattern)
rho Term
t) (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg Pattern)
rho Term
u) ArgName
x

instance Subst A.ProblemEq where
  type SubstArg A.ProblemEq = Term
  applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq
applySubst Substitution' (SubstArg ProblemEq)
rho (A.ProblemEq Pattern
p Term
v Dom Type
a) =
    (Term -> Dom Type -> ProblemEq) -> (Term, Dom Type) -> ProblemEq
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Pattern -> Term -> Dom Type -> ProblemEq
A.ProblemEq Pattern
p) ((Term, Dom Type) -> ProblemEq) -> (Term, Dom Type) -> ProblemEq
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Term, Dom Type))
-> (Term, Dom Type) -> (Term, Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Term, Dom Type))
Substitution' (SubstArg ProblemEq)
rho (Term
v,Dom Type
a)

instance DeBruijn BraveTerm where
  deBruijnVar :: Int -> BraveTerm
deBruijnVar = Term -> BraveTerm
BraveTerm (Term -> BraveTerm) -> (Int -> Term) -> Int -> BraveTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
forall a. DeBruijn a => Int -> a
deBruijnVar
  deBruijnView :: BraveTerm -> Maybe Int
deBruijnView = Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (Term -> Maybe Int)
-> (BraveTerm -> Term) -> BraveTerm -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BraveTerm -> Term
unBrave

-- Assume substitution maps the given variable to a variable
lookupSVar ::  EndoSubst a => Substitution' a -> Nat -> Maybe Nat
lookupSVar :: forall a. EndoSubst a => Substitution' a -> Int -> Maybe Int
lookupSVar Substitution' a
sub Int
x = a -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (a -> Maybe Int) -> a -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Substitution' a -> Int -> a
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' a
sub Int
x

instance Subst a => Subst (Blocked a) where
  type SubstArg (Blocked a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a
applySubst Substitution' (SubstArg (Blocked a))
rho Blocked a
b = (a -> a) -> Blocked a -> Blocked a
forall a b. (a -> b) -> Blocked' Term a -> Blocked' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Blocked a))
rho) Blocked a
b

instance Subst DisplayForm where
  type SubstArg DisplayForm = Term
  applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm
applySubst Substitution' (SubstArg DisplayForm)
rho (Display Int
n Elims
ps DisplayTerm
v) =
    let rho' :: Substitution' Term
rho' = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' Term
Substitution' (SubstArg DisplayForm)
rho
        !ps' :: Elims
ps' = Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Elims)
rho' Elims
ps in
    Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n Elims
ps' (Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg DisplayTerm)
rho' DisplayTerm
v)


instance Subst DisplayTerm where
  type SubstArg DisplayTerm = Term
  applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
applySubst Substitution' (SubstArg DisplayTerm)
rho (DTerm' Term
v Elims
es)      = Term -> Elims -> DisplayTerm
DTerm' (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg DisplayTerm)
rho Term
v) (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Elims)
Substitution' (SubstArg DisplayTerm)
rho Elims
es
  applySubst Substitution' (SubstArg DisplayTerm)
rho (DDot' Term
v Elims
es)       = Term -> Elims -> DisplayTerm
DDot'  (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg DisplayTerm)
rho Term
v) (Elims -> DisplayTerm) -> Elims -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Elims)
Substitution' (SubstArg DisplayTerm)
rho Elims
es
  applySubst Substitution' (SubstArg DisplayTerm)
rho (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs)     = ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c ConInfo
ci ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [Arg DisplayTerm])
-> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [Arg DisplayTerm])
Substitution' (SubstArg DisplayTerm)
rho [Arg DisplayTerm]
vs
  applySubst Substitution' (SubstArg DisplayTerm)
rho (DDef QName
c [Elim' DisplayTerm]
es)        = QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
c ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [Elim' DisplayTerm])
-> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [Elim' DisplayTerm])
Substitution' (SubstArg DisplayTerm)
rho [Elim' DisplayTerm]
es
  applySubst Substitution' (SubstArg DisplayTerm)
rho (DWithApp DisplayTerm
v List1 DisplayTerm
vs Elims
es) = (DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm)
-> (DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
DWithApp ((DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm)
-> (DisplayTerm, List1 DisplayTerm, Elims) -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (DisplayTerm, List1 DisplayTerm, Elims))
-> (DisplayTerm, List1 DisplayTerm, Elims)
-> (DisplayTerm, List1 DisplayTerm, Elims)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (DisplayTerm, List1 DisplayTerm, Elims))
Substitution' (SubstArg DisplayTerm)
rho (DisplayTerm
v, List1 DisplayTerm
vs, Elims
es)

instance Subst a => Subst (Tele a) where
  type SubstArg (Tele a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a
applySubst Substitution' (SubstArg (Tele a))
rho  Tele a
EmptyTel         = Tele a
forall a. Tele a
EmptyTel
  applySubst Substitution' (SubstArg (Tele a))
rho (ExtendTel a
t Abs (Tele a)
tel) = a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Tele a))
rho a
t) (Abs (Tele a) -> Tele a) -> Abs (Tele a) -> Tele a
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Abs (Tele a)))
-> Abs (Tele a) -> Abs (Tele a)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Abs (Tele a)))
Substitution' (SubstArg (Tele a))
rho Abs (Tele a)
tel

instance Subst Teletype where
  type SubstArg Teletype = Term
  applySubst :: Substitution' (SubstArg Teletype) -> Teletype -> Teletype
applySubst Substitution' (SubstArg Teletype)
rho (EmptyTt Type
t)      = Type -> Teletype
EmptyTt (Type -> Teletype) -> Type -> Teletype
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg Teletype)
rho Type
t
  applySubst Substitution' (SubstArg Teletype)
rho (ExtendTt Dom Type
t Abs Teletype
tel) = Dom Type -> Abs Teletype -> Teletype
ExtendTt (Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Dom Type))
Substitution' (SubstArg Teletype)
rho Dom Type
t) (Abs Teletype -> Teletype) -> Abs Teletype -> Teletype
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg (Abs Teletype))
-> Abs Teletype -> Abs Teletype
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Abs Teletype))
Substitution' (SubstArg Teletype)
rho Abs Teletype
tel

instance Subst Constraint where
  type SubstArg Constraint = Term

  applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint
applySubst Substitution' (SubstArg Constraint)
rho = \case
    ValueCmp Comparison
cmp CompareAs
a Term
u Term
v       -> Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp (CompareAs -> CompareAs
forall a. TermSubst a => a -> a
rf CompareAs
a) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
u) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
v)
    ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v -> Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
cmp (Term -> Term
forall a. TermSubst a => a -> a
rf Term
p) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
t) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
u) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
v)
    ElimCmp [Polarity]
ps [IsForced]
fs Type
a Term
v Elims
e1 Elims
e2  -> [Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
ps [IsForced]
fs (Type -> Type
forall a. TermSubst a => a -> a
rf Type
a) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
v) (Elims -> Elims
forall a. TermSubst a => a -> a
rf Elims
e1) (Elims -> Elims
forall a. TermSubst a => a -> a
rf Elims
e2)
    SortCmp Comparison
cmp Sort
s1 Sort
s2        -> Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp (Sort -> Sort
forall a. TermSubst a => a -> a
rf Sort
s1) (Sort -> Sort
forall a. TermSubst a => a -> a
rf Sort
s2)
    LevelCmp Comparison
cmp Level
l1 Level
l2       -> Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp (Level -> Level
forall a. TermSubst a => a -> a
rf Level
l1) (Level -> Level
forall a. TermSubst a => a -> a
rf Level
l2)
    IsEmpty Range
r Type
a              -> Range -> Type -> Constraint
IsEmpty Range
r (Type -> Type
forall a. TermSubst a => a -> a
rf Type
a)
    FindInstance Range
r MetaId
m Maybe [Candidate]
cands   -> Range -> MetaId -> Maybe [Candidate] -> Constraint
FindInstance Range
r MetaId
m (Maybe [Candidate] -> Maybe [Candidate]
forall a. TermSubst a => a -> a
rf Maybe [Candidate]
cands)
    ResolveInstanceHead KwRange
kwr QName
q -> KwRange -> QName -> Constraint
ResolveInstanceHead KwRange
kwr (QName -> QName
forall a. TermSubst a => a -> a
rf QName
q)
    c :: Constraint
c@UnBlock{}              -> Constraint
c
    c :: Constraint
c@CheckFunDef{}          -> Constraint
c
    HasPTSRule Dom Type
a Abs Sort
s           -> Dom Type -> Abs Sort -> Constraint
HasPTSRule (Dom Type -> Dom Type
forall a. TermSubst a => a -> a
rf Dom Type
a) (Abs Sort -> Abs Sort
forall a. TermSubst a => a -> a
rf Abs Sort
s)
    UnquoteTactic Term
t Term
h Type
g      -> Term -> Term -> Type -> Constraint
UnquoteTactic (Term -> Term
forall a. TermSubst a => a -> a
rf Term
t) (Term -> Term
forall a. TermSubst a => a -> a
rf Term
h) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
g)
    CheckDataSort QName
q Sort
s        -> QName -> Sort -> Constraint
CheckDataSort QName
q (Sort -> Sort
forall a. TermSubst a => a -> a
rf Sort
s)
    CheckMetaInst MetaId
m          -> MetaId -> Constraint
CheckMetaInst MetaId
m
    CheckType Type
t              -> Type -> Constraint
CheckType (Type -> Type
forall a. TermSubst a => a -> a
rf Type
t)
    where
      {-# INLINE rf #-}
      rf :: forall a. TermSubst a => a -> a
      rf :: forall a. TermSubst a => a -> a
rf a
x = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg Constraint)
rho a
x

instance Subst CompareAs where
  type SubstArg CompareAs = Term
  applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs
applySubst Substitution' (SubstArg CompareAs)
rho (AsTermsOf Type
a) = Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> Type -> CompareAs
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg CompareAs)
rho Type
a
  applySubst Substitution' (SubstArg CompareAs)
rho CompareAs
AsTypes       = CompareAs
AsTypes

instance Subst a => Subst (Elim' a) where
  type SubstArg (Elim' a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a
applySubst Substitution' (SubstArg (Elim' a))
rho = \case
    Apply Arg a
v      -> Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg a))
Substitution' (SubstArg (Elim' a))
rho Arg a
v)
    IApply a
x a
y a
r -> a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Elim' a))
rho a
x) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Elim' a))
rho a
y) (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Elim' a))
rho a
r)
    e :: Elim' a
e@Proj{}     -> Elim' a
e

instance Subst a => Subst (Abs a) where
  type SubstArg (Abs a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a
applySubst Substitution' (SubstArg (Abs a))
rho (Abs ArgName
x a
a)   = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' (SubstArg a)
Substitution' (SubstArg (Abs a))
rho) a
a)
  applySubst Substitution' (SubstArg (Abs a))
rho (NoAbs ArgName
x a
a) = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Abs a))
rho a
a)

instance Subst a => Subst (Arg a) where
  {-# INLINE applySubst #-}
  type SubstArg (Arg a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
applySubst Substitution' (SubstArg (Arg a))
IdS Arg a
arg       = Arg a
arg
  applySubst Substitution' (SubstArg (Arg a))
rho (Arg ArgInfo
i a
t) =
    let !i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
            | Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i
    in ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i' (a -> Arg a) -> a -> Arg a
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Arg a))
rho a
t

instance Subst a => Subst (Named name a) where
  type SubstArg (Named name a) = SubstArg a
  {-# INLINE applySubst #-}
  applySubst :: Substitution' (SubstArg (Named name a))
-> Named name a -> Named name a
applySubst Substitution' (SubstArg (Named name a))
rho = (a -> a) -> Named name a -> Named name a
forall a b. (a -> b) -> Named name a -> Named name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Named name a))
rho)

instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) where
  type SubstArg (Dom' a b) = SubstArg a

  {-# INLINE applySubst #-}
  applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b
applySubst Substitution' (SubstArg (Dom' a b))
IdS Dom' a b
dom = Dom' a b
dom
  applySubst Substitution' (SubstArg (Dom' a b))
rho (Dom' inf :: DomInfo a
inf@(DomInfo ArgInfo
i Maybe NamedName
n Bool
f Maybe a
t) b
e) =
    let i' :: ArgInfo
i' | ArgInfo -> FreeVariables
forall a. LensFreeVariables a => a -> FreeVariables
getFreeVariables ArgInfo
i FreeVariables -> FreeVariables -> Bool
forall a. Eq a => a -> a -> Bool
== FreeVariables
unknownFreeVariables = ArgInfo
i
           | Bool
otherwise = FreeVariables -> ArgInfo -> ArgInfo
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables ArgInfo
i in
    let inf' :: DomInfo a
inf' | Maybe a
Nothing <- Maybe a
t = DomInfo a
inf
             | Bool
otherwise = ArgInfo -> Maybe NamedName -> Bool -> Maybe a -> DomInfo a
forall t.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> DomInfo t
DomInfo ArgInfo
i' Maybe NamedName
n Bool
f (Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Maybe a))
Substitution' (SubstArg (Dom' a b))
rho Maybe a
t) in
    DomInfo a -> b -> Dom' a b
forall t e. DomInfo t -> e -> Dom' t e
Dom' DomInfo a
inf' (b -> Dom' a b) -> b -> Dom' a b
forall a b. (a -> b) -> a -> b
$$! Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (Dom' a b))
rho b
e
    -- Dom i' n f $$! applySubst rho t $$! applySubst rho rw $$! applySubst rho e

instance Subst LetBinding where
  type SubstArg LetBinding = Term
  applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding
applySubst Substitution' (SubstArg LetBinding)
rho (LetBinding IsAxiom
isAxiom Origin
o Term
v Dom Type
t) = IsAxiom -> Origin -> Term -> Dom Type -> LetBinding
LetBinding IsAxiom
isAxiom Origin
o (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg LetBinding)
rho Term
v) (Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Dom Type))
Substitution' (SubstArg LetBinding)
rho Dom Type
t)

instance Subst ContextEntry where
  type SubstArg ContextEntry = Term
  applySubst :: Substitution' (SubstArg ContextEntry)
-> ContextEntry -> ContextEntry
applySubst Substitution' (SubstArg ContextEntry)
rho (CtxVar Name
x Dom Type
a)   = Name -> Dom Type -> ContextEntry
CtxVar Name
x (Dom Type -> ContextEntry) -> Dom Type -> ContextEntry
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Dom Type))
Substitution' (SubstArg ContextEntry)
rho Dom Type
a

instance Subst a => Subst (Maybe a) where
  type SubstArg (Maybe a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a
applySubst Substitution' (SubstArg (Maybe a))
rho Maybe a
ma = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (Maybe a))
rho (a -> a) -> Maybe a -> Maybe a
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Maybe a
ma

instance Subst a => Subst [a] where
  type SubstArg [a] = SubstArg a
  applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a]
applySubst Substitution' (SubstArg [a])
rho [] = []
  applySubst Substitution' (SubstArg [a])
rho (a
a:[a]
as) = let !as' :: [a]
as' = Substitution' (SubstArg [a]) -> [a] -> [a]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [a])
rho [a]
as in Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg [a])
rho a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as'

instance Subst a => Subst (List1 a) where
  type SubstArg (List1 a) = SubstArg a
  applySubst :: Substitution' (SubstArg (List1 a)) -> List1 a -> List1 a
applySubst Substitution' (SubstArg (List1 a))
rho (a
a :| [a]
as) = let !as' :: [a]
as' = Substitution' (SubstArg [a]) -> [a] -> [a]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [a])
Substitution' (SubstArg (List1 a))
rho [a]
as in Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (List1 a))
rho a
a a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| [a]
as'

instance (Ord k, Subst a) => Subst (Map k a) where
  type SubstArg (Map k a) = SubstArg a

instance Subst a => Subst (Ranged a) where
  type SubstArg (Ranged a) = SubstArg a

instance Subst a => Subst (WithHiding a) where
  type SubstArg (WithHiding a) = SubstArg a

instance Subst () where
  type SubstArg () = Term
  applySubst :: Substitution' (SubstArg ()) -> () -> ()
applySubst Substitution' (SubstArg ())
_ ()
_ = ()

instance (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) where
  type SubstArg (a, b) = SubstArg a
  {-# INLINE applySubst #-}
  applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b)
applySubst Substitution' (SubstArg (a, b))
rho (a
x,b
y) = (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (a, b))
rho a
x, Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (a, b))
rho b
y)

instance (Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) where
  type SubstArg (a, b, c) = SubstArg a
  applySubst :: Substitution' (SubstArg (a, b, c)) -> (a, b, c) -> (a, b, c)
applySubst Substitution' (SubstArg (a, b, c))
rho (a
x,b
y,c
z) = (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (a, b, c))
rho a
x, Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (a, b, c))
rho b
y, Substitution' (SubstArg c) -> c -> c
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg c)
Substitution' (SubstArg (a, b, c))
rho c
z)

instance
  ( Subst a, Subst b, Subst c, Subst d
  , SubstArg a ~ SubstArg b
  , SubstArg b ~ SubstArg c
  , SubstArg c ~ SubstArg d
  ) => Subst (a, b, c, d) where
  type SubstArg (a, b, c, d) = SubstArg a
  applySubst :: Substitution' (SubstArg (a, b, c, d))
-> (a, b, c, d) -> (a, b, c, d)
applySubst Substitution' (SubstArg (a, b, c, d))
rho (a
x,b
y,c
z,d
u) = (Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg (a, b, c, d))
rho a
x, Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (a, b, c, d))
rho b
y, Substitution' (SubstArg c) -> c -> c
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg c)
Substitution' (SubstArg (a, b, c, d))
rho c
z, Substitution' (SubstArg d) -> d -> d
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg d)
Substitution' (SubstArg (a, b, c, d))
rho d
u)

instance Subst Candidate where
  type SubstArg Candidate = Term
  applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate
applySubst Substitution' (SubstArg Candidate)
rho (Candidate CandidateKind
q Term
u Type
t OverlapMode
ov) = CandidateKind -> Term -> Type -> OverlapMode -> Candidate
Candidate CandidateKind
q (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Term)
Substitution' (SubstArg Candidate)
rho Term
u) (Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg Candidate)
rho Type
t) OverlapMode
ov

instance DeBruijn a => DeBruijn (Pattern' a) where
  deBruijnNamedVar :: ArgName -> Int -> Pattern' a
deBruijnNamedVar ArgName
n Int
i             = a -> Pattern' a
forall a. a -> Pattern' a
varP (a -> Pattern' a) -> a -> Pattern' a
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> a
forall a. DeBruijn a => ArgName -> Int -> a
deBruijnNamedVar ArgName
n Int
i
  -- deBruijnView returns Nothing, to prevent consS and the like
  -- from dropping the names and origins when building a substitution.
  deBruijnView :: Pattern' a -> Maybe Int
deBruijnView Pattern' a
_                   = Maybe Int
forall a. Maybe a
Nothing

fromPatternSubstitution :: PatternSubstitution -> Substitution
fromPatternSubstitution :: PatternSubstitution -> Substitution' Term
fromPatternSubstitution = (DeBruijnPattern -> Term)
-> PatternSubstitution -> Substitution' Term
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm

applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
applyPatSubst :: forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst = Substitution' Term -> a -> a
Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' Term -> a -> a)
-> (PatternSubstitution -> Substitution' Term)
-> PatternSubstitution
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternSubstitution -> Substitution' Term
fromPatternSubstitution

usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin :: forall a. PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin PatOrigin
o Pattern' a
p = case Pattern' a -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo Pattern' a
p of
  Maybe PatternInfo
Nothing -> Pattern' a
p
  Just PatternInfo
i  -> PatternInfo -> Pattern' a -> Pattern' a
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo (PatternInfo
i { patOrigin = o }) Pattern' a
p

usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo :: forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i Pattern' a
p = case Pattern' a -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p of
  Maybe PatOrigin
Nothing         -> Pattern' a
p
  Just PatOrigin
PatOSplit  -> Pattern' a
p
  Just PatOrigin
PatOAbsurd -> Pattern' a
p
  Just PatOrigin
_          -> case Pattern' a
p of
    (VarP PatternInfo
_ a
x) -> PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
i a
x
    (DotP PatternInfo
_ Term
u) -> PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i Term
u
    (ConP ConHead
c (ConPatternInfo PatternInfo
_ Bool
r Bool
ft Maybe (Arg Type)
b Bool
l) [NamedArg (Pattern' a)]
ps)
      -> ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c (PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo PatternInfo
i Bool
r Bool
ft Maybe (Arg Type)
b Bool
l) [NamedArg (Pattern' a)]
ps
    DefP PatternInfo
_ QName
q [NamedArg (Pattern' a)]
ps -> PatternInfo -> QName -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q [NamedArg (Pattern' a)]
ps
    (LitP PatternInfo
_ Literal
l) -> PatternInfo -> Literal -> Pattern' a
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
i Literal
l
    ProjP{} -> Pattern' a
forall a. HasCallStack => a
__IMPOSSIBLE__
    MaskP{} -> Pattern' a
forall a. HasCallStack => a
__IMPOSSIBLE__
    (IApplyP PatternInfo
_ Term
t Term
u a
x) -> PatternInfo -> Term -> Term -> a -> Pattern' a
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i Term
t Term
u a
x

instance Subst DeBruijnPattern where
  type SubstArg DeBruijnPattern = DeBruijnPattern
  applySubst :: Substitution' (SubstArg DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
applySubst Substitution' (SubstArg DeBruijnPattern)
IdS = DeBruijnPattern -> DeBruijnPattern
forall a. a -> a
id
  applySubst Substitution' (SubstArg DeBruijnPattern)
rho = \case
    VarP PatternInfo
i DBPatVar
x     ->
      PatternInfo -> DeBruijnPattern -> DeBruijnPattern
forall a. PatternInfo -> Pattern' a -> Pattern' a
usePatternInfo PatternInfo
i (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
      ArgName -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> ArgName
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
      PatternSubstitution -> Int -> DeBruijnPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
    DotP PatternInfo
i Term
u     -> PatternInfo -> Term -> DeBruijnPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i (Term -> DeBruijnPattern) -> Term -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
u
    ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
ps -> ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci {conPType = applyPatSubst rho (conPType ci)} ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg DeBruijnPattern])
Substitution' (SubstArg DeBruijnPattern)
rho [NamedArg DeBruijnPattern]
ps
    DefP PatternInfo
i QName
q [NamedArg DeBruijnPattern]
ps  -> PatternInfo
-> QName -> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q ([NamedArg DeBruijnPattern] -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [NamedArg DeBruijnPattern])
Substitution' (SubstArg DeBruijnPattern)
rho [NamedArg DeBruijnPattern]
ps
    MaskP DeBruijnPattern
p      -> DeBruijnPattern -> DeBruijnPattern
forall x. Pattern' x -> Pattern' x
MaskP (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$! Substitution' (SubstArg DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg DeBruijnPattern)
rho DeBruijnPattern
p
    p :: DeBruijnPattern
p@(LitP PatternInfo
_ Literal
_) -> DeBruijnPattern
p
    p :: DeBruijnPattern
p@ProjP{}    -> DeBruijnPattern
p
    IApplyP PatternInfo
i Term
t Term
u DBPatVar
x ->
      case ArgName -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> ArgName
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Int -> DeBruijnPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho (Int -> DeBruijnPattern) -> Int -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x of
        IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
y -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
t) (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
u) DBPatVar
y
        VarP  PatternInfo
_ DBPatVar
y       -> PatternInfo -> Term -> Term -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
i (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
t) (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho Term
u) DBPatVar
y
        DeBruijnPattern
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
    where
      useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
      useName :: ArgName -> DeBruijnPattern -> DeBruijnPattern
useName ArgName
n (VarP PatternInfo
o DBPatVar
x)
        | ArgName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (DBPatVar -> ArgName
dbPatVarName DBPatVar
x)
        = PatternInfo -> DBPatVar -> DeBruijnPattern
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
o (DBPatVar -> DeBruijnPattern) -> DBPatVar -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar
x { dbPatVarName = n }
      useName ArgName
_ DeBruijnPattern
x = DeBruijnPattern
x

instance Subst Range where
  type SubstArg Range = Term
  applySubst :: Substitution' (SubstArg Range) -> Range -> Range
applySubst Substitution' (SubstArg Range)
_ = Range -> Range
forall a. a -> a
id

---------------------------------------------------------------------------
-- * Projections
---------------------------------------------------------------------------

-- | @projDropParsApply proj o args = 'projDropPars' proj o `'apply'` args@
--
--   This function is an optimization, saving us from construction lambdas we
--   immediately remove through application.
projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
projDropParsApply (Projection Maybe QName
prop QName
d Arg QName
r Int
_ ProjLams
lams) ProjOrigin
o Args
args =
  case [Arg ArgName] -> Maybe ([Arg ArgName], Arg ArgName)
forall a. [a] -> Maybe ([a], a)
initLast ([Arg ArgName] -> Maybe ([Arg ArgName], Arg ArgName))
-> [Arg ArgName] -> Maybe ([Arg ArgName], Arg ArgName)
forall a b. (a -> b) -> a -> b
$ ProjLams -> [Arg ArgName]
getProjLams ProjLams
lams of
    -- If we have no more abstractions, we must be a record field
    -- (projection applied already to record value).
    Maybe ([Arg ArgName], Arg ArgName)
Nothing -> if Bool
proper then QName -> Elims -> Term
Def QName
d (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args else Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    Just ([Arg ArgName]
pars, Arg ArgInfo
i ArgName
y) ->
      let core :: Term
core
            | Bool
proper    = ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
y (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
d]
            | Bool
otherwise = ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
y (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [] Term -> Arg QName -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg QName
r]
            -- Issue2226: get ArgInfo for principal argument from projFromType
      -- Now drop pars many args
          ([Arg ArgName]
pars', Args
args') = [Arg ArgName] -> Args -> ([Arg ArgName], Args)
forall a b. [a] -> [b] -> ([a], [b])
dropCommon [Arg ArgName]
pars Args
args
      -- We only have to abstract over the parameters that exceed the arguments.
      -- We only have to apply to the arguments that exceed the parameters.
      in (Arg ArgName -> Term -> Term) -> Term -> [Arg ArgName] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr (\ (Arg ArgInfo
ai ArgName
x) -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x) (Term
core Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
args') [Arg ArgName]
pars'
  where proper :: Bool
proper = Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust Maybe QName
prop

---------------------------------------------------------------------------
-- * Telescopes
---------------------------------------------------------------------------

-- ** Telescope view of a type

type TelView = TelV Type
data TelV a  = TelV { forall a. TelV a -> Tele (Dom a)
theTel :: Tele (Dom a), forall a. TelV a -> a
theCore :: a }
  deriving (Int -> TelV a -> [Char] -> [Char]
[TelV a] -> [Char] -> [Char]
TelV a -> [Char]
(Int -> TelV a -> [Char] -> [Char])
-> (TelV a -> [Char])
-> ([TelV a] -> [Char] -> [Char])
-> Show (TelV a)
forall a. Show a => Int -> TelV a -> [Char] -> [Char]
forall a. Show a => [TelV a] -> [Char] -> [Char]
forall a. Show a => TelV a -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall a. Show a => Int -> TelV a -> [Char] -> [Char]
showsPrec :: Int -> TelV a -> [Char] -> [Char]
$cshow :: forall a. Show a => TelV a -> [Char]
show :: TelV a -> [Char]
$cshowList :: forall a. Show a => [TelV a] -> [Char] -> [Char]
showList :: [TelV a] -> [Char] -> [Char]
Show, (forall a b. (a -> b) -> TelV a -> TelV b)
-> (forall a b. a -> TelV b -> TelV a) -> Functor TelV
forall a b. a -> TelV b -> TelV a
forall a b. (a -> b) -> TelV a -> TelV b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TelV a -> TelV b
fmap :: forall a b. (a -> b) -> TelV a -> TelV b
$c<$ :: forall a b. a -> TelV b -> TelV a
<$ :: forall a b. a -> TelV b -> TelV a
Functor)

deriving instance (TermSubst a, Eq  a) => Eq  (TelV a)
deriving instance (TermSubst a, Ord a) => Ord (TelV a)

-- | Takes off all exposed function domains from the given type.
--   This means that it does not reduce to expose @Pi@-types.
telView' :: Type -> TelView
telView' :: Type -> TelView
telView' = Int -> Type -> TelView
telView'UpTo (-Int
1)

-- | @telView'UpTo n t@ takes off the first @n@ exposed function types of @t@.
-- Takes off all (exposed ones) if @n < 0@.
telView'UpTo :: Int -> Type -> TelView
telView'UpTo :: Int -> Type -> TelView
telView'UpTo Int
0 Type
t = Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
telView'UpTo Int
n Type
t = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
  Pi Dom Type
a Abs Type
b  -> Dom Type -> 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) -> TelView -> TelView
forall a b. (a -> b) -> a -> b
$ Int -> Type -> TelView
telView'UpTo (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)
  Term
_       -> Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t

-- | Add given binding to the front of the telescope.
absV :: Dom a -> ArgName -> TelV a -> TelV a
absV :: forall a. Dom a -> ArgName -> TelV a -> TelV a
absV Dom a
a ArgName
x (TelV Tele (Dom a)
tel a
t) = Tele (Dom a) -> a -> TelV a
forall a. Tele (Dom a) -> a -> TelV a
TelV (Dom a -> Abs (Tele (Dom a)) -> Tele (Dom a)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom a
a (ArgName -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. ArgName -> a -> Abs a
Abs ArgName
x Tele (Dom a)
tel)) a
t


-- ** Creating telescopes from lists of types

-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' :: forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f []     Dom Type
t = []
bindsToTel' Name -> a
f (Name
x:[Name]
xs) Dom Type
t = let !rest :: [Dom (a, Type)]
rest = (Name -> a) -> [Name] -> Dom Type -> [Dom (a, Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f [Name]
xs (Int -> Dom Type -> Dom Type
forall a. Subst a => Int -> a -> a
raise Int
1 Dom Type
t) in (Type -> (a, Type)) -> Dom Type -> Dom (a, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> a
f Name
x,) Dom Type
t Dom (a, Type) -> [Dom (a, Type)] -> [Dom (a, Type)]
forall a. a -> [a] -> [a]
: [Dom (a, Type)]
rest

bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel :: [Name] -> Dom Type -> [Dom' Term (ArgName, Type)]
bindsToTel = (Name -> ArgName)
-> [Name] -> Dom Type -> [Dom' Term (ArgName, Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> ArgName
nameToArgName

bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel'1 :: forall a. (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel'1 Name -> a
f = (Name -> a) -> [Name] -> Dom Type -> ListTel' a
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f ([Name] -> Dom Type -> ListTel' a)
-> (List1 Name -> [Name]) -> List1 Name -> Dom Type -> ListTel' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Name -> [Item (List1 Name)]
List1 Name -> [Name]
forall l. IsList l => l -> [Item l]
List1.toList

bindsToTel1 :: List1 Name -> Dom Type -> ListTel
bindsToTel1 :: List1 Name -> Dom Type -> [Dom' Term (ArgName, Type)]
bindsToTel1 = [Name] -> Dom Type -> [Dom' Term (ArgName, Type)]
bindsToTel ([Name] -> Dom Type -> [Dom' Term (ArgName, Type)])
-> (List1 Name -> [Name])
-> List1 Name
-> Dom Type
-> [Dom' Term (ArgName, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Name -> [Item (List1 Name)]
List1 Name -> [Name]
forall l. IsList l => l -> [Item l]
List1.toList

-- | Turn a typed binding @(x1 .. xn : A)@ into a telescope.
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel []       Type
t = Telescope
forall a. Tele a
EmptyTel
namedBindsToTel (NamedArg Name
x : [NamedArg Name]
xs) Type
t =
  let !rest :: Telescope
rest = [NamedArg Name] -> Type -> Telescope
namedBindsToTel [NamedArg Name]
xs (Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
1 Type
t) in
  Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
t Type -> Dom' Term () -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x) (ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName (Name -> ArgName) -> Name -> ArgName
forall a b. (a -> b) -> a -> b
$ NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x) Telescope
rest)

namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 = [NamedArg Name] -> Type -> Telescope
namedBindsToTel ([NamedArg Name] -> Type -> Telescope)
-> (List1 (NamedArg Name) -> [NamedArg Name])
-> List1 (NamedArg Name)
-> Type
-> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (NamedArg Name) -> [Item (List1 (NamedArg Name))]
List1 (NamedArg Name) -> [NamedArg Name]
forall l. IsList l => l -> [Item l]
List1.toList

domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName :: NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x = () () -> Dom' Term Name -> Dom' Term ()
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term Name
forall a t. NamedArg a -> Dom' t a
domFromNamedArg ((Named NamedName Name -> Named NamedName Name)
-> NamedArg Name -> NamedArg Name
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Name -> Named NamedName Name
forceName NamedArg Name
x)
  where
    -- If no explicit name is given we use the bound name for the label.
    forceName :: Named NamedName Name -> Named NamedName Name
forceName (Named Maybe NamedName
Nothing Name
x) = Maybe NamedName -> Name -> Named NamedName Name
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
$ Range -> ArgName -> Ranged ArgName
forall a. Range -> a -> Ranged a
Ranged (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) (ArgName -> Ranged ArgName) -> ArgName -> Ranged ArgName
forall a b. (a -> b) -> a -> b
$ Name -> ArgName
nameToArgName Name
x) Name
x
    forceName Named NamedName Name
x = Named NamedName Name
x

domNameFromNamedArgName :: NamedArg Name -> Dom Name
domNameFromNamedArgName :: NamedArg Name -> Dom' Term Name
domNameFromNamedArgName NamedArg Name
x = NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x Name -> Dom' Term () -> Dom' Term Name
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x

-- ** Abstracting in terms and types

mkPiSort :: Dom Type -> Abs Type -> Sort
mkPiSort :: Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
a Abs Type
b = Dom Term -> Sort -> Abs Sort -> Sort
piSort (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Dom Type -> Dom Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
a) (Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a) (Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> Abs Type -> Abs Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b)

-- | @mkPi dom t = telePi (telFromList [dom]) t@
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPi :: Dom' Term (ArgName, Type) -> Type -> Type
mkPi !Dom' Term (ArgName, Type)
dom Type
b = Term -> Type
el (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a (ArgName -> Type -> Abs Type
forall a. (Subst a, Free a) => ArgName -> a -> Abs a
mkAbs ArgName
x Type
b)
  where
    x :: ArgName
x = (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type) -> ArgName) -> (ArgName, Type) -> ArgName
forall a b. (a -> b) -> a -> b
$ Dom' Term (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (ArgName, Type)
dom
    a :: Dom Type
a = (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type) -> Dom' Term (ArgName, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (ArgName, Type)
dom
    el :: Term -> Type
el = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type) -> Sort -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
a (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
x Type
b)

mkLam :: Arg ArgName -> Term -> Term
mkLam :: Arg ArgName -> Term -> Term
mkLam Arg ArgName
a Term
v = ArgInfo -> Abs Term -> Term
Lam (Arg ArgName -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo Arg ArgName
a) (ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (Arg ArgName -> ArgName
forall e. Arg e -> e
unArg Arg ArgName
a) Term
v)

lamView :: Term -> ([Arg ArgName], Term)
lamView :: Term -> ([Arg ArgName], Term)
lamView (Lam ArgInfo
h (Abs   ArgName
x Term
b)) = ([Arg ArgName] -> [Arg ArgName])
-> ([Arg ArgName], Term) -> ([Arg ArgName], Term)
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 (ArgInfo -> ArgName -> Arg ArgName
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h ArgName
x Arg ArgName -> [Arg ArgName] -> [Arg ArgName]
forall a. a -> [a] -> [a]
:) (([Arg ArgName], Term) -> ([Arg ArgName], Term))
-> ([Arg ArgName], Term) -> ([Arg ArgName], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg ArgName], Term)
lamView Term
b
lamView (Lam ArgInfo
h (NoAbs ArgName
x Term
b)) = ([Arg ArgName] -> [Arg ArgName])
-> ([Arg ArgName], Term) -> ([Arg ArgName], Term)
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 (ArgInfo -> ArgName -> Arg ArgName
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h ArgName
x Arg ArgName -> [Arg ArgName] -> [Arg ArgName]
forall a. a -> [a] -> [a]
:) (([Arg ArgName], Term) -> ([Arg ArgName], Term))
-> ([Arg ArgName], Term) -> ([Arg ArgName], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg ArgName], Term)
lamView (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
b)
lamView Term
t                   = ([], Term
t)

unlamView :: [Arg ArgName] -> Term -> Term
unlamView :: [Arg ArgName] -> Term -> Term
unlamView [Arg ArgName]
xs Term
b = (Arg ArgName -> Term -> Term) -> Term -> [Arg ArgName] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg ArgName -> Term -> Term
mkLam Term
b [Arg ArgName]
xs

telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' Abs Type -> Abs Type
reAbs = Telescope -> Type -> Type
telePi where
  telePi :: Telescope -> Type -> Type
telePi Telescope
EmptyTel          Type
t = Type
t
  telePi (ExtendTel Dom Type
u Abs Telescope
tel) Type
t = Term -> Type
el (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
u (Abs Type -> Term) -> Abs Type -> Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> Abs Type
reAbs Abs Type
b
    where
      b :: Abs Type
b  = (Telescope -> Type -> Type
`telePi` Type
t) (Telescope -> Type) -> Abs Telescope -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Telescope
tel
      el :: Term -> Type
el = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type) -> Sort -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
u Abs Type
b

-- | Uses free variable analysis to introduce 'NoAbs' bindings.
telePi :: Telescope -> Type -> Type
telePi :: Telescope -> Type -> Type
telePi = (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' Abs Type -> Abs Type
forall a. (Subst a, Free a) => Abs a -> Abs a
reAbs

-- | Everything will be an 'Abs'.
telePi_ :: Telescope -> Type -> Type
telePi_ :: Telescope -> Type -> Type
telePi_ = (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePi' Abs Type -> Abs Type
forall a. a -> a
id

-- | Only abstract the visible components of the telescope,
--   and all that bind variables.  Everything will be an 'Abs'!
-- Caution: quadratic time!

telePiVisible :: Telescope -> Type -> Type
telePiVisible :: Telescope -> Type -> Type
telePiVisible Telescope
EmptyTel Type
t = Type
t
telePiVisible (ExtendTel Dom Type
u Abs Telescope
tel) Type
t
    -- If u is not declared visible and b can be strengthened, skip quantification of u.
    | Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Dom Type
u, NoAbs ArgName
x Type
t' <- Abs Type
b' = Type
t'
    -- Otherwise, include quantification over u.
    | Bool
otherwise = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
u Abs Type
b) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
u Abs Type
b
  where
    b :: Abs Type
b  = Abs Telescope
tel Abs Telescope -> (Telescope -> Type) -> Abs Type
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Telescope -> Type -> Type
`telePiVisible` Type
t)
    b' :: Abs Type
b' = Abs Type -> Abs Type
forall a. (Subst a, Free a) => Abs a -> Abs a
reAbs Abs Type
b

-- | Performs void ('noAbs') abstraction over telescope.
class TeleNoAbs a where
  teleNoAbs :: a -> Term -> Term

instance TeleNoAbs ListTel where
  teleNoAbs :: [Dom' Term (ArgName, Type)] -> Term -> Term
teleNoAbs [Dom' Term (ArgName, Type)]
tel Term
t = (Dom' Term (ArgName, Type) -> Term -> Term)
-> Term -> [Dom' Term (ArgName, Type)] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Dom' Term (ArgName, Type)
d -> ArgInfo -> Abs Term -> Term
Lam (Dom' Term (ArgName, Type)
d Dom' Term (ArgName, Type)
-> Getting ArgInfo (Dom' Term (ArgName, Type)) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (ArgName, Type)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
NoAbs ((ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst (Dom' Term (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (ArgName, Type)
d))) Term
t [Dom' Term (ArgName, Type)]
tel

instance TeleNoAbs Telescope where
  teleNoAbs :: Telescope -> Term -> Term
teleNoAbs Telescope
tel = [Dom' Term (ArgName, Type)] -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs ([Dom' Term (ArgName, Type)] -> Term -> Term)
-> [Dom' Term (ArgName, Type)] -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel


-- ** Telescope typing

-- | Given arguments @vs : tel@ (vector typing), extract their individual types.
--   Returns @Nothing@ is @tel@ is not long enough.

typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel Telescope
_ []                         = [Dom Type] -> Maybe [Dom Type]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
typeArgsWithTel (ExtendTel Dom Type
dom Abs Telescope
tel) (Term
v : [Term]
vs) = (Dom Type
dom Dom Type -> [Dom Type] -> [Dom Type]
forall a. a -> [a] -> [a]
:) ([Dom Type] -> [Dom Type]) -> Maybe [Dom Type] -> Maybe [Dom Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> [Term] -> Maybe [Dom Type]
typeArgsWithTel (Abs Telescope -> SubstArg Telescope -> Telescope
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Telescope
tel Term
SubstArg Telescope
v) [Term]
vs
typeArgsWithTel EmptyTel{} (Term
_:[Term]
_)             = Maybe [Dom Type]
forall a. Maybe a
Nothing

---------------------------------------------------------------------------
-- * Clauses
---------------------------------------------------------------------------

-- | In compiled clauses, the variables in the clause body are relative to the
--   pattern variables (including dot patterns) instead of the clause telescope.
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody :: Clause -> Maybe Term
compiledClauseBody Clause
cl = Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Permutation -> Substitution' Term
forall a. DeBruijn a => Permutation -> Substitution' a
renamingR Permutation
perm) (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl
  where perm :: Permutation
perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
cl

---------------------------------------------------------------------------
-- * Syntactic equality and order
--
-- Needs weakening.
---------------------------------------------------------------------------

deriving instance Eq Substitution
deriving instance Ord Substitution

deriving instance Eq Sort
deriving instance Ord Sort
deriving instance Eq Level
deriving instance Ord Level
deriving instance Eq PlusLevel
deriving instance Eq NotBlocked
deriving instance Eq t => Eq (Blocked t)
deriving instance Eq CandidateKind
deriving instance Eq Candidate
deriving instance Ord CandidateKind
deriving instance Ord Candidate

-- Andreas, 2019-11-16, issue #4201: to avoid potential unintended
-- performance loss, the Eq instance for Constraint is disabled:
--
-- -- deriving instance Eq Constraint
--
-- I am tempted to write
--
--   instance Eq Constraint where (==) = undefined
--
-- but this does not give a compilation error anymore when trying
-- to use equality on constraints.
-- Therefore, I hope this comment is sufficient to prevent a resurrection
-- of the Eq instance for Constraint.

deriving instance Eq Section

instance Ord PlusLevel where
  -- Compare on the atom first. Makes most sense for levelMax.
  compare :: PlusLevel' Term -> PlusLevel' Term -> Ordering
compare (Plus Integer
n Term
a) (Plus Integer
m Term
b) = (Term, Integer) -> (Term, Integer) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Term
a,Integer
n) (Term
b,Integer
m)

-- | Syntactic 'Type' equality, ignores sort annotations.
instance Eq a => Eq (Type' a) where
  == :: Type' a -> Type' a -> Bool
(==) = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (a -> a -> Bool) -> (Type' a -> a) -> Type' a -> Type' a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Type' a -> a
forall t a. Type'' t a -> a
unEl

instance Ord a => Ord (Type' a) where
  compare :: Type' a -> Type' a -> Ordering
compare = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> a -> Ordering)
-> (Type' a -> a) -> Type' a -> Type' a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Type' a -> a
forall t a. Type'' t a -> a
unEl

-- | Syntactic 'Term' equality, ignores stuff below @DontCare@ and sharing.
instance Eq Term where
  Var Int
x Elims
vs   == :: Term -> Term -> Bool
== Var Int
x' Elims
vs'   = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
  Lam ArgInfo
h Abs Term
v    == Lam ArgInfo
h' Abs Term
v'    = ArgInfo
h ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
h' Bool -> Bool -> Bool
&& Abs Term
v  Abs Term -> Abs Term -> Bool
forall a. Eq a => a -> a -> Bool
== Abs Term
v'
  Lit Literal
l      == Lit Literal
l'       = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
  Def QName
x Elims
vs   == Def QName
x' Elims
vs'   = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
x' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
  Con ConHead
x ConInfo
_ Elims
vs == Con ConHead
x' ConInfo
_ Elims
vs' = ConHead
x ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
x' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
  Pi Dom Type
a Abs Type
b     == Pi Dom Type
a' Abs Type
b'     = Dom Type
a Dom Type -> Dom Type -> Bool
forall a. Eq a => a -> a -> Bool
== Dom Type
a' Bool -> Bool -> Bool
&& Abs Type
b Abs Type -> Abs Type -> Bool
forall a. Eq a => a -> a -> Bool
== Abs Type
b'
  Sort Sort
s     == Sort Sort
s'      = Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s'
  Level Level
l    == Level Level
l'     = Level
l Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Level
l'
  MetaV MetaId
m Elims
vs == MetaV MetaId
m' Elims
vs' = MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' Bool -> Bool -> Bool
&& Elims
vs Elims -> Elims -> Bool
forall a. Eq a => a -> a -> Bool
== Elims
vs'
  DontCare Term
_ == DontCare Term
_   = Bool
True
  Dummy{}    == Dummy{}      = Bool
True
  Term
_          == Term
_            = Bool
False

instance Eq a => Eq (Pattern' a) where
  VarP PatternInfo
_ a
x        == :: Pattern' a -> Pattern' a -> Bool
== VarP PatternInfo
_ a
y          = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
  DotP PatternInfo
_ Term
u        == DotP PatternInfo
_ Term
v          = Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v
  ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' a)]
ps     == ConP ConHead
c' ConPatternInfo
_ [NamedArg (Pattern' a)]
qs      = ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c Bool -> Bool -> Bool
&& [NamedArg (Pattern' a)]
ps [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)] -> Bool
forall a. Eq a => a -> a -> Bool
== [NamedArg (Pattern' a)]
qs
  LitP PatternInfo
_ Literal
l        == LitP PatternInfo
_ Literal
l'         = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
  ProjP ProjOrigin
_ QName
f       == ProjP ProjOrigin
_ QName
g         = QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g
  IApplyP PatternInfo
_ Term
u Term
v a
x == IApplyP PatternInfo
_ Term
u' Term
v' a
y = Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
u' Bool -> Bool -> Bool
&& Term
v Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
v' Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
  DefP PatternInfo
_ QName
f [NamedArg (Pattern' a)]
ps     == DefP PatternInfo
_ QName
g [NamedArg (Pattern' a)]
qs       = QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g Bool -> Bool -> Bool
&& [NamedArg (Pattern' a)]
ps [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)] -> Bool
forall a. Eq a => a -> a -> Bool
== [NamedArg (Pattern' a)]
qs
  Pattern' a
_               == Pattern' a
_                 = Bool
False

instance Ord Term where
  Var Int
a Elims
b    compare :: Term -> Term -> Ordering
`compare` Var Int
x Elims
y    = (Int, Elims) -> (Int, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int
x, Elims
b) (Int
a, Elims
y)
                                    -- sort de Bruijn indices down (#2765)
  Var{}      `compare` Term
_          = Ordering
LT
  Term
_          `compare` Var{}      = Ordering
GT
  Def QName
a Elims
b    `compare` Def QName
x Elims
y    = (QName, Elims) -> (QName, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (QName
a, Elims
b) (QName
x, Elims
y)
  Def{}      `compare` Term
_          = Ordering
LT
  Term
_          `compare` Def{}      = Ordering
GT
  Con ConHead
a ConInfo
_ Elims
b  `compare` Con ConHead
x ConInfo
_ Elims
y  = (ConHead, Elims) -> (ConHead, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ConHead
a, Elims
b) (ConHead
x, Elims
y)
  Con{}      `compare` Term
_          = Ordering
LT
  Term
_          `compare` Con{}      = Ordering
GT
  Lit Literal
a      `compare` Lit Literal
x      = Literal -> Literal -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Literal
a Literal
x
  Lit{}      `compare` Term
_          = Ordering
LT
  Term
_          `compare` Lit{}      = Ordering
GT
  Lam ArgInfo
a Abs Term
b    `compare` Lam ArgInfo
x Abs Term
y    = (ArgInfo, Abs Term) -> (ArgInfo, Abs Term) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ArgInfo
a, Abs Term
b) (ArgInfo
x, Abs Term
y)
  Lam{}      `compare` Term
_          = Ordering
LT
  Term
_          `compare` Lam{}      = Ordering
GT
  Pi Dom Type
a Abs Type
b     `compare` Pi Dom Type
x Abs Type
y     = (Dom Type, Abs Type) -> (Dom Type, Abs Type) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Dom Type
a, Abs Type
b) (Dom Type
x, Abs Type
y)
  Pi{}       `compare` Term
_          = Ordering
LT
  Term
_          `compare` Pi{}       = Ordering
GT
  Sort Sort
a     `compare` Sort Sort
x     = Sort -> Sort -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Sort
a Sort
x
  Sort{}     `compare` Term
_          = Ordering
LT
  Term
_          `compare` Sort{}     = Ordering
GT
  Level Level
a    `compare` Level Level
x    = Level -> Level -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Level
a Level
x
  Level{}    `compare` Term
_          = Ordering
LT
  Term
_          `compare` Level{}    = Ordering
GT
  MetaV MetaId
a Elims
b  `compare` MetaV MetaId
x Elims
y  = (MetaId, Elims) -> (MetaId, Elims) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (MetaId
a, Elims
b) (MetaId
x, Elims
y)
  MetaV{}    `compare` Term
_          = Ordering
LT
  Term
_          `compare` MetaV{}    = Ordering
GT
  DontCare{} `compare` DontCare{} = Ordering
EQ
  DontCare{} `compare` Term
_          = Ordering
LT
  Term
_          `compare` DontCare{} = Ordering
GT
  Dummy{}    `compare` Dummy{}    = Ordering
EQ

-- | Equality of binders relies on weakening
--   which is a special case of renaming
--   which is a special case of substitution.
instance (Subst a, Eq a) => Eq (Abs a) where
  NoAbs ArgName
_ a
a == :: Abs a -> Abs a -> Bool
== NoAbs ArgName
_ a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b  -- no need to raise if both are NoAbs
  Abs a
a         == Abs a
b         = Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
b

instance (Subst a, Ord a) => Ord (Abs a) where
  NoAbs ArgName
_ a
a compare :: Abs a -> Abs a -> Ordering
`compare` NoAbs ArgName
_ a
b = a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b  -- no need to raise if both are NoAbs
  Abs a
a         `compare` Abs a
b         = Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
b

deriving instance Ord a => Ord (Dom a)

instance (Eq a) => Eq (Elim' a) where
  Apply  Arg a
a == :: Elim' a -> Elim' a -> Bool
== Apply  Arg a
b = Arg a
a Arg a -> Arg a -> Bool
forall a. Eq a => a -> a -> Bool
== Arg a
b
  Proj ProjOrigin
_ QName
x == Proj ProjOrigin
_ QName
y = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
  IApply a
x a
y a
r == IApply a
x' a
y' a
r' = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' Bool -> Bool -> Bool
&& a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y' Bool -> Bool -> Bool
&& a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
r'
  Elim' a
_ == Elim' a
_ = Bool
False

instance (Ord a) => Ord (Elim' a) where
  Apply  Arg a
a compare :: Elim' a -> Elim' a -> Ordering
`compare` Apply  Arg a
b = Arg a
a Arg a -> Arg a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Arg a
b
  Proj ProjOrigin
_ QName
x `compare` Proj ProjOrigin
_ QName
y = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
  IApply a
x a
y a
r `compare` IApply a
x' a
y' a
r' = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
x' Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
y a
y' Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
r a
r'
  Apply{}  `compare` Elim' a
_        = Ordering
LT
  Elim' a
_        `compare` Apply{}  = Ordering
GT
  Proj{}   `compare` Elim' a
_        = Ordering
LT
  Elim' a
_        `compare` Proj{}   = Ordering
GT

deriving instance Eq (DomInfo Term)

deriving instance Ord (DomInfo Term)

---------------------------------------------------------------------------
-- * Sort stuff
---------------------------------------------------------------------------

-- | @univSort' univInf s@ gets the next higher sort of @s@, if it is
--   known (i.e. it is not just @UnivSort s@).
--
--   Precondition: @s@ is reduced
univSort' :: Sort -> Either Blocker Sort
univSort' :: Sort -> Either Blocker Sort
univSort' (Univ Univ
u Level
l)   = Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ (Univ -> Univ
univUniv Univ
u) (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' (Inf Univ
u Integer
n)    = Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ
univUniv Univ
u) (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n
univSort' Sort
LevelUniv    = Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
1
univSort' Sort
IntervalUniv = Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
1
univSort' Sort
CofUniv      = Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
1
univSort' (MetaS MetaId
m Elims
_)  = Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' FunSort{}    = Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' PiSort{}     = Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' UnivSort{}   = Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' DefS{}       = Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
univSort' DummyS{}     = Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock

univSort :: Sort -> Sort
univSort :: Sort -> Sort
univSort Sort
s = (Blocker -> Sort) -> Either Blocker Sort -> Sort
forall a b. (a -> b) -> Either a b -> b
fromRight (Sort -> Blocker -> Sort
forall a b. a -> b -> a
const (Sort -> Blocker -> Sort) -> Sort -> Blocker -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
s) (Either Blocker Sort -> Sort) -> Either Blocker Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Either Blocker Sort
univSort' Sort
s

sort :: Sort -> Type
sort :: Sort -> Type
sort Sort
s = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Sort
univSort Sort
s) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
s

ssort :: Level -> Type
ssort :: Level -> Type
ssort Level
l = Sort -> Type
sort (Level -> Sort
forall t. Level' t -> Sort' t
SSet Level
l)

-- | A sort can either be small (Type l, Prop l, Size, ...)  or large
--   (Typeω n).
data SizeOfSort = SizeOfSort
  { SizeOfSort -> Univ
szSortUniv :: Univ
  , SizeOfSort -> Integer
szSortSize :: Integer
  }

pattern SmallSort :: Univ -> SizeOfSort
pattern $bSmallSort :: Univ -> SizeOfSort
$mSmallSort :: forall {r}. SizeOfSort -> (Univ -> r) -> ((# #) -> r) -> r
SmallSort u = SizeOfSort u (-1)

pattern LargeSort :: Univ -> Integer -> SizeOfSort
-- What I want to write here is:
-- @
--   pattern LargeSort u n = SizeOfSort u n | n >= 0
-- @
-- But I have to write:
pattern $bLargeSort :: Univ -> Integer -> SizeOfSort
$mLargeSort :: forall {r}.
SizeOfSort -> (Univ -> Integer -> r) -> ((# #) -> r) -> r
LargeSort u n <- ((\ x :: SizeOfSort
x@(SizeOfSort Univ
u Integer
n) -> Bool -> Maybe ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) Maybe () -> SizeOfSort -> Maybe SizeOfSort
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SizeOfSort
x) -> Just (SizeOfSort u n))
-- DON'T WORK:
-- pattern LargeSort u n <- (n >= 0 -> True)
-- pattern LargeSort u n <- (n >= 0 -> SizeOfSort u n)
-- pattern LargeSort u n <- ((>= 0) . szSortSize -> SizeOfSort u n)
  where LargeSort Univ
u Integer
n = Univ -> Integer -> SizeOfSort
SizeOfSort Univ
u Integer
n

{-# COMPLETE SmallSort, LargeSort #-}

-- | Returns @Left blocker@ for unknown (blocked) sorts, and otherwise
--   returns @Right s@ where @s@ indicates the size and fibrancy.
sizeOfSort :: Sort -> Either Blocker SizeOfSort
sizeOfSort :: Sort -> Either Blocker SizeOfSort
sizeOfSort = \case
  Univ Univ
u Level
_     -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
u
  Sort
LevelUniv    -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
UType
  Sort
IntervalUniv -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
USSet
  Sort
CofUniv      -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> SizeOfSort
SmallSort Univ
USSet
  Inf Univ
u Integer
n      -> SizeOfSort -> Either Blocker SizeOfSort
forall a b. b -> Either a b
Right (SizeOfSort -> Either Blocker SizeOfSort)
-> SizeOfSort -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> SizeOfSort
LargeSort Univ
u Integer
n
  MetaS MetaId
m Elims
_    -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left (Blocker -> Either Blocker SizeOfSort)
-> Blocker -> Either Blocker SizeOfSort
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
  FunSort{}    -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  PiSort{}     -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  UnivSort{}   -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  DefS{}       -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  DummyS{}     -> Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock

isSmallSort :: Sort -> Bool
isSmallSort :: Sort -> Bool
isSmallSort Sort
s = case Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s of
  Right SmallSort{} -> Bool
True
  Either Blocker SizeOfSort
_                 -> Bool
False

-- | Compute the sort of a function type from the sorts of its domain and codomain.
--
--   The first argument is the value of `isLevelUniverseEnabled`
funSort' :: Bool -> Sort -> Sort -> Either Blocker Sort
-- Andreas, 2023-05-12, AIM XXXVI, pri #6623:
-- On GHC 8.6 and 8.8 this pattern matching triggers warning
-- "Pattern match checker exceeded (2000000) iterations in a case alternative."
-- No clue how to turn off this warning, so we have to turn off -Werror for GHC < 8.10.
funSort' :: Bool -> Sort -> Sort -> Either Blocker Sort
funSort' Bool
hasLevelUniv Sort
a Sort
b = case (Sort -> Sort
normLU Sort
a, Sort -> Sort
normLU Sort
b) of
  (Univ Univ
u Level
a      , Univ Univ
u' Level
b    ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ (Univ -> Univ -> Univ
funUniv Univ
u Univ
u') (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Inf Univ
ua Integer
m      , Sort
b            ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
b Either Blocker SizeOfSort
-> (SizeOfSort -> Sort) -> Either Blocker Sort
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (SizeOfSort Univ
ub Integer
n) -> Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ -> Univ
funUniv Univ
ua Univ
ub) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n)
  (Sort
a             , Inf Univ
ub Integer
n     ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
a Either Blocker SizeOfSort
-> (SizeOfSort -> Sort) -> Either Blocker Sort
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (SizeOfSort Univ
ua Integer
m) -> Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ -> Univ
funUniv Univ
ua Univ
ub) (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n)

  -- @IntervalUniv@ behaves like @SSet@, but functions into @Type@ land in @Type@
  (Sort
IntervalUniv  , Sort
IntervalUniv ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
  (Sort
IntervalUniv  , Univ Univ
u Level
b     ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u Level
b
  (Sort
IntervalUniv  , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Univ Univ
u Level
a      , Sort
IntervalUniv ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level
a
  (Sort
_             , Sort
IntervalUniv ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock

  (Sort
CofUniv       , Univ Univ
_ Level
b     ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet Level
b
  (Univ Univ
_ Level
a      , Sort
CofUniv      ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet Level
a
  (Sort
CofUniv       , Sort
CofUniv      ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0

  -- No need to handle @LevelUniv@ in a special way here when --level-universe isn't on,
  -- since this function is currently always called after reduction.
  -- It would be safer to take it into account here, but would imply passing the option along as an argument.
  (Sort
LevelUniv     , Sort
LevelUniv    ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right Sort
forall t. Sort' t
LevelUniv
  (Sort
_             , Sort
LevelUniv    ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
LevelUniv     , Sort
b            ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
b Either Blocker SizeOfSort
-> (SizeOfSort -> Sort) -> Either Blocker Sort
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    SmallSort Univ
ub -> Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
ub Integer
0
    LargeSort{}  -> Sort
b
  (MetaS MetaId
m Elims
_     , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
  (Sort
_             , MetaS MetaId
m Elims
_    ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
  (FunSort{}     , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , FunSort{}    ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (PiSort{}      , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , PiSort{}     ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (UnivSort{}    , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , UnivSort{}   ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (DefS{}        , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , DefS{}       ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (DummyS{}      , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , DummyS{}     ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock

  where
  normLU :: Sort -> Sort
normLU = Bool -> (Sort -> Sort) -> Sort -> Sort
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
hasLevelUniv \case
             Sort
LevelUniv -> Integer -> Sort
mkType Integer
0
             Sort
s         -> Sort
s

funSort :: Bool -> Sort -> Sort -> Sort
funSort :: Bool -> Sort -> Sort -> Sort
funSort Bool
hasLevelUniv Sort
a Sort
b = (Blocker -> Sort) -> Either Blocker Sort -> Sort
forall a b. (a -> b) -> Either a b -> b
fromRight (Sort -> Blocker -> Sort
forall a b. a -> b -> a
const (Sort -> Blocker -> Sort) -> Sort -> Blocker -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
a Sort
b) (Either Blocker Sort -> Sort) -> Either Blocker Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Bool -> Sort -> Sort -> Either Blocker Sort
funSort' Bool
hasLevelUniv Sort
a Sort
b

{-# SPECIALISE funSortM' :: Sort -> Sort -> TCM (Either Blocker Sort) #-}
funSortM' :: HasOptions m => Sort -> Sort -> m (Either Blocker Sort)
funSortM' :: forall (m :: * -> *).
HasOptions m =>
Sort -> Sort -> m (Either Blocker Sort)
funSortM' Sort
a Sort
b = do
  hasLevelUniv <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
isLevelUniverseEnabled
  return $ funSort' hasLevelUniv a b

{-# SPECIALISE funSortM :: Sort -> Sort -> TCM Sort #-}
funSortM :: HasOptions m => Sort -> Sort -> m Sort
funSortM :: forall (m :: * -> *). HasOptions m => Sort -> Sort -> m Sort
funSortM Sort
a Sort
b = do
  hasLevelUniv <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
isLevelUniverseEnabled
  return $ funSort hasLevelUniv a b

-- | Compute the sort of a pi type from three inputs:
--   1. The "raw" domain of the pi type (without the sort)
--   2. The sort of the domain
--   3. The sort of the codomain (which lives in an extended context)
--
-- Note that unlike funSort', we don't care whether --level-universe is
-- enabled here. Instead, we just return a FunSort constructor and
-- assume it will be simplified in the next step. See also:
-- * `instance Reduce Sort` in Agda.TypeChecking.Substitute (this file)
-- * `inferPiSort` in Agda.TypeChecking.Sort
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' Dom Term
a Sort
s1       (NoAbs ArgName
_ Sort
s2) = Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 Sort
s2
piSort' Dom Term
a Sort
s1 s2Abs :: Abs Sort
s2Abs@(Abs   ArgName
_ Sort
s2) = case Int -> Sort -> Maybe FlexRig
forall a. Free a => Int -> a -> Maybe FlexRig
flexRigOccurrenceIn Int
0 Sort
s2 of
  Maybe FlexRig
Nothing -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Sort -> Either Blocker Sort) -> Sort -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Impossible -> Abs Sort -> Sort
forall a. Subst a => Impossible -> Abs a -> a
noabsApp Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ Abs Sort
s2Abs
  Just FlexRig
o  -> Dom Term
-> Sort
-> Abs Sort
-> FlexRig
-> IsCodomainNormalised
-> Either Blocker Sort
piSortAbs Dom Term
a Sort
s1 Abs Sort
s2Abs FlexRig
o IsCodomainNormalised
CodomainNotNormalised

data IsCodomainNormalised = CodomainNormalised | CodomainNotNormalised

-- | Compute the sort of a pi type where the codomain sort is a proper Abs.
--   Compared to piSort' we take two additional arguments:
--   4. The occurrence of the variable in the codomain.
--   5. Whether we have already tried to remove the dependency by
--      normalising the codomain sort (e.g. with forceNoAbs)
piSortAbs
  :: Dom Term
  -> Sort
  -> Abs Sort
  -> FlexRig
  -> IsCodomainNormalised
  -> Either Blocker Sort
piSortAbs :: Dom Term
-> Sort
-> Abs Sort
-> FlexRig
-> IsCodomainNormalised
-> Either Blocker Sort
piSortAbs Dom Term
a Sort
s1 NoAbs{} FlexRig
_ IsCodomainNormalised
_ = Either Blocker Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
piSortAbs Dom Term
a Sort
s1 (Abs ArgName
x Sort
s2) FlexRig
occ IsCodomainNormalised
norm = case (Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s1 , Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s2) of
  (Right (SmallSort Univ
u1) , Right (SmallSort Univ
u2)) -> case FlexRig
occ of
    FlexRig
StronglyRigid -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0)
    FlexRig
Unguarded     -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0)
    -- Jesper, 2026-02-17: A weakly rigid occurrence might disappear after
    -- normalisation (see #8393) so we refrain from making a final verdict here.
    -- unless we are sure further normalisation will not remove the dependency
    FlexRig
WeaklyRigid -> case IsCodomainNormalised
norm of
      IsCodomainNormalised
CodomainNormalised -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0)
      IsCodomainNormalised
CodomainNotNormalised -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
alwaysUnblock
    Flexible MetaSet
ms -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$! MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
  (Right (LargeSort Univ
u1 Integer
n) , Right (SmallSort Univ
u2)) -> let !u :: Univ
u = Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 in Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n)
  -- large sorts cannot depend on variables
  (Either Blocker SizeOfSort
_             , Right LargeSort{}) -> Either Blocker Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
  (Left Blocker
blocker  , Right SizeOfSort
_          ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
blocker
  (Right SizeOfSort
_       , Left Blocker
blocker     ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
blocker
  (Left Blocker
blocker1 , Left Blocker
blocker2    ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left (Blocker -> Either Blocker Sort) -> Blocker -> Either Blocker Sort
forall a b. (a -> b) -> a -> b
$! Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
blocker1 Blocker
blocker2

piSort :: Dom Term -> Sort -> Abs Sort -> Sort
piSort :: Dom Term -> Sort -> Abs Sort -> Sort
piSort Dom Term
a Sort
s1 Abs Sort
s2 = (Blocker -> Sort) -> Either Blocker Sort -> Sort
forall a b. (a -> b) -> Either a b -> b
fromRight (Sort -> Blocker -> Sort
forall a b. a -> b -> a
const (Sort -> Blocker -> Sort) -> Sort -> Blocker -> Sort
forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom Term
a Sort
s1 Abs Sort
s2) (Either Blocker Sort -> Sort) -> Either Blocker Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' Dom Term
a Sort
s1 Abs Sort
s2

{-# SPECIALISE piSortM :: Dom Term -> Sort -> Abs Sort -> TCM Sort #-}
piSortM :: HasOptions m => Dom Term -> Sort -> Abs Sort -> m Sort
piSortM :: forall (m :: * -> *).
HasOptions m =>
Dom Term -> Sort -> Abs Sort -> m Sort
piSortM Dom Term
va Sort
s1 Abs Sort
s2 = case Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' Dom Term
va Sort
s1 Abs Sort
s2 of
  Left Blocker
_ -> Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort Dom Term
va Sort
s1 Abs Sort
s2
  -- Jesper, 2025-09-15: if a PiSort reduces to a FunSort, piSort'
  -- just returns the FunSort without trying to simplify it further.
  -- So if we get a FunSort here we call funSortM in the hopes
  -- of getting a simpler result. But we DON'T call reduce as that
  -- can lead to quadratic behavior, see #8096.
  Right (FunSort Sort
s1' Sort
s2') -> Sort -> Sort -> m Sort
forall (m :: * -> *). HasOptions m => Sort -> Sort -> m Sort
funSortM Sort
s1' Sort
s2'
  Right Sort
s' -> Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s'



---------------------------------------------------------------------------
-- * Level stuff
---------------------------------------------------------------------------

-- | Computes @n0 ⊔ a₁ ⊔ a₂ ⊔ ... ⊔ aₙ@ and return its canonical form.
levelMax :: Integer -> [PlusLevel] -> Level
levelMax :: Integer -> [PlusLevel' Term] -> Level
levelMax !Integer
n0 [PlusLevel' Term]
as0 = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n [PlusLevel' Term]
as
  where
    -- step 1: flatten nested @Level@ expressions in @PlusLevel@s
    Max Integer
n1 [PlusLevel' Term]
as1 = Level -> Level
expandLevel (Level -> Level) -> Level -> Level
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n0 [PlusLevel' Term]
as0
    -- step 2: remove subsumed @PlusLevel@s and sort what remains
    as :: [PlusLevel' Term]
as        = [PlusLevel' Term] -> [PlusLevel' Term]
removeSubsumed [PlusLevel' Term]
as1
    -- step 3: set constant to 0 if it is subsumed by one of the @PlusLevel@s
    greatestB :: Integer
greatestB = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [ Integer
n | Plus Integer
n Term
_ <- [PlusLevel' Term]
as ]
    n :: Integer
n | Integer
n1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
greatestB = Integer
n1
      | Bool
otherwise      = Integer
0

    lmax :: Integer -> [PlusLevel] -> [Level] -> Level
    lmax :: Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax Integer
m [PlusLevel' Term]
as []              = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m [PlusLevel' Term]
as
    lmax Integer
m [PlusLevel' Term]
as (Max Integer
n [PlusLevel' Term]
bs : [Level]
ls) = Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel' Term]
bs [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. [a] -> [a] -> [a]
++! [PlusLevel' Term]
as) [Level]
ls

    expandLevel :: Level -> Level
    expandLevel :: Level -> Level
expandLevel (Max Integer
m [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> [Level] -> Level
lmax Integer
m [] ([Level] -> Level) -> [Level] -> Level
forall a b. (a -> b) -> a -> b
$ (PlusLevel' Term -> Level) -> [PlusLevel' Term] -> [Level]
forall a b. (a -> b) -> [a] -> [b]
map'' PlusLevel' Term -> Level
expandPlus [PlusLevel' Term]
as

    expandPlus :: PlusLevel -> Level
    expandPlus :: PlusLevel' Term -> Level
expandPlus (Plus Integer
m Term
l) = Integer -> Level -> Level
levelPlus Integer
m (Term -> Level
expandTm Term
l)

    expandTm :: Term -> Level
expandTm (Level Level
l)       = Level -> Level
expandLevel Level
l
    expandTm Term
l               = Term -> Level
forall t. t -> Level' t
atomicLevel Term
l

    removeSubsumed :: [PlusLevel' Term] -> [PlusLevel' Term]
removeSubsumed =
      ((Term, Integer) -> PlusLevel' Term)
-> [(Term, Integer)] -> [PlusLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map' (\(Term
a, Integer
n) -> Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n Term
a) ([(Term, Integer)] -> [PlusLevel' Term])
-> ([PlusLevel' Term] -> [(Term, Integer)])
-> [PlusLevel' Term]
-> [PlusLevel' Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      Map Term Integer -> [(Term, Integer)]
forall k a. Map k a -> [(k, a)]
MapS.toAscList (Map Term Integer -> [(Term, Integer)])
-> ([PlusLevel' Term] -> Map Term Integer)
-> [PlusLevel' Term]
-> [(Term, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      (Integer -> Integer -> Integer)
-> [(Term, Integer)] -> Map Term Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
MapS.fromListWith Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max ([(Term, Integer)] -> Map Term Integer)
-> ([PlusLevel' Term] -> [(Term, Integer)])
-> [PlusLevel' Term]
-> Map Term Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      (PlusLevel' Term -> (Term, Integer))
-> [PlusLevel' Term] -> [(Term, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map' (\(Plus Integer
n Term
a) -> (Term
a, Integer
n))

-- | Given two levels @a@ and @b@, compute @a ⊔ b@ and return its
--   canonical form.
levelLub :: Level -> Level -> Level
levelLub :: Level -> Level -> Level
levelLub (Max Integer
m [PlusLevel' Term]
as) (Max Integer
n [PlusLevel' Term]
bs) = Integer -> [PlusLevel' Term] -> Level
levelMax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$! [PlusLevel' Term]
as [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. [a] -> [a] -> [a]
++! [PlusLevel' Term]
bs

levelTm :: Level -> Term
levelTm :: Level -> Term
levelTm Level
l =
  case Level
l of
    Max Integer
0 [Plus Integer
0 Term
l] -> Term
l
    Level
_                -> Level -> Term
Level Level
l