{-# 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
class Apply t where
apply :: t -> Args -> t
applyE :: t -> Elims -> t
apply t :: t
t args :: 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
applys :: Apply t => t -> [Term] -> t
applys :: t -> [Term] -> t
applys t :: t
t vs :: [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
apply1 :: Apply t => t -> Term -> t
apply1 :: t -> Term -> t
apply1 t :: t
t u :: Term
u = t -> [Term] -> t
forall t. Apply t => t -> [Term] -> t
applys t
t [ Term
u ]
class Abstract t where
abstract :: Telescope -> t -> t
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 rho :: 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 :: 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 0
raiseFrom :: Subst t a => Nat -> Nat -> a -> a
raiseFrom :: Nat -> Nat -> a -> a
raiseFrom n :: Nat
n k :: 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)
subst :: Subst t a => Int -> t -> a -> a
subst :: Nat -> t -> a -> a
subst i :: Nat
i u :: 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 err :: 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])
substUnder :: Subst t a => Nat -> t -> a -> a
substUnder :: Nat -> t -> a -> a
substUnder n :: Nat
n u :: 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 0 t
u))
instance Subst Term QName where
applySubst :: Substitution' Term -> QName -> QName
applySubst _ q :: QName
q = QName
q
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 0 rho :: Substitution' a
rho = Substitution' a
rho
wkS n :: Nat
n (Wk m :: Nat
m rho :: 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 n :: Nat
n (EmptyS err :: Empty
err) = Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
err
wkS n :: Nat
n rho :: 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 n :: 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 t :: a
t (Wk m :: Nat
m rho :: Substitution' a
rho)
| Just n :: 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
+ 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
- 1) (Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
liftS 1 Substitution' a
rho)
consS u :: a
u rho :: Substitution' a
rho = a -> Substitution' a -> Substitution' a
forall a b. a -> b -> b
seq a
u (a
u a -> Substitution' a -> Substitution' a
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' a
rho)
singletonS :: DeBruijn a => Int -> a -> Substitution' a
singletonS :: Nat -> a -> Substitution' a
singletonS n :: Nat
n u :: a
u = (Nat -> a) -> [Nat] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar [0..Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-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)
inplaceS :: Subst a a => Int -> a -> Substitution' a
inplaceS :: Nat -> a -> Substitution' a
inplaceS k :: Nat
k u :: 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
+ 1) (Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS 1)
liftS :: Int -> Substitution' a -> Substitution' a
liftS :: Nat -> Substitution' a -> Substitution' a
liftS 0 rho :: Substitution' a
rho = Substitution' a
rho
liftS k :: Nat
k IdS = Substitution' a
forall a. Substitution' a
IdS
liftS k :: Nat
k (Lift n :: Nat
n rho :: 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 k :: Nat
k rho :: Substitution' a
rho = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
Lift Nat
k Substitution' a
rho
dropS :: Int -> Substitution' a -> Substitution' a
dropS :: Nat -> Substitution' a -> Substitution' a
dropS 0 rho :: Substitution' a
rho = Substitution' a
rho
dropS n :: Nat
n IdS = Nat -> Substitution' a
forall a. Nat -> Substitution' a
raiseS Nat
n
dropS n :: Nat
n (Wk m :: Nat
m rho :: 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 n :: Nat
n (u :: a
u :# rho :: 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
- 1) Substitution' a
rho
dropS n :: Nat
n (Strengthen _ rho :: 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
- 1) Substitution' a
rho
dropS n :: Nat
n (Lift 0 rho :: Substitution' a
rho) = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
dropS n :: Nat
n (Lift m :: Nat
m rho :: Substitution' a
rho) = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS 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
- 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
- 1) Substitution' a
rho
dropS n :: Nat
n (EmptyS err :: Empty
err) = Empty -> Substitution' a
forall a. Empty -> a
absurd Empty
err
composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a
composeS :: Substitution' a -> Substitution' a -> Substitution' a
composeS rho :: Substitution' a
rho IdS = Substitution' a
rho
composeS IdS sgm :: Substitution' a
sgm = Substitution' a
sgm
composeS rho :: Substitution' a
rho (EmptyS err :: Empty
err) = Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
err
composeS rho :: Substitution' a
rho (Wk n :: Nat
n sgm :: 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 rho :: Substitution' a
rho (u :: a
u :# sgm :: 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 rho :: Substitution' a
rho (Strengthen err :: Empty
err sgm :: 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 rho :: Substitution' a
rho (Lift 0 sgm :: Substitution' a
sgm) = Substitution' a
forall a. HasCallStack => a
__IMPOSSIBLE__
composeS (u :: a
u :# rho :: Substitution' a
rho) (Lift n :: Nat
n sgm :: 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
- 1) Substitution' a
sgm)
composeS rho :: Substitution' a
rho (Lift n :: Nat
n sgm :: Substitution' a
sgm) = Substitution' a -> Nat -> a
forall a. Subst a a => Substitution' a -> Nat -> a
lookupS Substitution' a
rho 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 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
- 1) Substitution' a
sgm))
splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS :: Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS 0 rho :: Substitution' a
rho = (Substitution' a
rho, Empty -> Substitution' a
forall a. Empty -> Substitution' a
EmptyS Empty
forall a. HasCallStack => a
__IMPOSSIBLE__)
splitS n :: Nat
n (u :: a
u :# rho :: 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
- 1) Substitution' a
rho
splitS n :: Nat
n (Strengthen err :: Empty
err rho :: 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
- 1) Substitution' a
rho
splitS n :: Nat
n (Lift 0 _) = (Substitution' a, Substitution' a)
forall a. HasCallStack => a
__IMPOSSIBLE__
splitS n :: Nat
n (Wk m :: Nat
m rho :: 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 n :: Nat
n 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 n :: Nat
n (Lift m :: Nat
m rho :: Substitution' a
rho) = Nat -> Substitution' a -> Substitution' a
forall a. Nat -> Substitution' a -> Substitution' a
wkS 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 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
- 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
- 1) Substitution' a
rho)
splitS n :: Nat
n (EmptyS err :: Empty
err) = (Substitution' a, Substitution' a)
forall a. HasCallStack => a
__IMPOSSIBLE__
infixr 4 ++#
(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
us :: [a]
us ++# :: [a] -> Substitution' a -> Substitution' a
++# rho :: 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
prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS :: Empty -> [Maybe a] -> Substitution' a -> Substitution' a
prependS err :: Empty
err us :: [Maybe a]
us rho :: 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 Nothing rho :: Substitution' a
rho = Empty -> Substitution' a -> Substitution' a
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Empty
err Substitution' a
rho
f (Just u :: a
u) rho :: 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 us :: [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 err :: Empty
err us :: [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 :: Empty -> Int -> Substitution' a
strengthenS :: Empty -> Nat -> Substitution' a
strengthenS err :: 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 rho :: Substitution' a
rho i :: Nat
i = case Substitution' a
rho of
IdS -> Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
i
Wk n :: Nat
n 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
< 0 then a
forall a. HasCallStack => a
__IMPOSSIBLE__ else Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
j
Wk n :: Nat
n rho :: 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)
u :: a
u :# rho :: Substitution' a
rho | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== 0 -> a
u
| Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< 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
- 1)
Strengthen err :: Empty
err rho :: Substitution' a
rho
| Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== 0 -> Empty -> a
forall a. Empty -> a
absurd Empty
err
| Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< 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
- 1)
Lift n :: Nat
n rho :: 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 err :: Empty
err -> Empty -> a
forall a. Empty -> a
absurd Empty
err
listS :: Subst a a => [(Int,a)] -> Substitution' a
listS :: [(Nat, a)] -> Substitution' a
listS ((i :: Nat
i,t :: a
t):ts :: [(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
absApp :: Subst t a => Abs a -> t -> a
absApp :: Abs a -> t -> a
absApp (Abs _ v :: a
v) u :: t
u = Nat -> t -> a -> a
forall t a. Subst t a => Nat -> t -> a -> a
subst 0 t
u a
v
absApp (NoAbs _ v :: a
v) _ = a
v
lazyAbsApp :: Subst t a => Abs a -> t -> a
lazyAbsApp :: Abs a -> t -> a
lazyAbsApp (Abs _ v :: a
v) u :: 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
lazyAbsApp (NoAbs _ v :: a
v) _ = a
v
noabsApp :: Subst t a => Empty -> Abs a -> a
noabsApp :: Empty -> Abs a -> a
noabsApp err :: Empty
err (Abs _ v :: a
v) = Empty -> a -> a
forall t a. Subst t a => Empty -> a -> a
strengthen Empty
err a
v
noabsApp _ (NoAbs _ v :: a
v) = a
v
absBody :: Subst t a => Abs a -> a
absBody :: Abs a -> a
absBody (Abs _ v :: a
v) = a
v
absBody (NoAbs _ v :: a
v) = Nat -> a -> a
forall t a. Subst t a => Nat -> a -> a
raise 1 a
v
mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a
mkAbs :: ArgName -> a -> Abs a
mkAbs x :: ArgName
x v :: a
v | 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 (-1) a
v)
reAbs :: (Subst t a, Free a) => Abs a -> Abs a
reAbs :: Abs a -> Abs a
reAbs (NoAbs x :: ArgName
x v :: a
v) = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x a
v
reAbs (Abs x :: ArgName
x v :: a
v) = ArgName -> a -> Abs a
forall t a. (Subst t a, Free a) => ArgName -> a -> Abs a
mkAbs ArgName
x a
v
underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b
underAbs :: (a -> b -> b) -> a -> Abs b -> Abs b
underAbs cont :: a -> b -> b
cont a :: a
a b :: Abs b
b = case Abs b
b of
Abs x :: ArgName
x t :: 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 1 a
a) b
t
NoAbs x :: ArgName
x t :: 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 :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term
underLambdas :: Nat -> (a -> Term -> Term) -> a -> Term -> Term
underLambdas n :: Nat
n cont :: a -> Term -> Term
cont a :: a
a = Nat -> a -> Term -> Term
loop Nat
n a
a where
loop :: Nat -> a -> Term -> Term
loop 0 a :: a
a v :: Term
v = a -> Term -> Term
cont a
a Term
v
loop n :: Nat
n a :: a
a v :: Term
v = case Term
v of
Lam h :: ArgInfo
h b :: 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
-1) a
a Abs Term
b
_ -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__