package acl2s.lib.certify;
	
	import java.io.BufferedReader;
	import java.io.BufferedWriter;
	import java.io.File;
	import java.io.FileReader;
	import java.io.FileWriter;
	import java.io.IOException;
	import java.io.PrintWriter;
	
	import org.peterd.util.io.MiscIO;
	
	import acl2s.lib.parse.EmptyParse;
	import acl2s.lib.parse.ParseException;
	import acl2s.lib.parse.StringParser;
	import acl2s.lib.parse.obj.Cons;
	import acl2s.lib.parse.obj.LispObject;
	import acl2s.lib.parse.obj.Str;
	import acl2s.lib.parse.obj.Sym;
	
	public class MaybeExtractPreamble {
		static final String oldprefix = "#|$ACL2-A2S-PREAMBLE$;";
		static final String prefix = "#|$ACL2s-Preamble$;";
		static final String oldpostfix = ";$ACL2-A2S-PREAMBLE$|#";
		static final String postfix = ";$ACL2s-Preamble$|#";
		
		static void go(File lispFile) throws IOException, ParseException {
			String fullBase = MiscIO.removeFileExtension(lispFile.getAbsolutePath());
			String base = MiscIO.removeFileExtension(lispFile.getName());
			File outFile = new File(fullBase + ".acl2");
	
			go(lispFile,outFile,base,false, null);
		}
		
		static void go(File lispFile, boolean force, PrintWriter commentary) throws IOException, ParseException {
			String fullBase = MiscIO.removeFileExtension(lispFile.getAbsolutePath());
			String base = MiscIO.removeFileExtension(lispFile.getName());
			File outFile = new File(fullBase + ".acl2");
	
			go(lispFile, outFile, base, force, commentary);
		}
		
		static void go(File inFile, File outFile, String base, boolean force, PrintWriter commentary)
		throws IOException, ParseException {
			String line;
			BufferedWriter bw;
			String preamble = null;
			PrintWriter c = commentary;
			

			if (!force && outFile.exists() &&
					inFile.lastModified() <= outFile.lastModified()) {
				if (c != null) c.println("Preamble file already up to date.");
				return;
			}
	
			

			if (c != null) c.print("Reading preamble... ");
			
			BufferedReader br = new BufferedReader(new FileReader(inFile));
			
			do {
				line = br.readLine();

				if (line == null) {
					// no preamble

					if (c != null) c.println("none found.");

					if (outFile.exists()) {
						// just touch output file
						if (c != null) c.println("Touching existing .acl2 file.");
						outFile.setLastModified(System.currentTimeMillis());
						return;
					} else {
						// use a default

						if (c != null) c.print("Using default... ");
						preamble = "(begin-book t :skip-proofs-okp t :defaxioms-okp t :ttags :all)\n";
					}

				} else if (line.endsWith(prefix) || line.endsWith(oldprefix)) {
					// extract preamble

					if (c != null) c.print("extracting... ");
					StringBuilder pBuilder = new StringBuilder();
					
					for(;;) {
						line = br.readLine();

						if (line == null) break;

						if (line.endsWith(postfix)) {
							pBuilder.append(line.substring(0, line.length() - postfix.length()));
							pBuilder.append('\n');
							break;
						}

						if (line.endsWith(oldpostfix)) {
							pBuilder.append(line.substring(0, line.length() - oldpostfix.length()));
							pBuilder.append('\n');
							break;
						}
						pBuilder.append(line);
						pBuilder.append("\n");
					}
					
					preamble = pBuilder.toString();
				} // else keep looking for start of preamble

			} while (preamble == null);
	
			br.close();
			
			StringParser parser = new StringParser(null, preamble);
			int lastFormStart = -1;
			for (;;) {
				parser.skipSpaceAndComments();

				if (parser.eof()) break;
				lastFormStart = parser.getPos();
				acl2s.lib.parse.no_obj.LispObject.parse(parser);
			}

			if (lastFormStart < 0) throw new EmptyParse();
			
			parser.setPos(lastFormStart);
			
			LispObject lastForm = LispObject.parseOne(parser);
			

			if (!(lastForm instanceof Cons) ||

				!(((Cons)lastForm).car instanceof Sym) ||

				!(((Sym)((Cons)lastForm).car).sym.equals("BEGIN-BOOK"))) {
				throw new ParseException("Malformed preamble (does not end in begin-book form).");
			}
			
			LispObject cdr = ((Cons)lastForm).cdr;
			
			LispObject newLastForm =
				new Cons(Certifier.certifyBookSym,
						new Cons(new Str(base),
								new Cons(Certifier.questionSym, cdr)));
			

			if (c != null) c.print("saving... ");

			bw = new BufferedWriter(new FileWriter(outFile, false));
			

			bw.write(preamble.substring(0, lastFormStart));
			bw.write("\n");
			bw.write(newLastForm.toString());
			bw.write("\n");
	
			bw.flush();
			bw.close();
			if (c != null) c.println("done.");
		}
		
		public static void main(String[] args) {
			try {
				if (args.length < 1) {
					throw new IllegalArgumentException("Must specify one file to read (and optionally a file to write to).");
				}
	
				File outFile;
				if (args.length == 1) {
					String fullBase = MiscIO.removeFileExtension(args[0]);
					outFile = new File(fullBase + ".acl2");
				} else if (args.length == 2) {
					outFile = new File(args[1]);
				} else {
					throw new IllegalArgumentException("Must specify one file to read (and optionally a file to write to).");
				}
	
				File inFile = new File(args[0]);
				String base = MiscIO.removeFileExtension(inFile.getName());
	
				go(inFile,outFile,base,false,new PrintWriter(System.out));
			} catch (Throwable t) {
				t.printStackTrace();
				System.exit(1);
			}
		}
	}