package isac.gui.mawen.scalaterm;

import isac.bridge.Isabelle_Isac

import isac.bridge.xml.DataTypes

import edu.tum.cs.isabelle.pure._  // for Term

import edu.tum.cs.isabelle._       // for Codec

import edu.tum.cs.isabelle.japi._  // for JSystem

import junit.framework.TestCase

import org.junit.Assert._

/**

 * Create libisabelle's Scala Term from String for tests.

 * Compare ScalaAstFromString.

 */

class ScalaTermFromString extends TestCase {

  var sys_ : JSystem = null

  override def setUp() {

    sys_ = Isabelle_Isac.connect();

  }

  /**

   * test output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term

   */

  def test_scala_of_term() {

    println("/--BEGIN isac.gui.mawen.TestUseCases#test_scala_of_term");

    var term_str = "aaa"

    var tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    var term = DataTypes.xml_to_Term(tree)

    assertEquals(term,

      // copied output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term

      Free("aaa", TFree("'a", List())) 

    )

    term_str = "let aaa = bbb in aaa"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    term = DataTypes.xml_to_Term(tree)

    assertEquals(term,

      // copied output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term

      App(App(Const("HOL.Let", Type("fun", List(TFree("'a", List("HOL.type")),Type("fun", List(Type("fun", List(TFree("'a", List("HOL.type")),TFree("'a", List("HOL.type")))),TFree("'a", List("HOL.type"))))))), Free("bbb", TFree("'a", List("HOL.type")))), Abs("aaa", TFree("'a", List("HOL.type")), Bound(0))) 

    )

    // ATTENTION: numerals are different due to specific Isac code: 

    // ~~/src/Tools/isac/ProgLang/termC.sml: numbers_to_string

    term_str = "0"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    term = DataTypes.xml_to_Term(tree)

    assertEquals(term,

      // NOT copied:

      Free("0", TFree("'a", List("Groups.zero")))

    )

    // copied output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term (without parse*)

    Const("Groups.zero_class.zero", TFree("'a", List("Groups.zero"))) 

    println("\\--END isac.gui.mawen.TestUseCases#test_scala_of_term");

  }

  def test_etc() {

    println("/--BEGIN isac.gui.mawen.syntax.ScalaAstFromString#test_etc");

    //dummy

    var term_str = "dummy"

    var tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    var term = DataTypes.xml_to_Term(tree)

    term_str = "(aaa, bbb, ccc, ddd)"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    term = DataTypes.xml_to_Term(tree)

    assertEquals(term,

      // copied output from SML: writeln(scala_of_term(@{term "(aaa, bbb, ccc)"}))

    App(

      App(

        Const("Product_Type.Pair", Type("fun", List(TFree("'a", List("HOL.type")),Type("fun", List(Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type")))))),Type("Product_Type.prod", List(TFree("'a", List("HOL.type")),Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))))))),

        Free("aaa", TFree("'a", List("HOL.type")))),

      App(

        App(

          Const("Product_Type.Pair", Type("fun", List(TFree("'b", List("HOL.type")),Type("fun", List(Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type")))),Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))))),

          Free("bbb", TFree("'b", List("HOL.type")))),

        App(

          App(

            Const("Product_Type.Pair", Type("fun", List(TFree("'c", List("HOL.type")),Type("fun", List(TFree("'d", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))),

            Free("ccc", TFree("'c", List("HOL.type")))),

          Free("ddd", TFree("'d", List("HOL.type"))

        ))

      ))

    )

    println("\\--END isac.gui.mawen.syntax.ScalaAstFromString#test_etc");

  }

  override def tearDown() {

    sys_.dispose()

    super.tearDown()

  }

}