{"action":"created","issue":{"url":"https://api.github.com/repos/kframework/k/issues/1903","labels_url":"https://api.github.com/repos/kframework/k/issues/1903/labels{/name}","comments_url":"https://api.github.com/repos/kframework/k/issues/1903/comments","events_url":"https://api.github.com/repos/kframework/k/issues/1903/events","html_url":"https://github.com/kframework/k/issues/1903","id":121863035,"number":1903,"title":"`Production` vs `SyntaxSort`","user":{"login":"cos","id":37514,"avatar_url":"https://avatars.githubusercontent.com/u/37514?v=3","gravatar_id":"","url":"https://api.github.com/users/cos","html_url":"https://github.com/cos","followers_url":"https://api.github.com/users/cos/followers","following_url":"https://api.github.com/users/cos/following{/other_user}","gists_url":"https://api.github.com/users/cos/gists{/gist_id}","starred_url":"https://api.github.com/users/cos/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cos/subscriptions","organizations_url":"https://api.github.com/users/cos/orgs","repos_url":"https://api.github.com/users/cos/repos","events_url":"https://api.github.com/users/cos/events{/privacy}","received_events_url":"https://api.github.com/users/cos/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/kframework/k/labels/refactoring","name":"refactoring","color":"bfe5bf"}],"state":"open","locked":false,"assignee":{"login":"cos","id":37514,"avatar_url":"https://avatars.githubusercontent.com/u/37514?v=3","gravatar_id":"","url":"https://api.github.com/users/cos","html_url":"https://github.com/cos","followers_url":"https://api.github.com/users/cos/followers","following_url":"https://api.github.com/users/cos/following{/other_user}","gists_url":"https://api.github.com/users/cos/gists{/gist_id}","starred_url":"https://api.github.com/users/cos/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cos/subscriptions","organizations_url":"https://api.github.com/users/cos/orgs","repos_url":"https://api.github.com/users/cos/repos","events_url":"https://api.github.com/users/cos/events{/privacy}","received_events_url":"https://api.github.com/users/cos/received_events","type":"User","site_admin":false},"milestone":null,"comments":2,"created_at":"2015-12-12T15:56:15Z","updated_at":"2015-12-15T19:19:37Z","closed_at":null,"body":"Right now, in KORE, we define new sorts by either a `Production` or a `SyntaxSort`. `SyntaxSort` can only introduce a sort, not define a subsort relation.\r\n\r\nThis is inconsistent as it is an attempt to separate sorts from productions, but at the same time using `Production` is required to encode sort-only properties like subsorting. The duality ripples into a lot ugly \"case\"-driven code.\r\n\r\nI think we ended up with this situation because subsorting and productions share the same syntax in `kore.k`. \r\n\r\nI propose to either:\r\n 1. Eliminate `SyntaxSort` all together and use a `Production` with no production items instead.\r\n 2. Add a \"supersort\" field to `SyntaxSort` such that it will encode all subsort relations. We could also enforce that all sorts descend from the some explicit top sort, i.e., `syntax Foo` becomes `syntax Foo ::= Top`. Not sure if that top sort should be `K` or a newly introduced one. Considering `K` has other implications, we might want to go for `Top`.\r\n\r\n@grosu, @radumereuta, @bmmoore, @dwightguth, what do you think?\r\n\r\nIt's not a huge deal and I won't argue strongly for it but it struck me when skimming through the code in `Module`."},"comment":{"url":"https://api.github.com/repos/kframework/k/issues/comments/164863546","html_url":"https://github.com/kframework/k/issues/1903#issuecomment-164863546","issue_url":"https://api.github.com/repos/kframework/k/issues/1903","id":164863546,"user":{"login":"bmmoore","id":698479,"avatar_url":"https://avatars.githubusercontent.com/u/698479?v=3","gravatar_id":"","url":"https://api.github.com/users/bmmoore","html_url":"https://github.com/bmmoore","followers_url":"https://api.github.com/users/bmmoore/followers","following_url":"https://api.github.com/users/bmmoore/following{/other_user}","gists_url":"https://api.github.com/users/bmmoore/gists{/gist_id}","starred_url":"https://api.github.com/users/bmmoore/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bmmoore/subscriptions","organizations_url":"https://api.github.com/users/bmmoore/orgs","repos_url":"https://api.github.com/users/bmmoore/repos","events_url":"https://api.github.com/users/bmmoore/events{/privacy}","received_events_url":"https://api.github.com/users/bmmoore/received_events","type":"User","site_admin":false},"created_at":"2015-12-15T19:19:37Z","updated_at":"2015-12-15T19:19:37Z","body":"The current role of `SyntaxSort` is for declaring sort attributes, or sometimes just to introduce sorts without giving them any content yet.\r\n\r\nI'm very much against mixing that back together with subsorting declarations. For just one complication, if there was an optional subsort field, would the attributes of the SyntaxSort switch between describing the parent sort or the subsorting relationship based on whether that subsort field is set?\r\n\r\nSplitting up Production might be reasonable, I'd have to see a bit more detailed proposal."}}