Skip to content

Ограничения на значение в системе типов: не просто Число, а число в диапазоне #4319

Description

@nixel2007

Задача

Кроме самого типа значения, про него часто известно больше: не просто Число, а число больше нуля или в диапазоне от 0 до 5. Сейчас такое знание отбрасывается, хотя для диагностик оно ценно — индексы коллекций, деление на ноль, Найти с его -1, границы Для Сч = 1 По Н.

Вопрос задачи: принять такие ограничения в систему типов и научиться их считать.

Куда это ложится

В модели уже есть нужное разделение. TypeRef — сущность реестра: интернируется, по ней ищутся члены, отвечает на вопрос «что это за тип». TypeSet поверх набора ссылок несёт знание о значении в конкретном месте: типы элементов коллекции (Массив из СправочникСсылка.Товары) и поля «открытого» объекта (Структура с известными ключами).

Ограничение на значение — та же категория, что localFields. Поэтому ему место третьей декорацией в TypeSet:

refs:          {Число}
elementTypes:  {}
localFields:   {}
constraints:   {Число → [0..5]}      ← новое

В TypeRef класть нельзя: он интернируется и служит ключом реестра членов, а «Число больше нуля» и «Число» — один тип с одними членами.

Что уже готово принять

  • Расчёт по потоку управления (VariableFlowAnalyzer) — это и есть машинерия для такого анализа: присваивание задаёт значение, слияние путей объединяет, охраняющее условие сужает.
  • Сужение по условиям (GuardConditionNarrowing) — готовое место, куда дописывать разбор сравнений: Если Х > 0 Тогда даёт ограничение ровно там же, где сейчас ТипЗнч(Х) = Тип("...") даёт замену набора типов.
  • Операции сужения TypeSet.retaining / TypeSet.without — работают по ссылкам, ограничения поедут вместе с остающимися.

Что придётся менять принципиально

Сходимость расчёта. Набор типов конечен, поэтому объединение в точках слияния рано или поздно перестаёт расти, и предел в шестнадцать проходов — формальность. Диапазоны образуют бесконечную решётку: в цикле Счётчик = Счётчик + 1 диапазон растёт на каждой итерации и расчёт не сойдётся никогда.

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

Разбор выражений. Условия сейчас разбираются узко: ТипЗнч(Х) = Тип("...") и сравнение с Неопределено. Для ограничений нужен разбор арифметики и сравнений (Х > 0, Х <= Н, Х = Счётчик + 1) — это вычислитель, а не сопоставление с образцом.

Цена в аллокациях. TypeSet неизменяемый и создаётся в каждой точке слияния. Ещё одна карта удорожает каждое объединение — путь горячий, добавлять туда работу нужно с замером.

Предлагаемый порядок

  1. Ограничения без циклов: сходимость тривиальна, покрывает прямолинейный код и охранные проверки.
  2. Расширение для циклов — отдельно, с отдельным замером.

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

Связано с #4318 (расчёт типов по потоку управления).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions