轉換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