Comment scope inconsistent in the presence of subtheories

[rappatoni]

Commenting out subtheories does not currently work. Neither commenting out a whole theory that contains substheories. Sometimes things appear to break only in syntax-highlighting. Sometimes during type-checking as well.

Panoptikum-Repo: https://gl.kwarc.info/rappatoni/panoptikum

Code example:

namespace http://mathhub.info/Panoptikum/examples❚

/T Comments interact with subtheories in strange and unexpected ways.
This interaction appears to break things at different levels (Syntax Highlighting/Parsing/Type-Checking) as the following examples show.
❚

fixmeta ur:?LF ❚

theory Test =
/T This is produces syntax highligthing warnings and breaks highlighting of comments
 thereafter but type-checks and builds correctly❙
test: type ❙
    // theory Sub_test =
    ❚
test_function: test ⟶ test ❙
❚

theory Test_two =
/T This produces a type-checking error: unknown keyword: test_function❙
test: type ❙
    // theory Sub_test =
        a: test ❙
    ❚
test_function: test ⟶ test ❙
❚

// theory Test_three =
/T This produces a type-checking error: unknown keyword: test_function❙
test: type ❙
    theory Sub_test =
    ❚
test_function: test ⟶ test ❙
❚

[Jazzpirate]

It's actually perfectly consistent, but unintuitive if you think of it as "commenting out a theory".

A comment is delimited by the approriate delimiter for where the comment occurs. A comment outside of a module is delimited by a module delimiter, because it appears on the "module level".

A comment inside a module is delimited by a declaration delimiter, because it appears on the "declaration level".

A theory - even inside another theory - is delimited by a module delimiter. However, if you now comment out such a theory, and it is nested, then the comment is inside a theory and hence delimited by a declaration delimiter. If a module delimiter appears instead, I would expect that the whole module is being closed, which explains the type-checking error in Test_two - (the delimiter that is supposed to close the (commented out) theory Sub_test closes Test_two instead, hence test_function is outside of a module).
Test_three naturally doesn't work, no idea why it should - ctest_function occurs outside of any theory, which is not allowed.

I have no idea why the theory Test does not throw a type checking error, though.

Inconsistencies between MMT's parser and IntelliJ's syntax highlighting (which I guess you mean by Syntax Highlighting) are quite possible. If we can identify what exactly the discrepancies are they might be fixable, but since IntelliJ uses a fixed BNF grammar whereas MMT does not, there's a decent chance that they aren't fixable at all.

Given the above, it's not entirely clear what the supposed bug is - except for a possible bug in the INtelliJ plugin, which doesn't belong here though ;)

[Jazzpirate]

Ah, I now understand why theory Test works, but theory Test_two doesn't:

The comment inside the first theory is closed by a module delimiter, but that one does not close the whole module.

In the second theory however, the comment is closed by the declaration delimiter following "a : test", and then another module delimiter appears, which closes the whole module.

Consequently, a comment inside a theory being delimited by a module delimiter seems to be allowed and not close the surrounding module.

EDIT: I think I can adapt the BNF in the IntelliJ Plugin accordingly

[Jazzpirate]

Here's an actual weirdness though:

1. comments on the declaration level can be closed by module delimiters. This closes the comment and nothing else.
   but:
2. comments on the object level can be close by object delimiters, closing the comment, or declaration delimiters, or module delimiters, both of which close the whole constant, but not the module.

Some further experimentation shows, that constants can also be closed by module delimiters without closing the module.

So the actual rules seems to be:

1. Object Delimiters close the current object (type/definiens/notation/alias/role/metadata/comment inside a constant)
2. Declaration Delimiters close the current declaration
3. Module Delimiters close the currently open declaration, if one is open, or the currently open module if no declaration needs closing.

This means: Objects are always closed with their containing declarations, but declarations need to always be explicitly closed before their containing module can be closed.
@florian-rabe to what degree is this expected behavior?

[rappatoni]

Here is the behaviour I would expect:

• If modules can be declared inside other modules as submodules (I am not sure whether those modules are actually on the object level or on the module level. I assume they remain on the module level?) then so should module-level comment. So if I "comment out" a subtheory, the comment should always be ended by the next module level delimiter (i.e. the commented-out module's delimiter).

• Likewise, if modules can have submodules within their scope (e.g. theories with subtheories), delimited by a module-level delimiter, then so should module level comments.

[rappatoni]

In other words, whatever theory and view declarations do to "figure out" which level they are on/which delimiter pertains to them, comments should do the same thing.

[rappatoni]

I assume the problem is that comment keywords are not level-specific like module keywords which makes this difficult to implement.

[Jazzpirate]

That's fundamentally counter to what comments are though.

Firstly: Apparently comments in modules can be delimited by module delimiters - see my previous comment.
Secondly: A comment inside a module should be closed by a declaration delimiter. That's a given. I don't think you'll disagree. Your problem is that a comment inside a module is not only delimited by a module delimiter though. And they really shouldn't be, ever ;)

The solution you propose would require for comments to be actively parsed to look for e.g. the keyword "theory" in order to actively skip declaration delimiters that would otherwise close the comment. And I maintain that that would yield entirely different problems. For example:

theory Bla =
// this theory contains whatever DD
const a : b DD
MD

^ this theory would now be empty, because the comment contains the keyword "theory" and hence only ends at the MD at the bottom.

[Jazzpirate]

In other words, whatever theory and view declarations do to "figure out" which level they are on/which delimiter pertains to them, comments should do the same thing.

They do, that's exactly your problem ;)

[rappatoni]

The solution you propose would require for comments to be actively parsed to look for e.g. the keyword "theory" in order to actively skip declaration delimiters that would otherwise close the comment. And I maintain that that would yield entirely different problems. For example:

theory Bla
// this theory contains whatever DD
const a : b DD
MD

^ this theory would now be empty, because the comment contains the keyword "theory" and hence only ends at the MD at the bottom.

This is indeed a problem. Then it seems the only option to achieve what I want would be level-specific comment key words.

Secondly: A comment inside a module should be closed by a declaration delimiter. That's a given. I don't think you'll disagree. Your problem is that a comment inside a module is not only delimited by a module delimiter though. And they really shouldn't be, ever ;)

This would also work, then one would just wrap the submodule with a comment and a declaration-level delimiter, right?

[Jazzpirate]

This would also work, then one would just wrap the submodule with a comment and a declaration-level delimiter, right?

...this already works. That's exactly how comments work ;)

Your problem is exactly that that is how it works.

If you comment out a non-empty theory, this theory will contain declaration delimiters. These dellimiters close a comment. What you want is for a comment to not be closed by those declaration delimiters, and instead only close when encountering the module delimiter that closes the theory that you comment out. But as I said, for that to work, the parser would have to actively parse the comment to realize that it contains a theory, and then skip the declaration delimiters.

I maintain that that is counter to the whole point of comments; which is that they're not actively being parsed ;) And no other language does that - imagine that in Scala a comment that would contain a "{" would only close if the correponding "}" is encountered... that would cause a lot more confusion than it would solve.

Then it seems the only option to achieve what I want would be level-specific comment key words.

That would be possible, but also horrible. Nobody wants to memorize three distinct comment keywords and which level which belongs to.
But I agree that the current comment handling is not nice either...

[kohlhase]

I think we have to distinguish between "comments" and "commenting out". Both are legitimate, and they are related.
But comments are not ideal for commenting out as the discussion shows.
Some languages have "paired comments" that are intended for commenting out. Maybe MMT could profit from something like this.

[rappatoni]

Another "solution" would be always having to escape keywords in comments. But that is horrible too.

[rappatoni]

I think we have to distinguish between "comments" and "commenting out". Both are legitimate, and they are related.
But comments are not ideal for commenting out as the discussion shows.
Some languages have "paired comments" that are intended for commenting out. Maybe MMT could profit from something like this.

Would this correspond to having dedicated keyword/delimiter pair for those?

[Jazzpirate]

Some languages have "paired comments" that are intended for commenting out. Maybe MMT could profit from something like this.

All comments in MMT are paired, the problem is that the ending element of the pair changes depending on the level.

I vaguely remember there being a "good" reason why that is the case, but maybe that reason is now obsolete...? Or one picks a separate comment delimiter (also horrible)?

Anyway, all of this is something that can/should be discussed

[kohlhase]

There is also the issue of "semantic" and "syntactic" comments, ...

MMT comments are more on the semantic side.
commenting out should be syntactic.
So a new commenting out pair (e.g. <!-- .... --> like in XML) which can be complicated (so that it does not interfere with other syntax) could help,.

[rappatoni]

There is also the issue of "semantic" and "syntactic" comments, ...

MMT comments are more on the semantic side.
commenting out should be syntactic.
So a new commenting out pair (e.g. <!-- .... --> like in XML) which can be complicated (so that it does not interfere with other syntax) could help,.

Shouldn't the "//"-comments be syntactic in that sense and the "/T" comments semantic? Or is there a semantic use for "//"-comments?

[florian-rabe]

When I designed the // comment syntax, I liked how it lets users comment out multi-line declarations with a change in a single place.

Later I realized it doesn't work well for commenting out the outer one of nested theory/structure declarations.
But I didn't have an immediate idea how to fix it. So I ignored the problem.

[ComFreek]

Tangential: If there are concrete working/intended-to-fail test cases for syntax highlighters, I'd be more than happy to integrate them into the highlighters I've written.