Allow @ in constructor declarations

anoma · Oct 15, 2024 · ed51cc6 · ed51cc6
1 parent 8353914
commit ed51cc6
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 16 deletions.
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -813,7 +813,7 @@ deriving stock instance Ord (RhsAdt 'Parsed)
 deriving stock instance Ord (RhsAdt 'Scoped)
 
 data RhsRecord (s :: Stage) = RhsRecord
-  { _rhsRecordDelim :: Irrelevant (KeywordRef, KeywordRef),
+  { _rhsRecordDelim :: Irrelevant (Maybe KeywordRef, KeywordRef, KeywordRef),
     _rhsRecordStatements :: [RecordStatement s]
   }
   deriving stock (Generic)

diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1424,7 +1424,7 @@ instance (SingI s) => PrettyPrint (RecordField s) where
 
 instance (SingI s) => PrettyPrint (RhsRecord s) where
   ppCode RhsRecord {..} = do
-    let Irrelevant (l, r) = _rhsRecordDelim
+    let Irrelevant (kwat, l, r) = _rhsRecordDelim
         fields'
           | [] <- _rhsRecordStatements = mempty
           | [f] <- _rhsRecordStatements = ppCode f
@@ -1436,7 +1436,8 @@ instance (SingI s) => PrettyPrint (RhsRecord s) where
                       (ppCode <$> _rhsRecordStatements)
                   )
                 <> hardline
-    ppCode l <> fields' <> ppCode r
+        a = ppCode <$> kwat
+    a ?<> ppCode l <> fields' <> ppCode r
 
 instance (SingI s) => PrettyPrint (RhsAdt s) where
   ppCode = align . sep . fmap ppExpressionAtomType . (^. rhsAdtArguments)
@@ -1461,7 +1462,9 @@ ppConstructorDef singleConstructor ConstructorDef {..} = do
       where
         spaceMay = case r of
           ConstructorRhsGadt {} -> space
-          ConstructorRhsRecord {} -> space
+          ConstructorRhsRecord RhsRecord {..}
+            | isJust (fst3 (_rhsRecordDelim ^. unIrrelevant)) -> mempty
+            | otherwise -> space
           ConstructorRhsAdt a
             | null (a ^. rhsAdtArguments) -> mempty
             | otherwise -> space

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1589,10 +1589,11 @@ rhsAdt = P.label "<constructor arguments>" $ do
 
 rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsRecord 'Parsed)
 rhsRecord = P.label "<constructor record>" $ do
+  a <- optional (kw kwAt)
   l <- kw delimBraceL
   _rhsRecordStatements <- P.sepEndBy recordStatement semicolon
   r <- kw delimBraceR
-  let _rhsRecordDelim = Irrelevant (l, r)
+  let _rhsRecordDelim = Irrelevant (a, l, r)
   return RhsRecord {..}
 
 recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordStatement 'Parsed)

diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix
@@ -4,33 +4,27 @@ module test060;
 import Stdlib.Prelude open hiding {fst};
 
 type Triple (A B C : Type) :=
-  mkTriple {
+  mkTriple@{
     fst : A;
     snd : B;
     thd : C
   };
 
 type Pair' (A B : Type) :=
-  mkPair {
+  mkPair@{
     fst : A;
     snd : B
   };
 
 mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool
-  | mkPair@{fst := mkPair@{fst; snd := nil};
-           snd := zero :: _} := fst
+  | mkPair@{fst := mkPair@{fst; snd := nil}; snd := zero :: _} := fst
   | x := case x of _ := false;
 
 main : Triple Nat Nat Nat :=
   let
     p : Triple Nat Nat Nat := mkTriple 2 2 2;
-    p' : Triple Nat Nat Nat :=
-      p@Triple{
-        fst := fst + 1;
-        snd := snd * 3 + thd + fst
-      };
-    f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
-      (@Triple{fst := fst * 10});
+    p' : Triple Nat Nat Nat := p@Triple{fst := fst + 1; snd := snd * 3 + thd + fst};
+    f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple{fst := fst * 10});
   in if
     | mf
       mkPair@{