001    package escjava.vcGeneration.simplify;
002    
003    import java.util.HashMap;
004    import java.io.*;
005    
006    import escjava.vcGeneration.*;
007    import escjava.translate.*;
008    import javafe.ast.*;
009    
010    public class SimplifyProver extends ProverType {
011        
012        public String labelRename(String label) {
013            return label;
014        }
015        
016        public TVisitor visitor(Writer out) throws IOException {
017            return new TSimplifyVisitor(out);
018        }
019    
020        public void getProof(Writer out, String proofName, TNode term) throws IOException {
021            generateTerm(out, term);
022        }
023    
024        public String getVariableInfo(VariableInfo caller) {
025    
026            /*
027             * This method is special since <explanation>
028             * FIXME
029             */
030    
031            if (caller.type != TNode._Type)
032                return caller.old;
033    
034            else {
035                if (caller.old.equals("boolean"))
036                    return "T_bool"; // fixme not sure
037                else if (caller.old.equals("char"))
038                    return "T_char";
039                else if (caller.old.equals("DOUBLETYPE"))
040                    return "T_double";
041                else if (caller.old.equals("double"))
042                    return "T_double";
043                else if (caller.old.equals("JMLDataGroup"))
044                    return "|T_org.jmlspecs.lang.JMLDataGroup|";
045                else if (caller.old.equals("INTTYPE"))
046                    return "T_int";
047                else if (caller.old.equals("integer"))
048                    return "T_int";
049                else if (caller.old.equals("Unknown tag <242>"))
050                    return "T_anytype";
051                else {
052                    if (caller.old.startsWith("java.")) //check if in the form java.x.y 
053                        return "T_" + caller.old;
054                    else {
055                        TDisplay.warn(this, "getVariableInfo()", "Type not handled : "
056                                + caller.old);
057                        TDisplay.warn(this, "getVariableInfo()",
058                                "Considering it as a user defined type");
059                        return "T_" + caller.old;
060                    }
061                }
062            }
063    
064        }
065    
066        public String getTypeInfo(TypeInfo caller) {
067            return null;
068        }
069    
070        public void init() {
071            // Predefined types
072    
073            TNode._Reference = TNode.addType("%Reference", "%Reference");
074            TNode._Time = TNode.addType("%Time", "%Time");
075            TNode._Type = TNode.addType("%Type", "%Type");
076            TNode._boolean = TNode.addType("boolean", "boolean");
077            TNode._char = TNode.addType("char", "char");
078            TNode._DOUBLETYPE = TNode.addType("DOUBLETYPE", "DOUBLETYPE");
079            TNode._double = TNode.addType("double", "double");
080            TNode._Field = TNode.addType("%Field", "%Field");
081            TNode._INTTYPE = TNode.addType("INTTYPE", "INTTYPE");
082            TNode._integer = TNode.addType("integer", "integer");
083            TNode._float = TNode.addType("float", "float");
084            TNode._Path = TNode.addType("%Path", "%Path"); // used to modelize different ways
085            // of terminating a function
086            //_String = addType("String", "String"); fixme, does this type appears in original proof ?
087    
088            // Predefined variables name
089            // variables used by the old proof system and that we still need
090            TNode.addName("ecReturn", "%Path", "ecReturn");
091            TNode.addName("ecThrow", "%Path", "ecThrow");
092            TNode.addName("XRES", "%Reference", "XRES");        
093        }
094        
095        public Expr addTypeInfo(InitialState initState, Expr tree) {
096            tree = GC.implies(initState.getInitialState(), tree);
097            return tree;
098        }
099        
100        public TNode rewrite(TNode tree) {
101            // Intentionally does nothing
102            return tree;
103        }
104    
105            public void generateDeclarations(/*@non_null*/Writer s, HashMap variablesName) throws IOException {
106                    // TODO Auto-generated method stub
107                    
108            }
109    }