The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-11-23 14:25 GMT+01:00 Frédéric Besson <frederic.besson AT inria.fr>:

Dear all,

I would like to trace some Coq extracted code.
Something like:
Parameter Trace : nat -> unit.

Definition f (n : nat) := let _ := Trace n in n.

Extract Constant Trace => "trace_nat ».  (* Here, I will perform side-effect *)
Separate Extraction f.

I have the problem that the extraction mechanism is too clever.
It removes my call to Trace under the « false » assumption that it is side-effect free.

Is there a way to instruct the extraction not to do that ?
For instance: Hey, this is an axiom : do not assume there is no side-effect!"

It seems that disabling optimisations is not enough i.e Unset Extraction Optimize.

Does anyone know about any way?

Thanks,
—
Frédéric

​There is no side effect in Coq, assuming extraction will manage side effects is wrong.

(Think of extraction to Haskell which has no side effect, unless you do really dirty things.)

If your real code uses side effect, then you loose most of the point of having done your proofs in Coq.

Still, you are not doomed, as you can rely on some tricks, like monads (if you do not know anything about monads, you should probably read a little about them, it could be useful to solve your problem).

Declare a constant of type "state -> nat -> state", and pass sequentially all your states to your functions.

Then implement "state" with what ever you want.

Parameter state : Type.

Definition sequence := state -> state.

Parameter trace_nat : nat -> sequence.

(* print all nats from n to 0 *)

Definition count_down​ : nat -> sequence :=

  fix count_down (n : nat) : sequence :=

  match n with

  | O => trace_nat O

  | S n => fun s =>
           let s := trace_nat (S n) in
           count_down n s

  end.

​And then for you extracted code, you can do a side effect with implementing "state" with "unit",

and "trace_nat : nat -> unit -> unit" (ok there is one "unit" more) as "fun n () => print_nat n".

Of course, your "main" function will have an extra "unit" parameter.

That should solve your problem, as with that, the state must be kept and follow some path from "inputs" to "outputs".

Being abstract, the extraction cannot optimize anything on it, and must be keep the result.
This also ensure sequential execution of all your "side effect" stuff.

You can even simply not implement "state" with a side effect, but with a list of natural numbers.

Then you could run your "main" program with the empty list, and then print the whole list as result (but storing the list might take a lot of space).