Четыре поверхности записи

Одну программу flang можно записать четырьмя наборами слов: русским, английским, эсперанто и китайским. Это не четыре языка и не перевод. если, if, se и 如果 — одно и то же слово языка, записанное четырьмя способами, и разбор даёт одно дерево.

Отсюда следует практический вопрос, ради которого стоит читать дальше: на какой из четырёх вам можно писать? Ответ короткий и неудобный, поэтому он стоит здесь, а не в конце.

Писать можно на четырёх. Доказывать — на двух

\* Китайская программа печатается в python, java, csharp и elixir. Цели c, cpp, go, js, ts и rust её пока отказываются печатать: иероглифические имена у них схлопываются в одно слово, и печать отказывает столкновением имён. Разбор ниже — «Печать и имена».

Второй строкой всё и сказано. Язык продаёт доказуемость; словаря доказательств на эсперанто и китайском нет, и написать требует, обеспечивает, убывает или индукция по на них не на чем. Программа на китайском проверится и запустится; доказать о ней что-нибудь вы не сможете.

Поэтому дерево и написано на двух поверхностях из четырёх, а не на четырёх: эсперанто и китайский существуют в таблице целиком, но пользоваться ими всерьёз пока нельзя — на них в дереве написаны только две демонстрационные программы, и лежат они в docs/examples/surfaces/.

Полная таблица слов — на странице Словарь языка; она печатается из той же единственной таблицы, по которой разбирается любой файл, и пустая клетка в ней значит, что слова нет.

Что именно молчит

Четырнадцать понятий на двух поверхностях — это всё доказательства

Самое важное здесь не число, а то, ЧТО именно молчит. Все четырнадцать понятий, открытых только на русской и английской поверхностях, — словарь доказательств и завершаемости:

Причина названа в самой таблице: у этих понятий нет устоявшегося слова ни в эсперанто, ни в китайском, а requires и ensures стоят парой в Eiffel, JML и Dafny. Придуманное слово хуже отсутствующего: сказать, что китайское доказательство пишется наполовину по-английски, — значит соврать дважды.

Печать и имена

Пустая клетка словаря видна в таблице. Печать в чужой язык упирается в другое — в то, как имя функции превращается в идентификатор цели.

Печать режет имя по «словарным символам» и всё прочее считает разделителем. Для знаков препинания это верно: длинное тире в имени в идентификатор попасть не должно. Цели python, java, csharp и elixir словарными считают и буквы всех четырёх поверхностей, поэтому имена печатаются как есть:

Цели c, cpp, go, js, ts и rust режут имя по латинице и цифрам. У иероглифического имени словарных символов не остаётся вовсе, все имена схлопываются в одно слово, и печать честно отказывает по столкновению, а не печатает разные функции под одним именем:

$ flang emit docs/examples/surfaces/factorial.zh.flang --target js --out …
flang emit: печать отказала — имена «乘积» и «前置» дают один идентификатор «value» — переименуйте одно из них в модели

Дело не в самом языке C: fn_乘积 собирается и работает и там — cc -std=c99 -Wall -Wextra -Werror -pedantic не говорит ни слова.

Отказ остаётся там, где имя действительно не выводится. Знаки препинания — разделители, имя из одного препинания даёт value, а столкновение имён — отказ, а не молчаливое переименование.

Семь понятий на трёх поверхностях

Одно понятие на одной поверхности

alias — русское это («список чисел» это …). Английского, эсперантского и китайского слова у него нет вовсе: это единственное понятие таблицы, доступное только на русской поверхности.

Счёт целиком

По поверхностям: русская — 158 понятий из 158, английская — 157, китайская — 142, эсперанто — 137. Всего фраз в таблице 661: у понятия слов бывает несколько (равен, равна, равно).

Одна строка, четыре записи

если н не больше 1     то 1  иначе н умножить на («Факториал» от (н минус 1))
if n is at most 1      then 1  else n times («Factorial» of (n minus 1))
se n ne pli granda ol 1  tiam 1  alie n fojoj («Faktorialo» de (n minus 1))
如果 n 不大于 1          那么 1  否则 n 乘以 （«阶乘» 的 （n 减 1））

Это четыре строки из четырёх файлов дерева, а не выдумка страницы: docs/examples/rosetta/factorial.flang, docs/examples/rosetta/factorial-english.flang, docs/examples/surfaces/factorial.eo.flang, docs/examples/surfaces/factorial.zh.flang. Каждый проходит проверку сам по себе — одной и той же командой, меняется только имя файла:

flang check docs/examples/rosetta/factorial.flang
flang check docs/examples/surfaces/factorial.zh.flang

Все четыре отвечают одинаково: «функций 5, из них с доказанным завершением 3; типов 0» и «замечаний нет».

Имена МОДУЛЕЙ у всех четырёх латинские — «Factorial», «Factorial», «Faktorialo», «Factorial zh», — и это правило Р7 (имена в коде): имя модуля становится именем напечатанного файла, а от кириллического имени выходил бы транслит, от иероглифического — пустое слово value; ни то, ни другое не читается. Поверхность выбирается ключевыми словами и именами функций, а не именем модуля: в русском файле стоит «Факториал» от (н минус 1).

Насколько «одно дерево» — правда

Утверждение «разбор даёт одно дерево» стоит проверить, а не принять на слово, — и в сыром виде оно неверно.

Сырые деревья не совпадают. С русским образцом расходятся 74 слота у английской и 76 у эсперанто и китайской (bootstrap/flang run-script surfaces:run):

Все они — имена, которые выбрал автор: «Факториал», «Factorial», «Faktorialo», «阶乘». Имя — не язык. Ни один из этих слотов не разбор: ни kind, ни op, ни данные задачи. 2432902008176640000 во всех четырёх файлах написано одинаково — двадцать факториал не переводится.

Дальше два хода. Сверка: деревья сличаются с точностью до взаимно однозначного переименования — не «похоже», а биекция, отдельным словарём на каждую область видимости; всякий слот вне списка переименовываемых сверяется побуквенно. Прогон даёт: «совпали», связано имён 26 (английская) и 27 (эсперанто, китайская). Канонизация: имена заменяются порядковыми номерами по обходу дерева — и только они (вычеркнуто 24). После канонизации деревья четырёх файлов побайтово не совпадают: прогон отвечает «совпали побайтово: НЕТ». Сверка с биекцией при этом проходит; что именно расходится после канонизации, прогон не называет, и утверждение «совпадают байт в байт» страница не держит, пока этот прогон не позеленеет.

Стоит понимать, чего это НЕ доказывает. Поверхности — одна таблица слов в лексере, и разборщик не знает, каким словом набрано ключевое понятие; совпадение деревьев тут следует из устройства, а не открывается прогоном. Прогон нужен ради второй половины утверждения — что расходятся только имена автора и больше ничего. Вот её и стоит перепроверять.

Как это устроено

Таблица одна: понятие → слова на четырёх поверхностях. Она лежит в разборе языка одной константой SURFACE_TABLE, и из неё печатается всё остальное — плоский список слов, словарь диагностик, страница Словарь языка и числа этой страницы. Второго списка нет, поэтому разъехаться нечему.

Поверхность файла определяется большинством голосов среди ключевых слов, а не первым словом: файл на эсперанто начинается с английского module, потому что эсперантского слова у этого понятия нет, и по первому слову вся диагностика файла говорила бы по-английски.

Смешение поверхностей законно ровно там, где на поверхности слова нет, — и это не поблажка, а прямое следствие честного молчания таблицы.

Перепроверить

bootstrap/flang run-script surfaces:run    перемерить
bootstrap/flang run-script surfaces:check  сверить числа этой страницы с прогоном

Эта проверка не стоит в CI, и знать об этом важнее, чем читать числа выше. Сборка сайта (node docs/site/build.mjs --check) о поверхностях не знает и остаётся зелёной, когда страница врёт; звать surfaces:check приходится руками.