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..1751141e9 --- /dev/null +++ b/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" +``` diff --git a/experiments/idris/fathom.ipkg b/experiments/idris/fathom.ipkg new file mode 100644 index 000000000..dddbe420c --- /dev/null +++ b/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 = diff --git a/experiments/idris/src/Fathom.idr b/experiments/idris/src/Fathom.idr new file mode 100644 index 000000000..5c4e3d434 --- /dev/null +++ b/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 diff --git a/experiments/idris/src/Fathom/Base.idr b/experiments/idris/src/Fathom/Base.idr new file mode 100644 index 000000000..298246392 --- /dev/null +++ b/experiments/idris/src/Fathom/Base.idr @@ -0,0 +1,256 @@ +module Fathom.Base + + +import Data.Bits +import Data.Colist +import Data.List +import Data.Vect + + +||| Return the type of an expression, without consuming it +public export +typeOf : {1 A : Type} -> (0 x : A) -> Type +typeOf _ = A + + +--------------------------- +-- 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, Target : Type) + + ||| Decoders consume a _target value_ and produce either: + ||| + ||| - a _source 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 + + + ||| Encoders take a _source value_ and produce either: + ||| + ||| - a _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 -> Maybe Target + + +parameters (Source, Target : Type) + + ||| Decode a portion of a _target value_, leaving some remaining for + ||| subsequent decoding. + ||| + ||| @ Source The type of source values (usually an in-memory data structure) + ||| @ Target The type of target values (usually a byte-stream) + public export + DecodePart : Type + DecodePart = Decode (Source, Target) Target + + + ||| Consumes a _source value_ and the remaining _target value_, returning + ||| a fully encoded target value. + ||| + ||| @ Source The type of source values (usually an in-memory data structure) + ||| @ Target The type of target values (usually a byte-stream) + public export + EncodePart : Type + EncodePart = Encode (Source, Target) Target + + +parameters {0 Source, Target : Type} + + public export + toDecodeFull : (Monoid Target, Eq Target) => DecodePart Source Target -> Decode Source Target + toDecodeFull decode target = Prelude.do + (source, target') <- decode target + if target == neutral then Just source else Nothing + + + public export + toEncodeFull : Monoid Target => EncodePart Source Target -> Encode Source Target + toEncodeFull encode source = encode (source, neutral) + + + public export + toEncodePart : Monoid Target => Encode Source Target -> EncodePart Source Target + toEncodePart encode (source, target) = [| encode source <+> Just target |] + + +namespace DecodePart + + -- TODO: Should probably implement functor, applicative, or monad here. or use + -- the reader, writer or state monad transformers + + public export + map : {0 S1, S2, T : Type} -> (S1 -> S2) -> DecodePart S1 T -> DecodePart S2 T + map f decode target = + Prelude.map (\(source, target') => (f source, target)) (decode target) + + + public export + pure : {0 S, T : Type} -> S -> DecodePart S T + pure source target = Just (source, target) + + + public export + (<*>) : {0 S1, S2, T : Type} -> DecodePart (S1 -> S2) T -> DecodePart S1 T -> DecodePart S2 T + (<*>) decodeFun decode target = do + (fun, target1) <- decodeFun target + (source, target2) <- decode target1 + Just (fun source, target2) + + + public export + ignore : {0 S, T : Type} -> DecodePart S T -> DecodePart () T + ignore = map (const ()) + + + public export + bind : {0 S1, S2, T : Type} -> DecodePart S1 T -> (S1 -> DecodePart S2 T) -> DecodePart S2 T + bind decode1 decode2 target = do + (source1, target') <- decode1 target + decode2 source1 target' + + + public export + (>>=) : {0 S1, S2, T : Type} -> DecodePart S1 T -> (S1 -> DecodePart S2 T) -> DecodePart S2 T + (>>=) = bind + + + public export + (<|>) : {0 S, T : Type} -> DecodePart S T -> Lazy (DecodePart S T) -> DecodePart S T + (<|>) decode1 decode2 target = + Prelude.(<|>) (decode1 target) (decode2 target) + + +---------------------- +-- ENCODING TARGETS -- +---------------------- + + +||| A potentially infinite stream of bits +public export +BitStream : Type +BitStream = Colist Bool + +%name BitStream bits + + +||| A potentially infinite stream of bytes +public export +ByteStream : Type +ByteStream = Colist Bits8 + +%name ByteStream bytes + + +||| A finite bit buffer +public export +BitBuffer : Type +BitBuffer = List Bool + +%name BitBuffer bits + + +||| A finite byte buffer +public export +ByteBuffer : Type +ByteBuffer = List Bits8 + +%name ByteBuffer bytes + + +||| An array of bits of a known size +public export +BitArray : Nat -> Type +BitArray len = Vect len Bool + +%name BitArray bits + + +||| An array of bytes of a known size +public export +ByteArray : Nat -> Type +ByteArray len = Vect len Bits8 + +%name ByteArray bytes + + +||| The byte order of some encoded data, usually a number. +public export +data ByteOrder : Type where + LE : ByteOrder + BE : ByteOrder + + +namespace ByteStream + + export + decodeU8 : DecodePart Bits8 ByteStream + decodeU8 [] = Nothing + decodeU8 (x :: bytes) = Just (x, bytes) + + + export + encodeU8 : Encode Bits8 ByteStream + encodeU8 x = Just [x] + + + export + decodeU16 : ByteOrder -> DecodePart Bits16 ByteStream + decodeU16 LE = DecodePart.do + b0 <- map (cast {to = Bits16}) decodeU8 + b1 <- map (cast {to = Bits16}) decodeU8 + pure (b0 .|. b1 `shiftL` fromNat 8) + decodeU16 BE = DecodePart.do + b0 <- map (cast {to = Bits16}) decodeU8 + b1 <- map (cast {to = Bits16}) decodeU8 + pure (b0 `shiftL` fromNat 8 .|. b1) + + + export + encodeU16 : ByteOrder -> Encode Bits16 ByteStream + encodeU16 LE x = Just [cast x, cast (x `shiftR` fromNat 8)] + encodeU16 BE x = Just [cast (x `shiftR` fromNat 8), cast x] + + + export + decodeU32 : ByteOrder -> DecodePart Bits32 ByteStream + decodeU32 LE = DecodePart.do + b0 <- map (cast {to = Bits32}) decodeU8 + b1 <- map (cast {to = Bits32}) decodeU8 + b2 <- map (cast {to = Bits32}) decodeU8 + b3 <- map (cast {to = Bits32}) decodeU8 + pure (b0 .|. b1 `shiftL` fromNat 8 .|. b2 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 24) + decodeU32 BE = DecodePart.do + b0 <- map (cast {to = Bits32}) decodeU8 + b1 <- map (cast {to = Bits32}) decodeU8 + b2 <- map (cast {to = Bits32}) decodeU8 + b3 <- map (cast {to = Bits32}) decodeU8 + pure (b0 `shiftL` fromNat 24 .|. b1 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 8 .|. b3) + + + export + encodeU32 : ByteOrder -> Encode Bits32 ByteStream + encodeU32 LE x = Just [cast x, cast (x `shiftR` fromNat 8), cast (x `shiftR` fromNat 16), cast (x `shiftR` fromNat 24)] + encodeU32 BE x = Just [cast (x `shiftR` fromNat 24), cast (x `shiftR` fromNat 16), cast (x `shiftR` fromNat 8), cast x] + + + -- decodeU : Bits a => ByteOrder -> DecodePart a ByteStream + -- encodeU : Bits a => ByteOrder -> Encode a ByteStream diff --git a/experiments/idris/src/Fathom/Data/Bit.idr b/experiments/idris/src/Fathom/Data/Bit.idr new file mode 100644 index 000000000..ad7aab6ca --- /dev/null +++ b/experiments/idris/src/Fathom/Data/Bit.idr @@ -0,0 +1,71 @@ +||| Binary digits + +module Fathom.Data.Bit + + +||| A binary digit +public export +data Bit : Type where + B0 : Bit + B1 : Bit + + +public export +Cast Bit Bool where + cast B0 = True + cast B1 = False + +public export +Cast Bit Nat where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Int where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Integer where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Bits8 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Bits16 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Bits32 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Bits64 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Int8 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Int16 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Int32 where + cast B0 = 0 + cast B1 = 1 + +public export +Cast Bit Int64 where + cast B0 = 0 + cast B1 = 1 diff --git a/experiments/idris/src/Fathom/Data/Iso.idr b/experiments/idris/src/Fathom/Data/Iso.idr new file mode 100644 index 000000000..fd68090e5 --- /dev/null +++ b/experiments/idris/src/Fathom/Data/Iso.idr @@ -0,0 +1,50 @@ +||| Isomorphisms between types + +module Fathom.Data.Iso + + +||| A datatype that forms a proof that two types are isomorphic to each other, +||| ie. can be converted to and from each other while preserving information. +public export +record Iso (0 A : Type) (0 B : Type) where + constructor MkIso + to : A -> B + from : B -> A + 0 toFrom : (y : B) -> to (from y) = y + 0 fromTo : (x : A) -> from (to x) = x + + +sym : Iso a b -> Iso b a +sym iso = MkIso + { to = iso.from + , from = iso.to + , toFrom = iso.fromTo + , fromTo = iso.toFrom + } + + +isoSym : Iso (Iso a b) (Iso b a) +isoSym = MkIso + { to = sym + , from = sym + , toFrom = \(MkIso _ _ _ _) => Refl + , fromTo = \(MkIso _ _ _ _) => Refl + } + + +cong : (f : Type -> Type) -> Iso a b -> Iso (f a) (f b) +cong f iso = MkIso + { to = \fa => ?todo_to + , from = \fb => ?todo_from + , toFrom = ?todo_toFrom + , fromTo = ?todo_fromTo + } + + +trans : Iso a b -> Iso b c -> Iso a c +trans isoAB isoBC = MkIso + { to = isoBC.to . isoAB.to + , from = isoAB.from . isoBC.from + , toFrom = \c => trans ?todo_toFrom1' (isoBC.toFrom c) + , fromTo = \c => ?todo_fromTo' + } diff --git a/experiments/idris/src/Fathom/Data/Sing.idr b/experiments/idris/src/Fathom/Data/Sing.idr new file mode 100644 index 000000000..f364e42af --- /dev/null +++ b/experiments/idris/src/Fathom/Data/Sing.idr @@ -0,0 +1,61 @@ +module Fathom.Data.Sing + + +||| A type constrained to a single value +||| +||| The underlying value is erased at runtime, as it can be converted back to +||| the index by reconstructing the value as required. +public export +data Sing : {0 A : Type} -> (x : A) -> Type where + MkSing : {0 A : Type} -> (0 x : A) -> Sing x + + +||| Reconstruct a singleton with a runtime value. +public export +val : {0 A : Type} -> {x : A} -> Sing x -> A +val (MkSing _) = x + + +||| Update the value contained in a singleton with a function. +export +map : {0 A, B : Type} -> {0 x : A} -> (f : A -> B) -> Sing x -> Sing (f x) +map f (MkSing y) = MkSing (f y) + + + +namespace SingEq + -- NOTE: Unsure if this representation is actually needed? + + ||| A type constrained to be a single value, with an associated equality proof. + ||| + ||| The underlying value and the proof are both erased at runtime, as they can + ||| be converted back to the index by reconstructing the value as required. + ||| + ||| Inspired by the singleton type [found in Adga’s documentation](https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html#the-inspect-idiom). + public export + record SingEq {0 A : Type} (x : A) where + constructor MkSingEq + ||| The underlying value of the singleton (erased at run-time) + 0 val : A + ||| A proof that @val is the same as the indexed value (erased at run-time) + {auto 0 prf : x = val} + + + ||| Convert a singleton back to its underlying value restoring it with a value + ||| constructed runtime + public export + val : {0 A : Type} -> {x : A} -> SingEq x -> A + val (MkSingEq _) = x + + + ||| Update the value contained in a singleton with a function. + export + map : {0 A, B : Type} -> {0 x : A} -> (f : A -> B) -> SingEq x -> SingEq (f x) + map f (MkSingEq y {prf}) = MkSingEq (f y) {prf = cong f prf} + + +withEq : {0 A : Type} -> {0 x : A} -> Sing x -> SingEq x +withEq (MkSing x) = MkSingEq x + +withoutEq : {0 A : Type} -> {0 x : A} -> SingEq x -> Sing x +withoutEq {x} (MkSingEq _) = MkSing x diff --git a/experiments/idris/src/Fathom/Data/Word.idr b/experiments/idris/src/Fathom/Data/Word.idr new file mode 100644 index 000000000..4dac845cd --- /dev/null +++ b/experiments/idris/src/Fathom/Data/Word.idr @@ -0,0 +1,26 @@ +module Fathom.Data.Word + + +import Data.Fin + +import Fathom.Data.Bit + + +||| A binary word with a specified number of bits +public export +data Word : (0 size : Nat) -> Type where + Z : Word 0 + S : Bit -> {0 n : Nat} -> Word n -> Word (S n) + + +export +Cast (Word size) Nat where + cast Z = 0 + cast (S B0 w) = cast w * 2 + cast (S B1 w) = S (cast w * 2) + +export +Cast (Word size) Bits8 where + cast Z = 0 + cast (S B0 w) = cast w * 2 + cast (S B1 w) = (cast w * 2) + 1 diff --git a/experiments/idris/src/Fathom/Format/IndexedInductive.idr b/experiments/idris/src/Fathom/Format/IndexedInductive.idr new file mode 100644 index 000000000..f20dc19ac --- /dev/null +++ b/experiments/idris/src/Fathom/Format/IndexedInductive.idr @@ -0,0 +1,227 @@ +||| 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.Format.IndexedInductive + + +import Data.Colist +import Data.DPair +import Data.HVect +import Data.Vect + +import Fathom.Base +import Fathom.Data.Iso +import Fathom.Data.Sing + + +--------------------------------- +-- INDEXED FORMAT DESCRIPTIONS -- +--------------------------------- + + +||| Universe of format descriptions indexed by their machine representations +public export +data FormatOf : Type -> Type where + End : FormatOf Unit + Fail : FormatOf Void + Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit + Choice : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (Either A B) + Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A) + Tuple : {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps) + Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B) + Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + + +namespace FormatOf + + -- Support for do notation + + public export + pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + pure = Pure + + public export + (>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + (>>=) = Bind + + + --------------------------- + -- ENCODER/DECODER PAIRS -- + --------------------------- + + + export + decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S) + decode End = + \case [] => Just ((), []) + (_::_) => Nothing + decode Fail = const Nothing + decode (Pure x) = pure (MkSing x) + decode (Ignore f _) = ignore (decode f) + decode (Choice f1 f2) = + [| Left (decode f1) |] <|> [| Right (decode f2) |] + decode (Repeat 0 f) = pure [] + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Tuple {reps = []} []) = pure [] + decode (Tuple {reps = _::_} (f :: fs)) = DecodePart.do + x <- decode f + xs <- decode (Tuple fs) + pure (x :: xs) + -- FIXME: Ambiguous elaboration for some reason?? + -- [| decode f :: decode (Tuple fs) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] + decode (Bind f1 f2) = do + x <- decode f1 + y <- decode (f2 x) + pure (x ** y) + + + export + encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S) + encode End () = pure [] + encode (Pure x) (MkSing _) = pure [] + encode (Ignore f def) () = encode f def + encode (Choice f1 f2) (Left x) = encode f1 x + encode (Choice f1 f2) (Right y) = encode f2 y + encode (Repeat Z f) [] = pure [] + encode (Repeat (S len) f) (x :: xs) = + [| encode f x <+> encode (Repeat len f) xs |] + encode (Tuple {reps = []} []) [] = pure [] + encode (Tuple {reps = _::_} (f :: fs)) (x :: xs) = + [| encode f x <+> encode (Tuple fs) xs |] + encode (Pair f1 f2) (x, y) = + [| encode f1 x <+> encode f2 y |] + encode (Bind f1 f2) (x ** y) = + [| encode f1 x <+> encode (f2 x) y |] + + +------------------------- +-- FORMAT DESCRIPTIONS -- +------------------------- + + +||| A format description of an arbitrary representation +public export +record Format where + constructor MkFormat + ||| The in-memory representation of the format description + 0 Rep : Type + ||| The underlying format description + format : FormatOf Rep + + +namespace Format + + decode : (f : Format) -> Decode (Rep f, Colist a) (Colist a) + decode f = FormatOf.decode f.format + + + encode : (f : Format) -> Encode (Rep f) (Colist a) + encode f = FormatOf.encode f.format + + +------------------------------------ +-- FORMAT DESCRIPTION CONVERSIONS -- +------------------------------------ + + +namespace Format + + public export + toFormatOf : (f : Format) -> FormatOf f.Rep + toFormatOf (MkFormat _ f) = f + + + ||| Convert a format description into an indexed format description with an + ||| equality proof that the representation is the same as the index. + public export + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A + toFormatOfEq (Element f prf) = rewrite sym prf in f.format + + +namespace FormatOf + + public export + toFormat : {0 A : Type} -> FormatOf A -> Format + toFormat f = MkFormat A f + + + ||| Convert an indexed format description to a existential format description, + ||| along with a proof that the representation is the same as the index. + public export + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) + toFormatEq f = Element (MkFormat A f) Refl + + +public export +toFormatOfIso : Iso Format (Exists FormatOf) +toFormatOfIso = MkIso + { to = \f => Evidence _ (toFormatOf f) + , from = \(Evidence _ f) => toFormat f + , toFrom = \(Evidence _ _) => Refl + , fromTo = \(MkFormat _ _) => Refl + } + + +public export +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf) +toFormatOfEqIso = MkIso + { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) + , from = \(Evidence _ f) => Evidence _ (toFormatEq f) + , toFrom = \(Evidence _ _) => Refl + , fromTo = \(Evidence _ (Element (MkFormat _ _) Refl)) => Refl + } + + +------------------------- +-- FORMAT CONSTRUCTORS -- +------------------------- + +-- Helpful constructors for building non-indexed format descriptions. +-- This also tests if we can actually meaningfully use the `Format` type. + +namespace Format + + public export + end : Format + end = MkFormat () End + + + public export + fail : Format + fail = MkFormat Void Fail + + + public export + pure : {0 A : Type} -> (x : A) -> Format + pure x = MkFormat (Sing x) (Pure x) + + + public export + skip : (f : Format) -> (def : f.Rep) -> Format + skip f def = MkFormat Unit (Ignore (toFormatOf f) def) + + + public export + repeat : (len : Nat) -> Format -> Format + repeat len f = MkFormat (Vect len f.Rep) (Repeat len (toFormatOf f)) + + + public export + pair : Format -> Format -> Format + pair f1 f2 = MkFormat (f1.Rep, f2.Rep) (Pair (toFormatOf f1) (toFormatOf f2)) + + + public export + bind : (f : Format) -> (Rep f -> Format) -> Format + bind f1 f2 = + MkFormat (x : f1.Rep ** (f2 x).Rep) + (Bind (toFormatOf f1) (\x => toFormatOf (f2 x))) + + + public export + (>>=) : (f : Format) -> (Rep f -> Format) -> Format + (>>=) = bind diff --git a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr b/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr new file mode 100644 index 000000000..72c035bb3 --- /dev/null +++ b/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr @@ -0,0 +1,287 @@ +||| 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.Format.IndexedInductiveCustom + + +import Data.Colist +import Data.DPair +import Data.HVect +import Data.Vect + +import Fathom.Base +import Fathom.Data.Iso +import Fathom.Data.Sing + + +--------------------------------- +-- INDEXED FORMAT DESCRIPTIONS -- +--------------------------------- + + +||| A custom format description. +||| +||| We’d prefer to just import `Fathom.Format.Record`, but Idris’ imports are a +||| bit temperamental and result in ambiguities when importing modules that +||| contain types of the same name as those defined in the current module. +public export +record CustomFormatOf (Rep : Type) where + constructor MkCustomFormatOf + decode : Decode (Rep, ByteStream) ByteStream + encode : Encode Rep ByteStream + + +||| Universe of format descriptions indexed by their machine representations +public export +data FormatOf : (A : Type) -> Type where + End : FormatOf Unit + Fail : FormatOf Void + Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit + Choice : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (Either A B) + Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A) + Tuple : {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps) + Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B) + Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + Custom : {0 A : Type} -> (f : CustomFormatOf A) -> FormatOf A + + +namespace FormatOf + + -- Support for do notation + + public export + pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + pure = Pure + + public export + (>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + (>>=) = Bind + + + --------------------------- + -- ENCODER/DECODER PAIRS -- + --------------------------- + + + export + decode : {0 A : Type} -> (f : FormatOf A) -> DecodePart A ByteStream + decode End = + \case [] => Just ((), []) + (_::_) => Nothing + decode Fail = const Nothing + decode (Pure x) = pure (MkSing x) + decode (Ignore f _) = ignore (decode f) + decode (Choice f1 f2) = + [| Left (decode f1) |] <|> [| Right (decode f2) |] + decode (Repeat 0 f) = pure [] + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Tuple {reps = []} []) = pure [] + decode (Tuple {reps = _::_} (f :: fs)) = DecodePart.do + x <- decode f + xs <- decode (Tuple fs) + pure (x :: xs) + -- FIXME: Ambiguous elaboration for some reason?? + -- [| decode f :: decode (Tuple fs) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] + decode (Bind f1 f2) = do + x <- decode f1 + y <- decode (f2 x) + pure (x ** y) + decode (Custom f) = f.decode + + + export + encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream + encode End () = pure [] + encode (Pure x) (MkSing _) = pure [] + encode (Ignore f def) () = encode f def + encode (Choice f1 f2) (Left x) = encode f1 x + encode (Choice f1 f2) (Right y) = encode f2 y + encode (Repeat Z f) [] = pure [] + encode (Repeat (S len) f) (x :: xs) = + [| encode f x <+> encode (Repeat len f) xs |] + encode (Tuple {reps = []} []) [] = pure [] + encode (Tuple {reps = _::_} (f :: fs)) (x :: xs) = + [| encode f x <+> encode (Tuple fs) xs |] + encode (Pair f1 f2) (x, y) = + [| encode f1 x <+> encode f2 y |] + encode (Bind f1 f2) (x ** y) = + [| encode f1 x <+> encode (f2 x) y |] + encode (Custom f) x = f.encode x + + + -------------------- + -- CUSTOM FORMATS -- + -------------------- + + + public export + u8 : FormatOf Nat + u8 = Custom (MkCustomFormatOf + { decode = map cast decodeU8 + , encode = encodeU8 . cast {to = Bits8} + }) + + + public export + u16Le : FormatOf Nat + u16Le = Custom (MkCustomFormatOf + { decode = map cast (decodeU16 LE) + , encode = encodeU16 LE . cast {to = Bits16} + }) + + + public export + u16Be : FormatOf Nat + u16Be = Custom (MkCustomFormatOf + { decode = map cast (decodeU16 BE) + , encode = encodeU16 BE . cast {to = Bits16} + }) + + + public export + u32Le : FormatOf Nat + u32Le = Custom (MkCustomFormatOf + { decode = map cast (decodeU32 LE) + , encode = encodeU32 LE . cast {to = Bits32} + }) + + + public export + u32Be : FormatOf Nat + u32Be = Custom (MkCustomFormatOf + { decode = map cast (decodeU32 BE) + , encode = encodeU32 BE . cast {to = Bits32} + }) + + +------------------------- +-- FORMAT DESCRIPTIONS -- +------------------------- + + +||| A format description of an arbitrary representation +public export +record Format where + constructor MkFormat + ||| The in-memory representation of the format description + 0 Rep : Type + ||| The underlying format description + format : FormatOf Rep + + +namespace Format + + decode : (f : Format) -> Decode (Rep f, ByteStream) ByteStream + decode f = FormatOf.decode f.format + + + encode : (f : Format) -> Encode (Rep f) ByteStream + encode f = FormatOf.encode f.format + + +------------------------------------ +-- FORMAT DESCRIPTION CONVERSIONS -- +------------------------------------ + + +namespace Format + + public export + toFormatOf : (f : Format) -> FormatOf f.Rep + toFormatOf (MkFormat _ f) = f + + + ||| Convert a format description into an indexed format description with an + ||| equality proof that the representation is the same as the index. + public export + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A + toFormatOfEq (Element f prf) = rewrite sym prf in f.format + + +namespace FormatOf + + public export + toFormat : {0 A : Type} -> FormatOf A -> Format + toFormat f = MkFormat A f + + + ||| Convert an indexed format description to a existential format description, + ||| along with a proof that the representation is the same as the index. + public export + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) + toFormatEq f = Element (MkFormat A f) Refl + + +public export +toFormatOfIso : Iso Format (Exists FormatOf) +toFormatOfIso = MkIso + { to = \f => Evidence _ (toFormatOf f) + , from = \(Evidence _ f) => toFormat f + , toFrom = \(Evidence _ _) => Refl + , fromTo = \(MkFormat _ _) => Refl + } + + +public export +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf) +toFormatOfEqIso = MkIso + { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) + , from = \(Evidence _ f) => Evidence _ (toFormatEq f) + , toFrom = \(Evidence _ _) => Refl + , fromTo = \(Evidence _ (Element (MkFormat _ _) Refl)) => Refl + } + + +------------------------- +-- FORMAT CONSTRUCTORS -- +------------------------- + +-- Helpful constructors for building non-indexed format descriptions. +-- This also tests if we can actually meaningfully use the `Format` type. + +namespace Format + + public export + end : Format + end = MkFormat () End + + + public export + fail : Format + fail = MkFormat Void Fail + + + public export + pure : {0 A : Type} -> (x : A) -> Format + pure x = MkFormat (Sing x) (Pure x) + + + public export + ignore : (f : Format) -> (def : f.Rep) -> Format + ignore f def = MkFormat Unit (Ignore (toFormatOf f) def) + + + public export + repeat : (len : Nat) -> Format -> Format + repeat len f = MkFormat (Vect len f.Rep) (Repeat len (toFormatOf f)) + + + public export + pair : Format -> Format -> Format + pair f1 f2 = MkFormat (f1.Rep, f2.Rep) (Pair (toFormatOf f1) (toFormatOf f2)) + + + public export + bind : (f : Format) -> (Rep f -> Format) -> Format + bind f1 f2 = + MkFormat (x : f1.Rep ** (f2 x).Rep) + (Bind (toFormatOf f1) (\x => toFormatOf (f2 x))) + + + public export + (>>=) : (f : Format) -> (Rep f -> Format) -> Format + (>>=) = bind diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr b/experiments/idris/src/Fathom/Format/InductiveRecursive.idr new file mode 100644 index 000000000..336fb8d71 --- /dev/null +++ b/experiments/idris/src/Fathom/Format/InductiveRecursive.idr @@ -0,0 +1,272 @@ +||| 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 recursion](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-recursive 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.Format.InductiveRecursive + + +import Data.Colist +import Data.DPair +import Data.HVect +import Data.Vect + +import Fathom.Base +import Fathom.Data.Iso +import Fathom.Data.Sing + + +------------------------- +-- FORMAT DESCRIPTIONS -- +------------------------- + + +mutual + ||| Universe of format descriptions + public export + data Format : Type where + End : Format + Fail : Format + Pure : {0 A : Type} -> A -> Format + Ignore : (f : Format) -> (def : f.Rep) -> Format + Choice : Format -> Format -> Format + Repeat : Nat -> Format -> Format + Tuple : {0 len : Nat} -> Vect len Format -> Format + Pair : Format -> Format -> Format + Bind : (f : Format) -> (f.Rep -> Format) -> Format + + + ||| The in-memory representation of format descriptions + public export + Rep : Format -> Type + Rep End = Unit + Rep Fail = Void + Rep (Pure x) = Sing x + Rep (Ignore _ _) = Unit + Rep (Choice f1 f2) = Either f1.Rep f2.Rep + Rep (Repeat len f) = Vect len f.Rep + Rep (Tuple fs) = HVect (map (.Rep) fs) + Rep (Pair f1 f2) = (f1.Rep, f2.Rep) + Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep) + + + ||| Field syntax for representations + public export + (.Rep) : Format -> Type + (.Rep) = Rep + + +namespace Format + + -- Support for do notation + + public export + pure : {0 A : Type} -> A -> Format + pure = Pure + + public export + (>>=) : (f : Format) -> (f.Rep -> Format) -> Format + (>>=) = Bind + + + --------------------------- + -- ENCODER/DECODER PAIRS -- + --------------------------- + + + export + decode : (f : Format) -> DecodePart f.Rep (Colist a) + decode End = + \case [] => Just ((), []) + (_::_) => Nothing + decode Fail = const Nothing + decode (Pure x) = pure (MkSing x) + decode (Ignore f _) = ignore (decode f) + decode (Choice f1 f2) = + [| Left (decode f1) |] <|> [| Right (decode f2) |] + decode (Repeat 0 f) = pure [] + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Tuple []) = pure [] + decode (Tuple (f :: fs)) = + [| decode f :: decode (Tuple fs) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] + decode (Bind f1 f2) = do + x <- decode f1 + y <- decode (f2 x) + pure (x ** y) + + + export + encode : (f : Format) -> Encode f.Rep (Colist a) + encode End () = pure [] + encode (Pure x) (MkSing _) = pure [] + encode (Ignore f def) () = encode f def + encode (Choice f1 f2) (Left x) = encode f1 x + encode (Choice f1 f2) (Right y) = encode f2 y + encode (Repeat Z f) [] = pure [] + encode (Repeat (S len) f) (x :: xs) = + [| encode f x <+> encode (Repeat len f) xs |] + encode (Tuple []) [] = pure [] + encode (Tuple (f :: fs)) (x :: xs) = + [| encode f x <+> encode (Tuple fs) xs |] + encode (Pair f1 f2) (x, y) = + [| encode f1 x <+> encode f2 y |] + encode (Bind f1 f2) (x ** y) = + [| encode f1 x <+> encode (f2 x) y |] + + +--------------------------------- +-- INDEXED FORMAT DESCRIPTIONS -- +--------------------------------- + + +||| A format description refined with a fixed representation +public export +data FormatOf : (A : Type) -> Type where + MkFormatOf : (f : Format) -> FormatOf f.Rep + + +namespace FormatOf + + decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream + decode (MkFormatOf f) = Format.decode f + + + encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream + encode (MkFormatOf f) = Format.encode f + + +------------------------------------ +-- FORMAT DESCRIPTION CONVERSIONS -- +------------------------------------ + + +namespace Format + + public export + toFormatOf : (f : Format) -> FormatOf f.Rep + toFormatOf f = MkFormatOf f + + + ||| Convert a format description into an indexed format description with an + ||| equality proof that the representation is the same as the index. + public export + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A + toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f + + +namespace FormatOf + + public export + toFormat : {0 A : Type} -> FormatOf A -> Format + toFormat (MkFormatOf f) = f + + + ||| Convert an indexed format description to a existential format description, + ||| along with a proof that the representation is the same as the index. + public export + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) + toFormatEq (MkFormatOf f) = Element f Refl + + +public export +toFormatOfIso : Iso Format (Exists FormatOf) +toFormatOfIso = MkIso + { to = \f => Evidence _ (toFormatOf f) + , from = \(Evidence _ f) => toFormat f + , toFrom = \(Evidence _ (MkFormatOf _)) => Refl + , fromTo = \_ => Refl + } + + +public export +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf) +toFormatOfEqIso = MkIso + { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) + , from = \(Evidence _ f) => Evidence _ (toFormatEq f) + , toFrom = \(Evidence _ (MkFormatOf _)) => Refl + , fromTo = \(Evidence _ (Element _ Refl)) => Refl + } + + +--------------------------------- +-- INDEXED FORMAT CONSTRUCTORS -- +--------------------------------- + +-- Helpful constructors for building index format descriptions. +-- This also tests if we can actually meaningfully use the `FormatOf` type. + +namespace FormatOf + + public export + end : FormatOf Unit + end = MkFormatOf End + + + public export + fail : FormatOf Void + fail = MkFormatOf Fail + + + public export + pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + pure x = MkFormatOf (Pure x) + + + public export + ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit + ignore f def with (toFormatEq f) + ignore _ def | (Element f prf) = MkFormatOf (Ignore f (rewrite prf in def)) + + + public export + repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A) + repeat len f with (toFormatEq f) + repeat len _ | (Element f prf) = + toFormatOfEq (Element (Repeat len f) (cong (Vect len) prf)) + + + public export + pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B) + pair f1 f2 with (toFormatEq f1, toFormatEq f2) + pair _ _ | (Element f1 prf1, Element f2 prf2) = + toFormatOfEq (Element (Pair f1 f2) + (rewrite prf1 in rewrite prf2 in Refl)) + + + public export + bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + bind f1 f2 with (toFormatEq f1) + bind _ f2 | (Element f1 prf) = + ?todoFormatOf_bind + -- toFormatOfEq + -- (Bind f1' (\x => + -- case toFormatEq (f2 x) of + -- (f2' ** prf) => toFormatEq ?todo) + -- ** rewrite prf in ?todoPrfF1) + -- -- MkFormatOf (Bind f1 (\x => + -- -- case toFormatEq (f2 x) of + -- -- (f2' ** prf) => toFormatOfEq ?todo)) + + + public export + (>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + (>>=) = bind diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr new file mode 100644 index 000000000..ec24f85f6 --- /dev/null +++ b/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr @@ -0,0 +1,314 @@ +||| Experimenting with an approach to extending inductive-recursive format +||| descriptions with custom formats. + +module Fathom.Format.InductiveRecursiveCustom + + +import Data.Bits +import Data.Colist +import Data.DPair +import Data.HVect +import Data.Vect + +import Fathom.Base +import Fathom.Data.Iso +import Fathom.Data.Sing + + +------------------------- +-- FORMAT DESCRIPTIONS -- +------------------------- + + +||| A custom format description. +||| +||| We’d prefer to just import `Fathom.Format.Record`, but Idris’ imports are a +||| bit temperamental and result in ambiguities when importing modules that +||| contain types of the same name as those defined in the current module. +public export +record CustomFormat where + constructor MkCustomFormat + Rep : Type + decode : Decode (Rep, ByteStream) ByteStream + encode : Encode Rep ByteStream + + +mutual + ||| Universe of format descriptions + public export + data Format : Type where + End : Format + Fail : Format + Pure : {0 A : Type} -> A -> Format + Ignore : (f : Format) -> (def : f.Rep) -> Format + Choice : Format -> Format -> Format + Repeat : Nat -> Format -> Format + Tuple : {0 len : Nat} -> Vect len Format -> Format + Pair : Format -> Format -> Format + Bind : (f : Format) -> (f.Rep -> Format) -> Format + Custom : (f : CustomFormat) -> Format + + + ||| The in-memory representation of format descriptions + public export + Rep : Format -> Type + Rep End = Unit + Rep Fail = Void + Rep (Pure x) = Sing x + Rep (Ignore _ _) = Unit + Rep (Choice f1 f2) = Either f1.Rep f2.Rep + Rep (Repeat len f) = Vect len f.Rep + Rep (Tuple fs) = HVect (map (.Rep) fs) + Rep (Pair f1 f2) = (f1.Rep, f2.Rep) + Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep) + Rep (Custom f) = f.Rep + + + ||| Field syntax for representations + public export + (.Rep) : Format -> Type + (.Rep) = Rep + + +namespace Format + + -- Support for do notation + + public export + pure : {0 A : Type} -> A -> Format + pure = Pure + + public export + (>>=) : (f : Format) -> (f.Rep -> Format) -> Format + (>>=) = Bind + + + --------------------------- + -- ENCODER/DECODER PAIRS -- + --------------------------- + + + export + decode : (f : Format) -> DecodePart f.Rep ByteStream + decode End = + \case [] => Just ((), []) + (_::_) => Nothing + decode Fail = const Nothing + decode (Pure x) = pure (MkSing x) + decode (Ignore f _) = ignore (decode f) + decode (Choice f1 f2) = + [| Left (decode f1) |] <|> [| Right (decode f2) |] + decode (Repeat 0 f) = pure [] + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Tuple []) = pure [] + decode (Tuple (f :: fs)) = + [| decode f :: decode (Tuple fs) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] + decode (Bind f1 f2) = do + x <- decode f1 + y <- decode (f2 x) + pure (x ** y) + decode (Custom f) = f.decode + + + export + encode : (f : Format) -> Encode f.Rep ByteStream + encode End () = pure [] + encode (Pure x) (MkSing _) = pure [] + encode (Ignore f def) () = encode f def + encode (Choice f1 f2) (Left x) = encode f1 x + encode (Choice f1 f2) (Right y) = encode f2 y + encode (Repeat Z f) [] = pure [] + encode (Repeat (S len) f) (x :: xs) = + [| encode f x <+> encode (Repeat len f) xs |] + encode (Tuple []) [] = pure [] + encode (Tuple (f :: fs)) (x :: xs) = + [| encode f x <+> encode (Tuple fs) xs |] + encode (Pair f1 f2) (x, y) = + [| encode f1 x <+> encode f2 y |] + encode (Bind f1 f2) (x ** y) = + [| encode f1 x <+> encode (f2 x) y |] + encode (Custom f) x = f.encode x + + + -------------------- + -- CUSTOM FORMATS -- + -------------------- + + + public export + u8 : Format + u8 = Custom (MkCustomFormat + { Rep = Nat + , decode = map cast decodeU8 + , encode = encodeU8 . cast {to = Bits8} + }) + + + public export + u16Le : Format + u16Le = Custom (MkCustomFormat + { Rep = Nat + , decode = map cast (decodeU16 LE) + , encode = encodeU16 LE . cast {to = Bits16} + }) + + + public export + u16Be : Format + u16Be = Custom (MkCustomFormat + { Rep = Nat + , decode = map cast (decodeU16 BE) + , encode = encodeU16 BE . cast {to = Bits16} + }) + + + public export + u32Le : Format + u32Le = Custom (MkCustomFormat + { Rep = Nat + , decode = map cast (decodeU32 LE) + , encode = encodeU32 LE . cast {to = Bits32} + }) + + + public export + u32Be : Format + u32Be = Custom (MkCustomFormat + { Rep = Nat + , decode = map cast (decodeU32 BE) + , encode = encodeU32 BE . cast {to = Bits32} + }) + + +--------------------------------- +-- INDEXED FORMAT DESCRIPTIONS -- +--------------------------------- + + +||| A format description indexed with a fixed representation +public export +data FormatOf : (Rep : Type) -> Type where + MkFormatOf : (f : Format) -> FormatOf f.Rep + + +namespace FormatOf + + decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream + decode (MkFormatOf f) = Format.decode f + + + encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream + encode (MkFormatOf f) = Format.encode f + + +------------------------------------ +-- FORMAT DESCRIPTION CONVERSIONS -- +------------------------------------ + + +namespace Format + + public export + toFormatOf : (f : Format) -> FormatOf f.Rep + toFormatOf f = MkFormatOf f + + + ||| Convert a format description into an indexed format description with an + ||| equality proof that the representation is the same as the index. + public export + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A + toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f + + +namespace FormatOf + + public export + toFormat : {0 A : Type} -> FormatOf A -> Format + toFormat (MkFormatOf f) = f + + + ||| Convert an indexed format description to a existential format description, + ||| along with a proof that the representation is the same as the index. + public export + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) + toFormatEq (MkFormatOf f) = Element f Refl + + +public export +toFormatOfIso : Iso Format (Exists FormatOf) +toFormatOfIso = MkIso + { to = \f => Evidence _ (toFormatOf f) + , from = \(Evidence _ f) => toFormat f + , toFrom = \(Evidence _ (MkFormatOf _)) => Refl + , fromTo = \_ => Refl + } + + +public export +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf) +toFormatOfEqIso = MkIso + { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) + , from = \(Evidence _ f) => Evidence _ (toFormatEq f) + , toFrom = \(Evidence _ (MkFormatOf _)) => Refl + , fromTo = \(Evidence _ (Element _ Refl)) => Refl + } + + +--------------------------------- +-- INDEXED FORMAT CONSTRUCTORS -- +--------------------------------- + +-- Helpful constructors for building index format descriptions. +-- This also tests if we can actually meaningfully use the `FormatOf` type. + +namespace FormatOf + + public export + end : FormatOf Unit + end = MkFormatOf End + + + public export + fail : FormatOf Void + fail = MkFormatOf Fail + + + public export + pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + pure x = MkFormatOf (Pure x) + + + public export + ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit + ignore f def with (toFormatEq f) + ignore _ def | (Element f prf) = MkFormatOf (Ignore f (rewrite prf in def)) + + + public export + repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A) + repeat len f with (toFormatEq f) + repeat len _ | (Element f prf) = + toFormatOfEq (Element (Repeat len f) (cong (Vect len) prf)) + + + public export + pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B) + pair f1 f2 with (toFormatEq f1, toFormatEq f2) + pair _ _ | (Element f1 prf1, Element f2 prf2) = + toFormatOfEq (Element (Pair f1 f2) + (rewrite prf1 in rewrite prf2 in Refl)) + + + public export + bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + bind f1 f2 with (toFormatEq f1) + bind _ f2 | (Element f1 prf) = + ?todoFormatOf_bind + + + public export + (>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + (>>=) = bind diff --git a/experiments/idris/src/Fathom/Format/Record.idr b/experiments/idris/src/Fathom/Format/Record.idr new file mode 100644 index 000000000..8e033a116 --- /dev/null +++ b/experiments/idris/src/Fathom/Format/Record.idr @@ -0,0 +1,364 @@ +||| Open format universe +||| +||| This module defines an open universe of binary format descriptions using +||| records to define an interface. 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 ‘coinductively defined +||| universes’ that [some type theorists were proposing](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-12.pdf#page=79), +||| but I may be mistaken. + +module Fathom.Format.Record + + +import Data.Colist +import Data.DPair +import Data.HVect +import Data.Vect + +import Fathom.Base +import Fathom.Data.Iso +import Fathom.Data.Sing + + +------------------------- +-- FORMAT DESCRIPTIONS -- +------------------------- + + +public export +record Format where + constructor MkFormat + Rep : Type + decode : DecodePart Rep ByteStream + encode : Encode Rep ByteStream + + +namespace Format + + public export + end : Format + end = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Unit + + decode : DecodePart Rep ByteStream + decode [] = Just ((), []) + decode (_::_) = Nothing + + encode : Encode Rep ByteStream + encode () = Just [] + + + public export + fail : Format + fail = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Void + + decode : DecodePart Rep ByteStream + decode = const Nothing + + encode : Encode Rep ByteStream + 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 : DecodePart Rep ByteStream + decode = pure (MkSing x) + + encode : Encode Rep ByteStream + encode (MkSing _) = pure [] + + + public export + ignore : (f : Format) -> (def : f.Rep) -> Format + ignore f def = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = () + + decode : DecodePart Rep ByteStream + decode = ignore f.decode + + encode : Encode Rep ByteStream + encode () = f.encode def + + + public export + choice : Format -> Format -> Format + choice f1 f2 = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Either f1.Rep f2.Rep + + decode : DecodePart Rep ByteStream + decode = + [| Left f1.decode |] <|> [| Right f2.decode |] + + encode : Encode Rep ByteStream + encode (Left x) = f1.encode x + encode (Right y) = f2.encode y + + + public export + repeat : Nat -> Format -> Format + repeat len f = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = Vect len f.Rep + + decode : DecodePart Rep ByteStream + decode = go len where + go : (len : Nat) -> DecodePart (Vect len f.Rep) ByteStream + go 0 = pure [] + go (S len) = [| f.decode :: go len |] + + encode : Encode Rep ByteStream + encode = go len where + go : (len : Nat) -> Encode (Vect len f.Rep) ByteStream + go 0 [] = pure [] + go (S len) (x :: xs) = [| f.encode x <+> go len xs |] + + + public export + tuple : {0 len : Nat} -> Vect len Format -> Format + tuple fs = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = HVect (map (.Rep) fs) + + decode : DecodePart Rep ByteStream + decode = go fs where + go : {0 len : Nat} -> (fs : Vect len Format) -> DecodePart (HVect (map (.Rep) fs)) ByteStream + go [] = pure [] + go (f :: fs) = [| f.decode :: go fs |] + + encode : Encode Rep ByteStream + encode = go fs where + go : {0 len : Nat} -> (fs : Vect len Format) -> Encode (HVect (map (.Rep) fs)) ByteStream + go [] [] = pure [] + go (f :: fs) (x :: xs) = [| f.encode x <+> go fs xs |] + + + public export + pair : Format -> Format -> Format + pair f1 f2 = MkFormat { Rep, decode, encode } where + Rep : Type + Rep = (f1.Rep, f2.Rep) + + decode : DecodePart Rep ByteStream + decode = + [| (,) f1.decode f2.decode |] + + encode : Encode Rep ByteStream + encode (x, y) = + [| f1.encode x <+> f2.encode y |] + + + 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 : DecodePart Rep ByteStream + decode = do + x <- f1.decode + y <- (f2 x).decode + pure (x ** y) + + encode : Encode Rep ByteStream + encode (x ** y) = + [| f1.encode x <+> (f2 x).encode y |] + + + -- Support for do notation + + public export + (>>=) : (f : Format) -> (Rep f -> Format) -> Format + (>>=) = bind + + +-------------------- +-- CUSTOM FORMATS -- +-------------------- + + +namespace Format + + public export + u8 : Format + u8 = MkFormat + { Rep = Nat + , decode = map cast decodeU8 + , encode = encodeU8 . cast {to = Bits8} + } + + + public export + u16Le : Format + u16Le = MkFormat + { Rep = Nat + , decode = map cast (decodeU16 LE) + , encode = encodeU16 LE . cast {to = Bits16} + } + + + public export + u16Be : Format + u16Be = MkFormat + { Rep = Nat + , decode = map cast (decodeU16 BE) + , encode = encodeU16 BE . cast {to = Bits16} + } + + + public export + u32Le : Format + u32Le = MkFormat + { Rep = Nat + , decode = map cast (decodeU32 LE) + , encode = encodeU32 LE . cast {to = Bits32} + } + + + public export + u32Be : Format + u32Be = MkFormat + { Rep = Nat + , decode = map cast (decodeU32 BE) + , encode = encodeU32 BE . cast {to = Bits32} + } + + +--------------------------------- +-- INDEXED FORMAT DESCRIPTIONS -- +--------------------------------- + + +||| A format description refined with a fixed representation +public export +data FormatOf : (A : Type) -> Type where + MkFormatOf : (f : Format) -> FormatOf f.Rep + + +namespace FormatOf + + decode : {0 A : Type} -> (f : FormatOf A) -> DecodePart (A) ByteStream + decode (MkFormatOf f) = Format.decode f + + + encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream + encode (MkFormatOf f) = Format.encode f + + +------------------------------------ +-- FORMAT DESCRIPTION CONVERSIONS -- +------------------------------------ + + +namespace Format + + public export + toFormatOf : (f : Format) -> FormatOf f.Rep + toFormatOf f = MkFormatOf f + + + ||| Convert a format description into an indexed format description with an + ||| equality proof that the representation is the same as the index. + public export + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A + toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f + + +namespace FormatOf + + public export + toFormat : {0 A : Type} -> FormatOf A -> Format + toFormat (MkFormatOf f) = f + + + ||| Convert an indexed format description to a existential format description, + ||| along with a proof that the representation is the same as the index. + public export + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) + toFormatEq (MkFormatOf f) = Element f Refl + + +public export +toFormatOfIso : Iso Format (Exists FormatOf) +toFormatOfIso = MkIso + { to = \f => Evidence _ (toFormatOf f) + , from = \(Evidence _ f) => toFormat f + , toFrom = \(Evidence _ (MkFormatOf _)) => Refl + , fromTo = \_ => Refl + } + + +public export +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => Rep f = a)))) (Exists FormatOf) +toFormatOfEqIso = MkIso + { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) + , from = \(Evidence _ f) => Evidence _ (toFormatEq f) + , toFrom = \(Evidence _ (MkFormatOf _)) => Refl + , fromTo = \(Evidence _ (Element _ Refl)) => Refl + } + + +--------------------------------- +-- INDEXED FORMAT CONSTRUCTORS -- +--------------------------------- + +-- Helpful constructors for building index format descriptions. +-- This also tests if we can actually meaningfully use the `FormatOf` type. + +namespace FormatOf + + public export + end : FormatOf Unit + end = MkFormatOf end + + + public export + fail : FormatOf Void + fail = MkFormatOf fail + + + public export + pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x) + pure x = MkFormatOf (pure x) + + + public export + ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit + ignore f def with (toFormatEq f) + ignore _ def | (Element f prf) = MkFormatOf (ignore f (rewrite prf in def)) + + + public export + repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A) + repeat len f with (toFormatEq f) + repeat len _ | (Element f prf) = + toFormatOfEq (Element (repeat len f) (cong (Vect len) prf)) + + + public export + pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B) + pair f1 f2 with (toFormatEq f1, toFormatEq f2) + pair _ _ | (Element f1 prf1, Element f2 prf2) = + toFormatOfEq (Element (pair f1 f2) + (rewrite prf1 in rewrite prf2 in Refl)) + + + public export + bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + bind f1 f2 with (toFormatEq f1) + bind _ f2 | (Element f1 prf) = + ?todoFormatOf_bind + + + public export + (>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x) + (>>=) = bind diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr new file mode 100644 index 000000000..6f56d8a4f --- /dev/null +++ b/experiments/idris/src/Playground.idr @@ -0,0 +1,255 @@ +module Playground + + +import Data.Colist +import Data.Vect +import Data.HVect + +import Fathom.Base +import Fathom.Data.Sing +import Fathom.Format.InductiveRecursive as IndRec +import Fathom.Format.IndexedInductive as Indexed +import Fathom.Format.Record as Record + + +-- Experiment with converting between the different styles of format universes + + +||| Convert an inductive-recursive format universe into a record format +public export +format : IndRec.Format -> Record.Format +format f = Record.MkFormat + { Rep = f.Rep + , decode = decode f + , encode = encode f + } + + +||| Convert 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 = decode f + , encode = 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 +-- Ignore 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 +-- Ignore 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 f.Rep +indRecToIndexed End = Indexed.End +indRecToIndexed Fail = Indexed.Fail +indRecToIndexed (Pure x) = Indexed.Pure x +indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def +indRecToIndexed (Choice f1 f2) = Indexed.Choice (indRecToIndexed f1) (indRecToIndexed f2) +indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f) +indRecToIndexed (Tuple fs) = ?todo_indRecToIndexedTuple +indRecToIndexed (Pair f1 f2) = Indexed.Pair (indRecToIndexed f1) (indRecToIndexed f2) +indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToIndexed (g x)) + + +mutual + + ||| Convert an indexed format description to an inductive-recursive format + indexedToIndRecFormat : (f : Indexed.Format) -> (f' : IndRec.Format ** f.Rep = f'.Rep) + indexedToIndRecFormat (MkFormat () End) = (End ** Refl) + indexedToIndRecFormat (MkFormat Void Fail) = (Fail ** Refl) + indexedToIndRecFormat (MkFormat (Sing x) (Pure x)) = (Pure x ** Refl) + indexedToIndRecFormat (MkFormat () (Ignore f def)) with (indexedToIndRecFormatOf f) + _ | MkFormatOf f' = (Ignore f' def ** Refl) + indexedToIndRecFormat (MkFormat (Either _ _) (Choice f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2) + _ | (MkFormatOf f1', MkFormatOf f2') = (Choice f1' f2' ** Refl) + indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f) + _ | MkFormatOf f' = (Repeat len f' ** Refl) + indexedToIndRecFormat (MkFormat (HVect reps) (Tuple fs)) = + ?todo_indexedToIndRecFormatTuple + indexedToIndRecFormat (MkFormat (_, _) (Pair f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2) + _ | (MkFormatOf f1', MkFormatOf f2') = (Pair f1' f2' ** Refl) + indexedToIndRecFormat (MkFormat (x : _ ** _) (Bind f1 f2)) with (indexedToIndRecFormatOf f1) + _ | MkFormatOf f1' = + (Bind f1' (\x => ?indexedToIndRecFormatBind_f2) ** ?todoBindPrf) + + + ||| Convert an indexed format description to an inductive-recursive format + indexedToIndRecFormatOf : {0 A : Type} -> (f : Indexed.FormatOf A) -> IndRec.FormatOf A + indexedToIndRecFormatOf End = MkFormatOf End + indexedToIndRecFormatOf Fail = MkFormatOf Fail + indexedToIndRecFormatOf (Pure x) = MkFormatOf (Pure x) + indexedToIndRecFormatOf (Ignore f def) with (indexedToIndRecFormatOf f) + _ | MkFormatOf f' = MkFormatOf (Ignore f' def) + indexedToIndRecFormatOf (Choice f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2) + _ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Choice f1' f2') + indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f) + _ | MkFormatOf f' = MkFormatOf (Repeat len f') + indexedToIndRecFormatOf (Tuple fs) = + ?todo_indexedToIndRecFormatOfTuple + indexedToIndRecFormatOf (Pair f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2) + _ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Pair f1' f2') + indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormatOf f1) + _ | MkFormatOf f1' = + -- -- let + -- -- bindF1F2 = Bind f1' (\x => + -- -- let + -- -- (f2' ** _) = toFormat (indexedToIndRecFormatOf (f2 x)) + -- -- in + -- -- ?indexedToIndRecFormatOfBind_f2) + -- -- in + -- -- ?indexedToIndRecFormatOfBind + -- MkFormatOf (Bind f1' (\x => + -- let + -- (f2' ** prf) = toFormat (indexedToIndRecFormatOf (f2 x)) + -- in + -- ?indexedToIndRecFormatOfBind_f2)) + -- indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormat (MkFormat _ f1)) + -- _ | (f1' ** prf) = + ?indexedToIndRecFormatOfBind + + +-- ||| Convert an indexed format description to an inductive-recursive format +-- indexedToIndRec : {0 A : Type} -> (f : Indexed.FormatOf A) -> IndRec.FormatOf A +-- indexedToIndRec End = MkFormatOf IndRec.End +-- indexedToIndRec Fail = MkFormatOf IndRec.Fail +-- indexedToIndRec (Pure x) = MkFormatOf (IndRec.Pure x) +-- indexedToIndRec (Ignore f def) with (indexedToIndRec f) +-- indexedToIndRec (Ignore _ def) | MkFormatOf f = MkFormatOf (IndRec.Ignore f def) +-- indexedToIndRec (Repeat len f) with (indexedToIndRec f) +-- indexedToIndRec (Repeat len _) | MkFormatOf f = MkFormatOf (IndRec.Repeat len f) +-- indexedToIndRec (Bind f1 f2) with (indexedToIndRec f1) +-- indexedToIndRec (Bind _ f2) | MkFormatOf f1 = +-- ?todo_indexedToIndRec + +-- indexedToIndRec (Bind f1 f2) with (indexedToIndRec f1) + -- _ | (MkFormatOf End) = MkFormatOf (Bind End ?todo_indexedToIndRec_2) + -- _ | (MkFormatOf Fail) = MkFormatOf (Bind Fail absurd) + -- _ | (MkFormatOf (Pure f)) = MkFormatOf (Bind ?todo_indexedToIndRec_4) + -- _ | (MkFormatOf (Ignore f def)) = MkFormatOf (Bind ?todo_indexedToIndRec_5) + -- _ | (MkFormatOf (Repeat k x)) = MkFormatOf (Bind ?todo_indexedToIndRec_6) + -- _ | (MkFormatOf (Bind f g)) = MkFormatOf (Bind ?todo_indexedToIndRec_7) + +-- indexedToIndRec (Bind f1 f2) with (sameRep (indexedToIndRec f1)) +-- indexedToIndRec (Bind _ f2) | (f1' ** prf) = +-- rewrite sym prf in MkFormatOf (Bind f1' (\x => ?todo_indexedToIndRec)) +-- where +-- indexedToIndRecF2 : {0 A : Type} -> {0 B : A -> Type} -> ((x : A) -> Indexed.FormatOf (B x)) -> ((x : A) -> IndRec.FormatOf (B x)) +-- indexedToIndRecF2 x = ?todofF2 + +-- indexedToIndRec (Bind f1 f2) with (indexedToIndRec f1) +-- indexedToIndRec (Bind _ f2) | MkFormatOf f1 = +-- let +-- bindF1 = Bind f1 +-- bodyF2 : x : f1.Rep -> FormatOf () +-- bodyF2 = x : f1.Rep => +-- case sameRep (indexedToIndRec (f2 x)) of +-- (f2' ** prf) => f2') +-- in +-- ?todo_indexedToIndRec +-- where +-- indexedToIndRecF2 : {0 A : Type} -> {0 B : A -> Type} -> ((x : A) -> Indexed.FormatOf (B x)) -> ((x : A) -> IndRec.FormatOf (B x)) +-- indexedToIndRecF2 x = ?todofF2 + +-- indexedToIndRec (Bind f1 f2) with (sameRep (indexedToIndRec f1)) +-- _ | (End ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_2 +-- _ | (Fail ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_3 +-- _ | ((Pure f) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_4 +-- _ | ((Ignore f def) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_5 +-- _ | ((Repeat k x) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_6 +-- _ | ((Bind f g) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_7 + +-- indexedToIndRec (Bind f1 f2) with (sameRep (indexedToIndRec f1)) +-- indexedToIndRec (Bind _ f2) | (f1' ** prf) = +-- let bindF1 = Bind f1' in + -- MkFormatOf (Bind f1' (\x => + -- let + -- f2' = f2 x + -- -- f2'' = sameRep f2' + -- in + -- ?help)) + -- let f1' = indexedToIndRec f1 + -- (f1'', fromRep) = sameRep' f1' + -- in + +-- indexedToIndRec (Bind f1 f2) = indexedToIndRecBind f1 f2 +-- indexedToIndRec (Bind f1 f2) with (sameRep (indexedToIndRec f1)) +-- indexedToIndRec (Bind _ f2) | (f1 ** prf) = +-- let hmm = Bind f1 +-- in +-- -- f1 : Format +-- -- 0 A : Type +-- -- f2 : (x : f1.Rep) -> FormatOf (B x) +-- -- ------------------------------ +-- -- todo_indexedToIndRec : FormatOf (DPair (Rep f1) (\x => B x)) + -- ?todo_indexedToIndRec + -- MkFormatOf (Bind f1 (\x => ?help)) +-- -- let +-- -- -- x' : A +-- -- -- x' = x +-- -- f2' = f2 x +-- -- MkFormatOf f2'' = indexedToIndRec f2' +-- -- in +-- -- f2'')) + +-- indexedToIndRec' : {0 A : Type} -> (f : Indexed.FormatOf A) -> IndRec.Format +-- indexedToIndRec' End = IndRec.End +-- indexedToIndRec' Fail = IndRec.Fail +-- indexedToIndRec' (Pure x) = IndRec.Pure x +-- indexedToIndRec' (Ignore f def) with (MkFormatOf (indexedToIndRec' f)) +-- _ | f' = IndRec.Ignore (indexedToIndRec' f) ?todo1 +-- indexedToIndRec' (Repeat len f) = IndRec.Repeat len (indexedToIndRec' f) +-- indexedToIndRec' (Bind f1 f2) = IndRec.Bind (indexedToIndRec' f1) ?todo2 + + +-- indexedToIndRec'' : (f : Indexed.Format) -> IndRec.Format +-- indexedToIndRec'' (MkFormat () End) = IndRec.End +-- indexedToIndRec'' (MkFormat Void Fail) = IndRec.Fail +-- indexedToIndRec'' (MkFormat (Sing x) (Pure x)) = IndRec.Pure x +-- indexedToIndRec'' (MkFormat () (Ignore f def)) with (indexedToIndRec'' (MkFormat _ f)) +-- _ | f'' = IndRec.Ignore f'' ?tododef +-- indexedToIndRec'' (MkFormat rep (Repeat len f)) = IndRec.Repeat len (indexedToIndRec'' f) +-- indexedToIndRec'' (MkFormat rep (Bind f1 f2)) = IndRec.Bind (indexedToIndRec'' f1) ?todo2 + + +-- Reproduction of difficulties in OpenType format, drawing parallels to +-- Tarski-style universes. + +record Flag where + constructor MkFlag + id : Nat + repeat : case id of + 0 => Nat + S n => Sing {A = Nat} 0 + +record SimpleGlyph where + constructor MkSimpleGlyph + flag : Flag + flag_repeat : Sing {A = Nat} (case flag of + MkFlag 0 repeat => repeat + MkFlag (S n) repeat => val repeat) diff --git a/experiments/idris/src/Playground/Extraction.idr b/experiments/idris/src/Playground/Extraction.idr new file mode 100644 index 000000000..75e0c99e0 --- /dev/null +++ b/experiments/idris/src/Playground/Extraction.idr @@ -0,0 +1,112 @@ +||| Thinking about extracting format descriptions to Rust + +module Playground.Extraction + + +import Fathom.Data.Sing +import Fathom.Format.InductiveRecursiveCustom + + +namespace Rust + + data RType : Type where + Var : String -> RType + U8 : RType + U16 : RType + U32 : RType + U64 : RType + I8 : RType + I16 : RType + I32 : RType + I64 : RType + Never : RType + Tuple : List RType -> RType + Vec : RType -> RType + + + data Item : Type where + Struct : List (String, RType) -> Item + Enum : List (String, RType) -> Item + DecodeFn : () -> Item + EncodeFn : () -> Item + + + record Module where + constructor MkModule + items : List (String, Item) + + +namespace Compile + + -- TODO: Cache compilations of definitions + -- eg. of structs, enums, endocers and decoders + + + compileFormat : Format -> (Rust.Module -> Maybe Rust.Module) + compileFormat f = + -- compile rep + -- compile decode + -- compile encode + ?todo_compileFormat + + + compileRep : (f : Format) -> Maybe Rust.RType + compileRep End = Just (Rust.Tuple []) + compileRep Fail = Just (Rust.Never) + compileRep (Ignore _ _) = Just (Rust.Tuple []) + compileRep (Choice f1 f2) = + ?todo_compileRepChoice + compileRep (Repeat _ f) = + Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a + -- fixed size array if the length is known + -- or just throw away the info + compileRep (Tuple fs) = + ?todo_compileRepTuple + compileRep (Pure x) = + ?todo_compileSingRep -- TODO: interpret an Idris type as a Rust type?? + -- perhaps we need to restrict this? + compileRep (Pair f1 f2) = + Just (Rust.Tuple + [ !(compileRep f1) + , !(compileRep f2) + ]) + compileRep (Bind f1 f2) = + Just (Tuple + [ !(compileRep f1) + , !(compileRep (f2 ?todo_compileBind_x)) -- TODO: how to bind the output? + -- enum based on the values of `x : Rep f1`? + -- depends on how `x` is used inside `f2` + ]) + compileRep (Custom f) = + -- TODO: f.RustRep + Nothing + + + compileDecode : Format -> (Rust.Module -> Maybe Rust.Module) + compileDecode End = ?todo_compileDecodeEnd + compileDecode Fail = ?todo_compileDecodeFail + compileDecode (Pure x) = ?todo_compileDecodePure + compileDecode (Ignore f _) = ?todo_compileDecodeIgnore + compileDecode (Choice f1 f2) = ?todo_compileDecodeChoice + compileDecode (Repeat len f) = ?todo_compileDecodeRepeat + compileDecode (Tuple fs) = ?todo_compileDecodeTuple + compileDecode (Pair f1 f2) = ?todo_compileDecodePair + compileDecode (Bind f1 f2) = ?todo_compileDecodeBind + compileDecode (Custom f) = + -- TODO: f.rustDecode + ?todo_compileDecodeCustom + + + compileEncode : Format -> (Rust.Module -> Maybe Rust.Module) + compileEncode End = ?todo_compileEncodeEnd + compileEncode Fail = ?todo_compileEncodeFail + compileEncode (Pure x) = ?todo_compileEncodePure + compileEncode (Ignore f def) = ?todo_compileEncodeIgnore + compileEncode (Choice f1 f2) = ?todo_compileEncodeChoice + compileEncode (Repeat len f) = ?todo_compileEncodeRepeat + compileEncode (Tuple fs) = ?todo_compileEncodeTuple + compileEncode (Pair f1 f2) = ?todo_compileEncodePair + compileEncode (Bind f1 f2) = ?todo_compileEncodeBind + compileEncode (Custom f) = + -- TODO: f.rustEncode + ?todo_compileEncodeCustom diff --git a/experiments/idris/src/Playground/HeterogeneousSequences.idr b/experiments/idris/src/Playground/HeterogeneousSequences.idr new file mode 100644 index 000000000..d0ebdf596 --- /dev/null +++ b/experiments/idris/src/Playground/HeterogeneousSequences.idr @@ -0,0 +1,31 @@ +-- Heterogeneous sequence example + +module Playground.HeterogeneousSequences + + +import Data.Vect +import Data.HVect + +import Fathom.Base +import Fathom.Data.Sing +import Fathom.Format.Record + + +namespace Format + + ||| Construct a format based on a type tag + value : Nat -> Format + value 1 = u8 + value 2 = u16Be + value 4 = u32Be + value _ = fail + + + ||| An annoying example from: https://github.com/yeslogic/fathom/issues/394 + ouch : Format + ouch = do + len <- u16Be + types <- repeat len u16Be + values <- tuple (map value types) + -- ^^^^^ heterogeneous sequence of formats + pure () diff --git a/experiments/idris/src/Playground/OpenType/IndexedInductive.idr b/experiments/idris/src/Playground/OpenType/IndexedInductive.idr new file mode 100644 index 000000000..53d3d20c9 --- /dev/null +++ b/experiments/idris/src/Playground/OpenType/IndexedInductive.idr @@ -0,0 +1,99 @@ +||| Reproduction of difficulties in OpenType format + +module Playground.OpenType.IndexedInductive + + +import Fathom.Data.Sing +import Fathom.Format.IndexedInductiveCustom + + +namespace FormatOf + + Flag : Type + Flag = + ( id : Nat + ** repeat : + case id of + 0 => Nat + S n => Sing {A = Nat} 0 + ** Sing () + ) + + + (.repeat) : Flag -> Nat + (.repeat) (0 ** repeat ** _) = repeat + (.repeat) (S _ ** repeat ** _) = val repeat + + + -- def flag = { + -- flag <- u8, + -- repeat <- match (flag & 8 != (0 : U8)) { + -- true => u8, + -- false => succeed U8 0, + -- }, + -- }; + flag : FormatOf Flag + flag = do + flag <- u8 + repeat <- case flag of + 0 => u8 + S _ => Pure {A = Nat} 0 + Pure () + + + SimpleGlyph : Type + SimpleGlyph = + ( flag : Flag + ** Sing (flag.repeat + 1) + ) + + + -- def simple_glyph = fun (number_of_contours : U16) => { + -- ... + -- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8), + -- ... + -- }; + simple_glyph : FormatOf SimpleGlyph + simple_glyph = do + flag <- flag + Pure (flag.repeat + 1) + + +namespace Format + + -- Reproduction of difficulties in OpenType format + + -- def flag = { + -- flag <- u8, + -- repeat <- match (flag & 8 != (0 : U8)) { + -- true => u8, + -- false => succeed U8 0, + -- }, + -- }; + flag : Format + flag = Format.do + id <- toFormat u8 + repeat <- case id of + 0 => toFormat u8 + S n => pure {A = Nat} 0 + pure () + + + -- def simple_glyph = fun (number_of_contours : U16) => { + -- ... + -- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8), + -- ... + -- }; + simple_glyph : Format + simple_glyph = Format.do + flag <- flag + let + repeat : Nat + repeat = ?todo_repeat + -- repeat = case the (Format.Rep flag) flag of + -- (0 ** repeat ** MkSing ()) => repeat + -- (S n ** repeat ** MkSing ()) => repeat + + -- Error: While processing right hand side of simple_glyph. While processing right hand side + -- of simple_glyph,repeat. Can't match on 0 as it must have a polymorphic type. + pure (repeat + 1) diff --git a/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr b/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr new file mode 100644 index 000000000..01ae5f459 --- /dev/null +++ b/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr @@ -0,0 +1,92 @@ +||| Reproduction of difficulties in OpenType format + +module Playground.OpenType.InductiveRecursive + + +import Fathom.Data.Sing +import Fathom.Format.InductiveRecursiveCustom + + +namespace Format + + -- def flag = { + -- flag <- u8, + -- repeat <- match (flag & 8 != (0 : U8)) { + -- true => u8, + -- false => succeed U8 0, + -- }, + -- }; + flag : Format + flag = do + id <- u8 + repeat <- case id of + 0 => u8 + S _ => Pure {A = Nat} 0 + Pure () + + + (.repeat) : Format.flag.Rep -> Nat + (.repeat) (0 ** repeat ** _) = repeat + (.repeat) (S _ ** repeat ** _) = val repeat + + + -- def simple_glyph = fun (number_of_contours : U16) => { + -- ... + -- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8), + -- ... + -- }; + simple_glyph : Format + simple_glyph = do + flag <- flag + Pure (flag.repeat + 1) + + +namespace FormatOf + + Flag : Type + Flag = + ( id : Nat + ** repeat : + case id of + 0 => Nat + S n => Sing {A = Nat} 0 + ** Sing () + ) + + (.repeat) : Flag -> Nat + (.repeat) (0 ** repeat ** _) = repeat + (.repeat) (S _ ** repeat ** _) = val repeat + + + -- def flag = { + -- flag <- u8, + -- repeat <- match (flag & 8 != (0 : U8)) { + -- true => u8, + -- false => succeed U8 0, + -- }, + -- }; + flag : FormatOf Flag + flag = FormatOf.do + flag <- toFormatOf u8 + repeat <- case flag of + 0 => toFormatOf u8 + S _ => pure {A = Nat} 0 + pure () + + + SimpleGlyph : Type + SimpleGlyph = + ( flag : Flag + ** Sing (flag.repeat + 1) + ) + + + -- def simple_glyph = fun (number_of_contours : U16) => { + -- ... + -- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8), + -- ... + -- }; + simple_glyph : FormatOf SimpleGlyph + simple_glyph = FormatOf.do + flag <- flag + pure (flag.repeat + 1) diff --git a/experiments/idris/src/Playground/OpenType/Record.idr b/experiments/idris/src/Playground/OpenType/Record.idr new file mode 100644 index 000000000..c9bdce4da --- /dev/null +++ b/experiments/idris/src/Playground/OpenType/Record.idr @@ -0,0 +1,92 @@ +||| Reproduction of difficulties in OpenType format + +module Playground.OpenType.Record + + +import Fathom.Data.Sing +import Fathom.Format.Record + + +namespace Format + + -- def flag = { + -- flag <- u8, + -- repeat <- match (flag & 8 != (0 : U8)) { + -- true => u8, + -- false => succeed U8 0, + -- }, + -- }; + flag : Format + flag = do + id <- u8 + repeat <- case id of + 0 => u8 + S _ => pure {A = Nat} 0 + pure () + + + (.repeat) : Format.flag.Rep -> Nat + (.repeat) (0 ** repeat ** _) = repeat + (.repeat) (S _ ** repeat ** _) = val repeat + + + -- def simple_glyph = fun (number_of_contours : U16) => { + -- ... + -- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8), + -- ... + -- }; + simple_glyph : Format + simple_glyph = do + flag <- flag + pure (flag.repeat + 1) + + +namespace FormatOf + + Flag : Type + Flag = + ( id : Nat + ** repeat : + case id of + 0 => Nat + S n => Sing {A = Nat} 0 + ** Sing () + ) + + (.repeat) : Flag -> Nat + (.repeat) (0 ** repeat ** _) = repeat + (.repeat) (S _ ** repeat ** _) = val repeat + + + -- def flag = { + -- flag <- u8, + -- repeat <- match (flag & 8 != (0 : U8)) { + -- true => u8, + -- false => succeed U8 0, + -- }, + -- }; + flag : FormatOf Flag + flag = FormatOf.do + flag <- toFormatOf u8 + repeat <- case flag of + 0 => toFormatOf u8 + S _ => pure {A = Nat} 0 + pure () + + + SimpleGlyph : Type + SimpleGlyph = + ( flag : Flag + ** Sing (flag.repeat + 1) + ) + + + -- def simple_glyph = fun (number_of_contours : U16) => { + -- ... + -- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8), + -- ... + -- }; + simple_glyph : FormatOf SimpleGlyph + simple_glyph = FormatOf.do + flag <- flag + pure (flag.repeat + 1) diff --git a/flake.nix b/flake.nix index 4c996f3d6..d832fca4e 100644 --- a/flake.nix +++ b/flake.nix @@ -74,19 +74,60 @@ # 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) + # Keyboard input is currently broken on the version of Idris 2 + # on nixPkgs (v0.5.1). To work around this, run Idris shells with: + # + # $ rlwrap [options] idris2 ... + # + # See: https://github.com/idris-lang/Idris2/issues/54 + pkgs.rlwrap + ]; + }; + + # 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 +137,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 );