From 46d73889ae26f8c0d0b34c666ef1b35ad2af859e Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 19 Nov 2024 18:18:22 +0100
Subject: [PATCH] pragmas

---
 src/Juvix/Compiler/Concrete/Language/Base.hs           |  3 ++-
 src/Juvix/Compiler/Concrete/Translation/FromSource.hs  |  1 +
 .../Compiler/Internal/Translation/FromConcrete.hs      | 10 ++++++----
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index c009fd0b1b..7505c8f065 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -648,7 +648,8 @@ deriving stock instance Ord (FunctionDefBody 'Parsed)
 deriving stock instance Ord (FunctionDefBody 'Scoped)
 
 data Deriving (s :: Stage) = Deriving
-  { _derivingKw :: KeywordRef,
+  { _derivingPragmas :: Maybe ParsedPragmas,
+    _derivingKw :: KeywordRef,
     _derivingFunLhs :: FunctionLhs s
   }
   deriving stock (Generic)
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 66cc7d0877..3e7d32a8cb 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -458,6 +458,7 @@ derivingInstance ::
   ParsecS r (Deriving 'Parsed)
 derivingInstance = do
   _derivingKw <- kw kwDeriving
+  _derivingPragmas <- getPragmas
   let opts =
         FunctionSyntaxOptions
           { _funAllowOmitType = False,
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 32a90494af..103318a96c 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -71,7 +71,6 @@ newtype DefaultArgsStack = DefaultArgsStack
 
 makeLenses ''DefaultArgsStack
 
--- TODO use Store.moduletable for deriving
 fromConcrete ::
   (Members '[Reader EntryPoint, Error JuvixError, Reader Store.ModuleTable, NameIdGen, Termination] r) =>
   Scoper.ScoperResult ->
@@ -421,7 +420,7 @@ goDeriving Deriving {..} = do
   (funArgs, ret) <- Internal.unfoldFunType <$> goDefType _derivingFunLhs
   let (mtrait, traitArgs) = Internal.unfoldExpressionApp ret
   (n, der) <- findDerivingTrait mtrait
-  deriveTrait der name funArgs (n, traitArgs)
+  deriveTrait der _derivingPragmas name funArgs (n, traitArgs)
 
 deriveTrait ::
   ( Members
@@ -436,6 +435,7 @@ deriveTrait ::
       r
   ) =>
   Internal.DerivingTrait ->
+  Maybe ParsedPragmas ->
   Internal.Name ->
   [Internal.FunctionParameter] ->
   (Internal.InductiveName, [Internal.ApplicationArg]) ->
@@ -526,22 +526,24 @@ deriveEq ::
        ]
       r
   ) =>
+  Maybe ParsedPragmas ->
   Internal.FunctionName ->
   [Internal.FunctionParameter] ->
   (Internal.InductiveName, [Internal.ApplicationArg]) ->
   Sem r Internal.FunctionDef
-deriveEq instanceName funParams (eqName, args) = do
+deriveEq pragmas instanceName funParams (eqName, args) = do
   arg <- getArg
   argsInfo <- goArgsInfo instanceName
   lam <- eqLambda arg
   mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq
   let body = mkEq Internal.@@ lam
       ty = Internal.foldFunType funParams (Internal.foldApplication (Internal.toExpression eqName) args)
+  pragmas' <- goPragmas pragmas
   return
     Internal.FunctionDef
       { _funDefTerminating = False,
         _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance,
-        _funDefPragmas = mempty,
+        _funDefPragmas = pragmas',
         _funDefArgsInfo = argsInfo,
         _funDefDocComment = Nothing,
         _funDefName = instanceName,