转换NAT在勒柯克提取big_int到Ocaml程序编写

Question

我做提取转换nat到big_int

当我使用的库：ExtrOcamlNatBigInt，它不big_int在Ocaml

所以我返回正确的类型修改它（文件ExtrOcamlNatBigInt），但我找不到定义函数nat_case的方式，因为在Ocaml的库文件Big_int中它们没有函数nat_case。

Extract Inductive nat => "Big_int.big_int" 
    [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "Big_int.nat_case". 

我试图通过定义一个第二个定义为nat_case：

Extract Inductive nat => "Big_int.big_int" 
    [ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "(fun fO fS n -> 
    let one = Big_int.unit_big_int in 
    if n = Big_int.zero_big_int then fO() else fS (n - one))". 

下面是使用第二个定义后的结果：

(** val nat_rect : 
    'a1 -> (Big_int.big_int -> 'a1 -> 'a1) -> Big_int.big_int -> 'a1 **) 

let rec nat_rect f f0 n = 
    let one = Big_int.unit_big_int in 
    if n = Big_int.zero_big_int then f() else f0 (n - one) 
    (fun _ -> 
    f) 
    (fun n0 -> 
    f0 n0 (nat_rect f f0 n0)) n 

我在行n得到一个错误else f0 (n - one)：

文件“Datatypes.ml”，第68行，51-52字符：错误：此表达式的类型为Big_int.big_int但预期的表达int类型的

我认为这是因为minus（-）

的

我还修改minus提取：

Extract Constant minus => "fun n m -> Big_int.max_big_int Big_int.zero_big_int 
    (Big_int.sub_big_int n m)". 

能否请你帮我来定义函数nat_case为Big_int？非常感谢你。

Answer 1

(-)保留为整数运算，不能对big_int使用相同的运算符。更换

(n - one) 

由：

Big_int.sub_big_int n one