Allow @ in constructor declarations (#3099)

* Closes #3041 
* The old syntax without `@` is still accepted, but the formatter
changes it to the new syntax

CODING.md

@@ -129,7 +129,7 @@ Example:
 ```
 type BinaryTree (A : Type) :=
   | leaf
-  | node {
+  | node@{
       left : BinaryTree A;
       element : A;
       right : BinaryTree A

examples/demo/Demo.juvix

@@ -18,8 +18,8 @@ log2 (n : Nat) : Nat :=
     | else := log2 (div n 2) + 1;
 
 type Tree (A : Type) :=
-  | leaf {element : A}
-  | node {
+  | leaf@{element : A}
+  | node@{
       element : A;
       left : Tree A;
       right : Tree A

examples/milestone/Bank/Bank.juvix

@@ -14,7 +14,7 @@ bankAddress : Address := 1234;
 
 type Token :=
   --- Arguments are: owner, gates, amount.
-  mkToken {
+  mkToken@{
     owner : Address;
     gates : Nat;
     amount : Nat

examples/milestone/Hanoi/Hanoi.juvix

@@ -39,7 +39,7 @@ showPeg : Peg -> String
 
 --- A Move represents a move between pegs
 type Move :=
-  mkMove {
+  mkMove@{
     from : Peg;
     to : Peg
   };

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -7,7 +7,7 @@ import Logic.Symbol open public;
 import Logic.Extra open;
 
 --- A 3x3 grid of ;Square;s
-type Board := mkBoard {squares : List (List Square)};
+type Board := mkBoard@{squares : List (List Square)};
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
 possibleMoves : (list : List Square) -> List Nat

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -13,7 +13,7 @@ type Error :=
     terminate : String → Error;
 
 type GameState :=
-  mkGameState {
+  mkGameState@{
     board : Board;
     player : Symbol;
     error : Error

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -7,9 +7,9 @@ import Logic.Extra open;
 --- A square is each of the holes in a board
 type Square :=
   | --- An empty square has a ;Nat; that uniquely identifies it
-    empty {id : Nat}
+    empty@{id : Nat}
   | --- An occupied square has a ;Symbol; in it
-    occupied {player : Symbol};
+    occupied@{player : Symbol};
 
 instance
 eqSquareI : Eq Square :=

juvix-stdlib

@@ -1 +1 @@
-Subproject commit ff351799c068e7b3e23dd903547d228dc30aff5e
+Subproject commit e164aa14503ff11dbcf0dc96bcd4cfa4d757b76d

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)

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 (_, l, r) = _rhsRecordDelim
         fields'
           | [] <- _rhsRecordStatements = mempty
           | [f] <- _rhsRecordStatements = ppCode f
@@ -1436,7 +1436,7 @@ instance (SingI s) => PrettyPrint (RhsRecord s) where
                       (ppCode <$> _rhsRecordStatements)
                   )
                 <> hardline
-    ppCode l <> fields' <> ppCode r
+    ppCode kwAt <> ppCode l <> fields' <> ppCode r
 
 instance (SingI s) => PrettyPrint (RhsAdt s) where
   ppCode = align . sep . fmap ppExpressionAtomType . (^. rhsAdtArguments)
@@ -1461,7 +1461,7 @@ ppConstructorDef singleConstructor ConstructorDef {..} = do
       where
         spaceMay = case r of
           ConstructorRhsGadt {} -> space
-          ConstructorRhsRecord {} -> space
+          ConstructorRhsRecord {} -> mempty
           ConstructorRhsAdt a
             | null (a ^. rhsAdtArguments) -> mempty
             | otherwise -> space

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)

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@{

tests/positive/Format.juvix

@@ -280,7 +280,7 @@ end;
 module EmptyRecords;
   import Stdlib.Data.Bool.Base open;
 
-  type T := mkT {};
+  type T := mkT@{};
 
   x : T := mkT@{};
 
@@ -294,7 +294,7 @@ module Traits;
   import Stdlib.Prelude open hiding {Show; mkShow; module Show};
 
   trait
-  type Show A := mkShow {show : A → String};
+  type Show A := mkShow@{show : A → String};
 
   instance
   showStringI : Show String :=
@@ -354,7 +354,7 @@ end;
 module OperatorRecord;
   trait
   type Natural A :=
-    myNatural {
+    myNatural@{
       syntax operator + additive;
       + : A -> A -> A;
 
@@ -372,7 +372,7 @@ end;
 
 module RecordFieldPragmas;
   type Pr (A B : Type) :=
-    mkPr {
+    mkPr@{
       --- Judoc for A
       {-# inline: false #-}
       pfst : A;

tests/positive/InstanceImport/M.juvix

@@ -1,7 +1,7 @@
 module M;
 
 trait
-type T A := mkT {pp : A → A};
+type T A := mkT@{pp : A → A};
 
 type Unit := unit;
 

tests/positive/Internal/Positivity2/main.juvix

@@ -53,7 +53,7 @@ module E6;
     | zero
     | suc Nat;
 
-  type Box := mkBox {unbox : Nat};
+  type Box := mkBox@{unbox : Nat};
 
-  type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
+  type Foldable := mkFoldable@{for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
 end;

tests/positive/Isabelle/Program.juvix

@@ -111,13 +111,13 @@ type Either' A B :=
 
 {-# isabelle-ignore: true #-}
 type R' :=
-  mkR' {
+  mkR'@{
     r1' : Nat;
     r2' : Nat
   };
 
 type R :=
-  mkR {
+  mkR@{
     r1 : Nat;
     r2 : Nat
   };

tests/positive/Puns.juvix

@@ -5,7 +5,7 @@ type A := a;
 type B := b;
 
 type S :=
-  mkS {
+  mkS@{
     fieldA : A;
     fieldB : B;
     fieldC : A;

tests/positive/RecordIterator.juvix

@@ -2,7 +2,7 @@ module RecordIterator;
 
 trait
 type Foldable (container elem : Type) :=
-  mkFoldable {
+  mkFoldable@{
     syntax iterator for {init := 1; range := 1};
     for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
 

tests/positive/Termination/issue2414.juvix

@@ -3,7 +3,7 @@ module issue2414;
 import Stdlib.Prelude open;
 
 trait
-type T := mkT {tt : T};
+type T := mkT@{tt : T};
 
 f {{T}} : Nat → Nat
   | zero := zero