#!/usr/bin/python

import os, sys, re, platform
from datetime import datetime

#html
NA_HTML = '-'

#latex
VERIFIED_TEX = '\\verified{}'
FALSIFIED_TEX = '\\falsified{}'
NA_TEX = '--'

###########################################################
WARNING_REGEX = r'^\s*WARNING\: (\d+ wellformedness check failed)\!$'
LEMMA_REGEX = r'^\s*(\w+) \((all-traces|exists-trace)\): (.+ \(\d+ steps\))$'
RULE_HEADER_REGEX = r'^rule \(modulo E\) (\w+)\:$'
RULE_HEADER_SPTHY_REGEX = r'^rule (\w+)\:$'
TIME_REGEX = r'^real\s([\dmsh\.\,]+)$'
GNU_TIME_REGEX = r'^.*\s([\d\:\.\,]+)elapsed.*$'
STEPS_REGEX = r'( - found trace| - no trace found)? \(\d+ steps\)'

def to_timeformat(time):
	hours = int(time / 3600)
	time -= hours * 3600
	mins = int(time / 60)
	time  -= mins * 60
	secs = time

	if mins + hours > 0:
		if hours > 0:
			tt = str(hours) + 'h'\
						+ '{:02d}'.format(mins) + 'm'\
						+ '{0:02.0f}'.format(secs) + 's'
		else:
			tt = str(mins) + 'm' + '{0:02.0f}'.format(secs) + 's'
	else:
		tt = '{0:.0f}'.format(secs) + 's'
	
	return tt

def differ_for_hline(prev_proto_name, proto_name):
	if prev_proto_name == '': return False
	try:
		return proto_name.split('_')[:1] != prev_proto_name.split('_')[0:1]
	except:
		return False
	#return False

def to_secs(time):
	t = 0.0
	if 'h' in time:
		t += int(time.split('h')[0]) * 3600
		time = time.split('h')[1]
	if 'm' in time:
		t += int(time.split('m')[0]) * 60
		time = time.split('m')[1]
	t += float(time.split('s')[0])
	return t

def list_to_table_entry(items, verified, proto_idx):
	html_list = []		
	for idx in range(len(items)):
		if idx == proto_idx and items[proto_idx] in verified:
			html_list.append('<td class="verified">'+items[proto_idx]+'</td>')
		else:
			_class = ''
			if items[idx].startswith('falsified'):
				_class = ' class="red"'
			elif "verified" in items[idx]:
				_class = ' class="green"'		
			
			html_list += '<td'+_class+'>' + items[idx] + '</td>'			
	return '<tr>' + ''.join(html_list) + '</tr>'

def create_html_code(directories, columns, tex_replace):

	print 'Starting collecting results...'

	global_results = []
	cols = ['No.', 'Protocol']

	rules_min = 100000000
	rules_max = -1
	rules_sum = 0

	loc_min = 100000000
	loc_max = -1
	loc_sum = 0

	time_sum = 0.0
	time_min = 1000000000.0
	time_max = 0.0

	proto_count = 0
	files = []
	for dir in directories:
		if not dir.endswith('/'): dir += '/'
		try:
			if os.getcwd() == os.path.abspath(dir):
				files += [file for file in os.listdir('./') if '.proof' in file]
			else:
				files += [dir + file for file in os.listdir(dir) if '.proof' in file]
		except:
			print '[Error] Invalid directory:', dir
			return None

	files.sort()
	files.reverse() #reverse order happens to be better

	for file in files:
		results = {}
		proto = file.replace('.proof', '')
		print 'Parsing', proto
		
		proto_count += 1
		results['No.'] = str(proto_count)
		results['Protocol'] = os.path.basename(proto)
		
		lines = open(file).readlines()
		for line in lines:
			col = None
			m = re.match(WARNING_REGEX, line)
			if m:
				col = 'WARNING'
				result = m.group(1)
			else:
				m = re.match(LEMMA_REGEX, line)
				if m:
					(col, result) = m.group(1,3)				

			if col:
				results[ col ] = result.strip()
				if col not in cols:
					cols.append(col)
					
		#rules
		rule_names = []
		for line in lines:
			m = re.match(RULE_HEADER_REGEX, line)
			if m : rule_names.append(m.group(1))
		
		num_rules = len(rule_names)
		if num_rules < rules_min: rules_min = num_rules
		if num_rules > rules_max: rules_max = num_rules			
		rules_sum += num_rules
		results['Rules'] = str(num_rules)

		if os.path.exists(proto + '.spthy'):
			#inspect the spthy file for diff in rule names
			for line in open(proto + '.spthy').readlines():
				m = re.match(RULE_HEADER_SPTHY_REGEX, line)
				if m and m.group(1) not in rule_names:
					print '[Warning] Rule "' + m.group(1) + '" occurs in "' + proto\
								+ '.spthy" but not in "' + proto + '.proof"'
			#lines of code
			loc = len(open(proto + '.spthy').readlines())
			if loc < loc_min: loc_min = loc
			if loc > loc_max: loc_max = loc
			loc_sum  += loc
			results['LoC'] = str(loc)
		else:
			print '[Warning] No theory file found for:', proto

		#timings
		time_display = None
		for line in lines:
			res = re.match(TIME_REGEX, line)
			if res:
				t = res.group(1)
				t = to_secs (t)					
				time_display = to_timeformat(t)
				time_sum += t
				if t < time_min: time_min = t
				if t > time_max: time_max = t
			else:
				#try to parse GNU time format
				res = re.match(GNU_TIME_REGEX, line)
				if res:
					t = res.group(1).replace(':', 'h')
					i = t.rfind('h')
					t = to_secs (t[:i]+ 'm' + t[i+1:] + 's')					
					time_display = to_timeformat(t)
					time_sum += t
					if t < time_min: time_min = t
					if t > time_max: time_max = t									
			
		if time_display:
			results['Time'] = time_display
		
		global_results.append(results)

	#global_results.sort(key=protocol_name)
	
	# move 'WARNING' column to the third position		
	#if 'WARNING' in cols:
	#	index = cols.index('WARNING')
	#	cols = ['No.', 'Protocol', 'WARNING'] + cols[2:index] + cols[index+1:]
	#	cols = cols[:index] + cols[index+1:] + ['WARNING']

	#check that the result of lemma x matches that of lemma x_minimal
	for results in global_results:
		x_group = {}
		for (col, res) in results.iteritems():
			key = col.replace('_minimal', '')
			res = re.sub(STEPS_REGEX, '', res)				
			if key not in x_group:
				x_group[key] = set()
			x_group[key].add(res)
		
		differ = [k for (k,v) in x_group.iteritems() if len(v) > 1]
		for col in differ:
			print '[Warning] The results of lemmas "' + col\
						+ '" and "' + col +'_minimal" differ for:', results['Protocol']
	
	# add 'Rules', 'LoC' and 'Time' columns
	cols = cols + ['Rules', 'LoC', 'Time']

	if columns != 'all': cols = columns

	#list verified protocols
	verified = []
	for res in global_results:
		results = [v for (k,v) in res.iteritems() if k in cols]
		i = 0
		while i < len(results):
			if results[i].startswith('falsified'):
				break
			i += 1
		if i == len(results):
			verified.append(res['Protocol'])

	#HTML code
	html = '<!DOCTYPE html><html>\
					<head><style>\
					.main {\
						font-size: .9em;\
						margin: .8em;\
						font-family: arial, sans-serif;\
					}\
					table {\
						border-collapse: collapse;\
					}\
					td, th {\
						text-align: left;\
						padding: 10px;\
					}\
					th {\
						background-color: #2471A3;\
						color: white;\
						font-weight: normal;\
					}\
					tr:nth-child(odd) {\
						background-color: #f2f2f2;\
					}\
					tr:hover {\
						background-color: #D6EAF8;\
					}\
					.summary {\
						line-height: 1.2em;\
					}\
					.verified {\
					}\
					.verified {\
						//background-color: #4CAF50;\
						//color: white;\
						font-weight: bold;\
					}\
					.green {\
						color: green;\
					}\
					.red {\
						color: red;\
					}\
					.x-scrollable {\
						overflow-x: auto;\
						white-space: nowrap;\
					}\
					.latex-code {padding: .5em;\
						font-family: Consolas, "courier new";\
						background-color: #f2f2f2;}\
					</style></head>'
	html += '<body><div class="main">'

	#table ==============================================
	html += '<h2>Analysis results</h2><div class="x-scrollable"><table>'
	
	#table head
	html += '<tr>' + ''.join(['<th>' + col + '</th>' for col in cols]) + '</tr>'	
	#start constructing latex code
	tex = '\\begin{tabular}{' + '&nbspl'*len(cols) +' }<br/>\\hline<br/>\
				\\bfseries&nbsp' +\
				'&nbsp\\bfseries&nbsp'.join(cols) + '\\\\<br/>\\hline<br/>'
	
	prev_proto_name = ''
	idx = cols.index('Protocol')		
	#table body
	for results in global_results:
		results_list = []
		for col in cols:
			res = NA_HTML
			if col in results:
				res = results[col]
				if res.startswith('analysis incomplete'):
					res = NA_HTML
			results_list.append(res)
			
		html += list_to_table_entry(results_list, verified, idx)

		#start constructing latex code
		latex_results = []
		for r in results_list:
			r = re.sub(STEPS_REGEX, '', r)
			r = r.replace('verified', VERIFIED_TEX)
			r = r.replace('falsified', FALSIFIED_TEX)
			r = r.replace(NA_HTML, NA_TEX)
			latex_results.append(r)
		
		if results_list[idx] in verified:
			latex_results = latex_results[:idx]\
											+ ['\\bfseries ' + latex_results[idx]]\
											+ latex_results[idx+1:]

		proto_name = results_list[idx]
		#replace with latex annotations in file
		if tex_replace != None:
				if proto_name in tex_replace:
					for (col_name, repl) in tex_replace[proto_name].iteritems():
						try:
							col_idx = cols.index(col_name)
							latex_results[col_idx] = repl
						except:
							print "[Warning] Couldn't replace in tex, result of '"\
										+ col_name +"' for protocol '"+ proto_name + "' does not exist"
		
		'''latex_results = latex_results[:idx]\
										+ ['\\modelfont{' + latex_results[idx]+'}']\
										+ latex_results[idx+1:]'''
		#separate blocks
		if differ_for_hline(prev_proto_name, proto_name): tex += '\\hline<br/>'
		prev_proto_name = proto_name
		
		tex += '&nbsp&&nbsp'.join(latex_results) + '\\\\<br/>'

	tex += '\\hline<br/>\\end{tabular}<br/>'
	html += '</table></div>'
	
	#summary ===============================================
	html += '<h2>Summary</h2><div class="summary">\
					<p><b>Protocols: </b> '\
					+ 'total ' + str(proto_count) + ', '\
					+ 'verified ' + str(len(verified)) + '</p>'
	
	if proto_count != 0:		
		ave = (0.0+rules_sum)/proto_count
		html += '<p><b>Number of rules:</b> '\
						+ "min " + str(rules_min) + ', '\
						+ "ave " + str(int(ave)) + ', '\
						+ "max " + str(rules_max) + '</p>'
		
		if loc_sum != 0:
			ave = (0.0+loc_sum)/proto_count
			html += '<p><b>Lines of code:</b> '\
						+ "min " + str(loc_min) + ', '\
						+ "ave " + str(int(ave)) + ', '\
						+ "max " + str(loc_max) + '</p>'
		
		ave = time_sum/proto_count
		html += '<p><b>Time:</b> '\
					+ "min " + to_timeformat(time_min) + ', '\
					+ "ave " + to_timeformat(ave) + ', '\
					+ "max " + to_timeformat(time_max) + ', '\
					+ "sum " + to_timeformat(time_sum) + '</p>'
	#html += '<p><b>System info:</b> " + str(platform.uname()) + '</p>'
	html += '<p><b>Folder(s):</b> ' + ', '.join(directories) + '</p>'
	#html += '<p><b>Report generated on:</b> '\
	#				+ datetime.now().strftime("%Y-%m-%d %H:%M:%S") + '</p>'					
	html += '</div>'

		
	#latex code ========================================
	html += '<h2>Latex code</h2><div class="latex-code x-scrollable">'
	tex = tex.replace('_', '\\_')
	tex = '%define your \\falsified and \\verified commands here<br/>' + tex
	html += tex +'</div></div></body></html>'
	return html

def main():
	args = sys.argv[1:]

	#defaults
	directories = set()
	lemmas = 'all'
	output = None
	tex_replace = {}
	
	for idx in range(1, len(sys.argv)):
		arg = sys.argv[idx]
		
		if arg.startswith('--lemmas='):
			file = arg.split('=',1)[1]
			try:
				lemmas = []
				for l in open(file).readlines():
					l = re.sub(r'#.*', '', l).strip()
					if l != '': lemmas.append(l)
			except Exception as e:
				#print '[Error] Something went wrong when loading the lemmas from:', file
				print e
				return
				
			if 'Protocol' not in lemmas:
				print '[Error] No "Protocol" column found in:', file
				return
		
		elif arg.startswith('--output='):
			output = arg.split('=',1)[1]
		
		elif arg.startswith('--tex-replace='):
			file = arg.split('=',1)[1]
			try:
				for line in open(file).readlines():
					if line.strip() == '' or line.startswith('#'):
						continue
					(proto, lemma, repl) = line.split(' ',2)
					if proto not in tex_replace:
						tex_replace[proto] = {}					
					if lemma not in tex_replace[proto]:
						tex_replace[proto][lemma] = {}
					tex_replace[proto][lemma] = repl[:-1]
			except Exception as e:
				print '[Warning] Something went wrong with the tex notes file:', file\
							+ ', so it will be ignored' 
				print e
				tex_replace = {}
		
		else:
			directories.add(arg)

	if len(directories) == 0:
		directories = ['./']

	if not output:
		tail = '-'.join([os.path.abspath(dir).split('/')[-1] for dir in directories])
		if tail != '':
			tail = '-' + tail
		output = 'results' + tail + '.html'

	html = create_html_code(directories, lemmas, tex_replace)
	
	if html:
		print 'Writing output to:', os.path.basename(output)
		outfile = open(output, 'w')
		outfile.write(html)
		outfile.close()
		print 'Done.'

main()
