The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

reaz wrote:
> Consider following code segment. I want to print messages in <>.
>
> Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
>   match s with
>   | Cminor.Sskip => Sskip <print "skip">
>   | Cminor.Sassign id e =>  Sassign id (sel_expr e) <print "assign">
>   | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr
> rhs) <print "store">
>   | Cminor.Scall optid sg fn args =>
>       Scall optid sg (sel_expr fn) (sel_exprlist args) <print "call">
>   | Cminor.Stailcall sg fn args => 
>       Stailcall sg (sel_expr fn) (sel_exprlist args)
>   | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
>   | Cminor.Sifthenelse e ifso ifnot =>
>       Sifthenelse (condexpr_of_expr (sel_expr e))
>                   (sel_stmt ifso) (sel_stmt ifnot)
>   | Cminor.Sloop body => Sloop (sel_stmt body)
>   | Cminor.Sblock body => Sblock (sel_stmt body)
>   | Cminor.Sexit n => Sexit n
>   | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl
>   | Cminor.Sreturn None => Sreturn None
>   | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e))
>   | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body)
>   | Cminor.Sgoto lbl => Sgoto lbl
>   end.
>
>   
You can't print at these locations.  It looks like you want to "trace" 
the execution of your function.  To do so, I would suggest extracting 
some OCaml code and then adding print statements in the Ocaml code, 
which is often quite readable.

Of course, it is not advisable to keep this kind of code that is partly 
obtained mechanically and partly modified by hand, but for understanding 
and debugging purposes, it may be useful.

I hope this helps,

Yves