Remove @? syntax and format

Data/List.juvix

@@ -12,8 +12,13 @@ rangeStep : Nat -> Nat -> List Nat
         | (suc n) xs := go n (n * step :: xs);
     in go n nil;
 
-unzipWith : {A : Type} -> {B : Type} -> {C : Type} -> (A -> B -> C) -> List (Pair A B) -> List C :=
-  map << uncurry;
+unzipWith
+  : {A : Type}
+    -> {B : Type}
+    -> {C : Type}
+    -> (A -> B -> C)
+    -> List (Pair A B)
+    -> List C := map << uncurry;
 
 range : Nat -> List Nat
   | n := rangeStep 1 n;

Example.juvix

@@ -8,9 +8,11 @@ import Data.String open;
 
 import Test.QuickCheckTest as QC;
 
-prop-reverseDoesNotChangeLength (xs : List Int) : Bool := length (reverse xs) == length xs;
+prop-reverseDoesNotChangeLength (xs : List Int) : Bool :=
+  length (reverse xs) == length xs;
 
-prop-reverseReverseIsIdentity (xs : List Int) : Bool := eqListInt xs (reverse (reverse xs));
+prop-reverseReverseIsIdentity (xs : List Int) : Bool :=
+  eqListInt xs (reverse (reverse xs));
 
 prop-tailLengthOneLess (xs : List Int) : Bool :=
   isEmpty xs || ofNat (length (tail xs)) == intSubNat (length xs) 1;
@@ -23,9 +25,13 @@ prop-mergeSumLengths (xs : List Int) (ys : List Int) : Bool :=
 
 prop-partition (xs : List Int) (p : Int -> Bool) : Bool :=
   case partition p xs of
-    lhs, rhs := all p lhs && not (any p rhs) && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
+    lhs, rhs :=
+      all p lhs
+        && not (any p rhs)
+        && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
 
-prop-distributive (a : Int) (b : Int) (f : Int -> Int) : Bool := f (a + b) == f a + f b;
+prop-distributive (a : Int) (b : Int) (f : Int -> Int) : Bool :=
+  f (a + b) == f a + f b;
 
 prop-add-sub (a : Int) (b : Int) : Bool := a == a + b - b;
 
@@ -36,36 +42,45 @@ prop-gcd-bad (a : Int) (b : Int) : Bool := gcd a b > ofNat 1;
 gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" prop-gcd-bad;
 
 partitionTest : QC.Test :=
-  QC.mkTest "partition: recombination of the output equals the input" prop-partition;
+  QC.mkTest
+    "partition: recombination of the output equals the input"
+    prop-partition;
 
-testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" prop-distributive;
+testDistributive : QC.Test :=
+  QC.mkTest "all functions are distributive over +" prop-distributive;
 
-reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength;
+reverseLengthTest : QC.Test :=
+  QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
   QC.mkTest "reverse of reverse is identity" prop-reverseReverseIsIdentity;
 
 splitAtRecombineTest : QC.Test :=
-  QC.mkTest "splitAt: recombination of the output is equal to the input list" prop-splitAtRecombine;
+  QC.mkTest
+    "splitAt: recombination of the output is equal to the input list"
+    prop-splitAtRecombine;
 
 mergeSumLengthsTest : QC.Test :=
   QC.mkTest
     "merge: sum of the lengths of input lists is equal to the length of output list"
     prop-mergeSumLengths;
 
 tailLengthOneLessTest : QC.Test :=
-  QC.mkTest "tail: length of output is one less than input unless empty" prop-tailLengthOneLess;
+  QC.mkTest
+    "tail: length of output is one less than input unless empty"
+    prop-tailLengthOneLess;
 
 main : IO :=
   readLn
-    \ {seed :=
+    \{seed :=
       QC.runTestsIO
         100
         (stringToNat seed)
-        [ partitionTest
-        ; reverseLengthTest
-        ; reverseReverseIdTest
-        ; splitAtRecombineTest
-        ; mergeSumLengthsTest
-        ; tailLengthOneLessTest
+        [
+          partitionTest;
+          reverseLengthTest;
+          reverseReverseIdTest;
+          splitAtRecombineTest;
+          mergeSumLengthsTest;
+          tailLengthOneLessTest;
         ]};

Package.juvix

@@ -3,9 +3,9 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "quickcheck";
-    version := mkVersion 0 17 0;
+    version := mkVersion 0 18 0;
     dependencies := [defaultStdlib];
     main := just "Example.juvix";
   };

Test/QuickCheck.juvix

@@ -8,13 +8,18 @@ import Test.QuickCheck.Property open public;
 import Test.QuickCheck.Outcome open public;
 import Test.QuickCheck.Testable open public;
 
-quickcheck {Predicate : Type} {{Testable Predicate}} : Nat -> Nat -> Predicate -> Outcome
+quickcheck
+  {Predicate : Type} {{Testable Predicate}} : Nat -> Nat -> Predicate -> Outcome
   | attemptNum startSeed predicate :=
     let
-      seeds : List Nat := map (n in range attemptNum) startSeed + n;
+      seeds : List Nat :=
+        map (n in range attemptNum) {
+          startSeed + n
+        };
       runOne (prop : Property) (nextSeed : Nat) : Outcome :=
         let
           result : Outcome := runProp prop (mkStdGen nextSeed);
-        in overFailure result \ {f := f@Failure{seed := nextSeed}};
-      runAll (prop : Property) : Outcome := foldMap monoidOutcome (runOne prop) seeds;
+        in overFailure result \{f := f@Failure{seed := nextSeed}};
+      runAll (prop : Property) : Outcome :=
+        foldMap monoidOutcome (runOne prop) seeds;
     in runAll (Testable.toProp predicate);

Test/QuickCheck/Arbitrary.juvix

@@ -7,32 +7,37 @@ import Test.QuickCheck.CoArbitrary open;
 
 -- | A generator associated with a type A
 trait
-type Arbitrary (A : Type) := mkArbitrary {gen : Gen A};
+type Arbitrary (A : Type) :=
+  mkArbitrary@{
+    gen : Gen A;
+  };
 
 runArb {A} {{Arbitrary A}} (rand : StdGen) : A := Gen.run Arbitrary.gen rand;
 
 instance
-arbitraryNat : Arbitrary Nat := mkArbitrary (mkGen \ {rand := fst (stdNext rand)});
+arbitraryNat : Arbitrary Nat :=
+  mkArbitrary (mkGen \{rand := fst (stdNext rand)});
 
 instance
 arbitraryInt : Arbitrary Int :=
   mkArbitrary
     (mkGen
-      \ {rand :=
+      \{rand :=
         let
           runRand : Pair Nat StdGen := stdNext rand;
           n : Nat := fst runRand;
           isPos : Bool := fst (randBool (snd runRand));
         in ite isPos (ofNat n) (negSuc n)});
 
 instance
-arbitraryBool : Arbitrary Bool := mkArbitrary (mkGen \ {rand := fst (randBool rand)});
+arbitraryBool : Arbitrary Bool :=
+  mkArbitrary (mkGen \{rand := fst (randBool rand)});
 
 instance
 arbitraryList {A} {{Arbitrary A}} : Arbitrary (List A) :=
   mkArbitrary
     (mkGen
-      \ {rand :=
+      \{rand :=
         let
           randSplit : Pair StdGen StdGen := stdSplit rand;
           rand1 : StdGen := fst randSplit;
@@ -49,14 +54,15 @@ arbitraryList {A} {{Arbitrary A}} : Arbitrary (List A) :=
         in randList rand2 len});
 
 instance
-arbitraryFunction {A B} {{CoArbitrary A}} {{Arbitrary B}} : Arbitrary (A -> B) :=
+arbitraryFunction
+  {A B} {{CoArbitrary A}} {{Arbitrary B}} : Arbitrary (A -> B) :=
   mkArbitrary (promote (CoArbitrary.coarbitrary Arbitrary.gen));
 
 instance
 arbitraryMaybe {A} {{Arbitrary A}} : Arbitrary (Maybe A) :=
   mkArbitrary
     (mkGen
-      \ {rand :=
+      \{rand :=
         let
           randSplit : Pair StdGen StdGen := stdSplit rand;
           rand1 : StdGen := fst randSplit;
@@ -67,10 +73,11 @@ arbitraryMaybe {A} {{Arbitrary A}} : Arbitrary (Maybe A) :=
           | else := nothing});
 
 instance
-arbitraryResult {A B} {{Arbitrary A}} {{Arbitrary B}} : Arbitrary (Result A B) :=
+arbitraryResult
+  {A B} {{Arbitrary A}} {{Arbitrary B}} : Arbitrary (Result A B) :=
   mkArbitrary
     (mkGen
-      \ {rand :=
+      \{rand :=
         let
           randSplit : Pair StdGen StdGen := stdSplit rand;
           rand1 : StdGen := fst randSplit;

Test/QuickCheck/CoArbitrary.juvix

@@ -6,7 +6,10 @@ import Test.QuickCheck.Gen open;
 
 -- | A perturbation of a generator associated with a type B
 trait
-type CoArbitrary (A : Type) := mkCoarbitrary {coarbitrary : {B : Type} -> Gen B -> A -> Gen B};
+type CoArbitrary (A : Type) :=
+  mkCoarbitrary@{
+    coarbitrary : {B : Type} -> Gen B -> A -> Gen B;
+  };
 
 binaryDigits : Nat -> List Nat
   | n :=
@@ -25,14 +28,19 @@ perturb : Int -> StdGen -> StdGen
             splitG : Pair StdGen StdGen := stdSplit g;
           in ite b (snd splitG) (fst splitG);
       terminating
-      digitsParity : List Bool := map (x in binaryDigits (abs n)) x == 0;
-    in for (rand := vary (n < ofNat 0) rand0) (b in digitsParity)
-         vary b rand;
+      digitsParity : List Bool :=
+        map (x in binaryDigits (abs n)) {
+          x == 0
+        };
+    in for (rand := vary (n < ofNat 0) rand0) (b in digitsParity) {
+      vary b rand
+    };
 
 instance
 coarbitraryInt : CoArbitrary Int :=
-  mkCoarbitrary \ {g n := mkGen \ {rand := Gen.run g (perturb n rand)}};
+  mkCoarbitrary \{g n := mkGen \{rand := Gen.run g (perturb n rand)}};
 
 instance
 coarbitraryListInt : CoArbitrary (List Int) :=
-  mkCoarbitrary \ {g xs := mkGen \ {rand := Gen.run g (foldr perturb (perturb 0 rand) xs)}};
+  mkCoarbitrary
+    \{g xs := mkGen \{rand := Gen.run g (foldr perturb (perturb 0 rand) xs)}};

Test/QuickCheck/Gen.juvix

@@ -3,6 +3,10 @@ module Test.QuickCheck.Gen;
 import Data.Random open;
 
 --- A generator of values of type A
-type Gen (A : Type) := mkGen {run : StdGen -> A};
+type Gen (A : Type) :=
+  mkGen@{
+    run : StdGen -> A;
+  };
 
-promote {A B} (f : A -> Gen B) : Gen (A -> B) := mkGen \ {rand a := Gen.run (f a) rand};
+promote {A B} (f : A -> Gen B) : Gen (A -> B) :=
+  mkGen \{rand a := Gen.run (f a) rand};

Test/QuickCheck/Outcome.juvix

@@ -5,9 +5,9 @@ import Data.Monoid open;
 import Data.String open;
 
 type Failure :=
-  mkFailure {
+  mkFailure@{
     seed : Nat;
-    counterExamples : List String
+    counterExamples : List String;
   };
 
 type Outcome :=
@@ -34,7 +34,7 @@ showOutcomeI : Show Outcome := mkShow showOutcome;
 monoidOutcome : Monoid Outcome :=
   monoid
     success
-    \ {
+    \{
       | x@(failure _) _ := x
       | _ y := y
     };

Test/QuickCheck/Property.juvix

@@ -5,6 +5,10 @@ import Test.QuickCheck.Gen open;
 import Test.QuickCheck.Outcome open;
 
 --- A testable predicate from which we can obtain a ;Gen Outcome;
-type Property := mkProperty {getGen : Gen Outcome};
+type Property :=
+  mkProperty@{
+    getGen : Gen Outcome;
+  };
 
-runProp (p : Property) (rand : StdGen) : Outcome := Gen.run (Property.getGen p) rand;
+runProp (p : Property) (rand : StdGen) : Outcome :=
+  Gen.run (Property.getGen p) rand;

Test/QuickCheck/Testable.juvix

@@ -10,13 +10,17 @@ import Test.QuickCheck.Gen open;
 
 --- A conversion from a Type A to a ;Property;
 trait
-type Testable (A : Type) := mkTestable {toProp : A -> Property};
+type Testable (A : Type) :=
+  mkTestable@{
+    toProp : A -> Property;
+  };
 
-forAll {A T : Type} {{Show A}} {{Arbitrary A}} {{Testable T}} : (A -> T) -> Property
+forAll
+  {A T : Type} {{Show A}} {{Arbitrary A}} {{Testable T}} : (A -> T) -> Property
   | prop :=
     mkProperty
       (mkGen
-        \ {rand :=
+        \{rand :=
           let
             srand : Pair StdGen StdGen := stdSplit rand;
             rand1 : StdGen := fst srand;
@@ -26,24 +30,28 @@ forAll {A T : Type} {{Show A}} {{Arbitrary A}} {{Testable T}} : (A -> T) -> Prop
             res : Outcome := runProp subProp rand2;
           in overFailure
             res
-            \ {f := f@Failure{counterExamples := Show.show arg :: Failure.counterExamples f}}});
+            \{f :=
+              f@Failure{counterExamples := Show.show arg
+                :: Failure.counterExamples f}}});
 
 instance
 testableProperty : Testable Property := mkTestable id;
 
 instance
-testableOutcome : Testable Outcome := mkTestable \ {r := mkProperty (mkGen (const r))};
+testableOutcome : Testable Outcome :=
+  mkTestable \{r := mkProperty (mkGen (const r))};
 
 instance
 testableBool : Testable Bool :=
   let
     toOutcome : Bool -> Outcome
       | b := ite b success (failure (mkFailure 0 nil));
-  in mkTestable \ {b := Testable.toProp (toOutcome b)};
+  in mkTestable \{b := Testable.toProp (toOutcome b)};
 
 instance
-testableFunction {A T} {{Show A}} {{Arbitrary A}} {{Testable T}} : Testable (A -> T) :=
-  mkTestable \ {f := forAll f};
+testableFunction
+  {A T} {{Show A}} {{Arbitrary A}} {{Testable T}} : Testable (A -> T) :=
+  mkTestable \{f := forAll f};
 
 instance
 showableFunction {A B : Type} : Show (A -> B) := mkShow (const "function");