変換のNATはOCamlの

Question

にコックの抽出にbig_intする

私はnat私は、ライブラリを使用

big_intに変換抽出をしています（ファイルExtrOcamlNatBigInt）を変更してください、しかし、私は関数nat_caseを定義する方法を見つけることができません。なぜなら、Ocamlのlibary Big_intには、関数nat_caseがないからです。私はラインのnでエラーが発生しました

(** 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 

：ここ

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

は、2番目の定義を使用した後の結果である：

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

は私がでnat_caseのための2番目の定義を定義しようelse f0 (n - one)：

ファイル「Datatypes.ml」、行68、文字51-52：エラー：この式はBig_int.big_int型を持つが、発現は、私はそれが理由minus（-）

のだと思います

int型で期待されていました

私もminus抽出変更：

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

あなたがBig_intのための機能nat_caseを定義するために私を助けてもらえますか？どうもありがとうございました。

Answer 1

(-)は整数演算に予約されていますので、big_intには同じ演算子を使用できません。

Big_int.sub_big_int n one