{"action":"closed","issue":{"url":"https://api.github.com/repos/Deducteam/Dedukti/issues/22","repository_url":"https://api.github.com/repos/Deducteam/Dedukti","labels_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/22/labels{/name}","comments_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/22/comments","events_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/22/events","html_url":"https://github.com/Deducteam/Dedukti/issues/22","id":291313212,"node_id":"MDU6SXNzdWUyOTEzMTMyMTI=","number":22,"title":"Bracket checking too restrictive and obscure","user":{"login":"Gaspi","id":3737683,"node_id":"MDQ6VXNlcjM3Mzc2ODM=","avatar_url":"https://avatars0.githubusercontent.com/u/3737683?v=4","gravatar_id":"","url":"https://api.github.com/users/Gaspi","html_url":"https://github.com/Gaspi","followers_url":"https://api.github.com/users/Gaspi/followers","following_url":"https://api.github.com/users/Gaspi/following{/other_user}","gists_url":"https://api.github.com/users/Gaspi/gists{/gist_id}","starred_url":"https://api.github.com/users/Gaspi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Gaspi/subscriptions","organizations_url":"https://api.github.com/users/Gaspi/orgs","repos_url":"https://api.github.com/users/Gaspi/repos","events_url":"https://api.github.com/users/Gaspi/events{/privacy}","received_events_url":"https://api.github.com/users/Gaspi/received_events","type":"User","site_admin":false},"labels":[{"id":752482145,"node_id":"MDU6TGFiZWw3NTI0ODIxNDU=","url":"https://api.github.com/repos/Deducteam/Dedukti/labels/question","name":"question","color":"cc317c","default":true}],"state":"closed","locked":false,"assignee":{"login":"francoisthire","id":2529963,"node_id":"MDQ6VXNlcjI1Mjk5NjM=","avatar_url":"https://avatars1.githubusercontent.com/u/2529963?v=4","gravatar_id":"","url":"https://api.github.com/users/francoisthire","html_url":"https://github.com/francoisthire","followers_url":"https://api.github.com/users/francoisthire/followers","following_url":"https://api.github.com/users/francoisthire/following{/other_user}","gists_url":"https://api.github.com/users/francoisthire/gists{/gist_id}","starred_url":"https://api.github.com/users/francoisthire/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/francoisthire/subscriptions","organizations_url":"https://api.github.com/users/francoisthire/orgs","repos_url":"https://api.github.com/users/francoisthire/repos","events_url":"https://api.github.com/users/francoisthire/events{/privacy}","received_events_url":"https://api.github.com/users/francoisthire/received_events","type":"User","site_admin":false},"assignees":[{"login":"francoisthire","id":2529963,"node_id":"MDQ6VXNlcjI1Mjk5NjM=","avatar_url":"https://avatars1.githubusercontent.com/u/2529963?v=4","gravatar_id":"","url":"https://api.github.com/users/francoisthire","html_url":"https://github.com/francoisthire","followers_url":"https://api.github.com/users/francoisthire/followers","following_url":"https://api.github.com/users/francoisthire/following{/other_user}","gists_url":"https://api.github.com/users/francoisthire/gists{/gist_id}","starred_url":"https://api.github.com/users/francoisthire/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/francoisthire/subscriptions","organizations_url":"https://api.github.com/users/francoisthire/orgs","repos_url":"https://api.github.com/users/francoisthire/repos","events_url":"https://api.github.com/users/francoisthire/events{/privacy}","received_events_url":"https://api.github.com/users/francoisthire/received_events","type":"User","site_admin":false},{"login":"Gaspi","id":3737683,"node_id":"MDQ6VXNlcjM3Mzc2ODM=","avatar_url":"https://avatars0.githubusercontent.com/u/3737683?v=4","gravatar_id":"","url":"https://api.github.com/users/Gaspi","html_url":"https://github.com/Gaspi","followers_url":"https://api.github.com/users/Gaspi/followers","following_url":"https://api.github.com/users/Gaspi/following{/other_user}","gists_url":"https://api.github.com/users/Gaspi/gists{/gist_id}","starred_url":"https://api.github.com/users/Gaspi/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Gaspi/subscriptions","organizations_url":"https://api.github.com/users/Gaspi/orgs","repos_url":"https://api.github.com/users/Gaspi/repos","events_url":"https://api.github.com/users/Gaspi/events{/privacy}","received_events_url":"https://api.github.com/users/Gaspi/received_events","type":"User","site_admin":false},{"login":"GuillaumeGen","id":13106909,"node_id":"MDQ6VXNlcjEzMTA2OTA5","avatar_url":"https://avatars1.githubusercontent.com/u/13106909?v=4","gravatar_id":"","url":"https://api.github.com/users/GuillaumeGen","html_url":"https://github.com/GuillaumeGen","followers_url":"https://api.github.com/users/GuillaumeGen/followers","following_url":"https://api.github.com/users/GuillaumeGen/following{/other_user}","gists_url":"https://api.github.com/users/GuillaumeGen/gists{/gist_id}","starred_url":"https://api.github.com/users/GuillaumeGen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/GuillaumeGen/subscriptions","organizations_url":"https://api.github.com/users/GuillaumeGen/orgs","repos_url":"https://api.github.com/users/GuillaumeGen/repos","events_url":"https://api.github.com/users/GuillaumeGen/events{/privacy}","received_events_url":"https://api.github.com/users/GuillaumeGen/received_events","type":"User","site_admin":false}],"milestone":null,"comments":5,"created_at":"2018-01-24T18:29:50Z","updated_at":"2018-08-27T09:59:23Z","closed_at":"2018-08-27T09:59:23Z","author_association":"MEMBER","body":"Brackets are replaced with fresh unapplied \"a la Miller\" variables together with the promise of a systematic conversion check before the rule is fired.\r\n\r\nFor instance the rule\r\n```[s1, s2, a, b] Term {rule s1 s2} (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).```\r\nis interpreted as \r\n```[?_1, s1, s2, a, b] Term ?_1 (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).```\r\ntogether with the promise that the rule is only applied when `?_1` is convertible with `rule s1 s2`.\r\n\r\nA couple of sanity checks are performed when type checking the rule:\r\n- The bracketed term should not use the locally bounded variables since it corresponds to *unapplied* variable from the context.\r\n- Same for its type.\r\n- The type inferred for the fresh variable in place of the bracket cannot depend on context variable occurring after the bracket. It seems reasonable to expect the bracketed term to have a type respecting this property as well.\r\n\r\n(Potential) issues:\r\n- For now the checks seem too restrictive. The term in brackets cannot depend on context variable declared after it in the rule context. Is there a reason for that ?\r\n- Are the checks necessary ? Do we fail later on anyway if they are omitted ?\r\n- Error messages could be more explicit. Make the distinction between all three reasons to fail.\r\n- Should we fail or simply warn the user ? It could be that the user somehow \"knows better\" and indeed expects a term depending variables it's not supposed to."}}
{"actor":{"display_login":"francoisthire"}}