diff options
Diffstat (limited to 'src/full/Agda/TypeChecking/Substitute/Class.hs')
-rw-r--r-- | src/full/Agda/TypeChecking/Substitute/Class.hs | 256 |
1 files changed, 256 insertions, 0 deletions
diff --git a/src/full/Agda/TypeChecking/Substitute/Class.hs b/src/full/Agda/TypeChecking/Substitute/Class.hs new file mode 100644 index 0000000..3628a38 --- /dev/null +++ b/src/full/Agda/TypeChecking/Substitute/Class.hs @@ -0,0 +1,256 @@ +{-# LANGUAGE CPP #-} + +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 + +#include "undefined.h" +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 args = applyE t $ map Apply args + applyE t es = apply t $ map argFromElim es + -- precondition: all @es@ are @Apply@s + +-- | Apply to some default arguments. +applys :: Apply t => t -> [Term] -> t +applys t vs = apply t $ map defaultArg vs + +-- | Apply to a single default argument. +apply1 :: Apply t => t -> Term -> t +apply1 t u = applys t [ u ] + +--------------------------------------------------------------------------- +-- * Abstraction +--------------------------------------------------------------------------- + +-- | @(abstract args v) `apply` args --> v[args]@. +class Abstract t where + abstract :: Telescope -> t -> t + +--------------------------------------------------------------------------- +-- * Substitution and raising/shifting/weakening +--------------------------------------------------------------------------- + +-- | Apply a substitution. + +-- For terms: +-- +-- Γ ⊢ ρ : Δ +-- Δ ⊢ t : σ +-- ----------- +-- Γ ⊢ tρ : σρ + +class DeBruijn t => Subst t a | a -> t where + applySubst :: Substitution' t -> a -> a + +raise :: Subst t a => Nat -> a -> a +raise = raiseFrom 0 + +raiseFrom :: Subst t a => Nat -> Nat -> a -> a +raiseFrom n k = applySubst (liftS n $ raiseS k) + +-- | Replace de Bruijn index i by a 'Term' in something. +subst :: Subst t a => Int -> t -> a -> a +subst i u = applySubst $ singletonS i u + +strengthen :: Subst t a => Empty -> a -> a +strengthen err = applySubst (compactS err [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 n u = applySubst (liftS n (singletonS 0 u)) + +--------------------------------------------------------------------------- +-- * Explicit substitutions +--------------------------------------------------------------------------- + +-- See Syntax.Internal for the definition. + +idS :: Substitution' a +idS = IdS + +wkS :: Int -> Substitution' a -> Substitution' a +wkS 0 rho = rho +wkS n (Wk m rho) = Wk (n + m) rho +wkS n EmptyS = EmptyS +wkS n rho = Wk n rho + +raiseS :: Int -> Substitution' a +raiseS n = wkS n idS + +consS :: DeBruijn a => a -> Substitution' a -> Substitution' a +consS t (Wk m rho) + | Just n <- deBruijnView t, + n + 1 == m = wkS (m - 1) (liftS 1 rho) +consS u rho = seq u (u :# rho) + +-- | To replace index @n@ by term @u@, do @applySubst (singletonS n u)@. +singletonS :: DeBruijn a => Int -> a -> Substitution' a +singletonS n u = map deBruijnVar [0..n-1] ++# consS u (raiseS 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 k u = singletonS k u `composeS` liftS (k + 1) (raiseS 1) + +-- | Lift a substitution under k binders. +liftS :: Int -> Substitution' a -> Substitution' a +liftS 0 rho = rho +liftS k IdS = IdS +liftS k (Lift n rho) = Lift (n + k) rho +liftS k rho = Lift k rho + +dropS :: Int -> Substitution' a -> Substitution' a +dropS 0 rho = rho +dropS n IdS = raiseS n +dropS n (Wk m rho) = wkS m (dropS n rho) +dropS n (u :# rho) = dropS (n - 1) rho +dropS n (Strengthen _ rho) = dropS (n - 1) rho +dropS n (Lift 0 rho) = __IMPOSSIBLE__ +dropS n (Lift m rho) = wkS 1 $ dropS (n - 1) $ liftS (m - 1) rho +dropS n EmptyS = __IMPOSSIBLE__ + +-- | @applySubst (ρ `composeS` σ) v == applySubst ρ (applySubst σ v)@ +composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a +composeS rho IdS = rho +composeS IdS sgm = sgm +composeS rho EmptyS = EmptyS +composeS rho (Wk n sgm) = composeS (dropS n rho) sgm +composeS rho (u :# sgm) = applySubst rho u :# composeS rho sgm +composeS rho (Strengthen err sgm) = Strengthen err (composeS rho sgm) +composeS rho (Lift 0 sgm) = __IMPOSSIBLE__ +composeS (u :# rho) (Lift n sgm) = u :# composeS rho (liftS (n - 1) sgm) +composeS rho (Lift n sgm) = lookupS rho 0 :# composeS rho (wkS 1 (liftS (n - 1) sgm)) + +-- If Γ ⊢ ρ : Δ, Θ then splitS |Θ| ρ = (σ, δ), with +-- Γ ⊢ σ : Δ +-- Γ ⊢ δ : Θσ +splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a) +splitS 0 rho = (rho, EmptyS) +splitS n (u :# rho) = second (u :#) $ splitS (n - 1) rho +splitS n (Strengthen err rho) = second (Strengthen err) $ splitS (n - 1) rho +splitS n (Lift 0 _) = __IMPOSSIBLE__ +splitS n (Wk m rho) = wkS m *** wkS m $ splitS n rho +splitS n IdS = (raiseS n, liftS n EmptyS) +splitS n (Lift m rho) = wkS 1 *** liftS 1 $ splitS (n - 1) (liftS (m - 1) rho) +splitS n EmptyS = __IMPOSSIBLE__ + +infixr 4 ++# + +(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a +us ++# rho = foldr consS rho us + +prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a +prependS err us rho = foldr f rho us + where + f Nothing rho = Strengthen err rho + f (Just u) rho = consS u rho + +parallelS :: DeBruijn a => [a] -> Substitution' a +parallelS us = us ++# idS + +compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a +compactS err us = prependS err us idS + +-- | Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ +strengthenS :: Empty -> Int -> Substitution' a +strengthenS err n + | n < 0 = __IMPOSSIBLE__ + | otherwise = iterate (Strengthen err) idS !! n + +lookupS :: Subst a a => Substitution' a -> Nat -> a +lookupS rho i = case rho of + IdS -> deBruijnVar i + Wk n IdS -> let j = i + n in + if j < 0 then __IMPOSSIBLE__ else deBruijnVar j + Wk n rho -> applySubst (raiseS n) (lookupS rho i) + u :# rho | i == 0 -> u + | i < 0 -> __IMPOSSIBLE__ + | otherwise -> lookupS rho (i - 1) + Strengthen err rho + | i == 0 -> absurd err + | i < 0 -> __IMPOSSIBLE__ + | otherwise -> lookupS rho (i - 1) + Lift n rho | i < n -> deBruijnVar i + | otherwise -> raise n $ lookupS rho (i - n) + EmptyS -> __IMPOSSIBLE__ + +--------------------------------------------------------------------------- +-- * 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 _ v) u = subst 0 u v +absApp (NoAbs _ v) _ = 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 _ v) u = applySubst (u :# IdS) v -- Note: do not use consS here! +lazyAbsApp (NoAbs _ v) _ = v + +-- | Instantiate an abstraction that doesn't use its argument. +noabsApp :: Subst t a => Empty -> Abs a -> a +noabsApp err (Abs _ v) = strengthen err v +noabsApp _ (NoAbs _ v) = v + +absBody :: Subst t a => Abs a -> a +absBody (Abs _ v) = v +absBody (NoAbs _ v) = raise 1 v + +mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a +mkAbs x v | 0 `freeIn` v = Abs x v + | otherwise = NoAbs x (raise (-1) v) + +reAbs :: (Subst t a, Free a) => Abs a -> Abs a +reAbs (NoAbs x v) = NoAbs x v +reAbs (Abs x v) = mkAbs x 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 cont a b = case b of + Abs x t -> Abs x $ cont (raise 1 a) t + NoAbs x t -> NoAbs x $ cont a 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 n cont a v = loop n a v where + loop 0 a v = cont a v + loop n a v = case ignoreSharing v of + Lam h b -> Lam h $ underAbs (loop $ n-1) a b + _ -> __IMPOSSIBLE__ + |