package acl2s.plugin;
	
	import java.io.File;
	import java.util.ArrayList;
	
	import acl2s.lib.contentassist.BareBatchConfig;
	import acl2s.lib.contentassist.FileDictionary;
	import acl2s.lib.contentassist.WorkspaceDictionary;
	import acl2s.lib.parse.Parser;
	import acl2s.lib.session.IBaseConfig;
	import acl2s.lib.session.MyBaseConfig;
	
	import java.io.BufferedReader;
	import java.io.BufferedWriter;
	import java.io.FileWriter;
	import java.io.IOException;
	import java.io.CharArrayWriter;
	
	import org.peterd.util.ExceptionHandler;
	
	import acl2s.lib.session.BatchSession;
	
	
	public class GroundZeroIndexer extends Thread implements ExceptionHandler<IOException> {
		private String acl2path;
		private CharArrayWriter writer;
		private BufferedReader in;
		
		public GroundZeroIndexer(BufferedReader in) {
			this.in = in;
		}
		
		public GroundZeroIndexer(MyBaseConfig baseConfig) {
			this.acl2path = baseConfig.getCmdLine()[0];
			writer = new CharArrayWriter();
			this.in = null;
		}
	
		protected boolean started = false;
		protected boolean finished = false;
		protected boolean killed = false;
		
		public synchronized boolean started() {
			return started;
		}
		
		public synchronized boolean finished() {
			return finished;
		}
	
		protected BatchSession sess = null;
		
		public synchronized void kill() {
			killed = true;
			if (sess != null) {
				sess.kill();
			}
		}
	
			
		protected void finish() {
			synchronized (GroundZeroIndexer.this) {
				sess = null;
				finished = true;
			}
		}
		
		private void load() {
			String line;
			boolean consts = false;
			try {
				
				while ((line = in.readLine()) != null) {
					if (!consts) {
						if (line.equals("$AcL2S-BeGin-ThE-GrOuNdZeRo-DeFcOnStS$")) {
							consts = true;
							continue;
						}
						WorkspaceDictionary.addSymbol(null, line, FileDictionary.CharacterTreeNodeType.DEFUN, -1, 0, null);
					} else {
						WorkspaceDictionary.addSymbol(null, line, FileDictionary.CharacterTreeNodeType.DEFCONST, -1, 0, null);
					}
				}
			} catch (IOException e) {
				return;
			}
		}
	
		public synchronized void start() {
			if (started) throw new IllegalStateException("Already started.");
	
			started = true;
			notifyAll();
			
			if (this.in != null) {
				load();
				return;
			}
			
			IBaseConfig baseConfig = Acl2sPlugin.getBaseConfig();
			String cmd = "(make-event" +
					     "(let* ((defun-code '(defun foo (x) " +
	                                           "(cond ((endp x) nil) " +
	                                                  "((eq (caar x) ':DEFINITION) (cons (cadar x) (foo (cdr x)))) " +
	                                                  "(t (foo (cdr x)))))) " +
	                             "(defun-code2 '(defun bar (wrld) " +
	   					                          "(cond ((endp wrld) nil) " +
	   				                              "((or (not (true-listp (car wrld))) (< (length (car wrld)) 6)) (bar (cdr wrld))) " +
	   					                          "(t (let ((etyp (caar wrld)) " +
	   					                         "(prop (cadar wrld)) " +
	   					                         "(body (cdddr (car wrld)))) " +
	   					                          "(cond ((and (eq etyp 'acl2::event-landmark) " +
	   					                          "(eq prop 'acl2::global-value) " +
	                                                 "(eq (car body) 'ACL2::DEFCONST))"  +
	                                                 "(cons (cadr body) (bar (cdr wrld)))) " +
	   					                          "(t (bar (cdr wrld))))))))) " +
	                            "(call-code '(let ((world (w state))) (foo (universal-theory :here)))) " +
	                            "(call-code2 '(bar (acl2::w acl2::state)))) " +
				         "(er-progn (ld (list defun-code defun-code2 call-code call-code2) " +
	                     ":ld-prompt nil " +
	                     ":ld-verbose t " +
	                     ":ld-error-triples t " +
	                     ":ld-error-action :error) " +
	                     "(value '(value-triple :passed)))))";
			synchronized (GroundZeroIndexer.this) {
				if (killed) {
					finish();
					return;  // ABORT
				}
				sess = new BatchSession(new BareBatchConfig(baseConfig, cmd), new File("/"));
			}
			
			BatchSession.OutputHandler h = sess.createOutputHandler(writer);
			h.setSnipEnabled(false);
			h.setSnipCaptureEnabled(false);
			h.appendPostEOFhook(new Runnable() {
				public void run () {
					ArrayList<String> results = new ArrayList<String>();
					String toPrune = writer.toString();
					toPrune = toPrune.substring(toPrune.indexOf("(BAR FOO "));
					int startConst = Parser.parseListOfSymbols(toPrune, results, 0);
					BufferedWriter w = null;
					try {

						w = new BufferedWriter(new FileWriter("groundzero.def"));
						w.write(GroundZeroIndexer.this.acl2path + "\n");
					} catch (IOException e) {
						w = null;
					}
					for (int i = 2; i < results.size(); ++i) {
						if (w != null) {
							try {
								w.write(results.get(i) + "\n");
							} catch (IOException e) {
								w = null;
							}
						}
						WorkspaceDictionary.addSymbol(null, results.get(i), FileDictionary.CharacterTreeNodeType.DEFUN, -1, 0, null);
					}
					results.clear();
					if (w != null) {
						try {
							w.write("$AcL2S-BeGin-ThE-GrOuNdZeRo-DeFcOnStS$\n");
						} catch (IOException e) {
							w = null;
						}
					}
					Parser.parseListOfSymbols(toPrune, results, toPrune.indexOf('(', startConst+1));
					for (int i = 0; i < results.size(); ++i) {
						if (w != null) {
							try {
								w.write(results.get(i) + "\n");
							} catch (IOException e) {
								w = null;
							}
						}
						WorkspaceDictionary.addSymbol(null, results.get(i), FileDictionary.CharacterTreeNodeType.DEFCONST, -1, 0, null);
					}
					try {
						if (w != null) w.close();
					} catch (IOException e) {}
				}
			});
			h.setExceptionHandler(GroundZeroIndexer.this);
			
			try {
				sess.init();
			} catch (IOException e) {
				return;
			}
			
			h.start();
		}
		
		public void waitFor() throws InterruptedException {
			synchronized (this) {
				while (!finished) {
					wait();
				}
			}
		}
		
		protected void dispose() {
			kill();
		}
		
		protected synchronized void doHandleException(IOException e) {
			kill();
		}
	
		// STATIC STUFF
		
		public static void ensureStarted(MyBaseConfig baseConfig) {
			if (!Acl2sPlugin.getDefault().inEventThread()) throw new IllegalStateException();
			(new GroundZeroIndexer(baseConfig)).start();
		}
	
		public void handleException(IOException e) {
			// TODO Auto-generated method stub
			
		}
	}