[ fix ] missing modules in .ipkg files (#3124)

Additionally, we now have bash options to make sure we will fail hard were
this situation to arise once again.

.github/scripts/katla.sh

@@ -1,4 +1,7 @@
-#!/bin/sh
+#!/bin/bash
+
+set -eu
+set -o pipefail
 
 prefix="../../libs"
 

libs/base/Data/List.idr

@@ -561,6 +561,11 @@ init [] impossible
 init [x] = []
 init (x :: xs@(_::_)) = x :: init xs
 
+||| Computes the minimum of a non-empty list
+public export
+minimum : Ord a => (xs : List a) -> {auto 0 _ : NonEmpty xs} -> a
+minimum (x :: xs) = foldl min x xs
+
 ||| Attempt to deconstruct the list into a head and a tail.
 public export
 uncons' : List a -> Maybe (a, List a)

libs/base/base.ipkg

@@ -6,9 +6,9 @@ opts = "--ignore-missing-ipkg -Wno-shadowing"
 modules = Control.App,
           Control.App.Console,
           Control.App.FileIO,
-
           Control.Applicative.Const,
-
+          Control.Function,
+          Control.Function.FunExt,
           Control.Monad.Either,
           Control.Monad.Error.Either,
           Control.Monad.Error.Interface,
@@ -28,12 +28,11 @@ modules = Control.App,
           Control.Monad.Writer,
           Control.Monad.Writer.CPS,
           Control.Monad.Writer.Interface,
-          Control.WellFounded,
-          Control.Function,
-          Control.Function.FunExt,
-          Control.Relation,
           Control.Ord,
           Control.Order,
+          Control.Relation,
+          Control.Relation.Closure,
+          Control.WellFounded,
 
           Data.Bifoldable,
           Data.Bits,
@@ -45,7 +44,6 @@ modules = Control.App,
           Data.Contravariant,
           Data.DPair,
           Data.Either,
-          Data.Integral,
           Data.Fin,
           Data.Fin.Order,
           Data.Fuel,
@@ -53,19 +51,16 @@ modules = Control.App,
           Data.IOArray,
           Data.IOArray.Prims,
           Data.IORef,
+          Data.Integral,
           Data.List,
-          Data.SnocList,
-          Data.SnocList.Elem,
-          Data.SnocList.Quantifiers,
-          Data.SnocList.Operations,
           Data.List.Elem,
           Data.List.HasLength,
-          Data.List.Views,
           Data.List.Quantifiers,
+          Data.List.Views,
           Data.List1,
           Data.List1.Elem,
-          Data.List1.Quantifiers,
           Data.List1.Properties,
+          Data.List1.Quantifiers,
           Data.Maybe,
           Data.Morphisms,
           Data.Nat,
@@ -75,6 +70,10 @@ modules = Control.App,
           Data.Ref,
           Data.Rel,
           Data.Singleton,
+          Data.SnocList,
+          Data.SnocList.Elem,
+          Data.SnocList.Operations,
+          Data.SnocList.Quantifiers,
           Data.So,
           Data.SortedMap,
           Data.SortedMap.Dependent,
@@ -83,23 +82,23 @@ modules = Control.App,
           Data.String,
           Data.These,
           Data.Vect,
-          Data.Vect.Elem,
           Data.Vect.AtIndex,
+          Data.Vect.Elem,
           Data.Vect.Quantifiers,
           Data.Zippable,
 
           Debug.Trace,
 
+          Decidable.Decidable,
+          Decidable.Equality,
+          Decidable.Equality.Core,
+
           Deriving.Common,
           Deriving.Foldable,
           Deriving.Functor,
           Deriving.Show,
           Deriving.Traversable,
 
-          Decidable.Decidable,
-          Decidable.Equality,
-          Decidable.Equality.Core,
-
           Language.Reflection,
           Language.Reflection.TT,
           Language.Reflection.TTImp,

libs/contrib/Data/IOMatrix.idr

@@ -0,0 +1,43 @@
+module Data.IOMatrix
+
+import Data.IOArray.Prims
+
+%default total
+
+export
+record IOMatrix a where
+  constructor MkIOMatrix
+  maxWidth  : Int
+  maxHeight : Int
+  content   : ArrayData (Maybe a)
+
+export
+width : IOMatrix a -> Int
+width = maxWidth
+
+export
+height : IOMatrix a -> Int
+height = maxHeight
+
+export
+new : HasIO io => (width, height : Int) -> io (IOMatrix a)
+new width height
+  = pure $ MkIOMatrix width height
+         !(primIO (prim__newArray (width * height) Nothing))
+
+toPosition : IOMatrix a -> Int -> Int -> Maybe Int
+toPosition (MkIOMatrix w h arr) i j
+  = do guard (not (i < 0 || j < 0 || i >= w || j >= h))
+       pure (i * h + j)
+
+export
+write : HasIO io => IOMatrix a -> Int -> Int -> a -> io Bool
+write mat i j el = case toPosition mat i j of
+  Nothing => pure False
+  Just pos => True <$ primIO (prim__arraySet (content mat) pos (Just el))
+
+export
+read : HasIO io => IOMatrix a -> Int -> Int -> io (Maybe a)
+read mat i j = case toPosition mat i j of
+  Nothing => pure Nothing
+  Just pos => primIO (prim__arrayGet (content mat) pos)

libs/contrib/contrib.ipkg

@@ -35,6 +35,8 @@ modules = Control.ANSI,
 
           Data.Int.Order,
 
+          Data.IOMatrix,
+
           Data.Late,
 
           Data.Linear.Array,
@@ -118,6 +120,7 @@ modules = Control.ANSI,
 
           Debug.Buffer,
 
+          Decidable.Finite.Fin,
           Decidable.Order.Strict,
           Decidable.Decidable.Extra,
 
@@ -140,6 +143,7 @@ modules = Control.ANSI,
           System.Path,
 
           Text.Bounded,
+          Text.Distance.Levenshtein,
           Text.Lexer,
           Text.Lexer.Core,
           Text.Lexer.Tokenizer,

src/Libraries/Text/Distance/Levenshtein.idr

@@ -2,7 +2,7 @@ module Libraries.Text.Distance.Levenshtein
 
 import Data.String
 import Libraries.Data.IOMatrix
-import Libraries.Data.List.Extra
+import Libraries.Data.List.Extra as Lib
 
 %default total
 
@@ -15,10 +15,11 @@ spec a b = loop (fastUnpack a) (fastUnpack b) where
   loop xs [] = length xs -- insertions
   loop (x :: xs) (y :: ys)
     = if x == y then loop xs ys -- match
-      else 1 + minimum [ loop (x :: xs) ys -- insert y
-                       , loop xs (y :: ys) -- delete x
-                       , loop xs ys        -- substitute y for x
-                       ]
+      else 1 + Lib.minimum
+           [ loop (x :: xs) ys -- insert y
+           , loop xs (y :: ys) -- delete x
+           , loop xs ys        -- substitute y for x
+           ]
 
 ||| Dynamic programming
 export
@@ -57,11 +58,11 @@ compute a b = do
                  in if c == d then 0 else
                     if isAlpha c && isAlpha d then 1 else
                     if isDigit c && isDigit d then 1 else 2
-      write mat i j $
-        minimum [ 1    + !(get i (j-1))     -- insert y
-                , 1    + !(get (i-1) j)     -- delete x
-                , cost + !(get (i-1) (j-1)) -- equal or substitute y for x
-                ]
+      write mat i j $ Lib.minimum
+        [ 1    + !(get i (j-1))     -- insert y
+        , 1    + !(get (i-1) j)     -- delete x
+        , cost + !(get (i-1) (j-1)) -- equal or substitute y for x
+        ]
 
   -- Once the matrix is fully filled, we can simply read the top right corner
   integerToNat . cast <$> get w h

tests/idris2/reflection/reflection025/expected

@@ -43,7 +43,7 @@ LOG elab:0: current fn: [< CurrFn.f]
 LOG elab:0: current fn: [< CurrFn.f']
 LOG elab:0: current fn: [< CurrFn.f'']
 LOG elab:0: current fn: [< CurrFn.f''', CurrFn.case block in "f'''"]
-LOG elab:0: current fn: [< CurrFn.n, CurrFn.4799:2662:f]
+LOG elab:0: current fn: [< CurrFn.n, CurrFn.4800:2662:f]
 LOG elab:0: current fn: [< CurrFn.w, CurrFn.with block in "w"]
 LOG elab:0: current fn: [< CurrFn.w, CurrFn.with block in "w"]
 ------------
@@ -53,7 +53,7 @@ LOG elab:0: === current fn: [< RefDefsDeep.f] ===
 LOG elab:0: === current fn: [< RefDefsDeep.f'] ===
 LOG elab:0: === current fn: [< RefDefsDeep.f''] ===
 LOG elab:0: === current fn: [< RefDefsDeep.f''', RefDefsDeep.case block in "f'''"] ===
-LOG elab:0: === current fn: [< RefDefsDeep.n, RefDefsDeep.4813:2927:f] ===
+LOG elab:0: === current fn: [< RefDefsDeep.n, RefDefsDeep.4814:2927:f] ===
 LOG elab:0: === current fn: [< RefDefsDeep.w, RefDefsDeep.with block in "w"] ===
 LOG elab:0: === current fn: [< RefDefsDeep.w, RefDefsDeep.with block in "w"] ===
 LOG elab:0: Names `RefDefsDeep.f` refers to:
@@ -174,7 +174,7 @@ LOG elab:0:   - Prelude.Basics.True
 LOG elab:0:   - Prelude.Basics.False
 LOG elab:0:   - Builtin.assert_total
 LOG elab:0:   - Builtin.MkUnit
-LOG elab:0:   - RefDefsDeep.4813:2927:f
+LOG elab:0:   - RefDefsDeep.4814:2927:f
 LOG elab:0:   - RefDefsDeep.case block in "n,f"
 LOG elab:0: 
 LOG elab:0: Names `RefDefsDeep.w` refers to:

www/source/index.md

@@ -84,6 +84,12 @@ you will need to pass `-p linear` to `idris2` to use modules defined in it.
 Similarly to `contrib` and `linear`, you will need to pass `-p network`
 to `idris2` to use modules defined in it.
 
+#### [Test](https://idris-lang.github.io/Idris2/test)
+
+`test` is the add-on to `base` you'll need to write test suites.
+Similarly to other add-ons, you will need to pass `-p test` to
+`idris2` to use modules defined in it.
+
 #### [Papers](https://idris-lang.github.io/Idris2/papers)
 
 `papers` is not installed by default.