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
,这是好的,但它不是我想要的。