From 13938edab7d5aabbc3d9634561c1a2de0b3a63a3 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Fri, 21 Nov 2025 16:13:37 +0100
Subject: [PATCH] Implement 'existing' keyword for skipping compilation of a
 symbol

This is useful for things that are defined in a FOREIGN pragma, either by importing from a Haskell module or as an inline Haskell definition
---
 src/Agda2Hs/Compile.hs       | 3 ++-
 src/Agda2Hs/Compile/Utils.hs | 1 +
 src/Agda2Hs/Pragma.hs        | 2 ++
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index f76cc499..d98bbd4b 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -117,7 +117,8 @@ compile genv tlm _ def =
 
       case (p , theDef def) of
         (NoPragma            , _         ) -> return []
-        (ExistingClassPragma , _         ) -> return []
+        (ExistingPragma      , _         ) -> return []
+        (ExistingClassPragma , Record{}  ) -> return []
         (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index b228d0be..24fffec4 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -195,6 +195,7 @@ hasCompilePragma q = processPragma q <&> \case
   InlinePragma{} -> True
   DefaultPragma{} -> True
   ClassPragma{} -> True
+  ExistingPragma{} -> True
   ExistingClassPragma{} -> True
   UnboxPragma{} -> True
   TransparentPragma{} -> True
diff --git a/src/Agda2Hs/Pragma.hs b/src/Agda2Hs/Pragma.hs
index 1f6a5822..d8f42235 100644
--- a/src/Agda2Hs/Pragma.hs
+++ b/src/Agda2Hs/Pragma.hs
@@ -51,6 +51,7 @@ data ParsedPragma
   | InlinePragma
   | DefaultPragma [Hs.Deriving ()]
   | ClassPragma [String]
+  | ExistingPragma
   | ExistingClassPragma
   | UnboxPragma Strictness
   | TransparentPragma
@@ -89,6 +90,7 @@ processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case
   Just (CompilerPragma r s)
     | "class" `isPrefixOf` s      -> return $ ClassPragma (words $ drop 5 s)
     | s == "inline"               -> return InlinePragma
+    | s == "existing"             -> return ExistingPragma
     | s == "existing-class"       -> return ExistingClassPragma
     | s == "unboxed"              -> return $ UnboxPragma Lazy
     | s == "unboxed-strict"       -> return $ UnboxPragma Strict