package acl2s.lib.session;
	
	import java.io.File;
	import java.io.IOException;
	import java.io.InputStreamReader;
	import java.io.OutputStreamWriter;
	import java.io.Serializable;
	import java.util.ArrayList;
	import java.util.HashMap;
	import java.util.Map;
	import java.util.Set;
	import java.util.concurrent.locks.Lock;
	import java.util.concurrent.locks.ReentrantLock;
	
	import org.peterd.util.Misc;
	import org.peterd.util.io.AsyncWriter;
	import org.peterd.util.io.LineReader;
	import org.peterd.util.process.InterruptibleProcess;
	
	import acl2s.lib.parse.IPackageDefinition;
	import acl2s.lib.parse.IParseContext;
	import acl2s.lib.parse.PackageDefinition;
	import acl2s.lib.parse.ParseContext;
	import acl2s.lib.parse.ParseException;
	import acl2s.lib.parse.obj.Cons;
	import acl2s.lib.parse.obj.Int;
	import acl2s.lib.parse.obj.LispObject;
	import acl2s.lib.parse.obj.NotListException;
	import acl2s.lib.parse.obj.Num;
	import acl2s.lib.parse.obj.Rat;
	import acl2s.lib.parse.obj.Str;
	import acl2s.lib.parse.obj.Sym;
	import acl2s.lib.parse.obj.Zero;
	import acl2s.lib_driver.IAcl2sLibDriver;
	import acl2s.lib_driver.IAcl2sLibErrorHandler;
	import acl2s.lib_driver.IAcl2sLibThreadManager;
	
	public class InteractiveSession {
		protected InterruptibleProcess proc;
		protected boolean busy;
		protected Lock outReadLock;
		protected AsyncWriter acl2Input;
		protected LineReader acl2Output;
		protected StatusData status;
		protected EnvData env;
		protected EnvData oldEnv;
		protected final IAcl2sLibErrorHandler errorHandler;
		protected final IAcl2sLibThreadManager threadMgr;
		protected final ISessionConfig config;
		protected final File workingDir;
		protected final Killer killer;
		protected long secret;
		protected boolean interruptPending;
		protected String[] cmdLine;
		protected HashMap<String,IPackageDefinition> pkgDefs = new HashMap<String, IPackageDefinition>();
		
		public InteractiveSession(IAcl2sLibDriver driver, ISessionConfig config, File workingDir) {
			proc = null;
			this.config = config;
			this.workingDir = workingDir;
			errorHandler = driver.getErrorHandler();
			threadMgr = driver.getThreadManager();
			killer = new Killer();
			pkgDefs.putAll(BootstrapParseContext.pkgs);
		}
	
		public synchronized void beginInit() throws IOException, IllegalStateException {
			if (proc != null)  throw new IllegalStateException();
			cmdLine = config.getBaseConfig().getCmdLine();
			proc = InterruptibleProcess.exec(cmdLine, workingDir, config.getBaseConfig(), true);
			acl2Input = new AsyncWriter(new OutputStreamWriter(proc.getStdin())).fork();

			acl2Output = new LineReader(new InputStreamReader(proc.getStdout()));
			busy = true;
			interruptPending = false;
			outReadLock = new ReentrantLock();
			status = new StatusData();
			status.success = true;  // so that startup appears to succeed
			oldEnv = new EnvData();
			env = null;
			secret = Misc.random.nextLong() & 0xfffffffffffffffL;
	
			// Initial input stuff
			String[] startup = config.getStartup(secret);
			if (startup != null) {
				for (int i = 0; i < startup.length; i++) {
					acl2Input.write(startup[i]);
				}
			}
		}
		
		public synchronized IResultInfo fullInit() throws IllegalStateException, IOException, SessionDeadException {
			beginInit();
			try {
				return finishCmd();
			} catch (SessionNotBusyException e) {
				// shouldn't happen
				throw new IllegalStateException(e);
			}
		}
		
		public void dispose() {
			kill();
		}
		
		public void close() throws SessionStateException {
			close(1000);
		}
		
		public synchronized void close(int millis) throws SessionStateException {
			if (proc == null) return;
			if (busy) throw new SessionBusyException();
			if (env == null) throw new SessionStateException();
			try {
				acl2Input.write("#.\n(acl2s::clear-acl2s-password " + secret + " acl2::state)\n(acl2::value :q)\n(acl2::good-bye)\n");
				acl2Input.close();
				busy = true;
			} catch (IOException ioe) {
				errorHandler.warning("Error while closing ACL2 session.", ioe);
			} finally {
				try {
					proc.waitFor(millis);
				} catch (Exception e) {
					proc.kill();
				}
				proc = null;
			}
		}
		
		public synchronized boolean interrupted() {
			return interruptPending || status.interrupted;
		}
		
		public synchronized void interrupt() throws SessionDeadException, SessionNotBusyException {
			if (proc == null) throw new SessionDeadException();
			if (!busy && env != null) throw new SessionNotBusyException();
			if (interrupted()) return;
			try {
				proc.interrupt();
				busy = true;
				interruptPending = true;
			} catch (IOException ioe) {
				errorHandler.error("Error while interrupting ACL2 session.", ioe);
				proc.kill();
				proc = null;
				return;
			}
		}
	
		/*
		public void abort() throws SessionDeadException, SessionStateException {
			miscInput("#.");
		}
		
		public synchronized void interruptOrAbort()	throws SessionDeadException {
			try {
				if (busy || env == null) {
					interrupt();
				} else if (env == null || env.inWormhole()) {
					abort();
				}
			} catch (SessionStateException sse) {
				// shouldn't happen
			}
		}
		//*/
		
		public synchronized boolean isAlive() {
			return proc != null;
		}
		
		// call this if you already have the mutex or don't mind waiting
		public synchronized void kill() {
			try {
				close();
			} catch (SessionStateException e) {
				if (proc != null) {
					proc.kill();
					proc = null;
				}
			}
		}
		
		class Killer implements Runnable {
			public void run() {
				kill();
			}
		}
			
		// call this if you don't want to wait for this mutex
		public void forkKill() {
			threadMgr.delayedExec(killer, 0, true);
		}
		
		public Runnable getKiller() { return killer; }
		
		
		static final Sym WITH_LIMIT = Sym.bootstrapCreate("WITH-PROVER-TIME-LIMIT");
		static final int LIMIT_DENOM = 1000;
		static final float LIMIT_MAX = Integer.MAX_VALUE / LIMIT_DENOM;
		
		public synchronized IResultInfo systemCmd(LispObject cmd, float proverTimeLimit)
		throws SessionDeadException, SessionStateException {
			if (proverTimeLimit <= 0f || proverTimeLimit >= LIMIT_MAX) throw new IllegalArgumentException();
	
			Num limit = Rat.create((int)(proverTimeLimit * LIMIT_DENOM) + 1, LIMIT_DENOM);
			return systemCmd(new Cons(WITH_LIMIT,
					         new Cons(limit,
					         new Cons(cmd, Sym.nilInstance))));
		}
		
		public synchronized IResultInfo systemCmd(LispObject cmd)
		throws SessionDeadException, SessionStateException {
			return systemCmd(cmd.toString(env.getParseContext()));
		}
		
		public synchronized IResultInfo systemCmd(String cmd, float proverTimeLimit)
		throws SessionDeadException, SessionStateException {
			if (proverTimeLimit <= 0f || proverTimeLimit >= LIMIT_MAX) throw new IllegalArgumentException();
			
			String num = Integer.toString((int)(proverTimeLimit * LIMIT_DENOM) + 1, env.getReadBase());
			String denom = Integer.toString(LIMIT_DENOM, env.getReadBase());
			return systemCmd("(ACL2::WITH-PROVER-TIME-LIMIT " + num + "/" + denom + " " + cmd + ")");
		}
		
		public synchronized IResultInfo systemCmd(String cmd)
		throws SessionDeadException, SessionStateException {
			userCmd(cmd);
			return finishCmd();
		}
		
		public synchronized void userCmd(String s)
		throws SessionDeadException, SessionStateException {
			if (s == null) {
				status = new StatusData();
				return;
			}
			if (proc == null) throw new SessionDeadException();
			if (busy) throw new SessionBusyException();
			if (env == null) throw new SessionStateException("Not accepting commands at the moment.");
			status = new StatusData();
			oldEnv = env;
			env = null;
			try {
				acl2Input.write(s);
				acl2Input.write('\n');
				//acl2Input.flush();
				busy = true;
			} catch (IOException ioe) {
				errorHandler.error("Error while writing command input to ACL2.", ioe);
				kill();
			}
		}
	
		public synchronized void miscInput(LispObject obj) throws SessionDeadException, SessionStateException {
			miscInput(obj.toString());
		}
		
		public synchronized void miscInput(String s) throws SessionDeadException, SessionStateException {
			if (proc == null) throw new SessionDeadException();
			if (busy) throw new SessionBusyException();
			if (env != null) throw new SessionStateException("Not expecting non-command input.");
			try {
				acl2Input.write(s);
				acl2Input.write('\n');
				//acl2Input.flush();
				busy = true;
			} catch (IOException ioe) {
				errorHandler.error("Error while writing misc input to ACL2.", ioe);
				kill();
			}
		}
		
		public synchronized IResultInfo finishCmd() throws SessionDeadException, SessionNotBusyException {
			if (!busy) {
				if (isAlive()) {
					throw new SessionNotBusyException();
				} else {
					throw new SessionDeadException();
				}
			}
			StringBuilder ret = new StringBuilder();
			String s;
			for (;;) {
				s = readLineUntilPrompt();
				if (s == null) return new Result(ret.toString(),status);
				ret.append(s);
			}
		}
		
		private transient final ArrayList<String> lines = new ArrayList<String>();
		public String[] readLinesUntilPrompt(int max) {
			String first = readLineUntilPrompt();
			if (first == null) return null;
			
			lines.clear();
			lines.add(first);
			for (;;) {
				if (max > 0 && lines.size() >= max) break;
				if (!acl2Output.ready()) {
					try {
						Thread.sleep(100);
					} catch (InterruptedException e) {
						// ignore
					}
					if (!acl2Output.ready()) {
						break;
					}
				}
				String line = readLineUntilPrompt();
				if (line == null) {
					break;
				} else {
					lines.add(line);
				}
			}
			return lines.toArray(new String[lines.size()]);
		}
		
		static final String SUCCESS = "${SuCcEsS}$\n";
		static final int SUCCESS_LEN = SUCCESS.length();
		
		static final String BEGIN_PKG = "$DeFpKg{$\n";
		static final int BEGIN_PKG_LEN = BEGIN_PKG.length();
		static final String END_PKG = "$DeFpKg}$\n";
		static final int END_PKG_LEN = END_PKG.length();
	
		static final String BEGIN_ENV = "$EnViRoNmEnT{$\n";
		static final int BEGIN_ENV_LEN = BEGIN_ENV.length();
		static final String MIDDLE_ENV = "$EnViRoNmEnT$";
		static final int MIDDLE_ENV_LEN = MIDDLE_ENV.length();
		static final String END_ENV = "$EnViRoNmEnT}$\n"; 
		static final int END_ENV_LEN = END_ENV.length();
		
		static final String READ_OBJECT = "${ReAd-ObJeCt}$\n";
		static final int READ_OBJECT_LEN = READ_OBJECT.length();
		
		private transient final StringBuilder buf = new StringBuilder(100);	
		public String readLineUntilPrompt() {
			if (!outReadLock.tryLock()) throw new IllegalStateException("Multiple threads trying to read.");
			try {
				String s;
				int start;
				synchronized (this) {
					if (proc == null) throw new SessionDeadException();
					if (!busy) return null;
				}
				boolean lineRead;
				buf.setLength(0);
				lineRead = acl2Output.readLineTo(buf);
				if (!lineRead) throw new SessionDeadException();
				buf.append('\n');
				s = buf.toString();
				synchronized (this) {
					if (interruptPending && MyBaseConfig.isConsoleInterrupt(s)) {
						interruptPending = false;
						status.interrupted = true;
					}
				}
				
				if (s.endsWith("$\n")) { // optimization: check for common suffix
	
					if (s.endsWith(SUCCESS)) {
						synchronized (this) {
							status.success = true;
						}
						s = s.substring(0,s.length() - SUCCESS_LEN);
					}
	
					if (s.endsWith(BEGIN_ENV)) {
						start = s.length() - BEGIN_ENV_LEN;
						// slow but rare:
						while (!s.endsWith(END_ENV)) {
							lineRead = acl2Output.readLineTo(buf);
							if (!lineRead) throw new SessionDeadException();
							buf.append('\n');
							s = buf.toString();
						}
						int end = s.indexOf(MIDDLE_ENV);
						if (end < start + BEGIN_ENV_LEN) {
							errorHandler.error("Bad environment output from ACL2.  Aborting session.", null);
							throw new SessionDeadException();
						}
						String sub = s.substring(start + BEGIN_ENV_LEN,end);
						synchronized (this) {
							env = new EnvData();
							try {
								LispObject o = LispObject.canonicalParseFirst(sub);
								
								processPrompt(o);
							} catch (ParseException pe) {
								errorHandler.error("Erroroneous environment output from ACL2.  Aborting session.", pe);
								throw new SessionDeadException();
							}
							String pr = s.substring(end + MIDDLE_ENV_LEN, s.length() - END_ENV_LEN);
							env.setPrompt(pr);
						}
	
						s = s.substring(0,start);
					}
	
					if (s.endsWith(BEGIN_PKG)) {
						start = s.length() - BEGIN_PKG_LEN;
						// slow but rare enough:
						while (!s.endsWith(END_PKG)) {
							lineRead = acl2Output.readLineTo(buf);
							if (!lineRead) throw new SessionDeadException();
							buf.append('\n');
							s = buf.toString();
						}
						
						String defStr = s.substring(start + BEGIN_PKG_LEN, s.length() - END_PKG_LEN);
						
						try {
							LispObject defObj = LispObject.canonicalParseFirst(defStr);
							Cons defCons = (Cons) defObj;
							String pkgName = ((Str)defCons.car).value;
							LispObject[] importObjs = Cons.listToArray(defCons.cdr);
							Sym[] imports = new Sym[importObjs.length];
							System.arraycopy(importObjs, 0, imports, 0, importObjs.length);
							IPackageDefinition def = new PackageDefinition(pkgName, imports);
							synchronized (this) {
								pkgDefs.put(pkgName, def);
							}
						} catch (ClassCastException e) {
							errorHandler.error("Erroroneous package definition output from ACL2.  Aborting session.", e);
							throw new SessionDeadException();
						} catch (ArrayStoreException e) {
							errorHandler.error("Erroroneous package definition output from ACL2.  Aborting session.", e);
							throw new SessionDeadException();
						} catch (ParseException e) {
							errorHandler.error("Erroroneous package definition output from ACL2.  Aborting session.", e);
							throw new SessionDeadException();
						} catch (NotListException e) {
							errorHandler.error("Erroroneous package definition output from ACL2.  Aborting session.", e);
							throw new SessionDeadException();
						}
						
						s = s.substring(0,start);
					}
					
					if (s.endsWith(READ_OBJECT)) {
						s = s.substring(0,s.length() - READ_OBJECT_LEN);
						synchronized (this) {
							if (!interruptPending) {
								busy = false;
								notifyAll();
							} else {
								s = s + "\n(interruption arrived after completion of above)";
								
								// if win32 SBCL with my ctrl+c hack, poke it to get interrupt to happen 
								//acl2Input.write("#+sbcl-ctrlc-hack (acl2::mv (acl2::time-limit4-reached-p \"foo\") :invisible acl2::state)\n");
							}
						}
					}
				}
				
				return s;
			} catch (SessionDeadException sde) {
				synchronized (this) {
					status.interrupted = true;
					status.success = false;
					if (proc != null) {
						proc.kill();
						proc = null;
					}
				}
				return null;
			} catch (IOException ioe) {
				synchronized (this) {
					if (proc == null) return null;
					status.interrupted = true;
					status.success = false;
					kill();
				}
				errorHandler.error("Error while reading ACL2 output.", ioe);
				return null;
			} finally {
				outReadLock.unlock();
			}
		}
		
		protected synchronized void processPrompt(LispObject obj) throws ParseException {
			env.fromObjAndPkgDefs(obj, pkgDefs);
			status.superDone = env.superDone;
			status.extendedWorld = env.superDone > oldEnv.superDone;
			if (env.ldLevel > oldEnv.ldLevel) { // another way success can happen
				status.success = true;
			}
		}
		
		public long getSecret() { return secret; }
		public IEnvInfo getEnvInfo() { return env; }
		public IStatusInfo getStatusInfo() { return status; }
		
		static class StatusData implements IStatusInfo, Serializable {
			private static final long serialVersionUID = 3L;
			
			boolean extendedWorld = false;
			boolean interrupted = false;
			boolean success = false;
			int superDone;
			
			public boolean wasInterrupted() {
				return interrupted;
			}
	
			public boolean wasSuccess() {
				return success;
			}
	
			public boolean extendedLogicalState() {
				return extendedWorld;
			}
	
			public int getSuperDoneSize() {
				return superDone;
			}
		}
	
		static Set<String> bootstrapPkgs = BootstrapParseContext.instance.getBootstrapPackages();
		
		static class EnvData extends ParseContext implements IEnvInfo, Serializable {
			private static final long serialVersionUID = 2L;
			
			String prompt;
			int ldLevel;
			int superDone;
			int superUndone;
			int eventIndex;
			boolean inWormhole;
			boolean inRawMode;
			
			EnvData() {
				ldLevel = 1;
				superDone = 1;
				superUndone = 0;
				pkgs = new HashMap<String, IPackageDefinition>();
			}
			
			void fromObjAndPkgDefs(LispObject obj, Map<String,IPackageDefinition> pkgDefs) throws ParseException {
				try {
					Cons lst = (Cons)obj;
					defltPackage = ((Str)lst.car).value;
					
					lst = (Cons)(lst.cdr);
					ldLevel = ((Int)lst.car).v.intValue();
					
					lst = (Cons)(lst.cdr);
					inWormhole = !(lst.car instanceof Zero);
					
					lst = (Cons)(lst.cdr);
					inRawMode = !(lst.car instanceof Zero);
					
					lst = (Cons)(lst.cdr);
					LispObject[] pkgNames = Cons.listToArray(lst.car);
					
					pkgs.clear();
					for (LispObject o : pkgNames) {
						String pkgName = ((Str)o).value; 
						pkgs.put(pkgName, pkgDefs.get(pkgName));
					}
					
					lst = (Cons)(lst.cdr);
					eventIndex = ((Int)lst.car).v.intValue();
	
					lst = (Cons)(lst.cdr);
					superDone = ((Int)lst.car).v.intValue();
					
					lst = (Cons)(lst.cdr);
					superUndone = ((Int)lst.car).v.intValue();
				} catch (ClassCastException cce) {
					throw new ParseException("Invalid prompt data.");
				} catch (NotListException e) {
					throw new ParseException("Invalid prompt data.");
				}
			}
	
			void setPrompt(String s) {
				prompt = s;
			}
			
			public int getLdLevel() {
				return ldLevel;
			}
	
			public String getPakage() {
				return getDefaultPackage();
			}
	
			public String getPrompt() {
				return prompt;
			}
			
			public int getLastEventIndex() {
				return eventIndex;
			}
			
			public boolean inWormhole() {
				return inWormhole;
			}
	
			public boolean inRawMode() {
				return inRawMode;
			}
	
			public int getSuperDoneSize() {
				return superDone;
			}
	
			public int getSuperUndoneSize() {
				return superUndone;
			}
	
			public IParseContext getParseContext() {
				return this;
			}
	
			public void forgetRedo() {
				superUndone = 0;
			}
		}
		
		static class Result implements IResultInfo {
			private static final long serialVersionUID = 2L;
	
			final String output;
			final boolean interrupted;
			final boolean success;
			final boolean affectedWorld;
			final int superDone;
			
			public Result(String output, StatusData p) {
				this.output = output;
				this.interrupted = p.interrupted;
				this.success = p.success;
				this.affectedWorld = p.extendedWorld;
				this.superDone = p.superDone;
			}
			
			public String getOutput() {
				return output;
			}
	
			public boolean wasInterrupted() {
				return interrupted;
			}
	
			public boolean wasSuccess() {
				return success;
			}
	
			public boolean extendedLogicalState() {
				return affectedWorld;
			}
	
			public int getSuperDoneSize() {
				return superDone;
			}
		}
		
		public String[] getCmdLine() {
			return cmdLine;
		}
		
		public ISessionConfig getConfig() {
			return config;
		}
	}