Update stdlib and format

anoma · Jul 19, 2024 · ee933d5 · ee933d5
1 parent c4c7af9
commit ee933d5
Show file tree

Hide file tree

Showing 16 changed files with 101 additions and 209 deletions.
diff --git a/Data/BinaryTree.juvix b/Data/BinaryTree.juvix
@@ -7,16 +7,13 @@ type BinaryTree (A : Type) :=
   | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
 
 --- fold a tree in depth first order
-fold {A B} (f : A -> B -> B -> B) (acc : B)
-  : BinaryTree A -> B :=
+fold {A B} (f : A -> B -> B -> B) (acc : B) : BinaryTree A -> B :=
   let
     go (acc : B) : BinaryTree A -> B
       | leaf := acc
       | (node l a r) := f a (go acc l) (go acc r);
   in go acc;
 
-length : {A : Type} -> BinaryTree A -> Nat :=
-  fold λ {_ l r := 1 + l + r} 0;
+length : {A : Type} -> BinaryTree A -> Nat := fold λ {_ l r := 1 + l + r} 0;
 
-to-list : {A : Type} -> BinaryTree A -> List A :=
-  fold λ {e ls rs := e :: ls ++ rs} nil;
+to-list : {A : Type} -> BinaryTree A -> List A := fold λ {e ls rs := e :: ls ++ rs} nil;
diff --git a/Data/Map.juvix b/Data/Map.juvix
@@ -31,30 +31,25 @@ type Map A B := mkMap (AVLTree (Binding A B));
 empty {A B} : Map A B := mkMap AVL.empty;
 
 {-# specialize: [1, f] #-}
-insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B)
-  : Map A B -> Map A B
+insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B) : Map A B -> Map A B
   | (mkMap s) :=
     let
       f' : Binding A B -> Binding A B -> Binding A B
         | (binding a b1) (binding _ b2) := binding a (f b1 b2);
     in mkMap (Set.insertWith f' (binding k v) s);
 
-insert {A B : Type} {{Ord A}}
-  : A -> B -> Map A B -> Map A B :=
-  insertWith λ {old new := new};
+insert {A B : Type} {{Ord A}} : A -> B -> Map A B -> Map A B := insertWith λ {old new := new};
 
 {-# specialize: [1] #-}
 lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B
   | (mkMap s) := mapMaybe value (Set.lookupWith key k s);
 
 {-# specialize: [1, f] #-}
-fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List
-  (Pair A B)) : Map A B :=
+fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List (Pair A B)) : Map A B :=
   for (acc := empty) (k, v in xs)
     insertWith f k v acc;
 
-fromList {A B} {{Ord A}} : List (Pair A B) -> Map A B :=
-  fromListWith λ {old new := new};
+fromList {A B} {{Ord A}} : List (Pair A B) -> Map A B := fromListWith λ {old new := new};
 
 toList {A B} : Map A B -> List (Pair A B)
   | (mkMap s) := map (x in Set.toList s) toPair x;
@@ -63,5 +58,4 @@ size {A B} : Map A B -> Nat
   | (mkMap s) := Set.size s;
 
 instance
-eqMapI {A B} {{Eq A}} {{Eq B}} : Eq (Map A B) :=
-  mkEq (Eq.eq on toList);
+eqMapI {A B} {{Eq A}} {{Eq B}} : Eq (Map A B) := mkEq (Eq.eq on toList);
diff --git a/Data/Queue/Base.juvix b/Data/Queue/Base.juvix
@@ -43,17 +43,14 @@ check {A} : Queue A -> Queue A
 --  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
 pop {A} : Queue A -> Maybe (Pair A (Queue A))
   | (queue nil _) := nothing
-  | (queue (x :: front) back) :=
-    just (x, check (queue front back));
+  | (queue (x :: front) back) := just (x, check (queue front back));
 
 --- 𝒪(1). Adds an element to the end of the ;Queue;.
 push {A} (x : A) : Queue A -> Queue A
   | (queue front back) := check (queue front (x :: back));
 
 --- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
-pushMany {A} (xs : List A) (q : Queue A) : Queue A :=
-  for (acc := q) (x in xs)
-    push x acc;
+pushMany {A} (xs : List A) (q : Queue A) : Queue A := for (acc := q) (x in xs) push x acc;
 
 --- 𝒪(n). Build a ;Queue; from a ;List;.
 fromList {A} (xs : List A) : Queue A := pushMany xs empty;
@@ -69,13 +66,10 @@ size {A} : Queue A -> Nat
   | (queue front back) := length front + length back;
 
 instance
-eqQueueI {A} {{Eq A}} : Eq (Queue A) :=
-  mkEq ((==) on toList);
+eqQueueI {A} {{Eq A}} : Eq (Queue A) := mkEq ((==) on toList);
 
 instance
-showQueueI {A} {{Show A}} : Show (Queue A) :=
-  mkShow (toList >> Show.show);
+showQueueI {A} {{Show A}} : Show (Queue A) := mkShow (toList >> Show.show);
 
 instance
-ordQueueI {A} {{Ord A}} : Ord (Queue A) :=
-  mkOrd (Ord.cmp on toList);
+ordQueueI {A} {{Ord A}} : Ord (Queue A) := mkOrd (Ord.cmp on toList);
diff --git a/Data/Set.juvix b/Data/Set.juvix
@@ -1,7 +1,7 @@
 module Data.Set;
 
-import Data.Set.AVL open public;
-
+import
+Data.Set.AVL open public;
 import Stdlib.Trait.Eq as Eq open using {Eq};
 import Stdlib.Trait.Ord as Ord open using {Ord};
 

diff --git a/Data/Set/AVL.juvix b/Data/Set/AVL.juvix
@@ -37,22 +37,17 @@ type BalanceFactor :=
 {-# inline: true #-}
 diffFactor {A} : AVLTree A -> Int
   | empty := 0
-  | (node _ _ left right) :=
-    intSubNat (height right) (height left);
+  | (node _ _ left right) := intSubNat (height right) (height left);
 
 --- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree
 --- minus the height of the left subtree.
 balanceFactor {A} (t : AVLTree A) : BalanceFactor :=
   let
     diff : Int := diffFactor t;
-  in ite
-    (0 < diff)
-    LeanRight
-    (ite (diff < 0) LeanLeft LeanNone);
+  in ite (0 < diff) LeanRight (ite (diff < 0) LeanLeft LeanNone);
 
 --- 𝒪(1). Helper function for creating a node.
-mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A)
-  : AVLTree A :=
+mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A) : AVLTree A :=
   node val (1 + max (height l) (height r)) l r;
 
 --- 𝒪(1). Left rotation.
@@ -62,8 +57,7 @@ rotateLeft {A} : AVLTree A -> AVLTree A
 
 --- 𝒪(1). Right rotation.
 rotateRight {A} : AVLTree A -> AVLTree A
-  | (node z _ (node y _ x t3) t4) :=
-    mknode y x (mknode z t3 t4)
+  | (node z _ (node y _ x t3) t4) := mknode y x (mknode z t3 t4)
   | n := n;
 
 --- 𝒪(1). Applies local rotations if needed.
@@ -72,7 +66,7 @@ balance : {A : Type} -> AVLTree A -> AVLTree A
   | n@(node x h l r) :=
     let
       factor : BalanceFactor := balanceFactor n;
-    in case factor of {
+    in case factor of
          | LeanRight :=
            case balanceFactor r of {
              | LeanLeft := rotateLeft (mknode x l (rotateRight r))
@@ -83,52 +77,45 @@ balance : {A : Type} -> AVLTree A -> AVLTree A
              | LeanRight := rotateRight (mknode x (rotateLeft l) r)
              | _ := rotateRight n
            }
-         | LeanNone := n
-       };
+         | LeanNone := n;
 
 --- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function.
 --- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
-lookupWith {A K} {{o : Ord K}} (f : A -> K) (x : K)
-  : AVLTree A -> Maybe A :=
+lookupWith {A K} {{o : Ord K}} (f : A -> K) (x : K) : AVLTree A -> Maybe A :=
   let
     {-# specialize-by: [o, f] #-}
     go : AVLTree A -> Maybe A
       | empty := nothing
       | m@(node y h l r) :=
-        case Ord.cmp x (f y) of {
+        case Ord.cmp x (f y) of
           | LT := go l
           | GT := go r
-          | EQ := just y
-        };
+          | EQ := just y;
   in go;
 
 --- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
 {-# specialize: [1] #-}
-member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool :=
-  lookupWith id x >> isJust;
+member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool := lookupWith id x >> isJust;
 
 --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree; using a function to
 --- deduplicate entries.
 ---
 --- Assumption: Given a1 == a2 then f a1 a2 == a1 == a2
 --- where == comes from Ord a.
-insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A)
-  : AVLTree A -> AVLTree A :=
+insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A) : AVLTree A -> AVLTree A :=
   let
     {-# specialize-by: [o, f] #-}
     go : AVLTree A -> AVLTree A
       | empty := mknode x empty empty
       | m@(node y h l r) :=
-        case Ord.cmp x y of {
+        case Ord.cmp x y of
           | LT := balance (mknode y (go l) r)
           | GT := balance (mknode y l (go r))
-          | EQ := node (f y x) h l r
-        };
+          | EQ := node (f y x) h l r;
   in go;
 
 --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;.
-insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A :=
-  insertWith (flip const);
+insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A := insertWith (flip const);
 
 --- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
 delete {A} {{o : Ord A}} (x : A) : AVLTree A -> AVLTree A :=
@@ -137,27 +124,23 @@ delete {A} {{o : Ord A}} (x : A) : AVLTree A -> AVLTree A :=
     deleteMin : AVLTree A -> Maybe (Pair A (AVLTree A))
       | empty := nothing
       | (node v _ l r) :=
-        case deleteMin l of {
+        case deleteMin l of
           | nothing := just (v, r)
-          | just (m, l') := just (m, mknode v l' r)
-        };
+          | just (m, l') := just (m, mknode v l' r);
     {-# specialize-by: [o] #-}
     go : AVLTree A -> AVLTree A
       | empty := empty
       | (node y h l r) :=
-        case Ord.cmp x y of {
+        case Ord.cmp x y of
           | LT := balance (mknode y (go l) r)
           | GT := balance (mknode y l (go r))
           | EQ :=
-            case l of {
+            case l of
               | empty := r
               | _ :=
-                case deleteMin r of {
+                case deleteMin r of
                   | nothing := l
-                  | just (minRight, r') := balance (mknode minRight l r')
-                }
-            }
-        };
+                  | just (minRight, r') := balance (mknode minRight l r');
   in go;
 
 --- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;.
@@ -176,21 +159,19 @@ lookupMax {A} : AVLTree A -> Maybe A
 
 --- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;.
 {-# specialize: [1] #-}
-deleteMany {A} {{Ord A}} (d : List A) (t : AVLTree A)
-  : AVLTree A := for (acc := t) (x in d) delete x acc;
+deleteMany {A} {{Ord A}} (d : List A) (t : AVLTree A) : AVLTree A :=
+  for (acc := t) (x in d)
+    delete x acc;
 
 --- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that
 --- every two children do not differ on height by more than 1.
 isBalanced {A} : AVLTree A -> Bool
   | empty := true
-  | n@(node _ _ l r) :=
-    isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
+  | n@(node _ _ l r) := isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
 
 --- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
 {-# specialize: [1] #-}
-fromList {A} {{Ord A}} (l : List A) : AVLTree A :=
-  for (acc := empty) (x in l)
-    insert x acc;
+fromList {A} {{Ord A}} (l : List A) : AVLTree A := for (acc := empty) (x in l) insert x acc;
 
 --- 𝒪(𝓃). Returns the number of elements of an ;AVLTree;.
 size {A} : AVLTree A -> Nat
@@ -222,18 +203,13 @@ prettyDebug {A} {{Show A}} : AVLTree A -> String :=
 --- 𝒪(𝓃).
 toTree {A} : AVLTree A -> Maybe (Tree A)
   | empty := nothing
-  | (node v _ l r) :=
-    just
-      (Tree.node v (catMaybes (toTree l :: toTree r :: nil)));
+  | (node v _ l r) := just (Tree.node v (catMaybes (toTree l :: toTree r :: nil)));
 
 --- Returns the textual representation of an ;AVLTree;.
-pretty {A} {{Show A}} : AVLTree A -> String :=
-  toTree >> maybe "empty" Tree.treeToString;
+pretty {A} {{Show A}} : AVLTree A -> String := toTree >> maybe "empty" Tree.treeToString;
 
 instance
-eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) :=
-  mkEq ((==) on toList);
+eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) := mkEq ((==) on toList);
 
 instance
-ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) :=
-  mkOrd (Ord.cmp on toList);
+ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) := mkOrd (Ord.cmp on toList);
diff --git a/Data/Tmp.juvix b/Data/Tmp.juvix
@@ -6,8 +6,7 @@ import Stdlib.Trait open;
 
 printNatListLn : List Nat → IO
   | nil := printStringLn "nil"
-  | (x :: xs) :=
-    printNat x >>> printString " :: " >>> printNatListLn xs;
+  | (x :: xs) := printNat x >>> printString " :: " >>> printNatListLn xs;
 
 mapMaybe {A B} (f : A -> B) : Maybe A -> Maybe B
   | nothing := nothing

diff --git a/Data/Tree.juvix b/Data/Tree.juvix
@@ -10,8 +10,7 @@ Forest (A : Type) : Type := List (Tree A);
 positive
 type Tree (A : Type) := node A (List (Tree A));
 
-shift (first other : String) (xs : List String)
-  : List String :=
+shift (first other : String) (xs : List String) : List String :=
   zipWith (++str) (first :: replicate (length xs) other) xs;
 
 terminating
@@ -22,11 +21,8 @@ terminating
 drawForest {A} {{Show A}} : Forest A -> List String
   | [] := []
   | [h] := "|" :: shift "`- " "   " (draw h)
-  | (h :: hs) :=
-    "|" :: shift "+- " "|  " (draw h) ++ drawForest hs;
+  | (h :: hs) := "|" :: shift "+- " "|  " (draw h) ++ drawForest hs;
 
-treeToString {A} {{Show A}} : Tree A -> String :=
-  draw >> unlines;
+treeToString {A} {{Show A}} : Tree A -> String := draw >> unlines;
 
-forestToString {A} {{Show A}} : Forest A -> String :=
-  drawForest >> unlines;
+forestToString {A} {{Show A}} : Forest A -> String := drawForest >> unlines;
diff --git a/Data/UnbalancedSet.juvix b/Data/UnbalancedSet.juvix
@@ -7,23 +7,20 @@ import Stdlib.Trait.Ord as Ord open using {Ord; mkOrd; module Ord};
 import Data.BinaryTree as Tree;
 open Tree using {BinaryTree; leaf; node};
 
-type UnbalancedSet (A : Type) :=
-  unbalancedSet : Ord A -> BinaryTree A -> UnbalancedSet A;
+type UnbalancedSet (A : Type) := unbalancedSet : Ord A -> BinaryTree A -> UnbalancedSet A;
 
-empty {A} {{o : Ord A}} : UnbalancedSet A :=
-  unbalancedSet o leaf;
+empty {A} {{o : Ord A}} : UnbalancedSet A := unbalancedSet o leaf;
 
 member? {A} (x : A) : UnbalancedSet A -> Bool
   | (unbalancedSet o@(mkOrd cmp) t) :=
     let
       go : BinaryTree A -> Bool
         | leaf := false
         | (node l y r) :=
-          case cmp x y of {
+          case cmp x y of
             | Ord.LT := go l
             | Ord.GT := go r
-            | Ord.EQ := true
-          };
+            | Ord.EQ := true;
     in go t;
 
 insert {A} (x : A) : UnbalancedSet A -> UnbalancedSet A
@@ -32,11 +29,10 @@ insert {A} (x : A) : UnbalancedSet A -> UnbalancedSet A
       go : BinaryTree A -> BinaryTree A
         | leaf := node leaf x leaf
         | n@(node l y r) :=
-          case cmp x y of {
+          case cmp x y of
             | Ord.LT := node (go l) y r
             | Ord.EQ := n
-            | Ord.GT := node l y (go r)
-          };
+            | Ord.GT := node l y (go r);
     in unbalancedSet o (go t);
 
 length {A} : UnbalancedSet A -> Nat

diff --git a/Package.juvix b/Package.juvix
@@ -3,11 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "containers";
-     version := mkVersion 0 12 0;
-     dependencies := [ github
-                       "anoma"
-                       "juvix-stdlib"
-                       "v0.4.0"
-                     ]};
+  defaultPackage@?{
+    name := "containers";
+    version := mkVersion 0 13 0;
+    dependencies := [github "anoma" "juvix-stdlib" "v0.5.0"]
+  };