coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
- To: reaz <reazshawon AT gmail.com>
- Cc: Yves.Bertot AT sophia.inria.fr, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] print string in coq-8.1.pl3
- Date: Tue, 4 Aug 2009 20:12:14 -0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=nP1gbCkFaVVF9T8c1QyG40uAJ++Hq1UlcBFCIvIe3UpaS6i8iK9m9Z7I4r+viEcN8G YF0cEjWxJccLHWGIlxGYx9mt/x3rLwVyySeu1B8PKXW+/ljGQRsDrwtHenGxnU+kQyST OHkjOUkNe7WCnj0T6mR/dyA+ESDqeuiyoyRa4=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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: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.
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.
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
- [Coq-Club] print string in coq-8.1.pl3, reaz
- Re: [Coq-Club] print string in coq-8.1.pl3,
Yves Bertot
- Re: [Coq-Club] print string in coq-8.1.pl3,
reaz
- Re: [Coq-Club] print string in coq-8.1.pl3,
Yves Bertot
- Re: [Coq-Club] print string in coq-8.1.pl3, Gregory Malecha
- Re: [Coq-Club] print string in coq-8.1.pl3,
Yves Bertot
- Re: [Coq-Club] print string in coq-8.1.pl3,
reaz
- Re: [Coq-Club] print string in coq-8.1.pl3,
Yves Bertot
Archive powered by MhonArc 2.6.16.