(* Title: tests for mathml.sml

   Author: Walther Neuper 060311

   (c) isac-team 2006

*)

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

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

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

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

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

"--------- encode ^^^ -> ^ ---------------------------------------";

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

"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";

"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";

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

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

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

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

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

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

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

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

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

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

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

"--------- encode ^^^ -> ^ ---------------------------------------";

"--------- encode ^^^ -> ^ ---------------------------------------";

"--------- encode ^^^ -> ^ ---------------------------------------";

val str = "a^^^2+b^^^2=c^^^2";

if decode str = "a^2+b^2=c^2" then ()

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

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

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

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

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

if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()

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

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

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

formula2xml 1 (str2term str);

(* AK110725 

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

                   Failed to parse term*)*)

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

Thy_Info.get_theory "Isac";

parse_patt;

parse_patt (Thy_Info.get_theory "Isac");

(*parse_patt (Thy_Info.get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"

Failed to parse term*)*)

"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str);

(thy, str) 

|>> thy2ctxt

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

Failed to parse term*)*)

Proof_Context.read_term_pattern;

(@{theory "Isac"}, str) |>> thy2ctxt;

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

(*AK110725 To be continued...*)

*)

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

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

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

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

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

"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";

"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";

"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";

val c = "^";

val cs = ["^","^","^","d","e"];

if rm_doublets c [] cs = Symbol.explode "^de" 

then () else error "rm_doublets '^^^de' CHANGED";

val cs = ["a","b","^","^","^","d","e"];

if rm_doublets c [] cs = Symbol.explode "ab^de" 

then () else error "rm_doublets 'ab^^^de' CHANGED";

val cstr = 

"-4 * b ^^^^^^^^^ 2 / (a + b) + 4 * a ^^^^^^^^^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)";

val cs = Symbol.explode cstr;

if rm_doublets c [] cs = Symbol.explode 

  "-4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)"

then () else error "rm_doublets '-4 * b ^^^^^..' CHANGED";

"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";

"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";

"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";

if encode cstr = 

"-4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b) -4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b)"

then () else error "encode '-4 * b ^^^^^..' CHANGED";

"--------- 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 ------------------";

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 ^^^ 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 ^^^ 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"