calculus annotations: check proc calls

[Philipp15b]

According to the documentation, calculus annotations do not check that proc calls are sound: they do not check that a proc only calls procs (and vice versa for coprocs), and neither do they check that the callee's calculus corresponds to the caller's calculus. Warnings/errors for these should be added.