[Draft] Reintegrate Framework V2 into Framework V1

[pmbittner]

This PR reintegrates all changes and additions from V2 of the framework back to V1. Apart from file movement and module renaming, notable differences are

• generalisation of function languages to allow for a parameterised expression type and output type. We need this for variability languages whose expressions and variants are parameterised in a domain. Previously, expressions and variants would have to be fixed to a domain before reusing the function language definitions. This however caused weaker forms of completeness and incompleteness, so I decided to add the domain as a type parameter to function languages. This feels a bit odd but works fine with function language. It also introduces some annoying fiddly problems with implicit parameters. Feedback welcome.
• new definitions for soundness and completeness: Both theorems are now formulated on function languages. As of now, they feel a bit clunky but its the best solution I could came up with so far that is still compatible with variability languages.
• reformulation of the old languages (CCC, BCC, OC) in terms of the new framework and constructors. Only for option calculus, we cannot reuse any variability constructors yet.