Tuples: support them on the classic clausification pathway, and fix the existing tuple machinery

[quickbeam123]

Why

TFX tuples ([$int,$int] sorts, [a,b] terms, $let([a,b] := t, ...) bindings) were reachable
only with -newcnf on: the parser rejected every tuple construct otherwise, and FOOLElimination
answered a tuple binding with NOT_IMPLEMENTED. Since newcnf is off by default, a TFX problem
using tuples died at parse time in the default strategy and in every portfolio slice that does not
turn newcnf on.

The newcnf pathway, which was supposed to be the one that works, turned out to be broken on
essentially every tuple shape that the two existing test problems do not cover. Of the 46 TPTP
problems that use tuple bindings, 20 crashed a debug build under -newcnf on --mode clausify.
Three-line inputs were enough to hit assertion violations, out-of-bounds reads and undefined
behaviour, in the kernel tuple machinery, in the parser, and in NewCNF itself.

What this PR does

Two things, in eight self-contained commits (each commit message explains its own bug and carries
the exact pre-fix reproducer):

1. Tuple $let is implemented in FOOLElimination, and the parser gate is removed, so tuples
now work on both clausification pathways. The implementation does not duplicate any let machinery:
it de-tuplifies a tuple binding into a nest of ordinary, single-symbol bindings and re-enters
process() on the result,

$let([c1,...,cn] := [s1,...,sn], t)
  ~~> $let(c1 := s1, ... $let(cn := sn, t) ... )

$let([c1,...,cn] := s, t)
  ~~> $let(g := s, $let(c1 := proj_1(g), ... $let(cn := proj_n(g), t) ... ))

where g is a fresh constant of the tuple sort and proj_i are the destructors of the tuple term
algebra (whose axioms TheoryAxioms already emits, since the algebra is registered at parse time).
Everything else — free variables, the symbol-renaming shortcut, definition introduction, Boolean
bindings — is the existing, well-exercised code path.

Two properties make this work out cleanly:

• sequentialising the simultaneous binding is sound because c1,...,cn cannot occur in s: the
  parser only publishes them once the whole definition group has been read, so a use of their name
  in s refers to a symbol of an enclosing scope. The code says so, with a pointer to the place
  in Parse/TPTP.cpp that guarantees it;
• a Boolean component needs no special case. It is a nullary predicate whose right hand side is the
  $o-sorted term proj_i(g), and process() already turns such a term into proj_i(g) = $true.
  This is precisely where NewCNF went wrong (it built a literal out of a function functor), so the
  new code avoids the bug by construction rather than by copying and patching.

g is declared over exactly the type variables of the tuple sort (none, in the monomorphic case),
so its arguments are always variables and the generic path never has to match a concrete sort.

2. The tuple machinery that both pathways share is fixed. The bugs were: a projection lookup in
Kernel/Theory that never matched a real projection while matching unrelated symbols, and then read
past the end of the destructor array; a "is this a tuple constructor?" query that extended the
signature as a side effect; a parser that decided "this is a tuple binding" from the result sort, so
an ordinary binding of a tuple-sorted symbol dereferenced a null list; a parser that could not read a
tuple binding inside a simultaneous definition group at all; and two NewCNF defects around Boolean
components and the arity of the constant naming a de-tuplified binding.

Effect

• tuple problems now parse and clausify without -newcnf on: all 45 first-order TPTP problems with
  tuple bindings clausify cleanly on the FOOLElimination pathway, none of which could previously be
  parsed at all;
• on the newcnf pathway the same corpus goes from 20 crashes to none;
• on non-tuple problems nothing changes: clausifier output is byte-identical to master on samples
  from problemsTX0.txt and problemsTX1.txt, with and without newcnf.

The two pathways produce different (though each correct) clause sets for the same tuple problem, as
they do for other FOOL constructs; no attempt is made to make them agree.

Testing

• UnitTests/tTuple.cpp — new unit test for the kernel-level tuple invariants; its cases fail
  before the corresponding commits and pass after;
• thirteen new problems in checks/theory/, covering monomorphic and polymorphic tuple bindings,
  tuple and non-tuple right hand sides, Boolean components, variable right hand sides, nesting,
  simultaneous groups, shadowing, and tuple terms outside any $let — wired into checks/sanity
  for both pathways and, where applicable, with -ile off;
• full ctest passes (100/100).

Notes for the reviewer

• checks/sanity has a pre-existing failure earlier in the script,
  Problems/DAT/DAT023_1.p with -alasca on -alascai on -thf on (assertion at
  Kernel/Inference.cpp:461), which aborts the run before it reaches the tuple section. It fails on
  master too and is untouched here; I verified the tuple and FOOL sections separately.
• Unrelated, unfixed, noticed in passing: after a TPTP USER_ERROR the input-syntax auto-detection
  falls back to SMTLIB2 and asserts in Shell/LispParser.hpp:109.
• The now-live projection lookup would have switched on $proj(i, t) printing, which TPTP cannot
  read back; that printing is removed rather than resurrected. Projections print as the ordinary
  function symbols they are.

[mezpusz]

I think this might be false. A polymorphic n-tuple has n type arguments and n term arguments, e.g. tuple_ctor2 : !>[X0 : $tType, X1 : $tType] : (X0 * X1) > tuple2(X0, X1), where tuple2 is the type constructor for 2 tuples. An example term is tuple_ctor2($int, $i, 2, f(a)) with 4 arguments.

[quickbeam123]

"The worry is dispelled — the code is right, but the reviewer was reacting to a genuinely misleading comment."

(More in a new commit, we new tests coming.)