Skip to content

Commit

Permalink
Allow trailing semicolons everywhere (#3123)
Browse files Browse the repository at this point in the history
* Closes #3039
* Closes #3043
* Closes #2970
* Closes #3089
* Parser allows trailing semicolons for any kind of semicolon-separated
items:
  - let-block statements,
  - module statements,
  - record declaration statements,
  - record update fields,
  - record pattern fields,
  - named application arguments,
  - list literal items,
  - list pattern items,
  - open statement using/hiding items,
  - `syntax iterator` declaration parameters,
  - `syntax fixity` declaration parameters.
* Formatter prints trailing semicolons if the items are displayed on
separate lines, removes them if on a single line.
* The formatting of multiline lists is changed to make it consistent
with other semicolon-separated blocks:
```
[
  1;
  2;
  3;
]
```
instead of
```
[ 1
; 2
; 3
]
```
  • Loading branch information
lukaszcz authored Oct 29, 2024
1 parent 021f183 commit c143259
Show file tree
Hide file tree
Showing 25 changed files with 305 additions and 195 deletions.
2 changes: 1 addition & 1 deletion examples/demo/Demo.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ type Tree (A : Type) :=
| node@{
element : A;
left : Tree A;
right : Tree A
right : Tree A;
};

mirror {A} : (tree : Tree A) -> Tree A
Expand Down
2 changes: 1 addition & 1 deletion examples/milestone/Bank/Bank.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ type Token :=
mkToken@{
owner : Address;
gates : Nat;
amount : Nat
amount : Nat;
};

--- This module defines the type for balances and its associated operations.
Expand Down
2 changes: 1 addition & 1 deletion examples/milestone/Hanoi/Hanoi.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ showPeg : Peg -> String
type Move :=
mkMove@{
from : Peg;
to : Peg
to : Peg;
};

showMove (move : Move) : String :=
Expand Down
2 changes: 1 addition & 1 deletion examples/milestone/TicTacToe/Logic/Game.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ playMove (attemptedMove : Maybe Nat) (state : GameState) : GameState :=
mkGameState@{
board := mkBoard (map (map (replace player' k)) squares);
player := switch player';
error := noError
error := noError;
};

--- Returns ;just; if the given ;Nat; is in range of 1..9
Expand Down
4 changes: 2 additions & 2 deletions examples/milestone/TicTacToe/Logic/GameState.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ type GameState :=
mkGameState@{
board : Board;
player : Symbol;
error : Error
error : Error;
};

--- Textual representation of a ;GameState;
Expand All @@ -34,7 +34,7 @@ beginState : GameState :=
:: (7 :: 8 :: 9 :: nil)
:: nil));
player := X;
error := noError
error := noError;
};

--- ;true; if some player has won the game
Expand Down
2 changes: 1 addition & 1 deletion examples/milestone/TicTacToe/Logic/Square.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ eqSquareI : Eq Square :=
case square1, square2 of
| empty m, empty n := m == n
| occupied s, occupied t := s == t
| _, _ := false
| _, _ := false;
};

--- Textual representation of a ;Square;
Expand Down
2 changes: 1 addition & 1 deletion examples/milestone/TicTacToe/Logic/Symbol.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ eqSymbolI : Eq Symbol :=
case sym1, sym2 of
| O, O := true
| X, X := true
| _, _ := false
| _, _ := false;
};

--- Turns ;O; into ;X; and ;X; into ;O;
Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
Original file line number Diff line number Diff line change
Expand Up @@ -437,7 +437,7 @@ goStatement = \case

goFixity :: forall r. (Members '[Reader HtmlOptions] r) => FixitySyntaxDef 'Scoped -> Sem r Html
goFixity def = do
sig' <- ppHelper (ppFixityDefHeaderNew def)
sig' <- ppHelper (ppFixityDefHeader def)
header' <- defHeader (def ^. fixitySymbol) sig' (def ^. fixityDoc)
prec' <- mkPrec
ari' <- ari
Expand Down
90 changes: 46 additions & 44 deletions src/Juvix/Compiler/Concrete/Print/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -189,8 +189,10 @@ instance (SingI s) => PrettyPrint (ListPattern s) where
ppCode ListPattern {..} = do
let l = ppCode _listpBracketL
r = ppCode _listpBracketR
e = hsepSemicolon (map ppPatternParensType _listpItems)
l <> e <> r
e = case sing :: SStage s of
SParsed -> ppBlockOrList _listpItems
SScoped -> ppBlockOrList _listpItems
grouped (align (l <> e <> r))

instance PrettyPrint Interval where
ppCode = noLoc . pretty
Expand Down Expand Up @@ -323,8 +325,10 @@ instance (SingI s) => PrettyPrint (List s) where
ppCode List {..} = do
let l = ppCode _listBracketL
r = ppCode _listBracketR
es = vcatPreSemicolon (map ppExpressionType _listItems)
grouped (align (l <> spaceOrEmpty <> es <> lineOrEmpty <> r))
es = case sing :: SStage s of
SParsed -> ppBlockOrList _listItems
SScoped -> ppBlockOrList _listItems
grouped (align (l <> es <> r))

instance (SingI s) => PrettyPrint (NamedArgumentAssign s) where
ppCode NamedArgumentAssign {..} = do
Expand All @@ -350,14 +354,14 @@ instance (SingI s) => PrettyPrint (NamedApplicationNew s) where
ppCode NamedApplicationNew {..} = do
let args'
| null _namedApplicationNewArguments = mempty
| otherwise =
blockIndent $
sequenceWith
(semicolon >> line)
(ppCode <$> _namedApplicationNewArguments)
ppIdentifierType _namedApplicationNewName
<> ppCode _namedApplicationNewExhaustive
<> braces args'
| otherwise = ppBlock _namedApplicationNewArguments
grouped
( align
( ppIdentifierType _namedApplicationNewName
<> ppCode _namedApplicationNewExhaustive
<> braces args'
)
)

instance (SingI s) => PrettyPrint (NamedArgumentFunctionDef s) where
ppCode (NamedArgumentFunctionDef f) = ppCode f
Expand Down Expand Up @@ -389,14 +393,7 @@ instance (SingI s) => PrettyPrint (RecordUpdate s) where
let Irrelevant (l, r) = _recordUpdateDelims
fields'
| [f] <- _recordUpdateFields = ppCode f
| otherwise =
line
<> indent
( sequenceWith
(semicolon >> line)
(ppCode <$> _recordUpdateFields)
)
<> line
| otherwise = ppBlockOrList _recordUpdateFields
ppCode _recordUpdateAtKw
<> ppIdentifierType _recordUpdateTypeName
<> ppCode l
Expand All @@ -410,7 +407,7 @@ instance (SingI s) => PrettyPrint (DoubleBracesExpression s) where

instance (SingI s) => PrettyPrint (DoLet s) where
ppCode DoLet {..} = do
let letFunDefs' = blockIndent (ppBlock _doLetStatements)
let letFunDefs' = ppBlock _doLetStatements
ppCode _doLetKw
<> letFunDefs'
<> ppCode _doLetInKw
Expand Down Expand Up @@ -631,7 +628,7 @@ ppMaybeTopExpression isTop e = case isTop of

ppLet :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Let s -> Sem r ()
ppLet isTop Let {..} = do
let letFunDefs' = blockIndent (ppBlock _letFunDefs)
let letFunDefs' = ppBlock _letFunDefs
letExpression' = ppMaybeTopExpression isTop _letExpression
align $ ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'

Expand Down Expand Up @@ -847,8 +844,20 @@ ppLRExpression associates fixlr e =
(atomParens associates (atomicity e) fixlr)
(ppCode e)

ppBlock' :: (Members '[Reader Options, ExactPrint] r, Traversable t) => t (Sem r ()) -> Sem r ()
ppBlock' items = blockIndent (vsepHard (sepEndSemicolon items))

ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
ppBlock items = vsepHard (sepEndSemicolon (fmap ppCode items))
ppBlock items = ppBlock' (fmap ppCode items)

ppBlockOrList' :: (Members '[Reader Options, ExactPrint] r, Traversable t) => t (Sem r ()) -> Sem r ()
ppBlockOrList' items =
flatAlt
(ppBlock' items)
(hsepSemicolon items)

ppBlockOrList :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
ppBlockOrList items = ppBlockOrList' (fmap ppCode items)

instance (SingI s) => PrettyPrint (Lambda s) where
ppCode Lambda {..} = do
Expand All @@ -866,8 +875,8 @@ instance PrettyPrint Precedence where
PrecApp -> noLoc (pretty ("ω" :: Text))
PrecUpdate -> noLoc (pretty ("ω₁" :: Text))

ppFixityDefHeaderNew :: (SingI s) => PrettyPrinting (FixitySyntaxDef s)
ppFixityDefHeaderNew FixitySyntaxDef {..} = do
ppFixityDefHeader :: (SingI s) => PrettyPrinting (FixitySyntaxDef s)
ppFixityDefHeader FixitySyntaxDef {..} = do
let sym' = annotated (AnnKind KNameFixity) (ppSymbolType _fixitySymbol)
ppCode _fixitySyntaxKw <+> ppCode _fixityKw <+> sym'

Expand Down Expand Up @@ -905,14 +914,14 @@ instance (SingI s) => PrettyPrint (ParsedFixityInfo s) where
belowItem = do
a <- _fixityFieldsPrecBelow
return (ppCode Kw.kwBelow <+> ppCode Kw.kwAssign <+> ppSymbolList a)
items = hsepSemicolon (catMaybes [assocItem, sameItem, aboveItem, belowItem])
items = ppBlockOrList' (catMaybes [assocItem, sameItem, aboveItem, belowItem])
(l, r) = _fixityFieldsBraces ^. unIrrelevant
return (ppCode l <> items <> ppCode r)
return (grouped (ppCode l <> items <> ppCode r))
ppCode _fixityParsedArity <+?> rhs

instance (SingI s) => PrettyPrint (FixitySyntaxDef s) where
ppCode f@FixitySyntaxDef {..} = do
let header' = ppFixityDefHeaderNew f
let header' = ppFixityDefHeader f
body' = ppCode _fixityInfo
header' <+> ppCode _fixityAssignKw <+> body'

Expand Down Expand Up @@ -946,8 +955,8 @@ instance PrettyPrint ParsedIteratorInfo where
rangeItem = do
a <- _parsedIteratorInfoRangeNum
return (ppCode Kw.kwRange <+> ppCode Kw.kwAssign <+> ppInt a)
items = hsepSemicolon (catMaybes [iniItem, rangeItem])
ppCode l <> items <> ppCode r
items = ppBlockOrList' (catMaybes [iniItem, rangeItem])
grouped (ppCode l <> items <> ppCode r)

instance PrettyPrint IteratorSyntaxDef where
ppCode IteratorSyntaxDef {..} = do
Expand Down Expand Up @@ -1190,8 +1199,8 @@ instance (SingI s) => PrettyPrint (RecordPatternItem s) where
instance (SingI s) => PrettyPrint (RecordPattern s) where
ppCode r = do
let c = ppIdentifierType (r ^. recordPatternConstructor)
items = sepSemicolon (map ppCode (r ^. recordPatternItems))
c <> noLoc C.kwAt <> align (braces items)
items = ppBlockOrList (r ^. recordPatternItems)
grouped (align (c <> noLoc C.kwAt <> braces items))

instance PrettyPrint Pattern where
ppCode = \case
Expand Down Expand Up @@ -1241,14 +1250,14 @@ instance (SingI s) => PrettyPrint (HidingItem s) where
instance (SingI s) => PrettyPrint (HidingList s) where
ppCode HidingList {..} = do
let (openb, closeb) = _hidingBraces ^. unIrrelevant
items' = sequenceWith (semicolon <> space) (ppCode <$> _hidingList)
ppCode _hidingKw <+> ppCode openb <> items' <> ppCode closeb
items' = ppBlockOrList _hidingList
grouped (ppCode _hidingKw <+> ppCode openb <> items' <> ppCode closeb)

instance (SingI s) => PrettyPrint (UsingList s) where
ppCode UsingList {..} = do
let (openb, closeb) = _usingBraces ^. unIrrelevant
items' = sequenceWith (semicolon <> space) (ppCode <$> _usingList)
ppCode _usingKw <+> ppCode openb <> items' <> ppCode closeb
items' = ppBlockOrList _usingList
grouped (ppCode _usingKw <+> ppCode openb <> items' <> ppCode closeb)

instance (SingI s) => PrettyPrint (UsingHiding s) where
ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => UsingHiding s -> Sem r ()
Expand Down Expand Up @@ -1428,14 +1437,7 @@ instance (SingI s) => PrettyPrint (RhsRecord s) where
fields'
| [] <- _rhsRecordStatements = mempty
| [f] <- _rhsRecordStatements = ppCode f
| otherwise =
hardline
<> indent
( sequenceWith
(semicolon >> line)
(ppCode <$> _rhsRecordStatements)
)
<> hardline
| otherwise = ppBlock _rhsRecordStatements
ppCode kwAt <> ppCode l <> fields' <> ppCode r

instance (SingI s) => PrettyPrint (RhsAdt s) where
Expand Down
12 changes: 8 additions & 4 deletions src/Juvix/Compiler/Concrete/Translation/FromSource.hs
Original file line number Diff line number Diff line change
Expand Up @@ -423,7 +423,7 @@ phidingList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError,
phidingList = do
_hidingKw <- Irrelevant <$> kw kwHiding
l <- kw delimBraceL
_hidingList <- P.sepBy1 hidingItem semicolon
_hidingList <- P.sepEndBy1 hidingItem semicolon
r <- kw delimBraceR
return
HidingList
Expand All @@ -435,7 +435,7 @@ pusingList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, J
pusingList = do
_usingKw <- Irrelevant <$> kw kwUsing
l <- kw delimBraceL
_usingList <- P.sepBy1 usingItem semicolon
_usingList <- P.sepEndBy1 usingItem semicolon
r <- kw delimBraceR
return
UsingList
Expand Down Expand Up @@ -699,6 +699,8 @@ parsedFixityFields = do
bel <- toPermutationWithDefault Nothing (Just <$> belowAbove kwBelow)
abov <- toPermutationWithDefault Nothing (Just <$> belowAbove kwAbove)
sam <- toPermutationWithDefault Nothing (Just <$> same)
-- This is needed to allow an optional semicolon at the end
toPermutationWithDefault Nothing (return (Just ()))
pure (as, bel, abov, sam)
r <- kw delimBraceR
let _fixityFieldsBraces = Irrelevant (l, r)
Expand Down Expand Up @@ -769,6 +771,8 @@ parsedIteratorInfo = do
(_parsedIteratorInfoInitNum, _parsedIteratorInfoRangeNum) <- intercalateEffect semicolon $ do
ini <- toPermutationWithDefault Nothing (Just <$> pinit)
ran <- toPermutationWithDefault Nothing (Just <$> prangeNum)
-- This is needed to allow an optional semicolon at the end
toPermutationWithDefault Nothing (return (Just ()))
pure (ini, ran)
r <- kw delimBraceR
let _parsedIteratorInfoBraces = Irrelevant (l, r)
Expand Down Expand Up @@ -1059,14 +1063,14 @@ hole = kw kwHole
parseListPattern :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ListPattern 'Parsed)
parseListPattern = do
_listpBracketL <- Irrelevant <$> kw kwBracketL
_listpItems <- P.sepBy parsePatternAtoms (kw delimSemicolon)
_listpItems <- P.sepEndBy parsePatternAtoms (kw delimSemicolon)
_listpBracketR <- Irrelevant <$> kw kwBracketR
return ListPattern {..}

parseList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (List 'Parsed)
parseList = do
_listBracketL <- Irrelevant <$> kw kwBracketL
_listItems <- P.sepBy parseExpressionAtoms (kw delimSemicolon)
_listItems <- P.sepEndBy parseExpressionAtoms (kw delimSemicolon)
_listBracketR <- Irrelevant <$> kw kwBracketR
return List {..}

Expand Down
6 changes: 3 additions & 3 deletions src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -853,8 +853,8 @@ goExpression = \case
ExpressionRecordUpdate i -> goRecordUpdateApp i
ExpressionParensRecordUpdate i -> Internal.ExpressionLambda <$> goRecordUpdate (i ^. parensRecordUpdate)
where
goNamedApplication :: ScopedIden -> NonEmpty (ArgumentBlock 'Scoped) -> [Internal.ApplicationArg] -> Sem r Internal.Expression
goNamedApplication fun blocks extraArgs = do
goNamedApplication' :: ScopedIden -> NonEmpty (ArgumentBlock 'Scoped) -> [Internal.ApplicationArg] -> Sem r Internal.Expression
goNamedApplication' fun blocks extraArgs = do
s <- asks (^. S.infoNameSigs)
runReader s (runNamedArguments fun blocks extraArgs) >>= goDesugaredNamedApplication

Expand All @@ -869,7 +869,7 @@ goExpression = \case
sig <- fromJust <$> asks (^. S.infoNameSigs . at (name ^. S.nameId))
let fun = napp ^. namedApplicationNewName
blocks = createArgumentBlocks appargs (sig ^. nameSignatureArgs)
compiledNameApp <- goNamedApplication fun blocks extraArgs
compiledNameApp <- goNamedApplication' fun blocks extraArgs
case nonEmpty (appargs ^.. each . _NamedArgumentNewFunction) of
Nothing -> return compiledNameApp
Just funs -> do
Expand Down
6 changes: 3 additions & 3 deletions src/Juvix/Data/Effect/ExactPrint.hs
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,9 @@ align = region P.align
indent :: (Members '[ExactPrint] r) => Sem r () -> Sem r ()
indent = region (P.indent 2)

flatAlt :: (Members '[ExactPrint] r) => Sem r () -> Sem r () -> Sem r ()
flatAlt = regionAlt P.flatAlt (const id)

softline :: (Members '[ExactPrint] r) => Sem r ()
softline = noLoc P.softline

Expand Down Expand Up @@ -121,9 +124,6 @@ sepSemicolon = grouped . vsepSemicolon
vsepSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r ()
vsepSemicolon = sequenceWith (semicolon <> line)

vcatPreSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r ()
vcatPreSemicolon = sequenceWith (lineOrEmpty <> semicolon <> space)

hsepSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r ()
hsepSemicolon = sequenceWith (semicolon <> space)

Expand Down
Loading

0 comments on commit c143259

Please sign in to comment.