From feb422d445134d0be0212545935aa65c3db17e9e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Tue, 15 Oct 2024 19:15:37 +0200 Subject: [PATCH] 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 | 2 +- examples/demo/Demo.juvix | 4 ++-- examples/milestone/Bank/Bank.juvix | 2 +- examples/milestone/Hanoi/Hanoi.juvix | 2 +- examples/milestone/TicTacToe/Logic/Board.juvix | 2 +- .../milestone/TicTacToe/Logic/GameState.juvix | 2 +- examples/milestone/TicTacToe/Logic/Square.juvix | 4 ++-- juvix-stdlib | 2 +- src/Juvix/Compiler/Concrete/Language/Base.hs | 2 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 6 +++--- .../Compiler/Concrete/Translation/FromSource.hs | 3 ++- tests/Compilation/positive/test060.juvix | 16 +++++----------- tests/positive/Format.juvix | 8 ++++---- tests/positive/InstanceImport/M.juvix | 2 +- tests/positive/Internal/Positivity2/main.juvix | 4 ++-- tests/positive/Isabelle/Program.juvix | 4 ++-- tests/positive/Puns.juvix | 2 +- tests/positive/RecordIterator.juvix | 2 +- tests/positive/Termination/issue2414.juvix | 2 +- 19 files changed, 33 insertions(+), 38 deletions(-) diff --git a/CODING.md b/CODING.md index 8c67279e28..3cb1e16738 100644 --- a/CODING.md +++ b/CODING.md @@ -129,7 +129,7 @@ Example: ``` type BinaryTree (A : Type) := | leaf - | node { + | node@{ left : BinaryTree A; element : A; right : BinaryTree A diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix index 06a4e91fcd..f05c175d80 100644 --- a/examples/demo/Demo.juvix +++ b/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 diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix index ad1f7b128b..c40c61b7f6 100644 --- a/examples/milestone/Bank/Bank.juvix +++ b/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 diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix index c641593b4d..e750eeb366 100644 --- a/examples/milestone/Hanoi/Hanoi.juvix +++ b/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 }; diff --git a/examples/milestone/TicTacToe/Logic/Board.juvix b/examples/milestone/TicTacToe/Logic/Board.juvix index 28cfa06674..48782c3654 100644 --- a/examples/milestone/TicTacToe/Logic/Board.juvix +++ b/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 diff --git a/examples/milestone/TicTacToe/Logic/GameState.juvix b/examples/milestone/TicTacToe/Logic/GameState.juvix index 24853ef0a4..2547010256 100644 --- a/examples/milestone/TicTacToe/Logic/GameState.juvix +++ b/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 diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix index 46c8ecea20..d942795345 100644 --- a/examples/milestone/TicTacToe/Logic/Square.juvix +++ b/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 := diff --git a/juvix-stdlib b/juvix-stdlib index ff351799c0..e164aa1450 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit ff351799c068e7b3e23dd903547d228dc30aff5e +Subproject commit e164aa14503ff11dbcf0dc96bcd4cfa4d757b76d diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index fdd482376d..4be4b13a1e 100644 --- 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 index c34e083876..4d3b1d5bf1 100644 --- 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 (_, 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 diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 5fab4fc798..f250b49e01 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1589,10 +1589,11 @@ rhsAdt = P.label "" $ do rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsRecord 'Parsed) rhsRecord = P.label "" $ 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 index 04e26f8f0b..47ee4bf302 100644 --- 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@{ diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix index 65021767c3..dd89b41452 100644 --- a/tests/positive/Format.juvix +++ b/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; diff --git a/tests/positive/InstanceImport/M.juvix b/tests/positive/InstanceImport/M.juvix index d4f51b545e..6e78bb0e29 100644 --- a/tests/positive/InstanceImport/M.juvix +++ b/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; diff --git a/tests/positive/Internal/Positivity2/main.juvix b/tests/positive/Internal/Positivity2/main.juvix index 84f4f584f9..b559424c38 100644 --- a/tests/positive/Internal/Positivity2/main.juvix +++ b/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; diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 24d5ca0457..dfd8ea3436 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/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 }; diff --git a/tests/positive/Puns.juvix b/tests/positive/Puns.juvix index 6f8bf4df9a..d41d0d34b2 100644 --- a/tests/positive/Puns.juvix +++ b/tests/positive/Puns.juvix @@ -5,7 +5,7 @@ type A := a; type B := b; type S := - mkS { + mkS@{ fieldA : A; fieldB : B; fieldC : A; diff --git a/tests/positive/RecordIterator.juvix b/tests/positive/RecordIterator.juvix index d840360ad8..c504a60699 100644 --- a/tests/positive/RecordIterator.juvix +++ b/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; diff --git a/tests/positive/Termination/issue2414.juvix b/tests/positive/Termination/issue2414.juvix index eb2770db70..845c17b989 100644 --- a/tests/positive/Termination/issue2414.juvix +++ 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