agda2hs

agda2hs copied to clipboard

Add a primitive `Let` that is compiled to `let` in Haskell

2

jespercockx

The error produced when we detect clashing imports does not currently contain an error location, c.f. [the clashingImports function](https://github.com/agda/agda2hs/blob/master/src/Agda2Hs/Compile/Imports.hs#L69). One solution might be to add a field `importRange :: Range`...

omelkonian

Haskell does not have overloaded constructors, so we should make sure that we do not allow several constructors with the same name to be compiled to Haskell.

jespercockx

jespercockx

Disallow compilation of symbols from local modules

2

Haskell does not have local modules, so they should not be allowed by agda2hs. We could make an exception if the local module is `open public`ed at the top-level.

jespercockx

These are not supported in Haskell, so they should not be allowed.

jespercockx

Check that all used definitions are actually defined in the Haskell code

1

@flupe mentioned to me that it would be a good idea to check that all defined symbols that are used in the generated Haskell code are also actually defined in...

jespercockx

```agda open import Haskell.Prelude module _ where cast : {a b : Set} → @0 a ≡ b → a → b cast {a} {b} = cast' where cast' :...

jespercockx

Docs: add `syntax` trick to use Unicode instead of Haskell-compatible ASCII identifiers

1

Although users should generally use Haskell-compile identifiers for the definitions they compile with `agda2hs`, one could use `syntax` or `pattern` declarations in Agda to emulate Unicode mixfix definitions that are...

omelkonian

Adding mechanism to compile Haskell.Data.* modules to Data.* modules

3

I've opened a separate PR for this. There is now a list of module prefixes which get compiled to corresponding Haskell modules. E.g. `Haskell.Data.Map` becomes `Data.Map`. Actually, the test files...

viktorcsimma