1
嗨我寫的勒柯克到ocaml的提取,我想轉換類型:我可以將Positive,Nat轉換爲int32,Z轉換爲int嗎?
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
因爲勒柯克的庫中的Z
定義(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
,這是好的,但它不是我想要的。