chore: update to idris2-pkgs:latest

bobbbay · Apr 23, 2022 · 4302331 · 4302331
1 parent 71b0fb1
commit 4302331
Show file tree

Hide file tree

Showing 8 changed files with 280 additions and 109 deletions.
diff --git a/README.org b/README.org
@@ -10,7 +10,7 @@ N-dimensional arrays in Idris 2, featuring:
 At a very basic level, the API for an N-dimensional array in Dinwiddy is the following:
 
 #+begin_src idris
-Array (dimension : Nat) (sizes : Vect d Nat) (type : Type)
+Array : (dimension : Nat) -> (sizes : Vect dimension Nat) -> (type : Type)
 #+end_src
 
 For example, the following type declaration =x=:
@@ -33,4 +33,4 @@ x = [[ True,  True,  True ],
      [ False, False, True ]]
 #+end_src
 
-Check out =src= for more types and documentation. =examples/Life.idr= is a (WIP) implementation of Conway's game of life using Dinwiddy.
+Check out `examples` and `tests` for more information.
diff --git a/examples/Life.idr → examples/Examples/Life.idr b/examples/Life.idr → examples/Examples/Life.idr
@@ -1,33 +1,32 @@
-module Life
-
--- This example is a work in progress, as Dinwiddy evolves :).
+module Examples.Life
 
 import Dinwiddy
 
 import Data.Vect
 import Data.Fin
+
+||| Width of the board.
+W : Nat
+W = 10
+
+||| Height of the board.
+H : Nat
+H = 10
 
-||| A type for the size of the board.
+||| The size of the board.
 BoardSize : Vect 2 Nat
-BoardSize = [10, 10]
+BoardSize = [W, H]
 
-||| A basic board type: a 2D array of 10x10.
+||| A basic board type: a 2D array of Bools, with the size of BoardSize.
+||| A square is dead if it is False, and alive if it is True.
 Board : Type
 Board = Array 2 BoardSize Bool
 
 mutual
   ||| Given a board, apply another step onto it, effectively looping over every
   ||| point and calculating its status.
   step : Board -> Board
-
-  ||| Same as `step`, but does the bulk looping process.
-  step' : Vect n (Vect m Bool) -> Vect n (Vect m Bool)
-
-  isAlive : (Fin n, Fin m) -> Vect n (Vect m Bool) -> Bool
-  isAlive _ _ = True
-
-  ||| Given a location and a board, calculate the # of surrounding living blocks.
-  neighbours : (Fin 10, Fin 10) -> Board -> Nat
+  step b = b
 
 example : Board
 example = [[True, True, True, True, True, True, True, True, True, True],

diff --git a/examples/Examples/Main.idr b/examples/Examples/Main.idr
@@ -0,0 +1,7 @@
+module Examples.Main
+
+import Examples.Life
+
+main : IO ()
+main = do life
+          putStrLn "done examples"
diff --git a/examples/Main.idr b/examples/Main.idr
diff --git a/examples/examples.ipkg b/examples/examples.ipkg
@@ -2,9 +2,9 @@ package examples
 
 depends = dinwiddy
 
-modules = Main
-        , Life
+modules = Examples.Main
+        , Examples.Life
 
-main = Main
+main = Examples.Main
 
 executable = examples