и отвечу на вопрос про инлайнинг Pervasives.compare / fun (a : int) b -> . Дело в том, что в coq нет окамловского int'а. Я его и функцию сравнения ввожу аксиомами -- "Extract [Inlined] Constant" в коде. А для coq это содержимое -- просто строки, которые он копипастит в код, не долго думая. Это очень гибкое решение, хотя с очевидными недостатками. Ну и вот, где-то таки надо делать границу между coq- и ocaml-кодом. Я выбрал границу на уровне int и cmp_int. Сейчас ещё подумал и понял, что можно было бы выбрать границу на int и "<" и "=" для этих интов, которые экстрактить как "( < )" и "( == )", например. Однако сконструировать Lt/Eq/Gt несложно и не затратно, они представлены int'ами внутри, поэтому покатит и так, переписывать не буду уже, влом.
Вопрос, как эффективно отобразить из coq в ocaml тип nat в int? Я его использую, как беззнаковое целое - разрабатываю клиент для бинарного протокола. Как-то не весело видеть в выходном коде числа в единичной системе счисления - (S (S (S (S (S (S (S (S O)))))))).
Есть ли какая-нибудь литература по работе с числами в coq?
литературу не подскажу. А так -- знаю два подхода, оба кривые. 1. использовать не nat, а Z. То есть, Require Import ZArith. Open Scope Z_scope. или что-то типа того. Будет не единичная система счисления, а почти двоичная, но числа всё-таки будут записаны как значения индуктивного типа данных, ну и вся работа с ними будет тоже не самой быстрой. 2. аксиоматически определить int, указать пользовательскую экстракцию в "int", определить нужные операции и константы, а дальше, если нужно будет делать доказательства, то, видимо, работать с типом { i : int | Z_of_int i = some_Z }, где some_Z : Z, а Z_of_int -- аксиома, которую наделить свойствами однозначного отображения int -> Z, ну и другими свойствами, смотря что надо от int. Эта аксиома всё равно будет стёрта при экстракции. Но тут есть проблема в переполнении int. Её надо либо решить, либо признать, что она не важна в данном коде.
кстати, будет интересно узнать, чем закончится дело. Либо в каментах тут, либо в жаббер-конференции xmpp:ocaml@conference.jabber.ru (там coq вполне таки "в топик").
Comments 4
(The comment has been removed)
Дело в том, что в coq нет окамловского int'а. Я его и функцию сравнения ввожу аксиомами -- "Extract [Inlined] Constant" в коде. А для coq это содержимое -- просто строки, которые он копипастит в код, не долго думая. Это очень гибкое решение, хотя с очевидными недостатками. Ну и вот, где-то таки надо делать границу между coq- и ocaml-кодом. Я выбрал границу на уровне int и cmp_int. Сейчас ещё подумал и понял, что можно было бы выбрать границу на int и "<" и "=" для этих интов, которые экстрактить как "( < )" и "( == )", например. Однако сконструировать Lt/Eq/Gt несложно и не затратно, они представлены int'ами внутри, поэтому покатит и так, переписывать не буду уже, влом.
Reply
Есть ли какая-нибудь литература по работе с числами в coq?
Reply
А так -- знаю два подхода, оба кривые.
1. использовать не nat, а Z. То есть, Require Import ZArith. Open Scope Z_scope. или что-то типа того. Будет не единичная система счисления, а почти двоичная, но числа всё-таки будут записаны как значения индуктивного типа данных, ну и вся работа с ними будет тоже не самой быстрой.
2. аксиоматически определить int, указать пользовательскую экстракцию в "int", определить нужные операции и константы, а дальше, если нужно будет делать доказательства, то, видимо, работать с типом { i : int | Z_of_int i = some_Z }, где some_Z : Z, а Z_of_int -- аксиома, которую наделить свойствами однозначного отображения int -> Z, ну и другими свойствами, смотря что надо от int. Эта аксиома всё равно будет стёрта при экстракции. Но тут есть проблема в переполнении int. Её надо либо решить, либо признать, что она не важна в данном коде.
Reply
Reply
Leave a comment