Allow files without top module

[GoogleCodeExporter]

For throw-away Agda files, I would like to be able to omit the

  module JustAThrowAwayFileButModuleNameMustMatchFileNameExactly where

top-level module declaration.

Use cases:

• little bits of Agda code in a presentation
• test suite
• playing, experimentation and demonstration

If no module name is encounterd before the first non-import statement, just the (unqualified) file name is taken as module name.

Original issue reported on code.google.com by andreas....@gmail.com on 12 Nov 2013 at 1:59

[GoogleCodeExporter]

Allows either omitting the top-level module or defining it as module _ where.

Original comment by ulf.nor...@gmail.com on 13 Nov 2013 at 10:53

• Changed state: Fixed

[GoogleCodeExporter]

After the patches, the following module doesn't type-check:

module Foo
where

$ agda Foo.agda
...
Parse error Foo<ERROR> where ...

Original comment by andres.s...@gmail.com on 13 Nov 2013 at 12:27

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 13 Nov 2013 at 4:26

• Added labels: Milestone-2.3.4, Priority-High, Type-Defect
• Removed labels: Type-Enhancement

[GoogleCodeExporter]

That's by design. Put a space before the where. The top-level is now in a layout context, which makes the syntax more consistent than before (you couldn't write a local module like that before).

Original comment by ulf.nor...@gmail.com on 13 Nov 2013 at 8:34

• Changed state: Fixed

[andreasabel]

Fix for this issue introduced #1388 in commit f304322.
#1388 fixed in 470dbcf.

[andreasabel]

I admit that dropping the module header altogether did not pass the test of time. It makes recognizing the top-level module too context-dependent. Omitting the name and writing module _ where however seems stable.