ocaml - 将 Coq 提取到 Ocaml 时将 nat 转换为 big_int

Question

我正在做提取转换 nat至 big_int
当我使用图书馆时:ExtrOcamlNatBigInt ，它不会为 big_int 返回正确的类型在 Ocaml
所以我修改了它(文件 ExtrOcamlNatBigInt)，但我找不到定义函数 nat_case 的方法因为在图书馆Big_int Ocaml 他们没有功能 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