{"action":"created","issue":{"url":"https://api.github.com/repos/colis-anr/colis-language/issues/25","repository_url":"https://api.github.com/repos/colis-anr/colis-language","labels_url":"https://api.github.com/repos/colis-anr/colis-language/issues/25/labels{/name}","comments_url":"https://api.github.com/repos/colis-anr/colis-language/issues/25/comments","events_url":"https://api.github.com/repos/colis-anr/colis-language/issues/25/events","html_url":"https://github.com/colis-anr/colis-language/issues/25","id":368136941,"node_id":"MDU6SXNzdWUzNjgxMzY5NDE=","number":25,"title":"Seperate return code and behaviour in concrete semantics?","user":{"login":"benozol","id":197499,"node_id":"MDQ6VXNlcjE5NzQ5OQ==","avatar_url":"https://avatars1.githubusercontent.com/u/197499?v=4","gravatar_id":"","url":"https://api.github.com/users/benozol","html_url":"https://github.com/benozol","followers_url":"https://api.github.com/users/benozol/followers","following_url":"https://api.github.com/users/benozol/following{/other_user}","gists_url":"https://api.github.com/users/benozol/gists{/gist_id}","starred_url":"https://api.github.com/users/benozol/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/benozol/subscriptions","organizations_url":"https://api.github.com/users/benozol/orgs","repos_url":"https://api.github.com/users/benozol/repos","events_url":"https://api.github.com/users/benozol/events{/privacy}","received_events_url":"https://api.github.com/users/benozol/received_events","type":"User","site_admin":false},"labels":[{"id":1061216376,"node_id":"MDU6TGFiZWwxMDYxMjE2Mzc2","url":"https://api.github.com/repos/colis-anr/colis-language/labels/question","name":"question","color":"d876e3","default":true}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-10-09T10:11:49Z","updated_at":"2018-10-11T10:19:02Z","closed_at":"2018-10-11T08:20:42Z","author_association":"CONTRIBUTOR","body":"Currently, the return code and behaviour in the concrete semantics are kept together by a `type behaviour = BNormal bool | BExit bool`), just like in @Niols' previous version.\r\n\r\nIn the concrete interpreter, however, return code and behaviour are separated: the return code is a mutable field in the state and the behaviour is reflected by the OCaml behaviour (normal value or raised exception).\r\n\r\nI am wondering if this separation is actually closer to *The Truth* and should also be reflected in the inductive specification by putting the return code in the `context` (and removing `previous_result` from `input`). It may even simplify the proofs. WDYT? Did you already try that?"},"comment":{"url":"https://api.github.com/repos/colis-anr/colis-language/issues/comments/428901990","html_url":"https://github.com/colis-anr/colis-language/issues/25#issuecomment-428901990","issue_url":"https://api.github.com/repos/colis-anr/colis-language/issues/25","id":428901990,"node_id":"MDEyOklzc3VlQ29tbWVudDQyODkwMTk5MA==","user":{"login":"benozol","id":197499,"node_id":"MDQ6VXNlcjE5NzQ5OQ==","avatar_url":"https://avatars1.githubusercontent.com/u/197499?v=4","gravatar_id":"","url":"https://api.github.com/users/benozol","html_url":"https://github.com/benozol","followers_url":"https://api.github.com/users/benozol/followers","following_url":"https://api.github.com/users/benozol/following{/other_user}","gists_url":"https://api.github.com/users/benozol/gists{/gist_id}","starred_url":"https://api.github.com/users/benozol/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/benozol/subscriptions","organizations_url":"https://api.github.com/users/benozol/orgs","repos_url":"https://api.github.com/users/benozol/repos","events_url":"https://api.github.com/users/benozol/events{/privacy}","received_events_url":"https://api.github.com/users/benozol/received_events","type":"User","site_admin":false},"created_at":"2018-10-11T10:19:02Z","updated_at":"2018-10-11T10:19:02Z","author_association":"CONTRIBUTOR","body":"I was thinking about something like the following:\r\n```mlw\r\ntype input = { …; (* remove previous_result *) }\r\ntype context = { …; result: bool }\r\ntype behaviour = BNormal | BExit\r\ninductive eval_instruction input context state instruction state context behaviour\r\n```\r\nFor any `eval_instruction inp ctx sta ins sta' ctx' b`, the previous return code is `ctx.result` and the return code of the evaluation of `ins` is `ctx'.result`.\r\n\r\nThis corresponds closer to the signature of the interpreter where `state` and `context` are mixed in a (mutable) `Interpreter.state` and the behaviour is reflected by the OCaml behaviour. But I am really no sure if this solves any problem."}}
{"actor":{"display_login":"benozol"}}