propagate isabelle-ignore to record fields

anoma · Aug 14, 2024 · 5e59ce1 · 5e59ce1
1 parent 5a47874
commit 5e59ce1
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 13 deletions.
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1573,8 +1573,8 @@ checkSections sec = topBindings helper
                                 failMaybe $
                                   mkRec
                                     ^? constructorRhs
-                                      . _ConstructorRhsRecord
-                                      . to mkRecordNameSignature
+                                    . _ConstructorRhsRecord
+                                    . to mkRecordNameSignature
                               let info =
                                     RecordInfo
                                       { _recordInfoSignature = fs,
@@ -1650,14 +1650,27 @@ checkSections sec = topBindings helper
                                   _projectionKind = kind,
                                   _projectionFieldBuiltin = field ^. fieldBuiltin,
                                   _projectionDoc = field ^. fieldDoc,
-                                  _projectionPragmas = field ^. fieldPragmas
+                                  _projectionPragmas = combinePragmas (i ^. inductivePragmas) (field ^. fieldPragmas)
                                 }
                               where
                                 kind :: ProjectionKind
                                 kind = case field ^. fieldIsImplicit of
                                   ExplicitField -> ProjectionExplicit
                                   ImplicitInstanceField -> ProjectionCoercion
 
+                                combinePragmas :: Maybe ParsedPragmas -> Maybe ParsedPragmas -> Maybe ParsedPragmas
+                                combinePragmas p1 p2 = case (p1, p2) of
+                                  (Nothing, Nothing) -> Nothing
+                                  (Just p, Nothing) -> Just p
+                                  (Nothing, Just p) -> Just p
+                                  (Just p1', Just p2') ->
+                                    Just
+                                      ( over
+                                          (withLocParam . withSourceValue . pragmasIsabelleIgnore)
+                                          (\i2 -> i2 <|> (p1' ^. withLocParam . withSourceValue . pragmasIsabelleIgnore))
+                                          p2'
+                                      )
+
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
                             getFields = case i ^. inductiveConstructors of
                               c :| [] -> case c ^. constructorRhs of

diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
@@ -99,16 +99,6 @@ datatype ('A, 'B) Either'
   = Left' 'A |
     Right' 'B
 
-record R =
-  r1 :: nat
-  r2 :: nat
-
-fun r1 :: "R \<Rightarrow> nat" where
-  "r1 (mkR r1' r2') = r1'"
-
-fun r2 :: "R \<Rightarrow> nat" where
-  "r2 (mkR r1' r2') = r2'"
-
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bf b1 b2 = (\<not> (b1 \<and> b2))"