package acl2s.lib.session;
	
	import java.io.BufferedReader;
	import java.io.File;
	import java.io.FileReader;
	import java.io.IOException;
	import java.net.URISyntaxException;
	import java.net.URL;
	import java.util.ArrayList;
	import java.util.Arrays;
	import java.util.HashSet;
	import java.util.Iterator;
	import java.util.LinkedList;
	import java.util.List;
	import java.util.Map;
	
	import org.peterd.util.Misc;
	
	import acl2s.lib.parse.obj.Sym;
	import acl2s.lib_driver.IAcl2sLibErrorHandler;
	import acl2s.lib_example.BasicInteractiveSessionConfig;
	
	public class MyBaseConfig implements IBaseConfig {
		private static final long serialVersionUID = 2L;
	
		public MyBaseConfig(IAcl2sLibErrorHandler err, File hooksHome, File acl2Home, File[] modeHomes) {
			this.err = err;
			this.hooksHome = hooksHome;
			this.acl2Home = acl2Home;
			updateForNewHooksHome();
			updateForNewAcl2Home();
			addModeHomes(modeHomes);
		}
	
		protected IAcl2sLibErrorHandler err;
		protected File acl2Home;
		protected String htmlHomeUrl;
		protected String[] pathsToTry;
		
		protected File hooksHome;
		protected String hooksAcl2Path;
		
		protected ModeDir[] modeDirs = {}; // after update, dependency-respecting sequence 
		protected SessionMode[] modes = { SessionMode.compatible }; // kept as sequence of all known modes
		protected String modeAddIncludeBooks = "";
		
		public void setHooksHome(File f) {
			if (!Misc.equal(f, hooksHome)) {
				hooksHome = f;
				updateForNewHooksHome();
			}
		}
	
		protected void updateForNewHooksHome() {
			if (hooksHome == null) {
				hooksAcl2Path = null;
			} else {
				hooksAcl2Path = toAcl2PathDir(hooksHome);
			}
		}
		
		public String getHooksAcl2Path() {
			return hooksAcl2Path;
		}
		
		public File getHooksHome() {
			return hooksHome;
		}
	
		
		public void setAcl2Home(File f) {
			if (!Misc.equal(f, acl2Home)) {
				acl2Home = f;
				updateForNewAcl2Home();
			}
		}
		
		protected void updateForNewAcl2Home() {
			htmlHomeUrl = findHtmlHome(acl2Home);
			pathsToTry = findPaths(acl2Home);
		}
		
		
		public void addModeHomes(File... modeHomes) {
			if (modeHomes == null || modeHomes.length == 0) return;
			
			LinkedList<ModeDir> phase1 = new LinkedList<ModeDir>();
			for (File modeHome : modeHomes) {
				ModeDir d = ModeDir.maybeCreate(err, modeHome);
				if (d != null) {
					phase1.add(d);
				}
			}
			if (phase1.size() == 0) return;
			phase1.addAll(Arrays.asList(modeDirs));
			updateModes(phase1);
		}
		
		public void removeModeHomes(File... removeHomes) {
			if (removeHomes == null || removeHomes.length == 0) return;
			ArrayList<ModeDir> toRemove = new ArrayList<ModeDir>();
			for (File home : removeHomes) {
				ModeDir d = lookupModeDir(home);
				if (d != null) {
					toRemove.add(d);
				}
			}
			removeModeDirs(toRemove);
		}
		
		public void removeModeDirs(ModeDir... removeDirs) {
			removeModeDirs(Arrays.asList(removeDirs));
		}
		
		public void removeModeDirs(List<ModeDir> removeDirs) {
			if (removeDirs == null || removeDirs.size() == 0) return;
			
			LinkedList<ModeDir> phase1 = new LinkedList<ModeDir>();
			phase1.addAll(Arrays.asList(modeDirs));
			if (!phase1.removeAll(removeDirs)) return;
			
			updateModes(phase1);
		}
		
		static Sym systemKeyword = Sym.createKeyword("SYSTEM");
		
		protected void updateModes(LinkedList<ModeDir> phase1) {
			// order to satisfy dependencies
			ArrayList<ModeDir> phase2 = new ArrayList<ModeDir>(phase1.size());
			boolean added;
			HashSet<Sym> dirSyms = new HashSet<Sym>(phase1.size());
			dirSyms.add(systemKeyword);
			do {
				added = false;
				Iterator<ModeDir> rem = phase1.iterator();
				while (rem.hasNext()) {
					ModeDir modeDir = rem.next();
					boolean sat = true;
					for (Sym dep : modeDir.deps) {
						if (!dirSyms.contains(dep) && !Misc.equal(dep, modeDir.includeBookDirSym)) {
							sat = false;
						}
					}
					if (sat) {
						phase2.add(modeDir);
						rem.remove();
						if (modeDir.includeBookDirSym != null) {
							dirSyms.add(modeDir.includeBookDirSym);
							added = true;;
						}
					}
				}
			} while (added);
			
			
			for (ModeDir bad : phase1) {
				err.error("Mode dir has unsatisfied dependencies: " + bad.home.getAbsolutePath(), null);
			}
	
			modeDirs = phase2.toArray(new ModeDir[phase2.size()]);
			
			ArrayList<SessionMode> allModes = new ArrayList<SessionMode>();
			allModes.add(SessionMode.compatible);
			StringBuilder addInclBook = new StringBuilder();
			for (ModeDir modeDir : modeDirs) {
				addInclBook.append(modeDir.getAddIncludeBookDirString());
				for (SessionMode mode : modeDir.modes) {
					allModes.add(mode);
				}
			}
			modes = allModes.toArray(new SessionMode[allModes.size()]);
			Arrays.sort(modes);  // by precedence
			modeAddIncludeBooks = addInclBook.toString();
		}
		
		
		public String getDocBaseURL() {
			return htmlHomeUrl;
		}
		
		public String[] getCmdLine() {
			String cmd = fallbackCmd;
			for (String path : pathsToTry) {
				File f = new File(path);
				if (f.exists()) {
					cmd = path;
					break;
				}
			}
			return new String[] { cmd };
		}
	
	
		public void setupEnvironment(Map<String, String> env) {
			// script should set ACL2_SYSTEM_BOOKS better than we can
			env.put("ACL2-CUSTOMIZATION", "NONE"); // we will load it if we want it
		}
	
		public String getACL2sDocURL() {
			return Versions.getAcl2sDocInternetURLString();
		}
	
		public SessionMode[] getModes() {
			return modes;
		}
	
		public SessionMode getDefaultMode() {
			return modes[0];
		}
	
		public ModeDir[] getModeDirs() {
			return modeDirs;
		}
		
		public String getModeAddIncludeBooks() {
			return modeAddIncludeBooks;
		}
		
		public SessionMode lookupMode(String name) {
			for (SessionMode m : modes) {
				if (m.getName().equalsIgnoreCase(name)) {
					return m;
				}
			}
			return null;
		}
	
		public ModeDir lookupModeDir(File home) {
			for (ModeDir modeDir : modeDirs) {
				if (modeDir.home.equals(home)) {
					return modeDir;
				}
			}
			return null;
		}
		
		public ModeDir lookupModeDir(Sym dir) {
			for (ModeDir modeDir : modeDirs) {
				if (modeDir.includeBookDirSym == dir) {
					return modeDir;
				}
			}
			return null;
		}
		
		// ********************** STATIC STUFF ********************** //
		
		public static File getACL2HomeFromEnvironment() {
			return acl2HomeFromEnvironment;
		}
		
		public static File getHooksHomeFromEnvironment() {
			return hooksHomeFromEnvironment;
		}
		
		static final File acl2HomeFromEnvironment = findAcl2HomeFromEnvironment();
		static final File hooksHomeFromEnvironment = findHooksHomeFromEnvironment();
		
		static File findAcl2HomeFromEnvironment() {
			String tmp = System.getenv("ACL2_HOME");
			if (tmp == null || ! new File(tmp).isDirectory()) {
				tmp = System.getProperty("ACL2_HOME");
			}
			if (tmp == null || ! new File(tmp).isDirectory()) {
				tmp = System.getProperty("acl2.home");
			}
			if (tmp == null || ! new File(tmp).isDirectory()) {
				return null;
			} else {
				return new File(tmp).getAbsoluteFile();
			}
		}
		
		static File findHooksHomeFromEnvironment() {
			String tmp;
			tmp = System.getenv("ACL2S_HOOKS");
			if (tmp != null) {
				File f = new File(tmp);
				if (f.isDirectory()) {
					return f;
				}
			}
			tmp = System.getProperty("ACL2S_HOOKS");
			if (tmp != null) {
				File f = new File(tmp);
				if (f.isDirectory()) {
					return f;
				}
			}
			tmp = System.getProperty("acl2s.hooks");
			if (tmp != null) {
				File f = new File(tmp);
				if (f.isDirectory()) {
					return f;
				}
			}
			try {
				URL u = BasicInteractiveSessionConfig.class.getResource("hooks/preinit.lsp");
				if (u != null) {
					File f = new File(u.toURI()).getParentFile();
					if (f.isDirectory()) {
						return f;
					}
				}
			} catch (IllegalArgumentException e) {
			} catch (URISyntaxException e) {
			}
			try {
				URL u = BasicInteractiveSessionConfig.class.getResource("../hooks/preinit.lsp");
				if (u != null) {
					File f = new File(u.toURI()).getParentFile();
					if (f.isDirectory()) {
						return f;
					}
				}
			} catch (IllegalArgumentException e) {
			} catch (URISyntaxException e) {
			}
			return null; // could not find
		}
		
		
		
		public static final String fallbackCmd = "acl2";
		
		
		
		public static String findHtmlHome(File acl2HomeOption) {
			String tmp = null;
			if (acl2HomeOption != null) {
				File f = new File(new File(acl2HomeOption, "doc"), "HTML");
				if (new File(f, "acl2-doc.html").exists()) {
					tmp = "file://" + toAcl2PathDir(f);
				}
			}
			if (tmp == null) {
				tmp = Versions.getAcl2DocInternetURLString();
			}
			return tmp;
		}
		
		//harshrc:: Acl2HomeOption can be 
		//1. ACL2 build path set in eclipse preferences
		//2. ACL2s image plugin path (bundle in eclipse terminology)
		//3. ACL2_HOME environment variable set in OS
		//4. null (in which case we try to execute 'acl2')
		public static String[] findPaths(File acl2HomeOption) {
			boolean windows = File.separatorChar == '\\';
			
			ArrayList<String> paths = new ArrayList<String>();
			
			if (acl2HomeOption != null) {
				String hpath = acl2HomeOption.getAbsolutePath();
				if (windows) {
					paths.add(hpath + File.separator + "run_acl2.exe");
					paths.add(hpath + File.separator + "saved_acl2.bat");
					paths.add(hpath + File.separator + "bin" + File.separator + "acl2.exe");
				} else {
					paths.add(hpath + File.separator + "run_acl2");
					paths.add(hpath + File.separator + "saved_acl2");
				}
			}
			
			if (windows) {
				String minVer = Versions.getAcl2MinVersionString();
				String maxVer = Versions.getAcl2MaxVersionString();
				
				paths.add("C:\\ACL2-" + maxVer + "\\bin\\acl2.exe");
				paths.add("C:\\Program Files\\ACL2 " + maxVer + "\\bin\\acl2.exe");
				if (! minVer.equals(maxVer)) {
					paths.add("C:\\ACL2-" + minVer + "\\bin\\acl2.exe");
					paths.add("C:\\Program Files\\ACL2 " + minVer + "\\bin\\acl2.exe");
				}
			}
			
			return paths.toArray(new String[paths.size()]);
		}
	
		/*
		static final Sym BOOK_DEV = Sym.createKeyword("BOOK-DEV");
		static final Sym TTAGS = Sym.createKeyword("TTAGS");
		static final Sym IMPORTS = Sym.createKeyword("IMPORTS");
		static final Sym PRECEDENCE = Sym.createKeyword("PRECEDENCE");
		
		public static SessionMode[] getModesFromHome(File root) {
			try {
				File[] modeFiles = root.listFiles();
				ArrayList<SessionMode> foundModes = new ArrayList<SessionMode>(modeFiles.length);
				for (File mf : modeFiles) {
					if (!mf.getName().toLowerCase().endsWith("mode.lsp")) continue;
					try {
						FileInputStream stream = new FileInputStream(mf);
						LispObject[] md = LispObject.parseAll(new StreamParser(BootstrapParseContext.instance, stream));
						stream.close();
						if (md.length < 4) throw new ParseException("Expecting at least four lisp objects in file " + mf);
						if (!(md[0] instanceof Str) ||
								!(md[1] instanceof Str) ||
								!(md[2] instanceof Str)) {
							throw new ParseException("First three objects must be strings in file " + mf);
						}
						String name = ((Str)md[0]).value;
						String sdesc = ((Str)md[1]).value;
						String ldesc = ((Str)md[2]).value;
	
						// option defaults
						boolean bookdev = true;
						boolean ttags = false;
						LispObject extraImports = Sym.nilInstance;
						int precedence = Integer.MAX_VALUE;
	
						// options given with keywords
						if (!(md[3].isNil())) {
							try {
								LispObject optLst = Cons.deQuote(md[3]);
								while (!optLst.isNil()) {
									Cons c = (Cons) optLst;
									Sym opt = (Sym) c.car;
									c = (Cons) c.cdr;
									LispObject val = c.car;
									optLst = c.cdr;
	
									if (opt == BOOK_DEV) {
										bookdev = Cons.maybeDeQuote(val).isNotNil();
									} else if (opt == TTAGS) {
										ttags = Cons.maybeDeQuote(val).isNotNil();
									} else if (opt == IMPORTS) {
										// ensure either (unquoted) nil or quoted list
										extraImports = Cons.maybeDeQuote(val);
	
										if (extraImports.isNotNil()) {
											extraImports = Cons.quote(extraImports);
										}
									} else if (opt == PRECEDENCE) {
										val = Cons.maybeDeQuote(val);
										if (val instanceof Int) {
											BigInteger precInt = ((Int) val).v;
											if (precInt.bitLength() <= 31) {
												precedence = precInt.intValue();
											}
										}
									} else {
										// unrecognized
									}
								}
							} catch (Exception e) {
								throw new ParseException("Malformed keyword options in fourth object of file " + mf);
							}
						}
						LispObject[] initData = new LispObject[md.length - 4];
						System.arraycopy(md, 4, initData, 0, initData.length);
						foundModes.add(new SessionMode(root, name, sdesc, ldesc, bookdev, ttags, extraImports, precedence, initData));
					} catch (ParseException pe) {
						System.err.println("Unable to parse mode in registry (" + mf + "): " + pe.toString());
					}
				}
				
				if (foundModes.size() > 0) {
					SessionMode[] modes = foundModes.toArray(new SessionMode[foundModes.size()]);
					Arrays.sort(modes);
					return modes;
				}
				// otherwise, fallback:
			} catch (IOException ioe) {
				System.err.println("While reading mode registry: " + ioe.toString());
			}
			return SessionMode.compatibleOnly;
		}*/
		
		public static File[] getCertifyOrder(File hooksHome) throws IOException {

			BufferedReader r = new BufferedReader(new FileReader(new File(hooksHome, "certify-order.txt")));
			
			ArrayList<File> order = new ArrayList<File>();
			for (;;) {

				String line = r.readLine();

				if (line == null) break;

				if (line.length() > 0 && Character.isLetterOrDigit(line.charAt(0))) {
					File f = new File(hooksHome, line + ".lisp");
					if (f.exists()) {
						order.add(f);
					} else {
						System.err.println("Skipping non-existant hooks file: " + f);
					}
				}
			}
			return order.toArray(new File[order.size()]);
		}
		
		public static boolean isConsoleInterrupt(String line) {
			if (line.startsWith("************ ABORTING from raw Lisp ***********")) {
				return true; // ACL2's abort message, for everything but non-ansi GCL
			}
			if (line.startsWith("debugger invoked")) {
				return true; //harshrc// one of abort messages SBCL
			}
			if (line.startsWith("> Break: interrupt signal")) {
				return true; //harshrc// one of abort messages CCL
			}
			if (line.equals("Error: Console interrupt.\n")) {
				return true; // non-ansi GCL is special
			}
			/* These should not be needed now that we use ACL2's have the ABORTING line
			if (line.startsWith("Error: ")) {
				if (line.startsWith("Error: interrupted ")) {
					return true; // SBCL (older)
				}
				if (line.startsWith("Error: Interactive interrupt ")) {
					return true; // SBCL (newer)
				}
			}
			if (line.startsWith("> Break in process ")) {
				return true; // OpenMCL
			}
			*/
			return false;
		}
	
		public static String toAcl2PathString(String path) {
			if (File.separatorChar == '/') {
				return path;
			} else {
				return path.replace(File.separatorChar, '/');
			}
		}
		
		public static String toSystemPathString(String acl2Path) {
			if (File.separatorChar == '/') {
				return acl2Path;
			} else {
				return acl2Path.replace('/', File.separatorChar);
			}
		}
		
		public static String toAcl2PathFile(File f) {
			return toAcl2PathString(f.getAbsolutePath());
		}
	
		public static String toAcl2PathDir(File f) {
			String path = toAcl2PathFile(f);
			if (!path.endsWith("/")) {
				path += "/";
			}
			return path;
		}
	}