2

私は抽出変換natを行っていますbig_int

ライブラリを使用したとき: ExtrOcamlNatBigInt、正しい型を返しませbig_intんOcaml

nat_caseだから私はそれを修正します（ファイルExtrOcamlNatBigInt）が、Ocamlのライブラリには function がないため、関数を定義する方法が見つかり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_casebyの 2 番目の定義を定義しようとしています。

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 番目の定義を使用した後の結果を次に示します。

(** 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か? どうもありがとうございました。

4

1 に答える 1

3

(-)は整数演算用に予約されているため、同じ演算子を に使用することはできませんbig_int。交換

(n - one)

に ：

Big_int.sub_big_int n one
于 2012-04-17T12:10:16.110 に答える