[ new ] Added real higher-order matching to rewriting machinery

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -1086,8 +1086,9 @@ defRelevance = argInfoRelevance . defArgInfo
 
 -- | Non-linear (non-constructor) first-order pattern.
 data NLPat
-  = PVar (Maybe CtxId) !Int
-    -- ^ Matches anything (modulo non-linearity).
+  = PVar (Maybe CtxId) !Int [Arg Int]
+    -- ^ Matches anything (modulo non-linearity) that only contains bound
+    --   variables that occur in the given arguments.
   | PWild
     -- ^ Matches anything (e.g. irrelevant terms).
   | PDef QName PElims
@@ -2622,7 +2623,7 @@ instance KillRange CtxId where
   killRange (CtxId x) = killRange1 CtxId x
 
 instance KillRange NLPat where
-  killRange (PVar x y) = killRange1 PVar x y
+  killRange (PVar x y z) = killRange3 PVar x y z
   killRange (PWild)    = PWild
   killRange (PDef x y) = killRange2 PDef x y
   killRange (PLam x y) = killRange2 PLam x y

src/full/Agda/TypeChecking/Pretty.hs

@@ -389,7 +389,7 @@ instance PrettyTCM (Elim' DisplayTerm) where
   prettyTCM (Proj f)  = text "." <> prettyTCM f
 
 raisePatVars :: Int -> NLPat -> NLPat
-raisePatVars k (PVar id x) = PVar id (k+x)
+raisePatVars k (PVar id x bvs) = PVar id (k+x) bvs
 raisePatVars k (PWild)     = PWild
 raisePatVars k (PDef f es) = PDef f $ (fmap . fmap) (raisePatVars k) es
 raisePatVars k (PLam i u)  = PLam i $ fmap (raisePatVars k) u
@@ -398,7 +398,7 @@ raisePatVars k (PBoundVar i es) = PBoundVar i $ (fmap . fmap) (raisePatVars k) e
 raisePatVars k (PTerm t)   = PTerm t
 
 instance PrettyTCM NLPat where
-  prettyTCM (PVar id x) = prettyTCM (var x)
+  prettyTCM (PVar id x bvs) = prettyTCM (Var x (map (Apply . fmap var) bvs))
   prettyTCM (PWild)     = text $ "_"
   prettyTCM (PDef f es) = parens $
     prettyTCM f <+> fsep (map prettyTCM es)

src/full/Agda/TypeChecking/Reduce.hs

@@ -1167,7 +1167,7 @@ instance InstantiateFull Definition where
       return $ Defn rel x t pol occ df i c inst copy d
 
 instance InstantiateFull NLPat where
-  instantiateFull' (PVar x y) = return $ PVar x y
+  instantiateFull' (PVar x y z) = return $ PVar x y z
   instantiateFull' (PWild)    = return PWild
   instantiateFull' (PDef x y) = PDef <$> instantiateFull' x <*> instantiateFull' y
   instantiateFull' (PLam x y) = PLam x <$> instantiateFull' y

src/full/Agda/TypeChecking/Rewriting.hs

@@ -350,7 +350,7 @@ instance (Foldable f, NLPatVars a) => NLPatVars (f a) where
 instance NLPatVars NLPat where
   nlPatVars p =
     case p of
-      PVar _ i  -> singleton i
+      PVar _ i _ -> singleton i
       PDef _ es -> nlPatVars es
       PWild     -> empty
       PLam _ p' -> nlPatVars $ unAbs p'
@@ -375,7 +375,7 @@ instance KillCtxId RewriteRule where
 
 instance KillCtxId NLPat where
   killCtxId p = case p of
-    PVar _ i       -> PVar Nothing i
+    PVar _ i bvs   -> PVar Nothing i bvs
     PWild          -> p
     PDef f es      -> PDef f $ killCtxId es
     PLam i x       -> PLam i $ killCtxId x

src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs

@@ -38,8 +38,7 @@ import Data.Foldable ( foldMap )
 #endif
 
 import Data.Maybe
-import Data.Functor
-import Data.Traversable hiding (for)
+import Data.Traversable (Traversable,traverse)
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.IntSet (IntSet)
@@ -57,13 +56,16 @@ import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Reduce
 import Agda.TypeChecking.Reduce.Monad
 import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Telescope (renameP, permuteTel)
 
 import Agda.Utils.Either
 import Agda.Utils.Except
 import Agda.Utils.Functor
+import Agda.Utils.List
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Null
+import Agda.Utils.Permutation
 import Agda.Utils.Singleton
 import Agda.Utils.Size
 
@@ -99,14 +101,23 @@ instance PatternFrom Term NLPat where
     case ignoreSharing v of
       Var i es
        | i < k     -> PBoundVar i <$> patternFrom k es
-       | null es   -> do
-           let i' = i-k
-           -- Pattern variables are labeled with their context id, because they
-           -- can only be instantiated once they're no longer bound by the
-           -- context (see Issue 1652).
-           id <- (!! i') <$> getContextId
-           return $ PVar (Just id) i'
-       | otherwise -> done
+       | otherwise -> do
+         -- The arguments of `var i` should be distinct bound variables
+         -- in order to build a Miller pattern
+         let mbvs = mfilter fastDistinct $ forM es $ \e -> do
+                      e <- isApplyElim e
+                      case ignoreSharing $ unArg e of
+                        Var j [] | j < k -> Just $ e $> j
+                        _                -> Nothing
+         case mbvs of
+           Just bvs -> do
+             let i' = i-k
+             -- Pattern variables are labeled with their context id, because they
+             -- can only be instantiated once they're no longer bound by the
+             -- context (see Issue 1652).
+             id <- (!! i') <$> getContextId
+             return $ PVar (Just id) i' bvs
+           Nothing -> done
       Lam i t  -> PLam i <$> patternFrom k t
       Lit{}    -> done
       Def f es -> PDef f <$> patternFrom k es
@@ -229,7 +240,7 @@ instance Match NLPat Term where
             , msg ]) mzero
     case p of
       PWild  -> yes
-      PVar id i -> do
+      PVar id i bvs -> do
         -- If the variable is still bound by the current context, we cannot
         -- instantiate it so it has to match on the nose (see Issue 1652).
         ctx <- zip <$> getContextNames <*> getContextId
@@ -242,9 +253,15 @@ instance Match NLPat Term where
           Nothing -> do
             let boundVarOccs :: FreeVars
                 boundVarOccs = runFree (\var@(i,_) -> if i < n then singleton var else empty) IgnoreNot v
-            if null (rigidVars boundVarOccs)
-               then if null (flexibleVars boundVarOccs)
-                    then tellSub i (raise (-n) v)
+                allowedVars :: IntSet
+                allowedVars = IntSet.fromList (map unArg bvs)
+                perm :: Permutation
+                perm = Perm n $ reverse $ map unArg $ bvs
+                tel :: Telescope
+                tel = permuteTel perm k
+            if rigidVars boundVarOccs `IntSet.isSubsetOf` allowedVars
+               then if IntMap.keysSet (flexibleVars boundVarOccs) `IntSet.isSubsetOf` allowedVars
+                    then tellSub i $ teleLam tel $ renameP perm v
                     else matchingBlocked $ foldMap (foldMap $ \m -> Blocked m ()) $ flexibleVars boundVarOccs
                else no (text "")
       PDef f ps -> do
@@ -345,7 +362,8 @@ instance RaiseNLP a => RaiseNLP (Abs a) where
 
 instance RaiseNLP NLPat where
   raiseNLPFrom c k p = case p of
-    PVar _ _ -> p
+    PVar id i bvs -> let raise j = if j < c then j else j + k
+                     in PVar id i $ map (fmap raise) bvs
     PWild  -> p
     PDef f ps -> PDef f $ raiseNLPFrom c k ps
     PLam i q -> PLam i $ raiseNLPFrom c k q

src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs

@@ -208,7 +208,7 @@ instance EmbPrj Definition where
     valu _                                 = malformed
 
 instance EmbPrj NLPat where
-  icod_ (PVar a b)      = icode2 0 a b
+  icod_ (PVar a b c)    = icode3 0 a b c
   icod_ (PWild)         = icode0 1
   icod_ (PDef a b)      = icode2 2 a b
   icod_ (PLam a b)      = icode2 3 a b
@@ -217,14 +217,14 @@ instance EmbPrj NLPat where
   icod_ (PTerm a)       = icode1 6 a
 
   value = vcase valu where
-    valu [0, a, b] = valu2 PVar a b
-    valu [1]       = valu0 PWild
-    valu [2, a, b] = valu2 PDef a b
-    valu [3, a, b] = valu2 PLam a b
-    valu [4, a, b] = valu2 PPi a b
-    valu [5, a, b] = valu2 PBoundVar a b
-    valu [6, a]    = valu1 PTerm a
-    valu _         = malformed
+    valu [0, a, b, c] = valu3 PVar a b c
+    valu [1]          = valu0 PWild
+    valu [2, a, b]    = valu2 PDef a b
+    valu [3, a, b]    = valu2 PLam a b
+    valu [4, a, b]    = valu2 PPi a b
+    valu [5, a, b]    = valu2 PBoundVar a b
+    valu [6, a]       = valu1 PTerm a
+    valu _            = malformed
 
 instance EmbPrj RewriteRule where
   icod_ (RewriteRule a b c d e) = icode5' a b c d e

src/full/Agda/TypeChecking/Substitute.hs

@@ -782,7 +782,7 @@ instance Subst Term Pattern where
 
 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

test/Succeed/HORewriting.agda

@@ -0,0 +1,37 @@
+{-# OPTIONS --rewriting #-}
+
+open import Common.Nat
+open import Common.Equality
+
+postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set
+
+{-# BUILTIN REWRITE _↦_ #-}
+
+postulate
+  P : ∀ {a} {A : Set a} → A → Set
+
+postulate rew₁ : (f : Nat → Nat → Nat) → P (λ (x y z : Nat) → f z x) ↦ P f
+
+{-# REWRITE rew₁ #-}
+
+f : Nat → Nat → Nat → Nat
+f x _ z = x + z
+
+test : P f ≡ P (λ x z → z + x)
+test = refl
+
+postulate rew₂ : (f : Nat → Nat) → P (λ (x y : Nat) → f y) ↦ P f
+
+{-# REWRITE rew₂ #-}
+
+g : Nat → Nat → Nat
+g x y = y
+
+test₂ : P g ≡ P (λ (y : Nat) → y)
+test₂ = refl
+
+h : Nat → Nat → Nat → Nat
+h x y z = x
+
+test₃ : P h ≡ P (λ (z : Nat) → z)
+test₃ = refl