syntax.py

from math import remainder
import fol
import re
from random import randrange, choice

class UnableToParseError(Exception):
	def __init__(self, tokens):
		self.tokens = tokens
		super().__init__("Unable to parse sentence {}".format(tokens))

class AmbiguousParseError(Exception):
	def __init__(self, tokens, logical_forms):
		self.tokens = tokens
		self.logical_forms = logical_forms
		super().__init__("Sentence {} has multiple semantic parses {}".format(tokens, [fol.fol_to_tptp(lf) for lf in logical_forms]))

class SyntaxNode(object):
	def __init__(self, label, children=None):
		self.label = label
		self.children = children

def formula_to_np_prime(formula, morphology, quantified_variable, is_plural, no_adjectives):
	if type(formula) == fol.FOLFuncApplication and len(formula.args) == 1 and type(formula.args[0]) == fol.FOLVariable and formula.args[0].variable == quantified_variable:
		noun = formula.function
		if is_plural:
			noun = morphology.to_plural(noun)
		return SyntaxNode("NP'", [SyntaxNode("N", [SyntaxNode(noun)])])
	elif type(formula) == fol.FOLAnd and type(formula.operands[0]) == fol.FOLFuncApplication and not morphology.is_noun(formula.operands[0].function) and not no_adjectives:
		if len(formula.operands) == 2:
			other = formula.operands[1]
		else:
			other = fol.FOLAnd(formula.operands[1:])
		return SyntaxNode("NP'", [
				formula_to_adjp(formula.operands[0], morphology, quantified_variable),
				formula_to_np_prime(other, morphology, quantified_variable, is_plural, no_adjectives)
			])
	else:
		import pdb; pdb.set_trace()
		raise Exception("formula_to_np_prime ERROR: Unsupported formula type ({}).".format(type(formula)))

def can_be_adjp_np(formula, morphology):
	if type(formula) == fol.FOLFuncApplication:
		return True
	elif type(formula) in (fol.FOLAnd, fol.FOLOr):
		return all([type(operand) == fol.FOLFuncApplication and not morphology.is_noun(operand.function) for operand in formula.operands[:-1]])
	else:
		return False

def formula_to_np(formula, morphology, quantified_variable, is_plural, is_universally_quantified, is_negated, no_adjectives):
	if (type(formula) == fol.FOLOr and is_universally_quantified and not is_plural) or ((no_adjectives or not can_be_adjp_np(formula, morphology)) and type(formula) == fol.FOLAnd and is_universally_quantified and not is_plural):
		child_nodes = []
		for operand in formula.operands:
			if type(operand) == fol.FOLFuncApplication and not morphology.is_noun(operand.function):
				# this operand is predicative (adjectival phrase)
				child_nodes.append(formula_to_adjp(operand, morphology, quantified_variable))
			else:
				# this operand is a noun phrase
				child_nodes.append(formula_to_np(operand, morphology, quantified_variable, is_plural, False, is_negated, no_adjectives))
		has_commas = choice([True, False])
		cnj = ("or" if type(formula) == fol.FOLOr else "and")
		if len(formula.operands) > 2:
			if has_commas:
				result = [SyntaxNode(",")] * (len(child_nodes) * 2 - 1)
				result[0::2] = child_nodes
				child_nodes = result
				child_nodes.insert(len(child_nodes) - 1, SyntaxNode("CC", [SyntaxNode(cnj)]))
			else:
				result = [SyntaxNode("CC", [SyntaxNode(cnj)])] * (len(child_nodes) * 2 - 1)
				result[0::2] = child_nodes
				child_nodes = result
		else:
			child_nodes.insert(len(child_nodes) - 1, SyntaxNode("CC", [SyntaxNode(cnj)]))
		return SyntaxNode("NP", [
				SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("N", [SyntaxNode("everything")])])]),
			    SyntaxNode("SBAR", [
					SyntaxNode("WHNP", [SyntaxNode("that")]),
					SyntaxNode("VP", [
						SyntaxNode("V", [SyntaxNode("is")]),
						SyntaxNode("NP", child_nodes)
					]),
				])
			])

	np_prime = formula_to_np_prime(formula, morphology, quantified_variable, is_plural, no_adjectives)
	if is_negated:
		return SyntaxNode("NP", [
				SyntaxNode("DET", [SyntaxNode("no")]),
				np_prime
			])
	elif is_universally_quantified:
		if is_plural:
			if randrange(1) == 0:
				return SyntaxNode("NP", [np_prime])
			else:
				return SyntaxNode("NP", [
						SyntaxNode("DET", [SyntaxNode("all")]),
						np_prime
					])
		else:
			quantifier = choice(["each", "every"])
			return SyntaxNode("NP", [
					SyntaxNode("DET", [SyntaxNode(quantifier)]),
					np_prime
				])
	else:
		if is_plural:
			return SyntaxNode("NP", [np_prime])
		else:
			return SyntaxNode("NP", [
					SyntaxNode("DET", [SyntaxNode("a")]),
					np_prime
				])

def formula_to_adjp(formula, morphology, quantified_variable):
	if type(formula) == fol.FOLFuncApplication and len(formula.args) == 1 and type(formula.args[0]) == fol.FOLVariable and formula.args[0].variable == quantified_variable:
		adjective = formula.function
		return SyntaxNode("ADJP", [SyntaxNode("ADJ", [SyntaxNode(adjective)])])
	else:
		raise Exception("formula_to_adjp ERROR: Unsupported formula type ({}).".format(fol.fol_to_tptp(formula)))

def formula_to_vp_arg(formula, morphology, quantified_variable, is_plural, no_adjectives):
	if type(formula) == fol.FOLFuncApplication and not morphology.is_noun(formula.function):
		return formula_to_adjp(formula, morphology, quantified_variable)
	elif type(formula) == fol.FOLOr or (type(formula) == fol.FOLAnd and (no_adjectives or not can_be_adjp_np(formula, morphology))):
		child_nodes = []
		for operand in formula.operands:
			if type(operand) == fol.FOLFuncApplication and not morphology.is_noun(operand.function):
				# this operand is predicative (adjectival phrase)
				child_nodes.append(formula_to_adjp(operand, morphology, quantified_variable))
			else:
				# this operand is a noun phrase
				child_nodes.append(formula_to_np(operand, morphology, quantified_variable, is_plural, False, False, no_adjectives))
		has_commas = choice([True, False])
		cnj = ("or" if type(formula) == fol.FOLOr else "and")
		if len(formula.operands) > 2:
			if has_commas:
				result = [SyntaxNode(",")] * (len(child_nodes) * 2 - 1)
				result[0::2] = child_nodes
				child_nodes = result
				child_nodes.insert(len(child_nodes) - 1, SyntaxNode("CC", [SyntaxNode(cnj)]))
			else:
				result = [SyntaxNode("CC", [SyntaxNode(cnj)])] * (len(child_nodes) * 2 - 1)
				result[0::2] = child_nodes
				child_nodes = result
		else:
			child_nodes.insert(len(child_nodes) - 1, SyntaxNode("CC", [SyntaxNode(cnj)]))
		return SyntaxNode("NP", child_nodes)
	else:
		return formula_to_np(formula, morphology, quantified_variable, is_plural, False, False, no_adjectives)

def formula_to_clause(formula, morphology, no_adjectives=False, invert=False):
	if type(formula) == fol.FOLForAll and type(formula.operand) == fol.FOLIfThen:
		# determine if the clause will be singular or plural
		is_plural = choice([True, False])
		if invert:
			is_plural = False
		elif type(formula.operand.antecedent) == fol.FOLOr or (type(formula.operand.antecedent) == fol.FOLAnd and (no_adjectives or not can_be_adjp_np(formula.operand.antecedent, morphology))):
			is_plural = False

		# generate the subject and object phrases
		is_negated = (type(formula.operand.consequent) == fol.FOLNot)
		left = formula_to_np(formula.operand.antecedent, morphology, formula.variable, is_plural, True, False, no_adjectives)
		if is_negated:
			right = formula_to_vp_arg(formula.operand.consequent.operand, morphology, formula.variable, is_plural, no_adjectives)
		else:
			right = formula_to_vp_arg(formula.operand.consequent, morphology, formula.variable, is_plural, no_adjectives)

		verb = ("are" if is_plural else "is")
		if is_negated:
			if invert:
				return SyntaxNode("S", [
						SyntaxNode("V", [SyntaxNode(verb)]),
						left,
						SyntaxNode("VP", [
							SyntaxNode("ADVP", [SyntaxNode("ADV", [SyntaxNode("not")])]),
							right
						])
					])
			else:
				return SyntaxNode("S", [
						left,
						SyntaxNode("VP", [
							SyntaxNode("V", [SyntaxNode(verb)]),
							SyntaxNode("ADVP", [SyntaxNode("ADV", [SyntaxNode("not")])]),
							right
						])
					])
		else:
			if invert:
				return SyntaxNode("S", [
						SyntaxNode("V", [SyntaxNode(verb)]),
						left,
						SyntaxNode("VP", [
							right
						])
					])
			else:
				return SyntaxNode("S", [
						left,
						SyntaxNode("VP", [
							SyntaxNode("V", [SyntaxNode(verb)]),
							right
						])
					])

	elif type(formula) == fol.FOLNot and type(formula.operand) == fol.FOLExists and type(formula.operand.operand) == fol.FOLAnd:
		# determine if the clause will be singular or plural
		is_plural = choice([True, False])

		remaining_conjuncts = formula.operand.operand.operands[1:]
		if len(remaining_conjuncts) == 1:
			remaining_conjuncts = remaining_conjuncts[0]
		else:
			remaining_conjuncts = fol.FOLAnd(remaining_conjuncts)

		# generate the subject and object phrases
		left = formula_to_np(formula.operand.operand.operands[0], morphology, formula.operand.variable, is_plural, False, True, no_adjectives)
		right = formula_to_vp_arg(remaining_conjuncts, morphology, formula.operand.variable, is_plural, no_adjectives)

		verb = ("are" if is_plural else "is")
		if invert:
			return SyntaxNode("S", [
					SyntaxNode("V", [SyntaxNode(verb)]),
					left,
					SyntaxNode("VP", [
						right
					])
				])
		else:
			return SyntaxNode("S", [
					left,
					SyntaxNode("VP", [
						SyntaxNode("V", [SyntaxNode(verb)]),
						right
					])
				])

	elif type(formula) == fol.FOLFuncApplication and formula.function == "ASSUME" and len(formula.args) == 1:
		subclause = formula_to_clause(formula.args[0], morphology, no_adjectives, invert)
		return SyntaxNode("S", [
				SyntaxNode("VP", [
					SyntaxNode("V", [SyntaxNode("assume")]),
					subclause
				])
			])

	elif type(formula) == fol.FOLFuncApplication and formula.function == "CONTRADICTS" and len(formula.args) == 1:
		subclause = formula_to_clause(formula.args[0], morphology, no_adjectives, invert)
		return SyntaxNode("S", [
				SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode("this")])])]),
				SyntaxNode("VP", [
					SyntaxNode("V", [SyntaxNode("contradicts")]),
					SyntaxNode("PP", [
						SyntaxNode("P", [SyntaxNode("with")]),
						subclause
					])
				])
			])

	elif type(formula) == fol.FOLFuncApplication and formula.function == "BACKTRACK" and len(formula.args) == 1:
		subclause = formula_to_clause(formula.args[0], morphology, no_adjectives, invert)
		return SyntaxNode("S", [
				SyntaxNode("VP", [
					SyntaxNode("V", [SyntaxNode("backtrack")]),
					SyntaxNode("PP", [
						SyntaxNode("P", [SyntaxNode("to")]),
						subclause
					])
				])
			])

	elif type(formula) == fol.FOLFuncApplication and formula.function == "START_OVER" and len(formula.args) == 0:
		return SyntaxNode("S", [
				SyntaxNode("VP", [
					SyntaxNode("V", [SyntaxNode("try")]),
					SyntaxNode("ADVP", [
						SyntaxNode("ADV", [SyntaxNode("again")])
					])
				])
			])

	elif type(formula) == fol.FOLFuncApplication and formula.function == "SINCE" and len(formula.args) == 2:
		first = formula_to_clause(formula.args[0], morphology, no_adjectives, invert)
		second = formula_to_clause(formula.args[1], morphology, no_adjectives, invert)
		return SyntaxNode("S", [
				SyntaxNode("CC", [SyntaxNode("since")]),
				first, SyntaxNode(","), second])

	elif type(formula) == fol.FOLFuncApplication and len(formula.args) == 1 and type(formula.args[0]) == fol.FOLConstant:
		right = formula_to_vp_arg(fol.FOLFuncApplication(formula.function, [fol.FOLVariable(1)]), morphology, 1, False, no_adjectives)
		if invert:
			return SyntaxNode("S", [
					SyntaxNode("V", [SyntaxNode("is")]),
					SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode(formula.args[0].constant)])])]),
					SyntaxNode("VP", [
						right
					])
				])
		else:
			return SyntaxNode("S", [
					SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode(formula.args[0].constant)])])]),
					SyntaxNode("VP", [
						SyntaxNode("V", [SyntaxNode("is")]),
						right
					])
				])

	elif type(formula) == fol.FOLNot and type(formula.operand) == fol.FOLFuncApplication and len(formula.operand.args) == 1:
		right = formula_to_vp_arg(fol.FOLFuncApplication(formula.operand.function, [fol.FOLVariable(1)]), morphology, 1, False, no_adjectives)
		if invert:
			return SyntaxNode("S", [
					SyntaxNode("V", [SyntaxNode("is")]),
					SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode(formula.operand.args[0].constant)])])]),
					SyntaxNode("VP", [
						SyntaxNode("ADVP", [SyntaxNode("ADV", [SyntaxNode("not")])]),
						right
					])
				])
		else:
			return SyntaxNode("S", [
					SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode(formula.operand.args[0].constant)])])]),
					SyntaxNode("VP", [
						SyntaxNode("V", [SyntaxNode("is")]),
						SyntaxNode("ADVP", [SyntaxNode("ADV", [SyntaxNode("not")])]),
						right
					])
				])

	elif type(formula) == fol.FOLAnd or type(formula) == fol.FOLOr:
		# first check if the coordination can be expressed as a single noun phrase as in "A is a B"
		entity = None
		expressible_as_np = True
		right_lf = []
		for operand in formula.operands:
			if type(operand) == fol.FOLFuncApplication and len(operand.args) == 1 and type(operand.args[0]) == fol.FOLConstant and (entity == None or entity == operand.args[0]):
				entity = operand.args[0]
				right_lf.append(fol.FOLFuncApplication(operand.function, [fol.FOLVariable(1)]))
			else:
				expressible_as_np = False
				break

		if expressible_as_np:
			if type(formula) == fol.FOLAnd:
				right_formula = fol.FOLAnd(right_lf)
			else:
				right_formula = fol.FOLOr(right_lf)
			right = formula_to_vp_arg(right_formula, morphology, 1, False, no_adjectives)
			if invert:
				return SyntaxNode("S", [
						SyntaxNode("V", [SyntaxNode("is")]),
						SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode(entity.constant)])])]),
						SyntaxNode("VP", [
							right
						])
					])
			else:
				return SyntaxNode("S", [
						SyntaxNode("NP", [SyntaxNode("NP'", [SyntaxNode("NN", [SyntaxNode(entity.constant)])])]),
						SyntaxNode("VP", [
							SyntaxNode("V", [SyntaxNode("is")]),
							right
						])
					])

		child_nodes = [formula_to_clause(operand, morphology, no_adjectives, invert=False) for operand in formula.operands]
		has_commas = choice([True, False])
		coordinator = ("and" if type(formula) == fol.FOLAnd else "or")
		if len(formula.operands) > 2:
			if has_commas:
				result = [SyntaxNode(",")] * (len(child_nodes) * 2 - 1)
				result[0::2] = child_nodes
				child_nodes = result
				child_nodes.insert(len(child_nodes) - 1, SyntaxNode("CC", [SyntaxNode(coordinator)]))
			else:
				result = [SyntaxNode("CC", [SyntaxNode(coordinator)])] * (len(child_nodes) * 2 - 1)
				result[0::2] = child_nodes
				child_nodes = result
		else:
			child_nodes.insert(len(child_nodes) - 1, SyntaxNode("CC", [SyntaxNode(coordinator)]))
		return SyntaxNode("S", child_nodes)

	else:
		raise Exception("formula_to_clause ERROR: Unsupported formula type.")

def yield_tokens(tree):
	if tree.children == None:
		return [tree.label]

	tokens = []
	for child in tree.children:
		tokens.extend(yield_tokens(child))
	return tokens

def inflect(tokens, end_punctuation):
	for i in range(len(tokens)):
		if tokens[i] == "a":
			if i + 1 < len(tokens) and tokens[i + 1][0] in {'a', 'e', 'i', 'o', 'u'} and not tokens[i + 1].startswith('eu'):
				tokens[i] = "an"
	sentence = tokens[0]
	for token in tokens[1:]:
		if token == ',':
			sentence += token
		else:
			sentence += ' ' + token
	return sentence[0].upper() + sentence[1:] + end_punctuation

def is_int(text):
	try:
		int(text)
		return True
	except ValueError:
		return False

def parse_np_prime(tokens, index, morphology):
	# first check if the next two tokens form a compound common noun
	if index + 1 < len(tokens):
		compound = ' '.join(tokens[index:(index+2)])
	else:
		compound = None

	if compound != None and morphology.is_noun(compound):
		is_plural = (None if morphology.is_plural_noun(compound) else False)
		lf = fol.FOLFuncApplication(compound, [fol.FOLVariable(1)])
		index += 2
	elif compound != None and morphology.is_noun(compound.lower()):
		is_plural = (None if morphology.is_plural_noun(compound) else False)
		lf = fol.FOLFuncApplication(compound.lower(), [fol.FOLVariable(1)])
		index += 2
	elif compound != None and morphology.is_plural_noun(compound):
		is_plural = (None if morphology.is_noun(compound) else True)
		lf = fol.FOLFuncApplication(morphology.to_root(compound), [fol.FOLVariable(1)])
		index += 2
	elif compound != None and morphology.is_plural_noun(compound.lower()):
		is_plural = (None if morphology.is_noun(compound) else True)
		lf = fol.FOLFuncApplication(morphology.to_root(compound.lower()), [fol.FOLVariable(1)])
		index += 2
	elif compound != None and morphology.is_noun(tokens[index].lower()) and morphology.is_noun(tokens[index + 1]):
		is_plural = (None if morphology.is_plural_noun(tokens[index + 1]) else False)
		lf = fol.FOLAnd([
				fol.FOLFuncApplication(tokens[index].lower(), [fol.FOLVariable(1)]),
				fol.FOLFuncApplication(tokens[index + 1], [fol.FOLVariable(1)])
			])
		index += 2
	elif compound != None and morphology.is_noun(tokens[index].lower()) and morphology.is_plural_noun(tokens[index + 1]):
		is_plural = (None if morphology.is_noun(tokens[index + 1]) else True)
		lf = fol.FOLAnd([
				fol.FOLFuncApplication(tokens[index].lower(), [fol.FOLVariable(1)]),
				fol.FOLFuncApplication(morphology.to_root(tokens[index + 1]), [fol.FOLVariable(1)])
			])
		index += 2
	elif morphology.is_noun(tokens[index].lower()):
		is_plural = (None if morphology.is_plural_noun(tokens[index].lower()) else False)
		lf = fol.FOLFuncApplication(tokens[index].lower(), [fol.FOLVariable(1)])
		index += 1
	elif morphology.is_plural_noun(tokens[index].lower()):
		is_plural = (None if morphology.is_noun(tokens[index].lower()) else True)
		lf = fol.FOLFuncApplication(morphology.to_root(tokens[index].lower()), [fol.FOLVariable(1)])
		index += 1
	else:
		# the noun is not common
		is_plural = False
		if not morphology.is_proper_noun(tokens[index]) and not is_int(tokens[index]):
			return (None, None, None) # proper noun should be capitalized
		lf = fol.FOLConstant(tokens[index])
		index += 1
	return (lf, index, is_plural)

def parse_adjp(tokens, index, morphology):
	# this could be a coordinated or compound ADJP
	operands = []
	first_operand_index = None
	is_conjunction = False
	is_disjunction = False
	is_compound = False
	while index < len(tokens):
		last_index = index
		if tokens[index].lower() in {"and", "or", ",", "a", "an", "each", "every", "no", "all", "that", "is", "are", "so", "since", "as", "however", "therefore", "because"}:
			break
		if len(operands) != 0:
			has_comma = False
			if tokens[index] == ',':
				index += 1
				has_comma = True
			if tokens[index] == 'and':
				if is_compound or is_disjunction:
					break
				is_conjunction = True
				index += 1
			elif tokens[index] == 'or':
				if is_compound or is_conjunction:
					break
				is_disjunction = True
				index += 1
			elif not has_comma:
				if is_disjunction or is_conjunction:
					break
				is_compound = True
		if tokens[index].lower() == 'also':
			index += 1
		if len(operands) != 0 and morphology.is_any_noun(tokens[index].lower()):
			index = last_index
			break
		# could be an adverb
		operands.append(fol.FOLFuncApplication(tokens[index].lower(), [fol.FOLVariable(1)]))
		index += 1
		if first_operand_index == None:
			first_operand_index = index

	if len(operands) == 0:
		return (None, None)
	elif len(operands) == 1:
		return (operands[0], index)
	elif is_conjunction or is_compound:
		return (fol.FOLAnd(operands), index)
	elif is_disjunction:
		return (fol.FOLOr(operands), index)
	else:
		return (operands[0], first_operand_index)

def parse_np(tokens, index, morphology):
	if tokens[index].lower() in {"each", "every"}:
		is_quantified = True
		is_negated = False
		det_is_plural = False
		index += 1
	elif tokens[index].lower() == "all":
		is_quantified = True
		is_negated = False
		det_is_plural = True
		index += 1
	elif tokens[index].lower() in {"a", "an"}:
		is_quantified = False
		is_negated = False
		det_is_plural = False
		index += 1
	elif tokens[index].lower() == 'no':
		is_quantified = False
		is_negated = True
		det_is_plural = None
		index += 1
	elif tokens[index].lower() == 'everything' and tokens[index + 1] == 'that' and tokens[index + 2] == 'is':
		# parse universally quantified conjunction or disjunction
		index += 3
		operands = []
		is_conjunction = False
		is_disjunction = False
		while index < len(tokens):
			if len(operands) != 0:
				has_comma = False
				if tokens[index] == ',':
					index += 1
					has_comma = True
				if tokens[index] == 'and':
					if is_disjunction:
						return (None, None, None, None, None)
					is_conjunction = True
					index += 1
				elif tokens[index] == 'or':
					if is_conjunction:
						return (None, None, None, None, None)
					is_disjunction = True
					index += 1
				elif not has_comma:
					break
			(operand, new_index, operand_is_plural, operand_is_negated, operand_is_quantified) = parse_np(tokens, index, morphology)
			if operand == None:
				# try parsing as a predicative (ADJP)
				(operand, index) = parse_adjp(tokens, index, morphology)
				if operand == None:
					return (None, None, None, None, None)
				elif type(operand) == fol.FOLAnd:
					if is_disjunction:
						return (None, None, None, None, None)
					is_conjunction = True
					operands.extend(operand.operands)
				elif type(operand) == fol.FOLOr:
					if is_conjunction:
						return (None, None, None, None, None)
					is_disjunction = True
					operands.extend(operand.operands)
				else:
					operands.append(operand)
			else:
				index = new_index
				operands.append(operand)
		if len(operands) == 1:
			lf = operands[0]
		elif is_conjunction:
			lf = fol.FOLAnd(operands)
		elif is_disjunction:
			lf = fol.FOLOr(operands)
		else:
			return (None, None, None, None, None)
		return (lf, index, False, False, True)
	else:
		is_quantified = False
		is_negated = False
		det_is_plural = None

	adjp_operands = []
	while True:
		(lf, new_index, is_plural) = parse_np_prime(tokens, index, morphology)
		if lf == None and index + 1 < len(tokens):
			# try parsing an ADJP before the noun
			(adjp_lf, index) = parse_adjp(tokens, index, morphology)
			if adjp_lf == None or index >= len(tokens):
				return (None, None, None, None, None)
			if type(adjp_lf) in [fol.FOLAnd, fol.FOLOr]:
				adjp_operands.extend(adjp_lf.operands)
			else:
				adjp_operands.append(adjp_lf)
			(lf, new_index, is_plural) = parse_np_prime(tokens, index, morphology)
			if isinstance(lf, fol.FOLFormula):
				index = new_index
				np_operands = lf.operands if type(lf) == fol.FOLAnd else [lf]
				if type(adjp_lf) == fol.FOLOr:
					if type(lf) in [fol.FOLAnd, fol.FOLOr]:
						return (None, None, None, None, None)
					lf = fol.FOLOr(adjp_operands + np_operands)
				else:
					lf = fol.FOLAnd(adjp_operands + np_operands)
				break
			else:
				return (None, None, None, None, None)
		else:
			index = new_index
			break

	if det_is_plural != None and is_plural != None and is_plural != det_is_plural:
		return (None, None, None, None, None) # the grammatical number of the determiner and the noun don't agree

	return (lf, index, is_plural, is_negated, is_quantified)

def parse_vp_arg(tokens, index, morphology):
	operands = []
	operand_indices = []
	operand_plural = []
	is_conjunction = False
	is_disjunction = False
	is_plural = None
	if tokens[index] == 'either':
		is_disjunction = True
		index += 1
	elif tokens[index] == 'both':
		is_conjunction = True
		index += 1
	while index < len(tokens):
		if len(operands) != 0:
			has_comma = False
			if tokens[index] == ',':
				index += 1
				has_comma = True
			if tokens[index] == 'and':
				if is_disjunction:
					return []
				is_conjunction = True
				index += 1
			elif tokens[index] == 'or':
				if is_conjunction:
					return []
				is_disjunction = True
				index += 1
			elif not has_comma:
				if not is_conjunction and not is_disjunction:
					# the last comma was actually part of a higher-level coordination
					if len(operand_indices) == 1:
						index = operand_indices[0]
						is_plural = operand_plural[0]
					else:
						del operands[-1]
						index = operand_indices[-2]
						is_plural = operand_plural[-2]
				break
			elif has_comma:
				if is_conjunction or is_disjunction:
					index = operand_indices[-1]
					break
		if tokens[index] == 'not':
			negated = True
			index += 1
		else:
			negated = False
		(operand, new_index, operand_is_plural, is_negated, is_quantified) = parse_np(tokens, index, morphology)
		if type(operand) == fol.FOLConstant:
			if len(operands) > 0:
				index = operand_indices[-1]
			if len(operands) == 1:
				is_conjunction = False
				is_disjunction = False
			break
		elif operand == None or is_quantified or is_negated:
			# try parsing as a predicative (ADJP)
			(operand, index) = parse_adjp(tokens, index, morphology)
			if operand == None or (type(operand) == fol.FOLAnd and is_disjunction) or (type(operand) == fol.FOLOr and is_conjunction):
				if len(operands) > 1 and (is_conjunction or is_disjunction):
					index = operand_indices[-1]
					break
				elif len(operands) != 0:
					return [(operands[0], operand_indices[0], operand_plural[0])]
				else:
					return []
			if type(operand) == fol.FOLAnd:
				operands.extend(operand.operands)
				operand_indices.extend([-1]*(len(operands)-1) + [index])
				operand_plural.extend([is_plural]*len(operands))
				is_conjunction = True
			elif type(operand) == fol.FOLOr:
				operands.extend(operand.operands)
				operand_indices.extend([-1]*(len(operands)-1) + [index])
				operand_plural.extend([is_plural]*len(operands))
				is_disjunction = True
			else:
				operands.append(operand)
				operand_indices.append(index)
				operand_plural.append(is_plural)
		else:
			if negated:
				operand = fol.FOLNot(operand)
			index = new_index
			if is_plural == None:
				is_plural = operand_is_plural
			elif is_plural != operand_is_plural:
				if len(operands) != 0:
					return [(operands[0], operand_indices[0], operand_plural[0])]
				else:
					return []
			operands.append(operand)
			operand_indices.append(index)
			operand_plural.append(is_plural)
	# this is ambiguous, since the coordination may either be interpreted at this node or higher in the derivation tree
	if len(operands) == 1 and not is_conjunction and not is_disjunction:
		return [(operands[0], index, is_plural)]
	elif is_conjunction:
		if operand_indices[0] == -1:
			return [(fol.FOLAnd(operands), index, is_plural)]
		else:
			return [(operands[0], operand_indices[0], operand_plural[0]), (fol.FOLAnd(operands), index, is_plural)]
	elif is_disjunction:
		if operand_indices[0] == -1:
			return [(fol.FOLOr(operands), index, is_plural)]
		else:
			return [(operands[0], operand_indices[0], operand_plural[0]), (fol.FOLOr(operands), index, is_plural)]
	else:
		return []

def parse_clause(tokens, index, morphology, can_be_coordinated=True, complete_sentence=False):
	if tokens[index].lower() == 'is':
		is_plural = False
		invert = True
		index += 1
	elif tokens[index].lower() == 'are':
		is_plural = True
		invert = True
		index += 1
	elif tokens[index].lower() == "assume":
		outputs = parse_clause(tokens, index + 1, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("ASSUME", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif tokens[index].lower() in ["since", "as"]:
		outputs = parse_clause(tokens, index + 1, morphology)
		if len(outputs) == 1 and outputs[0][1] == len(tokens):
			# try parsing without coordination
			outputs = parse_clause(tokens, index + 1, morphology, can_be_coordinated=False)

		new_outputs = []
		for (lf, new_index, invert) in outputs:
			if new_index == len(tokens):
				continue
			if tokens[new_index] == ',':
				new_index += 1
			if new_index + 3 < len(tokens) and tokens[new_index:(new_index+4)] == ["the", "statement", "is", "proven"]:
				new_outputs.append((lf, new_index + 4, invert))
			else:
				right_outputs = parse_clause(tokens, new_index, morphology, complete_sentence=complete_sentence)
				for (right_lf, right_index, right_invert) in right_outputs:
					new_outputs.append((fol.FOLFuncApplication("SINCE", [lf, right_lf]), right_index, right_invert))
		return new_outputs
	elif tokens[index].lower() == "however":
		index += 1
		if index == len(tokens):
			return []
		elif tokens[index] == ',':
			index += 1
		outputs = parse_clause(tokens, index, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("HOWEVER", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif tokens[index].lower() == "therefore":
		index += 1
		if index == len(tokens):
			return []
		elif tokens[index] == ',':
			index += 1
		outputs = parse_clause(tokens, index, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("THEREFORE", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif index + 1 < len(tokens) and tokens[index].lower() == "this" and tokens[index + 1] == "proves":
		outputs = parse_clause(tokens, index + 2, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("THEREFORE", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif index + 2 < len(tokens) and tokens[index].lower() == "this" and tokens[index + 1] == "contradicts" and tokens[index + 2] == "with":
		outputs = parse_clause(tokens, index + 3, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("CONTRADICTS", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif index + 4 < len(tokens) and tokens[index].lower() == "this" and tokens[index + 1] == "contradicts" and tokens[index + 2] == "the" and tokens[index + 3] == "fact" and tokens[index + 4] == "that":
		outputs = parse_clause(tokens, index + 5, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("CONTRADICTS", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif index + 3 < len(tokens) and tokens[index].lower() == "this" and tokens[index + 1] == "is" and tokens[index + 2] == "a" and tokens[index + 3] == "contradiction":
		index += 4
		return [(fol.FOLFuncApplication("CONTRADICTS", []), index, False)]
	elif index < len(tokens) and tokens[index].lower() == "contradiction":
		index += 1
		return [(fol.FOLFuncApplication("CONTRADICTS", []), index, False)]
	elif index + 1 < len(tokens) and tokens[index].lower() == "backtrack" and tokens[index + 1] == "to":
		outputs = parse_clause(tokens, index + 2, morphology, complete_sentence=complete_sentence)
		return [(fol.FOLFuncApplication("BACKTRACK", [lf]), index, invert) for (lf, index, invert) in outputs]
	elif index + 1 < len(tokens) and tokens[index].lower() == "try" and tokens[index + 1] == "again":
		return [(fol.FOLFuncApplication("START_OVER", []), index + 2, False)]
	elif [token.lower() for token in tokens[index:(index+6)]] == ['according', 'to', 'the', 'given', 'information', ',']:
		return parse_clause(tokens, index + 6, morphology, complete_sentence=complete_sentence)
	else:
		is_plural = None
		invert = False

	(left_lf, index, np_is_plural, np_is_negated, is_quantified) = parse_np(tokens, index, morphology)
	if left_lf == None:
		return []
	if index == len(tokens):
		return [] # clause is incomplete
	if is_plural != None and is_plural != np_is_plural:
		return [] # grammatical number does not agree

	if not invert:
		if tokens[index] == 'is':
			is_plural = False
			index += 1
		elif tokens[index] == 'are':
			is_plural = True
			index += 1
		else:
			# missing main verb for this clause
			return []

	num_negations = 0
	while tokens[index] == 'not':
		num_negations += 1
		index += 1

	vp_args = parse_vp_arg(tokens, index, morphology)
	outputs = []
	for (right_lf, index, vp_is_plural) in vp_args:
		if vp_is_plural != None and vp_is_plural != is_plural:
			continue # grammatical number does not agree

		if type(left_lf) == fol.FOLConstant:
			if is_plural:
				continue # outside the coverage of the grammar
			lf = fol.substitute(right_lf, fol.FOLVariable(1), left_lf)
			for _ in range(num_negations):
				lf = fol.FOLNot(lf)
		elif is_quantified or np_is_plural == True or np_is_plural == None:
			if np_is_negated:
				if type(right_lf) == fol.FOLAnd:
					remaining_conjuncts = right_lf.operands
				else:
					remaining_conjuncts = [right_lf]
				lf = fol.FOLNot(fol.FOLExists(1, fol.FOLAnd([left_lf] + remaining_conjuncts)))
			else:
				for _ in range(num_negations):
					right_lf = fol.FOLNot(right_lf)
				lf = fol.FOLForAll(1, fol.FOLIfThen(left_lf, right_lf))
		else:
			continue # outside the coverage of the grammar

		if not can_be_coordinated:
			arg_outputs = [(lf, index)]
		else:
			# this may be coordination
			arg_outputs = []
			has_commas = None
			original_index = index
			is_conjunction = False
			is_disjunction = False
			operands = [lf]
			queue = [(operands, index, has_commas, is_conjunction, is_disjunction)]
			coordination_outputs = []
			while len(queue) != 0:
				(operands, index, has_commas, is_conjunction, is_disjunction) = queue.pop()
				if index == len(tokens):
					coordination_outputs.append((operands, index, is_conjunction, is_disjunction))
					continue
				old_index = index
				if tokens[index] == ',':
					if has_commas == False:
						break
					has_commas = True
					index += 1
				else:
					if has_commas == True:
						break
					has_commas = False
				if tokens[index] == 'and':
					if is_disjunction:
						index = old_index
						break
					is_conjunction = True
					index += 1
				elif tokens[index] == 'or':
					if is_conjunction:
						index = old_index
						break
					is_disjunction = True
					index += 1
				elif not has_commas:
					break
				elif is_conjunction or is_disjunction:
					# found a clause without "and"/"or" after an earlier clause with "and"/"or"
					index = old_index
					break
				coordinate_parses = parse_clause(tokens, index, morphology, can_be_coordinated=False)
				for coordinate_lf, index, _ in coordinate_parses:
					queue.append((operands + [coordinate_lf], index, has_commas, is_conjunction, is_disjunction))
				if len(coordinate_parses) == 0:
					coordination_outputs.append((operands, old_index, is_conjunction, is_disjunction))

			if len(coordination_outputs) == 0:
				coordination_outputs = [([lf], old_index, False, False)]
			for operands, index, is_conjunction, is_disjunction in coordination_outputs:
				if len(operands) == 1:
					new_lf = operands[0]
				elif not is_disjunction and len(operands) == 2 and type(operands[1]) == fol.FOLFuncApplication and operands[1].function == 'THEREFORE':
					new_lf = fol.FOLFuncApplication("SINCE", [operands[0], operands[1].args[0]])
				elif is_conjunction:
					new_lf = fol.FOLAnd(operands)
				elif is_disjunction:
					new_lf = fol.FOLOr(operands)
				else:
					index = original_index
					new_lf = lf

				if index + 2 < len(tokens):
					old_index = index
					if tokens[index] == ',':
						index += 1
					if tokens[index] in {'so', 'therefore'}:
						(conclusion_lf, index, _) = parse_singleton_clause(tokens, index + 1, morphology, complete_sentence=complete_sentence)
						if conclusion_lf == None:
							index = old_index
						else:
							new_lf = fol.FOLFuncApplication("SINCE", [new_lf, conclusion_lf])
					elif tokens[index] in ['because', 'since', 'as']:
						(premise_lf, index, _) = parse_singleton_clause(tokens, index + 1, morphology, complete_sentence=complete_sentence)
						if premise_lf == None:
							index = old_index
						else:
							new_lf = fol.FOLFuncApplication("SINCE", [premise_lf, new_lf])
					else:
						index = old_index

				arg_outputs.append((new_lf, index))

		outputs.extend([(lf, index, invert) for lf, index in arg_outputs if not (complete_sentence and index != len(tokens))])

	if len(outputs) == 0:
		return []
	elif len(outputs) != 1:
		# filter ambiguous outputs that don't complete the full sentence
		new_outputs = []
		for (lf, index, invert) in outputs:
			if index == len(tokens):
				new_outputs.append((lf, index, invert))
		if len(new_outputs) == 1:
			return [new_outputs[0]]

		# filter outputs where the next token is a verb
		if not can_be_coordinated:
			new_outputs = []
			for (lf, index, invert) in outputs:
				if index < len(tokens) and tokens[index] not in {"is", "are"}:
					new_outputs.append((lf, index, invert))
			if len(new_outputs) == 1:
				return [new_outputs[0]]

	return outputs

def parse_singleton_clause(tokens, index, morphology, can_be_coordinated=True, complete_sentence=False):
	outputs = parse_clause(tokens, index, morphology, can_be_coordinated=can_be_coordinated, complete_sentence=complete_sentence)
	if len(outputs) == 0:
		return (None, None, None)
	elif len(outputs) != 1:
		raise AmbiguousParseError(tokens[index:], [lf for (lf, _, _) in outputs])
	return outputs[0]

def parse_sentence(sentence, morphology, expect_invert=None):
	if type(sentence) == str:
		sentence = re.findall(r"[\w\-]+|[^\w\s]", sentence)
	outputs = parse_clause(sentence, 0, morphology, complete_sentence=True)

	new_outputs = []
	for (lf, index, invert) in outputs:
		if (expect_invert != None and invert != expect_invert) or index != len(sentence):
			continue # subject and auxiliary were either incorrectly inverted or incorrectly not inverted
		new_outputs.append((lf, index, invert))
	outputs = new_outputs

	if len(outputs) == 0:
		return None
	elif len(outputs) != 1:
		raise AmbiguousParseError(sentence, [lf for (lf, _, _) in outputs])
	return outputs[0][0]