Style & efficiency improvements

Data/BinaryTree.juvix

@@ -6,19 +6,14 @@ type BinaryTree (A : Type) :=
   | leaf : BinaryTree A
   | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
 
--- fold a tree in depth first order
-fold
-  : {A B : Type}
-    -> (A -> B -> B -> B)
-    -> B
-    -> BinaryTree A
-    -> B
-  | {A} {B} f acc :=
-    let
-      go (acc : B) : BinaryTree A -> B
-        | leaf := acc
-        | (node l a r) := f a (go acc l) (go acc r);
-    in go acc;
+--- fold a tree in depth first order
+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;

Data/Map.juvix

@@ -19,7 +19,7 @@ import Stdlib.Trait.Ord as Ord open using {Ord};
 
 import Test.JuvixUnit open;
 
-type Binding (A B : Type) := binding A B;
+type Binding A B := binding A B;
 
 key {A B} : Binding A B -> A
   | (binding a _) := a;
@@ -34,13 +34,13 @@ instance
 bindingKeyOrdering {A B} {{Ord A}} : Ord (Binding A B) :=
   mkOrd λ {b1 b2 := Ord.cmp (key b1) (key b2)};
 
-type Map (A B : Type) := mkMap (AVLTree (Binding A B));
+type Map A B := mkMap (AVLTree (Binding A B));
 
-empty : {A B : Type} -> Map A B := mkMap AVL.empty;
+empty {A B} : Map A B := mkMap AVL.empty;
 
-insertWith {A B} {{Ord A}}
-  : (B -> B -> B) -> A -> B -> Map A B -> Map A B
-  | f k v (mkMap s) :=
+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);
@@ -53,16 +53,15 @@ insert {A B : Type} {{Ord A}}
 lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B
   | (mkMap s) := mapMaybe value (Set.lookupWith key k s);
 
-fromListWith {A B} {{Ord A}}
-  : (B -> B -> B) -> List (A × B) -> Map A B
-  | f xs :=
-    for (acc := empty) (k, v in xs)
-      insertWith f k v acc;
+fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List
+  (A × B)) : Map A B :=
+  for (acc := empty) (k, v in xs)
+    insertWith f k v acc;
 
 fromList {A B} {{Ord A}} : List (A × B) -> Map A B :=
   fromListWith λ {old new := new};
 
-toList {A B : Type} : Map A B -> List (A × B)
+toList {A B} : Map A B -> List (A × B)
   | (mkMap s) := map (x in Set.toList s) toPair x;
 
 size {A B} : Map A B -> Nat

Data/Queue/Base.juvix

@@ -1,10 +1,10 @@
 --- This module provides an implementation of a First-In, First-Out (FIFO)
 --- queue based on Okasaki's "Purely Functional Data Structures." Ch.3.
 ---
---- This Okasaki Queue version data structure ensures worst-case constant-time
+--- This Okasaki Queue version data structure ensures amortized constant-time
 --- performance for basic operations such as push, pop, and front.
 ---
---- The OkasakiQueue consists of two lists (front and back) to separate
+--- The Okasaki Queue consists of two lists (front and back) to separate
 --- the concerns of adding and removing elements for ensuring efficient
 --- performance.
 module Data.Queue.Base;
@@ -33,18 +33,20 @@ head {A} : Queue A -> Maybe A
   | (queue nil _) := nothing
   | (queue (x :: _) _) := just x;
 
---- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
+--- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty
+--  then returns ;nothing;.
 tail {A} : Queue A -> Maybe (Queue A)
   | (queue nil _) := nothing
   | (queue (_ :: front) back) := just (queue front back);
 
---- 𝒪(n) in the worst-case scenario, but 𝒪(1) amortized
+--- 𝒪(n) worst-case, but 𝒪(1) amortized
+{-# inline: true #-}
 check {A} : Queue A -> Queue A
   | (queue nil back) := queue (reverse back) nil
   | q := q;
 
---- 𝒪(1). Returns the first element and the rest of the ;Queue;.
---- If the ;Queue; is empty then returns ;nothing;.
+--- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the
+--  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
 pop {A} : Queue A -> Maybe (A × Queue A)
   | (queue nil _) := nothing
   | (queue (x :: front) back) :=
@@ -55,8 +57,9 @@ 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) : Queue A -> Queue A
-  | q := foldr push q xs;
+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;
@@ -65,7 +68,7 @@ fromList {A} (xs : List A) : Queue A := pushMany xs empty;
 --- The elements are in the same order as they appear in the ;Queue;
 --- (i.e. the first element of the ;Queue; is the first element of the ;List;).
 toList {A} : Queue A -> List A
-  | (queue front back) := back ++ reverse front;
+  | (queue front back) := front ++ reverse back;
 
 --- 𝒪(n). Returns the number of elements in the ;Queue;.
 size {A} : Queue A -> Nat

Data/Set.juvix

@@ -7,8 +7,7 @@ import Stdlib.Trait.Eq as Eq open using {Eq};
 
 import Stdlib.Trait.Ord as Ord open using {Ord};
 
-Set : Type -> Type
-  | A := AVLTree A;
+syntax alias Set := AVLTree;
 
 eqSetI {A} {{Eq A}} : Eq (Set A) := eqAVLTreeI;
 

Data/Set/AVL.juvix

@@ -43,25 +43,26 @@ type BalanceFactor :=
   | --- Right children is higher.
     LeanRight;
 
+{-# inline: true #-}
 diffFactor {A} : AVLTree A -> Int
   | empty := 0
   | (node _ _ left right) :=
     Int.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} : AVLTree A -> BalanceFactor
-  | n :=
-    let
-      diff : Int := diffFactor n;
-    in if
-      (0 Int.< diff)
-      LeanRight
-      (if (diff Int.< 0) LeanLeft LeanNone);
+balanceFactor {A} (t : AVLTree A) : BalanceFactor :=
+  let
+    diff : Int := diffFactor t;
+  in if
+    (0 Int.< diff)
+    LeanRight
+    (if (diff Int.< 0) LeanLeft LeanNone);
 
 --- 𝒪(1). Helper function for creating a node.
-mknode {A} : A -> AVLTree A -> AVLTree A -> AVLTree A
-  | val l r := node val (1 + max (height l) (height r)) l r;
+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.
 rotateLeft {A} : AVLTree A -> AVLTree A
@@ -75,7 +76,7 @@ rotateRight {A} : AVLTree A -> AVLTree A
   | n := n;
 
 --- 𝒪(1). Applies local rotations if needed.
-balance : {a : Type} -> AVLTree a -> AVLTree a
+balance : {A : Type} -> AVLTree A -> AVLTree A
   | empty := empty
   | n@(node x h l r) :=
     let
@@ -95,60 +96,61 @@ balance : {a : Type} -> AVLTree a -> AVLTree a
     };
 
 --- 𝒪(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} {{Ord k}}
-  : (a -> k) -> k -> AVLTree a -> Maybe a
-  | f x :=
-    let
-      go : AVLTree a -> Maybe a
-        | empty := nothing
-        | m@(node y h l r) :=
-          case Ord.cmp x (f y) of {
-            | LT := go l
-            | GT := go r
-            | EQ := just y
-          };
-    in go;
+--- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
+{-# specialize: [1] #-}
+lookupWith {A K} {{Ord K}} (f : A -> K) (x : K)
+  : AVLTree A -> Maybe A :=
+  let
+    {-# specialize-by: [f] #-}
+    go : AVLTree A -> Maybe A
+      | empty := nothing
+      | m@(node y h l r) :=
+        case Ord.cmp x (f y) of {
+          | LT := go l
+          | GT := go r
+          | EQ := just y
+        };
+  in go;
 
 --- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
-member? {a} {{Ord a}} : a -> AVLTree a -> Bool
-  | x := isJust ∘ lookupWith id x;
+member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool :=
+  isJust ∘ lookupWith id x;
 
 --- 𝒪(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} {{Ord a}}
-  : (a -> a -> a) -> a -> AVLTree a -> AVLTree a
-  | f x :=
-    let
-      go : AVLTree a -> AVLTree a
-        | empty := mknode x empty empty
-        | m@(node y h l r) :=
-          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
-          };
-    in go;
+{-# specialize: [1] #-}
+insertWith {A} {{Ord A}} (f : A -> A -> A) (x : A)
+  : AVLTree A -> AVLTree A :=
+  let
+    {-# specialize-by: [f] #-}
+    go : AVLTree A -> AVLTree A
+      | empty := mknode x empty empty
+      | m@(node y h l r) :=
+        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
+        };
+  in go;
 
 --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;.
-insert {a : Type} {{Ord a}} : a -> AVLTree a -> AVLTree a :=
+insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A :=
   insertWith (flip const);
 
 --- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
-delete {a : Type} {{Ord a}} (x : a)
-  : AVLTree a -> AVLTree a :=
+delete {A} {{Ord A}} (x : A) : AVLTree A -> AVLTree A :=
   let
-    deleteMin : AVLTree a -> Maybe (a × AVLTree a)
+    deleteMin : AVLTree A -> Maybe (A × AVLTree A)
       | empty := nothing
       | (node v _ l r) :=
         case deleteMin l of {
           | nothing := just (v, r)
           | just (m, l') := just (m, mknode v l' r)
         };
-    go : AVLTree a -> AVLTree a
+    go : AVLTree A -> AVLTree A
       | empty := empty
       | (node y h l r) :=
         case Ord.cmp x y of {
@@ -167,50 +169,49 @@ delete {a : Type} {{Ord a}} (x : a)
   in go;
 
 --- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;.
-lookupMin : {a : Type} -> AVLTree a -> Maybe a
+lookupMin {A} : AVLTree A -> Maybe A
   | empty := nothing
   | (node y _ empty empty) := just y
   | (node _ _ empty r) := lookupMin r
   | (node _ _ l _) := lookupMin l;
 
 --- 𝒪(log 𝓃). Returns the maximum element of the ;AVLTree;.
-lookupMax : {a : Type} -> AVLTree a -> Maybe a
+lookupMax {A} : AVLTree A -> Maybe A
   | empty := nothing
   | (node y _ empty empty) := just y
   | (node _ _ l empty) := lookupMax l
   | (node _ _ _ r) := lookupMax r;
 
 --- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;.
-deleteMany {a : Type} {{Ord a}}
-  : List a -> AVLTree a -> AVLTree a
-  | d t := 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 : Type} -> AVLTree a -> Bool
+isBalanced {A} : AVLTree A -> Bool
   | empty := true
   | n@(node _ _ l r) :=
     isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
 
 --- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
-fromList {a : Type} {{Ord a}} (l : List a) : AVLTree a :=
+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 : Type} -> AVLTree a -> Nat
+size {A} : AVLTree A -> Nat
   | empty := 0
   | (node _ _ l r) := 1 + size l + size r;
 
 --- 𝒪(𝓃). Returns the elements of an ;AVLTree; in ascending order.
-toList : {a : Type} -> AVLTree a -> List a
+toList {A} : AVLTree A -> List A
   | empty := nil
   | (node x _ l r) := toList l ++ (x :: nil) ++ toList r;
 
 --- 𝒪(𝓃). Formats the tree in a debug friendly format.
-prettyDebug {a : Type} {{Show a}} : AVLTree a -> String :=
+prettyDebug {A} {{Show A}} : AVLTree A -> String :=
   let
-    go : AVLTree a -> String
+    go : AVLTree A -> String
       | empty := "_"
       | n@(node v h l r) :=
         "("
@@ -225,14 +226,14 @@ prettyDebug {a : Type} {{Show a}} : AVLTree a -> String :=
   in go;
 
 --- 𝒪(𝓃).
-toTree : {a : Type} -> AVLTree a -> Maybe (Tree a)
+toTree {A} : AVLTree A -> Maybe (Tree A)
   | empty := nothing
   | (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 :=
+pretty {A} {{Show A}} : AVLTree A -> String :=
   maybe "empty" Tree.treeToString ∘ toTree;
 
 instance

Data/String.juvix

@@ -3,5 +3,4 @@ module Data.String;
 import Stdlib.Prelude open;
 import Stdlib.Data.String.Ord open;
 
-null? : String -> Bool
-  | s := s == "";
+null? (s : String) : Bool := s == "";

Data/Tmp.juvix

@@ -8,16 +8,10 @@ printNatListLn : List Nat → IO
   | (x :: xs) :=
     printNat x >> printString " :: " >> printNatListLn xs;
 
-mapMaybe : {A B : Type} -> (A -> B) -> Maybe A -> Maybe B
-  | f m :=
-    case m of {
-      | nothing := nothing
-      | just a := just (f a)
-    };
+mapMaybe {A B} (f : A -> B) : Maybe A -> Maybe B
+  | nothing := nothing
+  | (just a) := just (f a);
 
-isJust : {A : Type} -> Maybe A -> Bool
-  | m :=
-    case m of {
-      | nothing := false
-      | just _ := true
-    };
+isJust {A} : Maybe A -> Bool
+  | nothing := false
+  | (just _) := true;