{-# LANGUAGE TypeFamilies #-}

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 t => Subst t a | a -> t where
  applySubst :: Substitution' t -> a -> a

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


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

raiseFrom :: Subst t a => Nat -> Nat -> a -> a
raiseFrom :: Nat -> Nat -> a -> a
raiseFrom Nat
n Nat
k = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Nat -> Substitution' t -> Substitution' t
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
n (Substitution' t -> Substitution' t)
-> Substitution' t -> Substitution' t
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution' t
forall a. Nat -> Substitution' a
raiseS Nat
k)

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

strengthen :: Subst t a => Empty -> a -> a
strengthen :: Empty -> a -> a
strengthen Empty
err = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Empty -> [Maybe t] -> Substitution' t
forall a. DeBruijn a => Empty -> [Maybe a] -> Substitution' a
compactS Empty
err [Maybe t
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 t a => Nat -> t -> a -> a
substUnder :: Nat -> t -> a -> a
substUnder Nat
n t
u = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Nat -> Substitution' t -> Substitution' t
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
n (Nat -> t -> Substitution' t
forall a. DeBruijn a => Nat -> a -> Substitution' a
singletonS Nat
0 t
u))

-- ** Identity instances

instance Subst Term QName where
  applySubst :: Substitution' Term -> QName -> QName
applySubst Substitution' Term
_ 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 Empty
err) = Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
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 :: Subst a 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.
Subst a 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 Empty
_ 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 Empty
err)       = Empty -> Substitution' a
forall a. Empty -> a
absurd Empty
err

-- | @applySubst (ρ `composeS` σ) v == applySubst ρ (applySubst σ v)@
composeS :: Subst a 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 Empty
err) = Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
err
composeS Substitution' a
rho (Wk Nat
n Substitution' a
sgm) = Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a 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' a -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' a
rho a
u a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' a
rho Substitution' a
sgm
composeS Substitution' a
rho (Strengthen Empty
err Substitution' a
sgm) = Empty -> Substitution' a -> Substitution' a
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Empty
err (Substitution' a -> Substitution' a -> Substitution' a
forall a.
Subst a 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.
Subst a 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. Subst a 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.
Subst a 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, Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
forall a. HasCallStack => a
__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 Empty
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 (Empty -> Substitution' a -> Substitution' a
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Empty
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
$ Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
forall a. HasCallStack => a
__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 Empty
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 => Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS :: Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Empty
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 = Empty -> Substitution' a -> Substitution' a
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Empty
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 => Empty -> [Maybe a] -> Substitution' a
compactS :: Empty -> [Maybe a] -> Substitution' a
compactS Empty
err [Maybe a]
us = Empty -> [Maybe a] -> Substitution' a -> Substitution' a
forall a.
DeBruijn a =>
Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Empty
err [Maybe a]
us Substitution' a
forall a. Substitution' a
idS

-- | Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
strengthenS :: Empty -> Int -> Substitution' a
strengthenS :: Empty -> Nat -> Substitution' a
strengthenS Empty
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 (Empty -> Substitution' a -> Substitution' a
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Empty
err) Substitution' a
forall a. Substitution' a
idS

lookupS :: Subst a 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' a -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
n) (Substitution' a -> Nat -> a
forall a. Subst a 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. Subst a a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
  Strengthen Empty
err Substitution' a
rho
             | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
0    -> Empty -> a
forall a. Empty -> a
absurd Empty
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. Subst a 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 t a. Subst t a => Nat -> a -> a
raise Nat
n (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Substitution' a -> Nat -> a
forall a. Subst a a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n)
  EmptyS Empty
err             -> Empty -> a
forall a. Empty -> a
absurd Empty
err


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

listS :: Subst a 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.
Subst a a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` [(Nat, a)] -> Substitution' a
forall a. Subst a a => [(Nat, a)] -> Substitution' a
listS [(Nat, a)]
ts
listS []         = Substitution' a
forall a. Substitution' a
IdS


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

-- | Instantiate an abstraction. Strict in the term.
absApp :: Subst t a => Abs a -> t -> a
absApp :: Abs a -> t -> a
absApp (Abs   ArgName
_ a
v) t
u = Nat -> t -> a -> a
forall t a. Subst t a => Nat -> t -> a -> a
subst Nat
0 t
u a
v
absApp (NoAbs ArgName
_ a
v) t
_ = 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 t a => Abs a -> t -> a
lazyAbsApp :: Abs a -> t -> a
lazyAbsApp (Abs   ArgName
_ a
v) t
u = Substitution' t -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (t
u t -> Substitution' t -> Substitution' t
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' t
forall a. Substitution' a
IdS) a
v  -- Note: do not use consS here!
lazyAbsApp (NoAbs ArgName
_ a
v) t
_ = a
v

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

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

mkAbs :: (Subst t 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 t a. Subst t a => Nat -> a -> a
raise (-Nat
1) a
v)

reAbs :: (Subst t 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 t a. (Subst t 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 t 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 Abs b
b = case Abs b
b of
  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 t a. Subst t 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 :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term
underLambdas :: Nat -> (a -> Term -> Term) -> a -> Term -> Term
underLambdas Nat
n a -> Term -> Term
cont a
a = Nat -> a -> Term -> Term
loop Nat
n a
a where
  loop :: Nat -> a -> Term -> Term
loop Nat
0 a
a Term
v = a -> Term -> Term
cont a
a Term
v
  loop Nat
n a
a Term
v = case Term
v of
    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 t a b. Subst t 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__