Как можно идентифицировать неснятые конструкции Racket при использовании полного языка Rosette?

Question

Одна из самых распространенных ошибок, которые я допускаю при реализации программного синтезатора с Розетка , использует неснятые конструкции Racket небезопасным способом, который заставляет синтезатор выводить (unsat).

На самом деле, как начинающему программисту Rosette, трудно просто определить неснятые конструкции Racket, которые могут вызывать проблемы.Я думал, что DrRacket может помочь, например, не показывать стрелки от линии #lang rosette на неснятые конструкции Racket, такие как assv, но это не так, то естьон отображал стрелки как для неподнятых (например, assv), так и для поднятых операторов (например, first).

Я использовал две стратегии: (i) построение кода синтеза в rosette/safeнасколько я могу переключиться на полный язык, что неудобно, так как я не могу использовать более новые и изящные конструкции Racker и (ii) просмотреть конструкции, которые я использую в своем коде, и проверить, «предоставлены» ли они rosette/base/base.rkt, что утомительно.

Есть предложения от опытных программистов Rosette?

Answer 1

Один из подходов - начать программирование на rosette/safe, а затем при необходимости потребовать необходимые вам конструкции из Racket.Тогда, если что-то пойдет не так, будет легче выяснить, где и когда они это сделали.

Так, например, ваш код будет выглядеть примерно так:

   #lang rosette/safe

   (require (only-in racket for assv))

Как ваша кодовая базарастет, вы также можете собрать все эти импорта в один модуль, который их экспортирует.Тогда для остальной части вашего кода потребуется этот модуль, который будет действовать как пользовательская версия rosette/safe плюс минимальное количество необходимых вам конструкций Racket.