The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi Reaz,

If you don't want to manually edit the extracted code (which can get a bit hairy when making changes) you can always define an identity function which takes an extra string parameter which it prints. Something like:

Require Import Ascii String.
Require Import Program.

Definition debug {T} (_: string) (v:T) : T := v.

Open Scope string_scope.

Fixpoint double (n : nat) : nat :=
  match n with
    | 0   => debug "hi" 0
    | S n => S (S (double n))
  end.

Extract Inductive ascii => "Debug.ascii" [ "Debug.Ascii" ].
Extract Inductive string  => "Debug.ascii list" [ "[]" "(::)" ].
Extract Inductive bool => "bool" [ "true" "false" ].

Extract Constant debug => "Debug.debug".

Extraction "test.ml" double.

with the file debug.ml containing:
type ascii =
  | Ascii of bool * bool * bool * bool * bool * bool * bool * bool

type nat =
  | O
  | S of nat

let ascii_to_char asc =
  let Ascii (a, b, c, d, e, f, g, h) = asc in
  let bits : bool list = [a;b;c;d;e;f;g;h] in
  let ch = List.fold_right (fun v a -> a * 2 + if v then 1 else 0) bits 0 in
  Char.chr ch

let list_ascii_to_string s =
  let rec r s =
    match s with
      [] -> ""
    | first :: rest ->
        (String.make 1 (ascii_to_char first)) ^ (r rest)
  in r s

let debug s v =
  let _ = print_string ((list_ascii_to_string s) ^ "\r\n") in
  v

i hope this helps.

On Tue, Aug 4, 2009 at 2:29 AM, Yves Bertot <Yves.Bertot AT sophia.inria.fr> wrote:

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
gregory malecha