flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Форма, которую разбор уже отвергает, — самое дешёвое место для нового синтаксиса, и цена измерена

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

Что именно занято.

дыраотказ ДОчем занято
проверки варианта выражением нетFLANG_PARSE: ожидался знак ')'<выражение> это вариант «Имя»это уже ключевое (тип «Х» это …), вариант уже ключевое, сочетание в позиции выражения было ошибкой
поле суммы из выражения не достатьFLANG_TYPE: доступ к полю «ключ» требует записи, а не «Связь»та же запись значение.поле, разрешённая у суммы из одного варианта — разбор её брал всегда, отвергала проверка типов
дано число: число не вводит переменнуюFLANG_UNKNOWN_NAME: имя «число» не связанота же запись, признак прежний (двоеточие вторым токеном), расширен только вопрос о первом

Занятость проверяется прогоном, а не глазами. ./ярлык слово:занятость это → голых вхождений в корпусе из 374 файлов 0; в ёлочках 9, в строках 80, в комментариях 1941 — эти безопасны, закавыченное имя ключевым словом не станет никогда. grep тут врёт в большую сторону, потому что считает как раз их.

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

И третья такая же дешёвая, потому что новый узел не заводился вовсе. итог это вариант «Успех» разбирается в обычный разбор с двумя ветвями: названный вариант даёт да, любоенет. Ни типизатор, ни вычислитель, ни восемь генераторов кода не узнают, что появилась новая запись, — они видят узел match, который читают с первого дня. Проверка исчерпывающести, разбор образцов и печать наследуются целиком, а не пишутся второй раз рядом.

Чем подтверждено. Ветка vypusk/vyrazimost, коммит fa953d69 и далее. flang/test/vyrazimost.test.mjs — 16 утверждений; снятие любой из шести правок красит от одного до пяти из них. Мера замера двадцати (benchmarks/proof-cost/schyot-20.mjs): содержательных утверждений было 2 из 20, стало 5 из 20.

Чем ограничено. Приём кончается там, где нужного отвергаемого места нет. Четвёртая дыра — равенства на параметре типа — им не закрывается: результат равен запасное отвергается не разбором и не одним правилом типа, а тем, что понятия «какие типы сравнимы и чем» в языке нет вовсе. Это не занятие свободной формы, а новое понятие в системе типов, и решает его владелец языка.

Связано: unstatable-costs-more-than-unprovable, tautologies-close-for-free, a-language-form-must-reach-code-generation