Handle contextual functions in PushTopAmbiguityUp

[Scott-Guest]

Part of #3880

PushTopAmbiguityUp ensures that the LHS of any top-level rewrite is not an Ambiguity by pushing any such Ambiguity above the containing #RuleContent. This simplifies sort inference by making the declared sort of the LHS readily available, as needed for function, macro, etc. rules.

This PR fixes some issues in PushTopAmbiguityUp, namely

• Correctly handle contextual functions. This was partly responsible for [K-Bug] Incorrect parsing and crash with ambiguous contextual function #3880, but is not the only issue there.
• Ensure that we don't introduce nested ambiguities. I couldn't come up with a contrived enough test case to prove this is necessary, but conceptually this would be an issue if the #RuleBody is itself an Ambiguity containing a top-level rewrite whose LHS is an Ambiguity.
• General code clean-up - documentation, better naming, factoring out some duplication

[Baltoli]

Looks good!