0001-drop-forced-args-from-termination.patch

From 12bb502c978c8aca394e45def80e0717d912f431 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Sun, 21 May 2023 20:42:57 +0200
Subject: [PATCH] drop forced args from termination

---
 src/full/Agda/Termination/TermCheck.hs | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs
index 62e237ea0..7d6fb5b36 100644
--- a/src/full/Agda/Termination/TermCheck.hs
+++ b/src/full/Agda/Termination/TermCheck.hs
@@ -51,6 +51,7 @@ import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.Functions
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.Forcing
 import Agda.TypeChecking.Records -- (isRecordConstructor, isInductiveRecord)
 import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull, appDefE')
 import Agda.TypeChecking.SizedTypes
@@ -1471,9 +1472,19 @@ compareVar i (Masked m p) = do
     ConP s _ [p] | Just (conName s) == suc ->
       setUsability True . decrease 1 <$> compareVar i (notMasked $ namedArg p)
 
-    ConP c _ ps -> if m then no else setUsability True <$> do
+    ConP c pi ps -> if m then no else setUsability True <$> do
+      forcedArgs <- getForcedArgs $ conName c
+      let ps' = go forcedArgs ps
+          go xs (p:ps) = case nextIsForced xs of
+            (Forced, xs) -> go xs ps
+            (NotForced, xs) -> p:go xs ps
+          go _ [] = []
+      reportSDoc "term.forced" 30 $
+        vcat [ "pattern before:" <+> pretty (ConP c pi ps)
+             , "pattern after: " <+> pretty (ConP c pi ps')
+             ]
       decrease <$> offsetFromConstructor (conName c)
-               <*> (Order.supremum <$> mapM (compareVar i . notMasked . namedArg) ps)
+               <*> (Order.supremum <$> mapM (compareVar i . notMasked . namedArg) ps')
     DefP _ c ps -> if m then no else setUsability True <$> do
       decrease <$> offsetFromConstructor c
                <*> (Order.supremum <$> mapM (compareVar i . notMasked . namedArg) ps)
-- 
2.39.2 (Apple Git-143)