(* Title: tests for mathml.sml

   Author: Walther Neuper 060311

   (c) isac-team 2006

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"within struct ---------------------------------------------------";

"-----------------------------------------------------------------";

"--------- encode \<up> -> ^ ---------------------------------------";

"--------- encode < -> &lt and > -> &gt --------------------------";

"--------- fun rm_doublets '-4 * b \<up>\<up>\<up> 2 / (...' -----------";

"--------- fun decode '-4 * b \<up>\<up>\<up> 2 / (...' ----------------";

"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

"--------- create testdata for TestPIDE.java#testTermTransfer ----";

"-----------------------------------------------------------------";

"exported from struct --------------------------------------------";

"-----------------------------------------------------------------";

"--------- ... ---------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"within struct ---------------------------------------------------";

"-----------------------------------------------------------------";

(*==================================================================*)

"--------- encode \<up> -> ^ ---------------------------------------";

"--------- encode \<up> -> ^ ---------------------------------------";

"--------- encode \<up> -> ^ ---------------------------------------";

val str = "a\<up>2+b\<up>2=c\<up>2";

if decode str = "a\<up>2+b\<up>2=c\<up>2" then ()

else error "mathml.sml: diff.behav. in encode \<up> -> ^";

"--------- encode < -> &lt; and > -> &gt; --------------------------";

"--------- encode < -> &lt; and > -> &gt; --------------------------";

"--------- encode < -> &lt; and > -> &gt; --------------------------";

val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n";

if decode str = "?bdv occurs_in ?b; 0 &lt; ?n |] ==&gt; ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n" then ()

else error "mathml.sml: diff.behav. in encode '<' and '>'";

(*========== inhibit exn AK110725 ================================================

"----- check 'manually' the xml-output of calling functions ------";

formula2xml 1 (TermC.str2term str);

(* AK110725 

(*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

                   Failed to TermC.parse term*)*)

"~~~~~ fun TermC.str2term, args:"; val (str) = (str);

ThyC.get_theory "Isac_Knowledge";

TermC.parse_patt;

TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");

(*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

Failed to TermC.parse term*)*)

"~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);

(thy, str) 

|>> ThyC.to_ctxt

(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

Failed to TermC.parse term*)*)

Proof_Context.read_term_pattern;

(@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;

"~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();

(*AK110725 To be continued...*)

*)

(*==================================================================*)

"-----------------------------------------------------------------";

"exported from struct --------------------------------------------";

"-----------------------------------------------------------------";

========== inhibit exn AK110725 ================================================*)

"--------- fun xmlstr --------------------------------------------";

"--------- fun xmlstr --------------------------------------------";

"--------- fun xmlstr --------------------------------------------";

val term = @{term "aaa + bbb::real"};

val str = term |> xml_of_term_NEW |> xmlstr 0;

if str =

"(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"

then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";

writeln str;

"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

(* xml_of_term_NEW o xml_to_term_NEW = id ... not valid, 

  as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.

val t = @{term "aaa + bbb::real"};

if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()

else error "xml_of_term_NEW |> xml_to_term_NEW changed"

*)

"--------- create testdata for TestPIDE.java#testTermTransfer ----";

"--------- create testdata for TestPIDE.java#testTermTransfer ----";

"--------- create testdata for TestPIDE.java#testTermTransfer ----";

val t = @{term "aaa + bbb::real"};

val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))

(* check the term structure *)

val Const ("HOL.eq", T1) $

     (Const ("Groups.plus_class.plus", T2) $ 

        Free ("aaa", T3) $ 

        Free ("bbb", _)) $

      Const ("processed_by_Isabelle_Isac", _) = ttt;

(* check the type structure *)

atomtyp T3;

Type ("Real.real", []);

atomtyp T2;

(*

*** Type (fun,[

*** . Type (Real.real,[])

*** . Type (fun,[

*** . . Type (Real.real,[])

*** . . Type (Real.real,[])

*** . . ]

*** . ]

with this \<up> build the typ ...*)

Type ("fun", [

  Type ("Real.real", []), 

  Type ("fun", [

    Type ("Real.real", []), 

    Type ("Real.real", [])])]);

atomtyp T1;

(*

*** Type (fun,[

*** . Type (Real.real,[])

*** . Type (fun,[

*** . . Type (Real.real,[])

*** . . Type (HOL.bool,[])

*** . . ]

*** . ]

with this \<up> build the typ ...*)

Type ("fun", [

  Type ("Real.real", []), 

  Type ("fun", [

    Type ("Real.real", []), 

    Type ("HOL.bool", [])])]);

(* now compose term + typ *)

val Const ("HOL.eq", Type ("fun", [

                       Type ("Real.real", []), 

                       Type ("fun", [

                         Type ("Real.real", []), 

                         Type ("HOL.bool", [])])])) $

     (Const ("Groups.plus_class.plus", Type ("fun", [

                                         Type ("Real.real", []), 

                                         Type ("fun", [

                                           Type ("Real.real", []), 

                                           Type ("Real.real", [])])])) $ 

        Free ("aaa", Type ("Real.real", [])) $ 

        Free ("bbb", Type ("Real.real", []))) $

      Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;

(* match out the original term from result*)

val Const ("HOL.eq", Type ("fun", [

                       Type ("Real.real", []), 

                       Type ("fun", [

                         Type ("Real.real", []), 

                         Type ("HOL.bool", [])])])) $

      t' $

      Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;

if t = t' then () else error "something with test_term changed"