{"action":"opened","issue":{"url":"https://api.github.com/repos/kframework/kore/issues/94","repository_url":"https://api.github.com/repos/kframework/kore","labels_url":"https://api.github.com/repos/kframework/kore/issues/94/labels{/name}","comments_url":"https://api.github.com/repos/kframework/kore/issues/94/comments","events_url":"https://api.github.com/repos/kframework/kore/issues/94/events","html_url":"https://github.com/kframework/kore/issues/94","id":318724073,"number":94,"title":"Missing location information from error when unexpected sort","user":{"login":"radumereuta","id":5113255,"avatar_url":"https://avatars1.githubusercontent.com/u/5113255?v=4","gravatar_id":"","url":"https://api.github.com/users/radumereuta","html_url":"https://github.com/radumereuta","followers_url":"https://api.github.com/users/radumereuta/followers","following_url":"https://api.github.com/users/radumereuta/following{/other_user}","gists_url":"https://api.github.com/users/radumereuta/gists{/gist_id}","starred_url":"https://api.github.com/users/radumereuta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/radumereuta/subscriptions","organizations_url":"https://api.github.com/users/radumereuta/orgs","repos_url":"https://api.github.com/users/radumereuta/repos","events_url":"https://api.github.com/users/radumereuta/events{/privacy}","received_events_url":"https://api.github.com/users/radumereuta/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-04-29T15:04:09Z","updated_at":"2018-04-29T15:04:09Z","closed_at":null,"author_association":"MEMBER","body":"Input:\r\n```\r\n[]\r\nmodule TEST\r\n\r\nsort Int{} []\r\nsort String{} []\r\nsort Exp{} []\r\n\r\nsymbol inj{SIn,SOut}(SIn): SOut []\r\nsymbol info{S}(String{}, S) : S []\r\nsymbol input{}(Int{}, Int{}) : String{} []\r\n\r\naxiom{} // input: \"-1\"\r\n info{Exp{}}(input{}(\\dv{Int{}}(\"1\"),\\dv{Int{}}(\"2\")),\r\n        inj{Int{},Exp{}}(\r\n            info{Int{}}(\\and{String{}}(input{}(\\dv{Int{}}(\"1\"),\\dv{Int{}}(\"2\")),\r\n                            \\equals{String{},String{}}(input{}(\\dv{Int{}}(\"1\"),\\dv{Int{}}(\"2\")), \"-15\")),\r\n                        \\dv{Int{}}(\"-1\"))\r\n    )) []\r\nendmodule []\r\n```\r\noutput:\r\n```\r\nc:\\work\\kore\\src\\main\\haskell>stack exec -- kore-parser ..\\..\\..\\..\\test\\test2.kore\r\n\"Reading the input fileTimeSpec {sec = 0, nsec = 635559}\"\r\n\"Parsing the fileTimeSpec {sec = 0, nsec = 1488235}\"\r\n\"Verifying the definitionTimeSpec {sec = 0, nsec = 1661928}\"\r\nkore-parser.EXE: Error in module 'TEST' -> axiom declaration -> symbol or alias 'info' -> symbol or alias 'inj' -> symbol or alias 'info' -> \\and -> \\equals -> <string>: Expecting object sort 'String{}' but got meta sort '#CharList{}'.\r\nCallStack (from HasCallStack):\r\n  error, called at app\\parser\\Main.hs:90:49 in main:Main\r\n```\r\nThe problem: `\"-15\"` was supposed to be `\\dv{Int{}}(\"-15\")`, but I had to find out by removing parts of the term and trying to parse.\r\nThis example can be minimized further, but I chose to leave it like this so it becomes more clear why we need location information everywhere.\r\n\r\nVersion used: 0e9818a (latest master)"}}
{"actor":{"display_login":"radumereuta"}}