#encoding: utf-8
import sys

import tokenizer
import tree
import copy
import string_stream

class VariableAssigner:
  def __init__(self, variables):
    self._variables = copy.deepcopy(variables)

  def next_name(self, kind):
    return self._variables[kind].pop(0)

class Convert:
  def __init__(self):
    self._variables = {}
    self._terms = {}

  def store_variables(self, kind, variables):
    if not kind in self._variables:
      self._variables[kind] = []
    self._variables[kind] += variables

  def undo_pseudo_infix(self, expression):
    term_index = None
    for i in xrange(0, len(expression)):
      element = expression[i]
      if element in self._terms:
        term_index = i
      elif element.__class__ == tree.Tree:
        self.undo_pseudo_infix(element)
    if term_index != None:
      term = expression[term_index]
      for j in xrange(term_index):
        expression[j + 1] = expression[j]
      expression[0] = term

  def capitalize_term(self, term):
    preset_names = {'∨': 'Disjunction'}
    if preset_names.has_key(term):
      return preset_names[term]
    else:
      return term.capitalize()

  def term_kind(self, definiens):
    if definiens[0].__class__ == 'a'.__class__:
      return self._terms[definiens[0]]
    else:
      raise Exception("Cannot figure out kind of " + definiens.to_string())

  def equality_operator(self, kind):
    if kind == "formula" or kind == "wff":
      return "↔"
    else:
      return '='

  def convert(self, input):
    expressions = tree.parse(input)
    i = 0
    while i < len(expressions):
      command = expressions[i]
      arguments = expressions[i + 1]

      if command == "kind" and arguments[0] == "variable":
        expressions[i] = '';
        expressions[i + 1] = '';
      elif command == "var":
        if arguments[0] == "variable":
          arguments[0] = "object"
        else:
          expressions[i] = "tvar"
        self.store_variables(arguments[0], arguments[1:])
      elif command == "term":
        assigner = VariableAssigner(self._variables)
        return_type = arguments[0]
        name_and_arguments = arguments[1]
        name = name_and_arguments[0]

        self._terms[name] = return_type

        for j in xrange(1, len(name_and_arguments)):
          name_and_arguments[j] = assigner.next_name(name_and_arguments[j])
      elif command == "def":
        definiendum = arguments[0]
        definiens = copy.deepcopy(arguments[1])
        self.undo_pseudo_infix(definiens)
        defined_term = definiendum[0]
        term_type = self.term_kind(definiens)

        expressions[i] = "term"
        expressions[i + 1] = tree.Tree(
          [term_type, ' ', copy.deepcopy(definiendum)])
        self._terms[definiendum[0]] = term_type

#        expressions.insert(i + 2, "\n")
        expressions.insert(i + 2, "stmt")
        stmt_args = tree.Tree([
          self.capitalize_term(defined_term),
          tree.Tree([]),
          tree.Tree([]),
          tree.Tree([self.equality_operator(term_type),
            definiendum, definiens])
        ])
        expressions.insert(i + 3, stmt_args)

        i += 2

      self.undo_pseudo_infix(arguments)
      i += 2

    return expressions.to_string()

class Wiki:
  def read(self, input):
    result = ''
    in_proof = False
    while True:
      line = input.readline()
      if line == '':
        break
      if line == "</jh>\n":
        in_proof = False
      elif in_proof:
        result += line

      if line == "<jh>\n":
        in_proof = True
    return result

  def convert(self, input):
    jhilbert = self.read(input)
    return Convert().convert(string_stream.StringStream(jhilbert))

if __name__ == '__main__':
  if len(sys.argv) != 3:
    print >> sys.stderr, 'Usage: JHILBERT-INPUT GHILBERT-OUTPUT'
    exit(1)
  input = open(sys.argv[1], "r")
  output = open(sys.argv[2], "w")

  output.write(Wiki().convert(input))


@@ -997,16 +997,23 @@
 ames = %7B
+%0A      
 '%E2%88%A8': 'Di
@@ -1022,16 +1022,124 @@
 unction'
+,%0A      '%E2%88%A7': 'Conjunction',%0A      '%E2%86%94': 'Biconditional',%0A      '%E2%86%92': 'Implication',%0A      '%C2%AC': 'Negation'%0A    
 %7D%0A    if

Add more names which we can use instead of capitalizing.