Use a custom prelude to improve compile performance

Data/BinaryTree.juvix

@@ -1,6 +1,6 @@
 module Data.BinaryTree;
 
-import Stdlib.Prelude open hiding {length};
+import Prelude open;
 
 type BinaryTree (A : Type) :=
   | leaf : BinaryTree A

Data/Map.juvix

@@ -1,24 +1,16 @@
 module Data.Map;
 
-import Stdlib.Prelude open hiding {length};
+import Prelude open;
 
-import Stdlib.Data.Nat.Ord as Nat;
 import Data.Set as Set;
 open Set using {Set};
 
 import Data.Set.AVL as AVL;
 open AVL using {AVLTree};
 
 import Data.BinaryTree as Tree;
-
 import Data.Tmp open;
 
-import Stdlib.Trait.Eq as Eq open using {Eq};
-
-import Stdlib.Trait.Ord as Ord open using {Ord};
-
-import Test.JuvixUnit open;
-
 type Binding A B := binding A B;
 
 key {A B} : Binding A B -> A

Data/Queue/Base.juvix

@@ -9,13 +9,7 @@
 --- performance.
 module Data.Queue.Base;
 
-import Stdlib.Prelude open;
-
-import Stdlib.Trait.Eq as Eq open using {Eq};
-
-import Stdlib.Trait.Ord as Ord open using {Ord};
-
-import Stdlib.Trait.Show as Show open using {Show};
+import Prelude open;
 
 --- A first-in-first-out data structure
 type Queue (A : Type) := queue (List A) (List A);
@@ -76,7 +70,7 @@ size {A} : Queue A -> Nat
 
 instance
 eqQueueI {A} {{Eq A}} : Eq (Queue A) :=
-  mkEq (Eq.eq on toList);
+  mkEq ((==) on toList);
 
 instance
 showQueueI {A} {{Show A}} : Show (Queue A) :=

Data/Set.juvix

@@ -1,10 +1,8 @@
 module Data.Set;
 
-import Stdlib.Prelude open;
 import Data.Set.AVL open public;
 
 import Stdlib.Trait.Eq as Eq open using {Eq};
-
 import Stdlib.Trait.Ord as Ord open using {Ord};
 
 syntax alias Set := AVLTree;

Data/Set/AVL.juvix

@@ -8,17 +8,11 @@
 --- constructing, modifying, and querying AVL trees.
 module Data.Set.AVL;
 
-import Stdlib.Prelude open;
+import Prelude open;
 import Data.Tmp open;
 
-import Stdlib.Data.Int as Int;
-import Stdlib.Data.Int.Ord as Int;
-
 import Data.Tree as Tree open using {Tree; Forest};
 
-import Stdlib.Trait.Eq as Eq open using {Eq};
-import Stdlib.Trait.Ord as Ord open using {Ord};
-
 --- A self-balancing binary search tree.
 type AVLTree (A : Type) :=
   | --- An empty AVL tree.
@@ -44,17 +38,17 @@ type BalanceFactor :=
 diffFactor {A} : AVLTree A -> Int
   | empty := 0
   | (node _ _ left right) :=
-    Int.intSubNat (height right) (height left);
+    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 if
-    (0 Int.< diff)
+    (0 < diff)
     LeanRight
-    (if (diff Int.< 0) LeanLeft LeanNone);
+    (if (diff < 0) LeanLeft LeanNone);
 
 --- 𝒪(1). Helper function for creating a node.
 mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A)
@@ -217,7 +211,7 @@ prettyDebug {A} {{Show A}} : AVLTree A -> String :=
         "("
           ++str go l
           ++str " h"
-          ++str Int.intToString (diffFactor n)
+          ++str Show.show (diffFactor n)
           ++str " "
           ++str Show.show v
           ++str " "
@@ -238,7 +232,7 @@ pretty {A} {{Show A}} : AVLTree A -> String :=
 
 instance
 eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) :=
-  mkEq (Eq.eq on toList);
+  mkEq ((==) on toList);
 
 instance
 ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) :=

Data/Tmp.juvix

@@ -1,7 +1,7 @@
 --- the functions here should be eventually put in the stdlib
 module Data.Tmp;
 
-import Stdlib.Prelude open;
+import Prelude open;
 
 printNatListLn : List Nat → IO
   | nil := printStringLn "nil"

Data/Tree.juvix

@@ -1,7 +1,7 @@
 --- N-Ary trees with pretty printing.
 module Data.Tree;
 
-import Stdlib.Prelude open;
+import Prelude open;
 
 --- A ;List; of trees.
 Forest (A : Type) : Type := List (Tree A);

Data/UnbalancedSet.juvix

@@ -1,10 +1,8 @@
 module Data.UnbalancedSet;
 
-import Stdlib.Prelude open hiding {length};
+import Prelude open;
 
-import Test.JuvixUnit open;
-
-import Stdlib.Trait.Ord as Ord;
+import Stdlib.Trait.Ord as Ord open using {Ord; mkOrd; module Ord};
 
 import Data.BinaryTree as Tree;
 open Tree using {BinaryTree; leaf; node};

Makefile

@@ -1,35 +1,18 @@
-
 all: test
 
-build/UnbalancedSet: $(wildcard ./**/*.juvix)
-	@mkdir -p build/
-	juvix compile Test/UnbalancedSet.juvix -o build/UnbalancedSet
-
-build/Map: $(wildcard ./**/*.juvix)
-	@mkdir -p build/
-	juvix compile Test/Map.juvix -o build/Map
-
-build/AVL: $(shell find . -name '*.juvix')
-	@mkdir -p build/
-	juvix compile Test/AVL.juvix -o build/AVL
-
-build/Queue: $(shell find . -name '*.juvix')
+build/Main: $(wildcard ./**/*.juvix)
 	@mkdir -p build/
-	juvix compile Test/Queue.juvix -o build/Queue
+	juvix compile test/Main.juvix -o build/Main
 
 .PHONY : test
-test: build/UnbalancedSet \
-		build/Map \
-		build/AVL \
-		build/Queue
-	./build/UnbalancedSet
-	./build/Map
-	./build/AVL
-	./build/Queue
+test: build/Main
+	./build/Main
 
 .PHONY: clean-build
 clean-build:
 	@rm -rf build/
+	@juvix clean
+	@(cd test && exec juvix clean)
 
 .PHONY: clean
 clean: clean-build

Package.juvix

@@ -1,11 +1,9 @@
 module Package;
 
-import PackageDescription.V1 open;
+import PackageDescription.V2 open;
 
 package : Package :=
   defaultPackage
     {name := "containers";
-     version := mkVersion 0 8 0;
-     dependencies := [ github "anoma" "juvix-stdlib" "v0.0.1"
-                     ; github "anoma" "juvix-test" "v0.7.0"
-                     ]};
+     version := mkVersion 0 9 0;
+     dependencies := [github "anoma" "juvix-stdlib" "v0.1.0"]};

Prelude.juvix

@@ -0,0 +1,18 @@
+module Prelude;
+
+import Juvix.Builtin.V1 open public;
+import Stdlib.Data.String.Base open public;
+import Stdlib.Data.Product open public;
+import Stdlib.Data.List.Base open public;
+import Stdlib.System.IO.Base open public;
+import Stdlib.System.IO.String open public;
+import Stdlib.System.IO.Nat open public;
+import Stdlib.Function open public;
+import Stdlib.Trait.Show open public;
+import Stdlib.Data.Bool.Base open public;
+import Stdlib.Data.Maybe open public;
+import Stdlib.Trait.Eq open public;
+import Stdlib.Trait.Ord open public;
+import Stdlib.Trait.Show open public;
+import Stdlib.Data.List open public;
+import Stdlib.Data.Int open public;

juvix.lock.yaml

@@ -1,19 +1,11 @@
 # This file was autogenerated by Juvix version 0.5.4.
 # Do not edit this file manually.
 
+version: 2
+checksum: fa591889966c8c48ba4f7528645bf526750780d41cb9ec603d473a020f6f58cd
 dependencies:
 - git:
     name: anoma_juvix-stdlib
-    ref: f68b0614ad695eaa13ead42f3466e0a78219f826
+    ref: 183d4e9329a648b339ebecf2122b3e9621c99ee8
     url: https://github.com/anoma/juvix-stdlib
   dependencies: []
-- git:
-    name: anoma_juvix-test
-    ref: 3ed8a393b45c75af2c2f4bc0b5262ce9f1115a05
-    url: https://github.com/anoma/juvix-test
-  dependencies:
-  - git:
-      name: anoma_juvix-stdlib
-      ref: f68b0614ad695eaa13ead42f3466e0a78219f826
-      url: https://github.com/anoma/juvix-stdlib
-    dependencies: []

test/Main.juvix

@@ -0,0 +1,10 @@
+module Main;
+
+import Test.JuvixUnit open;
+import Stdlib.System.IO open;
+import Test.AVL open using {suite as avlSuite};
+import Test.Map open using {suite as mapSuite};
+import Test.Queue open using {suite as queueSuite};
+import Test.UnbalancedSet open using {suite as unbalancedSetSuite};
+
+main : IO := runTestSuite avlSuite >> runTestSuite mapSuite >> runTestSuite queueSuite >> runTestSuite unbalancedSetSuite;

test/Package.juvix

@@ -0,0 +1,12 @@
+module Package;
+
+import PackageDescription.V2 open;
+
+package : Package :=
+  defaultPackage
+    {name := "containers-tests";
+     main := just "Main.juvix";
+     dependencies := [ github "anoma" "juvix-stdlib" "v0.1.0"
+                     ; github "anoma" "juvix-test" "v0.8.0"
+                     ; path "../"
+                     ]};

Test/AVL.juvix → test/Test/AVL.juvix

@@ -1,8 +1,13 @@
 module Test.AVL;
 
 import Test.JuvixUnit open;
+import Juvix.Builtin.V1 open;
+import Stdlib.System.IO.Base open;
+import Stdlib.System.IO.String open;
+import Stdlib.Data.Product open;
+import Stdlib.Data.List.Base open;
+
 import Data.Set.AVL open;
-import Stdlib.Prelude open;
 
 --- Test for size and balance.
 mkTests : String × Nat × AVLTree Nat -> List Test
@@ -42,7 +47,9 @@ tests : List Test :=
   ]
     ++ concatMap mkTests [s1; s2; s3; s4; s2-delete];
 
+suite : TestSuite := testSuite "AVL Set" tests;
+
 main : IO :=
   printStringLn (pretty (snd (snd s1)))
     >> printStringLn (prettyDebug (snd (snd s1)))
-    >> runTestSuite (testSuite "AVL Set" tests);
+    >> runTestSuite suite;

Test/Map.juvix → test/Test/Map.juvix

@@ -1,6 +1,10 @@
 module Test.Map;
 
-import Stdlib.Prelude open;
+import Juvix.Builtin.V1 open;
+import Stdlib.System.IO.Base open;
+import Stdlib.Data.Product open;
+import Stdlib.Data.List open using {quickSort};
+import Stdlib.Function open;
 import Test.JuvixUnit open;
 
 import Data.Map as Map;
@@ -58,4 +62,6 @@ tests : List Test :=
          [1, 1; 2, 2])
      ];
 
-main : IO := runTestSuite (testSuite "Map" tests);
+suite : TestSuite := testSuite "Map" tests;
+
+main : IO := runTestSuite suite;

Test/Queue.juvix → test/Test/Queue.juvix

@@ -1,9 +1,11 @@
 module Test.Queue;
 
-import Stdlib.Prelude open hiding {head; tail};
-import Stdlib.Data.Nat open;
-import Stdlib.Data.Maybe open;
+import Juvix.Builtin.V1 open;
+import Stdlib.System.IO.Base open;
+import Stdlib.Function open;
+import Stdlib.Data.Product open;
 import Test.JuvixUnit open;
+
 import Data.Queue open;
 
 q : Queue Nat := empty;
@@ -53,4 +55,6 @@ tests : List Test :=
          ((just ∘ fromList) [2; 3]))
      ];
 
-main : IO := runTestSuite $ testSuite "Queue" tests;
+suite : TestSuite := testSuite "Queue" tests;
+
+main : IO := runTestSuite suite;

Test/UnbalancedSet.juvix → test/Test/UnbalancedSet.juvix

@@ -1,6 +1,8 @@
 module Test.UnbalancedSet;
 
-import Stdlib.Prelude open;
+import Juvix.Builtin.V1 open;
+import Stdlib.Data.List open using {quickSort};
+import Stdlib.System.IO.Base open;
 import Test.JuvixUnit open;
 
 import Data.UnbalancedSet as Set;
@@ -38,4 +40,6 @@ tests : List Test :=
        (assertEqual "unexpected size" (Set.length setInSet) 1)
      ];
 
-main : IO := runTestSuite (testSuite "Set" tests);
+suite : TestSuite := testSuite "UnbalancedSet" tests;
+
+main : IO := runTestSuite suite;

test/juvix.lock.yaml

@@ -0,0 +1,28 @@
+# This file was autogenerated by Juvix version 0.5.4.
+# Do not edit this file manually.
+
+version: 2
+checksum: 9c99d2249f3a436551c361e1eb5bdec14679659d0773f19b5ff134a59e40dddc
+dependencies:
+- git:
+    name: anoma_juvix-stdlib
+    ref: 183d4e9329a648b339ebecf2122b3e9621c99ee8
+    url: https://github.com/anoma/juvix-stdlib
+  dependencies: []
+- git:
+    name: anoma_juvix-test
+    ref: 61c5404bddd04b5d768739192a25f1c3a6bce9eb
+    url: https://github.com/anoma/juvix-test
+  dependencies:
+  - git:
+      name: anoma_juvix-stdlib
+      ref: 183d4e9329a648b339ebecf2122b3e9621c99ee8
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []
+- path: ../
+  dependencies:
+  - git:
+      name: anoma_juvix-stdlib
+      ref: 183d4e9329a648b339ebecf2122b3e9621c99ee8
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []