1

嗨，我正在编写从 Coq 到 Ocaml 的提取，我想转换类型：

positive --> int32
N -> int32

但我想保留类型Z是int

这是我为提取这些条件所做的代码：

Require Import ZArith NArith.
Require Import ExtrOcamlBasic.

(* Mapping of [positive], [N], [Z] into [int32]. *)
Extract Inductive positive => int32
[ "(fun p-> let two = Int32.add Int32.one Int32.one in
    Int32.add Int32.one (Int32.mul two p))"
  "(fun p->
    let two = Int32.add Int32.one Int32.one in Int32.mul two p)" "Int32.one" ]
  "(fun f2p1 f2p f1 p -> let two = Int32.add Int32.one Int32.one in
    if p <= Int32.one then f1 () else if Int32.rem p two = Int32.zero then
    f2p (Int32.div p two) else f2p1 (Int32.div p two))".

Extract Inductive N => int32 [ "Int32.zero" "" ]
"(fun f0 fp n -> if n=Int32.zero then f0 () else fp n)".

Extract Inductive Z => int [ "0" "" "(~-)" ]
"(fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))".

我无法保留它，Z -> int因为ZCoq 库 ( BinInt.v )中的定义

Inductive Z : Set :=
  | Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

我收到一个错误：（函数 coq_Zdouble_plus_one）

文件“BinInt.ml”，第 38 行，字符 4-5：

错误：此表达式的类型为 int，但预期的表达式为 int32 类型

BinInt.ml

open BinPos
open Datatypes

(** val coq_Z_rect :
    'a1 -> (int32 -> 'a1) -> (int32 -> 'a1) -> int -> 'a1 **)

let coq_Z_rect f f0 f1 z =
  (fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))
    (fun _ ->
    f)
    (fun x ->
    f0 x)
    (fun x ->
    f1 x)
    z

(** val coq_Z_rec : 'a1 -> (int32 -> 'a1) -> (int32 -> 'a1) -> int -> 'a1 **)

let coq_Z_rec f f0 f1 z =
  (fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))
    (fun _ ->
    f)
    (fun x ->
    f0 x)
    (fun x ->
    f1 x)
    z

(** val coq_Zdouble_plus_one : int -> int **)

let coq_Zdouble_plus_one x =
  (fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))
    (fun _ ->
    Int32.one)
    (fun p ->
    ((fun p-> let two = Int32.add Int32.one Int32.one in
    Int32.add Int32.one (Int32.mul two p))
    p))
    (fun p -> (~-)
    (coq_Pdouble_minus_one p))
    x

如果我提取Z -> int32，没关系，但这不是我想要的。

4

1 回答 1

1

你的问题是Z内部建立在positive.

Inductive Z : Set := Z0 : Z
                   | Zpos : positive -> Z
                   | Zneg : positive -> Z
                   .

这意味着每当你得到 a 时Z，你真的得到 apositive和一些额外的信息。

如果你真的想为Zand使用不同的类型positive，你必须在intand之间插入转换函数int32。您也许可以使用提取功能来做到这一点，但我不确定如何——或者即使——这是可能的。

我看到的另一个问题是 s 上的匹配项中的代码Z可以使用positives ，这意味着您将不断地在类型之间进行转换，并失去其中一种类型可能比另一种类型具有的任何额外精度。如果可能的话，我会为两者使用相同的类型。

于 2012-05-03T14:23:15.377 回答