1 2module Agda.TypeChecking.Substitute.Class where 3 4import Control.Arrow ((***), second) 5 6 7import Agda.Syntax.Common 8import Agda.Syntax.Internal 9 10import Agda.TypeChecking.Free 11import Agda.TypeChecking.Substitute.DeBruijn 12 13import Agda.Utils.Empty 14import Agda.Utils.List 15 16import Agda.Utils.Impossible 17 18--------------------------------------------------------------------------- 19-- * Application 20--------------------------------------------------------------------------- 21 22-- | Apply something to a bunch of arguments. 23-- Preserves blocking tags (application can never resolve blocking). 24class Apply t where 25 apply :: t -> Args -> t 26 applyE :: t -> Elims -> t 27 28 apply t args = applyE t $ map Apply args 29 -- Andreas, 2018-06-18, issue #3136 30 -- This default instance should be removed to get more precise 31 -- crash locations (raise the IMPOSSIBLE in a more specific place). 32 -- applyE t es = apply t $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 33 -- precondition: all @es@ are @Apply@s 34 35-- | Apply to some default arguments. 36applys :: Apply t => t -> [Term] -> t 37applys t vs = apply t $ map defaultArg vs 38 39-- | Apply to a single default argument. 40apply1 :: Apply t => t -> Term -> t 41apply1 t u = applys t [ u ] 42 43--------------------------------------------------------------------------- 44-- * Abstraction 45--------------------------------------------------------------------------- 46 47-- | @(abstract args v) `apply` args --> v[args]@. 48class Abstract t where 49 abstract :: Telescope -> t -> t 50 51--------------------------------------------------------------------------- 52-- * Substitution and shifting\/weakening\/strengthening 53--------------------------------------------------------------------------- 54 55-- | Apply a substitution. 56 57-- For terms: 58-- 59-- Γ ⊢ ρ : Δ 60-- Δ ⊢ t : A 61-- ----------- 62-- Γ ⊢ tρ : Aρ 63 64class DeBruijn (SubstArg a) => Subst a where 65 type SubstArg a 66 applySubst :: Substitution' (SubstArg a) -> a -> a 67 68 default applySubst :: (a ~ f b, Functor f, Subst b, SubstArg a ~ SubstArg b) => Substitution' (SubstArg a) -> a -> a 69 applySubst rho = fmap (applySubst rho) 70 71-- | Simple constraint alias for a `Subst` instance `a` with arg type `t`. 72type SubstWith t a = (Subst a, SubstArg a ~ t) 73 74-- | `Subst` instance whose agument type is itself 75type EndoSubst a = SubstWith a a 76 77-- | `Subst` instance whose argument type is `Term` 78type TermSubst a = SubstWith Term a 79 80-- | Raise de Bruijn index, i.e. weakening 81raise :: Subst a => Nat -> a -> a 82raise = raiseFrom 0 83 84raiseFrom :: Subst a => Nat -> Nat -> a -> a 85raiseFrom n k = applySubst (raiseFromS n k) 86 87-- | Replace de Bruijn index i by a 'Term' in something. 88subst :: Subst a => Int -> SubstArg a -> a -> a 89subst i u = applySubst $ singletonS i u 90 91strengthen :: Subst a => Impossible -> a -> a 92strengthen err = applySubst (compactS err [Nothing]) 93 94-- | Replace what is now de Bruijn index 0, but go under n binders. 95-- @substUnder n u == subst n (raise n u)@. 96substUnder :: Subst a => Nat -> SubstArg a -> a -> a 97substUnder n u = applySubst (liftS n (singletonS 0 u)) 98 99-- ** Identity instances 100 101instance Subst QName where 102 type SubstArg QName = Term 103 applySubst _ q = q 104 105--------------------------------------------------------------------------- 106-- * Explicit substitutions 107--------------------------------------------------------------------------- 108 109-- See Syntax.Internal for the definition. 110 111idS :: Substitution' a 112idS = IdS 113 114wkS :: Int -> Substitution' a -> Substitution' a 115wkS 0 rho = rho 116wkS n (Wk m rho) = Wk (n + m) rho 117wkS n (EmptyS err) = EmptyS err 118wkS n rho = Wk n rho 119 120raiseS :: Int -> Substitution' a 121raiseS n = wkS n idS 122 123consS :: DeBruijn a => a -> Substitution' a -> Substitution' a 124consS t (Wk m rho) 125 | Just n <- deBruijnView t, 126 n + 1 == m = wkS (m - 1) (liftS 1 rho) 127consS u rho = seq u (u :# rho) 128 129-- | To replace index @n@ by term @u@, do @applySubst (singletonS n u)@. 130-- @ 131-- Γ, Δ ⊢ u : A 132-- --------------------------------- 133-- Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ 134-- @ 135singletonS :: DeBruijn a => Int -> a -> Substitution' a 136singletonS n u = map deBruijnVar [0..n-1] ++# consS u (raiseS n) 137 -- ALT: foldl (\ s i -> deBruijnVar i `consS` s) (consS u $ raiseS n) $ downFrom n 138 139-- | Single substitution without disturbing any deBruijn indices. 140-- @ 141-- Γ, A, Δ ⊢ u : A 142-- --------------------------------- 143-- Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ 144-- @ 145inplaceS :: EndoSubst a => Int -> a -> Substitution' a 146inplaceS k u = singletonS k u `composeS` liftS (k + 1) (raiseS 1) 147 148-- | Lift a substitution under k binders. 149liftS :: Int -> Substitution' a -> Substitution' a 150liftS 0 rho = rho 151liftS k IdS = IdS 152liftS k (Lift n rho) = Lift (n + k) rho 153liftS k rho = Lift k rho 154 155-- | @ 156-- Γ ⊢ ρ : Δ, Ψ 157-- ------------------- 158-- Γ ⊢ dropS |Ψ| ρ : Δ 159-- @ 160dropS :: Int -> Substitution' a -> Substitution' a 161dropS 0 rho = rho 162dropS n IdS = raiseS n 163dropS n (Wk m rho) = wkS m (dropS n rho) 164dropS n (u :# rho) = dropS (n - 1) rho 165dropS n (Strengthen _ rho) = dropS (n - 1) rho 166dropS n (Lift 0 rho) = __IMPOSSIBLE__ 167dropS n (Lift m rho) = wkS 1 $ dropS (n - 1) $ liftS (m - 1) rho 168dropS n (EmptyS err) = throwImpossible err 169 170-- | @applySubst (ρ `composeS` σ) v == applySubst ρ (applySubst σ v)@ 171composeS :: EndoSubst a => Substitution' a -> Substitution' a -> Substitution' a 172composeS rho IdS = rho 173composeS IdS sgm = sgm 174composeS rho (EmptyS err) = EmptyS err 175composeS rho (Wk n sgm) = composeS (dropS n rho) sgm 176composeS rho (u :# sgm) = applySubst rho u :# composeS rho sgm 177composeS rho (Strengthen err sgm) = Strengthen err (composeS rho sgm) 178composeS rho (Lift 0 sgm) = __IMPOSSIBLE__ 179composeS (u :# rho) (Lift n sgm) = u :# composeS rho (liftS (n - 1) sgm) 180composeS rho (Lift n sgm) = lookupS rho 0 :# composeS rho (wkS 1 (liftS (n - 1) sgm)) 181 182-- If Γ ⊢ ρ : Δ, Θ then splitS |Θ| ρ = (σ, δ), with 183-- Γ ⊢ σ : Δ 184-- Γ ⊢ δ : Θσ 185splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a) 186splitS 0 rho = (rho, EmptyS impossible) 187splitS n (u :# rho) = second (u :#) $ splitS (n - 1) rho 188splitS n (Strengthen err rho) = second (Strengthen err) $ splitS (n - 1) rho 189splitS n (Lift 0 _) = __IMPOSSIBLE__ 190splitS n (Wk m rho) = wkS m *** wkS m $ splitS n rho 191splitS n IdS = (raiseS n, liftS n $ EmptyS impossible) 192splitS n (Lift m rho) = wkS 1 *** liftS 1 $ splitS (n - 1) (liftS (m - 1) rho) 193splitS n (EmptyS err) = __IMPOSSIBLE__ 194 195infixr 4 ++# 196 197(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a 198us ++# rho = foldr consS rho us 199 200-- | @ 201-- Γ ⊢ ρ : Δ Γ ⊢ reverse vs : Θ 202-- ----------------------------- (treating Nothing as having any type) 203-- Γ ⊢ prependS vs ρ : Δ, Θ 204-- @ 205prependS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a 206prependS err us rho = foldr f rho us 207 where 208 f Nothing rho = Strengthen err rho 209 f (Just u) rho = consS u rho 210 211parallelS :: DeBruijn a => [a] -> Substitution' a 212parallelS us = us ++# idS 213 214compactS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a 215compactS err us = prependS err us idS 216 217-- | Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ 218strengthenS :: Impossible -> Int -> Substitution' a 219strengthenS err = indexWithDefault __IMPOSSIBLE__ $ iterate (Strengthen err) idS 220 221lookupS :: EndoSubst a => Substitution' a -> Nat -> a 222lookupS rho i = case rho of 223 IdS -> deBruijnVar i 224 Wk n IdS -> let j = i + n in 225 if j < 0 then __IMPOSSIBLE__ else deBruijnVar j 226 Wk n rho -> applySubst (raiseS n) (lookupS rho i) 227 u :# rho | i == 0 -> u 228 | i < 0 -> __IMPOSSIBLE__ 229 | otherwise -> lookupS rho (i - 1) 230 Strengthen err rho 231 | i == 0 -> throwImpossible err 232 | i < 0 -> __IMPOSSIBLE__ 233 | otherwise -> lookupS rho (i - 1) 234 Lift n rho | i < n -> deBruijnVar i 235 | otherwise -> raise n $ lookupS rho (i - n) 236 EmptyS err -> throwImpossible err 237 238 239-- | lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn. 240 241listS :: EndoSubst a => [(Int,a)] -> Substitution' a 242listS ((i,t):ts) = singletonS i t `composeS` listS ts 243listS [] = IdS 244 245-- | @Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ@ 246raiseFromS :: Nat -> Nat -> Substitution' a 247raiseFromS n k = liftS n $ raiseS k 248 249 250--------------------------------------------------------------------------- 251-- * Functions on abstractions 252-- and things we couldn't do before we could define 'absBody' 253--------------------------------------------------------------------------- 254 255-- | Instantiate an abstraction. Strict in the term. 256absApp :: Subst a => Abs a -> SubstArg a -> a 257absApp (Abs _ v) u = subst 0 u v 258absApp (NoAbs _ v) _ = v 259 260-- | Instantiate an abstraction. Lazy in the term, which allow it to be 261-- __IMPOSSIBLE__ in the case where the variable shouldn't be used but we 262-- cannot use 'noabsApp'. Used in Apply. 263lazyAbsApp :: Subst a => Abs a -> SubstArg a -> a 264lazyAbsApp (Abs _ v) u = applySubst (u :# IdS) v -- Note: do not use consS here! 265lazyAbsApp (NoAbs _ v) _ = v 266 267-- | Instantiate an abstraction that doesn't use its argument. 268noabsApp :: Subst a => Impossible -> Abs a -> a 269noabsApp err (Abs _ v) = strengthen err v 270noabsApp _ (NoAbs _ v) = v 271 272absBody :: Subst a => Abs a -> a 273absBody (Abs _ v) = v 274absBody (NoAbs _ v) = raise 1 v 275 276mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a 277mkAbs x v | 0 `freeIn` v = Abs x v 278 | otherwise = NoAbs x (raise (-1) v) 279 280reAbs :: (Subst a, Free a) => Abs a -> Abs a 281reAbs (NoAbs x v) = NoAbs x v 282reAbs (Abs x v) = mkAbs x v 283 284-- | @underAbs k a b@ applies @k@ to @a@ and the content of 285-- abstraction @b@ and puts the abstraction back. 286-- @a@ is raised if abstraction was proper such that 287-- at point of application of @k@ and the content of @b@ 288-- are at the same context. 289-- Precondition: @a@ and @b@ are at the same context at call time. 290underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b 291underAbs cont a = \case 292 Abs x t -> Abs x $ cont (raise 1 a) t 293 NoAbs x t -> NoAbs x $ cont a t 294 295-- | @underLambdas n k a b@ drops @n@ initial 'Lam's from @b@, 296-- performs operation @k@ on @a@ and the body of @b@, 297-- and puts the 'Lam's back. @a@ is raised correctly 298-- according to the number of abstractions. 299underLambdas :: TermSubst a => Int -> (a -> Term -> Term) -> a -> Term -> Term 300underLambdas n cont = loop n where 301 loop 0 a = cont a 302 loop n a = \case 303 Lam h b -> Lam h $ underAbs (loop $ n-1) a b 304 _ -> __IMPOSSIBLE__ 305