Extraction mechanism of Coq generate "failwith "AXIOM TO BE REALIZE""

Question

I have a module structure inside this module I declare a variable use for some function inside module A.

Module A.

  Variable a : nat.   

End A.

Then I use extraction mechanism.

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

or just

Extraction A.

It generated for me the code with a warning: "The following axiom must be realized in the extracted code: A.a"

type nat =
| O
| S of nat

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

  let a =
    failwith "AXIOM TO BE REALIZED"
 end

Here I received a with the failwith "AXIOM TO BE REALIZED" I couldn't run my function success because of this failwith

Because I have to use the variable a inside the module. I want to know is there a way to define a module that it won't generate failwith after the extraction? or something to do with the extraction that will not generate this failwith function?

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