2

我正在提取转换nat为big_int

当我使用库时：ExtrOcamlNatBigInt，它没有返回正确的类型big_intinOcaml

所以我修改了它（文件 ExtrOcamlNatBigInt），但我找不到定义函数的方法，nat_case因为在Big_intOcaml 的库中它们没有函数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 定义第二个定义：

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？非常感谢你。

4

1 回答 1

3

(-)保留给整数运算，您不能对 . 使用相同的运算符big_int。代替

(n - one)

经过 ：

Big_int.sub_big_int n one
于 2012-04-17T12:10:16.110 回答