package acl2s.plugin.indent;
	
	import java.util.Arrays;
	import java.util.HashSet;
	import java.util.Set;
	
	import org.eclipse.jface.text.BadLocationException;
	import org.eclipse.jface.text.IDocument;
	
	import acl2s.plugin.parse.LispToken;
	import acl2s.plugin.parse.LispTokens;
	
	public class DefaultLispIndent implements ILispIndent {
		protected final LispTokens tokens;
		protected final IDocument doc;
		
		public DefaultLispIndent(LispTokens tokens, IDocument doc) {
			this.tokens = tokens;
			this.doc = doc;
		}
	
		int getExistingBasicIndention(int line) throws BadLocationException {
			int start = doc.getLineOffset(line);
			int end = start + doc.getLineLength(line);
	
			int indent = 0;
			for (int i = start; i < end; i++) {
				char ch = doc.getChar(i);
				if (ch == ' ') {
					indent++;
				} else if (ch == '\t') {
					indent += 4;  // fallback;  shouldn't be tabs
				} else if (ch == '\n' || ch == '\r') {
					return -1;  // all space
				} else {
					return indent;
				}
			}
			return -1;  // all space & eof
		}
		
		public int getExistingLineIndention(int line) throws BadLocationException {
			if (line < 0) return 0;
			int start = doc.getLineOffset(line);
			LispToken t = tokens.getToken(tokens.getTokenIdxContaining(start));
			if (line > 0) {
				if (t.isLiteralMode(start-1,doc)) {
					return getExistingLineIndention(line-1);
				}
			}
			int end = start + doc.getLineLength(line);
			
			// hack to eliminate prompt
			if (t.type == LispToken.NONE_TOK && t.absoluteEnd() <= end) {
				start = t.absoluteEnd();
			}
			
			int indent = getExistingBasicIndention(line);
			if (indent >= 0) {
				return indent;
			} else {
				// nothing on line => do previous line
				return getExistingLineIndention(line - 1);
			}
		}
		
		// called from autoindenter, etc.
		public int getNextIndentionFrom(int offset) {
			return getNextIndentionFrom(offset, false);
		}
		
		protected int getNextIndentionFrom(int offset, boolean fromParam) {
			try {
				int tIdx;
				if (offset < doc.getLength()) {
					tIdx = tokens.getTokenIdxContaining(offset);
				} else {
					tIdx = tokens.getTokenCount() - 1;
				}
				LispToken t = tokens.getToken(tIdx);
				if (t.offset >= offset) { // if we're only preceded by space in this token
					if (t.inHashComment(offset - t.offset)) return -2; // no change, autoindent is fine
					tIdx--;
					if (tIdx < 0) return 0;
					t = tokens.getToken(tIdx);
				} else if (t.isLiteralMode(offset, doc)) { // newline interpreted *not* as whitespace
					if ((t.type == LispToken.STRING_TOK && doc.getChar(offset-1) == '~')
							|| t.type == LispToken.DOC_TOK) {
						// indent inside string if doc string or ~\n (as in fmt string)
						int line = doc.getLineOfOffset(offset);
						int lstart = doc.getLineOffset(line);
						while (t.offset < lstart) {
							// search for non-empty line to indent from
							// while start of string is before this line
							int indent = getExistingBasicIndention(line);
							if (indent >= 0) {
								return indent;
							}
							line--;
							lstart = doc.getLineOffset(line);
						}
						// else we've reached start of string, which is on this line
						if (t.type == LispToken.DOC_TOK) {
							return t.offset - lstart;  // to conform to ACL2 source conventions
						} else {
							return t.offset - lstart + 1;
						}
					} else {
						return -1; // no change, no autoindent
					}
				}
				
				int line = doc.getLineOfOffset(offset);
				if (!fromParam && t.absoluteEnd() < offset) {
					line = doc.getLineOfOffset(t.absoluteEnd());
				}
				int maxTIdx = tIdx;
				int lstart = doc.getLineOffset(line);
				int lstartTIdx = tokens.getTokenIdxContaining(lstart);
	
				while (lstart > 0 && line > 0 && 
						tokens.getToken(lstartTIdx).isLiteralMode(lstart-1, doc)) {
					line--;
					lstart = doc.getLineOffset(line);
					lstartTIdx = tokens.getTokenIdxContaining(lstart);
				}
				
				// hack to eliminate prompt
				LispToken st = tokens.getToken(lstartTIdx);
				if (st.type == LispToken.NONE_TOK) {
					lstart = st.absoluteEnd();
				}
				
				int balance = 0;
				for (tIdx = maxTIdx; tIdx >= lstartTIdx && balance < 1; tIdx--) {
					t = tokens.getToken(tIdx);
					balance += t.parenDelta();
					if (balance > 0) {
						break;
					}
				}
				
				if (balance > 0) {
					int indent = t.absoluteEnd() - lstart;
					if (tIdx + 1 <= maxTIdx) {
						LispToken fn = tokens.getToken(tIdx + 1);
						if (fn.type == LispToken.SYM_TOK) {
							String fName = doc.get(fn.offset,fn.length);

							fName = fName.toLowerCase();
							if (fName.startsWith("def") || indentNameSet.contains(fName)) {
								return indent + 1;
							}
						}
						if ((fn.type == LispToken.SYM_TOK && !(doc.getChar(fn.offset) == ':')) // sym but ot keyword
								|| fn.type == LispToken.STRING_TOK) {
							if (tIdx + 2 <= maxTIdx || fromParam) { // also a function and >= 1 parameter following
								LispToken param1 = tokens.getToken(tIdx + 2);
								indent = param1.offset - lstart;
							}
						}
					}
					return indent;
				}
				
				if (balance == 0) return getExistingLineIndention(line);
				
				// balance < 0
				for (tIdx = maxTIdx; tIdx >= lstartTIdx; tIdx--) {
					t = tokens.getToken(tIdx);
					if (t.isCParen()) {
						break;
					}
				}
				tIdx = tokens.matchParenTok(tIdx);
				if (tIdx < 0) return 0;
				t = tokens.getToken(tIdx);
				line = doc.getLineOfOffset(Math.min(offset,t.absoluteEnd()));
				lstart = doc.getLineOffset(line);
				return getNextIndentionFrom(t.offset,true);  // RECURSION!!
			} catch (BadLocationException e) {
				// impossible
				e.printStackTrace();
				return 0;
			}
		}
	
		public void indentLine(int line) {
			try {
				int docLen = doc.getLength();
				int start = doc.getLineOffset(line);
				int space = 0;
				int semis = 0;
				boolean allSpace = true;
				for (;;) {
					if (start+space >= docLen) break;
					char ch = doc.getChar(start+space);
					if (ch != ' ' && ch != '\t') {
						if (ch != '\r' && ch != '\n') allSpace = false;
						for (;;) {
							int i = start+space+semis;
							if (i >= docLen || doc.getChar(i) != ';') break;
							semis++;
						}
						break;
					}
					space++;
				}
	
				LispToken t;
				if (start > 0) {
					t = tokens.getToken(tokens.getTokenIdxContaining(start - 1));
				} else if (docLen > 0) {
					t = tokens.getToken(tokens.getTokenIdxContaining(start));
				} else {
					t = null;
				}
				
				boolean toBeginning = false;
				if (t != null &&
						t.offset >= start + doc.getLineLength(line) && // if the line is all whitespace
						!allSpace) { // and there's text in the line (comments)
					if (semis == 0 || semis >= 3) {
						return;  // don't change indent
					} else {				
						toBeginning = semis == 1;
					}
				}
				
				if (line == 0 || toBeginning) {
					if (space == 0) return; // no change
					doc.replace(start, space, "");
				} else {
					int indent = 0;
					indent = getNextIndentionFrom(start-1);
					if (indent < 0) return;  // indent shouldn't be changed (e.g. literal mode)
					if (indent == space) return; // no change
					String text = LispAutoIndent.getSpaces(indent);
					doc.replace(start, space, text);
				}
			} catch (BadLocationException e) {
				e.printStackTrace();
			}
		}
		
		String[] indentNames = new String[] { // def* automatically indented
				"let", "let*", "if" /*, "cond"  NO! */ /*"mv-let", NO! */ 
				, "er-let*", "assign", "theorem", "encapsulate"
		};
		Set<String> indentNameSet = new HashSet<String>(Arrays.asList(indentNames));
		
		
	}