001 package escjava.vcGeneration.coq;
002
003 import java.io.*;
004
005 import escjava.vcGeneration.*;
006 import escjava.vcGeneration.coq.visitor.ANotHandledVisitor;
007
008 /**
009 * In the Coq extension, we differentiate <code>Boolean</code>
010 * value and variables from usual <code>Prop</code>.
011 * So we have 2 visitors which are coupled.
012 * <p>
013 * This is the visitor used for <code>Boolean</code>
014 * used as <code>Prop</code> values. This class, the main Coq visitor
015 * is divided into smaller parts handling the different domain-specific
016 * functions. For instance all the functions on the Int are in the
017 * visitor class {@link escjava.vcGeneration.coq.visitor.AIntegralVisitor}.
018 * @see escjava.vcGeneration.coq.visitor
019 * @author J.Charles based on the work of C.Hurlin
020 * @version 14/11/2005
021 */
022 class TCoqVisitor extends ANotHandledVisitor {
023
024
025 TCoqVisitor(Writer out, CoqProver prover){
026 super(out, prover, null);
027 setVisitors(this, new TCoqBoolVisitor(out, this, super.out, p));
028 }
029
030 protected TCoqVisitor(Writer out, TCoqVisitor v, PrettyPrinter ppout, CoqProver p){
031 super(out, p, ppout);
032 setVisitors(v, this);
033 }
034
035
036 /*
037 * non automatic generated class
038 */
039 public void visitTName(/*@ non_null @*/ TName n) throws IOException{
040
041 /*
042 * This call handles everything, ie if n is a variable or a type name
043 */
044 VariableInfo vi = TNode.getVariableInfo(n.name);
045 String name = p.getVariableInfo(vi);
046 if(name.equals("Z"))
047 name = "T_Z";
048 out.appendN(name);
049 }
050
051 public void visitTRoot(/*@ non_null @*/ TRoot n) throws IOException{
052
053 for(int i = 0; i <= n.sons.size() - 1; i++)
054 n.getChildAt(i).accept(tcv);
055
056 }
057
058 /*
059 * class created using the perl script
060 */
061 public void visitTBoolImplies(/*@ non_null @*/ TBoolImplies n) throws IOException{
062 genericPropOp("->", n);
063 }
064
065 public void visitTBoolAnd(/*@ non_null @*/ TBoolAnd n) throws IOException{
066 genericPropOp("/\\", n);
067 }
068
069 public void visitTBoolOr(/*@ non_null @*/ TBoolOr n) throws IOException{
070 genericPropOp("\\/", n);
071 }
072
073 public void visitTBoolNot(/*@ non_null @*/ TBoolNot n) throws IOException{
074 unaryGeneric("negb ", n);
075 }
076
077 public void visitTBoolEQ(/*@ non_null @*/ TBoolEQ n) throws IOException{
078
079 printBoolEq(n);
080
081 }
082 public void printBoolEq(TFunction n) throws IOException{
083 //String s = "=";
084 if(n.sons.size() < 2 )
085 System.err.println("java.escjava.vcGeneration.TCoqVisitor.printBoolEq : the spaced out binary operator named = has a number of sons equals to "+n.sons.size()+" which is different from 2");
086 out.appendI("(");
087 for(int i =0; i < n.sons.size() - 1; i++) {
088
089 if(i != 0) {
090 out.appendN(" /\\ (");
091 }
092 else
093 out.appendN("(");
094 Object o = (n.getChildAt(i+1));
095 if((o instanceof TBoolean)) {
096 n.getChildAt(i).accept(tcv);
097 out.appendN(" = ");
098 n.getChildAt(i+1).accept(tcv);
099 }
100 else {
101 n.getChildAt(i).accept(tcbv);
102 out.appendN(" <-> ");
103 n.getChildAt(i+1).accept(tcbv);
104 }
105
106
107 out.appendN(")");
108 }
109 out.appendN(")");
110 if((n.getChildAt(1)) instanceof TName || (n.getChildAt(1)) instanceof TLiteral)
111 out.reduceIwNl();
112 else
113 out.reduceI();
114 }
115
116 public void visitTBoolNE(/*@ non_null @*/ TBoolNE n) throws IOException{
117 binOp("<>", n);
118 }
119
120 public void visitTAllocLT(/*@ non_null @*/ TAllocLT n) throws IOException{
121 binOp("<", n);
122 }
123
124 public void visitTAllocLE(/*@ non_null @*/ TAllocLE n) throws IOException{
125 binOp("<=", n);
126 }
127
128 public void visitTAnyEQ(/*@ non_null @*/ TAnyEQ n) throws IOException{
129 if(n.sons.size() == 2) {
130 Object son = n.sons.get(1);
131 if((son instanceof TAsLockSet) ||
132 (son instanceof TAsElems) ||
133 (son instanceof TAsField)) {
134 out.appendN("(* TAs *) True ");
135 return;
136 }
137 }
138
139 spacedBinOp("(* Any Eq *) =", n);
140
141 }
142
143 public void visitTAnyNE(/*@ non_null @*/ TAnyNE n) throws IOException{
144 binOp("<>", n);
145 }
146
147
148
149
150 public void visitTRefEQ(/*@ non_null @*/ TRefEQ n) throws IOException{
151 spacedBinOp("(* Ref Eq *) =", n);
152 }
153
154 public void visitTRefNE(/*@ non_null @*/ TRefNE n) throws IOException{
155 binOp("<>", n);
156 }
157
158 public void visitTTypeEQ(/*@ non_null @*/ TTypeEQ n) throws IOException{
159 spacedBinOp("(* Type Eq *) =", n);
160 }
161
162 public void visitTTypeNE(/*@ non_null @*/ TTypeNE n) throws IOException{
163 binOp("<>", n);
164 }
165
166 public void visitTTypeLE(/*@ non_null @*/ TTypeLE n) throws IOException{
167 genericFun("subtypes", n); //
168 }
169
170
171
172
173 public void visitTTypeOf(/*@ non_null @*/ TTypeOf n) throws IOException{
174 genericFun("typeof",n);
175 }
176
177 public void visitTForAll(/*@ non_null @*/ TForAll n) throws IOException{
178 out.appendI("(forall ");
179 int i =0;
180 StringBuffer sb = new StringBuffer();
181 //n.generateDeclarations(sb);
182 out.appendN(sb.toString());
183 for(; i < n.sons.size(); i++) {
184 TNode a = n.getChildAt(i);
185
186 /*
187 * If not last, output a space
188 */
189 if(!(a instanceof TName)) {
190 break;
191 }
192
193 out.appendN( "(");
194 TName var = (TName) a;
195 tcv.visitTName(var);
196
197 out.appendN( ": "+ p.getTypeInfo(TNode.getVariableInfo(var.name).type) + ")");
198
199 }
200 out.appendN(",");
201 if( i <n.sons.size() - 1)
202 i++;
203
204 TNode a = n.getChildAt(i);
205 out.appendN(" ");
206 a.accept(tcv);
207 out.appendN(")");
208 out.reduceI();
209 }
210
211 //
212
213 public void visitTIsAllocated(/*@ non_null @*/ TIsAllocated n) throws IOException{
214 genericFun("isAllocated", n);
215 }
216
217 public void visitTEClosedTime(/*@ non_null @*/ TEClosedTime n) throws IOException{
218 genericFun("eClosedTime", n);
219 }
220
221 public void visitTFClosedTime(/*@ non_null @*/ TFClosedTime n) throws IOException{
222 genericFun("fClosedTime", n);
223 }
224 public void visitTAsElems(/*@ non_null @*/ TAsElems n) throws IOException{
225 genericFun("asElems", n);
226 }
227
228 public void visitTAsField(/*@ non_null @*/ TAsField n) throws IOException{
229 genericFun("asField", n);
230 }
231
232 public void visitTString(/*@ non_null @*/ TString n) throws IOException{
233 out.appendN(" (typeof " + n.value+ ")" );
234 }
235
236 public void visitTBoolean(/*@ non_null @*/ TBoolean n) throws IOException{
237 if(n.value)
238 out.appendN(" (* bool*) true");
239 else
240 out.appendN("false");
241 }
242
243 public void visitTChar(/*@ non_null @*/ TChar n) throws IOException{
244 out.appendN(" (* a char value *)"+n.value);
245 }
246
247 public void visitTDouble(/*@ non_null @*/ TDouble n) throws IOException{
248 out.appendN(" (* a double value *)"+n.value);
249 }
250 public void visitTNull(/*@ non_null @*/ TNull n) throws IOException{
251 out.appendN(" null");
252 }
253
254 public void visitTMethodCall(/*@non_null*/TMethodCall call) throws IOException {
255 genericFun(p.getVariableInfo(call.getName()), call);
256 }
257
258 public void visitTUnset(/*@non_null*/TUnset n) throws IOException {
259 genericFun("unset", n);
260 }
261
262 public void visitTSum(TSum s) {
263 // TODO Auto-generated method stub
264
265 }
266
267
268 }