summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Substitute.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Substitute.hs')
-rw-r--r--src/full/Agda/TypeChecking/Substitute.hs643
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