Implement 'existing' keyword for skipping compilation of a symbol

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

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

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