The syntactic productions for the configuration should be part of the module

[cos]

Otherwise, we'll have to always do always account for klabels without syntax, which is cumbersome.

I think we already have them as we can parse, but they're not imported in the final module. @dwightguth, I think you know best where this fits.

[dwightguth]

I'm not sure I follow what you're saying. It sounds like you're talking about productions such as syntax KCell ::= "<k>" K "</k>", but those productions actually do become part of the parsed module. So I'm really not following what you mean.

[cos]

Found the problem: the heating/cooling rules are added the the same module containing the syntax, while the configuration syntax is only added to the final module.

We'll have to figure out how configuration modularization works at some point. For now, could the heating/cooling rules be added to the final module instead?

[dwightguth]

I mean, we could do something like this, but it doesn't really solve the underlying problem. What if I do the following:

module TEST-SYNTAX
  imports INT
  syntax Foo ::= foo(Int)
endmodule

module TEST1
  imports TEST-SYNTAX
  rule foo(5 => 6)
endmodule

module TEST2
  imports TEST1
  configuration <k> $PGM:K </k>
endmodule

Here also the rule is in a module that does not import the configuration.

What exactly are you trying to do, and why aren't you simply using the main execution module, which should have everything it needs?

[cos]

The compiler transformations are now correct with respect to modularization, i.e., the modules are preserved and the passes are applied recursively, not on the final flattened module

[cos]

I think we should strive to preserve that.

[dwightguth]

Okay but what does that rule even mean? If it's not in a module that imports the configuration, then it doesn't import the main cell that the language definition of K says it should get wrapped in. So what are you proposing the semantics of such a rule even should be? Are we just going to reject such rules? That's really inconvenient to declare that modules that don't import a configuration can't contain any rules.

[cos]

@dwightguth, you implemented the configuration-to-productions pass. Would it be easy to implement something along these lines?

Have a configuration syntax accept "@MODULE", which essentially inlines the configuration defined in MODULE.

We would then define <k> in the some small module that we import everywhere, and have the final configuration import and them mention @K. E.g.:

<T> @K <state> .Map </state> </T>

[cos]

If you like it and think it would not be too hard to implement, I will put up a wiki page with the proposal so we can have an agreement on it (fingers crossed).

[cos]

Okay but what does that rule even mean?

Exactly, semantically, the rule should be aware of at least part of the configuration.

[dwightguth]

okay so, there is one other problem which is, the compiler completes rules to the top right now. We would not be able to do that if we wanted to compose configurations together.

[cos]

hm... correct.

[dwightguth]

So, here's one thought. We could have some kind of pushout semantics for a module with a configuration declaration that imports another module with rules in it. Namely, a rule with no cells in it in a module with no configuration has no direct semantics by itself, but its semantics when imported from a module with a configuration declaration is that that module contains a rule which is wrapped by whatever the main cell in the configuration happens to be.

[cos]

Semantically, it is ok for the rules to not know about the entire configuration. The issue is that the configuration concretization is done statically.

To preserve behavior, one easy solution would be to move all rules to the bottom module before concretization. Configuration-abstraction-aware backends could choose not to do that, but all the current backends kind of need it.

[cos]

And yes, modularizing the configuration definitely requires including it in the definition of the our pushout. But it seems the pushout easily remains universal so it should be ok.