Warning with `total` and `constructor`

amelieled commented 1 year ago

What component is the issue in?

None

Which command

[X] kompile
[ ] kast
[ ] krun
[ ] kprove
[ ] kprovex
[ ] ksearch

What K Version?

K version: v5.5.116

Operating System

Linux

K Definitions (If Possible)

module TOTO-SYNTAX

    syntax T ::= "titi" [total, constructor]
    syntax T ::= "tutu"

endmodule

module TOTO
    imports TOTO-SYNTAX

    rule titi => tutu

endmodule

Steps to Reproduce

kompile toto.k generates:

[Warning] Compiler: The attribute 'total' was applied to a production which
does not have the 'function' attribute; the attribute was ignored.
    Source(/home/camel/REFACTOR/kamelo/tests/001_imp-dico/toto.k)
    Location(3,18,3,45)
    3 |     syntax T ::= "titi" [total, constructor]
      .                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~

Expected Results

[Warning] Compiler: The attribute 'total' was applied to a production which
is already declared with the 'constructor' attribute; the attribute was ignored because of useless.

or something like that (or no warning).

amelieled commented 1 year ago

If I delete the attribute total, no warning whereas the attribute constructor is also useless.

Baltoli commented 1 year ago

I don't think that constructor is a special attribute from the perspective of the K frontend, looking at the index: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md#attribute-index

In user K code (as opposed to KORE), the total attribute is only meaningful when applied to function rules, so I think this check is working as intended. Is there a specific use-case or example where this isn't the case for you?

amelieled commented 1 year ago

constructor isn't special but implicit if function isn't used. I don't understand this sentence: "In user K code (as opposed to KORE), the total attribute is only meaningful when applied to function rules" because K and Kore need to keep the same semantics.

From the user point of view, a constructor is total so the warning message is not adapted for the above example.

Baltoli commented 1 year ago

Sure, I see what you mean. I guess the changes required here are:

Add constructor to the list of valid attributes.. Its behaviour is a no-op when applied to a constructor, and should be an error when combined with function.
Warn the user if they specify constructor without total as well.
Turn off the warning you mention above for [constructor, total].

My understanding here is that you want to be able to write K code that more closely maps to the actual KORE that gets generated (i.e. specifying constructor manually rather than having it be autogenerated by the compiler). Is that correct?

amelieled commented 1 year ago

I agree because constructor is implicit.
That's depend: as constructor is implicit when you don't write function.
Or raise a different warning.

So, no, I don't want that K will become as KORE syntax. For me, K is syntactic sugar/ high-level language, and Kore is an assembly language.

Baltoli commented 1 year ago

So, no, I don't want that K will become as KORE syntax. For me, K is syntactic sugar/ high-level language, and Kore is an assembly language.

What is your use case for writing [constructor] in K code then? We can implement this easily enough, I just want to make sure I understand why it's desirable.

ehildenb commented 1 year ago

Reading this: https://fsl.cs.illinois.edu/publications/rosu-2017-lmcs.pdf

constructor implies surjective and injective, but also "no confusion".
total (new and unique) means "returns at least one element", which I think is a slightly weaker property than surjective, because surjective is written with an element variable on the left, which means a single element.
function (new and unique) means "returns at most one element", which I think is also weaker than surjective.

So, I guess constructor does imply function and total. I think until now, constructor has not been something we have let users write themselves, instead we just infer it as "productions without attributes".

It's a little strange though, because right now to mark something as constructor, you just don't put any attributes. But this also implies that it is function and total. So it's almost like by default we have a constructor attribute, but the user can override it to make that weaker into just function and/or total and/or injective attributes.

ehildenb commented 1 year ago

It seems that there are several options:

Don't emit a warning when constructor and total are used together, because total is implied by constructor.
Change the warning to say that total is redundant with constructor (or an error?)

@amelieled would it be helpful for us to always make sure that total and function are added to every constructor as well, because they are implied? Why are you originally trying to put both these attributes on a production in the first place?

amelieled commented 1 year ago

I guess the second option is the same as mine.

But constructor doesn't imply function (just injective and total) FMO.

My test comes from the fact that I am trying to check the adequacy between the K file and the generated Kore file.

ehildenb commented 1 year ago

Well, function just means "returns at most one value on every input", and "total" just means "returns at least one value on every input". So constructor, being injective and total, implies function, total.

So by default, productions are considered constructor, which implies function, total. Once you put function or function, total on it, then you are weakening what we're saying about the symbol.

ehildenb commented 1 year ago

We should make it so that Kore emission does not allow constructor productions to also have total and function and injective, because constructor subsumes the other attributes.

We also need to document this case.

radumereuta commented 1 year ago

We already have a warning for this case. We can make it an error simply by changing this line.

        if (prod.att().contains(Att.TOTAL()) && !prod.att().contains(Att.FUNCTION())) {
            kem.registerCompilerWarning(ExceptionType.IGNORED_ATTRIBUTE, errors,
                "The attribute 'total' was applied to a production which does not have the 'function' attribute; the attribute was ignored.", prod);
        }

Change to errors.add(KEMException.compilerError(...

runtimeverification / k