(* 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 / (...' ----------------";

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

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