package isac.gui.mawen.scalaterm

 import isac.gui.mawen.syntax.Ast

 import edu.tum.cs.isabelle.pure._

 import junit.framework.TestCase

 import java.lang.String

 import org.junit.Assert._

 class TestUtil extends TestCase {

   def test_string_of() {

     println("/--BEGIN isac.gui.mawen.scalaterm.TestUtil#test_string_of");

     assertEquals(Util.string_of(TestsDATA.t1), "aaa + bbb = processed_by_Isabelle_Isac")

     assertEquals(Util.string_of(TestsDATA.t2), "a + 2 * b + 3 * (c + d)")

     assertEquals(Util.string_of(TestsDATA.t31), "aaa + bbb + ccc")

     assertEquals(Util.string_of(TestsDATA.t32), "aaa + (bbb + ccc)")

     assertEquals(Util.string_of(TestsDATA.t41), "Diff (x + sin (x ^ 2), x)")

     assertEquals(Util.string_of(TestsDATA.t42), "d_d x (x + sin (x ^ 2))")

     // MAWEN example for reference No.1

     assertEquals(Util.string_of(TestsDATA.tt1()), "Simplify (1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5)")

     assertEquals(Util.string_of(TestsDATA.tt3()), "1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5")

     assertEquals(Util.string_of(TestsDATA.tt4()), "1 + 2 * x / (4 * z) + 5")

     assertEquals(Util.string_of(TestsDATA.tt5()), "1 + x / (2 * z) + 5")

     assertEquals(Util.string_of(TestsDATA.tt6()), "6 + x / (2 * z)")

     println("\\--END isac.gui.mawen.scalaterm.TestUtil#test_string_of");

   }

    /**

    * tested on validity with: http://www-archive.mozilla.org/projects/mathml/demo/tester.html

    */

   def test_mathml_of() {

     println("/--BEGIN isac.gui.mawen.scalaterm.TestUtil#mathml_of"); 

     assertEquals(Util.mathml_of(TestsDATA.tt3), TestsDATA.tt3_math());

     println("\\--END isac.gui.mawen.scalaterm.TestUtil#mathml_of");

   }

 }