module Agda.TypeChecking.Substitute.Class where

import Control.Arrow ((***), second)


import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute.DeBruijn

import Agda.Utils.Empty
import Agda.Utils.List

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Application
---------------------------------------------------------------------------

-- | Apply something to a bunch of arguments.
--   Preserves blocking tags (application can never resolve blocking).
class Apply t where
  apply  :: t -> Args -> t
  applyE :: t -> Elims -> t

  apply t
t Args
args = t -> Elims -> t
forall t. Apply t => t -> Elims -> t
applyE t
t (Elims -> t) -> Elims -> t
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args
  -- Andreas, 2018-06-18, issue #3136
  -- This default instance should be removed to get more precise
  -- crash locations (raise the IMPOSSIBLE in a more specific place).
  -- applyE t es  = apply  t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
    -- precondition: all @es@ are @Apply@s

-- | Apply to some default arguments.
applys :: Apply t => t -> [Term] -> t
applys :: t -> [Term] -> t
applys t
t [Term]
vs = t -> Args -> t
forall t. Apply t => t -> Args -> t
apply t
t (Args -> t) -> Args -> t
forall a b. (a -> b) -> a -> b
$ (Term -> Arg Term) -> [Term] -> Args
forall a b. (a -> b) -> [a] -> [b]
map Term -> Arg Term
forall a. a -> Arg a
defaultArg [Term]
vs

-- | Apply to a single default argument.
apply1 :: Apply t => t -> Term -> t
apply1 :: t -> Term -> t
apply1 t
t Term
u = t -> [Term] -> t
forall t. Apply t => t -> [Term] -> t
applys t
t [ Term
u ]

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

-- | @(abstract args v) `apply` args --> v[args]@.
class Abstract t where
  abstract :: Telescope -> t -> t

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

-- | Apply a substitution.

-- For terms:
--
--  Γ ⊢ ρ : Δ
--  Δ ⊢ t : A
-- -----------
-- Γ ⊢ tρ : Aρ

class DeBruijn (SubstArg a) => Subst a where
  type SubstArg a
  applySubst :: Substitution' (SubstArg a) -> a -> a

  default applySubst :: (a ~ f b, Functor f, Subst b, SubstArg a ~ SubstArg b) => Substitution' (SubstArg a) -> a -> a
  applySubst Substitution' (SubstArg a)
rho = (b -> b) -> f b -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution' (SubstArg b) -> b -> b
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg a)
Substitution' (SubstArg b)
rho)

-- | Simple constraint alias for a `Subst` instance `a` with arg type `t`.
type SubstWith t a = (Subst a, SubstArg a ~ t)

-- | `Subst` instance whose agument type is itself
type EndoSubst a = SubstWith a a

-- | `Subst` instance whose argument type is `Term`
type TermSubst a = SubstWith Term a

-- | Raise de Bruijn index, i.e. weakening
raise :: Subst a => Nat -> a -> a
raise :: Nat -> a -> a
raise = Nat -> Nat -> a -> a
forall a. Subst a => Nat -> Nat -> a -> a
raiseFrom Nat
0

raiseFrom :: Subst a => Nat -> Nat -> a -> a
raiseFrom :: Nat -> Nat -> a -> a
raiseFrom Nat
n Nat
k = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Nat -> Substitution' (SubstArg a)
forall a. Nat -> Nat -> Substitution' a
raiseFromS Nat
n Nat
k)

-- | Replace de Bruijn index i by a 'Term' in something.
subst :: Subst a => Int -> SubstArg a -> a -> a
subst :: Nat -> SubstArg a -> a -> a
subst Nat
i SubstArg a
u = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' (SubstArg a) -> a -> a)
-> Substitution' (SubstArg a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Nat -> SubstArg a -> Substitution' (SubstArg a)
forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
i SubstArg a
u

strengthen :: Subst a => Impossible -> a -> a
strengthen :: Impossible -> a -> a
strengthen Impossible
err = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> [Maybe (SubstArg a)] -> Substitution' (SubstArg a)
forall a. DeBruijn a => Impossible -> [Maybe a] -> Substitution' a
compactS Impossible
err [Maybe (SubstArg a)
forall a. Maybe a
Nothing])

-- | Replace what is now de Bruijn index 0, but go under n binders.
--   @substUnder n u == subst n (raise n u)@.
substUnder :: Subst a => Nat -> SubstArg a -> a -> a
substUnder :: Nat -> SubstArg a -> a -> a
substUnder Nat
n SubstArg a
u = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
n (Nat -> SubstArg a -> Substitution' (SubstArg a)
forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
0 SubstArg a
u))

-- ** Identity instances

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

---------------------------------------------------------------------------
-- * Explicit substitutions
---------------------------------------------------------------------------

-- See Syntax.Internal for the definition.

idS :: Substitution' a
idS :: Substitution' a
idS = Substitution' a
forall a. Substitution' a
IdS

wkS :: Int -> Substitution' a -> Substitution' a
wkS :: Nat -> Substitution' a -> Substitution' a
wkS Nat
0 Substitution' a
rho        = Substitution' a
rho
wkS Nat
n (Wk Nat
m Substitution' a
rho) = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
Wk (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m) Substitution' a
rho
wkS Nat
n (EmptyS Impossible
err) = Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Impossible
err
wkS Nat
n Substitution' a
rho        = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
Wk Nat
n Substitution' a
rho

raiseS :: Int -> Substitution' a
raiseS :: Nat -> Substitution' a
raiseS Nat
n = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
n Substitution' a
forall a. Substitution' a
idS

consS :: DeBruijn a => a -> Substitution' a -> Substitution' a
consS :: a -> Substitution' a -> Substitution' a
consS a
t (Wk Nat
m Substitution' a
rho)
  | Just Nat
n <- a -> Maybe Nat
forall a. DeBruijn a => a -> Maybe Nat
deBruijnView a
t,
    Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
m = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 Substitution' a
rho)
consS a
u Substitution' a
rho = a -> Substitution' a -> Substitution' a
seq a
u (a
u a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' a
rho)

-- | To replace index @n@ by term @u@, do @applySubst (singletonS n u)@.
--   @
--               Γ, Δ ⊢ u : A
--    ---------------------------------
--    Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ
--   @
singletonS :: DeBruijn a => Int -> a -> Substitution' a
singletonS :: Nat -> a -> Substitution' a
singletonS Nat
n a
u = (Nat -> a) -> [Nat] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar [Nat
0..Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1] [a] -> Substitution' a -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# a -> Substitution' a -> Substitution' a
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS a
u (Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
n)
  -- ALT: foldl (\ s i -> deBruijnVar i `consS` s) (consS u $ raiseS n) $ downFrom n

-- | Single substitution without disturbing any deBruijn indices.
--   @
--             Γ, A, Δ ⊢ u : A
--    ---------------------------------
--    Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ
--   @
inplaceS :: EndoSubst a => Int -> a -> Substitution' a
inplaceS :: Nat -> a -> Substitution' a
inplaceS Nat
k a
u = Nat -> a -> Substitution' a
forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
k a
u Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) (Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
1)

-- | Lift a substitution under k binders.
liftS :: Int -> Substitution' a -> Substitution' a
liftS :: Nat -> Substitution' a -> Substitution' a
liftS Nat
0 Substitution' a
rho          = Substitution' a
rho
liftS Nat
k Substitution' a
IdS          = Substitution' a
forall a. Substitution' a
IdS
liftS Nat
k (Lift Nat
n Substitution' a
rho) = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
Lift (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
k) Substitution' a
rho
liftS Nat
k Substitution' a
rho          = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
Lift Nat
k Substitution' a
rho

-- | @
--         Γ ⊢ ρ : Δ, Ψ
--      -------------------
--      Γ ⊢ dropS |Ψ| ρ : Δ
--   @
dropS :: Int -> Substitution' a -> Substitution' a
dropS :: Nat -> Substitution' a -> Substitution' a
dropS Nat
0 Substitution' a
rho                = Substitution' a
rho
dropS Nat
n Substitution' a
IdS                = Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
n
dropS Nat
n (Wk Nat
m Substitution' a
rho)         = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
m (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
dropS Nat
n Substitution' a
rho)
dropS Nat
n (a
u :# Substitution' a
rho)         = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
dropS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
rho
dropS Nat
n (Strengthen Impossible
_ Substitution' a
rho) = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
dropS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
rho
dropS Nat
n (Lift Nat
0 Substitution' a
rho)       = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
dropS Nat
n (Lift Nat
m Substitution' a
rho)       = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1 (Substitution' a -> Substitution' a)
-> Substitution' a -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
dropS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Substitution' a -> Substitution' a)
-> Substitution' a -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
rho
dropS Nat
n (EmptyS Impossible
err)       = Impossible -> Substitution' a
forall a. Impossible -> a
throwImpossible Impossible
err

-- | @applySubst (ρ `composeS` σ) v == applySubst ρ (applySubst σ v)@
composeS :: EndoSubst a => Substitution' a -> Substitution' a -> Substitution' a
composeS :: Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho Substitution' a
IdS = Substitution' a
rho
composeS Substitution' a
IdS Substitution' a
sgm = Substitution' a
sgm
composeS Substitution' a
rho (EmptyS Impossible
err) = Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Impossible
err
composeS Substitution' a
rho (Wk Nat
n Substitution' a
sgm) = Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
dropS Nat
n Substitution' a
rho) Substitution' a
sgm
composeS Substitution' a
rho (a
u :# Substitution' a
sgm) = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' a
Substitution' (SubstArg a)
rho a
u a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho Substitution' a
sgm
composeS Substitution' a
rho (Strengthen Impossible
err Substitution' a
sgm) = Impossible -> Substitution' a -> Substitution' a
forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Impossible
err (Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho Substitution' a
sgm)
composeS Substitution' a
rho (Lift Nat
0 Substitution' a
sgm) = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
composeS (a
u :# Substitution' a
rho) (Lift Nat
n Substitution' a
sgm) = a
u a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
sgm)
composeS Substitution' a
rho (Lift Nat
n Substitution' a
sgm) = Substitution' a -> Nat -> a
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho Nat
0 a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1 (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
sgm))

-- If Γ ⊢ ρ : Δ, Θ then splitS |Θ| ρ = (σ, δ), with
--   Γ ⊢ σ : Δ
--   Γ ⊢ δ : Θσ
splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS :: Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS Nat
0 Substitution' a
rho                  = (Substitution' a
rho, Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Impossible
HasCallStack => Impossible
impossible)
splitS Nat
n (a
u :# Substitution' a
rho)           = (Substitution' a -> Substitution' a)
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (a
u a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:#) ((Substitution' a, Substitution' a)
 -> (Substitution' a, Substitution' a))
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
forall a.
Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
rho
splitS Nat
n (Strengthen Impossible
err Substitution' a
rho) = (Substitution' a -> Substitution' a)
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Impossible -> Substitution' a -> Substitution' a
forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Impossible
err) ((Substitution' a, Substitution' a)
 -> (Substitution' a, Substitution' a))
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
forall a.
Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
rho
splitS Nat
n (Lift Nat
0 Substitution' a
_)           = (Substitution' a, Substitution' a)
forall a. HasCallStack => a
__IMPOSSIBLE__
splitS Nat
n (Wk Nat
m Substitution' a
rho)           = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
m (Substitution' a -> Substitution' a)
-> (Substitution' a -> Substitution' a)
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
m ((Substitution' a, Substitution' a)
 -> (Substitution' a, Substitution' a))
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
forall a.
Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS Nat
n Substitution' a
rho
splitS Nat
n Substitution' a
IdS                  = (Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
n, Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
n (Substitution' a -> Substitution' a)
-> Substitution' a -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Impossible -> Substitution' a
forall a. Impossible -> Substitution' a
EmptyS Impossible
HasCallStack => Impossible
impossible)
splitS Nat
n (Lift Nat
m Substitution' a
rho)         = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS Nat
1 (Substitution' a -> Substitution' a)
-> (Substitution' a -> Substitution' a)
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 ((Substitution' a, Substitution' a)
 -> (Substitution' a, Substitution' a))
-> (Substitution' a, Substitution' a)
-> (Substitution' a, Substitution' a)
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a -> (Substitution' a, Substitution' a)
forall a.
Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) Substitution' a
rho)
splitS Nat
n (EmptyS Impossible
err)         = (Substitution' a, Substitution' a)
forall a. HasCallStack => a
__IMPOSSIBLE__

infixr 4 ++#

(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
[a]
us ++# :: [a] -> Substitution' a -> Substitution' a
++# Substitution' a
rho = (a -> Substitution' a -> Substitution' a)
-> Substitution' a -> [a] -> Substitution' a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> Substitution' a -> Substitution' a
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Substitution' a
rho [a]
us

-- | @
--      Γ ⊢ ρ : Δ  Γ ⊢ reverse vs : Θ
--      ----------------------------- (treating Nothing as having any type)
--        Γ ⊢ prependS vs ρ : Δ, Θ
--   @
prependS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS :: Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
err [Maybe a]
us Substitution' a
rho = (Maybe a -> Substitution' a -> Substitution' a)
-> Substitution' a -> [Maybe a] -> Substitution' a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe a -> Substitution' a -> Substitution' a
f Substitution' a
rho [Maybe a]
us
  where
    f :: Maybe a -> Substitution' a -> Substitution' a
f Maybe a
Nothing  Substitution' a
rho = Impossible -> Substitution' a -> Substitution' a
forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Impossible
err Substitution' a
rho
    f (Just a
u) Substitution' a
rho = a -> Substitution' a -> Substitution' a
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS a
u Substitution' a
rho

parallelS :: DeBruijn a => [a] -> Substitution' a
parallelS :: [a] -> Substitution' a
parallelS [a]
us = [a]
us [a] -> Substitution' a -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' a
forall a. Substitution' a
idS

compactS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a
compactS :: Impossible -> [Maybe a] -> Substitution' a
compactS Impossible
err [Maybe a]
us = Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
err [Maybe a]
us Substitution' a
forall a. Substitution' a
idS

-- | Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
strengthenS :: Impossible -> Int -> Substitution' a
strengthenS :: Impossible -> Nat -> Substitution' a
strengthenS Impossible
err = Substitution' a -> [Substitution' a] -> Nat -> Substitution' a
forall a. a -> [a] -> Nat -> a
indexWithDefault Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__ ([Substitution' a] -> Nat -> Substitution' a)
-> [Substitution' a] -> Nat -> Substitution' a
forall a b. (a -> b) -> a -> b
$ (Substitution' a -> Substitution' a)
-> Substitution' a -> [Substitution' a]
forall a. (a -> a) -> a -> [a]
iterate (Impossible -> Substitution' a -> Substitution' a
forall a. Impossible -> Substitution' a -> Substitution' a
Strengthen Impossible
err) Substitution' a
forall a. Substitution' a
idS

lookupS :: EndoSubst a => Substitution' a -> Nat -> a
lookupS :: Substitution' a -> Nat -> a
lookupS Substitution' a
rho Nat
i = case Substitution' a
rho of
  Substitution' a
IdS                    -> Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
i
  Wk Nat
n Substitution' a
IdS               -> let j :: Nat
j = Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
n in
                            if  Nat
j Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
0 then a
forall a. HasCallStack => a
__IMPOSSIBLE__ else Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
j
  Wk Nat
n Substitution' a
rho               -> Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
n) (Substitution' a -> Nat -> a
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho Nat
i)
  a
u :# Substitution' a
rho   | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0    -> a
u
             | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
0     -> a
forall a. HasCallStack => a
__IMPOSSIBLE__
             | Bool
otherwise -> Substitution' a -> Nat -> a
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
  Strengthen Impossible
err Substitution' a
rho
             | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0    -> Impossible -> a
forall a. Impossible -> a
throwImpossible Impossible
err
             | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
0     -> a
forall a. HasCallStack => a
__IMPOSSIBLE__
             | Bool
otherwise -> Substitution' a -> Nat -> a
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
  Lift Nat
n Substitution' a
rho | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n     -> Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
i
             | Bool
otherwise -> Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise Nat
n (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Substitution' a -> Nat -> a
forall a. EndoSubst a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n)
  EmptyS Impossible
err             -> Impossible -> a
forall a. Impossible -> a
throwImpossible Impossible
err


-- | lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.

listS :: EndoSubst a => [(Int,a)] -> Substitution' a
listS :: [(Nat, a)] -> Substitution' a
listS ((Nat
i,a
t):[(Nat, a)]
ts) = Nat -> a -> Substitution' a
forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
i a
t Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` [(Nat, a)] -> Substitution' a
forall a. EndoSubst a => [(Nat, a)] -> Substitution' a
listS [(Nat, a)]
ts
listS []         = Substitution' a
forall a. Substitution' a
IdS

-- | @Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ@
raiseFromS :: Nat -> Nat -> Substitution' a
raiseFromS :: Nat -> Nat -> Substitution' a
raiseFromS Nat
n Nat
k = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
n (Substitution' a -> Substitution' a)
-> Substitution' a -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
k


---------------------------------------------------------------------------
-- * Functions on abstractions
--   and things we couldn't do before we could define 'absBody'
---------------------------------------------------------------------------

-- | Instantiate an abstraction. Strict in the term.
absApp :: Subst a => Abs a -> SubstArg a -> a
absApp :: Abs a -> SubstArg a -> a
absApp (Abs   ArgName
_ a
v) SubstArg a
u = Nat -> SubstArg a -> a -> a
forall a. Subst a => Nat -> SubstArg a -> a -> a
subst Nat
0 SubstArg a
u a
v
absApp (NoAbs ArgName
_ a
v) SubstArg a
_ = a
v

-- | Instantiate an abstraction. Lazy in the term, which allow it to be
--   __IMPOSSIBLE__ in the case where the variable shouldn't be used but we
--   cannot use 'noabsApp'. Used in Apply.
lazyAbsApp :: Subst a => Abs a -> SubstArg a -> a
lazyAbsApp :: Abs a -> SubstArg a -> a
lazyAbsApp (Abs   ArgName
_ a
v) SubstArg a
u = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (SubstArg a
u SubstArg a
-> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' (SubstArg a)
forall a. Substitution' a
IdS) a
v  -- Note: do not use consS here!
lazyAbsApp (NoAbs ArgName
_ a
v) SubstArg a
_ = a
v

-- | Instantiate an abstraction that doesn't use its argument.
noabsApp :: Subst a => Impossible -> Abs a -> a
noabsApp :: Impossible -> Abs a -> a
noabsApp Impossible
err (Abs   ArgName
_ a
v) = Impossible -> a -> a
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
err a
v
noabsApp Impossible
_   (NoAbs ArgName
_ a
v) = a
v

absBody :: Subst a => Abs a -> a
absBody :: Abs a -> a
absBody (Abs   ArgName
_ a
v) = a
v
absBody (NoAbs ArgName
_ a
v) = Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise Nat
1 a
v

mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a
mkAbs :: ArgName -> a -> Abs a
mkAbs ArgName
x a
v | Nat
0 Nat -> a -> Bool
forall a. Free a => Nat -> a -> Bool
`freeIn` a
v = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x a
v
          | Bool
otherwise    = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x (Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise (-Nat
1) a
v)

reAbs :: (Subst a, Free a) => Abs a -> Abs a
reAbs :: Abs a -> Abs a
reAbs (NoAbs ArgName
x a
v) = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x a
v
reAbs (Abs ArgName
x a
v)   = ArgName -> a -> Abs a
forall a. (Subst a, Free a) => ArgName -> a -> Abs a
mkAbs ArgName
x a
v

-- | @underAbs k a b@ applies @k@ to @a@ and the content of
--   abstraction @b@ and puts the abstraction back.
--   @a@ is raised if abstraction was proper such that
--   at point of application of @k@ and the content of @b@
--   are at the same context.
--   Precondition: @a@ and @b@ are at the same context at call time.
underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
underAbs :: (a -> b -> b) -> a -> Abs b -> Abs b
underAbs a -> b -> b
cont a
a = \case
  Abs   ArgName
x b
t -> ArgName -> b -> Abs b
forall a. ArgName -> a -> Abs a
Abs   ArgName
x (b -> Abs b) -> b -> Abs b
forall a b. (a -> b) -> a -> b
$ a -> b -> b
cont (Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise Nat
1 a
a) b
t
  NoAbs ArgName
x b
t -> ArgName -> b -> Abs b
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x (b -> Abs b) -> b -> Abs b
forall a b. (a -> b) -> a -> b
$ a -> b -> b
cont a
a b
t

-- | @underLambdas n k a b@ drops @n@ initial 'Lam's from @b@,
--   performs operation @k@ on @a@ and the body of @b@,
--   and puts the 'Lam's back.  @a@ is raised correctly
--   according to the number of abstractions.
underLambdas :: TermSubst a => Int -> (a -> Term -> Term) -> a -> Term -> Term
underLambdas :: Nat -> (a -> Term -> Term) -> a -> Term -> Term
underLambdas Nat
n a -> Term -> Term
cont = Nat -> a -> Term -> Term
loop Nat
n where
  loop :: Nat -> a -> Term -> Term
loop Nat
0 a
a = a -> Term -> Term
cont a
a
  loop Nat
n a
a = \case
    Lam ArgInfo
h Abs Term
b -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ (a -> Term -> Term) -> a -> Abs Term -> Abs Term
forall a b. Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
underAbs (Nat -> a -> Term -> Term
loop (Nat -> a -> Term -> Term) -> Nat -> a -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1) a
a Abs Term
b
    Term
_       -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__