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

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

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

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

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

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

import Debug.Trace (trace)

import Agda.Interaction.Options

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

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

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

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

import Agda.Utils.Impossible


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

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

instance Apply BraveTerm where
  applyE :: BraveTerm -> Elims -> BraveTerm
applyE = forall t.
(Coercible Term t, Apply t, EndoSubst t) =>
(Empty -> Term -> Elims -> Term) -> t -> Elims -> t
applyTermE (\ Empty
_ Term
t Elims
es ->  [Char] -> Elims -> Term
Dummy [Char]
"applyE" (forall a. Arg a -> Elim' a
Apply (forall a. a -> Arg a
defaultArg Term
t) forall a. a -> [a] -> [a]
: Elims
es))

-- | If @v@ is a record or constructed value, @canProject f v@
--   returns its field @f@.
canProject :: QName -> Term -> Maybe (Arg Term)
canProject :: QName -> Term -> Maybe (Arg Term)
canProject QName
f Term
v =
  case Term
v of
    -- Andreas, 2022-06-10, issue #5922: also unfold data projections
    -- (not just record projections).
    (Con (ConHead QName
_ DataOrRecord
_ Induction
_ [Arg QName]
fs) ConInfo
_ Elims
vs) -> do
      (Arg QName
fld, Int
i) <- forall a. (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex ((QName
fforall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg QName]
fs
      -- Jesper, 2019-10-17: dont unfold irrelevant projections
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ 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!).
      forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg QName
fld) forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a. Elim' a -> Maybe (Arg a)
isApplyElim forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. [a] -> Maybe a
listToMaybe (forall a. Int -> [a] -> [a]
drop Int
i Elims
vs)
    Term
_ -> forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc, funCovering :: Defn -> [Clause]
funCovering = [Clause]
cov, funInv :: Defn -> FunctionInverse
funInv = FunctionInverse
inv
            , funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Maybe ExtLamInfo
extLam
            , funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p0 } ->
      case Projection
p0 forall t. Apply t => t -> Args -> t
`apply` Args
args of
        p :: Projection
p@Projection{ projIndex :: Projection -> Int
projIndex = Int
n }
          | Int
n forall a. Ord a => a -> a -> Bool
< Int
0     -> Defn
d { funProjection :: Either ProjectionLikenessMissing Projection
funProjection = forall a. HasCallStack => a
__IMPOSSIBLE__ } -- TODO (#3123): we actually get here!
          -- case: applied only to parameters
          | Int
n forall a. Ord a => a -> a -> Bool
> Int
0     -> Defn
d { funProjection :: Either ProjectionLikenessMissing Projection
funProjection = forall a b. b -> Either a b
Right Projection
p }
          -- case: applied also to record value (n == 0)
          | Bool
otherwise ->
              Defn
d { funClauses :: [Clause]
funClauses        = forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args'
                , funCompiled :: Maybe CompiledClauses
funCompiled       = forall t. Apply t => t -> Args -> t
apply Maybe CompiledClauses
cc Args
args'
                , funCovering :: [Clause]
funCovering       = forall t. Apply t => t -> Args -> t
apply [Clause]
cov Args
args'
                , funInv :: FunctionInverse
funInv            = forall t. Apply t => t -> Args -> t
apply FunctionInverse
inv Args
args'
                , funProjection :: Either ProjectionLikenessMissing Projection
funProjection     = if Bool
isVar0 then forall a b. b -> Either a b
Right Projection
p{ projIndex :: Int
projIndex = Int
0 } else forall a b. a -> Either a b
Left ProjectionLikenessMissing
MaybeProjection
                , funExtLam :: Maybe ExtLamInfo
funExtLam         = (System -> System) -> ExtLamInfo -> ExtLamInfo
modifySystem (\ System
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ExtLamInfo
extLam
                }
              where
                larg :: Arg Term
larg  = forall a. a -> [a] -> a
last1 Arg Term
arg1 Args
args1 -- the record value
                args' :: Args
args' = [Arg Term
larg]
                isVar0 :: Bool
isVar0 = case forall e. Arg e -> e
unArg Arg Term
larg of Var Int
0 [] -> Bool
True; Term
_ -> Bool
False

    Datatype{ dataPars :: Defn -> Int
dataPars = Int
np, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl } ->
      Defn
d { dataPars :: Int
dataPars = Int
np forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Args
args
        , dataClause :: Maybe Clause
dataClause     = 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 forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Args
args
        , recClause :: Maybe Clause
recClause = forall t. Apply t => t -> Args -> t
apply Maybe Clause
cl Args
args, recTel :: Telescope
recTel = 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 forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Args
args }
    Primitive{ primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs } ->
      Defn
d { primClauses :: [Clause]
primClauses = forall t. Apply t => t -> Args -> t
apply [Clause]
cs Args
args }
    PrimitiveSort{} -> Defn
d

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

instance Apply PrimFun where
  apply :: PrimFun -> Args -> PrimFun
apply (PrimFun QName
x Int
ar Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def) Args
args = QName
-> Int
-> (Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
PrimFun QName
x (Int
ar forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Int
size Args
args) forall a b. (a -> b) -> a -> b
$ \ Args
vs -> Args -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
def (Args
args forall a. [a] -> [a] -> [a]
++ Args
vs)
  applyE :: PrimFun -> Elims -> PrimFun
applyE PrimFun
t Elims
es = forall t. Apply t => t -> Args -> t
apply PrimFun
t forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Apply Permutation where
  -- The permutation must start with [0..m - 1]
  -- NB: section (- m) not possible (unary minus), hence (flip (-) m)
  apply :: Permutation -> Args -> Permutation
apply (Perm Int
n [Int]
xs) Args
args = Int -> [Int] -> Permutation
Perm (Int
n forall a. Num a => a -> a -> a
- Int
m) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> b -> a -> c
flip (-) Int
m) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
m [Int]
xs
    where
      m :: Int
m = forall a. Sized a => a -> Int
size Args
args

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

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

-- | @(x:A)->B(x) `piApply` [u] = B(u)@
--
--   Precondition: The type must contain the right number of pis without
--   having to perform any reduction.
--
--   @piApply@ is potentially unsafe, the monadic 'piApplyM' is preferable.
piApply :: Type -> Args -> Type
piApply :: Type -> Args -> Type
piApply Type
t []                      = Type
t
piApply (El Sort
_ (Pi  Dom Type
_ Abs Type
b)) (Arg Term
a:Args
args) = forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Type
b (forall e. Arg e -> e
unArg Arg Term
a) Type -> Args -> Type
`piApply` Args
args
piApply Type
t Args
args                    =
  forall a. [Char] -> a -> a
trace ([Char]
"piApply t = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t forall a. [a] -> [a] -> [a]
++ [Char]
"\n  args = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Args
args) forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

instance Abstract Projection where
  abstract :: Telescope -> Projection -> Projection
abstract Telescope
tel Projection
p = Projection
p
    { projIndex :: Int
projIndex = forall a. Sized a => a -> Int
size Telescope
tel forall a. Num a => a -> a -> a
+ Projection -> Int
projIndex Projection
p
    , projLams :: ProjLams
projLams  = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel forall a b. (a -> b) -> a -> b
$ Projection -> ProjLams
projLams Projection
p
    }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance (Coercible a Term, Subst a) => Subst (Sort' a) where
  type SubstArg (Sort' a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a
applySubst Substitution' (SubstArg (Sort' a))
rho = \case
    Type Level' a
n     -> forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Level' a
n
    Prop Level' a
n     -> forall t. Level' t -> Sort' t
Prop forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Level' a
n
    Inf IsFibrant
f Integer
n    -> forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n
    SSet Level' a
n     -> forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Level' a
n
    Sort' a
SizeUniv   -> forall t. Sort' t
SizeUniv
    Sort' a
LockUniv   -> forall t. Sort' t
LockUniv
    Sort' a
IntervalUniv -> forall t. Sort' t
IntervalUniv
    PiSort Dom' a a
a Sort' a
s1 Abs (Sort' a)
s2 -> coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ Dom Term -> Sort -> Abs Sort -> Sort
piSort (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Dom' a a
a) (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s1) (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Abs (Sort' a)
s2)
    FunSort Sort' a
s1 Sort' a
s2 -> coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
funSort (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s1) (coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s2)
    UnivSort Sort' a
s -> coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ Sort -> Sort
univSort forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub Sort' a
s
    MetaS MetaId
x [Elim' a]
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub [Elim' a]
es
    DefS QName
d [Elim' a]
es  -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d forall a b. (a -> b) -> a -> b
$ forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub [Elim' a]
es
    s :: Sort' a
s@DummyS{} -> Sort' a
s
    where
      sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
      sub :: forall b. (Subst b, SubstArg a ~ SubstArg b) => b -> b
sub b
x = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' a))
rho b
x

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

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

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

instance Subst ConPatternInfo where
  type SubstArg ConPatternInfo = Term
  applySubst :: Substitution' (SubstArg ConPatternInfo)
-> ConPatternInfo -> ConPatternInfo
applySubst Substitution' (SubstArg ConPatternInfo)
rho ConPatternInfo
i = ConPatternInfo
i{ conPType :: Maybe (Arg Type)
conPType = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg ConPatternInfo)
rho forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
i }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance Subst Constraint where
  type SubstArg Constraint = Term

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

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

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

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

instance Subst a => Subst (Arg a) where
  type SubstArg (Arg a) = SubstArg a
  applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a
applySubst Substitution' (SubstArg (Arg a))
IdS Arg a
arg = Arg a
arg
  applySubst Substitution' (SubstArg (Arg a))
rho Arg a
arg = forall a. LensFreeVariables a => FreeVariables -> a -> a
setFreeVariables FreeVariables
unknownFreeVariables forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg a))
rho) Arg a
arg

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

-- ** Telescope view of a type

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

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

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

-- | @telView'UpTo n t@ takes off the first @n@ exposed function types of @t@.
-- Takes off all (exposed ones) if @n < 0@.
telView'UpTo :: Int -> Type -> TelView
telView'UpTo :: Int -> Type -> TelView
telView'UpTo Int
0 Type
t = forall a. Tele (Dom a) -> a -> TelV a
TelV forall a. Tele a
EmptyTel Type
t
telView'UpTo Int
n Type
t = case forall t a. Type'' t a -> a
unEl Type
t of
  Pi Dom Type
a Abs Type
b  -> forall a. Dom a -> [Char] -> TelV a -> TelV a
absV Dom Type
a (forall a. Abs a -> [Char]
absName Abs Type
b) forall a b. (a -> b) -> a -> b
$ Int -> Type -> TelView
telView'UpTo (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Type
b)
  Term
_       -> forall a. Tele (Dom a) -> a -> TelV a
TelV forall a. Tele a
EmptyTel Type
t

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


-- ** Creating telescopes from lists of types

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

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

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

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

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

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

domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName :: NamedArg Name -> Dom ()
domFromNamedArgName NamedArg Name
x = () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. NamedArg a -> Dom a
domFromNamedArg (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Name -> Named NamedName Name
forceName NamedArg Name
x)
  where
    -- If no explicit name is given we use the bound name for the label.
    forceName :: Named NamedName Name -> Named NamedName Name
forceName (Named Maybe NamedName
Nothing Name
x) = forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange Name
x) forall a b. (a -> b) -> a -> b
$ Name -> [Char]
nameToArgName Name
x) Name
x
    forceName Named NamedName Name
x = Named NamedName Name
x

-- ** Abstracting in terms and types

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

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

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

lamView :: Term -> ([Arg ArgName], Term)
lamView :: Term -> ([Arg [Char]], Term)
lamView (Lam ArgInfo
h (Abs   [Char]
x Term
b)) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h [Char]
x forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
lamView Term
b
lamView (Lam ArgInfo
h (NoAbs [Char]
x Term
b)) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
h [Char]
x forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ Term -> ([Arg [Char]], Term)
lamView (forall a. Subst a => Int -> a -> a
raise Int
1 Term
b)
lamView Term
t                   = ([], Term
t)

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

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

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

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

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

telePiVisible :: Telescope -> Type -> Type
telePiVisible :: Telescope -> Type -> Type
telePiVisible Telescope
EmptyTel Type
t = Type
t
telePiVisible (ExtendTel Dom Type
u Abs Telescope
tel) Type
t
    -- If u is not declared visible and b can be strengthened, skip quantification of u.
    | forall a. LensHiding a => a -> Bool
notVisible Dom Type
u, NoAbs [Char]
x Type
t' <- Abs Type
b' = Type
t'
    -- Otherwise, include quantification over u.
    | Bool
otherwise = forall t a. Sort' t -> a -> Type'' t a
El (Dom Type -> Abs Type -> Sort
mkPiSort Dom Type
u Abs Type
b) 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 forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (Telescope -> Type -> Type
`telePiVisible` Type
t)
    b' :: Abs Type
b' = forall a. (Subst a, Free a) => Abs a -> Abs a
reAbs Abs Type
b

-- | Abstract over a telescope in a term, producing lambdas.
--   Dumb abstraction: Always produces 'Abs', never 'NoAbs'.
--
--   The implementation is sound because 'Telescope' does not use 'NoAbs'.
teleLam :: Telescope -> Term -> Term
teleLam :: Telescope -> Term -> Term
teleLam  Telescope
EmptyTel         Term
t = Term
t
teleLam (ExtendTel Dom Type
u Abs Telescope
tel) Term
t = ArgInfo -> Abs Term -> Term
Lam (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
u) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope -> Term -> Term
teleLam Term
t 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 :: ListTel -> Term -> Term
teleNoAbs ListTel
tel Term
t = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = ([Char]
x, Type
_)} -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
ai forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
NoAbs [Char]
x) Term
t ListTel
tel

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


-- ** Telescope typing

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

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

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

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

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

deriving instance Eq Substitution
deriving instance Ord Substitution

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

deriving instance (Subst a, Eq a)  => Eq  (Tele a)
deriving instance (Subst a, Ord a) => Ord (Tele a)

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

deriving instance Eq Section

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

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

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

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

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

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

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

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

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

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

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

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

deriving instance Ord a => Ord (Dom a)

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

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


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

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

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

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

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

-- | A sort can either be small (Set l, Prop l, Size, ...)  or large
--   (Setω n).
data SizeOfSort
  = SmallSort IsFibrant
  | LargeSort IsFibrant Integer

-- | Returns @Left blocker@ for unknown (blocked) sorts, and otherwise
--   returns @Right s@ where @s@ indicates the size and fibrancy.
sizeOfSort :: Sort -> Either Blocker SizeOfSort
sizeOfSort :: Sort -> Either Blocker SizeOfSort
sizeOfSort Type{}       = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Prop{}       = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Sort
SizeUniv     = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Sort
LockUniv     = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsFibrant
sizeOfSort Sort
IntervalUniv = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsStrict
sizeOfSort (Inf IsFibrant
f Integer
n)    = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> SizeOfSort
LargeSort IsFibrant
f Integer
n
sizeOfSort SSet{}       = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ IsFibrant -> SizeOfSort
SmallSort IsFibrant
IsStrict
sizeOfSort (MetaS MetaId
m Elims
_)  = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
sizeOfSort FunSort{}    = forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort PiSort{}     = forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort UnivSort{}   = forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort DefS{}       = forall a b. a -> Either a b
Left Blocker
neverUnblock
sizeOfSort DummyS{}     = forall a b. a -> Either a b
Left Blocker
neverUnblock

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

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

-- | Compute the sort of a function type from the sorts of its
--   domain and codomain.
funSort' :: Sort -> Sort -> Either Blocker Sort
funSort' :: Sort -> Sort -> Either Blocker Sort
funSort' Sort
a Sort
b = case (Sort
a, Sort
b) of
  (Type Level
a        , Type Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Prop Level
a        , Type Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Type Level
a        , Prop Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
Prop forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Prop Level
a        , Prop Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
Prop forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (SSet Level
a        , SSet Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Type Level
a        , SSet Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (SSet Level
a        , Type Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (SSet Level
a        , Prop Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Prop Level
a        , SSet Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level -> Level -> Level
levelLub Level
a Level
b
  (Inf IsFibrant
af Integer
m      , Sort
b            ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SmallSort IsFibrant
bf   -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) Integer
m
    LargeSort IsFibrant
bf Integer
n -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
max Integer
m Integer
n
  (Sort
a             , Inf IsFibrant
bf Integer
n     ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SmallSort IsFibrant
af   -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) Integer
n
    LargeSort IsFibrant
af Integer
m -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
af IsFibrant
bf) forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
max Integer
m Integer
n
  (Sort
LockUniv      , Sort
b            ) -> forall a b. b -> Either a b
Right Sort
b
  -- No functions into lock types
  (Sort
a             , Sort
LockUniv     ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  -- @IntervalUniv@ behaves like @SSet@, but functions into @Type@ land in @Type@
  (Sort
IntervalUniv  , Sort
IntervalUniv ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
  (Sort
IntervalUniv  , SSet Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level
b
  (Sort
IntervalUniv  , Type Level
b       ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ Level
b
  (Sort
IntervalUniv  , Sort
_            ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Type Level
a        , Sort
IntervalUniv ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level
a
  (SSet Level
a        , Sort
IntervalUniv ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ Level
a
  (Sort
_             , Sort
IntervalUniv ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
SizeUniv      , Sort
b            ) -> forall a b. b -> Either a b
Right Sort
b
  (Sort
a             , Sort
SizeUniv     ) -> Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    SmallSort{} -> forall a b. b -> Either a b
Right forall t. Sort' t
SizeUniv
    LargeSort{} -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (MetaS MetaId
m Elims
_     , Sort
_            ) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
  (Sort
_             , MetaS MetaId
m Elims
_    ) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
  (FunSort{}     , Sort
_            ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , FunSort{}    ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (PiSort{}      , Sort
_            ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , PiSort{}     ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (UnivSort{}    , Sort
_            ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , UnivSort{}   ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (DefS{}        , Sort
_            ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , DefS{}       ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (DummyS{}      , Sort
_            ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock
  (Sort
_             , DummyS{}     ) -> forall a b. a -> Either a b
Left Blocker
neverUnblock

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

-- | Compute the sort of a pi type from the sorts of its domain
--   and codomain.
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
piSort' Dom Term
a Sort
s1       (NoAbs [Char]
_ Sort
s2) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 Sort
s2
piSort' Dom Term
a Sort
s1 s2Abs :: Abs Sort
s2Abs@(Abs   [Char]
_ Sort
s2) = case forall a. Free a => Int -> a -> Maybe FlexRig
flexRigOccurrenceIn Int
0 Sort
s2 of
  Maybe FlexRig
Nothing -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Impossible -> Abs a -> a
noabsApp forall a. HasCallStack => a
__IMPOSSIBLE__ Abs Sort
s2Abs
  Just FlexRig
o  -> case (Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s1 , Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s2) of
    (Right (SmallSort IsFibrant
f1) , Right (SmallSort IsFibrant
f2)) -> case FlexRig
o of
      FlexRig
StronglyRigid -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
0
      FlexRig
Unguarded     -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
0
      FlexRig
WeaklyRigid   -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
0
      Flexible MetaSet
ms   -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
    (Right (LargeSort IsFibrant
f1 Integer
n) , Right (SmallSort IsFibrant
f2)) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf (IsFibrant -> IsFibrant -> IsFibrant
fibrantLub IsFibrant
f1 IsFibrant
f2) Integer
n
    (Either Blocker SizeOfSort
_                     , Right LargeSort{}    ) -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- large sorts cannot depend on variables
    (Left Blocker
blocker          , Right SizeOfSort
_              ) -> forall a b. a -> Either a b
Left Blocker
blocker
    (Right SizeOfSort
_               , Left Blocker
blocker         ) -> forall a b. a -> Either a b
Left Blocker
blocker
    (Left Blocker
blocker1         , Left Blocker
blocker2        ) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
blocker1 Blocker
blocker2

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

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

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

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

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

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

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

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

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

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

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