Opt out of code generation for mock implementations

[ruifengx]

I am trying to wrap the Data.Sequence module for use with agda2hs. Rather than to postulate everything, I want to provide a mock definition (backed by Agda Lists) that also reduces within Agda. Therefore, I want a variant of COMPILE pragma that makes these mock definitions ignored like postulates (so that the generated code would import the Haskell module with the same name from containers). In addition, all the additional checks in agda2hs should be turned off for these definitions (as they do not need code generation).

I tried the rewrite rules (the YAML configuration file), but I have two problems with them. First, since I am in charge of the wrapping, I do not want information scattered in both the Agda source file and the YAML configuration. Second, I discovered that the rewrite rules behave differently from COMPILEd definitions. For example, I cannot seem to make agda2hs respect qualified imports (the imported names are always unqualified, clashing with names from Prelude; in the case for modules like Data.Sequence, the convention in Haskell is to always import them qualified).

Am I missing something? Is there already a solution for my problem? If not, do you think it makes sense to have such functionality?

Perhaps we can have some annotations on an Agda module that makes agda2hs skip code-generation for it, or perhaps we can introduce a command-line flag to only perform code-generation for the input Agda file (skipping its dependencies), providing finer-grained control?

[jespercockx]

This should already work if you just define an Agda module named Haskell.Data.Sequence which provides the definitions, it does not have to be just postulates.

If you want to have this on a more fine-grained level, then github.com//pull/446 should fix this.

Could you post a minimal example that demonstrates the problem with missing qualifiers?

[ruifengx]

Oh, thanks. I was speculating from what I see in the official base/containers libraries, and clearly I attributed to the wrong reason. (I observed that postulates without COMPILE pragma are generated as-is, and I thought being postulates are probably significant.)

For the unqualified imports with rewrite rules, here is a minimal reproducing example:

-- test.agda-lib
name: test
include: .
depend: standard-library agda2hs-base
flags: --erasure

-- Data/Sequence.agda
module Data.Sequence where
open import Haskell.Prelude hiding (length)
length : Nat
length = 0

-- Test.agda
module Test where
open import Haskell.Prelude
import Data.Sequence as Seq
test : Nat
test = Seq.length
{-# COMPILE AGDA2HS test #-}

# config.yaml
rewrites:
  - from: Data.Sequence.length
    to: length
    importing: Data.Sequence

Compile with agda2hs --config=config.yaml Test.agda -o haskell. The following Test.hs is generated:

module Test where

import Data.Sequence (length)
import Numeric.Natural (Natural)

test :: Natural
test = length

Notice how length is imported from Data.Sequence unqualified.

[jespercockx]

It's not an ideal solution, but you could specify that the import of Prelude should hide length: https://github.com/agda/agda2hs/blob/master/docs/source/features.md#handling-of-prelude

Maybe a better way to fix this would be to let the user decide whether a rewrite rule should produce a qualified or unqualified import.

[ruifengx]

Yes, that would be better.

I originally thought qualified imports should be preserved, even when a rewrite rule applies, but then I realised that the name would change, and a name clash might be eliminated or introduced as the result of renaming.

What I don't like about the workaround is that it hides the function globally, i.e., it applies to the whole project. If I am not mistaken, the YAML configuration file applies to all the recursive dependencies in an agda2hs invocation?

P.S. Since my main question is resolved (I should use the magic module path prefix Haskell.), should I close this issue, or should we leave it open and use this issue as a tracker to improve the documentation (mention this magic somewhere)?

[jespercockx]

P.S. Since my main question is resolved (I should use the magic module path prefix Haskell.), should I close this issue, or should we leave it open and use this issue as a tracker to improve the documentation (mention this magic somewhere)?

I think the least confusing thing to do is to close this issue and create new issue(s) for the remaining problem(s).