001 package escjava.vcGeneration.coq;
002
003 import java.util.HashMap;
004 import java.util.Iterator;
005 import java.util.Set;
006 import java.util.Vector;
007 import java.util.regex.Matcher;
008 import java.util.regex.Pattern;
009 import java.io.*;
010
011 import escjava.vcGeneration.*;
012 import escjava.translate.*;
013 import javafe.ast.*;
014
015
016 /**
017 * This class is an implementations of the interface {@link ProverType}.
018 * In order to handle the Coq theorem prover.
019 * @author J. Charles, based on the work of C. Hurlin and C.Pulley
020 * @version 14/11/2005
021 */
022 public class CoqProver extends ProverType {
023
024 public String labelRename(String label) {
025 label = label.replace('.','_');
026 label = label.replace('<','_');
027 label = label.replace('>','_');
028 return label;
029 }
030
031 /**
032 * @return an instance of the class {@link TCoqVisitor}.
033 */
034 public TVisitor visitor(Writer out) throws IOException {
035 return new TCoqVisitor(out, this);
036 }
037
038 /**
039 * @param proofname the name we should give to the generated lemma.
040 * @param declns the declarations of the forall.
041 * @param vc the generated verification condition.
042 * @return the Coq vernacular file representing the proof.
043 */
044 public void getProof(Writer out, String proofName, TNode term) throws IOException {
045
046 // // We try to generate the prelude.
047 // try {
048 // new Prelude(new File("defs.v")).generate();
049 // } catch (IOException e) {
050 // e.printStackTrace();
051 // }
052
053 // generate declarations
054 out.write("Load \"defs.v\".\n");
055 generatePureMethodsDeclarations(out);
056 out.write("Lemma " + proofName + " : \n");
057 out.write("forall ");
058 generateDeclarations(out, term);
059 out.write(" ,\n");
060 generateTerm(out, term);
061 out.write(".\n");
062 out.write("Proof with autosc.\n" + "Qed.");
063 }
064
065
066 /**
067 * Generates the pure methods declarations
068 * @param s The output for the declarations.
069 */
070 private void generatePureMethodsDeclarations(Writer s) throws IOException {
071 //Let's go for the purity:
072 Vector methNames = TMethodCall.methNames;
073 Vector methDefs = TMethodCall.methDefs;
074 for (int i = 0; i < methNames.size(); i++) {
075 s.write("Variable "
076 + getVariableInfo(((VariableInfo) methNames.get(i)))
077 + " : ");
078 TMethodCall tmc = (TMethodCall) (methDefs.get(i));
079 Vector v = tmc.getArgType();
080 for (int j = 0; j < v.size(); j++) {
081 TypeInfo ti = ((TypeInfo) v.get(j));
082 if (ti == null)
083 s.write("S -> ");
084 else
085 s.write(((TypeInfo) v.get(j)).def + " -> ");
086 }
087 if (tmc.type == null) {
088 s.write("S.\n");
089 } else {
090 s.write(tmc.type.def + ".\n");
091 }
092 }
093 }
094
095
096 /**
097 * @param caller the type to translate to Coq.
098 * @return a valid type name.
099 */
100 public String getTypeInfo(TypeInfo caller) {
101 if (caller.def == null)
102 coqRename(caller);
103 return caller.def;
104 }
105
106
107 /**
108 * Defines predefined Coq types, and some predefined variables
109 * (ecReturn, ecThrow and XRES).
110 * For now there is no String types should be extended in the future.
111 */
112 public void init() {
113 // Predefined types
114 TNode._Reference = TNode.addType("%Reference", "Reference");
115 TNode._Time = TNode.addType("%Time", "Time");
116 TNode._Type = TNode.addType("%Type", "Types");
117 TNode._boolean = TNode.addType("boolean", "bool");
118 TNode._char = TNode.addType("char", "t_char");
119 TNode._DOUBLETYPE = TNode.addType("DOUBLETYPE", "t_double");
120 TNode._double = TNode.addType("double", "t_double");
121 TNode._Field = TNode.addType("%Field", "Field");
122 TNode._INTTYPE = TNode.addType("INTTYPE", "t_int");
123 TNode._integer = TNode.addType("integer", "t_int");
124 TNode._float = TNode.addType("float", "t_float");
125 TNode._Path = TNode.addType("%Path", "Path");
126 // of terminating a function
127 //_String = addType("String" "String"); fixme, does this type appears in original proof ?
128
129 // Predefined variables name
130 // variables used by the old proof system and that we still need
131 TNode.addName("ecReturn", "%Path", "ecReturn");
132 TNode.addName("ecThrow", "%Path", "ecThrow");
133 TNode.addName("XRES", "%Reference", "XRes");
134 }
135
136 public Expr addTypeInfo(InitialState initState, Expr tree) {
137 //FIXME Our prover logic is (presumably?) typed, so why do we need to do this here?
138 tree = GC.implies(initState.getInitialState(), tree);
139 return tree;
140 }
141
142 /**
143 * Tries to simplify the given tree using the class
144 * {@link TProofTyperVisitor}.
145 * @param tree the tree to simplify.
146 */
147 public TNode rewrite(TNode tree) {
148 TProofTyperVisitor tptv = new TProofTyperVisitor();
149 try {
150 tree.accept(tptv);
151 } catch (IOException e) {
152 // This should never happen!?
153 }
154 //TProofSimplifier psvi = new TProofSimplifier();
155 //tree.accept(psvi);
156 return tree;
157 }
158
159
160 /**
161 * Rename the type, ie. the name {@link TypeInfo#old} to
162 * a proper Coq name in the variable {@link TypeInfo#def}
163 * @param t the type name to rename.
164 */
165 private void coqRename(TypeInfo t){
166
167 if(t.old.equals("null") )
168 t.def = "Reference";
169 else {
170 // common rules here //fixme, be more specific maybe
171 if(t.old.startsWith("java.")) //check if in the form java.x.y
172 t.def = t.old.replace('.','_');
173 else {
174 System.err.println("Type not handled in escjava::vcGeneration::TypeInfo::coqRename() : "+t.old);
175 System.err.println("Considering it as a user defined type... ie Types");
176 t.def = "ReferenceType";
177 }
178 }
179 }
180
181 /**
182 * Returns a valid Coq name corresponding to the given VariableInfo.
183 * @param vi the variable info to analyse.
184 */
185 public /*@ non_null @*/ String getVariableInfo(VariableInfo vi){
186 if(vi.type != TNode._Type){
187 if(vi.def == null)
188 coqRename(vi);
189
190 return vi.def;
191 }
192 else {
193 /*
194 * When variable is a type, we first have to check if it's in the type table.
195 * If yes, we take the name here (it's the case with predefined types like INTYPE, integer, Reference etc...
196 * Else it's normally a user defined Type
197 */
198
199 Set keySet = TNode.typesName.keySet();
200 Iterator iter = keySet.iterator();
201 TypeInfo tiTemp = null;
202 String keyTemp = null;
203
204 while(iter.hasNext()) {
205 try {
206 keyTemp = (String)iter.next();
207 } catch (Exception e){
208 System.err.println(e.getMessage());
209 }
210 tiTemp = (TypeInfo)TNode.typesName.get(keyTemp);
211 if(tiTemp.old.equals(vi.old)) {
212 return getTypeInfo(tiTemp);
213 }
214
215 }
216
217 System.err.println("Warning in " +
218 "escjava.java.vcGenerator.coq.CoqProver.getCoq(VariableInfo), " +
219 "considering "+
220 vi.old
221 +" as a user defined type, " +
222 "or a not (yet) handled variable.");
223
224 coqRename(vi);
225
226 return vi.def;
227 }
228 }
229
230 /**
231 * Rename the variable, ie. the name {@link VariableInfo#old} to
232 * a proper Coq name in the variable {@link VariableInfo#def}.
233 * Stolen from the PVS plugin...
234 * @param vi the variable to rename.
235 */
236 private void coqRename(VariableInfo vi){
237
238 String coq;
239 // definitions of different regexp used.
240 Pattern p1 = Pattern.compile("\\|(.*):(.*)\\.(.*)\\|");
241 Matcher m1 = p1.matcher(vi.old);
242
243 // <variables not handled>
244 Pattern p2 = Pattern.compile("Unknown tag <.*>");
245 Matcher m2 = p2.matcher(vi.old);
246
247 Pattern p3 = Pattern.compile("\\|brokenObj<.*>\\|");
248 Matcher m3 = p3.matcher(vi.old);
249 // </variables not handled>
250 Pattern p4 = Pattern.compile("\\|(.*):(.*)\\|");
251 Matcher m4 = p4.matcher(vi.old);
252 String name = null;
253 String line = null;
254 String column = null;
255
256 int i = 0;
257
258
259 //System.out.println("Performing regular expression matching against "+old+" ");
260
261 /*
262 This case is done first because some variables not handled are "%Type" ones
263 and thus otherwise they will be matched by the next if construct
264 */
265 if(m2.matches() || m3.matches() || vi.old.equals("brokenObj")) { // variable is not handled yet, ask David Cok about
266 // some things
267 coq = "(* %NotHandled *) brokenObj";
268 vi.type = TNode._Reference;
269
270 }
271
272 // <case 1>
273 /*
274 If variable's a type, we must prefix his renaming by userDef?.
275 Why ?
276 Because if the user defined a type named 'Reference', otherwise we will use is as it
277 in the proof and it will interfer with our predefined types.
278
279 Since '?' isn't a valid character in the java notation and is Ok for pvs,
280 we use it to make the difference.
281 */
282 else if(vi.type == TNode._Type){
283 System.err.println("Warning in escjava.java.vcGeneration.VariableInfo.coqRename() : considering "+vi.old+" as a user defined type.");
284
285 // renaming done here
286 coq = "userDef_"+ vi.old;
287 }
288 // </case 1>
289
290 // <case 2>, capturing |y:8.31|
291 else if(m1.matches()){
292 //@ assert m1.groupCount() == 3;
293
294 if(m1.groupCount() != 3)
295 System.err.println("Error in escjava.java.vcGeneration.VariableInfo.coqRename : m.groupCount() != 3");
296
297 for( i = 1; i <= m1.groupCount(); i++) {
298
299 if(m1.start(i) == -1 || m1.end(i) == -1)
300 System.err.println("Error in escjava.java.vcGeneration.VariableInfo.coqRename : return value of regex matching is -1");
301 else {
302
303 String temp = vi.old.substring(m1.start(i),m1.end(i));
304 //@ assert temp != null;
305
306 switch(i){
307 case 1 :
308 name = temp;
309 //@ assert name != null;
310 break;
311 case 2:
312 line = temp;
313 //@ assert line != null;
314 break;
315 case 3:
316 column = temp;
317 //@ assert column != null;
318 break;
319 default :
320 System.err.println("Error in escjava.java.vcGeneration.VariableInfo.coqRename : switch call incorrect, switch on value "+i);
321 }
322 } // no error in group
323 } // checking all group
324
325 /* renaming done here, if you want the way it's done
326 (for pattern like |y:8.31|)
327 do it here. */
328 coq = name+"_"+line+"_"+column;
329 } // </case 2>
330
331 else if(m4.matches()) {
332 if(m4.groupCount() != 2)
333 System.err.println("Error in escjava.java.vcGeneration.VariableInfo.coqRename : m.groupCount() != 3");
334
335 for( i = 1; i <= m4.groupCount(); i++) {
336
337 if(m4.start(i) == -1 || m4.end(i) == -1)
338 System.err.println("Error in escjava.java.vcGeneration.VariableInfo.coqRename : return value of regex matching is -1");
339 else {
340
341 String temp = vi.old.substring(m4.start(i),m4.end(i));
342 //@ assert temp != null;
343
344 switch(i){
345 case 1 :
346 name = temp;
347 //@ assert name != null;
348 break;
349 case 2:
350 line = temp;
351 //@ assert line != null;
352 break;
353 default :
354 System.err.println("Error in escjava.java.vcGeneration.VariableInfo.coqRename : switch call incorrect, switch on value "+i);
355 }
356 } // no error in group
357
358 } // checking all group
359
360
361 if(line.equals("unknown"))
362 coq = name;
363 else
364 coq = name+"_"+line;
365 }
366 else {
367 coq = vi.old; // FIXME handle everything
368 } // regexp didn't match
369 coq = removeInvalidChar(coq);
370
371 if(coq.equals("Z"))
372 coq = "z";
373 vi.def = coq;
374 }
375
376 /**
377 * Removes the invalid characters in Coq for a given String.
378 * @param name The name where some invalid characters appear.
379 * @return The name without the invalid characters.
380 */
381 public String removeInvalidChar (String name) {
382 name = name.replace('@', '_');
383 name = name.replace('#', '_');
384 name = name.replace('.', '_');
385 name = name.replace('-', '_');
386 name = name.replace('<', '_');
387 name = name.replace('>', '_');
388 name = name.replace('?', '_');
389 name = name.replace('[', '_');
390 name = name.replace(']', '_');
391 name = name.replace('!', '_');
392 name = name.replaceAll("\\|", "");
393 return name;
394 }
395
396
397 /**
398 * Generates the declarations for the forall construct in the Coq Fashion,
399 * i.e. (var1: Type1) (var2 : Type2)...
400 * @param s The output
401 * @param variablesNames the variables' names.
402 */
403 public void generateDeclarations(/*@ non_null @*/Writer s, HashMap variablesNames) throws IOException {
404 Set keySet = variablesNames.keySet();
405
406 Iterator iter = keySet.iterator();
407 String keyTemp = null;
408 VariableInfo viTemp = null;
409
410 while (iter.hasNext()) {
411
412 try {
413 keyTemp = (String) iter.next();
414 } catch (Exception e) {
415 System.err.println(e.getMessage());
416 }
417 viTemp = (VariableInfo) variablesNames.get(keyTemp);
418
419 String name = viTemp.getVariableInfo().toString();
420 if (name.equals("ecReturn") || name.equals("ecThrow")
421 || name.equals("t_int"))
422 continue;
423 if (viTemp.type != null) {
424 s.write("(");
425 s.write(viTemp.getVariableInfo() + " : "
426 + viTemp.type.getTypeInfo());
427 s.write(")");
428
429 } else {
430 s.write("(" + viTemp.getVariableInfo() + " : S)");
431 TDisplay
432 .warn(
433 this,
434 "generateDeclarations",
435 "Type of variable "
436 + keyTemp
437 + " is not set when declarating variables for the proof, skipping it...");
438 }
439 }
440 }
441 }