Merge branch 'main' into isabelle-pragmas

Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "stdlib";
-     version := mkVersion 0 0 1;
-     dependencies := []};
+  defaultPackage@?{
+    name := "stdlib";
+    version := mkVersion 0 0 1;
+    dependencies := []
+  };

Stdlib/Cairo/Ec.juvix

@@ -12,17 +12,13 @@ import Stdlib.Data.Bool open;
 module StarkCurve;
   ALPHA : Field := 1;
 
-  BETA : Field :=
-    0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89;
+  BETA : Field := 0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89;
 
-  ORDER : Field :=
-    0x800000000000010ffffffffffffffffb781126dcae7b2321e66a241adc64d2f;
+  ORDER : Field := 0x800000000000010ffffffffffffffffb781126dcae7b2321e66a241adc64d2f;
 
-  GEN_X : Field :=
-    0x1ef15c18599971b7beced415a40f0c7deacfd9b0d1819e03d723d8bc943cfca;
+  GEN_X : Field := 0x1ef15c18599971b7beced415a40f0c7deacfd9b0d1819e03d723d8bc943cfca;
 
-  GEN_Y : Field :=
-    0x5668060aa49730b7be4801df46ec62de53ecd11abe43a32873000c36e8dc1f;
+  GEN_Y : Field := 0x5668060aa49730b7be4801df46ec62de53ecd11abe43a32873000c36e8dc1f;
 end;
 
 builtin ec_point
@@ -45,8 +41,7 @@ isOnCurve : Point -> Bool
   | (mkPoint x y) :=
     if
       | y == 0 := x == 0
-      | else :=
-        y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
+      | else := y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
 
 --- Doubles a valid point p (computes p + p) on the elliptic curve.
 double : Point -> Point
@@ -58,7 +53,10 @@ double : Point -> Point
           slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y);
           r_x := slope * slope - x - x;
           r_y := slope * (x - r_x) - y;
-        in mkPoint (x := r_x; y := r_y);
+        in mkPoint@?{
+          x := r_x;
+          y := r_y
+        };
 
 --- Adds two valid points on the EC.
 add : Point -> Point -> Point
@@ -109,8 +107,7 @@ addMul (p : Point) (m : Field) (q : Point) : Point :=
       in sub r s;
 
 --- Computes m * p on the elliptic curve.
-mul (m : Field) (p : Point) : Point :=
-  addMul (mkPoint 0 0) m p;
+mul (m : Field) (p : Point) : Point := addMul (mkPoint 0 0) m p;
 
 module Operators;
   import Stdlib.Data.Fixity open;

Stdlib/Cairo/Poseidon.juvix

@@ -19,32 +19,19 @@ axiom poseidonHash : PoseidonState -> PoseidonState;
 
 --- Hashes one element and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHash1 (x : Field) : Field :=
-  PoseidonState.s0 (poseidonHash (mkPoseidonState x 0 1));
+poseidonHash1 (x : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseidonState x 0 1));
 
 --- Hashes two elements and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHash2 (x y : Field) : Field :=
-  PoseidonState.s0 (poseidonHash (mkPoseidonState x y 2));
+poseidonHash2 (x y : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseidonState x y 2));
 
 --- Hashes n elements and retrieves a single field element output.
 {-# eval: false #-}
 poseidonHashList (lst : List Field) : Field :=
   let
     go (acc : PoseidonState) : List Field -> PoseidonState
       | [] := poseidonHash acc@PoseidonState{s0 := s0 + 1}
-      | [x] :=
-        poseidonHash
-          acc@PoseidonState{
-            s0 := s0 + x;
-            s1 := s1 + 1
-          }
+      | [x] := poseidonHash acc@PoseidonState{   s0 := s0 + x; s1 := s1 + 1 }
       | (x1 :: x2 :: xs) :=
-        go
-          (poseidonHash
-            acc@PoseidonState{
-              s0 := s0 + x1;
-              s1 := s1 + x2
-            })
-          xs;
+        go (poseidonHash acc@PoseidonState{   s0 := s0 + x1; s1 := s1 + x2 }) xs;
   in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst);

Stdlib/Data/List/Base.juvix

@@ -18,6 +18,7 @@ elem {A} (eq : A → A → Bool) (s : A) : List A → Bool
 
 --- 𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or
 --- nothing if there's no such element.
+{-# specialize: [1] #-}
 find {A} (predicate : A → Bool) : List A → Maybe A
   | nil := nothing
   | (x :: xs) :=
@@ -67,13 +68,11 @@ filter {A} (f : A → Bool) : List A → List A
   | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs);
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
-length {A} (l : List A) : Nat :=
-  for (acc := zero) (_ in l) {suc acc};
+length {A} (l : List A) : Nat := for (acc := zero) (_ in l) {suc acc};
 
 --- 𝒪(𝓃). Returns the given ;List; in reverse order.
 {-# isabelle-function: {name: "rev"} #-}
-reverse {A} (l : List A) : List A :=
-  for (acc := nil) (x in l) {x :: acc};
+reverse {A} (l : List A) : List A := for (acc := nil) (x in l) {x :: acc};
 
 --- Returns a ;List; of length n where every element is the given value.
 replicate {A} : Nat → A → List A
@@ -96,8 +95,7 @@ splitAt {A} : Nat → List A → Pair (List A) (List A)
   | _ nil := nil, nil
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
-  | (suc m) (x :: xs) :=
-    case splitAt m xs of l1, l2 := x :: l1, l2;
+  | (suc m) (x :: xs) := case splitAt m xs of l1, l2 := x :: l1, l2;
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
 terminating
@@ -111,12 +109,9 @@ merge {A} {{Ord A}} : List A → List A → List A
 
 --- 𝒪(𝓃). Returns a tuple where the first component has the items that
 --- satisfy the predicate and the second component has the elements that don't.
-partition
-  {A} (f : A → Bool) : List A → Pair (List A) (List A)
+partition {A} (f : A → Bool) : List A → Pair (List A) (List A)
   | nil := nil, nil
-  | (x :: xs) :=
-    case partition f xs of
-      l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2);
+  | (x :: xs) := case partition f xs of l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2);
 
 syntax operator ++ cons;
 
@@ -130,8 +125,7 @@ snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil;
 
 --- Concatenates a ;List; of ;List;s.
 {-# isabelle-function: {name: "concat"} #-}
-flatten : {A : Type} → List (List A) → List A :=
-  foldl (++) nil;
+flatten : {A : Type} → List (List A) → List A := foldl (++) nil;
 
 --- 𝒪(𝓃). Inserts the given element before every element in the given ;List;.
 prependToAll {A} (sep : A) : List A → List A
@@ -177,8 +171,7 @@ null {A} : List A → Bool
 --- 𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function
 --- to each pair of elements from the input lists.
 {-# specialize: [1] #-}
-zipWith
-  {A B C} (f : A -> B -> C) : List A -> List B -> List C
+zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List C
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
@@ -215,9 +208,7 @@ quickSort {A} {{Ord A}} : List A → List A :=
     go : List A → List A
       | nil := nil
       | xs@(_ :: nil) := xs
-      | (x :: xs) :=
-        case partition (Ord.cmp x >> isGT) xs of
-          l1, l2 := go l1 ++ x :: go l2;
+      | (x :: xs) := case partition (Ord.cmp x >> isGT) xs of l1, l2 := go l1 ++ x :: go l2;
   in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
@@ -230,8 +221,7 @@ syntax iterator concatMap {init := 0; range := 1};
 
 --- Applies a function to every item on a ;List; and concatenates the result.
 --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.
-concatMap {A B} (f : A -> List B) : List A -> List B :=
-  map f >> flatten;
+concatMap {A B} (f : A -> List B) : List A -> List B := map f >> flatten;
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : List (List A) -> List (List A)

Stdlib/Data/Pair.juvix

@@ -10,8 +10,7 @@ import Stdlib.Trait.Show open;
 
 instance
 eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
-  | {{mkEq eq-a}} {{mkEq eq-b}} :=
-    mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
+  | {{mkEq eq-a}} {{mkEq eq-b}} := mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
 
 instance
 ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
@@ -24,9 +23,6 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
           | EQ := cmp-b b1 b2};
 
 instance
-showProductI
-  {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
+showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
   | {{mkShow show-a}} {{mkShow show-b}} :=
-    mkShow
-      λ {(a, b) :=
-        "(" ++str show-a a ++str " , " ++str show-b b ++str ")"};
+    mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"};

Stdlib/Data/Pair/Base.juvix

@@ -13,8 +13,7 @@ uncurry {A B C} (f : A -> B -> C) : Pair A B -> C
   | (a, b) := f a b;
 
 --- Converts a function with a product argument to a function of two arguments.
-curry {A B C} (f : Pair A B -> C) (a : A) (b : B) : C :=
-  f (a, b);
+curry {A B C} (f : Pair A B -> C) (a : A) (b : B) : C := f (a, b);
 
 --- Projects the first component of a tuple.
 fst {A B} : Pair A B → A

Stdlib/Data/Range.juvix

@@ -18,19 +18,12 @@ type Range N :=
 syntax iterator for {init := 1; range := 1};
 
 {-# specialize: [1, 2, 3, 5] #-}
-for
-  {A N}
-  {{Ord N}}
-  {{Natural N}}
-  (f : A → N → A)
-  (a : A)
-  : Range N → A
+for {A N} {{Ord N}} {{Natural N}} (f : A → N → A) (a : A) : Range N → A
   | mkRange@{low; high; step} :=
     let
       {-# specialize-by: [f] #-}
       terminating
-      go (acc : A) (n : N) : A :=
-        ite (n > high) acc (go (f acc n) (n + step));
+      go (acc : A) (n : N) : A := ite (n > high) acc (go (f acc n) (n + step));
     in go a low;
 
 syntax operator to range;
@@ -43,5 +36,4 @@ syntax operator step step;
 
 --- `x to y step s` is the range [x,x+s,..,y]
 {-# inline: always #-}
-step {N} (r : Range N) (s : N) : Range N :=
-  r@Range{step := s};
+step {N} (r : Range N) (s : N) : Range N := r@Range{step := s};

Stdlib/Data/Result/Base.juvix

@@ -12,22 +12,15 @@ type Result E A :=
 
 --- Apply the onError function if the value is ;error; or apply the
 --- onOk function if the value is ;ok;.
-handleResult
-  {E A B}
-  (onError : E -> B)
-  (onOk : A -> B)
-  : Result E A -> B
+handleResult {E A B} (onError : E -> B) (onOk : A -> B) : Result E A -> B
   | (error a) := onError a
   | (ok a) := onOk a;
 
 --- Apply a function to the ;error; value of a Result.
-mapError
-  {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A :=
-  handleResult (f >> error) ok;
+mapError {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A := handleResult (f >> error) ok;
 
 --- Apply a function to the ;ok; value of a Result.
-mapOk {E A C} (f : A -> C) : Result E A -> Result E C :=
-  handleResult error (f >> ok);
+mapOk {E A C} (f : A -> C) : Result E A -> Result E C := handleResult error (f >> ok);
 
 --- Return ;true; if the value is an ;error;, otherwise ;false;.
 isError {E A} : Result E A -> Bool
@@ -50,11 +43,9 @@ fromOk {E A} (default : A) : Result E A -> A
   | (ok b) := b;
 
 --- Convert a Result to a Maybe. An ;error; value becomes `nothing`.
-resultToMaybe {E A} : Result E A -> Maybe A :=
-  handleResult (const nothing) just;
+resultToMaybe {E A} : Result E A -> Maybe A := handleResult (const nothing) just;
 
 --- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`.
-maybeToResult
-  {E A} (defaultError : E) : Maybe A -> Result E A
+maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A
   | nothing := error defaultError
   | (just x) := ok x;

Stdlib/Data/String/Base.juvix

@@ -9,5 +9,4 @@ import Stdlib.Data.Fixity open;
 concatStr : List String -> String := foldl (++str) "";
 
 --- Joins a ;List; of ;String;s with "\n".
-unlines : List String -> String :=
-  intersperse "\n" >> concatStr;
+unlines : List String -> String := intersperse "\n" >> concatStr;

Stdlib/Extra/Gcd.juvix

@@ -7,14 +7,7 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Data.Bool open;
 
 --- Computes the greatest common divisor.
-gcd
-  {A}
-  {{Eq A}}
-  {{Ord A}}
-  {{Natural A}}
-  {{DivMod A}}
-  (a b : A)
-  : A :=
+gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} {{DivMod A}} (a b : A) : A :=
   let
     -- Internal helper for computing the greatest common divisor. The first element
     -- should be smaller than the second.

Stdlib/Function.juvix

@@ -47,8 +47,7 @@ iterate {A} : Nat -> (A -> A) -> A -> A
 syntax operator on lapp;
 
 {-# inline: 2 #-}
-on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C :=
-  f (g a) (g b);
+on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C := f (g a) (g b);
 
 syntax operator >-> seq;
 

Stdlib/System/IO.juvix

@@ -8,8 +8,6 @@ import Stdlib.System.IO.String open public;
 
 import Stdlib.Trait.Show open;
 
-print {A} {{Show A}} (a : A) : IO :=
-  printString (Show.show a);
+print {A} {{Show A}} (a : A) : IO := printString (Show.show a);
 
-printLn {A} {{Show A}} (a : A) : IO :=
-  printStringLn (Show.show a);
+printLn {A} {{Show A}} (a : A) : IO := printStringLn (Show.show a);

Stdlib/System/IO/Bool.juvix

@@ -7,5 +7,4 @@ import Stdlib.System.IO.String open;
 builtin bool-print
 axiom printBool : Bool → IO;
 
-printBoolLn (b : Bool) : IO :=
-  printBool b >>> printString "\n";
+printBoolLn (b : Bool) : IO := printBool b >>> printString "\n";

Stdlib/System/IO/Int.juvix

@@ -7,5 +7,4 @@ import Stdlib.System.IO.String open;
 builtin int-print
 axiom printInt : Int → IO;
 
-printIntLn (i : Int) : IO :=
-  printInt i >>> printString "\n";
+printIntLn (i : Int) : IO := printInt i >>> printString "\n";

Stdlib/System/IO/Nat.juvix

@@ -7,5 +7,4 @@ import Stdlib.System.IO.String open;
 builtin nat-print
 axiom printNat : Nat → IO;
 
-printNatLn (n : Nat) : IO :=
-  printNat n >>> printString "\n";
+printNatLn (n : Nat) : IO := printNat n >>> printString "\n";

Stdlib/System/IO/String.juvix

@@ -9,5 +9,4 @@ axiom printString : String → IO;
 builtin IO-readline
 axiom readLn : (String → IO) → IO;
 
-printStringLn (s : String) : IO :=
-  printString s >>> printString "\n";
+printStringLn (s : String) : IO := printString s >>> printString "\n";

Stdlib/Trait/Partial.juvix

@@ -4,10 +4,8 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Debug.Fail as Debug;
 
 trait
-type Partial :=
-  mkPartial {fail : {A : Type} -> String -> A};
+type Partial := mkPartial {fail : {A : Type} -> String -> A};
 
 open Partial public;
 
-runPartial {A} (f : {{Partial}} -> A) : A :=
-  f {{mkPartial Debug.failwith}};
+runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}};

test/Package.juvix

@@ -3,11 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "stdlib-test";
-     dependencies := [ path "../"
-                     ; github
-                       "anoma"
-                       "juvix-quickcheck"
-                       "8e5d49682fb0b861fc0a1aed95cfebab03231d85"
-                     ]};
+  defaultPackage@?{
+    name := "stdlib-test";
+    dependencies :=
+      [path "../"; github "anoma" "juvix-quickcheck" "8e5d49682fb0b861fc0a1aed95cfebab03231d85"]
+  };