{-# 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 err' :: Empty -> Term -> Elims -> Term
err' m :: t
m [] = t
m
applyTermE err' :: Empty -> Term -> Elims -> Term
err' m :: t
m es :: Elims
es = Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$
    case t -> Term
forall a b. Coercible a b => a -> b
coerce t
m of
      Var i :: Int
i es' :: Elims
es'   -> Int -> Elims -> Term
Var Int
i (Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es)
      Def f :: QName
f es' :: Elims
es'   -> QName -> Elims -> Elims -> Term
defApp QName
f Elims
es' Elims
es  -- remove projection redexes
      Con c :: ConHead
c ci :: ConInfo
ci args :: 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 _ b :: Abs Term
b     ->
        case Elims
es of
          Apply a :: Arg Term
a : es0 :: Elims
es0      -> Abs t -> t -> t
forall t a. Subst t a => Abs a -> t -> a
lazyAbsApp (Abs Term -> Abs t
forall a b. Coercible a b => a -> b
coerce Abs Term
b :: Abs t) (Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> 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 _ _ a :: Term
a : es0 :: Elims
es0 -> Abs t -> t -> t
forall t a. Subst t a => Abs a -> t -> a
lazyAbsApp (Abs Term -> Abs t
forall a b. Coercible a b => a -> b
coerce Abs Term
b :: Abs t) (Term -> t
forall a b. Coercible a b => a -> b
coerce Term
a)         t -> Elims -> Term
forall x. Coercible t x => x -> Elims -> Term
`app` Elims
es0
          _             -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV x :: MetaId
x es' :: 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 _ _      -> Empty -> Term
err Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
      Sort s :: 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 s :: String
s es' :: Elims
es' -> String -> Elims -> Term
Dummy String
s (Elims
es' Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es)
      DontCare mv :: 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 t :: x
t es :: Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ (x -> t
forall a b. Coercible a b => a -> b
coerce x
t :: t) t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
     err :: Empty -> Term
err e :: Empty
e = Empty -> Term -> Elims -> Term
err' Empty
e (t -> Term
forall a b. Coercible a b => a -> b
coerce t
m) Elims
es

instance Apply Term where
  applyE :: Term -> Elims -> Term
applyE = (Empty -> Term -> Elims -> Term) -> Term -> Elims -> Term
forall t.
(Coercible Term t, Apply t, 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 (\ _ t :: Term
t es :: Elims
es ->  String -> Elims -> Term
Dummy "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 f :: QName
f v :: Term
v =
  case Term
v of
    (Con (ConHead _ _ fs :: [Arg QName]
fs) _ vs :: Elims
vs) -> do
      (fld :: Arg QName
fld, i :: 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)
    _ -> 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 fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch                  ci :: ConInfo
ci args :: Elims
args []             = ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ci Elims
args
conApp fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch                  ci :: ConInfo
ci args :: Elims
args (a :: Elim' Term
a@Apply{} : es :: 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 fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch                  ci :: ConInfo
ci args :: Elims
args (a :: Elim' Term
a@IApply{} : es :: 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 fk :: Empty -> Term -> Elims -> Term
fk ch :: ConHead
ch@(ConHead c :: QName
c _ fs :: [Arg QName]
fs) ci :: ConInfo
ci args :: Elims
args ees :: Elims
ees@(Proj o :: ProjOrigin
o f :: QName
f : es :: Elims
es) =
  let failure :: c -> c
failure err :: 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
$
        "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]
++
        " 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
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]
++
        " 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
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]
++
        " 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 e :: 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 err :: 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 v :: Term
v es :: Elims
es = t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ t -> Elims -> t
forall t. Apply t => t -> Elims -> t
applyE (Term -> t
forall a b. Coercible a b => a -> b
coerce Term
v :: t) Elims
es
  in
   case (Arg QName -> Bool) -> [Arg QName] -> Maybe (Arg QName, Int)
forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex ((QName
fQName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool) -> (Arg QName -> QName) -> Arg QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg QName -> QName
forall e. Arg e -> e
unArg) [Arg QName]
fs of
     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 (fld :: Arg QName
fld, i :: 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 f :: QName
f [] (Apply a :: Arg Term
a : es :: Elims
es) | Just v :: 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 f :: QName
f es0 :: Elims
es0 es :: 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 ai :: ArgInfo
ai v :: 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 ai :: a
ai v :: 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 s :: Sort
s [] = Sort
s
  applyE s :: Sort
s es :: Elims
es = case Sort
s of
    MetaS x :: MetaId
x es' :: 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  d :: QName
d es' :: 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
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 tel :: Tele a
tel               []       = Tele a
tel
  apply EmptyTel          _        = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
  apply (ExtendTel _ tel :: Abs (Tele a)
tel) (t :: Arg Term
t : ts :: 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 t :: Tele a
t es :: 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 info :: ArgInfo
info x :: QName
x t :: Type
t pol :: [Polarity]
pol occ :: [Occurrence]
occ gens :: NumGeneralizableArgs
gens gpars :: [Maybe Name]
gpars df :: [LocalDisplayForm]
df m :: MutualId
m c :: CompiledRepresentation
c inst :: Maybe QName
inst copy :: Bool
copy ma :: Set QName
ma nc :: Bool
nc inj :: Bool
inj copat :: Bool
copat blk :: Blocked_
blk d :: Defn
d) args :: 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 t :: Definition
t es :: 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 r :: RewriteRule
r args :: 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 t :: RewriteRule
t es :: 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 occ :: [Occurrence]
occ args :: 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 t :: [Occurrence]
t es :: 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 pol :: [Polarity]
pol args :: 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 t :: [Polarity]
t es :: 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 NoGeneralizableArgs       args :: Args
args = NumGeneralizableArgs
NoGeneralizableArgs
  apply (SomeGeneralizableArgs n :: Int
n) args :: 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 t :: NumGeneralizableArgs
t es :: 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 ps :: [NamedArg (Pattern' a)]
ps args :: 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 0 ps :: [NamedArg (Pattern' x)]
ps = [NamedArg (Pattern' x)]
ps
    loop n :: a
n [] = [NamedArg (Pattern' x)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    loop n :: a
n (p :: NamedArg (Pattern' x)
p : ps :: [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
- 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 t :: [NamedArg (Pattern' a)]
t es :: 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 p :: Projection
p args :: 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 t :: Projection
t es :: 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 lams :: [Arg String]
lams) args :: 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 t :: ProjLams
t es :: 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 d :: Defn
d [] = Defn
d
  apply d :: Defn
d args :: Args
args = case Defn
d of
    Axiom{} -> Defn
d
    DataOrRecSig n :: 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 d :: 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 p0 :: 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
< 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
> 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 = 0 } else Maybe Projection
forall a. Maybe a
Nothing
                , funExtLam :: Maybe ExtLamInfo
funExtLam         = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (\ _ -> 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 0 [] -> Bool
True; _ -> 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 t :: Defn
t es :: 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 x :: QName
x ar :: Int
ar def :: Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) args :: 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
$ \ vs :: 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 t :: PrimFun
t es :: 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 rl :: Range
rl rf :: Range
rf tel :: Telescope
tel ps :: NAPs
ps b :: Maybe Term
b t :: Maybe (Arg Type)
t catchall :: Bool
catchall recursive :: Maybe Bool
recursive unreachable :: Maybe Bool
unreachable ell :: ExpandedEllipsis
ell) args :: 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 i :: Int
i v :: 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 _ _ [] [] = Substitution' a
forall a. Substitution' a
idS
        mkSub tm :: Term -> a
tm n :: Int
n (p :: NamedArg DeBruijnPattern
p : ps :: NAPs
ps) (v :: Term
v : vs :: [Term]
vs) =
          case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
            VarP _ (DBPatVar _ i :: 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
- 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
- 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 c :: ConHead
c _ ps' :: 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 o :: PatternInfo
o q :: QName
q ps' :: 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 _ _ _ (DBPatVar _ i :: 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
- 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
- 1) Term
v
        mkSub _ _ _ _ = 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 n :: Int
n tel :: Telescope
tel [] [] = Telescope
tel
        newTel n :: Int
n tel :: Telescope
tel (p :: NamedArg DeBruijnPattern
p : ps :: NAPs
ps) (v :: Term
v : vs :: [Term]
vs) =
          case NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
p of
            VarP _ (DBPatVar _ i :: Int
i) -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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
- 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
- 1) Term
v) NAPs
ps) [Term]
vs
            DotP{}              -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel Int
n Telescope
tel NAPs
ps [Term]
vs
            ConP c :: ConHead
c _ ps' :: 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 _ q :: QName
q ps' :: 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 _ _ _ (DBPatVar _ i :: Int
i) -> Int -> Telescope -> NAPs -> [Term] -> Telescope
newTel (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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
- 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
- 1) Term
v) NAPs
ps) [Term]
vs
        newTel _ tel :: Telescope
tel _ _ = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__

        projections :: ConHead -> Term -> [Term]
projections c :: ConHead
c v :: 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 ai :: ArgInfo
ai f :: QName
f <- ConHead -> [Arg QName]
conFields ConHead
c ]

        -- subTel i v (Δ₁ (xᵢ : A) Δ₂) = Δ₁ Δ₂[xᵢ = v]
        subTel :: t -> t -> Tele a -> Tele a
subTel i :: t
i v :: t
v EmptyTel = Tele a
forall a. HasCallStack => a
__IMPOSSIBLE__
        subTel 0 v :: t
v (ExtendTel _ tel :: 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 i :: t
i v :: t
v (ExtendTel a :: a
a tel :: 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
- 1) (Int -> t -> t
forall t a. Subst t a => Int -> a -> a
raise 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 t :: Clause
t es :: 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 cc :: CompiledClauses
cc args :: Args
args = case CompiledClauses
cc of
    Fail     -> CompiledClauses
forall a. CompiledClauses' a
Fail
    Done hs :: [Arg String]
hs t :: 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 [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
- 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 n :: Arg Int
n bs :: 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
<&> \ m :: 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 t :: CompiledClauses
t es :: 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 m :: ModuleName
m sys :: Maybe System
sys) args :: 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 t :: ExtLamInfo
t es :: 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 tel :: Telescope
tel sys :: [(Face, Term)]
sys) args :: 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 t :: System
t es :: 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 n :: Int
n a :: a
a) args :: 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 n :: Int
n a :: a
a) es :: 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 cop :: Bool
cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lz :: Bool
lz) args :: 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 cop :: Bool
cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lz :: Bool
lz) es :: 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 NotInjective  args :: Args
args = FunctionInverse
forall c. FunctionInverse' c
NotInjective
  apply (Inverse inv :: InversionMap Clause
inv) args :: 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 t :: FunctionInverse
t es :: 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 v :: Term
v)          args :: 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 v :: Term
v)           args :: 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 c :: ConHead
c ci :: ConInfo
ci vs :: [Arg DisplayTerm]
vs)     args :: 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 c :: QName
c es :: [Elim' DisplayTerm]
es)        args :: 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 v :: DisplayTerm
v ws :: [DisplayTerm]
ws es :: Elims
es) args :: 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 v :: Term
v)           es :: 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 v :: Term
v)            es :: 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 c :: ConHead
c ci :: ConInfo
ci vs :: [Arg DisplayTerm]
vs)      es :: 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 c :: QName
c es' :: [Elim' DisplayTerm]
es')        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 v :: DisplayTerm
v ws :: [DisplayTerm]
ws es' :: Elims
es') 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  ts :: [t]
ts args :: 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 ts :: [t]
ts es :: 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  b :: Blocked t
b args :: 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 b :: Blocked t
b es :: 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  x :: Maybe t
x args :: 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 x :: Maybe t
x es :: 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  x :: Maybe t
x args :: 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 x :: Maybe t
x es :: 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  x :: Map k v
x args :: 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 x :: Map k v
x es :: 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  x :: HashMap k v
x args :: 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 x :: HashMap k v
x es :: 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  (x :: a
x,y :: b
y) args :: 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 (x :: a
x,y :: b
y) es :: 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  (x :: a
x,y :: b
y,z :: c
z) args :: 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 (x :: a
x,y :: b
y,z :: c
z) es :: 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 x :: Drop a
x args :: 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 t :: Drop a
t es :: 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 tel :: Telescope
tel x :: 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 n :: Int
n xs :: [Int]
xs) args :: 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 t :: Permutation
t es :: 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 tel :: Telescope
tel (Perm n :: Int
n xs :: [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
$ [0..Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 t :: Type
t []                      = Type
t
piApply (El _ (Pi  _ b :: Abs Type
b)) (a :: Arg Term
a:args :: 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 t :: Type
t args :: Args
args                    =
  String -> Type -> Type
forall a. String -> a -> a
trace ("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]
++ "\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 EmptyTel s :: Sort
s = Sort
s
  abstract _        s :: Sort
s = Sort
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Abstract Telescope where
  EmptyTel           abstract :: Telescope -> Telescope -> Telescope
`abstract` tel :: Telescope
tel = Telescope
tel
  ExtendTel arg :: Dom Type
arg xtel :: Abs Telescope
xtel `abstract` tel :: 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 tel :: Telescope
tel (Defn info :: ArgInfo
info x :: QName
x t :: Type
t pol :: [Polarity]
pol occ :: [Occurrence]
occ gens :: NumGeneralizableArgs
gens gpars :: [Maybe Name]
gpars df :: [LocalDisplayForm]
df m :: MutualId
m c :: CompiledRepresentation
c inst :: Maybe QName
inst copy :: Bool
copy ma :: Set QName
ma nc :: Bool
nc inj :: Bool
inj copat :: Bool
copat blk :: Blocked_
blk d :: 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 tel :: Telescope
tel (RewriteRule q :: QName
q gamma :: Telescope
gamma f :: QName
f ps :: PElims
ps rhs :: Term
rhs t :: 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 tel :: Telescope
tel []  = []
  abstract tel :: Telescope
tel occ :: [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 tel :: Telescope
tel []  = []
  abstract tel :: Telescope
tel pol :: [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 tel :: Telescope
tel NoGeneralizableArgs       = NumGeneralizableArgs
NoGeneralizableArgs
  abstract tel :: Telescope
tel (SomeGeneralizableArgs n :: 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 tel :: Telescope
tel p :: 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 tel :: Telescope
tel (ProjLams lams :: [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 tel :: Telescope
tel (System tel1 :: Telescope
tel1 sys :: [(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 tel :: Telescope
tel d :: Defn
d = case Defn
d of
    Axiom{} -> Defn
d
    DataOrRecSig n :: 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 d :: 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 p :: 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
> 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
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
- 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 tel :: Telescope
tel (PrimFun x :: QName
x ar :: Int
ar def :: 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
$ \ts :: 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 tel :: Telescope
tel (Clause rl :: Range
rl rf :: Range
rf tel' :: Telescope
tel' ps :: NAPs
ps b :: Maybe Term
b t :: Maybe (Arg Type)
t catchall :: Bool
catchall recursive :: Maybe Bool
recursive unreachable :: Maybe Bool
unreachable ell :: 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 tel :: Telescope
tel Fail = CompiledClauses
forall a. CompiledClauses' a
Fail
  abstract tel :: Telescope
tel (Done xs :: [Arg String]
xs t :: 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 tel :: Telescope
tel (Case n :: Arg Int
n bs :: 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
<&> \ i :: 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 tel :: Telescope
tel (WithArity n :: Int
n a :: 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 tel :: Telescope
tel (Branches cop :: Bool
cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lz :: 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 m :: 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 m :: Int
m EmptyTel                     = []
namedTelVars m :: Int
m (ExtendTel !Dom Type
dom tel :: 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
-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
-1) (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel)

instance Abstract FunctionInverse where
  abstract :: Telescope -> FunctionInverse -> FunctionInverse
abstract tel :: Telescope
tel NotInjective  = FunctionInverse
forall c. FunctionInverse' c
NotInjective
  abstract tel :: Telescope
tel (Inverse inv :: 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 tel :: 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 tel :: Telescope
tel x :: 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 tel :: Telescope
tel m :: 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 tel :: Telescope
tel m :: 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
args x :: 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 info :: ArgInfo
info x :: 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]
:[])) ['a'..'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 err :: Empty
err p :: 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 n :: Int
n _) = 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 [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 err :: Empty
err p :: 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 rho :: Substitution' a
rho sgm :: 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 IdS t :: t
t = t
t
applySubstTerm rho :: Substitution' t
rho t :: t
t    = Term -> t
forall a b. Coercible a b => a -> b
coerce (Term -> t) -> Term -> t
forall a b. (a -> b) -> a -> b
$ case t -> Term
forall a b. Coercible a b => a -> b
coerce t
t of
    Var i :: Int
i es :: Elims
es    -> t -> Term
forall a b. Coercible a b => a -> b
coerce (t -> Term) -> t -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' t -> Int -> t
forall a. 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 h :: ArgInfo
h m :: 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 f :: QName
f es :: 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 c :: ConHead
c ci :: ConInfo
ci vs :: 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 x :: MetaId
x es :: 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 l :: Literal
l       -> Literal -> Term
Lit Literal
l
    Level l :: 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 a :: Dom Type
a b :: 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 s :: 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 mv :: 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 s :: String
s es :: 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 t :: b
t = a -> b
forall a b. Coercible a b => a -> b
coerce (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' t
rho (b -> a
forall a b. Coercible a b => a -> b
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 rho :: Substitution' t
rho (El s :: Sort' a
s t :: 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 rho :: Substitution' t
rho s :: Sort' a
s = case Sort' a
s of
    Type n :: 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 n :: 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
    Inf        -> Sort' a
forall t. Sort' t
Inf
    SizeUniv   -> Sort' a
forall t. Sort' t
SizeUniv
    PiSort a :: Dom' a (Type'' a a)
a s2 :: Abs (Sort' a)
s2 -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Sort -> Sort
piSort (Dom' a (Type'' a a) -> Dom Type
forall a b. Coercible a b => a -> b
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
forall a b. Coercible a b => a -> b
coerce (Abs (Sort' a) -> Abs Sort) -> Abs (Sort' a) -> Abs Sort
forall a b. (a -> b) -> a -> b
$ Abs (Sort' a) -> Abs (Sort' a)
forall a. Subst t a => a -> a
sub Abs (Sort' a)
s2)
    FunSort s1 :: Sort' a
s1 s2 :: Sort' a
s2 -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s1) (Sort' a -> Sort
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s2)
    UnivSort s :: Sort' a
s -> Sort -> Sort' a
forall a b. Coercible a b => a -> b
coerce (Sort -> Sort' a) -> Sort -> Sort' a
forall a b. (a -> b) -> a -> b
$ 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
forall a b. Coercible a b => a -> b
coerce (Sort' a -> Sort) -> Sort' a -> Sort
forall a b. (a -> b) -> a -> b
$ Sort' a -> Sort' a
forall a. Subst t a => a -> a
sub Sort' a
s
    MetaS x :: MetaId
x es :: [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 d :: QName
d es :: [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 x :: 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 rho :: Substitution' t
rho (Max n :: Integer
n as :: [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 rho :: Substitution' t
rho (Plus n :: Integer
n l :: 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 rho :: Substitution' t
rho (MetaLevel m :: MetaId
m vs :: [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 rho :: Substitution' t
rho (BlockedLevel m :: MetaId
m v :: 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 rho :: Substitution' t
rho (NeutralLevel _ v :: 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 rho :: Substitution' t
rho (UnreducedLevel v :: 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 rho :: Substitution' Term
rho = Name -> Name
forall c. c -> c
id

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

instance Subst Term ConPatternInfo where
  applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo
applySubst rho :: Substitution' Term
rho i :: 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 rho :: Substitution' Term
rho p :: Pattern
p = case Pattern
p of
    ConP c :: ConHead
c mt :: ConPatternInfo
mt ps :: [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 o :: PatternInfo
o q :: QName
q ps :: [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 o :: PatternInfo
o t :: 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 o :: PatternInfo
o s :: String
s     -> Pattern
p
    LitP o :: PatternInfo
o l :: Literal
l     -> Pattern
p
    ProjP{}      -> Pattern
p
    IApplyP o :: PatternInfo
o t :: Term
t u :: Term
u x :: 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 rho :: Substitution' Term
rho (A.ProblemEq p :: Pattern
p v :: Term
v a :: 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 i :: Int
i = Int -> [Arg Int] -> NLPat
PVar Int
i []
  deBruijnView :: NLPat -> Maybe Int
deBruijnView p :: NLPat
p = case NLPat
p of
    PVar i :: 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 p :: NLPat
p = case NLPat
p of
      PVar i :: Int
i xs :: [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 u :: Term
u        -> Term
u
      PDef f :: QName
f es :: PElims
es      -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PLam i :: ArgInfo
i u :: Abs NLPat
u       -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PPi a :: Dom NLPType
a b :: Abs NLPType
b        -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PSort s :: NLPSort
s        -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      PBoundVar i :: Int
i es :: 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 rho :: Substitution' NLPat
rho dom :: 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 rho :: Substitution' NLPat
rho p :: NLPat
p = case NLPat
p of
    PVar i :: Int
i bvs :: [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 f :: QName
f es :: 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 i :: ArgInfo
i u :: 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 a :: Dom NLPType
a b :: 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 s :: 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 i :: Int
i es :: 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 u :: 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 p :: NLPat
p ys :: [Arg Int]
ys = case NLPat
p of
        PVar i :: Int
i xs :: [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 u :: 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 f :: QName
f es :: PElims
es      -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PLam i :: ArgInfo
i u :: Abs NLPat
u       -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PPi a :: Dom NLPType
a b :: Abs NLPType
b        -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PSort s :: NLPSort
s        -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
        PBoundVar i :: Int
i es :: PElims
es -> NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Subst NLPat NLPType where
  applySubst :: Substitution' NLPat -> NLPType -> NLPType
applySubst rho :: Substitution' NLPat
rho (NLPType s :: NLPSort
s a :: 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 rho :: Substitution' NLPat
rho = \case
    PType l :: 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 l :: 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
    PInf      -> NLPSort
PInf
    PSizeUniv -> NLPSort
PSizeUniv

instance Subst NLPat RewriteRule where
  applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule
applySubst rho :: Substitution' NLPat
rho (RewriteRule q :: QName
q gamma :: Telescope
gamma f :: QName
f ps :: PElims
ps rhs :: Term
rhs t :: 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 rho :: Substitution' t
rho b :: 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 rho :: Substitution' Term
rho (Display n :: Int
n ps :: Elims
ps v :: 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 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 rho :: Substitution' Term
rho (DTerm v :: 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 rho :: Substitution' Term
rho (DDot v :: 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 rho :: Substitution' Term
rho (DCon c :: ConHead
c ci :: ConInfo
ci vs :: [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 rho :: Substitution' Term
rho (DDef c :: QName
c es :: [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 rho :: Substitution' Term
rho (DWithApp v :: DisplayTerm
v vs :: [DisplayTerm]
vs es :: 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 rho :: Substitution' t
rho  EmptyTel         = Tele a
forall a. Tele a
EmptyTel
  applySubst rho :: Substitution' t
rho (ExtendTel t :: a
t tel :: 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 rho :: Substitution' Term
rho c :: Constraint
c = case Constraint
c of
    ValueCmp cmp :: Comparison
cmp a :: CompareAs
a u :: Term
u v :: 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 cmp :: Comparison
cmp p :: Term
p t :: Type
t u :: Term
u v :: 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 ps :: [Polarity]
ps fs :: [IsForced]
fs a :: Type
a v :: Term
v e1 :: Elims
e1 e2 :: 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 a :: Type
a b :: Type
b cmp :: Comparison
cmp tel1 :: Telescope
tel1 tel2 :: 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 cmp :: Comparison
cmp s1 :: Sort
s1 s2 :: 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 cmp :: Comparison
cmp l1 :: Level
l1 l2 :: 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 c :: Constraint
c cs :: ProblemId
cs             -> Constraint -> ProblemId -> Constraint
Guarded (Constraint -> Constraint
forall a. Subst Term a => a -> a
rf Constraint
c) ProblemId
cs
    IsEmpty r :: Range
r a :: Type
a              -> Range -> Type -> Constraint
IsEmpty Range
r (Type -> Type
forall a. Subst Term a => a -> a
rf Type
a)
    CheckSizeLtSat t :: Term
t         -> Term -> Constraint
CheckSizeLtSat (Term -> Term
forall a. Subst Term a => a -> a
rf Term
t)
    FindInstance m :: MetaId
m b :: Maybe MetaId
b cands :: 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 s :: Sort
s          -> Sort -> Constraint
HasBiggerSort (Sort -> Sort
forall a. Subst Term a => a -> a
rf Sort
s)
    HasPTSRule a :: Dom Type
a s :: 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 m :: Maybe MetaId
m t :: Term
t h :: Term
h g :: 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 m :: MetaId
m          -> MetaId -> Constraint
CheckMetaInst MetaId
m
    where
      rf :: a -> a
rf x :: 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 rho :: Substitution' Term
rho (AsTermsOf a :: 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 rho :: Substitution' Term
rho AsSizes       = CompareAs
AsSizes
  applySubst rho :: Substitution' Term
rho AsTypes       = CompareAs
AsTypes

instance Subst t a => Subst t (Elim' a) where
  applySubst :: Substitution' t -> Elim' a -> Elim' a
applySubst rho :: Substitution' t
rho e :: Elim' a
e = case Elim' a
e of
    Apply v :: 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 x :: a
x y :: a
y r :: 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 rho :: Substitution' t
rho (Abs x :: String
x a :: 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 1 Substitution' t
rho) a
a
  applySubst rho :: Substitution' t
rho (NoAbs x :: String
x a :: 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 IdS arg :: Arg a
arg = Arg a
arg
  applySubst rho :: Substitution' t
rho arg :: 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 rho :: 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 IdS dom :: Dom' a b
dom = Dom' a b
dom
  applySubst rho :: Substitution' t
rho dom :: 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 _ _ = ()

instance (Subst t a, Subst t b) => Subst t (a, b) where
  applySubst :: Substitution' t -> (a, b) -> (a, b)
applySubst rho :: Substitution' t
rho (x :: a
x,y :: 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 rho :: Substitution' t
rho (x :: a
x,y :: b
y,z :: 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 rho :: Substitution' t
rho (x :: a
x,y :: b
y,z :: c
z,u :: 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 rho :: Substitution' Term
rho (Candidate u :: Term
u t :: Type
t ov :: 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 rho :: Substitution' Term
rho (OtherType t :: 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 rho :: Substitution' Term
rho (EqualityType s :: Sort
s eq :: QName
eq l :: Args
l t :: Arg Term
t a :: Arg Term
a b :: 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 n :: String
n i :: 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 _                   = 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 o :: PatOrigin
o p :: Pattern' a
p = case Pattern' a -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo Pattern' a
p of
  Nothing -> Pattern' a
p
  Just i :: 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 i :: PatternInfo
i p :: Pattern' a
p = case Pattern' a -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p of
  Nothing         -> Pattern' a
p
  Just PatOSplit  -> Pattern' a
p
  Just PatOAbsurd -> Pattern' a
p
  Just _          -> case Pattern' a
p of
    (VarP _ x :: a
x) -> PatternInfo -> a -> Pattern' a
forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
i a
x
    (DotP _ u :: Term
u) -> PatternInfo -> Term -> Pattern' a
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
i Term
u
    (ConP c :: ConHead
c (ConPatternInfo _ r :: Bool
r ft :: Bool
ft b :: Maybe (Arg Type)
b l :: Bool
l) ps :: [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 _ q :: QName
q ps :: [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 _ l :: 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 _ t :: Term
t u :: Term
u x :: 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 IdS p :: DeBruijnPattern
p = DeBruijnPattern
p
  applySubst rho :: Substitution' DeBruijnPattern
rho p :: DeBruijnPattern
p = case DeBruijnPattern
p of
    VarP i :: PatternInfo
i x :: 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 i :: PatternInfo
i u :: 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 c :: ConHead
c ci :: ConPatternInfo
ci ps :: 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 i :: PatternInfo
i q :: QName
q ps :: 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 i :: PatternInfo
i x :: Literal
x     -> DeBruijnPattern
p
    ProjP{}      -> DeBruijnPattern
p
    IApplyP i :: PatternInfo
i t :: Term
t u :: Term
u x :: 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 _ _ _ y :: 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  _ y :: 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
forall a. HasCallStack => a
__IMPOSSIBLE__
    where
      useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern
      useName :: String -> DeBruijnPattern -> DeBruijnPattern
useName n :: String
n (VarP o :: PatternInfo
o x :: 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 _ x :: DeBruijnPattern
x = DeBruijnPattern
x

instance Subst Term Range where
  applySubst :: Substitution' Term -> Range -> Range
applySubst _ = 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 prop :: Maybe QName
prop d :: QName
d r :: Arg QName
r _ lams :: ProjLams
lams) o :: ProjOrigin
o rel :: Relevance
rel args :: 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).
    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 (pars :: [Arg String]
pars, Arg i :: ArgInfo
i y :: 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 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 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
          (pars' :: [Arg String]
pars', args' :: 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 ai :: ArgInfo
ai x :: 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 (-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 0 t :: Type
t = Telescope -> Type -> TelView
forall a. Tele (Dom a) -> a -> TelV a
TelV Telescope
forall a. Tele a
EmptyTel Type
t
telView'UpTo n :: Int
n t :: Type
t = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
  Pi a :: Dom Type
a b :: 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
- 1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b)
  _       -> 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 a :: Dom a
a x :: String
x (TelV tel :: Tele (Dom a)
tel t :: 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' f :: Name -> a
f []     t :: Dom Type
t = []
bindsToTel' f :: Name -> a
f (x :: Name
x:xs :: [Name]
xs) t :: 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 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 []       t :: Type
t = Telescope
forall a. Tele a
EmptyTel
namedBindsToTel (x :: NamedArg Name
x : xs :: [NamedArg Name]
xs) t :: 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 1 Type
t)

domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName :: NamedArg Name -> Dom' Term ()
domFromNamedArgName x :: 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 Nothing x :: 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 x :: 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 b :: 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 a :: Arg String
a v :: 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' reAbs :: Abs Type -> Abs Type
reAbs = Telescope -> Type -> Type
telePi where
  telePi :: Telescope -> Type -> Type
telePi EmptyTel          t :: Type
t = Type
t
  telePi (ExtendTel u :: Dom Type
u tel :: Abs Telescope
tel) t :: 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 EmptyTel t :: Type
t = Type
t
telePiVisible (ExtendTel u :: Dom Type
u tel :: Abs Telescope
tel) t :: 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 x :: String
x t' :: 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  EmptyTel         t :: Term
t = Term
t
teleLam (ExtendTel u :: Dom Type
u tel :: Abs Telescope
tel) t :: 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 tel :: [Dom' Term (String, Type)]
tel t :: 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 = (x :: 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
t [Dom' Term (String, Type)]
tel

instance TeleNoAbs Telescope where
  teleNoAbs :: Telescope -> Term -> Term
teleNoAbs tel :: 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 _ []                         = [Dom Type] -> Maybe [Dom Type]
forall (m :: * -> *) a. Monad m => a -> m a
return []
typeArgsWithTel (ExtendTel dom :: Dom Type
dom tel :: Abs Telescope
tel) (v :: Term
v : vs :: [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{} (_:_)             = 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 cl :: 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' Term -> PlusLevel' Term -> Ordering
compare (Plus n :: Integer
n a :: LevelAtom' Term
a) (Plus m :: Integer
m b :: 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 x :: Int
x vs :: Elims
vs   == :: Term -> Term -> Bool
== Var x' :: Int
x' vs' :: 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 h :: ArgInfo
h v :: Abs Term
v    == Lam h' :: ArgInfo
h' v' :: 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 l :: Literal
l      == Lit l' :: Literal
l'       = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
  Def x :: QName
x vs :: Elims
vs   == Def x' :: QName
x' vs' :: 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 x :: ConHead
x _ vs :: Elims
vs == Con x' :: ConHead
x' _ vs' :: 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 a :: Dom Type
a b :: Abs Type
b     == Pi a' :: Dom Type
a' b' :: 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 s :: Sort
s     == Sort s' :: Sort
s'      = Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s'
  Level l :: Level
l    == Level l' :: Level
l'     = Level
l Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Level
l'
  MetaV m :: MetaId
m vs :: Elims
vs == MetaV m' :: MetaId
m' vs' :: 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 _ == DontCare _   = Bool
True
  Dummy{}    == Dummy{}      = Bool
True
  _          == _            = Bool
False

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

instance Ord Term where
  Var a :: Int
a b :: Elims
b    compare :: Term -> Term -> Ordering
`compare` Var x :: Int
x y :: 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` _          = Ordering
LT
  _          `compare` Var{}      = Ordering
GT
  Def a :: QName
a b :: Elims
b    `compare` Def x :: QName
x y :: 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` _          = Ordering
LT
  _          `compare` Def{}      = Ordering
GT
  Con a :: ConHead
a _ b :: Elims
b  `compare` Con x :: ConHead
x _ y :: 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` _          = Ordering
LT
  _          `compare` Con{}      = Ordering
GT
  Lit a :: Literal
a      `compare` Lit x :: Literal
x      = Literal -> Literal -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Literal
a Literal
x
  Lit{}      `compare` _          = Ordering
LT
  _          `compare` Lit{}      = Ordering
GT
  Lam a :: ArgInfo
a b :: Abs Term
b    `compare` Lam x :: ArgInfo
x y :: 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` _          = Ordering
LT
  _          `compare` Lam{}      = Ordering
GT
  Pi a :: Dom Type
a b :: Abs Type
b     `compare` Pi x :: Dom Type
x y :: 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` _          = Ordering
LT
  _          `compare` Pi{}       = Ordering
GT
  Sort a :: Sort
a     `compare` Sort x :: Sort
x     = Sort -> Sort -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Sort
a Sort
x
  Sort{}     `compare` _          = Ordering
LT
  _          `compare` Sort{}     = Ordering
GT
  Level a :: Level
a    `compare` Level x :: Level
x    = Level -> Level -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Level
a Level
x
  Level{}    `compare` _          = Ordering
LT
  _          `compare` Level{}    = Ordering
GT
  MetaV a :: MetaId
a b :: Elims
b  `compare` MetaV x :: MetaId
x y :: 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` _          = Ordering
LT
  _          `compare` MetaV{}    = Ordering
GT
  DontCare{} `compare` DontCare{} = Ordering
EQ
  DontCare{} `compare` _          = Ordering
LT
  _          `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 _ a :: a
a == :: Abs a -> Abs a -> Bool
== NoAbs _ b :: a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b  -- no need to raise if both are NoAbs
  a :: Abs a
a         == b :: 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 _ a :: a
a compare :: Abs a -> Abs a -> Ordering
`compare` NoAbs _ b :: 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
  a :: Abs a
a         `compare` b :: 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  a :: Arg a
a == :: Elim' a -> Elim' a -> Bool
== Apply  b :: Arg a
b = Arg a
a Arg a -> Arg a -> Bool
forall a. Eq a => a -> a -> Bool
== Arg a
b
  Proj _ x :: QName
x == Proj _ y :: QName
y = QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
y
  IApply x :: a
x y :: a
y r :: a
r == IApply x' :: a
x' y' :: a
y' r' :: 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'
  _ == _ = Bool
False

instance (Subst t a, Ord a) => Ord (Elim' a) where
  Apply  a :: Arg a
a compare :: Elim' a -> Elim' a -> Ordering
`compare` Apply  b :: Arg a
b = Arg a
a Arg a -> Arg a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Arg a
b
  Proj _ x :: QName
x `compare` Proj _ y :: QName
y = QName
x QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QName
y
  IApply x :: a
x y :: a
y r :: a
r `compare` IApply x' :: a
x' y' :: a
y' r' :: 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` _        = Ordering
LT
  _        `compare` Apply{}  = Ordering
GT
  Proj{}   `compare` _        = Ordering
LT
  _        `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' univInf :: Maybe Sort
univInf (Type l :: 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' univInf :: Maybe Sort
univInf (Prop l :: 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' univInf :: Maybe Sort
univInf Inf      = Maybe Sort
univInf
univSort' univInf :: Maybe Sort
univInf s :: Sort
s        = Maybe Sort
forall a. Maybe a
Nothing

univSort :: Maybe Sort -> Sort -> Sort
univSort :: Maybe Sort -> Sort -> Sort
univSort univInf :: Maybe Sort
univInf s :: 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' a :: Sort
a b :: Sort
b = case (Sort
a, Sort
b) of
  (Inf           , _            ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
  (_             , Inf          ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
  (Type a :: Level
a , Type b :: 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
  (SizeUniv      , b :: Sort
b            ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
b
  (_             , SizeUniv     ) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
SizeUniv
  (Prop a :: Level
a , Type b :: 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 a :: Level
a , Prop b :: 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 a :: Level
a , Prop b :: 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
  (a :: Sort
a             , b :: Sort
b            ) -> Maybe Sort
forall a. Maybe a
Nothing

funSort :: Sort -> Sort -> Sort
funSort :: Sort -> Sort -> Sort
funSort a :: Sort
a b :: 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' a :: Dom Type
a      (NoAbs _ b :: Sort
b) = Sort -> Sort -> Maybe Sort
funSort' (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) Sort
b
piSort' a :: Dom Type
a bAbs :: Abs Sort
bAbs@(Abs   _ b :: Sort
b) = case Int -> Sort -> Maybe (FlexRig' ())
forall a. Free a => Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn 0 Sort
b of
  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 o :: FlexRig' ()
o -> case FlexRig' ()
o of
    StronglyRigid -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
    Unguarded     -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
forall t. Sort' t
Inf
    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 a :: Dom Type
a b :: Abs Sort
b = case Dom Type -> Abs Sort -> Maybe Sort
piSort' Dom Type
a Abs Sort
b of
  Just s :: Sort
s -> Sort
s
  Nothing | NoAbs _ b' :: 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' Term] -> Level
levelMax n0 :: Integer
n0 as0 :: [PlusLevel' Term]
as0 = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n [PlusLevel' Term]
as
  where
    -- step 1: flatten nested @Level@ expressions in @LevelAtom@s
    Max n1 :: Integer
n1 as1 :: [PlusLevel' Term]
as1 = Level -> Level
expandLevel (Level -> Level) -> Level -> Level
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n0 [PlusLevel' Term]
as0
    -- step 2: remove subsumed @PlusLevel@s
    as2 :: [PlusLevel' Term]
as2       = [PlusLevel' Term] -> [PlusLevel' Term]
forall t. Eq (LevelAtom' t) => [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [PlusLevel' Term]
as1
    -- step 3: sort remaining @PlusLevel@s
    as :: [PlusLevel' Term]
as        = [PlusLevel' Term] -> [PlusLevel' Term]
forall a. Ord a => [a] -> [a]
List.sort [PlusLevel' Term]
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
$ 0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [ Integer
n | Plus n :: Integer
n _ <- [PlusLevel' Term]
as ]
    n :: Integer
n | Integer
n1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
greatestB = Integer
n1
      | Bool
otherwise      = 0

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

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

    expandPlus :: PlusLevel -> Level
    expandPlus :: PlusLevel' Term -> Level
expandPlus (Plus m :: Integer
m l :: 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 l :: LevelAtom' Term
l = case LevelAtom' Term
l of
      BlockedLevel _ v :: Term
v -> Term -> Level
expandTm Term
v
      NeutralLevel _ v :: Term
v -> Term -> Level
expandTm Term
v
      UnreducedLevel v :: Term
v -> Term -> Level
expandTm Term
v
      MetaLevel{}      -> Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max 0 [Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus 0 LevelAtom' Term
l]
      where
        expandTm :: Term -> Level
expandTm (Level l :: Level
l)       = Level -> Level
expandLevel Level
l
        expandTm (Sort (Type l :: Level
l)) = Level -> Level
expandLevel Level
l -- TODO: get rid of this horrible hack!
        expandTm v :: Term
v               = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max 0 [Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus 0 LevelAtom' Term
l]

    removeSubsumed :: [PlusLevel' t] -> [PlusLevel' t]
removeSubsumed [] = []
    removeSubsumed (Plus n :: Integer
n a :: LevelAtom' t
a : bs :: [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 _ a' :: 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 m :: Integer
m a' :: 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 m :: Integer
m as :: [PlusLevel' Term]
as) (Max n :: Integer
n bs :: [PlusLevel' Term]
bs) = Integer -> [PlusLevel' Term] -> Level
levelMax (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
m Integer
n) ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ [PlusLevel' Term]
as [PlusLevel' Term] -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. [a] -> [a] -> [a]
++ [PlusLevel' Term]
bs

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

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