Parser upcases all symbols, so case-distinct function symbols collapse (e.g. T and t become the same symbol)

[moratori]

Summary

The MKBTT/TRS parser interns every symbol after applying string-upcase. As a result, function symbols that differ only in letter case (e.g. T and t) are folded into a single symbol. Inputs that rely on case to distinguish function symbols are silently mis-parsed, and completion can report a "success" for a degenerate system that is not the one given.

This is not caused by the Common Lisp reader's default case conversion; it is an explicit string-upcase call in the parser.

Facts

1. All parsed symbols (function symbols, constants, variables) are interned through a single helper that upcases the name.

src/parser.lisp:30-33

(defun %intern-symbol-to-specified-package (string)
  (intern
    (string-upcase string)
    *parsed-symbol-intern-package*))

2. The lexer itself preserves case.

The MKBTT rules lexer accepts both cases as a single token class, so the original case is present in the token string and is only lost at intern time.

src/parser.lisp:108-112 (mkbtt-rules-lexer)

("[a-zA-Z0-9_%+%*%.%-/@&\\]+" (values :rules-symbol $$))

3. The printer additionally lowercases names on output, which hides the collapse.

• src/types.lisp:179 — variable: (string-downcase (symbol-name ...))
• src/types.lisp:197-198 — fterm: 0-arity printed with string-upcase, application printed with string-downcase
• src/types.lisp:260 — predicate: (string-downcase (symbol-name ...))

So source T -> interned |T| -> printed t and source t -> interned |T| -> printed t: both render as t.

4. Empirical reproduction.

Using tests/resources/eq_systems/Sim91_sims2.trs, whose source uses 6 function symbols (T t S s R r):

(let ((eqs (clover.parser:parse-mkbtt-expression <Sim91_sims2 source>)))
  (multiple-value-bind (consts funs) (clover.multicompletion::collect-symbol eqs)
    (print funs)))                       ; => (R T S)  ;

• Collected function symbols: (R T S) — 3 instead of 6.
• The first two rules T(t(x)) -> x and t(T(x)) -> x both become the same rule t(t(x)) = x (i.e. duplicates).
• Completion then reports success with a trivial system (x) => x), which is **not** a completion of the intended Sim91_sims2`.

5. Blast radius in the bundled JAIST completion corpus.

4 of 115 files use function symbols that collide under upcasing:

File	Colliding symbols
ASK93_5.trs	A/a, E/e, H/h, Q/q, W/w
LS94_G1.trs	A/a, B/b, C/c
LS94_P1.trs	R/r, S/s, T/t
Sim91_sims2.trs	R/r, S/s, T/t

These are group/monoid presentations where the uppercaseenerator (e.g. T = t^-1); the presence of both T(t(x))-> x and t(T(x)) -> x confirms the two are intended t

Impact

• Any input that distinguishes function symbols by case is mis-parsed.
• Completion may report a spurious "success" for a collahe affected inputs are not trustworthy.

Notes / possible directions (not yet decided)

• Primary locus is the string-upcase in %intern-symbo/parser.lisp:30). Preserving case there would require acoordinated change to the printer (src/types.lisp:179,it of:
  • hardcoded literal interns such as "NIL" / "CONS" (src/parser.lisp:193,197-198,306,310-311),
  • the premise/conseq grammars where case is used at the lexer level to classify [A-Z]+ as constants vs [a-z]+ as symbols,
  • any symbol-name comparisons that assume upper case.
• Alternatively, case-insensitivity could be documented as an intentional limitation, in which case the affected inputs should be marked out of scope.
• Suggested regression tests: parse->print->parse round-trip stability, and an assertion that T and t parse to distinct symbols.

[moratori]

Case-sensitivity remediation: plan and decision points

1. Current behavior (verified facts)

Symbol interning — single choke point

All parsed symbols (function symbols, constants, variables, and a few internal sentinels) are interned through one helper that upcases the name:

;; src/parser.lisp:30-33
(defun %intern-symbol-to-specified-package (string)
  (intern (string-upcase string) *parsed-symbol-intern-package*))

• *parsed-symbol-intern-package* = "CLOVER.PARSER" (src/property.lisp:26).
• Used by every grammar action, by rename.lisp:115/136/161, and for internal sentinels in unify.lisp (e.g. :341 "DUMMYRULEOREQPAIR"). "NIL"/"CONS" list sentinels: parser.lisp:193,197-198,306,310-311. The = predicate is interned separately (types.lisp:312, non-alphabetic, unaffected).

Lexers — case is used differently per grammar

• Resolution input (premise/conseq): [A-Z]+ → :constant, [a-z0-9_...]+ → :symbol. Case is consumed at the lexer to classify constant vs symbol; a mixed/upper-case function symbol is not expressible here (src/parser.lisp:78-81, 93-96).
• MKBTT/TRS input (rules/var): [a-zA-Z0-9_...]+ is a single token class, so mixed-case and case-distinct function symbols are expressible (src/parser.lisp:105, 112). This is the only grammar where the bug has semantic impact.

Term structs — partial case awareness already exists

• vterm already stores the original string and the comment states the intent:

  ;; src/types.lisp:181,186-188
  (:constructor vterm (var &optional original-str))
  ; mkbtt形式をパースする際に、大文字小文字を区別する必要があることから 元の文字列を保持する
  (original-str "" :type string :read-only t)

  But the identity (vterm.var) is still the upcased symbol; original-str is only consulted in converter.lisp:57,66 and substitute.lisp:24. The parser does pass it: (vterm (intern…) symbol) (parser.lisp:437-439,444-445).
• fterm and constant have no original-str equivalent — function-symbol/constant case is lost entirely (types.lisp:190-218).

Printer normalizes case (masks the collapse)

• vterm → string-downcase of .var (ignores original-str) — types.lisp:179
• fterm application → string-downcase; 0-arity → string-upcase — types.lisp:197-198
• constant → string-upcase — types.lisp:212
• literal predicate → string-downcase — types.lisp:260

So source T → |T| → printed t and source t → |T| → printed t: both render as t.

Downstream that reads symbol names (correctness-neutral but order-sensitive)

• Constant sort by name: multicompletion.lisp:65 (string<).
• Canonical key sort: clover.lisp:47, canonicalization.lisp:106.
• LPO precedence compares symbol-name strings (termorder.lisp).
  These stay correct under case preservation, but sort/precedence order changes (ASCII upper < lower).

2. Remediation options

Option A — Global case-preserving intern (smallest code change)

Drop string-upcase in %intern-symbol-to-specified-pac- Fixes MKBTT (T ≠ t) and removes latent collisions (ehe internal CONS).- Affects resolution too (constant ABCvs functionaby the same symbol).- Largest test-fixture migration (see §4).

Option B — Scoped to MKBTT via a dynamic switch

Add e.g. *fold-symbol-case* bound nil only on the MKion as-is.

• Minimal behavioral blast radius; matches the original "mkbttとの差異" design note.
• Adds a stateful flag and two code paths (more complexity, must be threaded through the shared helper).

Option C — Document as a limitation (no parser change)

Keep case-insensitive parsing; mark the 4 affected corpu, LS94_P1, Sim91_sims2`) as out of scope.

• Zero implementation risk; but the tool genuinely cannot accept these systems.

3. Coordinated changes required (if Option A or B)

1. Parser intern — parser.lisp:30 (drop or conditionalize string-upcase).
2. Printer — types.lisp:179/197-198/212/260 must print symbol-name verbatim, otherwise the round-trip stays wrong on display. Decide whether vterm printing should use original-str instead of .var.
3. Variable identity — decide whether vterm.var itself becomes case-sensitive, or whether the existing original-str path is made consistent. Today it is inconsistent: core unification uses upcased .var, while converter/substitute use original-str.
4. Internal sentinels — "NIL"/"CONS"/"DUMMYRULEOREQPAIR"/"DUMMYPRED" are interned (uppercase) into the same user package CLOVER.PARSER. Under case preservation only exact-case user symbols collide (today any case collides), so risk drops — but consider moving sentinels to a private package/keyword as hardening.
5. Test fixtures — parser tests assert upcased symbols for lowercase input, e.g. (parse-premise-logical-expression "pred(x)") is compared against (vterm 'CLOVER.PARSER::X), (fterm 'CLOVER.PARSER::F …), (constant 'CLOVER.PARSER::A) (tests/src/parser.lisp:14-81). These break under case preservation and must be migrated. Golden/printed outputs (tests/src/ui/batch.lisp, rendertree) may change.

4. Decision points (what to settle before coding)

1. Scope — Option A (global) vs B (MKBTT-only) vs C
2. Variable identity — make vterm.var case-sensitive, or standardize on original-str everywhere? (Resolve the existing inconsistency either way.)
3. Print policy — verbatim symbol-name for all, and for variables .var vs original-str; accept golden-output changes.
4. Sentinel namespace — keep NIL/CONS/DUMMY* in `Cm to avoid sharing the user namespace.
5. Resolution grammar — keep the [A-Z]+ = constantll-upper, function symbols all-lower); confirm nothingrelies on a constant and a like-named function symbol be
6. Ordering dependence — confirm no test/logic depent/precedence order (LPO precedence, constant sort,canonical-key sort).
7. Backward compatibility / migration — accept that existing inputs and fixtures assuming case-insensitivity change; plan the fixture migration and add regression tests:
   • parse → print → parse round-trip stability,
   • an assertion that T and t parse to distinct function symbols,
   • re-run the affected corpus (ASK93_5, LS94_G1, LS94_P1, Sim91_sims2) and re-interpret their completion results.

5. Recommendation (inference, medium confidence)

• If the goal is "accept these group/monoid systems correctly with least disturbance to resolution," Option B (MKBTT-scoped) aligns with the original design intent (the [A-Z]+=constant rule is a deliberate resolution-only convention) and keeps the resolution fixtures untouched.
• If a single, consistent case-sensitive model is preferred and a one-time fixture migration is acceptable, Option A is cleaner and also eliminates the latent cons/CONS-style collisions.
• In both cases, the printer must change together with the parser, and the variable identity inconsistency (.var vs original-str) should be resolved as part of the work, not left half-done.