1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-02 10:47:32 +03:00

Formatter: add braces when the iterator body is not enclosed (#3122)

* Closes #3091
* Formatter adds braces when the body is not enclosed in braces or
parentheses. Braces-enclosed body is always printed as a block on a new
line:
```
for (acc := 0) (x in lst) {
  x + acc
}
```
* If the body is enclosed in ordinary parentheses, then they are
preserved and the iterator is printed on a single line, if possible:
```
for (acc := 0) (x in lst) (x + acc)
```
This is sometimes useful when you want iterator application as an
argument to something.
This commit is contained in:
Łukasz Czajka 2024-10-25 11:42:01 +02:00 committed by GitHub
parent ddca867871
commit 3cf79faafb
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 60 additions and 56 deletions

View File

@ -304,17 +304,17 @@ instance (SingI s) => PrettyPrint (Range s) where
n <+> ppCode _rangeInKw <+> e
ppIterator :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Iterator s -> Sem r ()
ppIterator isTop Iterator {..} = do
ppIterator _isTop Iterator {..} = do
let n = ppIdentifierType _iteratorName
is = ppCode <$> _iteratorInitializers
rngs = ppCode <$> _iteratorRanges
is' = parens . hsepSemicolon <$> nonEmpty is
rngs' = parens . hsepSemicolon <$> nonEmpty rngs
b
| _iteratorBodyBraces = braces (oneLineOrNextNoIndent (ppTopExpressionType _iteratorBody))
| otherwise = line <> ppMaybeTopExpression isTop _iteratorBody
| _iteratorBodyBraces = space <> braces (blockIndent (ppTopExpressionType _iteratorBody))
| otherwise = parens (oneLineOrNextNoIndent (ppTopExpressionType _iteratorBody))
parensIf _iteratorParens $
hang (n <+?> is' <+?> rngs' <> b)
n <+?> is' <+?> rngs' <> b
instance PrettyPrint S.AName where
ppCode n = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.anameVerbatim)))

View File

@ -1615,9 +1615,10 @@ checkSections sec = topBindings helper
fs <-
failMaybe $
mkRec
^? constructorRhs
. _ConstructorRhsRecord
. to mkRecordNameSignature
^? ( constructorRhs
. _ConstructorRhsRecord
. to mkRecordNameSignature
)
let info =
RecordInfo
{ _recordInfoSignature = fs,

View File

@ -931,7 +931,8 @@ iterator = do
do
(_iteratorBody, _iteratorBodyBraces) <-
(,True) <$> braces parseExpressionAtoms
<|> (,False) <$> parseExpressionAtoms
<|> (,False) <$> parens parseExpressionAtoms
<|> (,True) <$> parseExpressionAtoms
let _iteratorParens = False
return $ Iterator {..}
where

View File

@ -24,11 +24,14 @@ gen : Nat → Tree
preorder : Tree → List Nat
| leaf := 0 :: nil
| (node1 c) := 1 :: preorder c
| (node2 l r) := 2 :: preorder l ++ preorder r
| (node1 c) := 1 :: preorder c
| (node2 l r) := 2 :: preorder l ++ preorder r
| (node3 l m r) := 3 :: preorder l ++ preorder m ++ preorder r;
combineDigits (xs : List Nat) : Nat := for (acc := 0) (x in xs) acc * 10 + x;
combineDigits (xs : List Nat) : Nat :=
for (acc := 0) (x in xs) {
acc * 10 + x
};
main : Nat :=
trace (combineDigits (preorder (gen 3)))

View File

@ -7,6 +7,6 @@ type BoxedList :=
| boxed (List Nat);
sumBoxedList : BoxedList -> Nat
| (boxed l) := for (acc := 0) (x in l) acc + x;
| (boxed l) := for (acc := 0) (x in l) (acc + x);
main : Nat := sumBoxedList (boxed [1;2;3]);

View File

@ -4,8 +4,7 @@ module test054;
import Stdlib.Prelude open;
syntax iterator myfor;
myfor : {A B : Type} → (A → B → A) → A → List B → A :=
foldl {_} {_} {{_}} {_};
myfor : {A B : Type} → (A → B → A) → A → List B → A := foldl {_} {_} {{_}} {_};
syntax iterator mymap {init := 0};
mymap : {A B : Type} → (A → B) → List A → List B
@ -13,7 +12,10 @@ mymap : {A B : Type} → (A → B) → List A → List B
| f (x :: xs) := f x :: mymap f xs;
sum : List Nat → Nat
| xs := myfor (acc := 0) (x in xs) {acc + x};
| xs :=
myfor (acc := 0) (x in xs) {
acc + x
};
sum' : List Nat → Nat
| xs := myfor λ {acc x := acc + x} 0 xs;
@ -21,39 +23,30 @@ sum' : List Nat → Nat
lst : List Nat := 1 :: 2 :: 3 :: 4 :: 5 :: nil;
syntax iterator myfor2 {init := 1; range := 2};
myfor2
: {A B C : Type}
→ (A → B → C → A)
→ A
→ List B
→ List C
→ A
myfor2 : {A B C : Type} → (A → B → C → A) → A → List B → List C → A
| f acc xs ys :=
myfor (acc' := acc) (x in xs)
myfor (acc'' := acc') (y in ys)
f acc'' x y;
myfor (acc' := acc) (x in xs) {
myfor (acc'' := acc') (y in ys) {
f acc'' x y
}
};
syntax iterator myzip2 {init := 2; range := 2};
myzip2
: {A A' B C : Type}
→ (A → A' → B → C → Pair A A')
→ A
→ A'
→ List B
→ List C
→ Pair A A'
myzip2 : {A A' B C : Type} → (A → A' → B → C → Pair A A') → A → A' → List B → List C → Pair A A'
| f a b xs ys :=
myfor (acc, acc' := a, b) (x, y in zip xs ys)
f acc acc' x y;
myfor (acc, acc' := a, b) (x, y in zip xs ys) {
f acc acc' x y
};
main : Nat :=
sum lst
+ sum' lst
+ fst (myfor (a, b := 0, 0) (x in lst) b + x, a)
+ (myfor2 (acc := 0) (x in lst; y in 1 :: 2 :: nil)
acc + x + y)
+ fst (myfor (a, b := 0, 0) (x in lst) (b + x, a))
+ myfor2 (acc := 0) (x in lst; y in 1 :: 2 :: nil) (acc + x + y)
+ fst
(myzip2 (a := 0; b := 0) (x in lst; y in reverse lst)
a + x * y, b + y)
+ myfor (a := 0) (x, y in mymap (x in lst) {x, x + 1})
a + x * y;
(myzip2 (a := 0; b := 0) (x in lst; y in reverse lst) {
a + x * y, b + y
})
+ myfor (a := 0) (x, y in mymap (x in lst) (x, x + 1)) {
a + x * y
};

View File

@ -26,7 +26,7 @@ myf'
| a0 f a b := myf a0 (f a0) a b true;
sum : List Nat -> Nat
| xs := for (acc := 0) (x in xs) {x + acc};
| xs := for (acc := 0) (x in xs) (x + acc);
funa : {A : Type} -> (A -> A) -> A -> A
| {A} f a :=

View File

@ -3,10 +3,11 @@ module test058;
import Stdlib.Prelude open;
sum (x : Nat) : Nat :=
for (acc := 0) (n in 1 to x) {acc + n};
sum (x : Nat) : Nat := for (acc := 0) (n in 1 to x) (acc + n);
sum' (x : Nat) : Nat :=
for (acc := 0) (n in 1 to x step 2) {acc + n};
for (acc := 0) (n in 1 to x step 2) {
acc + n
};
main : Nat := sum 100 + sum' 100;

View File

@ -5,7 +5,7 @@ import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;
trait
type T A := mkT {toNat : A -> Nat};
type T A := mkT@{toNat : A -> Nat};
instance
tNatI : T Nat := mkT id;
@ -29,16 +29,16 @@ tMaybeI {A} {{T A}} : T (Maybe A) :=
instance
tUnitFunI {A} {{T A}} : T (Unit -> A) :=
mkT@{
toNat {A} {{T A}} (f : Unit -> A) : Nat :=
T.toNat (f unit)
toNat {A} {{T A}} (f : Unit -> A) : Nat := T.toNat (f unit)
};
instance
tListI {A} {{T A}} : T (List A) :=
mkT@{
toNat {A} {{T A}} (xs : List A) : Nat :=
for (acc := 0) (x in xs)
for (acc := 0) (x in xs) {
acc + T.toNat {A} x
}
};
g : {A : Type} → {{T A}} → Nat := 5;

View File

@ -15,8 +15,10 @@ type Bool :=
main : Bool :=
let
z : Bool := false;
in itconst (a := true; b := false) (c in false; d in false)
for (x := true) (y in false)
case x of
| true := y
| false := z;
in itconst (a := true; b := false) (c in false; d in false) {
for (x := true) (y in false) {
case x of
| true := y
| false := z
}
};

View File

@ -19,4 +19,7 @@ foldl
(g : B -> elem -> B)
(ini : B)
(ls : container)
: B := for (acc := ini) (x in ls) {g acc x};
: B :=
for (acc := ini) (x in ls) {
g acc x
};