{"action":"opened","issue":{"url":"https://api.github.com/repos/GaloisInc/cryptol/issues/360","repository_url":"https://api.github.com/repos/GaloisInc/cryptol","labels_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/360/labels{/name}","comments_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/360/comments","events_url":"https://api.github.com/repos/GaloisInc/cryptol/issues/360/events","html_url":"https://github.com/GaloisInc/cryptol/issues/360","id":169200428,"number":360,"title":"Add import with function renaming","user":{"login":"robby-phd","id":4130340,"avatar_url":"https://avatars.githubusercontent.com/u/4130340?v=3","gravatar_id":"","url":"https://api.github.com/users/robby-phd","html_url":"https://github.com/robby-phd","followers_url":"https://api.github.com/users/robby-phd/followers","following_url":"https://api.github.com/users/robby-phd/following{/other_user}","gists_url":"https://api.github.com/users/robby-phd/gists{/gist_id}","starred_url":"https://api.github.com/users/robby-phd/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/robby-phd/subscriptions","organizations_url":"https://api.github.com/users/robby-phd/orgs","repos_url":"https://api.github.com/users/robby-phd/repos","events_url":"https://api.github.com/users/robby-phd/events{/privacy}","received_events_url":"https://api.github.com/users/robby-phd/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-08-03T18:29:02Z","updated_at":"2016-08-03T18:29:02Z","closed_at":null,"body":"Cryptol currently support qualified imports to avoid function name clashes.\r\nFor example, consider AES S-Box and T-Box specifications whose top-level encryption and decryption functions are named `aesEncrypt` and `aesDecrypt`, respectively.\r\n\r\nWhen trying to prove equivalences of their specification, one can currently use Cryptol qualified imports as follows:\r\n\r\n```\r\n// import aesEncrypt and aesDecrypt in AES as qualified names AESSBox::aesEncrypt and AESSBox::aesDecrypt\r\nimport AES as AESSBox(aesEncrypt, aesDecrypt)\r\n\r\n// import aesEncrypt and aesDecrypt in AESTBox as qualified names AESTBox::aesEncrypt and AESTBox::aesDecrypt\r\nimport AESTBox as AESTBox(aesEncrypt, aesDecrypt)\r\n```\r\n\r\nAnother approach that would be nice to have is renaming the imported functions, as follows:\r\n\r\n```\r\n// import function aesEncrypt and aesDecrypt in AES as top-level functions sboxEncrypt and sboxDecrypt\r\nimport AES(aesEncrypt => sboxEncrypt, aesDecrypt => sboxDecrypt)\r\n\r\n// import function aesEncrypt and aesDecrypt in AESTBox as top-level functions tboxEncrypt and tboxDecrypt\r\nimport AESTBox(aesEncrypt => tboxEncrypt, aesDecrypt => tboxDecrypt)\r\n```\r\n\r\nThis way, one can use unqualified names to refer to the functions, which would be especially useful for long module names. \r\n"}}
{"actor":{"display_login":"robby-phd"}}