Implement \real literals (#3570); fix LogicPrinter.quickPrintSemisequent (#243)

[unp1]

Related Issue

This pull request resolves #243 and #3570.

Intended Change

#243 — LogicPrinter.quickPrintSemisequent dropped the last formula

The method printed the semisequent without an enclosing layouter block, so the
pretty-printer never flushed its final pending break and the trailing formula was lost
(e.g. true, instead of true, false). The same formulas printed via a full sequent
rendered correctly because printSequent wraps its output in beginC/end. Fixed by
wrapping the semisequent in an explicit block, mirroring quickPrintTerm.

#3570 — real literals are now supported

\real literals such as 1.0r used to be rejected by the term parser. This PR
implements them end to end.

• Exact, unbounded representation. A real is a mathematical value, so RealLiteral
  now stores it as an arbitrary-precision pair (unscaledValue, scale) with value
  unscaledValue * 10^(-scale) — the BigDecimal scheme, but with an unbounded
  BigInteger scale rather than an int, and kept in canonical form (trailing zeros
  stripped) so equal values have equal fields. BigDecimal is used only to parse bounded
  source strings, never to hold the value.
• Term encoding. The literal is encoded as __R(unscaledValue, scale) over numbers
  (realHeader.key now declares real __R(numbers, numbers); and the real sort, moved
  out of integerHeader.key). TermBuilder.rTerm / RealLDT.translateLiteral /
  translateTerm build and decode it; because both operands are unbounded numbers, the
  value never passes through an int (a scale beyond Integer.MAX_VALUE round-trips).
• Parsing. ExpressionBuilder.visitRealLiteral builds the term; a negative literal
  folds the sign into the literal (the real LDT has no neg), mirroring the existing
  integer-literal handling and using a bootstrap-safe namespace lookup.
• Pretty-printing. A new Notation.RealLiteral prints __R(u, s) back as its
  canonical decimal with an r suffix (1.25r, -0.5r, 100r), the inverse of the
  parser; registered next to Z/FP/DFP.
• Example + regression test. standard_key/reals/realLiterals.key showcases real
  literals, real-sorted quantification and a real-valued assignment (via an update); it is
  wired into runAllProofs (it proves and reloads, so the printer→parser round-trip is
  checked on every CI run).

Decisions worth highlighting

• Reserved __ name. The wrapper is named __R rather than a bare identifier so it
  does not steal a name a user might declare in a problem file. This is the first user of a
  reserved-prefix convention; migrating the other built-in literal symbols
  (Z/C/FP/DFP) out of the user namespace is left as separate follow-up work.
• Scope. The RealLDT is intentionally still a stub: there are no arithmetic axioms
  yet (no +, *, < on reals), so only equality/structural reasoning is available. The
  real type is also not yet usable inside Java program blocks (\<{ ... }\>), only in the
  logic and in JML; the example therefore models an assignment with an update. Axiomatising
  real arithmetic is a separate, larger piece of work.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s):
  • Issue243Test — red before, green after the semisequent fix.
  • RealLDTTest — the (unscaledValue, scale) encoding round-trips (incl. negatives,
    leading-zero fractions, trailing-zero integers, and a scale beyond Integer.MAX_VALUE).
  • Issue3570Test — a real literal parses to sort real, and parser and pretty-printer
    are inverse (incl. negatives and trailing-zero canonicalization).
• I have tested the feature as follows: the unit tests above, plus the full regression
  suites :key.core:testRAP -PrapForks=10 (674 — including the new reals proof, which is
  proved and reloaded) and :key.core:testProveRules (203) — all green.
• I have checked that runtime performance has not deteriorated (the added parser/printer
  branches only fire for real literals; the extra namespace lookup mirrors the existing
  integer-literal handling on the same code path).

Additional information and contact(s)

PR prepared with AI tooling support.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.