Remove the idris2 compiler-library package

Dockerfile

@@ -6,6 +6,9 @@ RUN apt-get update && apt-get install --yes jq && rm -rf /var/lib/apt/lists/*
 # install the libraries exercises test against
 RUN pack install contrib tester
 
+# Remove the idris2 compiler-as-a-library package
+RUN rm -rf /root/.local/state/pack/install/*/idris2/idris2-0.8.0/idris2-0.8.0
+
 RUN rm -rf /root/.cache/pack/git
 
 FROM scratch

tests/disjoint-set/disjointset.ipkg

@@ -0,0 +1,5 @@
+package disjointset
+
+sourcedir = "src"
+modules = DisjointSet
+depends = contrib

tests/disjoint-set/expected_results.json

@@ -0,0 +1,4 @@
+{
+  "version": 1,
+  "status": "pass"
+}

tests/disjoint-set/pack.toml

@@ -0,0 +1,10 @@
+[custom.all.disjointset]
+type = "local"
+path = "."
+ipkg = "disjointset.ipkg"
+test = "test/test.ipkg"
+
+[custom.all.disjointset-test]
+type = "local"
+path = "test"
+ipkg = "test.ipkg"

tests/disjoint-set/src/DisjointSet.idr

@@ -0,0 +1,56 @@
+module DisjointSet
+
+import Data.Linear.Array
+
+-- Follow parent links to the representative of `i`.
+findRoot : (1 _ : LinArray Nat) -> Nat -> Res Nat (const (LinArray Nat))
+findRoot arr i =
+  let parent # arr = mread arr (cast i) in
+  case parent of
+    Just p  => if p == i then i # arr else findRoot arr p
+    Nothing => i # arr
+
+-- Point the representative of `i` at the representative of `j`.
+unite : (1 _ : LinArray Nat) -> Nat -> Nat -> LinArray Nat
+unite arr i j =
+  let ri # arr = findRoot arr i
+      rj # arr = findRoot arr j
+      _  # arr = write arr (cast ri) rj in
+  arr
+
+applyAll : (1 _ : LinArray Nat) -> List (Nat, Nat) -> LinArray Nat
+applyAll arr []                = arr
+applyAll arr ((a, b) :: rest)  = applyAll (unite arr a b) rest
+
+-- parent[i] := i for i in [lo, n)
+seed : (n : Nat) -> (lo : Nat) -> (1 _ : LinArray Nat) -> LinArray Nat
+seed n lo arr =
+  if lo >= n
+    then arr
+    else let _ # arr = write arr (cast lo) lo in
+         seed n (S lo) arr
+
+-- Pure representative lookup on the immutable snapshot.
+findRootI : IArray Nat -> Nat -> Nat
+findRootI arr i =
+  case read arr (cast i) of
+    Just p  => if p == i then i else findRootI arr p
+    Nothing => i
+
+-- Count representatives (elements that are their own parent) in [lo, n).
+countRoots : (n : Nat) -> (lo : Nat) -> IArray Nat -> Nat
+countRoots n lo arr =
+  if lo >= n
+    then 0
+    else let here = if findRootI arr lo == lo then 1 else 0 in
+         here + countRoots n (S lo) arr
+
+-- Number of disjoint sets among the elements [0, n) after applying the given
+-- union operations (each pair merges its two elements' sets).
+public export
+countComponents : (n : Nat) -> List (Nat, Nat) -> Nat
+countComponents n edges =
+  newArray (cast n) $ \arr =>
+    let 1 arr = seed n 0 arr
+        1 arr = applyAll arr edges in
+    toIArray arr (\iarr => countRoots n 0 iarr)

tests/disjoint-set/test/src/Main.idr

@@ -0,0 +1,24 @@
+module Main
+
+import System
+import Tester
+import Tester.Runner
+
+import DisjointSet
+
+tests : List Test
+tests =
+  [ test "no unions leaves every element in its own set" $ do
+      assertEq 5 (countComponents 5 [])
+  , test "chained unions merge everything into one set" $ do
+      assertEq 1 (countComponents 4 [(0, 1), (2, 3), (0, 2)])
+  , test "disjoint groups are counted separately" $ do
+      assertEq 3 (countComponents 6 [(0, 1), (1, 2), (3, 4)])
+  ]
+
+main : IO ()
+main = do
+  success <- runTests tests
+  if success
+     then putStrLn "All tests passed"
+     else exitFailure

tests/disjoint-set/test/test.ipkg

@@ -0,0 +1,7 @@
+package disjointset-test
+version = 0.1.0
+depends = disjointset
+  , tester
+executable = "disjointset-test"
+main = Main
+sourcedir = "src"