1 package acl2s.lib.certify;
2
3 import java.io.BufferedReader;
4 import java.io.BufferedWriter;
5 import java.io.File;
6 import java.io.FileReader;
7 import java.io.FileWriter;
8 import java.io.IOException;
9 import java.io.PrintWriter;
10
11 import org.peterd.util.io.MiscIO;
12
13 import acl2s.lib.parse.EmptyParse;
14 import acl2s.lib.parse.ParseException;
15 import acl2s.lib.parse.StringParser;
16 import acl2s.lib.parse.obj.Cons;
17 import acl2s.lib.parse.obj.LispObject;
18 import acl2s.lib.parse.obj.Str;
19 import acl2s.lib.parse.obj.Sym;
20
21 public class MaybeExtractPreamble {
22 static final String oldprefix = "#|$ACL2-A2S-PREAMBLE$;";
23 static final String prefix = "#|$ACL2s-Preamble$;";
24 static final String oldpostfix = ";$ACL2-A2S-PREAMBLE$|#";
25 static final String postfix = ";$ACL2s-Preamble$|#";
26
27 static void go(File lispFile) throws IOException, ParseException {
28 String fullBase = MiscIO.removeFileExtension(lispFile.getAbsolutePath());
29 String base = MiscIO.removeFileExtension(lispFile.getName());
30 File outFile = new File(fullBase + ".acl2");
31
32 go(lispFile,outFile,base,false, null);
33 }
34
35 static void go(File lispFile, boolean force, PrintWriter commentary) throws IOException, ParseException {
36 String fullBase = MiscIO.removeFileExtension(lispFile.getAbsolutePath());
37 String base = MiscIO.removeFileExtension(lispFile.getName());
38 File outFile = new File(fullBase + ".acl2");
39
40 go(lispFile, outFile, base, force, commentary);
41 }
42
43 static void go(File inFile, File outFile, String base, boolean force, PrintWriter commentary)
44 throws IOException, ParseException {
45 String line;
46 BufferedWriter bw;
47 String preamble = null;
48 PrintWriter c = commentary;
49
50 if (!force && outFile.exists() &&
51 inFile.lastModified() <= outFile.lastModified()) {
52 if (c != null) c.println("Preamble file already up to date.");
53 return;
54 }
55
56
57 if (c != null) c.print("Reading preamble... ");
58
|
Event do_not_call: |
"java.io.FileReader(java.io.File arg1)" implicitly uses the environment's default character set, which might lead to unexpected behavior. Consider using an InputStreamReader with a FileInputStream and an explicit character set. |
59 BufferedReader br = new BufferedReader(new FileReader(inFile));
60
61 do {
62 line = br.readLine();
63 if (line == null) {
64 // no preamble
65 if (c != null) c.println("none found.");
66 if (outFile.exists()) {
67 // just touch output file
68 if (c != null) c.println("Touching existing .acl2 file.");
69 outFile.setLastModified(System.currentTimeMillis());
70 return;
71 } else {
72 // use a default
73 if (c != null) c.print("Using default... ");
74 preamble = "(begin-book t :skip-proofs-okp t :defaxioms-okp t :ttags :all)\n";
75 }
76 } else if (line.endsWith(prefix) || line.endsWith(oldprefix)) {
77 // extract preamble
78 if (c != null) c.print("extracting... ");
79 StringBuilder pBuilder = new StringBuilder();
80
81 for(;;) {
82 line = br.readLine();
83 if (line == null) break;
84 if (line.endsWith(postfix)) {
85 pBuilder.append(line.substring(0, line.length() - postfix.length()));
86 pBuilder.append('\n');
87 break;
88 }
89 if (line.endsWith(oldpostfix)) {
90 pBuilder.append(line.substring(0, line.length() - oldpostfix.length()));
91 pBuilder.append('\n');
92 break;
93 }
94 pBuilder.append(line);
95 pBuilder.append("\n");
96 }
97
98 preamble = pBuilder.toString();
99 } // else keep looking for start of preamble
100 } while (preamble == null);
101
102 br.close();
103
104 StringParser parser = new StringParser(null, preamble);
105 int lastFormStart = -1;
106 for (;;) {
107 parser.skipSpaceAndComments();
108 if (parser.eof()) break;
109 lastFormStart = parser.getPos();
110 acl2s.lib.parse.no_obj.LispObject.parse(parser);
111 }
112 if (lastFormStart < 0) throw new EmptyParse();
113
114 parser.setPos(lastFormStart);
115
116 LispObject lastForm = LispObject.parseOne(parser);
117
118 if (!(lastForm instanceof Cons) ||
119 !(((Cons)lastForm).car instanceof Sym) ||
120 !(((Sym)((Cons)lastForm).car).sym.equals("BEGIN-BOOK"))) {
121 throw new ParseException("Malformed preamble (does not end in begin-book form).");
122 }
123
124 LispObject cdr = ((Cons)lastForm).cdr;
125
126 LispObject newLastForm =
127 new Cons(Certifier.certifyBookSym,
128 new Cons(new Str(base),
129 new Cons(Certifier.questionSym, cdr)));
130
131 if (c != null) c.print("saving... ");
132 bw = new BufferedWriter(new FileWriter(outFile, false));
133
134 bw.write(preamble.substring(0, lastFormStart));
135 bw.write("\n");
136 bw.write(newLastForm.toString());
137 bw.write("\n");
138
139 bw.flush();
140 bw.close();
141 if (c != null) c.println("done.");
142 }
143
144 public static void main(String[] args) {
145 try {
146 if (args.length < 1) {
147 throw new IllegalArgumentException("Must specify one file to read (and optionally a file to write to).");
148 }
149
150 File outFile;
151 if (args.length == 1) {
152 String fullBase = MiscIO.removeFileExtension(args[0]);
153 outFile = new File(fullBase + ".acl2");
154 } else if (args.length == 2) {
155 outFile = new File(args[1]);
156 } else {
157 throw new IllegalArgumentException("Must specify one file to read (and optionally a file to write to).");
158 }
159
160 File inFile = new File(args[0]);
161 String base = MiscIO.removeFileExtension(inFile.getName());
162
163 go(inFile,outFile,base,false,new PrintWriter(System.out));
164 } catch (Throwable t) {
165 t.printStackTrace();
166 System.exit(1);
167 }
168 }
169 }