{"action":"created","issue":{"url":"https://api.github.com/repos/CVC4/CVC4/issues/51","labels_url":"https://api.github.com/repos/CVC4/CVC4/issues/51/labels{/name}","comments_url":"https://api.github.com/repos/CVC4/CVC4/issues/51/comments","events_url":"https://api.github.com/repos/CVC4/CVC4/issues/51/events","html_url":"https://github.com/CVC4/CVC4/pull/51","id":40570727,"number":51,"title":"[RFC] Add adhoc polymorphism","user":{"login":"bobot","id":102849,"avatar_url":"https://avatars.githubusercontent.com/u/102849?v=3","gravatar_id":"","url":"https://api.github.com/users/bobot","html_url":"https://github.com/bobot","followers_url":"https://api.github.com/users/bobot/followers","following_url":"https://api.github.com/users/bobot/following{/other_user}","gists_url":"https://api.github.com/users/bobot/gists{/gist_id}","starred_url":"https://api.github.com/users/bobot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bobot/subscriptions","organizations_url":"https://api.github.com/users/bobot/orgs","repos_url":"https://api.github.com/users/bobot/repos","events_url":"https://api.github.com/users/bobot/events{/privacy}","received_events_url":"https://api.github.com/users/bobot/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":19,"created_at":"2014-08-19T09:00:50Z","updated_at":"2015-04-28T07:36:23Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/CVC4/CVC4/pulls/51","html_url":"https://github.com/CVC4/CVC4/pull/51","diff_url":"https://github.com/CVC4/CVC4/pull/51.diff","patch_url":"https://github.com/CVC4/CVC4/pull/51.patch"},"body":"This merge-request is a work in progress, used to discuss choices made in the implementation.\r\n\r\nThe basic idea is to change nothing (APPLY_UF, type-checking, ...) by working with instantiated function symbol. Global datastructures (`NodeManager::d_instanceFunction` and `NodeManager::d_parametricFunction` ) keep track of which function symbol is an instantiation of which polymorphic function. Type variable are usual type sort but registered in (`NodeManager::d_parameterVariables` for axioms, and `NodeManager::d_schemaVariables` for function schema).\r\n\r\nProgress:\r\n- [x] polymorphic function declaration parsing\r\n- [x] polymorphic axiom parsing\r\n- [ ] polymorphic function definition parsing\r\n- [x] polymorphic function application parsing (with/without as)\r\n- [x] type checking of requested polymorphic instance\r\n- [x] type checking of polymorphic application (usual application of the instantiated function)\r\n- [x] type checking of polymorphic lemmas\r\n- [x] Core infrastructure dealing with polymorphic function, function instantiations, type \"variable\".\r\n- [ ] printing of polymorphic function/axiom definition, application\r\n- [x] quantifier handling\r\n\r\nThe two first commits are fixes separately requested for merge #50.\r\n\r\n[Examples](https://github.com/bobot/CVC4/tree/feature/parametric/test/regress/regress0/parametric) of files."},"comment":{"url":"https://api.github.com/repos/CVC4/CVC4/issues/comments/96962533","html_url":"https://github.com/CVC4/CVC4/pull/51#issuecomment-96962533","issue_url":"https://api.github.com/repos/CVC4/CVC4/issues/51","id":96962533,"user":{"login":"bobot","id":102849,"avatar_url":"https://avatars.githubusercontent.com/u/102849?v=3","gravatar_id":"","url":"https://api.github.com/users/bobot","html_url":"https://github.com/bobot","followers_url":"https://api.github.com/users/bobot/followers","following_url":"https://api.github.com/users/bobot/following{/other_user}","gists_url":"https://api.github.com/users/bobot/gists{/gist_id}","starred_url":"https://api.github.com/users/bobot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bobot/subscriptions","organizations_url":"https://api.github.com/users/bobot/orgs","repos_url":"https://api.github.com/users/bobot/repos","events_url":"https://api.github.com/users/bobot/events{/privacy}","received_events_url":"https://api.github.com/users/bobot/received_events","type":"User","site_admin":false},"created_at":"2015-04-28T07:36:23Z","updated_at":"2015-04-28T07:36:23Z","body":"@danr no I don't allow `(assert (not (par (a) ...)))`, more generally (par (a) ...) can only be at toplevel. But in your case you can easily express it (if I understand correctly what you mean) by declaring an uninterpreted sort `a` and then using it in the assert without `par (a)`."}}