Improve function argument names

Stdlib/Data/BinaryTree.juvix

@@ -19,6 +19,6 @@ fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B :=
       | (node l a r) := f a (go acc l) (go acc r);
   in go acc tree;
 
-length {A} (tree : BinaryTree A) : Nat := fold \ {_ l r := 1 + l + r} 0 tree;
+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

@@ -9,7 +9,7 @@ import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
 instance
-boolEqI : Eq Bool :=
+eqBoolI : Eq Bool :=
   mkEq@{
     eq (x y : Bool) : Bool :=
       case x, y of
@@ -20,7 +20,7 @@ boolEqI : Eq Bool :=
 
 {-# specialize: true, inline: case #-}
 instance
-boolOrdI : Ord Bool :=
+ordBoolI : Ord Bool :=
   mkOrd@{
     cmp (x y : Bool) : Ordering :=
       case x, y of

Stdlib/Data/List/Base.juvix

@@ -68,11 +68,17 @@ filter {A} (predicate : A -> Bool) : (list : List A) -> List A
       | else := filter predicate hs;
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
-length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc};
+length {A} (list : List A) : Nat :=
+  listFor (acc := zero) (_ in list) {
+    suc acc
+  };
 
 --- 𝒪(𝓃). Returns the given ;List; in reverse order.
 {-# isabelle-function: {name: "rev"} #-}
-reverse {A} (l : List A) : List A := listFor (acc := nil) (x in l) {x :: acc};
+reverse {A} (list : List A) : List A :=
+  listFor (acc := nil) (x in list) {
+    x :: acc
+  };
 
 --- Returns a ;List; of length resultLength where every element is the given value.
 replicate {A} : (resultLength : Nat) -> (value : A) -> List A
@@ -188,13 +194,13 @@ 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) : (listA : List A) -> (listB : 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;
 
 --- 𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists.
-zip {A B} : (listA : List A) -> (listB : List B) -> List (Pair A B)
+zip {A B} : (list1 : List A) -> (list2 : List B) -> List (Pair A B)
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := (x, y) :: zip xs ys;
@@ -225,7 +231,7 @@ 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;.
@@ -243,5 +249,5 @@ concatMap {A B} (fun : A -> List B) (list : List A) : List B := flatten (listMap
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : (listOfLists : List (List A)) -> List (List A)
   | nil := nil
-  | (xs :: nil) := listMap λ {x := x :: nil} xs
+  | (xs :: nil) := listMap λ{x := x :: nil} xs
   | (xs :: xss) := zipWith (::) xs (transpose xss);

Stdlib/Data/Map.juvix

@@ -6,7 +6,7 @@ import Stdlib.Data.List open;
 import Stdlib.Data.Nat open;
 import Stdlib.Data.Bool open;
 
-import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Functor open using {Functor; mkFunctor; map as fmap};
 import Stdlib.Trait.Foldable open hiding {foldr; foldl};
 import Stdlib.Trait.Ord open;
 
@@ -57,154 +57,202 @@ insertWith
         binding := mkBinding key value;
       in mkMap (Set.insertWith fun' binding tree);
 
---- 𝒪(log 𝓃). Inserts an element into a ;Map; at a given key.
+--- 𝒪(log 𝓃). Inserts a new `key` and `value` into `map`. If `key` is already
+--- present in `map`, the associated value is replaced with the supplied
+--- `value`.
 {-# inline: true #-}
-insert {Key Value : Type} {{Ord Key}} : Key -> Value -> Map Key Value -> Map Key Value :=
-  insertWith \ {old new := new};
+insert
+  {Key Value : Type} {{Ord Key}} (key : Key) (elem : Value) (map : Map Key Value) : Map Key Value :=
+  insertWith (flip const) key elem map;
 
---- 𝒪(log 𝓃). Queries whether a given key is in a ;Map;.
+--- 𝒪(log 𝓃). Queries whether a given `key` is in `map`.
 {-# specialize: [1] #-}
-lookup {Key Value} {{Ord Key}} (lookupKey : Key) (container : Map Key Value) : Maybe Value :=
-  case container of mkMap s := map value (Set.lookupWith key lookupKey s);
+lookup {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Maybe Value :=
+  case map of mkMap s := fmap value (Set.lookupWith Binding.key key s);
 
---- 𝒪(log 𝓃). Queries whether a given key is in a ;Map;.
+--- 𝒪(log 𝓃). Queries whether a given `key` is in `map`.
 {-# specialize: [1] #-}
-isMember {Key Value} {{Ord Key}} (key : Key) (container : Map Key Value) : Bool :=
-  isJust (lookup key container);
+isMember {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Bool :=
+  isJust (lookup key map);
 
 {-# specialize: [1, f] #-}
 fromListWithKey
   {Key Value}
   {{Ord Key}}
-  (f : Key -> Value -> Value -> Value)
-  (xs : List (Pair Key Value))
-  : Map Key Value := for (acc := empty) (k, v in xs) {insertWith (f k) k v acc};
+  (fun : Key -> Value -> Value -> Value)
+  (list : List (Pair Key Value))
+  : Map Key Value :=
+  for (acc := empty) (k, v in list) {
+    insertWith (fun k) k v acc
+  };
 
 {-# inline: true #-}
 fromListWith
   {Key Value}
   {{Ord Key}}
-  (f : Value -> Value -> Value)
-  (xs : List (Pair Key Value))
-  : Map Key Value := fromListWithKey (const f) xs;
+  (fun : Value -> Value -> Value)
+  (list : List (Pair Key Value))
+  : Map Key Value := fromListWithKey (const fun) list;
 
 {-# inline: true #-}
-fromList {Key Value} {{Ord Key}} : List (Pair Key Value) -> Map Key Value :=
-  fromListWith λ {old new := new};
+fromList {Key Value} {{Ord Key}} (list : List (Pair Key Value)) : Map Key Value :=
+  fromListWith (flip const) list;
 
-toList {Key Value} (container : Map Key Value) : List (Pair Key Value) :=
-  case container of mkMap s := map (x in Set.toList s) {toPair x};
+toList {Key Value} (map : Map Key Value) : List (Pair Key Value) :=
+  case map of
+    mkMap s :=
+      fmap (x in Set.toList s) {
+        toPair x
+      };
 
 {-# specialize: [1, f] #-}
-fromSet {Key Value} {{Ord Key}} (f : Key -> Value) (set : Set Key) : Map Key Value :=
-  for (acc := empty) (k in set) {insert k (f k) acc};
+fromSet {Key Value} {{Ord Key}} (fun : Key -> Value) (set : Set Key) : Map Key Value :=
+  for (acc := empty) (k in set) {
+    insert k (fun k) acc
+  };
 
 --- 𝒪(1). Checks if a ;Map; is empty.
 {-# inline: true #-}
-isEmpty {Key Value} (container : Map Key Value) : Bool :=
-  case container of mkMap s := Set.isEmpty s;
+isEmpty {Key Value} (map : Map Key Value) : Bool := case map of mkMap s := Set.isEmpty s;
 
 --- 𝒪(𝓃). Returns the number of elements of a ;Map;.
 {-# inline: true #-}
-size {Key Value} (container : Map Key Value) : Nat := case container of mkMap s := Set.size s;
+size {Key Value} (map : Map Key Value) : Nat := case map of mkMap s := Set.size s;
 
---- 𝒪(log 𝓃). Removes a key assignment from a ;Map;.
+--- 𝒪(log 𝓃). Removes `key` assignment from `map`.
 {-# inline: true #-}
-delete {Key Value} {{Ord Key}} (deleteKey : Key) (container : Map Key Value) : Map Key Value :=
-  case container of mkMap s := mkMap (Set.deleteWith key deleteKey s);
+delete {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Map Key Value :=
+  case map of mkMap s := mkMap (Set.deleteWith Binding.key key s);
 
-keys {Key Value} (container : Map Key Value) : List Key :=
-  case container of mkMap s := map (x in Set.toList s) {key x};
+keys {Key Value} (map : Map Key Value) : List Key :=
+  case map of
+    mkMap s :=
+      fmap (x in Set.toList s) {
+        key x
+      };
 
-values {Key Value} (container : Map Key Value) : List Value :=
-  case container of mkMap s := map (x in Set.toList s) {value x};
+values {Key Value} (map : Map Key Value) : List Value :=
+  case map of
+    mkMap s :=
+      fmap (x in Set.toList s) {
+        value x
+      };
 
-keySet {Key Value} {{Ord Key}} (container : Map Key Value) : Set Key :=
-  case container of mkMap s := Set.map (x in s) {key x};
+keySet {Key Value} {{Ord Key}} (map : Map Key Value) : Set Key :=
+  case map of
+    mkMap s :=
+      Set.map (x in s) {
+        key x
+      };
 
-valueSet {Key Value} {{Ord Value}} (container : Map Key Value) : Set Value :=
-  case container of mkMap s := Set.map (x in s) {value x};
+valueSet {Key Value} {{Ord Value}} (map : Map Key Value) : Set Value :=
+  case map of
+    mkMap s :=
+      Set.map (x in s) {
+        value x
+      };
 
 {-# specialize: [f] #-}
 mapValuesWithKey
-  {Key Value1 Value2} (f : Key -> Value1 -> Value2) (container : Map Key Value1) : Map Key Value2 :=
-  case container of
-    mkMap s := mkMap (Set.Internal.unsafeMap \ {(mkBinding k v) := mkBinding k (f k v)} s);
+  {Key Value1 Value2} (fun : Key -> Value1 -> Value2) (map : Map Key Value1) : Map Key Value2 :=
+  case map of
+    mkMap s := mkMap (Set.Internal.unsafeMap \{(mkBinding k v) := mkBinding k (fun k v)} s);
 
 {-# inline: true #-}
-mapValues
-  {Key Value1 Value2} (f : Value1 -> Value2) (container : Map Key Value1) : Map Key Value2 :=
-  mapValuesWithKey (const f) container;
+mapValues {Key Value1 Value2} (fun : Value1 -> Value2) (map : Map Key Value1) : Map Key Value2 :=
+  mapValuesWithKey (const fun) map;
 
 {-# inline: true #-}
 singleton {Key Value} {{Ord Key}} (key : Key) (value : Value) : Map Key Value :=
   insert key value empty;
 
 {-# inline: true #-}
-foldr
-  {Key Value Acc} (f : Key -> Value -> Acc -> Acc) (acc : Acc) (container : Map Key Value) : Acc :=
-  case container of mkMap s := rfor (acc := acc) (x in s) {f (key x) (value x) acc};
+foldr {Key Value Acc} (fun : Key -> Value -> Acc -> Acc) (acc : Acc) (map : Map Key Value) : Acc :=
+  case map of
+    mkMap s :=
+      rfor (acc := acc) (x in s) {
+        fun (key x) (value x) acc
+      };
 
 {-# inline: true #-}
-foldl
-  {Key Value Acc} (f : Acc -> Key -> Value -> Acc) (acc : Acc) (container : Map Key Value) : Acc :=
-  case container of mkMap s := for (acc := acc) (x in s) {f acc (key x) (value x)};
+foldl {Key Value Acc} (fun : Acc -> Key -> Value -> Acc) (acc : Acc) (map : Map Key Value) : Acc :=
+  case map of
+    mkMap s :=
+      for (acc := acc) (x in s) {
+        fun acc (key x) (value x)
+      };
 
 syntax iterator all {init := 0; range := 1};
---- 𝒪(𝓃). Returns ;true; if all key-element pairs in the ;Map; satisfy the predicate.
+--- 𝒪(𝓃). Returns ;true; if all key-value pairs in `map` satisfy `predicate`.
 {-# inline: true #-}
-all {Key Value} (predicate : Key -> Value -> Bool) (container : Map Key Value) : Bool :=
-  case container of mkMap s := Set.all (x in s) {predicate (key x) (value x)};
+all {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
+  case map of
+    mkMap s :=
+      Set.all (x in s) {
+        predicate (key x) (value x)
+      };
 
 syntax iterator any {init := 0; range := 1};
---- 𝒪(𝓃). Returns ;true; if some key-element pair in the ;Map; satisfies the predicate.
+--- 𝒪(𝓃). Returns ;true; if some key-value pair in `map` satisfies `predicate`.
 {-# inline: true #-}
-any {Key Value} (predicate : Key -> Value -> Bool) (container : Map Key Value) : Bool :=
-  case container of mkMap s := Set.any (x in s) {predicate (key x) (value x)};
+any {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
+  case map of
+    mkMap s :=
+      Set.any (x in s) {
+        predicate (key x) (value x)
+      };
 
 syntax iterator filter {init := 0; range := 1};
---- 𝒪(n log n). Returns a ;Map; containing all key-element pairs of the given
---- map container that satisfy the predicate.
+--- 𝒪(n log n). Returns a ;Map; containing all key-value pairs of `map` that
+--- satisfy `predicate`.
 {-# inline: true #-}
 filter
   {Key Value}
   {{Ord Key}}
   (predicate : Key -> Value -> Bool)
-  (container : Map Key Value)
+  (map : Map Key Value)
   : Map Key Value :=
-  case container of mkMap s := mkMap (Set.filter (x in s) {predicate (key x) (value x)});
+  case map of
+    mkMap s :=
+      mkMap
+        (Set.filter (x in s) {
+          predicate (key x) (value x)
+        });
 
 syntax iterator partition {init := 0; range := 1};
 {-# inline: true #-}
 partition
   {Key Value}
   {{Ord Key}}
   (predicate : Key -> Value -> Bool)
-  (container : Map Key Value)
+  (map : Map Key Value)
   : Pair (Map Key Value) (Map Key Value) :=
-  case container of
+  case map of
     mkMap s :=
-      case Set.partition (x in s) {predicate (key x) (value x)} of
-        left, right := mkMap left, mkMap right;
+      case
+        Set.partition (x in s) {
+          predicate (key x) (value x)
+        }
+      of left, right := mkMap left, mkMap right;
 
 {-# specialize: true, inline: case #-}
 instance
 functorMapI {Key} : Functor (Map Key) :=
   mkFunctor@{
-    map {A B} (f : A -> B) (container : Map Key A) : Map Key B := mapValues f container
+    map {A B} (fun : A -> B) (container : Map Key A) : Map Key B := mapValues fun container
   };
 
 {-# specialize: true, inline: case #-}
 instance
 foldableMapI {Key Value} : Foldable (Map Key Value) (Pair Key Value) :=
   mkFoldable@{
     {-# inline: true #-}
-    for {B} (f : B -> Pair Key Value -> B) (acc : B) (container : Map Key Value) : B :=
-      foldl \ {a k v := f a (k, v)} acc container;
+    for {B} (f : B -> Pair Key Value -> B) (acc : B) (map : Map Key Value) : B :=
+      foldl \{a k v := f a (k, v)} acc map;
 
     {-# inline: true #-}
-    rfor {B} (f : B -> Pair Key Value -> B) (acc : B) (container : Map Key Value) : B :=
-      foldr \ {k v a := f a (k, v)} acc container
+    rfor {B} (f : B -> Pair Key Value -> B) (acc : B) (map : Map Key Value) : B :=
+      foldr \{k v a := f a (k, v)} acc map
   };
 
 instance

Stdlib/Data/Pair/Base.juvix

@@ -9,10 +9,10 @@ builtin pair
 type Pair (A B : Type) := , : A → B → Pair A B;
 
 --- Converts a function f of two arguments to a function with a product argument.
-uncurry {A B C} (f : A -> B -> C) (pair : Pair A B) : C := case pair of a, b := f a b;
+uncurry {A B C} (fun : A -> B -> C) (pair : Pair A B) : C := case pair of a, b := fun a b;
 
 --- Converts a function f 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} (fun : Pair A B -> C) (a : A) (b : B) : C := fun (a, b);
 
 --- Projects the first component of a tuple.
 fst {A B} (pair : Pair A B) : A := case pair of a, _ := a;
@@ -24,10 +24,10 @@ snd {A B} (pair : Pair A B) : B := case pair of _, b := b;
 swap {A B} (pair : Pair A B) : Pair B A := case pair of a, b := b, a;
 
 --- Applies a function f to the first component.
-first {A B A'} (f : A -> A') (pair : Pair A B) : Pair A' B := case pair of a, b := f a, b;
+first {A B A'} (fun : A -> A') (pair : Pair A B) : Pair A' B := case pair of a, b := fun a, b;
 
 --- Applies a function f to the second component.
-second {A B B'} (f : B -> B') (pair : Pair A B) : Pair A B' := case pair of a, b := a, f b;
+second {A B B'} (fun : B -> B') (pair : Pair A B) : Pair A B' := case pair of a, b := a, fun b;
 
 --- Applies a function f to both components.
-both {A B} (f : A -> B) (pair : Pair A A) : Pair B B := case pair of a, b := f a, f b;
+both {A B} (fun : A -> B) (pair : Pair A A) : Pair B B := case pair of a, b := fun a, fun b;

Stdlib/Data/Queue/Base.juvix

@@ -66,7 +66,9 @@ push {A} (x : A) (queue : Queue A) : Queue A :=
 
 --- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
 pushMany {A} (list : List A) (queue : Queue A) : Queue A :=
-  for (acc := queue) (x in list) {push x acc};
+  for (acc := queue) (x in list) {
+    push x acc
+  };
 
 --- 𝒪(n). Build a ;Queue; from a ;List;.
 fromList {A} (list : List A) : Queue A := pushMany list empty;