On Thu, Nov 14, 2024 at 10:56 PM Александр Коновалов a.v.konovalov87_AT_mail.ru <[email protected]> wrote:
> *«При выполнении линзы к термам, которые она выдаёт наружу, добавляется > информация о том, каким исходным термам они соответствуют. Достаточно при > этом аннотировать только те термы, которые отличаются от исходных.»* > > Я так понимаю, что каждая функция должна компилироваться в двух режимах: > в режиме линзы, когда она добавляет к термам аннотации, и в режиме > линзированной функции (который ещё и общий случай), когда аннотации должны > сохраняться (см. следующий абзац). Если функцию не удалось откомпилировать > в первом режиме (она не соответствует синтаксическим требованиям, > см. предыдущий абзац), то в её описателе добавляется соответствующий флаг > и попытка использовать её в роли линзы приводит к аварийному завершению > программы. > Да, так и есть. К счастью, в реальных программах необходимым условиям "линзы" будут соответствовать не так много функций. А те функции, которые случайно соответствуют, но не используются в качестве "линз", будут, скорее всего, маленькими. И поэтому особого раздувания кода не жду. On Thu, Nov 14, 2024 at 10:56 PM Александр Коновалов a.v.konovalov87_AT_mail.ru <[email protected]> wrote: > *«Надо только следить, чтобы код, порождённый компилятором для > „линзированной“ функции, не потерял аннотации термов.»* > > Собственно, вопрос в том, когда компилятор должен переносить аннотацию > с терма из образца в терм результата. > А, у вас компилятор заново строит результатное выражение, да? Т.е. если в образце -- скобки, и в результатном выражении -- скобки, то скобки в результатном выражении будут созданы заново? Тогда тяжело. В принципе, если навострить компилятор брать скобочные термы из образца и вставлять их (или их копию) в результатное выражение, то всё получится автоматически.
