001    package escjava.vcGeneration.coq;
002    
003    import java.io.*;
004    
005    import escjava.vcGeneration.*;
006    import escjava.vcGeneration.VariableInfo;
007    
008    
009    /**
010     * In the Coq extension, we differentiate <code>Boolean</code>
011     * value and variables from usual <code>Prop</code>.
012     * So we have 2 visitors which are coupled. 
013     * <p>
014     * This is the visitor used for <code>Boolean</code> specific values.  
015     * @author J.Charles
016     * @version 14/11/2005
017     */
018    public class TCoqBoolVisitor extends TCoqVisitor {
019            
020            /**
021             * Constructor of the couple  TCoqVisitor/TCoqBoolVisitor.
022             * It should not be called by any other class than TCoqVisitor.
023             * @param v the current visitor.
024             * @param o the current CoqStringBuffer.
025             * @param p the current instance of CoqProver.
026             */
027            TCoqBoolVisitor(Writer out, TCoqVisitor v, PrettyPrinter o, CoqProver p){
028            super(out, v, o, p);    
029        }
030            
031            
032            /**
033             * Boolean value seen as a prop boolean value:
034             * <code>True</code> or <code>False</code>.
035             * @see TCoqVisitor#visitTBoolean(TBoolean)
036             */
037            public void visitTBoolean(/*@ non_null @*/ TBoolean n) throws IOException{      
038                    if(n.value)
039                        out.appendN("True");
040                    else
041                        out.appendN("False");
042             }
043             
044             /**
045              * Boolean variables that are used within a prop
046              * should be translated in the form <code>myvar = true</code>
047              * @param n the variable to translate.
048              */
049             public void visitTName(/*@ non_null @*/ TName n) throws IOException{
050                        VariableInfo vi = TNode.getVariableInfo(n.name);
051                        String name = p.getVariableInfo(vi);
052                        if(name.equals("Z"))
053                            name = "T_Z";
054                            out.appendN(name + " = true");
055             }
056             
057             public void visitTSelect(/*@ non_null @*/ TSelect n) throws IOException{
058                    String pre = "";
059                    if(TNode._integer.equals(((TNode)n.sons.get(1)).type))
060                            pre = "arr";
061                    genericFun("BoolHeap." + pre +"select ", n);
062                    out.appendN(" = true");
063                }
064             
065             public void visitTBoolNot(/*@ non_null @*/ TBoolNot n) throws IOException{
066                    unaryProp("not ", n);
067             }
068    }