Add some sketches of Fathom’s core in Idris 2

.github/workflows/ci.yml

@@ -23,11 +23,11 @@ jobs:
         uses: cachix/install-nix-action@v17
 
       - name: cargo check
-        run: nix develop .#${{ matrix.rust-toolchain }} --command cargo check
+        run: nix develop .#rust-${{ matrix.rust-toolchain }} --command cargo check
       - name: cargo build
-        run: nix develop .#${{ matrix.rust-toolchain }} --command cargo build
+        run: nix develop .#rust-${{ matrix.rust-toolchain }} --command cargo build
       - name: cargo test
-        run: nix develop .#${{ matrix.rust-toolchain }} --command cargo test
+        run: nix develop .#rust-${{ matrix.rust-toolchain }} --command cargo test
 
   cargo-fmt:
     runs-on: ubuntu-latest
@@ -42,7 +42,7 @@ jobs:
         uses: cachix/install-nix-action@v17
 
       - name: Run cargo fmt
-        run: nix develop .#${{ matrix.rust-toolchain }} --command cargo fmt
+        run: nix develop .#rust-${{ matrix.rust-toolchain }} --command cargo fmt
 
   cargo-clippy:
     runs-on: ubuntu-latest
@@ -62,7 +62,7 @@ jobs:
         run: rm --recursive --force --verbose ~/.cargo/bin
 
       - name: Run cargo clippy
-        run: nix develop .#${{ matrix.rust-toolchain }} --command cargo clippy -- --deny warnings
+        run: nix develop .#rust-${{ matrix.rust-toolchain }} --command cargo clippy -- --deny warnings
 
   nixpkgs-fmt:
     runs-on: ubuntu-latest
@@ -74,4 +74,4 @@ jobs:
         uses: cachix/install-nix-action@v17
 
       - name: Run nixpkgs-fmt
-        run: nix develop --command nixpkgs-fmt --check .
+        run: nix develop .#nix --command nixpkgs-fmt --check .

experiments/README.md

@@ -13,6 +13,7 @@ In rough chronological order:
 5. [rust-prototype-v2](./rust-prototype-v2) (@brendanzab)
 6. [makam-spec](./makam-spec) (@brendanzab)
 7. [rust-prototype-v3](./rust-prototype-v3) (@brendanzab)
+8. [idris](./idris) (@brendanzab)
 
 The following repositories also provided us with valuable experience along the way:
 

experiments/idris/.gitignore

@@ -0,0 +1 @@
+build

experiments/idris/README.md

@@ -0,0 +1,27 @@
+# Core language experiments in Idris 2
+
+Some sketches of Fathom’s core language using Idris as a logical framework.
+
+> **Note:**
+>
+> Idris 2 does not yet support cumulatively or full totality checking, so the
+> definitions here may depend on inconsistency. We also don’t aim to prove any
+> properties of these definitions, this is more intended for experimentation.
+
+## Development setup
+
+Depends on the following:
+
+- [Idris 2](https://github.com/idris-lang/Idris2/blob/main/INSTALL.md)
+- [rlwrap](https://github.com/hanslub42/rlwrap) (optional - as a workaround for
+  [idris-lang/Idris2#54](https://github.com/idris-lang/Idris2/issues/54))
+
+If you use NixPkgs the above is installed as part of the default development
+shell in the [flake.nix](../../flake.nix) provided.
+
+## Usage
+
+```command
+$ rlwrap idris2 --repl experiments/idris/fathom.ipkg
+Main> :load "src/Playground.idr"
+```

experiments/idris/fathom.ipkg

@@ -0,0 +1,62 @@
+package fathom
+-- version =
+-- authors =
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- packages to add to search path
+depends = contrib
+
+-- modules to install
+modules = Fathom
+
+        , Fathom.Base
+        , Fathom.Data.Bit
+        , Fathom.Data.Iso
+        , Fathom.Data.Sing
+        , Fathom.Data.Word
+        , Fathom.Format.IndexedInductive
+        , Fathom.Format.IndexedInductiveCustom
+        , Fathom.Format.InductiveRecursive
+        , Fathom.Format.InductiveRecursiveCustom
+        , Fathom.Format.Record
+
+        , Playground
+        , Playground.Extraction
+        , Playground.HeterogeneousSequences
+        , Playground.OpenType.IndexedInductive
+        , Playground.OpenType.InductiveRecursive
+        , Playground.OpenType.Record
+
+-- main file (i.e. file to load at REPL)
+-- main =
+
+-- name of executable
+-- executable =
+-- opts =
+sourcedir = "src"
+builddir = "build"
+outputdir = "build/exec"
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =

experiments/idris/src/Fathom.idr

@@ -0,0 +1,7 @@
+||| A sketch of core Fathom in Idris 2
+
+import public Fathom.Base
+import public Fathom.Format.IndexedInductive
+import public Fathom.Format.InductiveRecursive
+import public Fathom.Format.InductiveRecursiveCustom
+import public Fathom.Format.Record