Syntax for backend types

[marcoeilers]

This PR adds syntax for domain types and domain functions that have interpretations given by the backend.
This functionality used to be available in the AST only.

Syntax example (as discussed in a previous Viper meeting):

domain myBV interpretation (SMTLIB: "(_ BitVec 32)", Boogie: "bv32") {

  function toBV32(i: Int): myBV interpretation "(_ int2bv 32)"
}

Consistency checks ensure that the given input program has interpretations for the current backend.

This domain type and function can be used like any other type and function, but will be interpreted to be the respective SMTLIB/Boogie type by Silicon and Carbon, respectively.
Frontends using the existing BackendFunction AST nodes will have to be adapted slightly (in particular, the declarations of those functions now have to be added to the program using domains, which was not the case before), but there are some constructors and deconstructors to keep existing code working where possible.

Accompanying PRs will modify Silicon and Carbon accordingly.

[marcoeilers]

Silicon PR 675 and Carbon PR 447 have to be merged before this one for tests to pass.