Извлечение программы с использованием собственных целых чисел / слов (не bignums) из теории Изабель

Question

Этот вопрос возникает в контексте, где Изабель используется для формальной разработки программного обеспечения, а не для чисто математической теории (и из контекста отдельного разработчика).

В лучшем случае программы SML, созданные на основе теории Изабель, используют SML. IntInf.int, а не собственный целочисленный тип, который Int.int; даже если Code_Target_Int, Code_Binary_Nat или же Code_Target_Nat используется. Исследование источников этих теорий, кажется, подтверждает, что это все, что он может сделать. Родные целые числа платформы могут потребоваться по нескольким причинам, включая эффективность и случай, когда императивная программа SML может быть необязательно переведена в подмножество императивного языка (например, C или Ada), что актуально, когда теория опирается на Imperative_HOL теория. codegen.pdf Документ, который поставляется с дистрибутивом Isabelle, не помог с этим, кроме как в предложении первого из вариантов ниже.

Варианты могут быть:

• Не используя Изабель int а также nat и заново создайте новый числовой тип с нуля, затем используйте code_printing команды (с его type_constructor а также constant) чтобы дать ему родное представление платформы и операции (подразумевает включение ограничений диапазона в теории): должно быть утомительно, хотя я надеюсь, что оно подвержено ошибкам из-за формальной среды. Обратите внимание, что это кажется возможным с собственной Изабель int а также nat… Это приводит к сбою генерации кода, и ничто не говорит о том, какие константы отсутствуют в code_printing команда.
• Если программа SML должна быть скомпилирована напрямую (например, с помощью MLTon), настройте среду SML с помощью замены IntInf структура: может быть небезопасной или неосуществимой, и все же требует включения ограничений диапазона в теорию, поэтому предыдущие варианты могут, наконец, быть лучше, чем этот.
• Нажмите на сгенерированную программу, чтобы изменить IntInf в Int: легко, но безопасно? (по крайней мере, IntInf реализует ту же подпись, что и Int делай, так может быть это безопасно). Как и выше, требует, чтобы в той или иной степени указывались границы теории, с этим все в порядке.
• Погружение во внутренности Изабель: безусловно, неразумно, даже хуже, чем второй вариант.
• Там существует Word теория, но, согласно некоторым прочтениям, она не подходит для этой цели.

Это другие известные варианты, не перечисленные здесь? Они комментируют перечисленные варианты?

Если нет готовых решений (я чувствую, что нет в то время), какие подсказки или треки были бы наиболее известны? (напр. ссылки на документы, упоминания понятий).

Обновить

Точки № 2 и № 3 в списке могут быть в порядке (если это действительно так), только если существует один целочисленный тип. Если в программе используется более одного, это не применимо.

Answer 1

Непосредственное создание родных слов от Изабель int будет несостоятельным, потому что ваша формализация не будет учитывать переполнение там, где оно существует в реальности.

Похоже, запись AFP Native_Word делает то, что вы хотите, хотя: http://afp.sourceforge.net/entries/Native_Word.shtml