[Agda] Allow cyclic module imports

[Martin Escardo]

On 26/04/18 09:29, nad at cse.gu.se wrote:
> On 2018-04-25 22:01, Martín Hötzel Escardó wrote:
>> There are a number of things to consider:
>>
>> (1) Is this easy to implement?
>>
>> (2) Does it have conceptual / software engineering disadvantages?
> 
> I'm not quite sure what you are proposing. Is the idea to treat
> everything in a module cycle as one big mutual block? 

No.

> Or is the idea to
> still require mutual blocks for things that are mutually recursive, but
> sort the mutual blocks topologically? 

Yes.

> In the latter case, should this
> sorting be done after meta-variables have been resolved (in which case I
> wonder how they are resolved), or based only on what the user has
> written in the code? And how should independent definitions be ordered?
> Or should the signature be modified so that it is no longer a list (of
> mutual blocks), but some kind of DAG?

In my example, I have a sets A, B, C of code for certain mathematical 
concepts a,b,c. At the moment, I have to break things e,g. in modules 
A1-A3, B1-B3, C1-C2

     A1
         B1
             C1
         B2
     A2
             C2
     A3
         B3

where the modules in each line depend on the modules in the previous 
lines. I would rather have only three modules A=A1+A2+A3, B=B1+B2+B3, 
and C=C1+C2, each of them cyclically importing each other, but Agda 
figuring out that there is no real cyclic dependency.

Martin