From 5bc6398977e03adb7b861fceaf7c4bf4b06160ca Mon Sep 17 00:00:00 2001 From: brendanzab Date: Wed, 24 Aug 2022 15:49:57 +1000 Subject: [PATCH] =?UTF-8?q?Add=20some=20sketches=20of=20Fathom=E2=80=99s?= =?UTF-8?q?=20core=20in=20Idris=202?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/ci.yml | 12 +- experiments/README.md | 1 + experiments/idris/.gitignore | 1 + experiments/idris/README.md | 8 + experiments/idris/fathom.ipkg | 48 +++++ experiments/idris/src/Fathom.idr | 1 + experiments/idris/src/Fathom/Base.idr | 107 +++++++++++ .../src/Fathom/Closed/IndexedInductive.idr | 82 ++++++++ .../src/Fathom/Closed/InductiveRecursive.idr | 179 ++++++++++++++++++ experiments/idris/src/Fathom/Open/Record.idr | 120 ++++++++++++ experiments/idris/src/Playground.idr | 119 ++++++++++++ flake.nix | 69 +++++-- 12 files changed, 724 insertions(+), 23 deletions(-) create mode 100644 experiments/idris/.gitignore create mode 100644 experiments/idris/README.md create mode 100644 experiments/idris/fathom.ipkg create mode 100644 experiments/idris/src/Fathom.idr create mode 100644 experiments/idris/src/Fathom/Base.idr create mode 100644 experiments/idris/src/Fathom/Closed/IndexedInductive.idr create mode 100644 experiments/idris/src/Fathom/Closed/InductiveRecursive.idr create mode 100644 experiments/idris/src/Fathom/Open/Record.idr create mode 100644 experiments/idris/src/Playground.idr diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2c4e01bc2..a2149c21c 100644 --- a/.github/workflows/ci.yml +++ b/.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 . diff --git a/experiments/README.md b/experiments/README.md index c15ca3101..75058e3d0 100644 --- a/experiments/README.md +++ b/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: diff --git a/experiments/idris/.gitignore b/experiments/idris/.gitignore new file mode 100644 index 000000000..378eac25d --- /dev/null +++ b/experiments/idris/.gitignore @@ -0,0 +1 @@ +build diff --git a/experiments/idris/README.md b/experiments/idris/README.md new file mode 100644 index 000000000..01f35f0cf --- /dev/null +++ b/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" +``` diff --git a/experiments/idris/fathom.ipkg b/experiments/idris/fathom.ipkg new file mode 100644 index 000000000..250c95184 --- /dev/null +++ b/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 = diff --git a/experiments/idris/src/Fathom.idr b/experiments/idris/src/Fathom.idr new file mode 100644 index 000000000..00781a8d2 --- /dev/null +++ b/experiments/idris/src/Fathom.idr @@ -0,0 +1 @@ +||| A sketch of core Fathom in Idris 2 diff --git a/experiments/idris/src/Fathom/Base.idr b/experiments/idris/src/Fathom/Base.idr new file mode 100644 index 000000000..ee5001008 --- /dev/null +++ b/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 diff --git a/experiments/idris/src/Fathom/Closed/IndexedInductive.idr b/experiments/idris/src/Fathom/Closed/IndexedInductive.idr new file mode 100644 index 000000000..4a0e01e15 --- /dev/null +++ b/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 diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr new file mode 100644 index 000000000..def23d60c --- /dev/null +++ b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr @@ -0,0 +1,179 @@ +||| A closed universe of format descriptions, using induction recursion between +||| the descriptions and their in-memory representation. This closely matches +||| the current implementation of format descriptions in Fathom. +||| +||| [Induction recusion](https://en.wikipedia.org/wiki/Induction-recursion) is +||| where an inductive datatype is defined simultaneously with a function that +||| operates on that type (see the @Format and @Rep definitions below). +||| +||| The universe is ‘closed’ in the sense tha new format descriptions cannot be +||| added to the type theory, although they can be composed out of other formats) +||| +||| This is similar to the approach used when defining type theories with +||| Tarski-style universes. In-fact inductive-recusrive datatypes as a language +||| feature were apparently originally motivated by this use case (see: [“A +||| General Formulation of Simultaneous Inductive-Recursive Definitions in Type +||| Theory”](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.4575) by +||| Dybjer). +||| +||| Inspiration for this approach is taken from [“The Power of Pi”](https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf) +||| by Oury and Swierstra. + +module Fathom.Closed.InductiveRecursive + + +import Data.Colist +import Data.Vect + +import Fathom.Base + +-- import Fathom.Open.Record + + +------------------------- +-- FORMAT DESCRIPTIONS -- +------------------------- + + +mutual + ||| Universe of format descriptions + public export + data Format : Type where + End : Format + Fail : Format + Pure : {0 A : Type} -> A -> Format + Skip : (f : Format) -> (def : Rep f) -> Format + Repeat : Nat -> Format -> Format + Bind : (f : Format) -> (Rep f -> Format) -> Format + + -- Questionable format descriptions + -- OrPure : (cond : Bool) -> (f : Format) -> (def : Rep f) -> Format + -- OfSing : (f : Format) -> Sing (Rep f) -> Format + -- OfEq : (f : Format) -> (r : Type) -> {auto 0 prf : Rep f = r} -> Format + + -- Broken stuff + -- Let : (f : Format) -> (Rep f -> Format) -> Format + -- Custom : (f : Record.Format) -> Format + + + ||| In-memory representation of format descriptions + public export + Rep : Format -> Type + Rep End = Unit + Rep Fail = Void + Rep (Skip _ _) = Unit + Rep (Repeat len f) = Vect len (Rep f) + Rep (Pure x) = Sing x + Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x)) + + -- Questionable format descriptions + -- Rep (OrPure _ f _) = Rep f + -- Rep (OfSing f r) = value r + -- Rep (OfEq f r) = r + + -- Broken stuff + -- Rep (Let f1 f2) = Rep (f2 ?halp) + -- Rep (Custom f) = f.Rep + + +--------------------------- +-- ENCODER/DECODER PAIRS -- +--------------------------- + + +export +decode : (f : Format) -> Decode (Rep f) (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'') + +-- Questionable format descriptions +-- decode (OrPure True f _) buffer = decode f buffer +-- decode (OrPure False _ def) buffer = Just (def, buffer) +-- decode (OfSing f (MkSing r {prf})) buffer = do +-- (x, buffer') <- decode f buffer +-- Just (rewrite sym prf in x, buffer') +-- decode (OfEq f _ {prf}) buffer = do +-- (x, buffer') <- decode f buffer +-- Just (rewrite sym prf in x, buffer') + +-- Broken stuff + + +export +encode : (f : Format) -> Encode (Rep f) (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' +-- Questionable format descriptions +-- encode (OrPure True f _) x buffer = encode f x buffer +-- encode (OrPure False _ def) x buffer = Just buffer +-- encode (OfSing f r) x buffer = do +-- buffer' <- encode f ?todo_x buffer +-- ?todo_encode +-- encode (OfEq f _ {prf}) x buffer = do +-- encode f (rewrite prf in x) buffer + + +----------------- +-- EXPERIMENTS -- +----------------- + + +||| A format description refined with a fixed representation +public export +FormatOf : (0 Rep : Type) -> Type +FormatOf rep = Refine Format (\f => Rep f = rep) + + +toFormatOf : (f : Format) -> FormatOf (Rep f) +toFormatOf f = refine f + + +export +either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2) +either True f1 _ = refine f1 +either False _ f2 = refine f2 + + +export +orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def) +orPure True f _ = f +orPure False _ def = refine (Pure def) + + +export +orPure' : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def) +orPure' True f _ = f +orPure' False _ def = refine (Pure def) + + +foo : (cond : Bool) -> (f : Format) -> Rep f -> Format +foo cond f def = case orPure cond (toFormatOf f) def of + MkRefine f' prf => + Bind f' (\x => case cond of + True => ?todo1 + False => ?todo2) diff --git a/experiments/idris/src/Fathom/Open/Record.idr b/experiments/idris/src/Fathom/Open/Record.idr new file mode 100644 index 000000000..3bcdada6f --- /dev/null +++ b/experiments/idris/src/Fathom/Open/Record.idr @@ -0,0 +1,120 @@ +||| Open format universe +||| +||| This module defines an open universe of binary format descriptions using +||| records to define an inderface. By defining formats in this way, the +||| universe of formats is open to extension. +||| +||| I’m not sure, but this reminds me a little of the ‘coinductive universes’ +||| that [some type theorists were proposing for HoTT](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-12.pdf#page=79), +||| but I may be mistaken. + +module Fathom.Open.Record + + +import Data.Colist +import Data.Vect + +import Fathom.Base + + +public export +record Format where + constructor MkFormat + Rep : Type + decode : Decode Rep BitStream + encode : Encode Rep BitStream + + +public export +end : Format +end = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Unit + + decode : Decode Rep BitStream + decode [] = Just ((), []) + decode (_::_) = Nothing + + encode : Encode Rep BitStream + encode () _ = Just [] + +public export +fail : Format +fail = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Void + + decode : Decode Rep BitStream + decode _ = Nothing + + encode : Encode Rep BitStream + encode x = void x + +public export +pure : {0 A : Type} -> A -> Format +pure x = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Sing x + + decode : Decode Rep BitStream + decode buffer = Just (MkSing x, buffer) + + encode : Encode Rep BitStream + encode (MkSing _) buffer = Just buffer + +public export +skip : (f : Format) -> (def : f.Rep) -> Format +skip f def = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = () + + decode : Decode Rep BitStream + decode buffer = do + (x, buffer') <- f.decode buffer + Just ((), buffer') + + encode : Encode Rep BitStream + encode () buffer = do + f.encode def buffer + + +public export +repeat : Nat -> Format -> Format +repeat len f = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Vect len f.Rep + + decode : Decode Rep BitStream + decode = go len where + go : (len : Nat) -> Decode (Vect len f.Rep) BitStream + go 0 buffer = Just ([], buffer) + go (S len) buffer = do + (x, buffer') <- f.decode buffer + (xs, buffer'') <- go len buffer' + Just (x :: xs, buffer'') + + encode : Encode Rep BitStream + encode = go len where + go : (len : Nat) -> Encode (Vect len f.Rep) BitStream + go 0 [] buffer = Just buffer + go (S len) (x :: xs) buffer = do + buffer' <- go len xs buffer + f.encode x buffer' + + +public export +bind : (f : Format) -> (f.Rep -> Format) -> Format +bind f1 f2 = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = (x : f1.Rep ** (f2 x).Rep) + + decode : Decode Rep BitStream + decode buffer = do + (x, buffer') <- f1.decode buffer + (y, buffer'') <- (f2 x).decode buffer' + Just ((x ** y), buffer'') + + encode : Encode Rep BitStream + encode (x ** y) buffer = do + buffer' <- (f2 x).encode y buffer + f1.encode x buffer' diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr new file mode 100644 index 000000000..f60b1274c --- /dev/null +++ b/experiments/idris/src/Playground.idr @@ -0,0 +1,119 @@ +module Playground + + +import Data.Colist +import Data.Vect + +import Fathom.Base +import Fathom.Closed.InductiveRecursive as IndRec +import Fathom.Closed.IndexedInductive as Indexed +import Fathom.Open.Record as Record + + +-- Experiment with converting between the different styles of format universes + + +||| Convert an inductive-recusive format universe into a record format +public export +format : IndRec.Format -> Record.Format +format f = Record.MkFormat + { Rep = IndRec.Rep f + , decode = IndRec.decode f + , encode = IndRec.encode f + } + + +||| Conver an indexed-inductive format universe into a record format +public export +formatOf : {Rep : Type} -> Indexed.FormatOf Rep -> Record.Format +formatOf f = Record.MkFormat + { Rep = Rep + , decode = Indexed.decode f + , encode = Indexed.encode f + } + + +-- public export +-- format' : IndRec.Format -> Record.Format +-- format' f = MkFormat { Rep, decode, encode } where +-- Rep : Type +-- Rep = IndRec.Rep f + +-- decode : Decode (IndRec.Rep f) BitStream +-- decode = case f of +-- End => end.decode +-- Fail => fail.decode +-- Pure x => (pure x).decode +-- Skip f def => (skip (format' f) def).decode +-- Repeat len f => (repeat len (format' f)).decode +-- Bind f1 f2 => (bind (format' f1) (\x => format' (f2 x))).decode +-- OfSing f r => (format' f).decode +-- OfEq f r => (format' f).decode + +-- encode : Encode Rep BitStream +-- encode = case f of +-- End => end.encode +-- Fail => fail.encode +-- Pure x => (pure x).encode +-- Skip f def => (skip (format' f) def).encode +-- Repeat len f => (repeat len (format' f)).encode +-- Bind f1 f2 => (bind (format' f1) (\x => format' (f2 x))).encode +-- OfSing f r => (format' f).encode +-- OfEq f r => (format' f).encode + + +||| Convert an inductive-recursive format description to an indexed format +indRecToIndexed : (f : IndRec.Format) -> Indexed.FormatOf (Rep f) +indRecToIndexed End = Indexed.End +indRecToIndexed Fail = Indexed.Fail +indRecToIndexed (Pure x) = Indexed.Pure x +indRecToIndexed (Skip f def) = Indexed.Skip (indRecToIndexed f) def +indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f) +indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToIndexed (g x)) +-- indRecToIndexed (OfSing f (MkSing _ {prf})) = rewrite sym prf in indRecToIndexed f +-- indRecToIndexed (OfEq f _ {prf}) = rewrite sym prf in indRecToIndexed f + + +-- ||| Convert an indexed format description to an inductive-recursive format +-- indexedToIndRec : {0 Rep : Type} -> (f : Indexed.FormatOf Rep) -> IndRec.FormatOf Rep +-- indexedToIndRec End = MkRefine { value = IndRec.End, prf = Refl } +-- indexedToIndRec Fail = MkRefine { value = IndRec.Fail, prf = Refl } +-- indexedToIndRec (Pure x) = MkRefine { value = IndRec.Pure x, prf = Refl } +-- indexedToIndRec (Skip {a} f def) = +-- let +-- MkRefine f' prf = indexedToIndRec f +-- symPrf = sym prf +-- def' = rewrite prf in def +-- in +-- MkRefine { value = IndRec.Skip f' ?todoDef, prf = ?todoSkip } +-- indexedToIndRec (Repeat len f) = MkRefine { value = IndRec.Repeat _ _, prf = ?todoRepeat } +-- indexedToIndRec (Bind f g) = MkRefine { value = IndRec.Bind _ _, prf = ?todoBind } + +||| Convert an indexed format description to an inductive-recursive format +indexedToIndRec : {0 Rep : Type} -> (f : Indexed.FormatOf Rep) -> IndRec.Format +indexedToIndRec End = IndRec.End +indexedToIndRec Fail = IndRec.Fail +indexedToIndRec (Pure x) = IndRec.Pure x +indexedToIndRec (Skip f def) = + IndRec.Skip (indexedToIndRec f) ?todo_def +-- ^^^^^^^^^ +-- Error: While processing right hand side of indexedToIndRec. Can't solve constraint between: a and Rep (indexedToIndRec f). +-- +-- def : a +-- f : FormatOf a +-- 0 Rep : Type +-- ------------------------------ +-- todo_def : Rep (indexedToIndRec f) +-- +indexedToIndRec (Repeat len f) = IndRec.Repeat len (indexedToIndRec f) +indexedToIndRec (Bind f1 f2) = IndRec.Bind (indexedToIndRec f1) (\x => indexedToIndRec ?todo_f2) +-- ^^^^^^^^ +-- Error: While processing right hand side of indexedToIndRec. Can't solve constraint +-- between: Rep (indexedToIndRec f1) and a (implicitly bound at Fathom.Test:86:1--86:95). +-- +-- f2 : (x : a) -> FormatOf (b x) +-- f1 : FormatOf a +-- 0 Rep : Type +-- x : Rep (indexedToIndRec f1) +-- ------------------------------ +-- todo_f2 : FormatOf ?Rep diff --git a/flake.nix b/flake.nix index 4c996f3d6..a5de25824 100644 --- a/flake.nix +++ b/flake.nix @@ -74,19 +74,53 @@ # If you want to live on the bleeding edge, you could also try using the # nightly shell with the following `.envrc` file: # - # use flake .#nightly + # use flake .#rust-nightly # # If you choose to use Direnv, note that `.envrc` should be added to # your local git excludes, or added to to your global gitignore. devShells = { - # Use the stable toolchain by default for development, to get the - # latest diagnostics and compiler improvements. + # Default development shell # # $ nix develop # $ nix develop --command cargo check # - default = self.devShells.${system}.stable; + default = + let + systemShells = self.devShells.${system}; + in + pkgs.mkShell { + inputsFrom = [ + # Use the stable toolchain by default for development to get the + # latest diagnostics and compiler improvements. + systemShells.rust-stable + systemShells.idris2 + systemShells.nix + ]; + }; + + # Idris 2 development shell for `./experiments/idris` + idris2 = pkgs.mkShell { + name = "idris2"; + packages = [ + # Idris 2 is currently broken on `aarch64-darwin` without + # resorting to some installation schenanigans with Racket: + # https://github.com/idris-lang/Idris2/issues/2404. For now it can + # just be emulated using Rosetta. + (if system == "aarch64-darwin" then + nixpkgs.legacyPackages.x86_64-darwin.idris2 + else + pkgs.idris2) + ]; + }; + + # Nix development shell + nix = pkgs.mkShell { + name = "nix"; + packages = [ pkgs.nixpkgs-fmt ]; + }; } // ( + # Rust development shells + # # Map over the `rustToolchains` defined above, creating a shell # environment for each. # @@ -96,28 +130,29 @@ # # For example, to run the tests using the `minimum` Rust toolchain: # - # $ nix develop .#minimum --command cargo test + # $ nix develop .#rust-stable --command cargo test # - lib.mapAttrs + lib.mapAttrs' (name: rustToolchain: let rustWithExtensions = rustToolchain.override { extensions = [ "rust-src" "rustfmt" "clippy" ]; }; in - pkgs.mkShell { - name = "${name}-shell"; + { + name = "rust-${name}"; + value = pkgs.mkShell { + name = "${name}-shell"; - packages = [ - rustWithExtensions - pkgs.nixpkgs-fmt - ]; + packages = [ + rustWithExtensions + ]; - # Print backtraces on panics - RUST_BACKTRACE = 1; - - # Certain tools like `rust-analyzer` won't work without this - RUST_SRC_PATH = "${rustWithExtensions}/lib/rustlib/src/rust/library"; + # Print backtraces on panics + RUST_BACKTRACE = 1; + # Certain tools like `rust-analyzer` won't work without this + RUST_SRC_PATH = "${rustWithExtensions}/lib/rustlib/src/rust/library"; + }; }) rustToolchains );