Add functions to the Map module and reformat

Stdlib/Cairo/Ec.juvix

@@ -13,20 +13,24 @@ import Stdlib.Data.Pair 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
 type Point :=
   mkPoint@{
     x : Field;
-    y : Field
+    y : Field;
   };
 
 module Internal;
@@ -57,9 +61,9 @@ double (point : Point) : Point :=
             r_x := slope * slope - x - x;
             r_y := slope * (x - r_x) - y;
           in mkPoint@?{
-            x := r_x;
-            y := r_y
-          };
+               x := r_x;
+               y := r_y;
+             };
 
 --- Adds two valid points on the EC.
 add (point1 point2 : Point) : Point :=

Stdlib/Cairo/Poseidon.juvix

@@ -8,7 +8,7 @@ type PoseidonState :=
   mkPoseidonState@{
     s0 : Field;
     s1 : Field;
-    s2 : Field
+    s2 : Field;
   };
 
 builtin poseidon
@@ -19,19 +19,21 @@ 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 (list : 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) list);

Stdlib/Data/BinaryTree.juvix

@@ -8,7 +8,7 @@ type BinaryTree (A : Type) :=
   | node@{
       left : BinaryTree A;
       element : A;
-      right : BinaryTree A
+      right : BinaryTree A;
     };
 
 --- fold a tree in depth-first order
@@ -21,4 +21,5 @@ fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B :=
 
 length {A} (tree : BinaryTree A) : Nat := fold \{_ l r := 1 + l + r} 0 tree;
 
-toList {A} (tree : BinaryTree A) : List A := fold \{e ls rs := e :: ls ++ rs} nil tree;
+toList {A} (tree : BinaryTree A) : List A :=
+  fold \{e ls rs := e :: ls ++ rs} nil tree;

Stdlib/Data/Bool.juvix

@@ -15,7 +15,7 @@ eqBoolI : Eq Bool :=
       case x, y of
         | true, true := true
         | false, false := true
-        | _ := false
+        | _ := false;
   };
 
 {-# specialize: true, inline: case #-}
@@ -27,7 +27,7 @@ ordBoolI : Ord Bool :=
         | false, false := Equal
         | false, true := LessThan
         | true, false := GreaterThan
-        | true, true := Equal
+        | true, true := Equal;
   };
 
 instance
@@ -36,5 +36,5 @@ showBoolI : Show Bool :=
     show (x : Bool) : String :=
       if
         | x := "true"
-        | else := "false"
+        | else := "false";
   };

Stdlib/Data/Byte.juvix

@@ -17,12 +17,12 @@ eqByteI : Eq Byte := mkEq (Byte.==);
 instance
 showByteI : Show Byte :=
   mkShow@{
-    show (x : Byte) : String := Show.show (Byte.toNat x)
+    show (x : Byte) : String := Show.show (Byte.toNat x);
   };
 
 {-# specialize: true, inline: case #-}
 instance
 fromNaturalByteI : FromNatural Byte :=
   mkFromNatural@{
-    fromNat := Byte.fromNat
+    fromNat := Byte.fromNat;
   };

Stdlib/Data/Field.juvix

@@ -19,22 +19,22 @@ eqFieldI : Eq Field := mkEq (Field.==);
 instance
 showFieldI : Show Field :=
   mkShow@{
-    show (f : Field) : String := Show.show (Field.toNat f)
+    show (f : Field) : String := Show.show (Field.toNat f);
   };
 
 {-# specialize: true, inline: case #-}
 instance
 fromNaturalFieldI : FromNatural Field :=
   mkFromNatural@{
-    fromNat := Field.fromNat
+    fromNat := Field.fromNat;
   };
 
 {-# specialize: true, inline: case #-}
 instance
 naturalFieldI : Natural Field :=
   mkNatural@{
     + := (Field.+);
-    * := (Field.*)
+    * := (Field.*);
   };
 
 {-# specialize: true, inline: case #-}
@@ -43,13 +43,13 @@ integralFieldI : Integral Field :=
   mkIntegral@{
     naturalI := naturalFieldI;
     - := (Field.-);
-    fromInt := Field.fromInt
+    fromInt := Field.fromInt;
   };
 
 {-# specialize: true, inline: case #-}
 instance
 numericFieldI : Numeric Field :=
   mkNumeric@{
     integralI := integralFieldI;
-    / := (Field./)
+    / := (Field./);
   };

Stdlib/Data/Int.juvix

@@ -37,15 +37,15 @@ showIntI : Show Int := mkShow intToString;
 instance
 fromNaturalIntI : FromNatural Int :=
   mkFromNatural@{
-    fromNat := ofNat
+    fromNat := ofNat;
   };
 
 {-# specialize: true, inline: case #-}
 instance
 naturalIntI : Natural Int :=
   mkNatural@{
     + := (Int.+);
-    * := (Int.*)
+    * := (Int.*);
   };
 
 {-# specialize: true, inline: case #-}
@@ -54,13 +54,13 @@ integralIntI : Integral Int :=
   mkIntegral@{
     naturalI := naturalIntI;
     - := (Int.-);
-    fromInt (x : Int) : Int := x
+    fromInt (x : Int) : Int := x;
   };
 
 {-# specialize: true, inline: case #-}
 instance
 divModIntI : DivMod Int :=
   mkDivMod@{
     div := Int.div;
-    mod := Int.mod
+    mod := Int.mod;
   };

Stdlib/Data/List.juvix

@@ -10,7 +10,11 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait open;
 import Stdlib.Trait.Partial open;
-import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable};
+import Stdlib.Trait.Foldable open using {
+  Foldable;
+  module Polymorphic;
+  fromPolymorphicFoldable;
+};
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
 phead {A} {{Partial}} : List A -> A
@@ -30,7 +34,8 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
           | else := false;
   in mkEq go;
 
-isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool := isElement (Eq.eq) elem list;
+isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool :=
+  isElement (Eq.eq) elem list;
 
 instance
 ordListI {A} {{Ord A}} : Ord (List A) :=
@@ -53,29 +58,30 @@ showListI {A} {{Show A}} : Show (List A) :=
       | nil := "nil"
       | (x :: xs) := Show.show x ++str " :: " ++str go xs;
   in mkShow@{
-    show (list : List A) : String :=
-      case list of
-        | nil := "nil"
-        | s := "(" ++str go s ++str ")"
-  };
+       show (list : List A) : String :=
+         case list of
+           | nil := "nil"
+           | s := "(" ++str go s ++str ")";
+     };
 
 {-# specialize: true, inline: case #-}
 instance
 functorListI : Functor List :=
   mkFunctor@{
-    map := listMap
+    map := listMap;
   };
 
 {-# specialize: true, inline: true #-}
 instance
-monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor;
+monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A :=
+  fromPolymorphicFunctor;
 
 {-# specialize: true, inline: case #-}
 instance
 polymorphicFoldableListI : Polymorphic.Foldable List :=
   Polymorphic.mkFoldable@{
     for := listFor;
-    rfor := listRfor
+    rfor := listRfor;
   };
 
 {-# specialize: true, inline: true #-}
@@ -88,11 +94,11 @@ applicativeListI : Applicative List :=
     pure {A} (a : A) : List A := [a];
     ap {A B} : (listOfFuns : List (A -> B)) -> (listOfAs : List A) -> List B
       | [] _ := []
-      | (f :: fs) l := map f l ++ ap fs l
+      | (f :: fs) l := map f l ++ ap fs l;
   };
 
 instance
 monadListI : Monad List :=
   mkMonad@{
-    bind := flip concatMap
+    bind := flip concatMap;
   };

Stdlib/Data/List/Base.juvix

@@ -34,7 +34,8 @@ listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> B
 
 --- Right-associative fold.
 {-# specialize: [1] #-}
-liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : B := listRfor (flip fun) acc list;
+liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : B :=
+  listRfor (flip fun) acc list;
 
 --- Left-associative and tail-recursive fold.
 {-# specialize: [1] #-}
@@ -138,7 +139,8 @@ snoc {A} (list : List A) (elem : A) : List A := list ++ elem :: nil;
 
 --- Concatenates a ;List; of ;List;s.
 {-# isabelle-function: {name: "concat"} #-}
-flatten {A} (listOfLists : List (List A)) : List A := listFoldl (++) nil listOfLists;
+flatten {A} (listOfLists : List (List A)) : List A :=
+  listFoldl (++) nil listOfLists;
 
 --- 𝒪(𝓃). Inserts the given separator before every element in the given ;List;.
 prependToAll {A} (separator : A) : (list : List A) -> List A
@@ -194,7 +196,8 @@ isEmpty {A} (list : 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} (fun : A -> B -> C) : (list1 : List A) -> (list2 : List B) -> List C
+zipWith
+  {A B C} (fun : A -> B -> C) : (list1 : List A) -> (list2 : List B) -> List C
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := fun x y :: zipWith fun xs ys;
@@ -231,7 +234,8 @@ quickSort {A} {{Ord A}} (list : List A) : List A :=
     go : List A -> List A
       | nil := nil
       | xs@(_ :: nil) := xs
-      | (x :: xs) := case partition \{y := y < x} xs of l1, l2 := go l1 ++ x :: go l2;
+      | (x :: xs) :=
+        case partition \{y := y < x} xs of l1, l2 := go l1 ++ x :: go l2;
   in go list;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
@@ -244,7 +248,8 @@ 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} (fun : A -> List B) (list : List A) : List B := flatten (listMap fun list);
+concatMap {A B} (fun : A -> List B) (list : List A) : List B :=
+  flatten (listMap fun list);
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : (listOfLists : List (List A)) -> List (List A)