[Coq-Club] print string in coq-8.1.pl3
Gregory Malecha
gmalecha at !NS! eecs.harvard.edu
Tue, 4 Aug 2009 20:12:14 -0400
--00163631059df09c42047059da5c
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
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@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
--00163631059df09c42047059da5c
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Hi Reaz,<br><br>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 ide=
ntity function which takes an extra string parameter which it prints. Somet=
hing like:<br>
<br>Require Import Ascii String.<br>Require Import Program.<br><br>Definiti=
on debug {T} (_: string) (v:T) : T :=3D v.<br><br>Open Scope string_scope.<=
br><br>Fixpoint double (n : nat) : nat :=3D<br>=C2=A0 match n with<br>=C2=
=A0=C2=A0=C2=A0 | 0=C2=A0=C2=A0 =3D> debug "hi" 0<br>
=C2=A0=C2=A0=C2=A0 | S n =3D> S (S (double n))<br>=C2=A0 end.<br><br>Ext=
ract Inductive ascii =3D> "Debug.ascii" [ "Debug.Ascii&qu=
ot; ].<br>Extract Inductive string=C2=A0 =3D> "Debug.ascii list&quo=
t; [ "[]" "(::)" ].<br>
Extract Inductive bool =3D> "bool" [ "true" "fa=
lse" ].<br><br>Extract Constant debug =3D> "Debug.debug".=
<br><br>Extraction "<a href=3D"http://test.ml">test.ml</a>" doubl=
e.<br>
<br>with the file <a href=3D"http://debug.ml">debug.ml</a> containing:<br>t=
ype ascii =3D<br>=C2=A0 | Ascii of bool * bool * bool * bool * bool * bool =
* bool * bool<br><br>type nat =3D<br>=C2=A0 | O<br>=C2=A0 | S of nat<br><br=
>let ascii_to_char asc =3D<br>
=C2=A0 let Ascii (a, b, c, d, e, f, g, h) =3D asc in<br>=C2=A0 let bits : b=
ool list =3D [a;b;c;d;e;f;g;h] in<br>=C2=A0 let ch =3D List.fold_right (fun=
v a -> a * 2 + if v then 1 else 0) bits 0 in<br>=C2=A0 Char.chr ch<br><=
br>let list_ascii_to_string s =3D<br>
=C2=A0 let rec r s =3D<br>=C2=A0=C2=A0=C2=A0 match s with<br>=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0 [] -> ""<br>=C2=A0=C2=A0=C2=A0 | first :: r=
est -><br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 (String.make 1 (asc=
ii_to_char first)) ^ (r rest)<br>=C2=A0 in r s<br><br>let debug s v =3D<br>=
=C2=A0 let _ =3D print_string ((list_ascii_to_string s) ^ "\r\n")=
in<br>
=C2=A0 v<br><br>i hope this helps.<br><br><div class=3D"gmail_quote">On Tue=
, Aug 4, 2009 at 2:29 AM, Yves Bertot <span dir=3D"ltr"><<a href=3D"mail=
to:Yves.Bertot@sophia.inria.fr">Yves.Bertot@sophia.inria.fr</a>></span> =
wrote:<br>
<blockquote class=3D"gmail_quote" style=3D"border-left: 1px solid rgb(204, =
204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class=3D"im"=
>reaz wrote:<br>
<blockquote class=3D"gmail_quote" style=3D"border-left: 1px solid rgb(204, =
204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Consider following code segment. I want to print messages in <>.<br>
<br>
Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=3D<br>
=C2=A0match s with<br>
=C2=A0| Cminor.Sskip =3D> Sskip <print "skip"><br>
=C2=A0| Cminor.Sassign id e =3D> =C2=A0Sassign id (sel_expr e) <prin=
t "assign"><br>
=C2=A0| Cminor.Sstore chunk addr rhs =3D> store chunk (sel_expr addr) (=
sel_expr<br>
rhs) <print "store"><br>
=C2=A0| Cminor.Scall optid sg fn args =3D><br>
=C2=A0 =C2=A0 =C2=A0Scall optid sg (sel_expr fn) (sel_exprlist args) <p=
rint "call"><br>
=C2=A0| Cminor.Stailcall sg fn args =3D> =C2=A0 =C2=A0 =C2=A0Stailcall=
sg (sel_expr fn) (sel_exprlist args)<br>
=C2=A0| Cminor.Sseq s1 s2 =3D> Sseq (sel_stmt s1) (sel_stmt s2)<br>
=C2=A0| Cminor.Sifthenelse e ifso ifnot =3D><br>
=C2=A0 =C2=A0 =C2=A0Sifthenelse (condexpr_of_expr (sel_expr e))<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(sel_stmt if=
so) (sel_stmt ifnot)<br>
=C2=A0| Cminor.Sloop body =3D> Sloop (sel_stmt body)<br>
=C2=A0| Cminor.Sblock body =3D> Sblock (sel_stmt body)<br>
=C2=A0| Cminor.Sexit n =3D> Sexit n<br>
=C2=A0| Cminor.Sswitch e cases dfl =3D> Sswitch (sel_expr e) cases dfl<=
br>
=C2=A0| Cminor.Sreturn None =3D> Sreturn None<br>
=C2=A0| Cminor.Sreturn (Some e) =3D> Sreturn (Some (sel_expr e))<br>
=C2=A0| Cminor.Slabel lbl body =3D> Slabel lbl (sel_stmt body)<br>
=C2=A0| Cminor.Sgoto lbl =3D> Sgoto lbl<br>
=C2=A0end.<br>
<br>
=C2=A0<br>
</blockquote></div>
You can't print at these locations. =C2=A0It looks like you want to &qu=
ot;trace" the execution of your function. =C2=A0To do so, I would sugg=
est extracting some OCaml code and then adding print statements in the Ocam=
l code, which is often quite readable.<br>
<br>
Of course, it is not advisable to keep this kind of code that is partly obt=
ained mechanically and partly modified by hand, but for understanding and d=
ebugging purposes, it may be useful.<br>
<br>
I hope this helps,<div><div></div><div class=3D"h5"><br>
<br>
Yves<br>
<br>
--------------------------------------------------------<br>
Bug reports: <a href=3D"http://logical.saclay.inria.fr/coq-bugs" target=3D"=
_blank">http://logical.saclay.inria.fr/coq-bugs</a><br>
Archives: <a href=3D"http://pauillac.inria.fr/pipermail/coq-club" target=3D=
"_blank">http://pauillac.inria.fr/pipermail/coq-club</a><br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 <a href=3D"http://pauillac.inria.fr/bin/wilma/=
coq-club" target=3D"_blank">http://pauillac.inria.fr/bin/wilma/coq-club</a>=
<br>
Info: <a href=3D"http://pauillac.inria.fr/mailman/listinfo/coq-club" target=
=3D"_blank">http://pauillac.inria.fr/mailman/listinfo/coq-club</a><br>
</div></div></blockquote></div><br><br clear=3D"all"><br>-- <br>gregory mal=
echa<br>
--00163631059df09c42047059da5c--