package acl2s.lib.parse.obj;
	
	import java.util.HashMap;
	
	import org.peterd.util.Misc;
	
	import acl2s.lib.parse.IPackageDefinition;
	import acl2s.lib.parse.IPackageWorld;
	import acl2s.lib.parse.NoSuchPackageException;
	import acl2s.lib.parse.ObjectNotSupported;
	import acl2s.lib.parse.IParseContext;
	import acl2s.lib.parse.ParseException;
	import acl2s.lib.parse.Parser;
	import acl2s.lib.parse.SymOrNumFns;
	import acl2s.lib.session.BootstrapParseContext;
	
	// interning allows us to compare sym and pack with ==
	public class Sym extends SymOrNum {
		private static final long serialVersionUID = 1L;
	
		public final String pack;
		public final String sym;
		
		Sym(String pack, String s) {
			this.pack = pack.intern();
			this.sym = s.intern();
		}
		
		String computeString(IParseContext pc) {
			String defPkg = pc == null ? null : pc.getDefaultPackage();
			StringBuilder b = new StringBuilder();
			if (pack.equals(keywordPkgName)) {
				b.append(":");
			} else {
				boolean prependPackage = true;
				
				try {
					if (Misc.equal(defPkg,pack) ||
						   (pc != null &&     // kill warning
							defPkg != null && // subsumes `pc != null`
							Misc.equal(pc.internedPackage(defPkg,sym),pack))) {
						prependPackage = false;
					}
				} catch (NoSuchPackageException e) {
					// shouldn't happen that default package doesn't exist
				}
				
				if (prependPackage) {
					b.append(partToString(pack));
					b.append("::");
				}
			}
			b.append(partToString(sym));
			return b.toString();
		}
		
		public static String partToString(String s) {
			int len = s.length();
			if (len == 0) {
				return barredToString(s);
			}
			if (len > 0) {
				char c = s.charAt(0);
				if (Character.isDigit(c)) {
					return barredToString(s);
				}
				if (c == '-' && len > 1) {
					return barredToString(s);
				}
				if (c == '_' || c == '^') {
					return barredToString(s);
				}
			}
			for (int i = 0; i < len; i++) {
				if (!isSafe(s.charAt(i))) {
					return barredToString(s);
				}
			}
			return s;
		}
		
		static String barredToString(String s) {
			StringBuilder b = new StringBuilder();
			b.append('|');
			for (int i = 0; i < s.length(); i++) {
				char c = s.charAt(i);
				if (c == '\\' || c == '|') {
					b.append('\\');
				}
				b.append(c);
			}
			b.append('|');
			return b.toString();
		}
	
		public boolean isNil() {
			return this == nilInstance;
		}
	
		public boolean probablyNil() {
			return sym == "NIL";
		}
		
		public boolean isKeyword() {
			return pack == keywordPkgName;
		}
	
		public boolean isACL2ConstantName() {
			return
				this == nilInstance ||
				this == tInstance ||
				(sym.length() > 2 && sym.startsWith("*") && sym.endsWith("*"));
		}
	
		public boolean isACL2EventName() {
			return !isKeyword() && !pack.equals(mainLispPkgName);
		}
		
		public boolean isACL2VariableName() {
			return !isKeyword() && !isACL2ConstantName() && !isReservedLLKeyword() &&
			  (pack != mainLispPkgName || BootstrapParseContext.acl2Pkg.internedPackage(sym) == mainLispPkgName);
		}
		
		public boolean isReservedLLKeyword() {
			return sym.startsWith("&");
		}
		
		public boolean interned() { return true; }
		
		public Sym resolve(IParseContext pc) throws ParseException {
			return this;
		}
		
		public boolean equals(Object o) {
			return this == o;  // because of database
		}
		
		public int hashCode() {

			return sym.hashCode() + (pack != null ? pack.hashCode() * 3 : 42);
		}
	
		public int hashcode() {
			return super.hashCode(); // because of database
		}
		
		public static Sym parse(Parser p) throws ParseException {
			char c = p.peek();
			if (c == '(') {
				p.advance(1);
				p.skipSpaceAndComments();
				if (p.peek() != ')') {
					throw new ParseException("Expected: ()");
				}
				p.advance(1);
				return nilInstance;
			}
			if (c == '.') {
				int i = 1;
				while (p.peek(i) == '.') i++;
				if (SymOrNumFns.isTerminator(p.peek(i))) {
					p.advance(i);
					throw new ParseException("Illegal dot(s).");
				}
			} else if (c == '#') {
				p.advance(1);
				p.skipToTerminator();
				throw new ParseException("Unrecognized #-sequence");
			}
			if (SymOrNumFns.isTerminator(p.peek())) {
				p.skip();
				throw new ParseException("Symbol expected.");
			}
			StringBuilder s1 = new StringBuilder();
			boolean mustBeExternal = false;
			boolean firstCharColon = false;
			c = p.peek();
			if (c == ':' && p.peek(1) != ':') {
				firstCharColon = true;
				p.skip();
				// p.skipSpace(); // GCL-ism.  not portable
				c = p.peek();
				if (SymOrNumFns.isTerminator(c)) {
					throw new ParseException("For portability, symbol syntax must immediately follow package delimiter.");
				}
			}
			while (!SymOrNumFns.isTerminator(c) && (firstCharColon || c != ':')) {
				if (c == '\\') {
					c = p.next();
					if (c == Parser.EOF) throw new ParseException("EOF after \\.");
					s1.append(c);
				} else if (c == '|') {
					c = p.next();
					while (c != '|' && c != Parser.EOF) {
						if (c == '\\') {
							c = p.next();
							if (c == Parser.EOF) throw new ParseException("EOF after \\.");
							s1.append(c);
						} else if (c == '\n' || c == '\r') {
							throw new ParseException("Unescaped newlines in symbols are not supported in ACL2s.");
						} else {
							s1.append(c);
						}
						c = p.next();
					}
					if (c == Parser.EOF) throw new ParseException("EOF before matching |.");
				} else {
					s1.append(Character.toUpperCase(c));
				}
				c = p.next();
			}
			if (firstCharColon) {
				return create(p.getContext(),keywordPkgName,s1.toString());
			} else if (c == ':') {
				StringBuilder s2 = new StringBuilder();
				p.skip();
				if (p.peek() == ':') {
					p.skip();
				} else {
					mustBeExternal = true;
				}
				// p.skipSpace(); // GCL-ism.  not portable
				c = p.peek();
				if (SymOrNumFns.isTerminator(c)) {
					throw new ParseException("For portability, symbol syntax must immediately follow package delimiter.");
				}
				do {
					if (c == '\\') {
						c = p.next();
						if (c == Parser.EOF) throw new ParseException("EOF after \\.");
						s2.append(c);
					} else if (c == '|') {
						c = p.next();
						while (c != '|' && c != Parser.EOF) {
							if (c == '\\') {
								c = p.next();
								if (c == Parser.EOF) throw new ParseException("EOF after \\.");
								s2.append(c);
							} else if (c == '\n' || c == '\r') {
								throw new ParseException("Unescaped newlines in symbols are not supported in ACL2s.");
							} else {
								s2.append(c);
							}
							c = p.next();
						}
						if (c == Parser.EOF) throw new ParseException("EOF before matching |.");
					} else if (c == ':') {
						p.skipToTerminator();
						throw new ParseException("Extra : after :: in symbol designator.");
					} else {
						s2.append(Character.toUpperCase(c));
					}
					c = p.next();
				} while (!SymOrNumFns.isTerminator(c));
				if (mustBeExternal) {
					throw new ObjectNotSupported("External symbol references not supported in ACL2.  Use '::'.");
				}
				return create(p.getContext(),s1.toString(),s2.toString());
			} else {
				return create(p.getContext(),s1.toString());
			}
		}
		
		public static Sym createACL2(IParseContext pc, String sym) {
			try {
				return create(pc,acl2PkgName,sym);
			} catch (ParseException e) {
				e.printStackTrace(); // won't happen
				return null;
			}
		}
		
		public static Sym createKeyword(String sym) {
			return SymDb.get(keywordPkgName, sym); // never any imports, etc.
		}
		
		public static Sym create(IParseContext pc, String sym) throws ParseException {
			return create(pc,null,sym);
		}
		
		public static Sym create(IParseContext pc, String pack, String sym) throws ParseException {
			if (pack == null) {
				if (pc != null) {
					pack = pc.getDefaultPackage();
				}
				if (pack == null) { // don't know what package it's supposed to go in
					return new UnpackagedSym(sym);
				}
			}
			String pkgNameError = checkPkgName(pack);
			if (pkgNameError != null) {
				throw new ObjectNotSupported(pkgNameError);
			}
			String truePack = null;
			if (pc != null) {
				truePack = pc.internedPackage(pack,sym); // could throw NoSuchPackageException
			}
			if (truePack == null) { // unknown how it should be interned
				return new UninternedSym(pack,sym);
			} else {
				return SymDb.get(truePack,sym);
			}
		}
	
		public static Sym create(IPackageWorld pwrld, String pack, String sym) throws NoSuchPackageException {
			if (pack == null) {
				return new UnpackagedSym(sym);
			}
			if (pwrld != null) {
				IPackageDefinition pdef = pwrld.getPackageDefinitions().get(pack);
				if (pdef == null) throw new NoSuchPackageException(pack);
				return SymDb.get(pdef.internedPackage(sym),sym);
			} else {
				return new UninternedSym(pack,sym);
			}
		}
		
		public static Sym bootstrapCreate(String string) {
			try {
				return create(BootstrapParseContext.instance,acl2PkgName,string);
			} catch (ParseException e) {
				// impossible;
				return null;
			}
		}
		
		// this is a little wacky in ACL2 because any non-empty string is allowed as a package name
		public static Sym pkgWitness(String pkg) {
			if (pkg == null || pkg.length() == 0) pkg = "ACL2";
			return SymDb.get(pkg, witnessName);
		}
		
		public static String checkPkgName(String pkg) {
			int len = pkg.length();
			if (len == 0) {
				return "The empty string is not a valid ACL2 package name.";
			}
			for (int i = 0; i < len; i++) {
				if (Character.isLowerCase(pkg.charAt(i))) {
					return "ACL2 package names may not contain lower-case characters.";
				}
			}
			if (pkg.startsWith("ACL2_*1*_")) {
				return "An ACL2 package name may not start with \"ACL2_*1*_\".  These are used internally.";
			}
			return null; // all good
		}
		
		public static Sym bool(boolean b) {
			return b ? tInstance : nilInstance;
		}
		
		// string constants automatically interned
		public static final String acl2PkgName = "ACL2";
		public static final String mainLispPkgName = "COMMON-LISP";
		public static final String keywordPkgName = "KEYWORD";
		public static final String witnessName = "ACL2-PKG-WITNESS";
		
		static class SymDb {
			static final HashMap<String,Sym> map = new HashMap<String,Sym>();
			public synchronized static Sym get(String pack, String sym) {
				Sym ret;
				String key = pack + '\0' + sym;
				ret = map.get(key);
				if (ret == null) {
					ret = new Sym(pack,sym);
					map.put(key,ret);
				}
				return ret;
			}
		}
	
		public static final Sym functionInstance = SymDb.get(mainLispPkgName,"FUNCTION");
		public static final Sym appendInstance = SymDb.get(mainLispPkgName,"APPEND");
		public static final Sym quoteInstance = SymDb.get(mainLispPkgName,"QUOTE");
		public static final Sym consInstance = SymDb.get(mainLispPkgName,"CONS");
		public static final Sym nilInstance = SymDb.get(mainLispPkgName,"NIL");
		public static final Sym tInstance = SymDb.get(mainLispPkgName,"T");
		
		public static final boolean isSafe(char c) {
			return c < safeLookup.length && safeLookup[c];
		}
		static final String safe = "ABCDEFGHIJKLMNOPQRSTUVWXYZ1234567890*/{}[]<>?+=-_&^%$@!~";
	
		static boolean[] safeLookup;
		static {
			int x = -1;
			for (int i = 0; i < safe.length(); i++) {
				if (safe.charAt(i) > x) {
					x = safe.charAt(i);
				}
			}
			safeLookup = new boolean[x + 1];  // initialized to falses
			for (int i = 0; i < safe.length(); i++) {
				safeLookup[safe.charAt(i)] = true;
			}
		}
	}