{"action":"created","issue":{"url":"https://api.github.com/repos/kframework/k/issues/2339","repository_url":"https://api.github.com/repos/kframework/k","labels_url":"https://api.github.com/repos/kframework/k/issues/2339/labels{/name}","comments_url":"https://api.github.com/repos/kframework/k/issues/2339/comments","events_url":"https://api.github.com/repos/kframework/k/issues/2339/events","html_url":"https://github.com/kframework/k/issues/2339","id":256574550,"number":2339,"title":"Question: resolving ambiguities using labels","user":{"login":"kheradmand","id":2971184,"avatar_url":"https://avatars2.githubusercontent.com/u/2971184?v=4","gravatar_id":"","url":"https://api.github.com/users/kheradmand","html_url":"https://github.com/kheradmand","followers_url":"https://api.github.com/users/kheradmand/followers","following_url":"https://api.github.com/users/kheradmand/following{/other_user}","gists_url":"https://api.github.com/users/kheradmand/gists{/gist_id}","starred_url":"https://api.github.com/users/kheradmand/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kheradmand/subscriptions","organizations_url":"https://api.github.com/users/kheradmand/orgs","repos_url":"https://api.github.com/users/kheradmand/repos","events_url":"https://api.github.com/users/kheradmand/events{/privacy}","received_events_url":"https://api.github.com/users/kheradmand/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2017-09-11T03:49:13Z","updated_at":"2017-09-11T22:52:28Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"Hi I have a definition and part of it looks like this:\r\n\r\n```\r\n    syntax CounterType ::=\r\n                          \"bytes\"       [klabel(CTBytes)]\r\n                        | \"packets\"     [klabel(CTPackets)]\r\n                        | \"bytes_and_packets\"\r\n\r\n    syntax MeterType ::=  \"bytes\"       [klabel(MTBytes)]\r\n                        | \"packets\"     [klabel(MTPackets)]\r\n   ...\r\n```\r\n\r\nI have the following rule:\r\n```\r\n  rule <k> @updateCounter (C:Id , I:Int) => T ==K bytes ... </k>\r\n     <statefuls> <stateful> <name> N </name> <opts> \"$counter_type\" |-> T:CounterType _:Map </opts> ... </stateful> ... </statefuls>\r\n```\r\n\r\nWhen I kompile the definition I get the following ambiguity warning:\r\n```\r\n[Warning] Inner Parser: Parsing ambiguity. Arbitrarily choosing the first.\r\n1: syntax MeterType@STATEFUL-SYNTAX ::= \"bytes\"\r\n[Location(#token(\"80\",Int@INT-SYNTAX),#token(\"27\",Int@INT-SYNTAX),#token(\"80\",Int@INT-SYNTAX),#token(\"57\",Int@INT-SYNTAX))\r\nSource(#token(\"/home/ali/P4/p4k/./src/syntax/stateful-syntax.k\",KString@KSTRING))\r\nklabel(#token(\"MTBytes\",AttributeValue))\r\nklabel(#token(\"MTBytes\",KString@KSTRING))]\r\n    MTBytes()\r\n2: syntax CounterType@STATEFUL-SYNTAX ::= \"bytes\"\r\n[Location(#token(\"40\",Int@INT-SYNTAX),#token(\"27\",Int@INT-SYNTAX),#token(\"40\",Int@INT-SYNTAX),#token(\"57\",Int@INT-SYNTAX))\r\nSource(#token(\"/home/ali/P4/p4k/./src/syntax/stateful-syntax.k\",KString@KSTRING))\r\nklabel(#token(\"CTBytes\",AttributeValue))\r\nklabel(#token(\"CTBytes\",KString@KSTRING))]\r\n    CTBytes()\r\n\tSource(./src/p4-semantics.k)\r\n\tLocation(763,49,763,54)\r\n```\r\n\r\nNow 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.  "},"comment":{"url":"https://api.github.com/repos/kframework/k/issues/comments/328681263","html_url":"https://github.com/kframework/k/issues/2339#issuecomment-328681263","issue_url":"https://api.github.com/repos/kframework/k/issues/2339","id":328681263,"user":{"login":"lucaspena","id":4020526,"avatar_url":"https://avatars3.githubusercontent.com/u/4020526?v=4","gravatar_id":"","url":"https://api.github.com/users/lucaspena","html_url":"https://github.com/lucaspena","followers_url":"https://api.github.com/users/lucaspena/followers","following_url":"https://api.github.com/users/lucaspena/following{/other_user}","gists_url":"https://api.github.com/users/lucaspena/gists{/gist_id}","starred_url":"https://api.github.com/users/lucaspena/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lucaspena/subscriptions","organizations_url":"https://api.github.com/users/lucaspena/orgs","repos_url":"https://api.github.com/users/lucaspena/repos","events_url":"https://api.github.com/users/lucaspena/events{/privacy}","received_events_url":"https://api.github.com/users/lucaspena/received_events","type":"User","site_admin":false},"created_at":"2017-09-11T22:52:27Z","updated_at":"2017-09-11T22:52:27Z","author_association":"CONTRIBUTOR","body":"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."}}
{"actor":{"display_login":"lucaspena"}}