Add some sketches of Fathom’s core in Idris 2

Author: brendanzab

.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,8 @@
+# Core language experiments in Idris 2
+
+Some sketches of Fathom’s core language using Idris as a logical framework.
+
+```command
+$ idris2 --repl experiments/idris/fathom.ipkg
+Main> :load "src/Playground.idr"
+```

experiments/idris/fathom.ipkg

@@ -0,0 +1,48 @@
+package fathom
+-- version =
+-- authors =
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- packages to add to search path
+-- depends =
+
+-- modules to install
+modules = Fathom
+        , Fathom.Base
+        , Fathom.Closed.InductiveRecursive
+        , Fathom.Closed.IndexedInductive
+        , Fathom.Open.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 @@
+||| A sketch of core Fathom in Idris 2

experiments/idris/src/Fathom/Base.idr

@@ -0,0 +1,107 @@
+module Fathom.Base
+
+
+import Data.Colist
+import Data.List
+
+
+------------------
+-- USEFUL TYPES --
+------------------
+
+
+||| A value that is refined by a proposition.
+|||
+||| This is a bit like `(x : A ** B)`, but with the second element erased.
+public export
+record Refine (0 A : Type) (0 P : A -> Type) where
+  constructor MkRefine
+  ||| The wrapped value
+  value : A
+  ||| The proof of the proposition
+  0 prf : P value
+
+||| Refine a value with a proposition
+public export
+refine : {0 A : Type} -> {0 P : A -> Type} -> (value : A) -> {auto 0 prf : P value} -> Refine A P
+refine value {prf} = MkRefine { value, prf }
+
+
+||| Singleton types
+|||
+||| Inspired by [this type](https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html#the-inspect-idiom)
+||| from the Agda docs.
+public export
+data Sing : {0 A : Type} -> (x : A) -> Type where
+  MkSing : {0 A : Type} -> {0 x : A} -> (y : A) -> {auto prf : x = y} -> Sing x
+
+||| Convert a singleton back to its underlying value
+public export
+value : {0 Val : Type} -> {0 x : Val} -> Sing x -> Val
+value (MkSing y) = y
+
+
+---------------------------
+-- ENCODER/DECODER PAIRS --
+---------------------------
+
+-- Inspiration taken from Narcissus:
+--
+-- * [Narcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formats](https://dl.acm.org/doi/10.1145/3341686)
+--   by Delaware et. al.
+-- * [`Narcissus/Common/Specs.v`](https://github.com/mit-plv/fiat/blob/master/src/Narcissus/Common/Specs.v)
+--
+-- TODO: Add support for [Narcissus-style stores](https://github.com/mit-plv/fiat/tree/master/src/Narcissus/Stores)
+
+parameters (Source : Type, Target : Type)
+
+  ||| Decoders consume a _target value_ and produce either:
+  |||
+  ||| - a _source value_ and _remaining target value_
+  ||| - or nothing if in error occurred
+  |||
+  ||| @ Source  The type of source values (usually an in-memory data structure)
+  ||| @ Target  The type of target values (usually a byte-stream)
+  public export
+  Decode : Type
+  Decode = Target -> Maybe (Source, Target)
+
+  ||| Encoders take a _source value_ and _remaining target value_ and produce either:
+  |||
+  ||| - an _updated target value_
+  ||| - or nothing if in error occurred
+  |||
+  ||| @ Source  The type of source values (usually an in-memory data structure)
+  ||| @ Target  The type of target values (usually a byte-stream)
+  public export
+  Encode : Type
+  Encode = Source -> Target -> Maybe Target
+
+
+----------------------
+-- ENCODING TARGETS --
+----------------------
+
+
+||| A possibly infinite stream of bits
+public export
+BitStream : Type
+BitStream = Colist Bool
+
+
+||| A possibly infinite stream of bytes
+public export
+ByteStream : Type
+ByteStream = Colist Bits8
+
+
+||| A finite bit buffer
+public export
+BitBuffer : Type
+BitBuffer = List Bool
+
+
+||| A finite byte buffer
+public export
+ByteBuffer : Type
+ByteBuffer = List Bits8

experiments/idris/src/Fathom/Closed/IndexedInductive.idr

@@ -0,0 +1,82 @@
+||| A closed universe of format descriptions as an inductive type, where the
+||| in-memory representation is tracked as an index on the type.
+
+module Fathom.Closed.IndexedInductive
+
+
+import Data.Colist
+import Data.Vect
+
+import Fathom.Base
+
+
+-------------------------
+-- FORMAT DESCRIPTIONS --
+-------------------------
+
+
+||| Universe of format descriptions indexed by their machine representations
+public export
+data FormatOf : (0 Rep : Type) -> Type where
+  End : FormatOf Unit
+  Fail : FormatOf Void
+  Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
+  Skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
+  Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
+  Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
+
+
+
+---------------------------
+-- ENCODER/DECODER PAIRS --
+---------------------------
+
+export
+decode : {0 Rep : Type} -> (f : FormatOf Rep) -> Decode Rep (Colist a)
+decode End [] = Just ((), [])
+decode End (_::_) = Nothing
+decode Fail _ = Nothing
+decode (Pure x) buffer =
+  Just (MkSing x, buffer)
+decode (Skip f _) buffer = do
+  (x, buffer') <- decode f buffer
+  Just ((), buffer')
+decode (Repeat 0 f) buffer =
+  Just ([], buffer)
+decode (Repeat (S len) f) buffer = do
+  (x, buffer') <- decode f buffer
+  (xs, buffer'') <- decode (Repeat len f) buffer'
+  Just (x :: xs, buffer'')
+decode (Bind f1 f2) buffer = do
+  (x, buffer') <- decode f1 buffer
+  (y, buffer'') <- decode (f2 x) buffer'
+  Just ((x ** y), buffer'')
+
+
+export
+encode : {0 Rep : Type} -> (f : FormatOf Rep) -> Encode Rep (Colist a)
+encode End () _ = Just []
+encode (Pure x) (MkSing _) buffer = Just buffer
+encode (Skip f def) () buffer = do
+  encode f def buffer
+encode (Repeat Z f) [] buffer = Just buffer
+encode (Repeat (S len) f) (x :: xs) buffer = do
+  buffer' <- encode (Repeat len f) xs buffer
+  encode f x buffer'
+encode (Bind f1 f2) (x ** y) buffer = do
+  buffer' <- encode (f2 x) y buffer
+  encode f1 x buffer'
+
+
+-----------------
+-- EXPERIMENTS --
+-----------------
+
+
+either : (cond : Bool) -> FormatOf a -> FormatOf b -> FormatOf (if cond then a else b)
+either True f1 _ = f1
+either False _ f2 = f2
+
+orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
+orPure True f _ = f
+orPure False _ def = Pure def