正、Natをint32、Zをintに抽出できますか？

Question

私は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))". 

私は（BinInt.v）コックのライブラリでZの定義のでZ -> intを保つためにそれを行うことはできません

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

私はエラーました：（関数coq_Zdouble_plus_one）

ファイル "BinInt.ml"、38行、文字4-5：

エラー：この式はint型を持っていますが、表現はしたが私はZ -> 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 

INT32タイプ に期待される、それはOKですが、それは私が欲しいものではありません。

Answer 1

Zはpositiveに内蔵されています。

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

この

は、あなたが Zを得るたび、あなたは本当に positiveといくつかの余分な情報を取得していることを意味します。

あなたが本当にZとpositiveのためのさまざまなタイプを使用する場合は、intとint32の間の変換関数を挿入する必要があります。抽出機能を使ってそのことを行うことは可能かもしれませんが、可能であっても、どうすればよいか分かりません。

Zのコード内のコードは、positiveが動作するようになります。つまり、タイプ間で絶えず変換され、タイプのいずれかの精度が失われている可能性があります。 。もし可能であれば、私は両方に同じタイプを使用したいと思います。