The Coq mailing list

[reaz <reazshawon AT gmail.com>]

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.

Yves Bertot wrote:
> 
> reaz wrote:
>> Can any one tell me how to print an arbitrary string in coq-8.1.pl3?
>>
>> Thanks.
>> --Reaz
>>   
> What do you mean by "printing"?  At what time do you want to print 
> something?  Or do you just want to write a program that returns a string 
> and evaluate this program to see its result?
> 
> For the latter just use "Eval compute".  Here is an example:
> 
> Require Import String.
> Open Scope string_scope.
> Eval compute in ("Hello " ++ "world!").
> 
> 
> If you want side effects to occur in the middle of goal-directed proofs, 
> you can also ask fail and idtac to display a message that you gave them 
> as argument.  This is explained in the documentation for these tactics 
> (pp. 197-198 in the pdf version of the reference manual).
> 
> 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
> 
> 

-- 
View this message in context: 
http://www.nabble.com/print-string-in-coq-8.1.pl3-tp24785276p24802020.html
Sent from the Coq mailing list archive at Nabble.com.