diff options
Diffstat (limited to 'src/full/Agda/TypeChecking/Substitute.hs')
| -rw-r--r-- | src/full/Agda/TypeChecking/Substitute.hs | 643 |
1 files changed, 286 insertions, 357 deletions
diff --git a/src/full/Agda/TypeChecking/Substitute.hs b/src/full/Agda/TypeChecking/Substitute.hs index dc48803..d2aee13 100644 --- a/src/full/Agda/TypeChecking/Substitute.hs +++ b/src/full/Agda/TypeChecking/Substitute.hs @@ -1,13 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} #if __GLASGOW_HASKELL__ <= 708 @@ -18,11 +11,12 @@ module Agda.TypeChecking.Substitute ( module Agda.TypeChecking.Substitute + , module Agda.TypeChecking.Substitute.Class + , module Agda.TypeChecking.Substitute.DeBruijn , Substitution'(..), Substitution ) where -import Control.Arrow ((***), second) - +import Control.Applicative import Data.Function import Data.Functor import Data.List hiding (sort, drop) @@ -37,52 +31,34 @@ import Debug.Trace (trace) import Agda.Syntax.Common import Agda.Syntax.Internal import Agda.Syntax.Internal.Pattern -import Agda.Syntax.Position +import qualified Agda.Syntax.Abstract as A import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Free as Free import Agda.TypeChecking.CompiledClause import Agda.TypeChecking.Positivity.Occurrence as Occ +import Agda.TypeChecking.Substitute.Class +import Agda.TypeChecking.Substitute.DeBruijn + import Agda.Utils.Empty import Agda.Utils.Functor import Agda.Utils.List import Agda.Utils.Permutation import Agda.Utils.Size import Agda.Utils.Tuple +import Agda.Utils.HashMap (HashMap) #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 ] - instance Apply Term where applyE m [] = m applyE m es = case m of Var i es' -> Var i (es' ++ es) Def f es' -> defApp f es' es -- remove projection redexes - Con c args -> conApp c args es + Con c ci args -> conApp c ci args es Lam _ b -> case es of Apply a : es0 -> lazyAbsApp b (unArg a) `applyE` es0 @@ -101,16 +77,16 @@ instance Apply Term where canProject :: QName -> Term -> Maybe (Arg Term) canProject f v = case ignoreSharing v of - (Con (ConHead _ _ fs) vs) -> do + (Con (ConHead _ _ fs) _ vs) -> do i <- elemIndex f fs headMaybe (drop i vs) _ -> Nothing -- | Eliminate a constructed term. -conApp :: ConHead -> Args -> Elims -> Term -conApp ch args [] = Con ch args -conApp ch args (Apply a : es) = conApp ch (args ++ [a]) es -conApp ch@(ConHead c _ fs) args (Proj f : es) = +conApp :: ConHead -> ConInfo -> Args -> Elims -> Term +conApp ch ci args [] = Con ch ci args +conApp ch ci args (Apply a : es) = conApp ch ci (args ++ [a]) es +conApp ch@(ConHead c _ fs) ci args (Proj o f : es) = let failure = flip trace __IMPOSSIBLE__ $ "conApp: constructor " ++ show c ++ " with fields " ++ show fs ++ @@ -118,6 +94,24 @@ conApp ch@(ConHead c _ fs) args (Proj f : es) = i = maybe failure id $ elemIndex f fs v = maybe failure argToDontCare $ headMaybe $ drop i args in applyE v es + + -- -- Andreas, 2016-07-20 futile attempt to magically fix ProjOrigin + -- fallback = v + -- in if not $ null es then applyE v es else + -- -- If we have no more eliminations, we can return v + -- if o == ProjSystem then fallback else + -- -- If the result is a projected term with ProjSystem, + -- -- we can can restore it to ProjOrigin o. + -- -- Otherwise, we get unpleasant printing with eta-expanded record metas. + -- caseMaybe (hasElims v) fallback $ \ (hd, es0) -> + -- caseMaybe (initLast es0) fallback $ \ (es1, e2) -> + -- case e2 of + -- -- We want to replace this ProjSystem by o. + -- Proj ProjSystem q -> hd (es1 ++ [Proj o q]) + -- -- Andreas, 2016-07-21 for the whole testsuite + -- -- this case was never triggered! + -- _ -> fallback + {- i = maybe failure id $ elemIndex f $ map unArg fs v = maybe failure unArg $ headMaybe $ drop i args @@ -184,14 +178,15 @@ instance Subst Term a => Apply (Tele a) where apply (ExtendTel _ tel) (t : ts) = lazyAbsApp tel (unArg t) `apply` ts instance Apply Definition where - apply (Defn info x t pol occ df m c inst copy d) args = - Defn info x (piApply t args) (apply pol args) (apply occ args) df m c inst copy (apply d args) + apply (Defn info x t pol occ df m c inst copy ma d) args = + Defn info x (piApply t args) (apply pol args) (apply occ args) df m c inst copy ma (apply d args) instance Apply RewriteRule where apply r args = RewriteRule { rewName = rewName r , rewContext = apply (rewContext r) args - , rewLHS = applySubst sub (rewLHS r) + , rewHead = rewHead r + , rewPats = applySubst sub (rewPats r) , rewRHS = applySubst sub (rewRHS r) , rewType = applySubst sub (rewType r) } @@ -211,16 +206,39 @@ instance Apply [Polarity] where #endif apply pol args = List.drop (length args) pol +-- | Make sure we only drop variable patterns. +#if __GLASGOW_HASKELL__ >= 710 +instance {-# OVERLAPPING #-} Apply [NamedArg (Pattern' a)] where +#else +instance Apply [NamedArg (Pattern' a)] where +#endif + apply ps args = loop (length args) ps + where + loop 0 ps = ps + loop n [] = __IMPOSSIBLE__ + loop n (p : ps) = + let recurse = loop (n - 1) ps + in case namedArg p of + VarP{} -> recurse + DotP{} -> __IMPOSSIBLE__ + LitP{} -> __IMPOSSIBLE__ + ConP{} -> __IMPOSSIBLE__ + ProjP{} -> __IMPOSSIBLE__ + instance Apply Projection where apply p args = p - { projIndex = projIndex p - size args - , projDropPars = projDropPars p `apply` args + { projIndex = projIndex p - size args + , projLams = projLams p `apply` args } +instance Apply ProjLams where + apply (ProjLams lams) args = ProjLams $ List.drop (length args) lams + instance Apply Defn where apply d [] = d apply d args = case d of Axiom{} -> d + AbstractDefn -> d Function{ funClauses = cs, funCompiled = cc, funInv = inv , funProjection = Nothing } -> d { funClauses = apply cs args @@ -268,9 +286,9 @@ instance Apply Defn where , dataClause = apply cl args -- , dataArgOccurrences = List.drop (length args) occ } - Record{ recPars = np, recConType = t, recClause = cl, recTel = tel + Record{ recPars = np, recClause = cl, recTel = tel {-, recArgOccurrences = occ-} } -> - d { recPars = np - size args, recConType = piApply t args + d { recPars = np - size args , recClause = apply cl args, recTel = apply tel args -- , recArgOccurrences = List.drop (length args) occ } @@ -283,13 +301,86 @@ instance Apply PrimFun where apply (PrimFun x ar def) args = PrimFun x (ar - size args) $ \vs -> def (args ++ vs) instance Apply Clause where - apply (Clause r tel ps b t catchall) args = + -- This one is a little bit tricksy after the parameter refinement change. + -- It is assumed that we only apply a clause to "parameters", i.e. + -- arguments introduced by lambda lifting. The problem is that these aren't + -- necessarily the first elements of the clause telescope. + apply cls@(Clause r tel ps b t catchall) args + | length args > length ps = __IMPOSSIBLE__ + | otherwise = Clause r - (apply tel args) - (List.drop (size args) ps) - (apply b args) - (applySubst (parallelS (map unArg args)) t) + tel' + (applySubst rhoP $ drop (length args) ps) + (applySubst rho b) + (applySubst rho t) catchall + where + -- We have + -- Γ ⊢ args, for some outer context Γ + -- Δ ⊢ ps, where Δ is the clause telescope (tel) + rargs = map unArg $ reverse args + rps = reverse $ take (length args) ps + n = size tel + + -- This is the new telescope. Created by substituting the args into the + -- appropriate places in the old telescope. We know where those are by + -- looking at the deBruijn indices of the patterns. + tel' = newTel n tel rps rargs + + -- We then have to create a substitution from the old telescope to the + -- new telescope that we can apply to dot patterns and the clause body. + rhoP :: PatternSubstitution + rhoP = mkSub DotP n rps rargs + rho = mkSub id n rps rargs + + substP :: Nat -> Term -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern] + substP i v = subst i (DotP v) + + -- Building the substitution from the old telescope to the new. The + -- interesting case is when we have a variable pattern: + -- We need Δ′ ⊢ ρ : Δ + -- where Δ′ = newTel Δ (xⁱ : ps) (v : vs) + -- = newTel Δ[xⁱ:=v] ps[xⁱ:=v'] vs + -- Note that we need v' = raise (|Δ| - 1) v, to make Γ ⊢ v valid in + -- ΓΔ[xⁱ:=v]. + -- A recursive call ρ′ = mkSub (substP i v' ps) vs gets us + -- Δ′ ⊢ ρ′ : Δ[xⁱ:=v] + -- so we just need Δ[xⁱ:=v] ⊢ σ : Δ and then ρ = ρ′ ∘ σ. + -- That's achieved by σ = singletonS i v'. + mkSub :: Subst a a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution' a + mkSub _ _ [] [] = idS + mkSub tm n (p : ps) (v : vs) = + case namedArg p of + VarP (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v') + where v' = raise (n - 1) v + DotP{} -> mkSub tm n ps vs + LitP{} -> __IMPOSSIBLE__ + ConP{} -> __IMPOSSIBLE__ + ProjP{} -> __IMPOSSIBLE__ + mkSub _ _ _ _ = __IMPOSSIBLE__ + + -- The parameter patterns 'ps' are all variables or dot patterns. If they + -- are variables they can appear anywhere in the clause telescope. This + -- function constructs the new telescope with 'vs' substituted for 'ps'. + -- Example: + -- tel = (x : A) (y : B) (z : C) (w : D) + -- ps = y@3 w@0 + -- vs = u v + -- newTel tel ps vs = (x : A) (z : C[u/y]) + newTel n tel [] [] = tel + newTel n tel (p : ps) (v : vs) = + case namedArg p of + VarP (DBPatVar _ i) -> newTel (n - 1) (subTel (size tel - 1 - i) v tel) (substP i (raise (n - 1) v) ps) vs + DotP{} -> newTel n tel ps vs + LitP{} -> __IMPOSSIBLE__ + ConP{} -> __IMPOSSIBLE__ + ProjP{} -> __IMPOSSIBLE__ + newTel _ tel _ _ = __IMPOSSIBLE__ + + -- subTel i v (Δ₁ (xᵢ : A) Δ₂) = Δ₁ Δ₂[xᵢ = v] + subTel i v EmptyTel = __IMPOSSIBLE__ + subTel 0 v (ExtendTel _ tel) = absApp tel v + subTel i v (ExtendTel a tel) = ExtendTel a $ subTel (i - 1) (raise 1 v) <$> tel instance Apply CompiledClauses where apply cc args = case cc of @@ -319,24 +410,19 @@ instance Apply FunctionInverse where apply NotInjective args = NotInjective apply (Inverse inv) args = Inverse $ apply inv args -instance Apply ClauseBody where - apply b [] = b - apply (Bind b) (a:args) = lazyAbsApp b (unArg a) `apply` args - apply (Body v) args = Body $ v `apply` args - apply NoBody _ = NoBody - applyE b [] = b - - applyE (Bind b) (Apply a : es) = lazyAbsApp b (unArg a) `applyE` es - applyE (Bind b) (Proj{} : es) = __IMPOSSIBLE__ - applyE (Body v) es = Body $ v `applyE` es - applyE NoBody _ = NoBody - instance Apply DisplayTerm where apply (DTerm v) args = DTerm $ apply v args apply (DDot v) args = DDot $ apply v args - apply (DCon c vs) args = DCon c $ vs ++ map (fmap DTerm) args + apply (DCon c ci vs) args = DCon c ci $ vs ++ map (fmap DTerm) args apply (DDef c es) args = DDef c $ es ++ map (Apply . fmap DTerm) args - apply (DWithApp v ws args') args = DWithApp v ws $ args' ++ args + apply (DWithApp v ws es) args = DWithApp v ws $ es ++ map Apply args + + applyE (DTerm v) es = DTerm $ applyE v es + applyE (DDot v) es = DDot $ applyE v es + applyE (DCon c ci vs) es = DCon c ci $ vs ++ map (fmap DTerm) ws + where ws = fromMaybe __IMPOSSIBLE__ $ allApplyElims es + applyE (DDef c es') es = DDef c $ es' ++ map (fmap DTerm) es + applyE (DWithApp v ws es') es = DWithApp v ws $ es' ++ es #if __GLASGOW_HASKELL__ >= 710 instance {-# OVERLAPPABLE #-} Apply t => Apply [t] where @@ -358,6 +444,10 @@ instance Apply v => Apply (Map k v) where apply x args = fmap (`apply` args) x applyE x es = fmap (`applyE` es) x +instance Apply v => Apply (HashMap k v) where + apply x args = fmap (`apply` args) x + applyE x es = fmap (`applyE` es) x + instance (Apply a, Apply b) => Apply (a,b) where apply (x,y) args = (apply x args, apply y args) applyE (x,y) es = (applyE x es , applyE y es ) @@ -401,10 +491,6 @@ piApply t args = -- * Abstraction --------------------------------------------------------------------------- --- | @(abstract args v) `apply` args --> v[args]@. -class Abstract t where - abstract :: Telescope -> t -> t - instance Abstract Term where abstract = teleLam @@ -420,15 +506,15 @@ instance Abstract Telescope where ExtendTel arg xtel `abstract` tel = ExtendTel arg $ xtel <&> (`abstract` tel) instance Abstract Definition where - abstract tel (Defn info x t pol occ df m c inst copy d) = - Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) df m c inst copy (abstract tel d) + abstract tel (Defn info x t pol occ df m c inst copy ma d) = + Defn info x (abstract tel t) (abstract tel pol) (abstract tel occ) df m c inst copy ma (abstract tel d) -- | @tel ⊢ (Γ ⊢ lhs ↦ rhs : t)@ becomes @tel, Γ ⊢ lhs ↦ rhs : t)@ -- we do not need to change lhs, rhs, and t since they live in Γ. -- See 'Abstract Clause'. instance Abstract RewriteRule where - abstract tel (RewriteRule q gamma lhs rhs t) = - RewriteRule q (abstract tel gamma) lhs rhs t + abstract tel (RewriteRule q gamma f ps rhs t) = + RewriteRule q (abstract tel gamma) f ps rhs t #if __GLASGOW_HASKELL__ >= 710 instance {-# OVERLAPPING #-} Abstract [Occ.Occurrence] where @@ -448,15 +534,18 @@ instance Abstract [Polarity] where instance Abstract Projection where abstract tel p = p - { projIndex = size tel + projIndex p - , projDropPars = abstract tel $ projDropPars p - , projArgInfo = if projIndex p > 0 then projArgInfo p else - domInfo $ last $ telToList tel + { projIndex = size tel + projIndex p + , projLams = abstract tel $ projLams p } +instance Abstract ProjLams where + abstract tel (ProjLams lams) = ProjLams $ + map (\ (Dom ai (x, _)) -> Arg ai x) (telToList tel) ++ lams + instance Abstract Defn where abstract tel d = case d of Axiom{} -> d + AbstractDefn -> d Function{ funClauses = cs, funCompiled = cc, funInv = inv , funProjection = Nothing } -> d { funClauses = abstract tel cs @@ -482,9 +571,8 @@ instance Abstract Defn where , dataNonLinPars = abstract tel nlps , dataClause = abstract tel cl } - Record{ recPars = np, recConType = t, recClause = cl, recTel = tel' } -> + Record{ recPars = np, recClause = cl, recTel = tel' } -> d { recPars = np + size tel - , recConType = abstract tel t , recClause = abstract tel cl , recTel = abstract tel tel' } @@ -500,7 +588,8 @@ instance Abstract PrimFun where instance Abstract Clause where abstract tel (Clause r tel' ps b t catchall) = Clause r (abstract tel tel') - (namedTelVars m tel ++ ps) (abstract tel b) + (namedTelVars m tel ++ ps) + b t -- nothing to do for t, since it lives under the telescope catchall where m = size tel + size tel' @@ -531,10 +620,6 @@ instance Abstract FunctionInverse where abstract tel NotInjective = NotInjective abstract tel (Inverse inv) = Inverse $ abstract tel inv -instance Abstract ClauseBody where - abstract EmptyTel b = b - abstract (ExtendTel _ tel) b = Bind $ fmap (`abstract` b) tel - #if __GLASGOW_HASKELL__ >= 710 instance {-# OVERLAPPABLE #-} Abstract t => Abstract [t] where #else @@ -548,6 +633,9 @@ instance Abstract t => Abstract (Maybe t) where instance Abstract v => Abstract (Map k v) where abstract tel m = fmap (abstract tel) m +instance Abstract v => Abstract (HashMap k v) where + abstract tel m = fmap (abstract tel) m + abstractArgs :: Abstract a => Args -> a -> a abstractArgs args x = abstract tel x where @@ -557,161 +645,24 @@ abstractArgs args x = abstract tel x names = cycle $ map (stringToArgName . (:[])) ['a'..'z'] --------------------------------------------------------------------------- --- * Explicit substitutions ---------------------------------------------------------------------------- - -class DeBruijn a where - debruijnVar :: Int -> a - debruijnVar = debruijnNamedVar underscore - debruijnNamedVar :: String -> Int -> a - debruijnNamedVar _ = debruijnVar - debruijnView :: a -> Maybe Int - -instance DeBruijn Term where - debruijnVar = var - debruijnView (Var n []) = Just n - debruijnView _ = Nothing - --- 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 - --- | 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__ - ---------------------------------------------------------------------------- -- * 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 +-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renaming _ π) : Term Γ -> Term Δ@ +renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a +renaming err p = prependS err gamma $ raiseS $ size p + where + gamma :: [Maybe a] + gamma = inversePermute p (deBruijnVar :: Int -> a) + -- gamma = safePermute (invertP (-1) p) $ map deBruijnVar [0..] -strengthen :: Subst t a => Empty -> a -> a -strengthen err = applySubst (compactS err [Nothing]) +-- | If @permute π : [a]Γ -> [a]Δ@, then @applySubst (renamingR π) : Term Δ -> Term Γ@ +renamingR :: DeBruijn a => Permutation -> Substitution' a +renamingR p@(Perm n _) = permute (reverseP p) (map deBruijnVar [0..]) ++# raiseS n --- | 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)) +-- | The permutation should permute the corresponding context. (right-to-left list) +renameP :: Subst t a => Empty -> Permutation -> a -> a +renameP err p = applySubst (renaming err p) instance Subst a a => Subst a (Substitution' a) where applySubst rho sgm = composeS rho sgm @@ -722,7 +673,7 @@ instance Subst Term Term where Var i es -> lookupS rho i `applyE` applySubst rho es Lam h m -> Lam h $ applySubst rho m Def f es -> defApp f [] $ applySubst rho es - Con c vs -> Con c $ applySubst rho vs + Con c ci vs -> Con c ci $ applySubst rho vs MetaV x es -> MetaV x $ applySubst rho es Lit l -> Lit l Level l -> levelTm $ applySubst rho l @@ -778,11 +729,11 @@ instance Subst Term Pattern where DotP t -> DotP $ applySubst rho t VarP s -> p LitP l -> p - ProjP _ -> p + ProjP{} -> p instance Subst Term NLPat where applySubst rho p = case p of - PVar id i -> p + PVar id i bvs -> p PWild -> p PDef f es -> PDef f $ applySubst rho es PLam i u -> PLam i $ applySubst rho u @@ -790,10 +741,13 @@ instance Subst Term NLPat where PBoundVar i es -> PBoundVar i $ applySubst rho es PTerm u -> PTerm $ applySubst rho u +instance Subst Term NLPType where + applySubst rho (NLPType s a) = NLPType (applySubst rho s) (applySubst rho a) + instance Subst Term RewriteRule where - applySubst rho (RewriteRule q gamma lhs rhs t) = + applySubst rho (RewriteRule q gamma f ps rhs t) = RewriteRule q (applySubst rho gamma) - (applySubst (liftS n rho) lhs) + f (applySubst (liftS n rho) ps) (applySubst (liftS n rho) rhs) (applySubst (liftS n rho) t) where n = size gamma @@ -809,9 +763,9 @@ instance Subst Term DisplayForm where instance Subst Term DisplayTerm where applySubst rho (DTerm v) = DTerm $ applySubst rho v applySubst rho (DDot v) = DDot $ applySubst rho v - applySubst rho (DCon c vs) = DCon c $ applySubst rho vs + applySubst rho (DCon c ci vs) = DCon c ci $ applySubst rho vs applySubst rho (DDef c es) = DDef c $ applySubst rho es - applySubst rho (DWithApp v vs ws) = uncurry3 DWithApp $ applySubst rho (v, vs, ws) + applySubst rho (DWithApp v vs es) = uncurry3 DWithApp $ applySubst rho (v, vs, es) instance Subst t a => Subst t (Tele a) where applySubst rho EmptyTel = EmptyTel @@ -833,6 +787,12 @@ instance Subst Term Constraint where where rf x = applySubst rho x +instance Subst Term ModuleParameters where + applySubst rho mp = mp { mpSubstitution = applySubst rho $ mpSubstitution mp } + +instance Subst Term A.NamedDotPattern where + applySubst rho (A.NamedDot x v a) = A.NamedDot x (applySubst rho v) (applySubst rho a) + instance Subst t a => Subst t (Elim' a) where applySubst rho e = case e of Apply v -> Apply $ applySubst rho v @@ -857,6 +817,9 @@ instance Subst t a => Subst t (Maybe a) where instance Subst t a => Subst t [a] where applySubst rho = map (applySubst rho) +instance (Ord k, Subst t a) => Subst t (Map k a) where + applySubst rho = fmap (applySubst rho) + instance Subst Term () where applySubst _ _ = () @@ -869,13 +832,8 @@ instance (Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) where instance (Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) where applySubst rho (x,y,z,u) = (applySubst rho x, applySubst rho y, applySubst rho z, applySubst rho u) -instance Subst Term ClauseBody where - applySubst rho (Body t) = Body $ applySubst rho t - applySubst rho (Bind b) = Bind $ applySubst rho b - applySubst _ NoBody = NoBody - instance Subst Term Candidate where - applySubst rho (Candidate u t eti) = Candidate (applySubst rho u) (applySubst rho t) eti + applySubst rho (Candidate u t eti ov) = Candidate (applySubst rho u) (applySubst rho t) eti ov instance Subst Term EqualityView where applySubst rho (OtherType t) = OtherType @@ -888,6 +846,53 @@ instance Subst Term EqualityView where (applySubst rho a) (applySubst rho b) +instance DeBruijn DeBruijnPattern where + debruijnNamedVar n i = VarP $ DBPatVar n i + deBruijnView (VarP x) = Just $ dbPatVarIndex x + deBruijnView _ = Nothing + +fromPatternSubstitution :: PatternSubstitution -> Substitution +fromPatternSubstitution = fmap patternToTerm + +applyPatSubst :: (Subst Term a) => PatternSubstitution -> a -> a +applyPatSubst = applySubst . fromPatternSubstitution + +instance Subst DeBruijnPattern DeBruijnPattern where + applySubst IdS p = p + applySubst rho p = case p of + VarP x -> useName (dbPatVarName x) $ lookupS rho $ dbPatVarIndex x + DotP u -> DotP $ applyPatSubst rho u + ConP c ci ps -> ConP c ci $ applySubst rho ps + LitP x -> p + ProjP{} -> p + where + useName :: PatVarName -> DeBruijnPattern -> DeBruijnPattern + useName n (VarP x) | isUnderscore (dbPatVarName x) = debruijnNamedVar n (dbPatVarIndex x) + useName _ x = x + +--------------------------------------------------------------------------- +-- * Projections +--------------------------------------------------------------------------- + +-- | @projDropParsApply proj o args = 'projDropPars' proj o `'apply'` args@ +-- +-- This function is an optimization, saving us from construction lambdas we +-- immediately remove through application. +projDropParsApply :: Projection -> ProjOrigin -> Args -> Term +projDropParsApply (Projection proper d r _ lams) o args = + case initLast $ getProjLams lams of + -- If we have no more abstractions, we must be a record field + -- (projection applied already to record value). + Nothing -> if proper then Def d $ map Apply args else __IMPOSSIBLE__ + Just (pars, Arg i y) -> + let core = if proper then Lam i $ Abs y $ Var 0 [Proj o d] + else Lam i $ Abs y $ Def d [Apply $ Var 0 [] <$ r] -- Issue2226: get ArgInfo for principal argument from projFromType + -- Now drop pars many args + (pars', args') = dropCommon pars args + -- We only have to abstract over the parameters that exceed the arguments. + -- We only have to apply to the arguments that exceed the parameters. + in List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (core `apply` args') pars' + --------------------------------------------------------------------------- -- * Telescopes --------------------------------------------------------------------------- @@ -1003,112 +1008,11 @@ instance TeleNoAbs ListTel where instance TeleNoAbs Telescope where teleNoAbs tel = teleNoAbs $ telToList tel --- | Dependent least upper bound, to assign a level to expressions --- like @forall i -> Set i@. --- --- @dLub s1 \i.s2 = \omega@ if @i@ appears in the rigid variables of @s2@. -dLub :: Sort -> Abs Sort -> Sort -dLub s1 (NoAbs _ s2) = sLub s1 s2 -dLub s1 b@(Abs _ s2) = case occurrence 0 s2 of - Flexible _ -> DLub s1 b - Irrelevantly -> DLub s1 b - NoOccurrence -> sLub s1 (noabsApp __IMPOSSIBLE__ b) --- Free.Unused -> sLub s1 (absApp b __IMPOSSIBLE__) -- triggers Issue784 - Free.Unused -> DLub s1 b - StronglyRigid -> Inf - Unguarded -> Inf - WeaklyRigid -> Inf - ---------------------------------------------------------------------------- --- * 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__ - --- | Methods to retrieve the 'clauseBody'. -class GetBody a where - getBody :: a -> Maybe Term - -- ^ Returns the properly raised clause 'Body', - -- and 'Nothing' if 'NoBody'. - getBodyUnraised :: a -> Maybe Term - -- ^ Just grabs the body, without raising the de Bruijn indices. - -- This is useful if you want to consider the body in context 'clauseTel'. - -instance GetBody ClauseBody where - getBody NoBody = Nothing - getBody (Body v) = Just v - getBody (Bind b) = getBody $ absBody b - - -- Andreas, 2014-08-25: The following 'optimization' is WRONG, - -- since it does not respect the order of Abs and NoAbs. - -- (They do not commute w.r.t. raise!!) - -- - -- getBody = body 0 - -- where - -- -- collect all shiftings and do them in the end in one go - -- body :: Int -> ClauseBody -> Maybe Term - -- body _ NoBody = Nothing - -- body n (Body v) = Just $ raise n v - -- body n (Bind (NoAbs _ v)) = body (n + 1) v - -- body n (Bind (Abs _ v)) = body n v - - getBodyUnraised NoBody = Nothing - getBodyUnraised (Body v) = Just v - getBodyUnraised (Bind b) = getBodyUnraised $ unAbs b -- Does not raise! - -instance GetBody Clause where - getBody = getBody . clauseBody - getBodyUnraised = getBodyUnraised . clauseBody +-- | In compiled clauses, the variables in the clause body are relative to the +-- pattern variables (including dot patterns) instead of the clause telescope. +compiledClauseBody :: Clause -> Maybe Term +compiledClauseBody cl = applySubst (renamingR perm) $ clauseBody cl + where perm = fromMaybe __IMPOSSIBLE__ $ clausePerm cl --------------------------------------------------------------------------- -- * Syntactic equality and order @@ -1129,8 +1033,6 @@ deriving instance Eq t => Eq (Blocked t) deriving instance Ord t => Ord (Blocked t) deriving instance Eq Candidate -deriving instance (Subst t a, Eq a) => Eq (Elim' a) -deriving instance (Subst t a, Ord a) => Ord (Elim' a) deriving instance (Subst t a, Eq a) => Eq (Tele a) deriving instance (Subst t a, Ord a) => Ord (Tele a) @@ -1160,7 +1062,7 @@ instance Eq Term where Lam h v == Lam h' v' = h == h' && v == v' Lit l == Lit l' = l == l' Def x vs == Def x' vs' = x == x' && vs == vs' - Con x vs == Con x' vs' = x == x' && vs == vs' + Con x _ vs == Con x' _ vs' = x == x' && vs == vs' Pi a b == Pi a' b' = a == a' && b == b' Sort s == Sort s' = s == s' Level l == Level l' = l == l' @@ -1181,7 +1083,7 @@ instance Ord Term where Def a b `compare` Def x y = compare (a, b) (x, y) Def{} `compare` _ = LT _ `compare` Def{} = GT - Con a b `compare` Con x y = compare (a, b) (x, y) + Con a _ b `compare` Con x _ y = compare (a, b) (x, y) Con{} `compare` _ = LT _ `compare` Con{} = GT Lit a `compare` Lit x = compare a x @@ -1214,6 +1116,17 @@ instance (Subst t a, Ord a) => Ord (Abs a) where Abs _ a `compare` Abs _ b = a `compare` b a `compare` b = absBody a `compare` absBody b +instance (Subst t a, Eq a) => Eq (Elim' a) where + Apply a == Apply b = a == b + Proj _ x == Proj _ y = x == y + _ == _ = False + +instance (Subst t a, Ord a) => Ord (Elim' a) where + Apply a `compare` Apply b = a `compare` b + Proj _ x `compare` Proj _ y = x `compare` y + Apply{} `compare` Proj{} = LT + Proj{} `compare` Apply{} = GT + --------------------------------------------------------------------------- -- * Level stuff --------------------------------------------------------------------------- @@ -1242,6 +1155,22 @@ sLub (DLub a NoAbs{}) c = __IMPOSSIBLE__ sLub (DLub a (Abs x b)) c = DLub a $ Abs x $ sLub b $ raise 1 c sLub a (DLub b c) = DLub (sLub a b) c +-- | Dependent least upper bound, to assign a level to expressions +-- like @forall i -> Set i@. +-- +-- @dLub s1 \i.s2 = \omega@ if @i@ appears in the rigid variables of @s2@. +dLub :: Sort -> Abs Sort -> Sort +dLub s1 (NoAbs _ s2) = sLub s1 s2 +dLub s1 b@(Abs _ s2) = case occurrence 0 s2 of + Flexible _ -> DLub s1 b + Irrelevantly -> DLub s1 b + NoOccurrence -> sLub s1 (noabsApp __IMPOSSIBLE__ b) +-- Free.Unused -> sLub s1 (absApp b __IMPOSSIBLE__) -- triggers Issue784 + Free.Unused -> DLub s1 b + StronglyRigid -> Inf + Unguarded -> Inf + WeaklyRigid -> Inf + lvlView :: Term -> Level lvlView v = case ignoreSharing v of Level l -> l |