Refactor operator applications in the parser (#3831)

Refactor operator applications in the parser (#3831)

This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes:

Indexed ops are carried in ParseOp via api::Op not Expr,
getKindForFunction is limited to "APPLY" kinds from the new API,
The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity.
TPTP should use DIVISION not DIVISION_TOTAL.
This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser.