Proper formatting of placeholders in TPTP

[ZachJHansen]

Placeholders are syntactically indistinguishable from symbolic constants, but semantically they behave like free variables. Since TPTP requires type-casting for comparisons, e.g.

$lesseq(a, n)

is forbidden if a is a function constant but n is an integer placeholder, this makes formatting them correctly in TPTP very inconvenient. Currently using a temporary rename-and-replace strategy with regexes as a post-processing step in zach/dev.

One option is to make placeholders part of the fol AST: general-sorted placeholders are treated similarly to symbolic constants and integer-sorted placeholders are treated similarly to integer terms. So, rather than replacing them with variables of the appropriate sort, we could replace them with zero-arity functions of the appropriate sort.

Ultimately, I'm not sure there is a perfect way to do this. Parsing and formatting should be context-independent, but the presence of a user guide affects whether n is treated as a symbolic constant, a free-valued integer function, or a free valued general function.

[teiesti]

FunctionConstants have been added to the FOL syntax tree in #78. All what is missing to resolve this issue is replacing symbolic constants in formulas corresponding to programs with function constants when specified in the user guide.