Двоичный уже отвечает про любую свою функцию, и новую команду под это заводить не надо

Когда проверке нужен ответ не про целую программу, а про сам язык — натуральное ли имя нат, какое каноническое имя у формы length, что цель печати считает занятым, — заводить под это команду в CLI не нужно. Бинарник умеет позвать любую функцию своего замыкания по имени и вернуть значение, и умел с самого начала.

Без аргументов и без терминала на входе он работает прогонщиком: JSON на входе, JSON на выходе, по запросу на строку.

$ printf '{"fn":"Названо натуральным","args":[{"s":"нат"}]}\n' | bootstrap/flang
{"ok":true,"value":true}

fn — имя функции, args — позиционные аргументы значениями рантайма: {"n":"5"} число (строкой, чтобы не потерять −0, NaN и бесконечности), {"s":"…"} строка, {"l":[…]} список, {"r":[[ключ,значение],…]} запись, {"v":имя,"f":[…]} вариант. Одним процессом задаётся сколько угодно вопросов.

Так открыты слой типов целиком, ядро доказательства целиком и все восемь генераторов кода.

Чем подтверждено. Ветка vypusk/shest-storozhey, коммиты 6d28909c и 6cb29848. Две проверки, считавшиеся мёртвыми после удаления второй реализации на JavaScript, ожили без единой правки бинарника: замер прироста от типа вес (308 файлов, 262 функции, 2 минуты) и проверка занятых генератором имён (155 модулей, 8 целей, 3 секунды). До этого под них планировались два новых ключа CLI и две перепечатки точки раскрутки по 17 минут каждая.

Чем ограничено. Отвечают только функции, попавшие в замыкание flang/self/bootstrap/compiler.flang. Проверяется это тем же запросом с пустым списком аргументов: ответ FLANG_TYPE («принимает N аргум., получено 0») означает «функция есть», FLANG_UNKNOWN_NAME — «в замыкание не втащена». Так измерено, что «Проверить факты» и «Проверить доказательства» есть, а «Поиск на сетке», «Таблица вызовов категорий», «Таблица ответов множеств», «Таблица вызовов функтора» — нет.

Второе ограничение — цена. Один процесс стоит около семи миллисекунд, поэтому вопросы надо задавать пачкой и помнить ответы: каноническое имя формы ядро доказательства спрашивает десятки тысяч раз, а разных имён у него меньше полусотни. Мост с памятью написан один раз — спросить и спроситьПачкой в flang/scripts/binary.mjs.

Третье: аргумент, который сам является разобранной программой, кодировать в этот вид дорого — дерево большого модуля это десятки тысяч узлов, и посылать его заново на каждый вопрос дороже, чем стоит весь замер. Для таких вопросов ключ у команды всё-таки нужен.

Связано: a-hand-written-list-outlives-the-tree, the-binary-is-silent-about-checks-it-does-not-have, a-test-check-revives-by-running-the-binary-not-by-a-second-parser