# encoding: utf-8

import unittest
import convert
import string_stream

class test_convert(unittest.TestCase):
  def process(self, inputString):
    return convert.Convert().convert(string_stream.StringStream(inputString))

  def test_empty(self):
    self.assertEqual("", self.process(""))

  def test_kind(self):
    self.assertEqual("kind (formula)", self.process("kind (formula)"))

  def test_should_preserve_whitespace_except_between_command_and_args(self):
    self.assertEqual("\t\nkind  \t\n(   formula \t )\n\n",
      self.process("\t\nkind  \t\n(   formula \t )\n\n"))

  def test_var_to_tvar(self):
    self.assertEqual("kind (formula)\ntvar (formula p)", self.process(
      "kind (formula)\nvar (formula p)"))

  def test_converts_var_to_var_for_kind_variable(self):
    # Might be kind of nice to clean up the whitespace where we remove
    # "kind (variable)", but maybe that isn't needed
    self.assertEqual("kind (object)\n \nvar (object x)", self.process(
      "kind (object)\nkind (variable)\nvar (variable x)"))

  def test_keeps_list_of_symbols_by_kind(self):
    converter =  convert.Convert()
    inputString = "var (formula p q)\nvar (formula r)\n"
    converter.convert(string_stream.StringStream(inputString))
    self.assertEqual({'formula': ['p', 'q', 'r']}, converter._variables)

  def test_can_assign_symbols_from_list(self):
    assigner = convert.VariableAssigner({'formula': ['p', 'q', 'r']})
    self.assertEqual('p', assigner.next_name('formula'))
    self.assertEqual('q', assigner.next_name('formula'))

  def test_converts_basic_stmt(self):
    result = self.process("""
kind (formula)
var (formula p q)
term (formula (→ formula formula))
stmt (AntecedentIntroduction () () (→ p (→ q p)))
""")
    self.assertEqual("""
kind (formula)
tvar (formula p q)
term (formula (→ p q))
stmt (AntecedentIntroduction () () (→ p (→ q p)))
""", result)

  def test_undoes_pseudo_infix(self):
    result = self.process("""
kind (formula)
var (formula p q)
term (formula (→ formula formula))
stmt (AntecedentIntroduction () () (p → (q → p)))
""")
    self.assertEqual("""
kind (formula)
tvar (formula p q)
term (formula (→ p q))
stmt (AntecedentIntroduction () () (→ p (→ q p)))
""", result)

  def test_undo_pseudo_infix_in_rule(self):
    result = self.process("""
kind (formula)
var (formula p q)
term (formula (→ formula formula))
stmt (applyModusPonens () (p (p → q)) q)
""")
    self.assertEqual("""
kind (formula)
tvar (formula p q)
term (formula (→ p q))
stmt (applyModusPonens () (p (→ p q)) q)
""", result)

  def wiki(self, string):
    return convert.Wiki().read(string_stream.StringStream(string))

  def wiki_convert(self, string):
    return convert.Wiki().convert(string_stream.StringStream(string))

  def test_read_wiki_no_proof(self):
    self.assertEqual("", self.wiki("I\nam a proof\nsite\n"))

  def test_read_wiki_open_jh(self):
    input = "<jh>\nkind (formula)\n</jh>\n"
    self.assertEqual("kind (formula)\n", self.wiki(input))

  def test_read_wiki_multiple_jh(self):
    input = "<jh>\nkind\n</jh>\nhere we define it\n<jh>\n (formula)\n</jh>\n"
    self.assertEqual("kind\n (formula)\n", self.wiki(input))

  def test_converts_proofs_in_wiki(self):
    self.assertEqual("kind (formula)\ntvar (formula p)\n", self.wiki_convert(
      "<jh>\nkind (formula)\nvar (formula p)\n</jh>\n"))


@@ -2534,24 +2534,483 @@
 %22, result)%0A%0A
+  def xtest_turn_def_into_term_and_statement(self):%0A    result = self.process(%22%22%22%0Akind (formula)%0Akind (number)%0Avar (number x y)%0Aterm (formula (= number number))%0Aterm (number (double number))%0Adef ((quadruple x) (double (double x)))%0A%22%22%22)%0A    self.assertEqual(%22%22%22%0Akind (formula)%0Akind (number)%0Atvar (number x y)%0Aterm (formula (= x y))%0Aterm (number (double x))%0Aterm (number (quadruple x))%0Astmt (Quadruple () () (= (quadruple x) (double (double x))))%0A%22%22%22, result)%0A%0A
   def wiki(s

Write test for turning def into term and stmt.