{-# LANGUAGE BangPatterns       #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# 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 (second)
import Control.Monad (guard)
import Data.Coerce
import Data.Function
import qualified Data.List as List
import Data.Map (Map)
import Data.Maybe
import Data.HashMap.Strict (HashMap)

import Debug.Trace (trace)
import Language.Haskell.TH.Syntax (thenCmp) -- lexicographic combination of Ordering

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.Empty
import Agda.Utils.Functor
import Agda.Utils.List
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, Subst t t)
           => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE :: (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
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$
    case t -> Term
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 -> (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
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 -> t -> t
forall t a. Subst t a => Abs a -> t -> a
lazyAbsApp (Abs Term -> Abs t
coerce Abs Term
b :: Abs t) (Term -> t
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) t -> Elims -> Term
forall x. Coercible t x => x -> Elims -> Term
`app` Elims
es0
          IApply Term
_ Term
_ Term
a : Elims
es0 -> Abs t -> t -> t
forall t a. Subst t a => Abs a -> t -> a
lazyAbsApp (Abs Term -> Abs t
coerce Abs Term
b :: Abs t) (Term -> t
coerce Term
a)         t -> Elims -> Term
forall x. Coercible t x => x -> 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 String
s Elims
es' -> String -> Elims -> Term
Dummy String
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 x. Coercible t x => x -> Elims -> Term
`app` Elims
es  -- Andreas, 2011-10-02
        -- need to go under DontCare, since "with" might resurrect irrelevant term
   where
     app :: Coercible t x => x -> Elims -> Term
     app :: x -> Elims -> Term
app x
t Elims
es = t -> Term
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ (x -> t
coerce x
t :: 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
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, Subst t 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, Subst t t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE (\ Empty
_ Term
t Elims
es ->  String -> Elims -> Term
Dummy String
"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 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
    (Con (ConHead QName
_ 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 :: (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp Empty -> Term -> Elims -> Term
fk ConHead
ch                  ConInfo
ci Elims
args []             = ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args
conApp Empty -> Term -> Elims -> Term
fk ConHead
ch                  ConInfo
ci Elims
args (a :: Elim' Term
a@Apply{} : Elims
es) = (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
fk ConHead
ch ConInfo
ci (Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim' Term
a]) Elims
es
conApp Empty -> Term -> Elims -> Term
fk ConHead
ch                  ConInfo
ci Elims
args (a :: Elim' Term
a@IApply{} : Elims
es) = (Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
forall t.
(Coercible t Term, Apply t) =>
(Empty -> Term -> Elims -> Term)
-> ConHead -> ConInfo -> Elims -> Elims -> Term
conApp @t Empty -> Term -> Elims -> Term
fk ConHead
ch ConInfo
ci (Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Elim' Term
a]) Elims
es
conApp Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch@(ConHead QName
c Induction
_ [Arg QName]
fs) ConInfo
ci Elims
args ees :: Elims
ees@(Proj ProjOrigin
o QName
f : Elims
es) =
  let failure :: c -> c
failure c
err = (String -> c -> c) -> c -> String -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> c -> c
forall a. String -> a -> a
trace c
err (String -> c) -> String -> c
forall a b. (a -> b) -> a -> b
$
        String
"conApp: constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
c String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
" with fields\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Arg QName -> String) -> [Arg QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Arg QName -> String) -> Arg QName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> String
forall a. Show a => a -> String
show) [Arg QName]
fs) String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
" and args\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Elim' Term -> String) -> Elims -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> (Elim' Term -> String) -> Elim' Term -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' Term -> String
forall a. Pretty a => a -> String
prettyShow) Elims
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
" projected by " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show 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 c. c -> c
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
fk 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
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
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 c. c -> c
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 c. c -> c
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 :: 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 Subst Term 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) -> Term -> Tele a
forall t a. Subst t a => Abs a -> t -> 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 Defn
d) Args
args =
    ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> 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 (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 (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 :: QName
-> Telescope -> QName -> PElims -> Term -> Type -> RewriteRule
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' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
sub (RewriteRule -> PElims
rewPats RewriteRule
r)
       , rewRHS :: Term
rewRHS     = Substitution' NLPat -> Term -> Term
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (RewriteRule -> Term
rewRHS RewriteRule
r)
       , rewType :: Type
rewType    = Substitution' NLPat -> Type -> Type
forall a. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst Substitution' NLPat
sub (RewriteRule -> Type
rewType 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 (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 (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 (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 a x.
(Eq a, Num a) =>
a -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [NamedArg (Pattern' a)]
ps
    where
    loop :: a -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop a
0 [NamedArg (Pattern' x)]
ps = [NamedArg (Pattern' x)]
ps
    loop a
n [] = [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    loop a
n (NamedArg (Pattern' x)
p : [NamedArg (Pattern' x)]
ps) =
      let recurse :: [NamedArg (Pattern' x)]
recurse = a -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
loop (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
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 String]
lams) Args
args = [Arg String] -> ProjLams
ProjLams ([Arg String] -> ProjLams) -> [Arg String] -> ProjLams
forall a b. (a -> b) -> a -> b
$ Int -> [Arg String] -> [Arg String]
forall a. Int -> [a] -> [a]
List.drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) [Arg String]
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 = 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 (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 -> Maybe Projection
funProjection = Maybe Projection
Nothing } ->
      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 -> Maybe Projection
funProjection = Just 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 :: Maybe Projection
funProjection = Maybe 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 :: Maybe Projection
funProjection = Projection -> Maybe Projection
forall a. a -> Maybe a
Just 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 :: Maybe Projection
funProjection     = if Bool
isVar0 then Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
p{ projIndex :: Int
projIndex = Int
0 } else Maybe Projection
forall a. Maybe a
Nothing
                , 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  = Args -> Arg Term
forall a. [a] -> a
last Args
args -- 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
{-
    Function{ funClauses = cs, funCompiled = cc, funInv = inv
            , funProjection = Just p@Projection{ projIndex = n } }
        -- case: only applying parameters
      | size args < n -> d { funProjection = Just $ p `apply` args }
        -- case: apply also to record value
      | otherwise     ->
        d { funClauses        = apply cs args'
          , funCompiled       = apply cc args'
          , funInv            = apply inv args'
          , funProjection     = Just $ p { projIndex = 0 } -- Nothing ?
          }
      where args' = [last args]  -- the record value
-}
    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 }

  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 NAPs
ps Maybe Term
b Maybe (Arg Type)
t Bool
catchall Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell) Args
args
      | Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> NAPs -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
ps = Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
      | Bool
otherwise =
      Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause Range
rl Range
rf
             Telescope
tel'
             (Substitution' DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rhoP (NAPs -> NAPs) -> NAPs -> NAPs
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) NAPs
ps)
             (Substitution' Term -> Maybe Term -> Maybe Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Maybe Term
b)
             (Substitution' Term -> Maybe (Arg Type) -> Maybe (Arg Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Maybe (Arg Type)
t)
             Bool
catchall
             Maybe Bool
recursive
             Maybe Bool
unreachable
             ExpandedEllipsis
ell
      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 :: NAPs
rps   = NAPs -> NAPs
forall a. [a] -> [a]
reverse (NAPs -> NAPs) -> NAPs -> NAPs
forall a b. (a -> b) -> a -> b
$ Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
take (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) NAPs
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 -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel NAPs
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 :: Substitution' DeBruijnPattern
rhoP = (Term -> DeBruijnPattern)
-> Int -> NAPs -> [Term] -> Substitution' DeBruijnPattern
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> DeBruijnPattern
forall a. Term -> Pattern' a
dotP Int
n NAPs
rps [Term]
rargs
        rho :: Substitution' Term
rho  = (Term -> Term) -> Int -> NAPs -> [Term] -> Substitution' Term
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> Term
forall c. c -> c
id   Int
n NAPs
rps [Term]
rargs

        substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
        substP :: Int -> Term -> NAPs -> NAPs
substP Int
i Term
v = Int -> DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Int -> t -> 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 :: Subst a a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a
        mkSub :: (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
_ Int
_ [] [] = Substitution' a
forall a. Substitution' a
idS
        mkSub Term -> a
tm Int
n (NamedArg DeBruijnPattern
p : NAPs
ps) (Term
v : [Term]
vs) =
          case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
            VarP PatternInfo
_ (DBPatVar String
_ Int
i) -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Term -> NAPs -> NAPs
substP Int
i Term
v' NAPs
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a 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 t a. Subst t 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 -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n NAPs
ps [Term]
vs
            ConP ConHead
c ConPatternInfo
_ NAPs
ps' -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs)
            DefP PatternInfo
o QName
q NAPs
ps' -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm Int
n (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) [Term]
vs
            LitP{}  -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
            ProjP{} -> Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
            IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar String
_ Int
i) -> (Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
forall a.
Subst a a =>
(Term -> a) -> Int -> NAPs -> [Term] -> Substitution' a
mkSub Term -> a
tm (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Term -> NAPs -> NAPs
substP Int
i Term
v' NAPs
ps) [Term]
vs Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a 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 t a. Subst t 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
_ NAPs
_ [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 -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel [] [] = Telescope
tel
        newTel Int
n Telescope
tel (NamedArg DeBruijnPattern
p : NAPs
ps) (Term
v : [Term]
vs) =
          case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
            VarP PatternInfo
_ (DBPatVar String
_ Int
i) -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Term -> Telescope -> Telescope
forall t t a t.
(Eq t, Num t, Subst t a, Subst t t) =>
t -> t -> 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
v Telescope
tel) (Int -> Term -> NAPs -> NAPs
substP Int
i (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v) NAPs
ps) [Term]
vs
            DotP{}              -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel NAPs
ps [Term]
vs
            ConP ConHead
c ConPatternInfo
_ NAPs
ps'        -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) (ConHead -> Term -> [Term]
projections ConHead
c Term
v [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
vs)
            DefP PatternInfo
_ QName
q NAPs
ps'        -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel (NAPs
ps' NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps) [Term]
vs
            LitP{}              -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
            ProjP{}             -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
            IApplyP PatternInfo
_ Term
_ Term
_ (DBPatVar String
_ Int
i) -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Term -> Telescope -> Telescope
forall t t a t.
(Eq t, Num t, Subst t a, Subst t t) =>
t -> t -> 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
v Telescope
tel) (Int -> Term -> NAPs -> NAPs
substP Int
i (Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
v) NAPs
ps) [Term]
vs
        newTel Int
_ Telescope
tel NAPs
_ [Term]
_ = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__

        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
$ 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 -> t -> Tele a -> Tele a
subTel t
i t
v Tele a
EmptyTel = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
        subTel t
0 t
v (ExtendTel a
_ Abs (Tele a)
tel) = Abs (Tele a) -> t -> Tele a
forall t a. Subst t a => Abs a -> t -> a
absApp Abs (Tele a)
tel t
v
        subTel t
i t
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 -> t -> Tele a -> Tele a
subTel (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Int -> t -> t
forall t a. Subst t a => Int -> a -> a
raise Int
1 t
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
    CompiledClauses
Fail     -> CompiledClauses
forall a. CompiledClauses' a
Fail
    Done [Arg String]
hs Term
t
      | [Arg String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg String]
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 String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg String]
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 String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
Done (Int -> [Arg String] -> [Arg String]
forall a. Int -> [a] -> [a]
List.drop Int
len [Arg String]
hs) (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' 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 (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 Maybe System
sys) Args
args = ModuleName -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
m (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 c. c -> c
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' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
sigma
      nargs :: Int
nargs = Args -> 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 -> Term -> Type
forall t a. Subst t a => Abs a -> t -> 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                    =
  String -> Type -> Type
forall a. String -> a -> a
trace (String
"piApply t = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  args = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Args -> String
forall a. Show a => a -> String
show 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 Defn
d) =
    ArgInfo
-> QName
-> Type
-> [Polarity]
-> [Occurrence]
-> NumGeneralizableArgs
-> [Maybe Name]
-> [LocalDisplayForm]
-> MutualId
-> CompiledRepresentation
-> Maybe QName
-> Bool
-> Set QName
-> Bool
-> Bool
-> Bool
-> Blocked_
-> 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 (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) =
    QName
-> Telescope -> QName -> PElims -> Term -> Type -> 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

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 String]
lams) = [Arg String] -> ProjLams
ProjLams ([Arg String] -> ProjLams) -> [Arg String] -> ProjLams
forall a b. (a -> b) -> a -> b
$
    (Dom' Term (String, Type) -> Arg String)
-> [Dom' Term (String, Type)] -> [Arg String]
forall a b. (a -> b) -> [a] -> [b]
map (\ !Dom' Term (String, Type)
dom -> Dom' Term String -> Arg String
forall t a. Dom' t a -> Arg a
argFromDom ((String, Type) -> String
forall a b. (a, b) -> a
fst ((String, Type) -> String)
-> Dom' Term (String, Type) -> Dom' Term String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
dom)) (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel) [Arg String] -> [Arg String] -> [Arg String]
forall a. [a] -> [a] -> [a]
++ [Arg String]
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 -> Maybe Projection
funProjection = Maybe Projection
Nothing  } ->
      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 -> Maybe Projection
funProjection = Just 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' else
        Defn
d' { funClauses :: [Clause]
funClauses  = Telescope -> [Clause] -> [Clause]
forall t. Abstract t => Telescope -> t -> t
abstract 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
          d' :: Defn
d' = Defn
d { funProjection :: Maybe Projection
funProjection = Projection -> Maybe Projection
forall a. a -> Maybe a
Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
forall a b. (a -> b) -> a -> b
$ Telescope -> Projection -> Projection
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Projection
p }
          tel1 :: Telescope
tel1 = [Dom' Term (String, Type)] -> Telescope
telFromList ([Dom' Term (String, Type)] -> Telescope)
-> [Dom' Term (String, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, 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 (String, Type)] -> [Dom' Term (String, Type)])
-> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel

    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 }

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' NAPs
ps Maybe Term
b Maybe (Arg Type)
t Bool
catchall Maybe Bool
recursive Maybe Bool
unreachable ExpandedEllipsis
ell) =
    Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause Range
rl Range
rf (Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
tel')
           (Int -> Telescope -> NAPs
namedTelVars Int
m Telescope
tel NAPs -> NAPs -> NAPs
forall a. [a] -> [a] -> [a]
++ NAPs
ps)
           Maybe Term
b
           Maybe (Arg Type)
t -- nothing to do for t, since it lives under the telescope
           Bool
catchall
           Maybe Bool
recursive
           Maybe Bool
unreachable
           ExpandedEllipsis
ell
      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
Fail = CompiledClauses
forall a. CompiledClauses' a
Fail
  abstract Telescope
tel (Done [Arg String]
xs Term
t) = [Arg String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
Done ((Dom' Term (String, Type) -> Arg String)
-> [Dom' Term (String, Type)] -> [Arg String]
forall a b. (a -> b) -> [a] -> [b]
map (Dom' Term String -> Arg String
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term String -> Arg String)
-> (Dom' Term (String, Type) -> Dom' Term String)
-> Dom' Term (String, Type)
-> Arg String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Type) -> String)
-> Dom' Term (String, Type) -> Dom' Term String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, Type) -> String
forall a b. (a, b) -> a
fst) (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel) [Arg String] -> [Arg String] -> [Arg String]
forall a. [a] -> [a] -> [a]
++ [Arg String]
xs) Term
t
  abstract Telescope
tel (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)

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 (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)
-> NAPs -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
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) (NAPs -> [Arg DeBruijnPattern])
-> (Telescope -> NAPs) -> Telescope -> [Arg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Telescope -> NAPs
namedTelVars Int
m)

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
namedTelVars :: Int -> Telescope -> NAPs
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 -> String -> Named NamedName DeBruijnPattern
namedDBVarP (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (String -> Named NamedName DeBruijnPattern)
-> String -> Named NamedName DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Abs Telescope -> String
forall a. Abs a -> String
absName Abs Telescope
tel) NamedArg DeBruijnPattern -> NAPs -> NAPs
forall a. a -> [a] -> [a]
:
  Int -> Telescope -> NAPs
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 (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 (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 (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 :: 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 String -> Telescope -> Telescope)
-> Telescope -> [Arg String] -> Telescope
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\arg :: Arg String
arg@(Arg ArgInfo
info String
x) -> Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
HasCallStack => Type
__DUMMY_TYPE__ Type -> Dom' Term String -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg String -> Dom' Term String
forall a. Arg a -> Dom a
domFromArg Arg String
arg) (Abs Telescope -> Telescope)
-> (Telescope -> Abs Telescope) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs String
x)
                      Telescope
forall a. Tele a
EmptyTel
              ([Arg String] -> Telescope) -> [Arg String] -> Telescope
forall a b. (a -> b) -> a -> b
$ (String -> Arg Term -> Arg String)
-> [String] -> Args -> [Arg String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> Arg Term -> Arg String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) [String]
names Args
args
        names :: [String]
names = [String] -> [String]
forall a. [a] -> [a]
cycle ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
stringToArgName (String -> String) -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String -> String
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 => Empty -> Permutation -> Substitution' a
renaming :: Empty -> Permutation -> Substitution' a
renaming Empty
err Permutation
p = Empty -> [Maybe a] -> Substitution' a -> Substitution' a
forall a.
DeBruijn a =>
Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Empty
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 :: Permutation -> Substitution' a
renamingR p :: Permutation
p@(Perm Int
n [Int]
_) = Permutation -> [a] -> [a]
forall a. Permutation -> [a] -> [a]
permute (Permutation -> Permutation
reverseP Permutation
p) ((Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar [Int
0..]) [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

-- | The permutation should permute the corresponding context. (right-to-left list)
renameP :: Subst t a => Empty -> Permutation -> a -> a
renameP :: Empty -> Permutation -> a -> a
renameP Empty
err Permutation
p = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Empty -> Permutation -> Substitution' t
forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming Empty
err Permutation
p)

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

{-# SPECIALIZE applySubstTerm :: Substitution -> Term -> Term #-}
{-# SPECIALIZE applySubstTerm :: Substitution' BraveTerm -> BraveTerm -> BraveTerm #-}
applySubstTerm :: forall t. (Coercible t Term, Subst t t, Apply t) => Substitution' t -> t -> t
applySubstTerm :: Substitution' t -> t -> t
applySubstTerm Substitution' t
IdS t
t = t
t
applySubstTerm Substitution' t
rho t
t    = Term -> t
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$ case t -> Term
coerce t
t of
    Var Int
i Elims
es    -> t -> Term
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' t -> Int -> t
forall a. Subst a 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
$ Abs Term -> Abs Term
forall a b. (Coercible b a, Subst 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
$ Level -> Level
forall a b. (Coercible b a, Subst 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
$ Sort -> Sort
forall a b. (Coercible b a, Subst 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
$ Term -> Term
forall a b. (Coercible b a, Subst t a) => b -> b
sub @t Term
mv
    Dummy String
s Elims
es  -> String -> Elims -> Term
Dummy String
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, Subst t a) => b -> b
   sub :: b -> b
sub b
t = a -> b
coerce (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (b -> a
coerce b
t :: a)
   subE :: Elims -> Elims
   subE :: Elims -> Elims
subE  = forall b. (Coercible b [Elim' t], Subst t [Elim' t]) => b -> b
forall a b. (Coercible b a, Subst 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 b.
(Coercible b (Dom' t (Type'' t t), Abs (Type'' t t)),
 Subst t (Dom' t (Type'' t t), Abs (Type'' t t))) =>
b -> b
forall a b. (Coercible b a, Subst t a) => b -> b
sub @(Dom' t (Type'' t t), Abs (Type'' t t))

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

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

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

instance (Coercible a Term, Subst t a) => Subst t (Sort' a) where
  applySubst :: Substitution' t -> Sort' a -> Sort' a
applySubst Substitution' t
rho Sort' a
s = case Sort' a
s of
    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 a. Subst t a => a -> a
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 a. Subst t a => a -> a
sub Level' a
n
    Sort' a
Inf        -> Sort' a
forall t. Sort' t
Inf
    Sort' a
SizeUniv   -> Sort' a
forall t. Sort' t
SizeUniv
    PiSort Dom' a (Type'' a a)
a Abs (Sort' a)
s2 -> Sort -> Sort' a
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
piSort (Dom' a (Type'' a a) -> Dom Type
coerce (Dom' a (Type'' a a) -> Dom Type)
-> Dom' a (Type'' a a) -> Dom Type
forall a b. (a -> b) -> a -> b
$ Dom' a (Type'' a a) -> Dom' a (Type'' a a)
forall a. Subst t a => a -> a
sub Dom' a (Type'' a a)
a) (Abs (Sort' a) -> Abs Sort
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 a. Subst t a => a -> a
sub Abs (Sort' a)
s2)
    FunSort Sort' a
s1 Sort' a
s2 -> Sort -> Sort' a
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (Sort' a -> Sort
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s1) (Sort' a -> Sort
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s2)
    UnivSort Sort' a
s -> Sort -> Sort' a
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Maybe Sort -> Sort -> Sort
univSort Maybe Sort
forall a. Maybe a
Nothing (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
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 a. Subst t a => a -> a
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 a. Subst t a => a -> a
sub [Elim' a]
es
    DummyS{}   -> Sort' a
s
    where sub :: a -> a
sub a
x = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x

instance Subst t a => Subst t (Level' a) where
  applySubst :: Substitution' t -> Level' a -> Level' a
applySubst Substitution' t
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' t -> [PlusLevel' a] -> [PlusLevel' a]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho [PlusLevel' a]
as

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

instance Subst t a => Subst t (LevelAtom' a) where
  applySubst :: Substitution' t -> LevelAtom' a -> LevelAtom' a
applySubst Substitution' t
rho (MetaLevel MetaId
m [Elim' a]
vs)   = MetaId -> [Elim' a] -> LevelAtom' a
forall t. MetaId -> [Elim' t] -> LevelAtom' t
MetaLevel MetaId
m    ([Elim' a] -> LevelAtom' a) -> [Elim' a] -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> [Elim' a] -> [Elim' a]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho [Elim' a]
vs
  applySubst Substitution' t
rho (BlockedLevel MetaId
m a
v) = MetaId -> a -> LevelAtom' a
forall t. MetaId -> t -> LevelAtom' t
BlockedLevel MetaId
m (a -> LevelAtom' a) -> a -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
v
  applySubst Substitution' t
rho (NeutralLevel NotBlocked
_ a
v) = a -> LevelAtom' a
forall t. t -> LevelAtom' t
UnreducedLevel (a -> LevelAtom' a) -> a -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
v
  applySubst Substitution' t
rho (UnreducedLevel a
v) = a -> LevelAtom' a
forall t. t -> LevelAtom' t
UnreducedLevel (a -> LevelAtom' a) -> a -> LevelAtom' a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
v

instance Subst Term Name where
  applySubst :: Substitution' Term -> Name -> Name
applySubst Substitution' Term
rho = Name -> Name
forall c. c -> c
id

instance {-# OVERLAPPING #-} Subst Term String where
  applySubst :: Substitution' Term -> String -> String
applySubst Substitution' Term
rho = String -> String
forall c. c -> c
id

instance Subst Term ConPatternInfo where
  applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo
applySubst Substitution' Term
rho ConPatternInfo
i = ConPatternInfo
i{ conPType :: Maybe (Arg Type)
conPType = Substitution' Term -> Maybe (Arg Type) -> Maybe (Arg Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
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 Term Pattern where
  applySubst :: Substitution' Term -> Pattern -> Pattern
applySubst Substitution' Term
rho Pattern
p = case Pattern
p of
    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' Term -> ConPatternInfo -> ConPatternInfo
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho ConPatternInfo
mt) ([NamedArg Pattern] -> Pattern) -> [NamedArg Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> [NamedArg Pattern] -> [NamedArg Pattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
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' Term -> [NamedArg Pattern] -> [NamedArg Pattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
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' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
t
    VarP PatternInfo
o String
s     -> Pattern
p
    LitP PatternInfo
o Literal
l     -> Pattern
p
    ProjP{}      -> Pattern
p
    IApplyP PatternInfo
o Term
t Term
u String
x -> PatternInfo -> Term -> Term -> String -> Pattern
forall x. PatternInfo -> Term -> Term -> x -> Pattern' x
IApplyP PatternInfo
o (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
t) (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
u) String
x

instance Subst Term A.ProblemEq where
  applySubst :: Substitution' Term -> ProblemEq -> ProblemEq
applySubst Substitution' Term
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' Term -> (Term, Dom Type) -> (Term, Dom Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
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 NLPat
p = case NLPat
p of
    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 :: (Subst Term a) => Substitution' NLPat -> a -> a
applyNLPatSubst :: Substitution' NLPat -> a -> a
applyNLPatSubst = Substitution' Term -> a -> a
forall t a. Subst t a => Substitution' t -> 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NLPat -> Term
nlPatToTerm
  where
    nlPatToTerm :: NLPat -> Term
    nlPatToTerm :: NLPat -> Term
nlPatToTerm NLPat
p = case NLPat
p of
      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 (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 :: Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom :: Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' NLPat
rho Dom a
dom = Substitution' NLPat -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst 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. Subst Term 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 NLPat where
  applySubst :: Substitution' NLPat -> NLPat -> NLPat
applySubst Substitution' NLPat
rho NLPat
p = case NLPat
p of
    PVar Int
i [Arg Int]
bvs -> Substitution' NLPat -> Int -> NLPat
forall a. Subst a a => Substitution' a -> Int -> a
lookupS 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' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' 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' NLPat -> Abs NLPat -> Abs NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' 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. Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyNLSubstToDom Substitution' NLPat
rho Dom NLPType
a) (Substitution' NLPat -> Abs NLPType -> Abs NLPType
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho Abs NLPType
b)
    PSort NLPSort
s -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> NLPSort -> NLPat
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> NLPSort -> NLPSort
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' 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' NLPat -> PElims -> PElims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' 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. Subst Term a => Substitution' NLPat -> a -> a
applyNLPatSubst 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 (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 NLPat NLPType where
  applySubst :: Substitution' NLPat -> NLPType -> NLPType
applySubst Substitution' NLPat
rho (NLPType NLPSort
s NLPat
a) = NLPSort -> NLPat -> NLPType
NLPType (Substitution' NLPat -> NLPSort -> NLPSort
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPSort
s) (Substitution' NLPat -> NLPat -> NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPat
a)

instance Subst NLPat NLPSort where
  applySubst :: Substitution' NLPat -> NLPSort -> NLPSort
applySubst Substitution' NLPat
rho = \case
    PType NLPat
l   -> NLPat -> NLPSort
PType (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> NLPat -> NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPat
l
    PProp NLPat
l   -> NLPat -> NLPSort
PProp (NLPat -> NLPSort) -> NLPat -> NLPSort
forall a b. (a -> b) -> a -> b
$ Substitution' NLPat -> NLPat -> NLPat
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' NLPat
rho NLPat
l
    NLPSort
PInf      -> NLPSort
PInf
    NLPSort
PSizeUniv -> NLPSort
PSizeUniv

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

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

instance Subst Term DisplayForm where
  applySubst :: Substitution' Term -> DisplayForm -> DisplayForm
applySubst Substitution' Term
rho (Display Int
n Elims
ps DisplayTerm
v) =
    Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
n (Substitution' Term -> Elims -> Elims
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' Term
rho) Elims
ps)
              (Substitution' Term -> DisplayTerm -> DisplayTerm
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n Substitution' Term
rho) DisplayTerm
v)

instance Subst Term DisplayTerm where
  applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm
applySubst Substitution' Term
rho (DTerm Term
v)        = Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
v
  applySubst Substitution' Term
rho (DDot Term
v)         = Term -> DisplayTerm
DDot  (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
v
  applySubst Substitution' Term
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' Term -> [Arg DisplayTerm] -> [Arg DisplayTerm]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [Arg DisplayTerm]
vs
  applySubst Substitution' Term
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' Term -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho [Elim' DisplayTerm]
es
  applySubst Substitution' Term
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' Term
-> (DisplayTerm, [DisplayTerm], Elims)
-> (DisplayTerm, [DisplayTerm], Elims)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho (DisplayTerm
v, [DisplayTerm]
vs, Elims
es)

instance Subst t a => Subst t (Tele a) where
  applySubst :: Substitution' t -> Tele a -> Tele a
applySubst Substitution' t
rho  Tele a
EmptyTel         = Tele a
forall a. Tele a
EmptyTel
  applySubst Substitution' t
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' t -> (a, Abs (Tele a)) -> (a, Abs (Tele a))
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (a
t, Abs (Tele a)
tel)

instance Subst Term Constraint where
  applySubst :: Substitution' Term -> Constraint -> Constraint
applySubst Substitution' Term
rho Constraint
c = case Constraint
c of
    ValueCmp Comparison
cmp CompareAs
a Term
u Term
v       -> Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp (CompareAs -> CompareAs
forall a. Subst Term a => a -> a
rf CompareAs
a) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
u) (Term -> Term
forall a. Subst Term 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. Subst Term a => a -> a
rf Term
p) (Type -> Type
forall a. Subst Term a => a -> a
rf Type
t) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
u) (Term -> Term
forall a. Subst Term 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. Subst Term a => a -> a
rf Type
a) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
v) (Elims -> Elims
forall a. Subst Term a => a -> a
rf Elims
e1) (Elims -> Elims
forall a. Subst Term a => a -> a
rf Elims
e2)
    TelCmp Type
a Type
b Comparison
cmp Telescope
tel1 Telescope
tel2 -> Type -> Type -> Comparison -> Telescope -> Telescope -> Constraint
TelCmp (Type -> Type
forall a. Subst Term a => a -> a
rf Type
a) (Type -> Type
forall a. Subst Term a => a -> a
rf Type
b) Comparison
cmp (Telescope -> Telescope
forall a. Subst Term a => a -> a
rf Telescope
tel1) (Telescope -> Telescope
forall a. Subst Term a => a -> a
rf Telescope
tel2)
    SortCmp Comparison
cmp Sort
s1 Sort
s2        -> Comparison -> Sort -> Sort -> Constraint
SortCmp Comparison
cmp (Sort -> Sort
forall a. Subst Term a => a -> a
rf Sort
s1) (Sort -> Sort
forall a. Subst Term a => a -> a
rf Sort
s2)
    LevelCmp Comparison
cmp Level
l1 Level
l2       -> Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
cmp (Level -> Level
forall a. Subst Term a => a -> a
rf Level
l1) (Level -> Level
forall a. Subst Term a => a -> a
rf Level
l2)
    Guarded Constraint
c ProblemId
cs             -> Constraint -> ProblemId -> Constraint
Guarded (Constraint -> Constraint
forall a. Subst Term a => a -> a
rf Constraint
c) ProblemId
cs
    IsEmpty Range
r Type
a              -> Range -> Type -> Constraint
IsEmpty Range
r (Type -> Type
forall a. Subst Term a => a -> a
rf Type
a)
    CheckSizeLtSat Term
t         -> Term -> Constraint
CheckSizeLtSat (Term -> Term
forall a. Subst Term a => a -> a
rf Term
t)
    FindInstance MetaId
m Maybe MetaId
b Maybe [Candidate]
cands   -> MetaId -> Maybe MetaId -> Maybe [Candidate] -> Constraint
FindInstance MetaId
m Maybe MetaId
b (Maybe [Candidate] -> Maybe [Candidate]
forall a. Subst Term a => a -> a
rf Maybe [Candidate]
cands)
    UnBlock{}                -> Constraint
c
    CheckFunDef{}            -> Constraint
c
    HasBiggerSort Sort
s          -> Sort -> Constraint
HasBiggerSort (Sort -> Sort
forall a. Subst Term 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. Subst Term a => a -> a
rf Dom Type
a) (Abs Sort -> Abs Sort
forall a. Subst Term a => a -> a
rf Abs Sort
s)
    UnquoteTactic Maybe MetaId
m Term
t Term
h Type
g    -> Maybe MetaId -> Term -> Term -> Type -> Constraint
UnquoteTactic Maybe MetaId
m (Term -> Term
forall a. Subst Term a => a -> a
rf Term
t) (Term -> Term
forall a. Subst Term a => a -> a
rf Term
h) (Type -> Type
forall a. Subst Term a => a -> a
rf Type
g)
    CheckMetaInst MetaId
m          -> MetaId -> Constraint
CheckMetaInst MetaId
m
    where
      rf :: a -> a
rf a
x = Substitution' Term -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho a
x

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

instance Subst t a => Subst t (Elim' a) where
  applySubst :: Substitution' t -> Elim' a -> Elim' a
applySubst Substitution' t
rho Elim' a
e = case Elim' a
e of
    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' t -> Arg a -> Arg a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
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' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x) (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
y) (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
r)
    Proj{}  -> Elim' a
e

instance Subst t a => Subst t (Abs a) where
  applySubst :: Substitution' t -> Abs a -> Abs a
applySubst Substitution' t
rho (Abs String
x a
a)   = String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Int -> Substitution' t -> Substitution' t
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' t
rho) a
a
  applySubst Substitution' t
rho (NoAbs String
x a
a) = String -> a -> Abs a
forall a. String -> a -> Abs a
NoAbs String
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
a

instance Subst t a => Subst t (Arg a) where
  applySubst :: Substitution' t -> Arg a -> Arg a
applySubst Substitution' t
IdS Arg a
arg = Arg a
arg
  applySubst Substitution' t
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho) Arg a
arg

instance Subst t a => Subst t (Named name a) where
  applySubst :: Substitution' t -> Named name a -> Named name a
applySubst Substitution' t
rho = (a -> a) -> Named name a -> Named name a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho)

instance (Subst t a, Subst t b) => Subst t (Dom' a b) where
  applySubst :: Substitution' t -> Dom' a b -> Dom' a b
applySubst Substitution' t
IdS Dom' a b
dom = Dom' a b
dom
  applySubst Substitution' t
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho) Dom' a b
dom{ domTactic :: Maybe a
domTactic = Substitution' t -> Maybe a -> Maybe a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (Dom' a b -> Maybe a
forall t e. Dom' t e -> Maybe t
domTactic Dom' a b
dom) }

instance Subst t a          => Subst t (Maybe a)      where
instance Subst t a          => Subst t [a]            where
instance (Ord k, Subst t a) => Subst t (Map k a)      where
instance Subst t a          => Subst t (WithHiding a) where

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

instance (Subst t a, Subst t b) => Subst t (a, b) where
  applySubst :: Substitution' t -> (a, b) -> (a, b)
applySubst Substitution' t
rho (a
x,b
y) = (Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho a
x, Substitution' t -> b -> b
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho b
y)

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

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

instance Subst Term Candidate where
  applySubst :: Substitution' Term -> Candidate -> Candidate
applySubst Substitution' Term
rho (Candidate Term
u Type
t Bool
ov) = Term -> Type -> Bool -> Candidate
Candidate (Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Term
u) (Substitution' Term -> Type -> Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho Type
t) Bool
ov

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

instance DeBruijn a => DeBruijn (Pattern' a) where
  debruijnNamedVar :: String -> Int -> Pattern' a
debruijnNamedVar String
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
$ String -> Int -> a
forall a. DeBruijn a => String -> Int -> a
debruijnNamedVar String
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 :: Substitution' DeBruijnPattern -> Substitution' Term
fromPatternSubstitution = (DeBruijnPattern -> Term)
-> Substitution' DeBruijnPattern -> Substitution' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm

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


usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatOrigin :: 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 :: 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 DeBruijnPattern where
  applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern
applySubst Substitution' DeBruijnPattern
IdS DeBruijnPattern
p = DeBruijnPattern
p
  applySubst Substitution' DeBruijnPattern
rho DeBruijnPattern
p = case DeBruijnPattern
p of
    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
$
      String -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> String
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
      Substitution' DeBruijnPattern -> Int -> DeBruijnPattern
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' 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
$ Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
u
    ConP ConHead
c ConPatternInfo
ci NAPs
ps -> ConHead -> ConPatternInfo -> NAPs -> DeBruijnPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci (NAPs -> DeBruijnPattern) -> NAPs -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho NAPs
ps
    DefP PatternInfo
i QName
q NAPs
ps  -> PatternInfo -> QName -> NAPs -> DeBruijnPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
i QName
q (NAPs -> DeBruijnPattern) -> NAPs -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern -> NAPs -> NAPs
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' DeBruijnPattern
rho NAPs
ps
    LitP PatternInfo
i Literal
x     -> DeBruijnPattern
p
    ProjP{}      -> DeBruijnPattern
p
    IApplyP PatternInfo
i Term
t Term
u DBPatVar
x -> case String -> DeBruijnPattern -> DeBruijnPattern
useName (DBPatVar -> String
dbPatVarName DBPatVar
x) (DeBruijnPattern -> DeBruijnPattern)
-> DeBruijnPattern -> DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Substitution' DeBruijnPattern -> Int -> DeBruijnPattern
forall a. Subst a a => Substitution' a -> Int -> a
lookupS Substitution' 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 (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
t) (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' 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 (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
t) (Substitution' DeBruijnPattern -> Term -> Term
forall a. Subst Term a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
rho Term
u) DBPatVar
y
                        DeBruijnPattern
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
    where
      useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
      useName :: String -> DeBruijnPattern -> DeBruijnPattern
useName String
n (VarP PatternInfo
o DBPatVar
x)
        | String -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (DBPatVar -> String
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 :: String
dbPatVarName = String
n }
      useName String
_ DeBruijnPattern
x = DeBruijnPattern
x

instance Subst Term Range where
  applySubst :: Substitution' Term -> Range -> Range
applySubst Substitution' Term
_ = Range -> Range
forall c. c -> c
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 String] -> Maybe ([Arg String], Arg String)
forall a. [a] -> Maybe ([a], a)
initLast ([Arg String] -> Maybe ([Arg String], Arg String))
-> [Arg String] -> Maybe ([Arg String], Arg String)
forall a b. (a -> b) -> a -> b
$ ProjLams -> [Arg String]
getProjLams ProjLams
lams of
    -- If we have no more abstractions, we must be a record field
    -- (projection applied already to record value).
    Maybe ([Arg String], Arg String)
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 String]
pars, Arg ArgInfo
i String
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
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
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
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
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 (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 String]
pars', Args
args') = [Arg String] -> Args -> ([Arg String], Args)
forall a b. [a] -> [b] -> ([a], [b])
dropCommon [Arg String]
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 String -> Term -> Term) -> Term -> [Arg String] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr (\ (Arg ArgInfo
ai String
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
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
x) (Term
core Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
args') [Arg String]
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 { TelV a -> Tele (Dom a)
theTel :: Tele (Dom a), TelV a -> a
theCore :: a }
  deriving (Int -> TelV a -> String -> String
[TelV a] -> String -> String
TelV a -> String
(Int -> TelV a -> String -> String)
-> (TelV a -> String)
-> ([TelV a] -> String -> String)
-> Show (TelV a)
forall a. Show a => Int -> TelV a -> String -> String
forall a. Show a => [TelV a] -> String -> String
forall a. Show a => TelV a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [TelV a] -> String -> String
$cshowList :: forall a. Show a => [TelV a] -> String -> String
show :: TelV a -> String
$cshow :: forall a. Show a => TelV a -> String
showsPrec :: Int -> TelV a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> TelV a -> String -> String
Show, a -> TelV b -> TelV a
(a -> b) -> TelV a -> TelV b
(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
<$ :: a -> TelV b -> TelV a
$c<$ :: forall a b. a -> TelV b -> TelV a
fmap :: (a -> b) -> TelV a -> TelV b
$cfmap :: forall a b. (a -> b) -> TelV a -> TelV b
Functor)

deriving instance (Subst Term a, Eq  a) => Eq  (TelV a)
deriving instance (Subst Term 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 -> String -> TelView -> TelView
forall a. Dom a -> String -> TelV a -> TelV a
absV Dom Type
a (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) (TelView -> TelView) -> 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 t a. Subst t 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
  where
    absV :: Dom a -> String -> TelV a -> TelV a
absV Dom a
a String
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 (String -> Tele (Dom a) -> Abs (Tele (Dom a))
forall a. String -> a -> Abs a
Abs String
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' :: (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' Term (a, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> a
f Name
x,) Dom Type
t Dom' Term (a, Type) -> ListTel' a -> ListTel' a
forall a. a -> [a] -> [a]
: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
forall a. (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel' Name -> a
f [Name]
xs (Int -> Dom Type -> Dom Type
forall t a. Subst t a => Int -> a -> a
raise Int
1 Dom Type
t)

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

-- | 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 (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
$ String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Name -> String
nameToArgName (Name -> String) -> Name -> String
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 t a. Subst t a => Int -> a -> a
raise Int
1 Type
t)

domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName :: NamedArg Name -> Dom' Term ()
domFromNamedArgName NamedArg Name
x = () () -> Dom' Term Name -> Dom' Term ()
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 (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 String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName) -> Ranged String -> NamedName
forall a b. (a -> b) -> a -> b
$ Range -> String -> Ranged String
forall a. Range -> a -> Ranged a
Ranged (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x) (String -> Ranged String) -> String -> Ranged String
forall a b. (a -> b) -> a -> b
$ Name -> String
nameToArgName Name
x) Name
x
    forceName Named NamedName Name
x = Named NamedName Name
x

-- ** Abstracting in terms and types

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

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

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
forall a. a -> Type'' Term a
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 :: a -> Type'' Term a
el = Sort -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> a -> Type'' Term a) -> Sort -> a -> Type'' Term a
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
piSort Dom Type
u (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)

-- | 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 t a. (Subst t 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 c. c -> c
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 String
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 Sort -> Sort
piSort Dom Type
u (Abs Sort -> Sort) -> Abs Sort -> Sort
forall a b. (a -> b) -> a -> b
$ 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) (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 t a. (Subst t 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 (String, Type)] -> Term -> Term
teleNoAbs [Dom' Term (String, Type)]
tel Term
t = (Dom' Term (String, Type) -> Term -> Term)
-> Term -> [Dom' Term (String, Type)] -> Term
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 = (String
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
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
x) Term
t [Dom' Term (String, Type)]
tel

instance TeleNoAbs Telescope where
  teleNoAbs :: Telescope -> Term -> Term
teleNoAbs Telescope
tel = [Dom' Term (String, Type)] -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs ([Dom' Term (String, Type)] -> Term -> Term)
-> [Dom' Term (String, Type)] -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, 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 (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 -> Term -> Telescope
forall t a. Subst t a => Abs a -> t -> a
absApp Abs Telescope
tel Term
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' Term -> Maybe Term -> Maybe Term
forall t a. Subst t a => Substitution' t -> 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 Candidate

deriving instance (Subst t a, Eq a)  => Eq  (Tele a)
deriving instance (Subst t 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 CompareAs
deriving instance Eq Section

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

instance Eq LevelAtom where
  == :: LevelAtom' Term -> LevelAtom' Term -> Bool
(==) = Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Term -> Term -> Bool)
-> (LevelAtom' Term -> Term)
-> LevelAtom' Term
-> LevelAtom' Term
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LevelAtom' Term -> Term
unLevelAtom

instance Ord LevelAtom where
  compare :: LevelAtom' Term -> LevelAtom' Term -> Ordering
compare = Term -> Term -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Term -> Term -> Ordering)
-> (LevelAtom' Term -> Term)
-> LevelAtom' Term
-> LevelAtom' Term
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LevelAtom' Term -> Term
unLevelAtom

-- | 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 -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
x Int
a Ordering -> Ordering -> Ordering
`thenCmp` Elims -> Elims -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Elims
b 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 t a, Eq a) => Eq (Abs a) where
  NoAbs String
_ a
a == :: Abs a -> Abs a -> Bool
== NoAbs String
_ 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 t a. Subst t a => Abs a -> a
absBody Abs a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Abs a -> a
forall t a. Subst t a => Abs a -> a
absBody Abs a
b

instance (Subst t a, Ord a) => Ord (Abs a) where
  NoAbs String
_ a
a compare :: Abs a -> Abs a -> Ordering
`compare` NoAbs String
_ 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 t a. Subst t a => Abs a -> a
absBody Abs a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Abs a -> a
forall t a. Subst t a => Abs a -> a
absBody Abs a
b

deriving instance Ord a => Ord (Dom a)

instance (Subst t 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 t 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@). @univInf@ is returned
--   as the sort of @Inf@.
--
--   Precondition: @s@ is reduced
univSort' :: Maybe Sort -> Sort -> Maybe Sort
univSort' :: Maybe Sort -> Sort -> Maybe Sort
univSort' Maybe Sort
univInf (Type Level
l) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe 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' Maybe Sort
univInf (Prop Level
l) = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe 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' Maybe Sort
univInf Sort
Inf      = Maybe Sort
univInf
univSort' Maybe Sort
univInf Sort
s        = Maybe Sort
forall a. Maybe a
Nothing

univSort :: Maybe Sort -> Sort -> Sort
univSort :: Maybe Sort -> Sort -> Sort
univSort Maybe Sort
univInf Sort
s = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
s) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Maybe Sort -> Sort -> Maybe Sort
univSort' Maybe Sort
univInf Sort
s

univInf :: (HasOptions m) => m (Maybe Sort)
univInf :: m (Maybe Sort)
univInf =
  m Bool -> m (Maybe Sort) -> m (Maybe Sort) -> m (Maybe Sort)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((PragmaOptions -> Bool
optOmegaInOmega (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` m Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType)
  {-then-} (Maybe Sort -> m (Maybe Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Sort -> m (Maybe Sort)) -> Maybe Sort -> m (Maybe Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf)
  {-else-} (Maybe Sort -> m (Maybe Sort)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Sort
forall a. Maybe a
Nothing)

-- | Compute the sort of a function type from the sorts of its
--   domain and codomain.
funSort' :: Sort -> Sort -> Maybe Sort
funSort' :: Sort -> Sort -> Maybe Sort
funSort' Sort
a Sort
b = case (Sort
a, Sort
b) of
  (Sort
Inf           , Sort
_            ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
  (Sort
_             , Sort
Inf          ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
  (Type Level
a , Type Level
b) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe 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
  (Sort
SizeUniv      , Sort
b            ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
b
  (Sort
_             , Sort
SizeUniv     ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
SizeUniv
  (Prop Level
a , Type Level
b) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe 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 -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe 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
  (Sort
a             , Sort
b            ) -> Maybe Sort
forall a. Maybe a
Nothing

funSort :: Sort -> Sort -> Sort
funSort :: Sort -> Sort -> Sort
funSort Sort
a Sort
b = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
a Sort
b) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Maybe Sort
funSort' Sort
a Sort
b

-- | Compute the sort of a pi type from the sorts of its domain
--   and codomain.
piSort' :: Dom Type -> Abs Sort -> Maybe Sort
piSort' :: Dom Type -> Abs Sort -> Maybe Sort
piSort' Dom Type
a      (NoAbs String
_ Sort
b) = Sort -> Sort -> Maybe Sort
funSort' (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) Sort
b
piSort' Dom Type
a bAbs :: Abs Sort
bAbs@(Abs   String
_ Sort
b) = case Int -> Sort -> Maybe (FlexRig' ())
forall a. Free a => Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn Int
0 Sort
b of
  Maybe (FlexRig' ())
Nothing -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just (Sort -> Maybe Sort) -> Sort -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Empty -> Abs Sort -> Sort
forall t a. Subst t a => Empty -> Abs a -> a
noabsApp Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ Abs Sort
bAbs
  Just FlexRig' ()
o -> case FlexRig' ()
o of
    FlexRig' ()
StronglyRigid -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
    FlexRig' ()
Unguarded     -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
    FlexRig' ()
WeaklyRigid   -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
    Flexible ()
_    -> Maybe Sort
forall a. Maybe a
Nothing
-- 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 Type -> Abs Sort -> Sort
piSort :: Dom Type -> Abs Sort -> Sort
piSort Dom Type
a Abs Sort
b = case Dom Type -> Abs Sort -> Maybe Sort
piSort' Dom Type
a Abs Sort
b of
  Just Sort
s -> Sort
s
  Maybe Sort
Nothing | NoAbs String
_ Sort
b' <- Abs Sort
b -> Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) Sort
b'
          | Bool
otherwise       -> Dom Type -> Abs Sort -> Sort
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort Dom Type
a Abs Sort
b

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

-- ^ Computes @n0 ⊔ a₁ ⊔ a₂ ⊔ ... ⊔ aₙ@ and return its canonical form.
levelMax :: Integer -> [PlusLevel] -> Level
levelMax :: Integer -> [PlusLevel] -> Level
levelMax Integer
n0 [PlusLevel]
as0 = Integer -> [PlusLevel] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n [PlusLevel]
as
  where
    -- step 1: flatten nested @Level@ expressions in @LevelAtom@s
    Max Integer
n1 [PlusLevel]
as1 = Level -> Level
expandLevel (Level -> Level) -> Level -> Level
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n0 [PlusLevel]
as0
    -- step 2: remove subsumed @PlusLevel@s
    as2 :: [PlusLevel]
as2       = [PlusLevel] -> [PlusLevel]
forall t. Eq (LevelAtom' t) => [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [PlusLevel]
as1
    -- step 3: sort remaining @PlusLevel@s
    as :: [PlusLevel]
as        = [PlusLevel] -> [PlusLevel]
forall a. Ord a => [a] -> [a]
List.sort [PlusLevel]
as2
    -- step 4: set constant to 0 if it is subsumed by one of the @PlusLevel@s
    greatestB :: Integer
greatestB = [Integer] -> Integer
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 LevelAtom' Term
_ <- [PlusLevel]
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] -> [Level] -> Level
lmax Integer
m [PlusLevel]
as []              = Integer -> [PlusLevel] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m [PlusLevel]
as
    lmax Integer
m [PlusLevel]
as (Max Integer
n [PlusLevel]
bs : [Level]
ls) = Integer -> [PlusLevel] -> [Level] -> Level
lmax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel]
bs [PlusLevel] -> [PlusLevel] -> [PlusLevel]
forall a. [a] -> [a] -> [a]
++ [PlusLevel]
as) [Level]
ls

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

    expandPlus :: PlusLevel -> Level
    expandPlus :: PlusLevel -> Level
expandPlus (Plus Integer
m LevelAtom' Term
l) = Integer -> Level -> Level
levelPlus Integer
m (Level -> Level) -> Level -> Level
forall a b. (a -> b) -> a -> b
$ LevelAtom' Term -> Level
expandAtom LevelAtom' Term
l

    expandAtom :: LevelAtom -> Level
    expandAtom :: LevelAtom' Term -> Level
expandAtom LevelAtom' Term
l = case LevelAtom' Term
l of
      BlockedLevel MetaId
_ Term
v -> Term -> Level
expandTm Term
v
      NeutralLevel NotBlocked
_ Term
v -> Term -> Level
expandTm Term
v
      UnreducedLevel Term
v -> Term -> Level
expandTm Term
v
      MetaLevel{}      -> Integer -> [PlusLevel] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [Integer -> LevelAtom' Term -> PlusLevel
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
0 LevelAtom' Term
l]
      where
        expandTm :: Term -> Level
expandTm (Level Level
l)       = Level -> Level
expandLevel Level
l
        expandTm (Sort (Type Level
l)) = Level -> Level
expandLevel Level
l -- TODO: get rid of this horrible hack!
        expandTm Term
v               = Integer -> [PlusLevel] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [Integer -> LevelAtom' Term -> PlusLevel
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
0 LevelAtom' Term
l]

    removeSubsumed :: [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [] = []
    removeSubsumed (Plus Integer
n LevelAtom' t
a : [PlusLevel' t]
bs)
      | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
ns = [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [PlusLevel' t]
bs
      | Bool
otherwise     = Integer -> LevelAtom' t -> PlusLevel' t
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
n LevelAtom' t
a PlusLevel' t -> [PlusLevel' t] -> [PlusLevel' t]
forall a. a -> [a] -> [a]
: [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [ PlusLevel' t
b | b :: PlusLevel' t
b@(Plus Integer
_ LevelAtom' t
a') <- [PlusLevel' t]
bs, LevelAtom' t
a LevelAtom' t -> LevelAtom' t -> Bool
forall a. Eq a => a -> a -> Bool
/= LevelAtom' t
a' ]
      where
        ns :: [Integer]
ns = [ Integer
m | Plus Integer
m LevelAtom' t
a' <- [PlusLevel' t]
bs, LevelAtom' t
a LevelAtom' t -> LevelAtom' t -> Bool
forall a. Eq a => a -> a -> Bool
== LevelAtom' t
a', Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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]
as) (Max Integer
n [PlusLevel]
bs) = Integer -> [PlusLevel] -> Level
levelMax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel] -> Level) -> [PlusLevel] -> Level
forall a b. (a -> b) -> a -> b
$ [PlusLevel]
as [PlusLevel] -> [PlusLevel] -> [PlusLevel]
forall a. [a] -> [a] -> [a]
++ [PlusLevel]
bs

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

unLevelAtom :: LevelAtom -> Term
unLevelAtom :: LevelAtom' Term -> Term
unLevelAtom (MetaLevel MetaId
x Elims
es)   = MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
unLevelAtom (NeutralLevel NotBlocked
_ Term
v) = Term
v
unLevelAtom (UnreducedLevel Term
v) = Term
v
unLevelAtom (BlockedLevel MetaId
_ Term
v) = Term
v