0

我在这个模块中有一个模块结构我声明了一个用于内部某些函数的变量module A。

Module A.

  Variable a : nat.   

End A.

然后我使用提取机制。

Extraction Language Ocaml.   
Set Extraction Optimize.
Set Extraction AccessOpaque.
Extraction A.

要不就

Extraction A.

它为我生成了带有警告的代码：“必须在提取的代码中实现以下公理：Aa”

type nat =
| O
| S of nat

module A = 
 struct 
  (** val a : nat **)

  let a =
    failwith "AXIOM TO BE REALIZED"
 end

在这里，我收到a了failwith "AXIOM TO BE REALIZED" 我无法成功运行我的功能，因为这个failwith

因为我必须使用a模块内部的变量。failwith我想知道有没有办法定义提取后不会生成的模块？还是与不会生成此failwith功能的提取有关？

4

1 回答 1

1

Well, at some point you'll have to provide a value for A.a. If you want to abstract A with respect to a, I guess that the most convenient way is to use a functor, which is directly translated as such in OCaml:

Module Type Param.
  Variable x: nat.
End Param.

Module A (Import P: Param).

  Definition a:=P.x.   

End A.

Extraction Language Ocaml.   
Set Extraction Optimize.
Set Extraction AccessOpaque.

Extraction "test.ml" A.

(Of course, you must instantiate the resulting OCaml functor A to run a computation).

于 2013-03-07T08:45:15.400 回答