Question: resolving ambiguities using labels

[kheradmand]

Hi I have a definition and part of it looks like this:

    syntax CounterType ::=
                          "bytes"       [klabel(CTBytes)]
                        | "packets"     [klabel(CTPackets)]
                        | "bytes_and_packets"

    syntax MeterType ::=  "bytes"       [klabel(MTBytes)]
                        | "packets"     [klabel(MTPackets)]
   ...

I have the following rule:

  rule <k> @updateCounter (C:Id , I:Int) => T ==K bytes ... </k>
     <statefuls> <stateful> <name> N </name> <opts> "$counter_type" |-> T:CounterType _:Map </opts> ... </stateful> ... </statefuls>

When I kompile the definition I get the following ambiguity warning:

[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: syntax MeterType@STATEFUL-SYNTAX ::= "bytes"
[Location(#token("80",Int@INT-SYNTAX),#token("27",Int@INT-SYNTAX),#token("80",Int@INT-SYNTAX),#token("57",Int@INT-SYNTAX))
Source(#token("/home/ali/P4/p4k/./src/syntax/stateful-syntax.k",KString@KSTRING))
klabel(#token("MTBytes",AttributeValue))
klabel(#token("MTBytes",KString@KSTRING))]
    MTBytes()
2: syntax CounterType@STATEFUL-SYNTAX ::= "bytes"
[Location(#token("40",Int@INT-SYNTAX),#token("27",Int@INT-SYNTAX),#token("40",Int@INT-SYNTAX),#token("57",Int@INT-SYNTAX))
Source(#token("/home/ali/P4/p4k/./src/syntax/stateful-syntax.k",KString@KSTRING))
klabel(#token("CTBytes",AttributeValue))
klabel(#token("CTBytes",KString@KSTRING))]
    CTBytes()
    Source(./src/p4-semantics.k)
    Location(763,49,763,54)

Now I want to disambiguate this using the labels but I don't know how. Trying T ==K CTBytes, T ==K CTBytes(), T ==K CTBytes(.KList), and getKLabel(T) ==K CTBytes haven't worked.

[kheradmand]

@daejunpark any ideas?

[lucaspena]

Hi Ali,

If you change the rule to

rule @updateCounter (C:Id , I:Int) => T ==K

parseToken("CounterType@STATEFUL-SYNTAX", "bytes") ...

 <statefuls> <stateful> <name> N </name> <opts> "$counter_type"

|-> T:CounterType _:Map ... ...

This is actually eliminating the ambiguity based on the sort rather than the label. I'm not sure if you can eliminate the ambiguity via the label.

On Mon, Sep 11, 2017 at 2:50 PM, Ali Kheradmand notifications@github.com wrote:

@daejunpark https://github.com/daejunpark any ideas?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/kframework/k/issues/2339#issuecomment-328639336, or mute the thread https://github.com/notifications/unsubscribe-auth/AD1ZLryq5qPrbCBx3XuzsBOOlbfr2C2Sks5shY8AgaJpZM4PSmmv .

-- Lucas Peña University of Illinois at Urbana-Champaign lpena7@illinois.edu (954) 882-7070

[kheradmand]

Thanks a lot @lucaspena :) 👍

[kheradmand]

@lucaspena Actually I don't know why the following happens:

<T> <k> @updateCounter ( my_indirect_counter , 0 )  ...
...
 <stateful> <stype> $counter </stype> <name> my_indirect_counter </name> <opts> "$counter_type" |-> packets "$instant_count" |-> 16384 "$table" |-> m_table "$saturating" |-> false "$signed" |-> false "$binding" |-> $static_global </opts> <vals> .Map </vals> <width> 0 </width> </stateful> 
... 
KDebug> step
1 Step(s) Taken.
KDebug> peek
<T> <k> false ...

I expected this to evaluate to true

the rule is:

rule <k> @updateCounter (C:Id , I:Int) => T ==K #parseToken("CounterType@STATEFUL-SYNTAX", "packets") ... </k>
     <statefuls> <stateful> <name> N </name> <opts> ("$counter_type" |-> T:CounterType) _:Map </opts> ... </stateful> ... </statefuls>

[lucaspena]

Hm, I'm not sure why that is. Do you think you can create a full minimal example I can look at? The rule seemed to go through fine in a small example I created locally. My only guess would be that when packets is placed into the opts map it has the wrong sort. What happens if MeterType is used in the rule instead of CounterType?

[kheradmand]

I will try that but the sort of T is checked in the rule : ...("$counter_type" |-> T:CounterType)...

[lucaspena]

Yea, the rule likely won't apply with that change. I would suggest that when packets is loaded into the map to also use the #parseToken syntax.

[kheradmand]

I don't know how to use #parseToken in that case, the rule is the following:

rule <k> @processDec(counter Name:Id { type : T:CounterType ; SOpt:StatefulOptionals COpt:CounterOptionals }) => . ... </k>
     <statefuls>
        (.Bag =>
            <stateful>
                <stype> $counter </stype>
                <name> Name </name>
                <opts> ("$counter_type" |-> T) @processStatefulOpts(SOpt, ("$binding" |-> $static_global)) @processCounterOpts(COpt, ("$signed" |-> false) ("$saturating" |-> false)) </opts>
                <width> 0 </width> // = inf
                ...
            </stateful>
        ) ...
     </statefuls>

I'll try a smaller definition to isolate the problem.

[kheradmand]

ok the problem was due to a typo in the rule

rule <k> @updateCounter (C:Id , I:Int) => T ==K #parseToken("CounterType@STATEFUL-SYNTAX", "packets") ... </k>
     <statefuls> <stateful> <name> N </name> <opts> ("$counter_type" |-> T:CounterType) _:Map </opts> ... </stateful> ... </statefuls>

N -> C But I also needed to add the attribute token to the production rules. Thanks @lucaspena

[lucaspena]

Great! Can we close this issue now?