Rewrite rules: specifiable imports from Prelude

[viktorcsimma]

Closes #192. Adds the opportunity to define the handling of Prelude in the config file. See the documentation update for details:

By default, agda2hs handles Prelude like other modules: it collects all the identifiers it finds we use from Prelude, and adds them to Prelude's import list.

In the config YAML, we can specify a different behaviour. The format is:

# First, we specify how to handle Prelude.
prelude:
  implicit: true
  hiding:           # if implicit is true
    - seq

  #using:           # if implicit is false
  #  - +
  #  - Num

# Then the rules themselves.
rules:

  # The rational type.
  - from: Data.Rational.Unnormalised.Base.ℚᵘ
    to: Rational
    importing: Data.Ratio
  - [...]

If implicit is true, then everything gets imported from Prelude, except for those that are specified in the hiding list. This can cause clashes if you reuse names from Prelude, hence the opportunity for a hiding list. If there is no such list, then everything gets imported.

If implicit is false, Prelude gets imported explicitly, and only those identifiers that are specified in the using list. If there is no such list, agda2hs reverts to the default behaviour (it tries to collect imports by itself).

[jespercockx]

Thanks, this is great once again! I'm actually thinking that perhaps it would even be a good idea to have implicit prelude set to true, since it is less likely to cause problems with identifiers being out of scope (at the cost of potentially having name clashes, but it is probably a good thing to have an error when you accidentally introduce a name clash with a function from Prelude).

[viktorcsimma]

Thank you:) I've tried out setting the default to an implicit Prelude, but this broke the tests in cases where Haskell.Prelude was imported with a qualifier (usually Pre). This might be solved by a qualified import, but then we would have to deal with the case when some of it is imported with a qualifier and some of it is not. Another option would be to simply delete the qualifier, but this would then create clashes that did not exist in the Agda code.

What do you think? Maybe we should leave it as it is for now and create an issue for changing the default.

[jespercockx]

Sure, that's a good idea.