{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | 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 Agda.TypeChecking.Substitute
  ( module Agda.TypeChecking.Substitute
  , module Agda.TypeChecking.Substitute.Class
  , module Agda.TypeChecking.Substitute.DeBruijn
  , Substitution'(..), Substitution
  ) where

import Control.Arrow (first, second)
import Control.Monad (guard)
import Control.Monad.Except (throwError)

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

import Debug.Trace (trace)

import Agda.Interaction.Options

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options (typeInType)
import Agda.TypeChecking.Free as Free
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence as Occ

import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Substitute.DeBruijn

import Agda.Utils.Either
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible


-- | 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.
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term #-}
{-# SPECIALIZE applyTermE :: (Empty -> Term -> Elims -> Term) -> BraveTerm -> Elims -> BraveTerm #-}
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 [] = t
m
applyTermE Empty -> Term -> Elims -> Term
err' 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
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
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 [Char]
s Elims
es' -> [Char] -> Elims -> Term
Dummy [Char]
s (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
     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 ->  [Char] -> Elims -> Term
Dummy [Char]
"applyE" (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
t) Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
es))

-- | 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
_ [Arg QName]
fs) ConInfo
_ Elims
vs) -> do
      (Arg QName
fld, Int
i) <- (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex ((QName
fQName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool) -> (Arg QName -> QName) -> Arg QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> QName
forall e. Arg e -> e
unArg) [Arg QName]
fs
      -- Jesper, 2019-10-17: dont unfold irrelevant projections
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Arg QName -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Arg QName
fld
      -- Andreas, 2018-06-12, issue #2170
      -- The ArgInfo from the ConHead is more accurate (relevance subtyping!).
      ArgInfo -> Arg Term -> Arg Term
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (Arg QName -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg QName
fld) (Arg Term -> Arg Term)
-> (Elim' Term -> Maybe (Arg Term))
-> Elim' Term
-> Maybe (Arg Term)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Elim' Term -> Maybe (Arg Term)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim (Elim' Term -> Maybe (Arg Term))
-> Maybe (Elim' Term) -> Maybe (Arg Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Elims -> Maybe (Elim' Term)
forall a. [a] -> Maybe a
listToMaybe (Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop Int
i Elims
vs)
    Term
_ -> Maybe (Arg Term)
forall a. Maybe a
Nothing

-- | 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 ConHead
ch                    ConInfo
ci Elims
args []                  = ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args
conApp Empty -> Term -> Elims -> Term
fallback ConHead
ch                    ConInfo
ci Elims
args    (a :: Elim' Term
a@Apply{} : Elims
es) = forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
fallback ConHead
ch ConInfo
ci (Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim' Term
a]) Elims
es
conApp Empty -> Term -> Elims -> Term
fallback ConHead
ch                    ConInfo
ci Elims
args   (a :: Elim' Term
a@IApply{} : Elims
es) = forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
fallback ConHead
ch ConInfo
ci (Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim' Term
a]) Elims
es
conApp Empty -> Term -> Elims -> Term
fallback ch :: ConHead
ch@(ConHead QName
c DataOrRecord
_ Induction
_ [Arg QName]
fs) ConInfo
ci Elims
args ees :: Elims
ees@(Proj ProjOrigin
o QName
f : Elims
es) =
  let failure :: forall a. a -> a
      failure :: forall a. a -> a
failure a
err = ([Char] -> a -> a) -> a -> [Char] -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Char] -> a -> a
forall a. [Char] -> a -> a
trace a
err ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [Char]
"conApp: constructor ", QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
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]
: (Arg QName -> [Char]) -> [Arg QName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> (Arg QName -> [Char]) -> Arg QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) [Arg QName]
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' Term -> [Char]) -> Elims -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char])
-> (Elim' Term -> [Char]) -> Elim' Term -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) Elims
args
        , [Char]
" projected by ", QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f
        ]
      isApply :: Elim' a -> Arg a
isApply Elim' a
e = Arg a -> Maybe (Arg a) -> Arg a
forall a. a -> Maybe a -> a
fromMaybe (Arg a -> Arg a
forall a. a -> a
failure Arg a
forall a. HasCallStack => a
__IMPOSSIBLE__) (Maybe (Arg a) -> Arg a) -> Maybe (Arg a) -> Arg a
forall a b. (a -> b) -> a -> b
$ Elim' a -> Maybe (Arg a)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elim' a
e
      stuck :: Empty -> Term
stuck Empty
err = Empty -> Term -> Elims -> Term
fallback Empty
err (ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args) [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f]
      -- Recurse using the instance for 't', see @applyTermE@
      app :: Term -> Elims -> Term
      app :: Term -> Elims -> Term
app Term
v Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ 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
  in
   case (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex ((QName
fQName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool) -> (Arg QName -> QName) -> Arg QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> QName
forall e. Arg e -> e
unArg) [Arg QName]
fs of
     Maybe (Arg QName, Int)
Nothing -> Term -> Term
forall a. a -> a
failure (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term
stuck Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Elims -> Term
`app` Elims
es
     Just (Arg QName
fld, Int
i) -> let
      -- Andreas, 2018-06-12, issue #2170
      -- We safe-guard the projected value by DontCare using the ArgInfo stored at the record constructor,
      -- since the ArgInfo in the constructor application might be inaccurate because of subtyping.
      v :: Term
v = Term -> (Elim' Term -> Term) -> Maybe (Elim' Term) -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Term -> Term
forall a. a -> a
failure (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Empty -> Term
stuck Empty
forall a. HasCallStack => a
__IMPOSSIBLE__) (Arg QName -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare Arg QName
fld (Term -> Term) -> (Elim' Term -> Term) -> Elim' Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
argToDontCare (Arg Term -> Term)
-> (Elim' Term -> Arg Term) -> Elim' Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> Arg Term
forall {a}. Elim' a -> Arg a
isApply) (Maybe (Elim' Term) -> Term) -> Maybe (Elim' Term) -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe (Elim' Term)
forall a. [a] -> Maybe a
listToMaybe (Elims -> Maybe (Elim' Term)) -> Elims -> Maybe (Elim' Term)
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Elims
forall a. Int -> [a] -> [a]
drop Int
i Elims
args
      in Term
v Term -> Elims -> Term
`app` Elims
es

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

{-
      i = maybe failure id    $ elemIndex f $ map unArg fs
      v = maybe failure unArg $ listToMaybe $ drop i args
      -- Andreas, 2013-10-20 see Issue543a:
      -- protect result of irrelevant projection.
      r = maybe __IMPOSSIBLE__ getRelevance $ listToMaybe $ drop i fs
      u | Irrelevant <- r = DontCare v
        | otherwise       = v
  in  applyE v es
-}

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

-- protect irrelevant fields (see issue 610)
argToDontCare :: Arg Term -> Term
argToDontCare :: Arg Term -> Term
argToDontCare (Arg ArgInfo
ai Term
v) = ArgInfo -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai Term
v

relToDontCare :: LensRelevance a => a -> Term -> Term
relToDontCare :: forall a. LensRelevance a => a -> Term -> Term
relToDontCare a
ai Term
v
  | Relevance
Irrelevant <- a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance a
ai = Term -> Term
dontCare Term
v
  | Bool
otherwise                     = Term
v

-- 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply Definition where
  apply :: Definition -> Args -> Definition
apply (Defn ArgInfo
info QName
x Type
t [Polarity]
pol [Occurrence]
occ NumGeneralizableArgs
gens [Maybe Name]
gpars [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe QName
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang Defn
d) Args
args =
    ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> 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) (NumGeneralizableArgs -> Args -> NumGeneralizableArgs
forall t. Apply t => t -> Args -> t
apply NumGeneralizableArgs
gens 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 QName
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang (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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply RewriteRule where
  apply :: RewriteRule -> Args -> RewriteRule
apply RewriteRule
r Args
args =
    let newContext :: Telescope
newContext = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply (RewriteRule -> Telescope
rewContext RewriteRule
r) Args
args
        sub :: Substitution' NLPat
sub        = Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
newContext) (Substitution' NLPat -> Substitution' NLPat)
-> Substitution' NLPat -> Substitution' NLPat
forall a b. (a -> b) -> a -> b
$ [NLPat] -> Substitution' NLPat
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([NLPat] -> Substitution' NLPat) -> [NLPat] -> Substitution' NLPat
forall a b. (a -> b) -> a -> b
$
                       [NLPat] -> [NLPat]
forall a. [a] -> [a]
reverse ([NLPat] -> [NLPat]) -> [NLPat] -> [NLPat]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> NLPat) -> Args -> [NLPat]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> NLPat
PTerm (Term -> NLPat) -> (Arg Term -> Term) -> Arg Term -> NLPat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Args
args
    in RewriteRule
       { rewName :: QName
rewName    = RewriteRule -> QName
rewName RewriteRule
r
       , rewContext :: Telescope
rewContext = Telescope
newContext
       , rewHead :: QName
rewHead    = RewriteRule -> QName
rewHead RewriteRule
r
       , rewPats :: PElims
rewPats    = Substitution' (SubstArg PElims) -> PElims -> PElims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg PElims)
Substitution' NLPat
sub (RewriteRule -> PElims
rewPats RewriteRule
r)
       , rewRHS :: Term
rewRHS     = Substitution' NLPat -> Term -> Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (RewriteRule -> Term
rewRHS RewriteRule
r)
       , rewType :: Type
rewType    = Substitution' NLPat -> Type -> Type
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (RewriteRule -> Type
rewType RewriteRule
r)
       , rewFromClause :: Bool
rewFromClause = RewriteRule -> Bool
rewFromClause RewriteRule
r
       }

  applyE :: RewriteRule -> Elims -> RewriteRule
applyE RewriteRule
t Elims
es = RewriteRule -> Args -> RewriteRule
forall t. Apply t => t -> Args -> t
apply RewriteRule
t (Args -> RewriteRule) -> Args -> RewriteRule
forall a b. (a -> b) -> a -> b
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply NumGeneralizableArgs where
  apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs
apply NumGeneralizableArgs
NoGeneralizableArgs       Args
args = NumGeneralizableArgs
NoGeneralizableArgs
  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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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
            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__
            IApplyP{} -> [NamedArg (Pattern' x)]
recurse

  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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply Projection where
  apply :: Projection -> Args -> Projection
apply Projection
p Args
args = Projection
p
    { projIndex :: Int
projIndex = Projection -> Int
projIndex Projection
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args
    , projLams :: ProjLams
projLams  = Projection -> ProjLams
projLams Projection
p ProjLams -> Args -> ProjLams
forall t. Apply t => t -> Args -> t
`apply` Args
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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply ProjLams where
  apply :: ProjLams -> Args -> ProjLams
apply (ProjLams [Arg [Char]]
lams) Args
args = [Arg [Char]] -> ProjLams
ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
forall a b. (a -> b) -> a -> b
$ Int -> [Arg [Char]] -> [Arg [Char]]
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 [Char]]
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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply Defn where
  apply :: Defn -> Args -> Defn
apply Defn
d [] = Defn
d
  apply Defn
d args :: Args
args@(Arg Term
arg1:Args
args1) = 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{} -> Defn
d
    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 :: [Clause]
funClauses    = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args
        , funCompiled :: Maybe CompiledClauses
funCompiled   = Maybe CompiledClauses -> Args -> Maybe CompiledClauses
forall t. Apply t => t -> Args -> t
apply Maybe CompiledClauses
cc Args
args
        , funCovering :: [Clause]
funCovering   = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cov Args
args
        , funInv :: FunctionInverse
funInv        = FunctionInverse -> Args -> FunctionInverse
forall t. Apply t => t -> Args -> t
apply FunctionInverse
inv Args
args
        , funExtLam :: Maybe ExtLamInfo
funExtLam     = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (System -> Args -> System
forall t. Apply t => t -> Args -> t
`apply` Args
args) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
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
p0 } ->
      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 }
          | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     -> Defn
d { funProjection :: Either ProjectionLikenessMissing Projection
funProjection = Either ProjectionLikenessMissing Projection
forall a. HasCallStack => a
__IMPOSSIBLE__ } -- TODO (#3123): we actually get here!
          -- case: applied only to parameters
          | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     -> Defn
d { funProjection :: Either ProjectionLikenessMissing Projection
funProjection = Projection -> Either ProjectionLikenessMissing Projection
forall a b. b -> Either a b
Right Projection
p }
          -- case: applied also to record value (n == 0)
          | Bool
otherwise ->
              Defn
d { funClauses :: [Clause]
funClauses        = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args'
                , funCompiled :: Maybe CompiledClauses
funCompiled       = Maybe CompiledClauses -> Args -> Maybe CompiledClauses
forall t. Apply t => t -> Args -> t
apply Maybe CompiledClauses
cc Args
args'
                , funCovering :: [Clause]
funCovering       = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cov Args
args'
                , funInv :: FunctionInverse
funInv            = FunctionInverse -> Args -> FunctionInverse
forall t. Apply t => t -> Args -> t
apply FunctionInverse
inv Args
args'
                , funProjection :: Either ProjectionLikenessMissing Projection
funProjection     = if Bool
isVar0 then Projection -> Either ProjectionLikenessMissing Projection
forall a b. b -> Either a b
Right Projection
p{ projIndex :: Int
projIndex = Int
0 } else ProjectionLikenessMissing
-> Either ProjectionLikenessMissing Projection
forall a b. a -> Either a b
Left ProjectionLikenessMissing
MaybeProjection
                , funExtLam :: Maybe ExtLamInfo
funExtLam         = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (\ System
_ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
extLam
                }
              where
                larg :: Arg Term
larg  = Arg Term -> Args -> Arg Term
forall a. a -> [a] -> a
last1 Arg Term
arg1 Args
args1 -- the record value
                args' :: Args
args' = [Arg Term
larg]
                isVar0 :: Bool
isVar0 = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
larg 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 :: Int
dataPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args
        , dataClause :: Maybe Clause
dataClause     = Maybe Clause -> Args -> Maybe Clause
forall t. Apply t => t -> Args -> t
apply Maybe Clause
cl Args
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 :: Int
recPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args
        , recClause :: Maybe Clause
recClause = Maybe Clause -> Args -> Maybe Clause
forall t. Apply t => t -> Args -> t
apply Maybe Clause
cl Args
args, recTel :: Telescope
recTel = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
tel Args
args
--        , recArgOccurrences = List.drop (length args) occ
        }
    Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
      Defn
d { conPars :: Int
conPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args }
    Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
      Defn
d { primClauses :: [Clause]
primClauses = [Clause] -> Args -> [Clause]
forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply PrimFun where
  apply :: PrimFun -> Args -> PrimFun
apply (PrimFun QName
x Int
ar Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) Args
args = QName
-> Int
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Args -> Int
forall a. Sized a => a -> Int
size Args
args) ((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
args Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
vs)
  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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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 Bool
catchall Maybe Bool
exact Maybe Bool
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)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> 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)
             Bool
catchall
             Maybe Bool
exact
             Maybe Bool
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 [Char]
_ 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]
ps' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
ps) (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__
            IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar [Char]
_ 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 [Char]
_ 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]
ps' [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
ps) (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__
            IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar [Char]
_ 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 = [ ArgInfo -> Term -> Term
forall a. LensRelevance a => a -> Term -> Term
relToDontCare ArgInfo
ai (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                            -- #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 (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai 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]
                          | Arg ArgInfo
ai QName
f <- ConHead -> [Arg 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply CompiledClauses where
  apply :: CompiledClauses -> Args -> CompiledClauses
apply CompiledClauses
cc Args
args = case CompiledClauses
cc of
    Fail [Arg [Char]]
hs -> [Arg [Char]] -> CompiledClauses
forall a. [Arg [Char]] -> CompiledClauses' a
Fail (Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
drop Int
len [Arg [Char]]
hs)
    Done [Arg [Char]]
hs Term
t
      | [Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
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 [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
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  [Arg [Char]] -> Term -> CompiledClauses
forall a. [Arg [Char]] -> a -> CompiledClauses' a
Done (Int -> [Arg [Char]] -> [Arg [Char]]
forall a. Int -> [a] -> [a]
List.drop Int
len [Arg [Char]]
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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 a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- Bool -> Bool
forall a. a -> a
id) (Face -> Face) -> (Term -> Term) -> (Face, Term) -> (Face, Term)
forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
-*- 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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 d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, 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 d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

instance Apply DisplayTerm where
  apply :: DisplayTerm -> Args -> DisplayTerm
apply (DTerm Term
v)          Args
args = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
v Args
args
  apply (DDot Term
v)           Args
args = Term -> DisplayTerm
DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
v 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 [DisplayTerm]
ws Elims
es) Args
args = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
v [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 = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v Elims
es
  applyE (DDot Term
v)            Elims
es = Term -> DisplayTerm
DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v 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 = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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 [DisplayTerm]
ws Elims
es') Elims
es = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp DisplayTerm
v [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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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]
  -- NB: section (- m) not possible (unary minus), hence (flip (-) m)
  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) -> Int -> Int -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip (-) 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
$ Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims 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 Type
t []                      = Type
t
piApply (El Sort
_ (Pi  Dom Type
_ Abs Type
b)) (Arg Term
a:Args
args) = Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Type
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Type -> Args -> Type
`piApply` Args
args
piApply Type
t Args
args                    =
  [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__

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

instance Abstract Term where
  abstract :: Telescope -> Term -> Term
abstract = Telescope -> Term -> Term
teleLam

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

instance Abstract Sort where
  abstract :: Telescope -> Sort -> Sort
abstract Telescope
EmptyTel Sort
s = Sort
s
  abstract Telescope
_        Sort
s = Sort
forall a. HasCallStack => a
__IMPOSSIBLE__

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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 ArgInfo
info QName
x Type
t [Polarity]
pol [Occurrence]
occ NumGeneralizableArgs
gens [Maybe Name]
gpars [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe QName
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang Defn
d) =
    ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> Language
-> Defn
-> Definition
Defn ArgInfo
info QName
x (Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Type
t) (Telescope -> [Polarity] -> [Polarity]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Polarity]
pol) (Telescope -> [Occurrence] -> [Occurrence]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Occurrence]
occ) (Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel NumGeneralizableArgs
gens)
      (Int -> Maybe Name -> [Maybe Name]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Maybe Name
forall a. Maybe a
Nothing [Maybe Name] -> [Maybe Name] -> [Maybe Name]
forall a. [a] -> [a] -> [a]
++ [Maybe Name]
gpars)
      [LocalDisplayForm]
df MutualId
m CompiledRepresentation
c Maybe QName
inst Bool
copy Set QName
ma Bool
nc Bool
inj Bool
copat Blocked_
blk Language
lang (Telescope -> Defn -> Defn
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Defn
d)

-- | @tel ⊢ (Γ ⊢ lhs ↦ rhs : t)@ becomes @tel, Γ ⊢ lhs ↦ rhs : t)@
--   we do not need to change lhs, rhs, and t since they live in Γ.
--   See 'Abstract Clause'.
instance Abstract RewriteRule where
  abstract :: Telescope -> RewriteRule -> RewriteRule
abstract Telescope
tel (RewriteRule QName
q Telescope
gamma QName
f PElims
ps Term
rhs Type
t Bool
c) =
    QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
q (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
gamma) QName
f PElims
ps Term
rhs Type
t Bool
c

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 NumGeneralizableArgs
NoGeneralizableArgs       = NumGeneralizableArgs
NoGeneralizableArgs
  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 :: Int
projIndex = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Projection -> Int
projIndex Projection
p
    , projLams :: ProjLams
projLams  = Telescope -> ProjLams -> ProjLams
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (ProjLams -> ProjLams) -> ProjLams -> ProjLams
forall a b. (a -> b) -> a -> b
$ Projection -> ProjLams
projLams Projection
p
    }

instance Abstract ProjLams where
  abstract :: Telescope -> ProjLams -> ProjLams
abstract Telescope
tel (ProjLams [Arg [Char]]
lams) = [Arg [Char]] -> ProjLams
ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
forall a b. (a -> b) -> a -> b
$
    (Dom' Term ([Char], Type) -> Arg [Char])
-> [Dom' Term ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ !Dom' Term ([Char], Type)
dom -> Dom' Term [Char] -> Arg [Char]
forall t a. Dom' t a -> Arg a
argFromDom (([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char])
-> Dom' Term ([Char], Type) -> Dom' Term [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term ([Char], Type)
dom)) (Telescope -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel) [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
forall a. [a] -> [a] -> [a]
++ [Arg [Char]]
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{} -> Defn
d
    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 :: [Clause]
funClauses  = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cs
        , funCompiled :: Maybe CompiledClauses
funCompiled = Telescope -> Maybe CompiledClauses -> Maybe CompiledClauses
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe CompiledClauses
cc
        , funCovering :: [Clause]
funCovering = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cov
        , funInv :: FunctionInverse
funInv      = Telescope -> FunctionInverse -> FunctionInverse
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel FunctionInverse
inv
        , funExtLam :: Maybe ExtLamInfo
funExtLam   = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (Telescope -> System -> System
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
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 :: Either ProjectionLikenessMissing Projection
funProjection = Projection -> Either ProjectionLikenessMissing Projection
forall a b. b -> Either a b
Right (Projection -> Either ProjectionLikenessMissing Projection)
-> Projection -> Either ProjectionLikenessMissing Projection
forall a b. (a -> b) -> a -> b
$ Telescope -> Projection -> Projection
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Projection
p
          , funClauses :: [Clause]
funClauses    = (Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map (Telescope -> Clause -> Clause
abstractClause Telescope
forall a. Tele a
EmptyTel) [Clause]
cs
          }
      else
        Defn
d { funProjection :: Either ProjectionLikenessMissing Projection
funProjection = Projection -> Either ProjectionLikenessMissing Projection
forall a b. b -> Either a b
Right (Projection -> Either ProjectionLikenessMissing Projection)
-> Projection -> Either ProjectionLikenessMissing Projection
forall a b. (a -> b) -> a -> b
$ Telescope -> Projection -> Projection
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Projection
p
          , funClauses :: [Clause]
funClauses    = (Clause -> Clause) -> [Clause] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map (Telescope -> Clause -> Clause
abstractClause Telescope
tel1) [Clause]
cs
          , funCompiled :: Maybe CompiledClauses
funCompiled   = Telescope -> Maybe CompiledClauses -> Maybe CompiledClauses
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 Maybe CompiledClauses
cc
          , funCovering :: [Clause]
funCovering   = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 [Clause]
cov
          , funInv :: FunctionInverse
funInv        = Telescope -> FunctionInverse -> FunctionInverse
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 FunctionInverse
inv
          , funExtLam :: Maybe ExtLamInfo
funExtLam     = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (\ System
_ -> System
forall a. HasCallStack => a
__IMPOSSIBLE__) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
extLam
          }
        where
          tel1 :: Telescope
tel1 = [Dom' Term ([Char], Type)] -> Telescope
telFromList ([Dom' Term ([Char], Type)] -> Telescope)
-> [Dom' Term ([Char], Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], 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 ([Char], Type)] -> [Dom' Term ([Char], Type)])
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], 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 :: Telescope
clauseTel = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
c }

    Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
      Defn
d { dataPars :: Int
dataPars       = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
        , dataClause :: Maybe Clause
dataClause     = Telescope -> Maybe Clause -> Maybe Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe Clause
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 :: Int
recPars    = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
        , recClause :: Maybe Clause
recClause  = Telescope -> Maybe Clause -> Maybe Clause
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Maybe Clause
cl
        , recTel :: Telescope
recTel     = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel'
        }
    Constructor{ conPars :: Defn -> Int
conPars = Int
np } ->
      Defn
d { conPars :: Int
conPars = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel }
    Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
      Defn
d { primClauses :: [Clause]
primClauses = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel [Clause]
cs }
    PrimitiveSort{} -> Defn
d

instance Abstract PrimFun where
    abstract :: Telescope -> PrimFun -> PrimFun
abstract Telescope
tel (PrimFun QName
x Int
ar Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) = QName
-> Int
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) ((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 Bool
catchall Maybe Bool
exact Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
    Range
-> Range
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> 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
           Bool
catchall
           Maybe Bool
exact
           Maybe Bool
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 [Char]]
xs   -> [Arg [Char]] -> CompiledClauses
forall a. [Arg [Char]] -> CompiledClauses' a
Fail ([Arg [Char]]
hs [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
forall a. [a] -> [a] -> [a]
++ [Arg [Char]]
xs)
      Done [Arg [Char]]
xs Term
t -> [Arg [Char]] -> Term -> CompiledClauses
forall a. [Arg [Char]] -> a -> CompiledClauses' a
Done ([Arg [Char]]
hs [Arg [Char]] -> [Arg [Char]] -> [Arg [Char]]
forall a. [a] -> [a] -> [a]
++ [Arg [Char]]
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 [Char]]
hs = (Dom' Term ([Char], Type) -> Arg [Char])
-> [Dom' Term ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term [Char] -> Arg [Char]
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term [Char] -> Arg [Char])
-> (Dom' Term ([Char], Type) -> Dom' Term [Char])
-> Dom' Term ([Char], Type)
-> Arg [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], Type) -> [Char])
-> Dom' Term ([Char], Type) -> Dom' Term [Char]
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst) ([Dom' Term ([Char], Type)] -> [Arg [Char]])
-> [Dom' Term ([Char], Type)] -> [Arg [Char]]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], 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 d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, 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) =
  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) (Int -> [Char] -> Named NamedName DeBruijnPattern
namedDBVarP (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ([Char] -> Named NamedName DeBruijnPattern)
-> [Char] -> Named NamedName DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Abs Telescope -> [Char]
forall a. Abs a -> [Char]
absName Abs Telescope
tel) NamedArg DeBruijnPattern
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. a -> [a] -> [a]
:
  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)

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

abstractArgs :: Abstract a => Args -> a -> a
abstractArgs :: forall a. Abstract a => Args -> a -> a
abstractArgs Args
args a
x = Telescope -> a -> a
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel a
x
    where
        tel :: Telescope
tel   = (Arg [Char] -> Telescope -> Telescope)
-> Telescope -> [Arg [Char]] -> Telescope
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\arg :: Arg [Char]
arg@(Arg ArgInfo
info [Char]
x) -> Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
HasCallStack => Type
__DUMMY_TYPE__ Type -> Dom' Term [Char] -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg [Char] -> Dom' Term [Char]
forall a. Arg a -> Dom a
domFromArg Arg [Char]
arg) (Abs Telescope -> Telescope)
-> (Telescope -> Abs Telescope) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Telescope -> Abs Telescope
forall a. [Char] -> a -> Abs a
Abs [Char]
x)
                      Telescope
forall a. Tele a
EmptyTel
              ([Arg [Char]] -> Telescope) -> [Arg [Char]] -> Telescope
forall a b. (a -> b) -> a -> b
$ ([Char] -> Arg Term -> Arg [Char])
-> [[Char]] -> Args -> [Arg [Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Char] -> Arg Term -> Arg [Char]
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [[Char]]
names Args
args
        names :: [[Char]]
names = [[Char]] -> [[Char]]
forall a. HasCallStack => [a] -> [a]
cycle ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (Char -> [Char]) -> [Char] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char]
stringToArgName ([Char] -> [Char]) -> (Char -> [Char]) -> Char -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:[])) [Char
'a'..Char
'z']

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

-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renaming _ π) : Term Γ -> Term Δ@
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 Γ@
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. (right-to-left list)
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

{-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-}
{-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-}
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    -> t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' t -> Int -> t
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' t
rho Int
i  t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims -> Elims
subE 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) => b -> b
sub @(Abs t) 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
$ Elims -> Elims
subE 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
$ Elims -> Elims
subE Elims
vs
    MetaV MetaId
x Elims
es  -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
subE 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) => b -> b
sub @(Level' t) Level
l
    Pi Dom Type
a Abs Type
b      -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi ((Dom Type, Abs Type) -> Term) -> (Dom Type, Abs Type) -> Term
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Type) -> (Dom Type, Abs Type)
subPi (Dom Type
a,Abs Type
b)
    Sort Sort
s      -> Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ forall a b. (Coercible b a, SubstWith t a) => b -> b
sub @(Sort' t) Sort
s
    DontCare Term
mv -> Term -> Term
dontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ forall a b. (Coercible b a, SubstWith t a) => b -> b
sub @t Term
mv
    Dummy [Char]
s Elims
es  -> [Char] -> Elims -> Term
Dummy [Char]
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
subE Elims
es
 where
   sub :: forall a b. (Coercible b a, SubstWith t a) => b -> b
   sub :: forall a b. (Coercible b a, SubstWith t a) => b -> b
sub b
t = a -> b
forall a b. Coercible a b => a -> b
coerce (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ 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)
   subE :: Elims -> Elims
   subE :: Elims -> Elims
subE  = forall a b. (Coercible b a, SubstWith t a) => b -> b
sub @[Elim' t]
   subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
   subPi :: (Dom Type, Abs Type) -> (Dom Type, Abs Type)
subPi = forall a b. (Coercible b a, SubstWith t a) => b -> b
sub @(Dom' t (Type'' t t), Abs (Type'' t t))

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

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 (Coercible a Term, 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 (Coercible a Term, 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
    Type Level' a
n     -> Level' a -> Sort' a
forall t. Level' t -> Sort' t
Type (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Level' a -> Level' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Level' a
n
    Prop Level' a
n     -> Level' a -> Sort' a
forall t. Level' t -> Sort' t
Prop (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Level' a -> Level' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Level' a
n
    Inf IsFibrant
f Integer
n    -> IsFibrant -> Integer -> Sort' a
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
    SSet Level' a
n     -> Level' a -> Sort' a
forall t. Level' t -> Sort' t
SSet (Level' a -> Sort' a) -> Level' a -> Sort' a
forall a b. (a -> b) -> a -> b
$ Level' a -> Level' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Level' a
n
    Sort' a
SizeUniv   -> Sort' a
forall t. Sort' t
SizeUniv
    Sort' a
LockUniv   -> Sort' a
forall t. Sort' t
LockUniv
    Sort' a
IntervalUniv -> Sort' a
forall t. Sort' t
IntervalUniv
    PiSort Dom' a a
a Sort' a
s1 Abs (Sort' a)
s2 -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Sort
piSort (Dom' a a -> Dom Term
forall a b. Coercible a b => a -> b
coerce (Dom' a a -> Dom Term) -> Dom' a a -> Dom Term
forall a b. (a -> b) -> a -> b
$ Dom' a a -> Dom' a a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Dom' a a
a) (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s1) (Abs (Sort' a) -> Abs Sort
forall a b. Coercible a b => a -> b
coerce (Abs (Sort' a) -> Abs Sort) -> Abs (Sort' a) -> Abs Sort
forall a b. (a -> b) -> a -> b
$ Abs (Sort' a) -> Abs (Sort' a)
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Abs (Sort' a)
s2)
    FunSort Sort' a
s1 Sort' a
s2 -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s1) (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s2)
    UnivSort Sort' a
s -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
univSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub 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
$ [Elim' a] -> [Elim' a]
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub [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
$ [Elim' a] -> [Elim' a]
forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub [Elim' a]
es
    s :: Sort' a
s@DummyS{} -> Sort' a
s
    where
      sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
      sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub b
x = Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (Sort' a))
rho b
x

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 [PlusLevel' a])
-> [PlusLevel' a] -> [PlusLevel' a]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [PlusLevel' a])
Substitution' (SubstArg (Level' 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 :: Maybe (Arg Type)
conPType = Substitution' (SubstArg (Maybe (Arg Type)))
-> Maybe (Arg Type) -> Maybe (Arg Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Maybe (Arg Type)))
Substitution' (SubstArg ConPatternInfo)
rho (Maybe (Arg Type) -> Maybe (Arg Type))
-> Maybe (Arg Type) -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
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 Pattern)
Substitution' (SubstArg Term)
rho Term
t
    p :: Pattern
p@(VarP PatternInfo
_o [Char]
_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 [Char]
x -> PatternInfo -> Term -> Term -> [Char] -> 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 Pattern)
Substitution' (SubstArg Term)
rho Term
t) (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Pattern)
Substitution' (SubstArg Term)
rho Term
u) [Char]
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

instance DeBruijn NLPat where
  deBruijnVar :: Int -> NLPat
deBruijnVar Int
i = Int -> [Arg Int] -> NLPat
PVar Int
i []
  deBruijnView :: NLPat -> Maybe Int
deBruijnView = \case
    PVar Int
i []   -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
    PVar{}      -> Maybe Int
forall a. Maybe a
Nothing
    PDef{}      -> Maybe Int
forall a. Maybe a
Nothing
    PLam{}      -> Maybe Int
forall a. Maybe a
Nothing
    PPi{}       -> Maybe Int
forall a. Maybe a
Nothing
    PSort{}     -> Maybe Int
forall a. Maybe a
Nothing
    PBoundVar{} -> Maybe Int
forall a. Maybe a
Nothing -- or... ?
    PTerm{}     -> Maybe Int
forall a. Maybe a
Nothing -- or... ?

applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst :: forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst = Substitution' Term -> a -> a
Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' Term -> a -> a)
-> (Substitution' NLPat -> Substitution' Term)
-> Substitution' NLPat
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NLPat -> Term) -> Substitution' NLPat -> Substitution' Term
forall a b. (a -> b) -> Substitution' a -> Substitution' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NLPat -> Term
nlPatToTerm
  where
    nlPatToTerm :: NLPat -> Term
    nlPatToTerm :: NLPat -> Term
nlPatToTerm = \case
      PVar Int
i [Arg Int]
xs      -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Int -> Elim' Term) -> [Arg Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term)
-> (Arg Int -> Arg Term) -> Arg Int -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Term) -> Arg Int -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
xs
      PTerm Term
u        -> Term
u
      PDef QName
f PElims
es      -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PLam ArgInfo
i Abs NLPat
u       -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PPi Dom NLPType
a Abs NLPType
b        -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PSort NLPSort
s        -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PBoundVar Int
i PElims
es -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__

applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom :: forall a.
SubstWith NLPat a =>
Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' NLPat
rho Dom a
dom = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' NLPat
rho (a -> a) -> Dom a -> Dom a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom a
dom{ domTactic :: Maybe Term
domTactic = Substitution' NLPat -> Maybe Term -> Maybe Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
rho (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Dom a -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom a
dom }

instance Subst NLPat where
  type SubstArg NLPat = NLPat
  applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat
applySubst Substitution' (SubstArg NLPat)
rho = \case
    PVar Int
i [Arg Int]
bvs     -> Substitution' NLPat -> Int -> NLPat
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' (SubstArg NLPat)
Substitution' NLPat
rho Int
i NLPat -> [Arg Int] -> NLPat
`applyBV` [Arg Int]
bvs
    PDef QName
f PElims
es      -> QName -> PElims -> NLPat
PDef QName
f (PElims -> NLPat) -> PElims -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg PElims) -> PElims -> PElims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg PElims)
Substitution' (SubstArg NLPat)
rho PElims
es
    PLam ArgInfo
i Abs NLPat
u       -> ArgInfo -> Abs NLPat -> NLPat
PLam ArgInfo
i (Abs NLPat -> NLPat) -> Abs NLPat -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Abs NLPat)) -> Abs NLPat -> Abs NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Abs NLPat))
Substitution' (SubstArg NLPat)
rho Abs NLPat
u
    PPi Dom NLPType
a Abs NLPType
b        -> Dom NLPType -> Abs NLPType -> NLPat
PPi (Substitution' NLPat -> Dom NLPType -> Dom NLPType
forall a.
SubstWith NLPat a =>
Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' (SubstArg NLPat)
Substitution' NLPat
rho Dom NLPType
a) (Substitution' (SubstArg (Abs NLPType))
-> Abs NLPType -> Abs NLPType
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Abs NLPType))
Substitution' (SubstArg NLPat)
rho Abs NLPType
b)
    PSort NLPSort
s        -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> NLPSort -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPat)
rho NLPSort
s
    PBoundVar Int
i PElims
es -> Int -> PElims -> NLPat
PBoundVar Int
i (PElims -> NLPat) -> PElims -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg PElims) -> PElims -> PElims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg PElims)
Substitution' (SubstArg NLPat)
rho PElims
es
    PTerm Term
u        -> Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> Term -> Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' (SubstArg NLPat)
Substitution' NLPat
rho Term
u

    where
      applyBV :: NLPat -> [Arg Int] -> NLPat
      applyBV :: NLPat -> [Arg Int] -> NLPat
applyBV NLPat
p [Arg Int]
ys = case NLPat
p of
        PVar Int
i [Arg Int]
xs      -> Int -> [Arg Int] -> NLPat
PVar Int
i ([Arg Int]
xs [Arg Int] -> [Arg Int] -> [Arg Int]
forall a. [a] -> [a] -> [a]
++ [Arg Int]
ys)
        PTerm Term
u        -> Term -> NLPat
PTerm (Term -> NLPat) -> Term -> NLPat
forall a b. (a -> b) -> a -> b
$ Term
u Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (Arg Int -> Arg Term) -> [Arg Int] -> Args
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Term) -> Arg Int -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Term
var) [Arg Int]
ys
        PDef QName
f PElims
es      -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PLam ArgInfo
i Abs NLPat
u       -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PPi Dom NLPType
a Abs NLPType
b        -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PSort NLPSort
s        -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PBoundVar Int
i PElims
es -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Subst NLPType where
  type SubstArg NLPType = NLPat
  applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType
applySubst Substitution' (SubstArg NLPType)
rho (NLPType NLPSort
s NLPat
a) = NLPSort -> NLPat -> NLPType
NLPType (Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPType)
rho NLPSort
s) (Substitution' (SubstArg NLPat) -> NLPat -> NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPType)
Substitution' (SubstArg NLPat)
rho NLPat
a)

instance Subst NLPSort where
  type SubstArg NLPSort = NLPat
  applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort
applySubst Substitution' (SubstArg NLPSort)
rho = \case
    PType NLPat
l   -> NLPat -> NLPSort
PType (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg NLPat) -> NLPat -> NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPat)
rho NLPat
l
    PProp NLPat
l   -> NLPat -> NLPSort
PProp (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg NLPat) -> NLPat -> NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPat)
rho NLPat
l
    PSSet NLPat
l   -> NLPat -> NLPSort
PSSet (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg NLPat) -> NLPat -> NLPat
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg NLPSort)
Substitution' (SubstArg NLPat)
rho NLPat
l
    PInf IsFibrant
f Integer
n  -> IsFibrant -> Integer -> NLPSort
PInf IsFibrant
f Integer
n
    NLPSort
PSizeUniv -> NLPSort
PSizeUniv
    NLPSort
PLockUniv -> NLPSort
PLockUniv
    NLPSort
PIntervalUniv -> NLPSort
PIntervalUniv

instance Subst RewriteRule where
  type SubstArg RewriteRule = NLPat
  applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule
applySubst Substitution' (SubstArg RewriteRule)
rho (RewriteRule QName
q Telescope
gamma QName
f PElims
ps Term
rhs Type
t Bool
c) =
    QName
-> Telescope
-> QName
-> PElims
-> Term
-> Type
-> Bool
-> RewriteRule
RewriteRule QName
q (Substitution' NLPat -> Telescope -> Telescope
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' (SubstArg RewriteRule)
Substitution' NLPat
rho Telescope
gamma)
                QName
f (Substitution' (SubstArg PElims) -> PElims -> PElims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' (SubstArg RewriteRule)
Substitution' NLPat
rho) PElims
ps)
                  (Substitution' NLPat -> Term -> Term
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' (SubstArg RewriteRule)
Substitution' NLPat
rho) Term
rhs)
                  (Substitution' NLPat -> Type -> Type
forall a. TermSubst a => Substitution' NLPat -> a -> a
applyNLPatSubst (Int -> Substitution' NLPat -> Substitution' NLPat
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' (SubstArg RewriteRule)
Substitution' NLPat
rho) Type
t)
                  Bool
c
    where n :: Int
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma

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) =
    Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n (Substitution' (SubstArg Elims) -> Elims -> Elims
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' Term
Substitution' (SubstArg DisplayForm)
rho) Elims
ps)
              (Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' Term
Substitution' (SubstArg DisplayForm)
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)        = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
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 DisplayTerm)
rho Term
v
  applySubst Substitution' (SubstArg DisplayTerm)
rho (DDot Term
v)         = Term -> DisplayTerm
DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
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 DisplayTerm)
rho Term
v
  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 [DisplayTerm]
vs Elims
es) = (DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm)
-> (DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp ((DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm)
-> (DisplayTerm, [DisplayTerm], Elims) -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (DisplayTerm, [DisplayTerm], Elims))
-> (DisplayTerm, [DisplayTerm], Elims)
-> (DisplayTerm, [DisplayTerm], Elims)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (DisplayTerm, [DisplayTerm], Elims))
Substitution' (SubstArg DisplayTerm)
rho (DisplayTerm
v, [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) -> (a, Abs (Tele a)) -> Tele a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> Abs (Tele a) -> Tele a
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel ((a, Abs (Tele a)) -> Tele a) -> (a, Abs (Tele a)) -> Tele a
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (a, Abs (Tele a)))
-> (a, Abs (Tele a)) -> (a, Abs (Tele a))
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (a, Abs (Tele a)))
Substitution' (SubstArg (Tele a))
rho (a
t, Abs (Tele a)
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)
    CheckSizeLtSat Term
t         -> Term -> Constraint
CheckSizeLtSat (Term -> Term
forall a. TermSubst a => a -> a
rf Term
t)
    FindInstance MetaId
m Maybe [Candidate]
cands     -> MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m (Maybe [Candidate] -> Maybe [Candidate]
forall a. TermSubst a => a -> a
rf Maybe [Candidate]
cands)
    c :: Constraint
c@UnBlock{}              -> Constraint
c
    c :: Constraint
c@CheckFunDef{}          -> Constraint
c
    HasBiggerSort Sort
s          -> Sort -> Constraint
HasBiggerSort (Sort -> Sort
forall a. TermSubst a => a -> a
rf Sort
s)
    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)
    CheckLockedVars Term
a Type
b Arg Term
c Type
d  -> Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars (Term -> Term
forall a. TermSubst a => a -> a
rf Term
a) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
b) (Arg Term -> Arg Term
forall a. TermSubst a => a -> a
rf Arg Term
c) (Type -> Type
forall a. TermSubst a => a -> a
rf Type
d)
    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)
    UsableAtModality WhyCheckModality
cc Maybe Sort
ms Modality
mod Term
m -> WhyCheckModality -> Maybe Sort -> Modality -> Term -> Constraint
UsableAtModality WhyCheckModality
cc (Maybe Sort -> Maybe Sort
forall a. TermSubst a => a -> a
rf Maybe Sort
ms) Modality
mod (Term -> Term
forall a. TermSubst a => a -> a
rf Term
m)
    where
      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
AsSizes       = CompareAs
AsSizes
  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 (Arg a -> Elim' a) -> Arg a -> Elim' a
forall a b. (a -> b) -> a -> b
$ 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 [Char]
x a
a)   = [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
Abs [Char]
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ 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 [Char]
x a
a) = [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x (a -> Abs a) -> a -> Abs 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 (Abs a))
rho a
a

instance Subst a => Subst (Arg a) where
  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 a
arg = FreeVariables -> Arg a -> Arg a
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables (Arg a -> Arg a) -> Arg a -> Arg a
forall a b. (a -> b) -> a -> b
$ (a -> a) -> Arg a -> Arg a
forall a b. (a -> b) -> Arg a -> Arg 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 (Arg a))
rho) Arg a
arg

instance Subst a => Subst (Named name a) where
  type SubstArg (Named name a) = SubstArg a
  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

  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' a b
dom = FreeVariables -> Dom' a b -> Dom' a b
forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables (Dom' a b -> Dom' a b) -> Dom' a b -> Dom' a b
forall a b. (a -> b) -> a -> b
$
    (b -> b) -> Dom' a b -> Dom' a b
forall a b. (a -> b) -> Dom' a a -> Dom' a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg b)
Substitution' (SubstArg (Dom' a b))
rho) Dom' a b
dom{ domTactic :: Maybe a
domTactic = 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 (Dom' a b -> Maybe a
forall t e. Dom' t e -> Maybe t
domTactic Dom' a b
dom) }

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

instance Subst a => Subst [a] where
  type SubstArg [a] = SubstArg a

instance (Ord k, Subst a) => Subst (Map k a) where
  type SubstArg (Map k 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
  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 Bool
ov) = CandidateKind -> Term -> Type -> Bool -> 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) Bool
ov

instance Subst EqualityView where
  type SubstArg EqualityView = Term
  applySubst :: Substitution' (SubstArg EqualityView)
-> EqualityView -> EqualityView
applySubst Substitution' (SubstArg EqualityView)
rho = \case
    OtherType Type
t          -> Type -> EqualityView
OtherType (Type -> EqualityView) -> Type -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityView)
Substitution' (SubstArg Type)
rho Type
t
    IdiomType Type
t          -> Type -> EqualityView
IdiomType (Type -> EqualityView) -> Type -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityView)
Substitution' (SubstArg Type)
rho Type
t
    EqualityViewType EqualityTypeData
eqt -> EqualityTypeData -> EqualityView
EqualityViewType (EqualityTypeData -> EqualityView)
-> EqualityTypeData -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg EqualityTypeData)
-> EqualityTypeData -> EqualityTypeData
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityTypeData)
Substitution' (SubstArg EqualityView)
rho EqualityTypeData
eqt

instance Subst EqualityTypeData where
  type SubstArg EqualityTypeData = Term
  applySubst :: Substitution' (SubstArg EqualityTypeData)
-> EqualityTypeData -> EqualityTypeData
applySubst Substitution' (SubstArg EqualityTypeData)
rho (EqualityTypeData Sort
s QName
eq Args
l Arg Term
t Arg Term
a Arg Term
b) = Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityTypeData
EqualityTypeData
    (Substitution' (SubstArg Sort) -> Sort -> Sort
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityTypeData)
Substitution' (SubstArg Sort)
rho Sort
s)
    QName
eq
    ((Arg Term -> Arg Term) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho) Args
l)
    (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
t)
    (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
a)
    (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
b)

instance DeBruijn a => DeBruijn (Pattern' a) where
  debruijnNamedVar :: [Char] -> Int -> Pattern' a
debruijnNamedVar [Char]
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
$ [Char] -> Int -> a
forall a. DeBruijn a => [Char] -> Int -> a
debruijnNamedVar [Char]
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 :: PatOrigin
patOrigin = 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__
    (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
$
      [Char] -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> [Char]
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 :: Maybe (Arg Type)
conPType = PatternSubstitution -> Maybe (Arg Type) -> Maybe (Arg Type)
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
Substitution' (SubstArg DeBruijnPattern)
rho (ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
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
    p :: DeBruijnPattern
p@(LitP PatternInfo
_ Literal
_) -> DeBruijnPattern
p
    p :: DeBruijnPattern
p@ProjP{}    -> DeBruijnPattern
p
    IApplyP PatternInfo
i Term
t Term
u DBPatVar
x ->
      case [Char] -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> [Char]
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 :: [Char] -> DeBruijnPattern -> DeBruijnPattern
useName [Char]
n (VarP PatternInfo
o DBPatVar
x)
        | [Char] -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (DBPatVar -> [Char]
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 :: [Char]
dbPatVarName = [Char]
n }
      useName [Char]
_ 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 -> Relevance -> Args -> Term
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply (Projection Maybe QName
prop QName
d Arg QName
r Int
_ ProjLams
lams) ProjOrigin
o Relevance
rel Args
args =
  case [Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char])
forall a. [a] -> Maybe ([a], a)
initLast ([Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char]))
-> [Arg [Char]] -> Maybe ([Arg [Char]], Arg [Char])
forall a b. (a -> b) -> a -> b
$ ProjLams -> [Arg [Char]]
getProjLams ProjLams
lams of
    -- If we have no more abstractions, we must be a record field
    -- (projection applied already to record value).
    Maybe ([Arg [Char]], Arg [Char])
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 [Char]]
pars, Arg ArgInfo
i [Char]
y) ->
      let irr :: Bool
irr = Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
rel
          core :: Term
core
            | Bool
proper Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
irr = ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
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
$ [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
Abs [Char]
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 [Char]]
pars', Args
args') = [Arg [Char]] -> Args -> ([Arg [Char]], Args)
forall a b. [a] -> [b] -> ([a], [b])
dropCommon [Arg [Char]]
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 [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> 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 [Char]
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
. [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x) (Term
core Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
args') [Arg [Char]]
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 -> [Char] -> TelView -> TelView
forall a. Dom a -> [Char] -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> [Char]
forall a. Abs a -> [Char]
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 -> [Char] -> TelV a -> TelV a
absV Dom a
a [Char]
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 ([Char] -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. [Char] -> a -> Abs a
Abs [Char]
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 = (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]
: (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)

bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel :: [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
bindsToTel = (Name -> [Char])
-> [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> [Char]
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 ([Char], Type)]
bindsToTel1 = [Name] -> Dom Type -> [Dom' Term ([Char], Type)]
bindsToTel ([Name] -> Dom Type -> [Dom' Term ([Char], Type)])
-> (List1 Name -> [Name])
-> List1 Name
-> Dom Type
-> [Dom' Term ([Char], 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 =
  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) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ [Char] -> Telescope -> Abs Telescope
forall a. [Char] -> a -> Abs a
Abs (Name -> [Char]
nameToArgName (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x) (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ [NamedArg Name] -> Type -> Telescope
namedBindsToTel [NamedArg Name]
xs (Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
1 Type
t)

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. NamedArg a -> Dom 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 [Char] -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged [Char] -> NamedName) -> Ranged [Char] -> NamedName
forall a b. (a -> b) -> a -> b
$ Range -> [Char] -> Ranged [Char]
forall a. Range -> a -> Ranged a
Ranged (Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x) ([Char] -> Ranged [Char]) -> [Char] -> Ranged [Char]
forall a b. (a -> b) -> a -> b
$ Name -> [Char]
nameToArgName Name
x) Name
x
    forceName Named NamedName Name
x = Named NamedName 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 ([Char], Type) -> Type -> Type
mkPi !Dom' Term ([Char], 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 ([Char] -> Type -> Abs Type
forall a. (Subst a, Free a) => [Char] -> a -> Abs a
mkAbs [Char]
x Type
b)
  where
    x :: [Char]
x = ([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char]) -> ([Char], Type) -> [Char]
forall a b. (a -> b) -> a -> b
$ Dom' Term ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom Dom' Term ([Char], Type)
dom
    a :: Dom Type
a = ([Char], Type) -> Type
forall a b. (a, b) -> b
snd (([Char], Type) -> Type) -> Dom' Term ([Char], Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term ([Char], 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 ([Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
Abs [Char]
x Type
b)

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

lamView :: Term -> ([Arg ArgName], Term)
lamView :: Term -> ([Arg [Char]], Term)
lamView (Lam ArgInfo
h (Abs   [Char]
x Term
b)) = ([Arg [Char]] -> [Arg [Char]])
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (ArgInfo -> [Char] -> Arg [Char]
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h [Char]
x Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
forall a. a -> [a] -> [a]
:) (([Arg [Char]], Term) -> ([Arg [Char]], Term))
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
lamView Term
b
lamView (Lam ArgInfo
h (NoAbs [Char]
x Term
b)) = ([Arg [Char]] -> [Arg [Char]])
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (ArgInfo -> [Char] -> Arg [Char]
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h [Char]
x Arg [Char] -> [Arg [Char]] -> [Arg [Char]]
forall a. a -> [a] -> [a]
:) (([Arg [Char]], Term) -> ([Arg [Char]], Term))
-> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], 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 [Char]] -> Term -> Term
unlamView [Arg [Char]]
xs Term
b = (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> 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 [Char] -> Term -> Term
mkLam Term
b [Arg [Char]]
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 [Char]
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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

-- | 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'.
teleLam :: Telescope -> Term -> Term
teleLam :: Telescope -> Term -> Term
teleLam  Telescope
EmptyTel         Term
t = Term
t
teleLam (ExtendTel Dom Type
u Abs Telescope
tel) Term
t = 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
$ (Telescope -> Term -> Term) -> Term -> Telescope -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope -> Term -> Term
teleLam Term
t (Telescope -> Term) -> Abs Telescope -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Telescope
tel

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

instance TeleNoAbs ListTel where
  teleNoAbs :: [Dom' Term ([Char], Type)] -> Term -> Term
teleNoAbs [Dom' Term ([Char], Type)]
tel Term
t = (Dom' Term ([Char], Type) -> Term -> Term)
-> Term -> [Dom' Term ([Char], 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{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = ([Char]
x, Type
_)} -> 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
. [Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs [Char]
x) Term
t [Dom' Term ([Char], Type)]
tel

instance TeleNoAbs Telescope where
  teleNoAbs :: Telescope -> Term -> Term
teleNoAbs Telescope
tel = [Dom' Term ([Char], Type)] -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs ([Dom' Term ([Char], Type)] -> Term -> Term)
-> [Dom' Term ([Char], Type)] -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], 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 (Subst a, Eq a)  => Eq  (Tele a)
deriving instance (Subst a, Ord a) => Ord (Tele a)

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

-- Andreas, 2017-10-04, issue #2775, ignore irrelevant arguments during with-abstraction.
--
-- For reasons beyond my comprehension, the following Eq instances are not employed
-- by with-abstraction in TypeChecking.Abstract.isPrefixOf.
-- Instead, I modified the general Eq instance for Arg to ignore the argument
-- if irrelevant.

-- -- | Ignore irrelevant arguments in equality check.
-- --   Also ignore origin.
-- instance {-# OVERLAPPING #-} Eq (Arg Term) where
--   a@(Arg (ArgInfo h r _o) t) == a'@(Arg (ArgInfo h' r' _o') t') = trace ("Eq (Arg Term) on " ++ show a ++ " and " ++ show a') $
--     h == h' && ((r == Irrelevant) || (r' == Irrelevant) || (t == t'))
--     -- Andreas, 2017-10-04: According to Syntax.Common, equality on Arg ignores Relevance and Origin.

-- instance {-# OVERLAPPING #-} Eq Args where
--   us == vs = length us == length vs && and (zipWith (==) us vs)

-- instance {-# OVERLAPPING #-} Eq Elims where
--   us == vs = length us == length vs && and (zipWith (==) us vs)

-- | 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 [Char]
_ a
a == :: Abs a -> Abs a -> Bool
== NoAbs [Char]
_ 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 [Char]
_ a
a compare :: Abs a -> Abs a -> Ordering
`compare` NoAbs [Char]
_ 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 (Subst a, 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 (Subst a, 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


---------------------------------------------------------------------------
-- * 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' (Type 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
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' (Prop 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
$ Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' (Inf IsFibrant
f 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f (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' (SSet 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
$ Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l
univSort' Sort
SizeUniv     = 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0
univSort' Sort
LockUniv     = 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0 -- lock polymorphism is not actually supported
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' (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 (Set l, Prop l, Size, ...)  or large
--   (Setω n).
data SizeOfSort
  = SmallSort IsFibrant
  | LargeSort IsFibrant Integer

-- | 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 Type{}       = 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
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Prop{}       = 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
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Sort
SizeUniv     = 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
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Sort
LockUniv     = 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
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort 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
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsStrict
sizeOfSort (Inf IsFibrant
f 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
$ IsFibrant -> Integer -> SizeOfSort
LargeSort IsFibrant
f Integer
n
sizeOfSort SSet{}       = 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
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsStrict
sizeOfSort (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
sizeOfSort FunSort{}    = Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort PiSort{}     = Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort UnivSort{}   = Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort DefS{}       = Blocker -> Either Blocker SizeOfSort
forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort 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

fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant
fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
IsStrict IsFibrant
a = IsFibrant
IsStrict
fibrantLub IsFibrant
a IsFibrant
IsStrict = IsFibrant
IsStrict
fibrantLub IsFibrant
a IsFibrant
b = IsFibrant
a

-- | Compute the sort of a function type from the sorts of its
--   domain and codomain.
funSort' :: Sort -> Sort -> Either Blocker Sort
funSort' :: Sort -> Sort -> Either Blocker Sort
funSort' Sort
a Sort
b = case (Sort
a, Sort
b) of
  (Type Level
a        , Type 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
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Prop Level
a        , Type 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
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Type Level
a        , Prop 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
Prop (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Prop Level
a        , Prop 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
Prop (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (SSet Level
a        , SSet 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 -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Type Level
a        , SSet 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 -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (SSet Level
a        , Type 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 -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (SSet Level
a        , Prop 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 -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Prop Level
a        , SSet 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 -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Inf IsFibrant
af Integer
m      , Sort
b            ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
b Either Blocker SizeOfSort
-> (SizeOfSort -> Either Blocker Sort) -> Either Blocker Sort
forall a b.
Either Blocker a -> (a -> Either Blocker b) -> Either Blocker b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SmallSort IsFibrant
bf   -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) Integer
m
    LargeSort IsFibrant
bf 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n
  (Sort
a             , Inf IsFibrant
bf Integer
n     ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
a Either Blocker SizeOfSort
-> (SizeOfSort -> Either Blocker Sort) -> Either Blocker Sort
forall a b.
Either Blocker a -> (a -> Either Blocker b) -> Either Blocker b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SmallSort IsFibrant
af   -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) Integer
n
    LargeSort IsFibrant
af Integer
m -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n
  (Sort
LockUniv      , Sort
b            ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right Sort
b
  -- No functions into lock types
  (Sort
a             , Sort
LockUniv     ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  -- @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  , SSet 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 -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level
b
  (Sort
IntervalUniv  , Type 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
Type (Level -> Sort) -> Level -> Sort
forall a b. (a -> b) -> a -> b
$ Level
b
  (Sort
IntervalUniv  , Sort
_            ) -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Type 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
  (SSet 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
SizeUniv      , Sort
b            ) -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right Sort
b
  (Sort
a             , Sort
SizeUniv     ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
a Either Blocker SizeOfSort
-> (SizeOfSort -> Either Blocker Sort) -> Either Blocker Sort
forall a b.
Either Blocker a -> (a -> Either Blocker b) -> Either Blocker b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SmallSort{} -> Sort -> Either Blocker Sort
forall a b. b -> Either a b
Right Sort
forall t. Sort' t
SizeUniv
    LargeSort{} -> Blocker -> Either Blocker Sort
forall a b. a -> Either a b
Left Blocker
neverUnblock
  (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

funSort :: Sort -> Sort -> Sort
funSort :: Sort -> Sort -> Sort
funSort 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
$ Sort -> Sort -> Either Blocker Sort
funSort' Sort
a Sort
b

-- | Compute the sort of a pi type from the sorts of its domain
--   and codomain.
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 [Char]
_ 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   [Char]
_ 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  -> case (Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s1 , Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s2) of
    (Right (SmallSort IsFibrant
f1) , Right (SmallSort IsFibrant
f2)) -> case FlexRig
o of
      FlexRig
StronglyRigid -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
0
      FlexRig
Unguarded     -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
0
      FlexRig
WeaklyRigid   -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
0
      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 IsFibrant
f1 Integer
n) , Right (SmallSort IsFibrant
f2)) -> 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
$ IsFibrant -> Integer -> Sort
forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
n
    (Either Blocker SizeOfSort
_                     , Right LargeSort{}    ) -> Either Blocker Sort
forall a. HasCallStack => a
__IMPOSSIBLE__ -- large sorts cannot depend on variables
    (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

-- Andreas, 2019-06-20
-- KEEP the following commented out code for the sake of the discussion on irrelevance.
-- piSort' a bAbs@(Abs   _ b) = case occurrence 0 b of
--     -- Andreas, Jesper, AIM XXIX, 2019-03-18, issue #3631
--     -- Remember the NoAbs here!
--     NoOccurrence  -> Just $ funSort a $ noabsApp __IMPOSSIBLE__ bAbs
--     -- Andreas, 2017-01-18, issue #2408:
--     -- The sort of @.(a : A) → Set (f a)@ in context @f : .A → Level@
--     -- is @dLub Set λ a → Set (lsuc (f a))@, but @DLub@s are not serialized.
--     -- Alternatives:
--     -- 1. -- Irrelevantly -> sLub s1 (absApp b $ DontCare $ Sort Prop)
--     --    We cheat here by simplifying the sort to @Set (lsuc (f *))@
--     --    where * is a dummy value.  The rationale is that @f * = f a@ (irrelevance!)
--     --    and that if we already have a neutral level @f a@
--     --    it should not hurt to have @f *@ even if type @A@ is empty.
--     --    However: sorts are printed in error messages when sorts do not match.
--     --    Also, sorts with a dummy like Prop would be ill-typed.
--     -- 2. We keep the DLub, and serialize it.
--     --    That's clean and principled, even though DLubs make level solving harder.
--     -- Jesper, 2018-04-20: another alternative:
--     -- 3. Return @Inf@ as in the relevant case. This is conservative and might result
--     --    in more occurrences of @Setω@ than desired, but at least it doesn't pollute
--     --    the sort system with new 'exotic' sorts.
--     Irrelevantly  -> Just Inf
--     StronglyRigid -> Just Inf
--     Unguarded     -> Just Inf
--     WeaklyRigid   -> Just Inf
--     Flexible _    -> Nothing

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

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