CVC4/CVC4 — pull request #51 by bobot (2014-08-19 09:00:50+00:00)
Title: [RFC] Add adhoc polymorphism

This merge-request is a work in progress, used to discuss choices made in the implementation.

The 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).

Progress:
- [x] polymorphic function declaration parsing
- [ ] polymorphic axiom parsing
- [ ] polymorphic function definition parsing
- [x] polymorphic function application parsing (with/without as)
- [ ] type checking of requested polymorphic instance
- [x] type checking of polymorphic application (usual application of the instantiated function)
- [ ] type checking of polymorphic lemmas
- [x] Core infrastructure dealing with polymorphic function, function instantiations, type "variable".
- [ ] printing of polymorphic function/axiom definition, application
- [ ] quantifier handling

The two first commits are fixes separately requested for merge.

[Examples](https://github.com/bobot/CVC4/tree/feature/parametric/test/regress/regress0/parametric) of files.