agda2hs

agda2hs copied to clipboard

Unary operators

2

Running `agda2hs` on code like ```agda +++_ : Nat → Nat +++_ x = 2 * x {-# COMPILE AGDA2HS +++_ #-} usage : Nat usage = +++ 5 ```...

bwbush

If an Agda module only contains typeclass instances (i.e., orphans), then `agda2hs` code in other modules do not have an `import` statement generated for the module with the instances. Here...

bwbush

Postulates are not exported

1

If a type is postulated, but aliased via the `COMPILE` pragma, it is not exported for other modules to use. In the example below, `ByteString` is not accessible from Haskell...

bwbush

Better support for wrapping Haskell modules via `postulate`

2

## Problem statement The mission statement of Adga2hs is to carve out a sublanguage of Agda that translates directly to Haskell, so that we can prove properties about Haskell-in-Agda programs...

HeinrichApfelmus

`agda2hs` fails unless `agda` or `agda2hs` is run first

2

The first execution of `agda2hs` fails for [this code](https://github.com/input-output-hk/peras-design/tree/56a57bb1475b60c76904909ead532cc0967a84de/src): ```console $ find -type f -name \*.agdai -delete $ agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda Checking Peras.QCD.Node.Specification...

bwbush

Code like ```agda instance iMaybeHashable : ⦃ i : Hashable a ⦄ → Hashable (Maybe a) iMaybeHashable {{_}} .hash Nothing = MakeHash ∘ hashBytes $ hash iUnitHashable tt iMaybeHashable {{i}}...

bwbush

Definition of `Functor` is inconsistent with `base-4.18.1.0` etc.

1

The `agda2hs` prelude puts `void` as a member of the typeclass, but the latest GHC base libraries do not. Compare `void` in https://github.com/agda/agda2hs/blob/7b3e48a35448acff9bb5823ca22623eafb000d15/lib/Haskell/Prim/Functor.agda#L15-L24 and to it's top-level placement in https://github.com/ghc/ghc/blob/f3225ed4b3f3c4309f9342c5e40643eeb0cc45da/libraries/base/Data/Functor.hs#L210-L211...

bwbush

Newtype constructor erroneously removed

2

Agda ```agda record Hash (a : Set) : Set where constructor MakeHash field hashBytes : ByteString open Hash public {-# COMPILE AGDA2HS Hash newtype deriving (Generic, Show) #-} instance iMaybeHashable...

bwbush

nix binary ignores interface files

1

I am expecting that agda2hs will not recompile the interface files, but it looks like this is not the case for the binary on my system. Is this expected behavior?...

stites

Work in progress. - proofs for iLawfulOrd Nat - in progress proof for iLawfulOrd Intreger

odderwiser