Я пытаюсь извлечь в Haskell программу на Coq, которая использует Z числа. Я хочу отобразить Coq's Z на целое число Хаскелла.
Я нашел несколько библиотек для того, чтобы нацеливать OCaml, но не на Хаскелл
Для этого нет библиотеки?
Мне нужны извлечения (найдено здесь ):
Extract Inductive positive => "Big.big_int"
[ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case".
Extract Inductive Z => "Big.big_int"
[ "Big.zero" "" "Big.opp" ] "Big.z_case".
Extract Inductive N => "Big.big_int"
[ "Big.zero" "" ] "Big.n_case".
но целится в Хаскелл.
Я просто спрошу: как это сделать?
Но во-вторых, я должен сказать, почему я не мог сделать это сам:
Полагаю, я не могу придумать это сам, возможно, потому, что неправильно что-то понимаю, например: почему во втором определении есть пустая строка? Определение Z имеет три конструктора: Z0, Zpos и Zneg. Я не вижу, как "Big.zero" "" "Big.opp" связано с этим.
Кроме того, я не понял, как работает последняя строка: «... последняя дополнительная строка, которая указывает, как выполнить сопоставление с образцом для этого индуктивного типа». (находится в документации ).
Глава Извлечение С.Ф. говорит, что «мы даем выражение OCaml, которое можно использовать как« рекурсор »для элементов типа. (Подумайте, церковные цифры.)».
Как приведенный ниже код является рекурсором или обрабатывает шаблоны?
"(fun zero succ n →
if n=0 then zero () else succ (n-1))".
После того, как я пойму эти вещи, я надеюсь, что смогу сам создать извлечения, которые мне могут понадобиться.