akargl@42176: (* Title: tests for mathml.sml
akargl@42176:    Author: Walther Neuper 060311
neuper@37906:    (c) isac-team 2006
neuper@37906: *)
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "--------- encode ^^^ -> ^ ---------------------------------------";
neuper@37906: "--------- encode < -> &lt and > -> &gt --------------------------";
wneuper@59177: "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
wneuper@59177: "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "--------- ... ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: (*==================================================================*)
neuper@37906: 
neuper@37906: "--------- encode ^^^ -> ^ ---------------------------------------";
neuper@37906: "--------- encode ^^^ -> ^ ---------------------------------------";
neuper@37906: "--------- encode ^^^ -> ^ ---------------------------------------";
neuper@37906: val str = "a^^^2+b^^^2=c^^^2";
neuper@37906: if decode str = "a^2+b^2=c^2" then ()
neuper@38031: else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
neuper@37906: 
akargl@42176: "--------- encode < -> &lt; and > -> &gt; --------------------------";
akargl@42176: "--------- encode < -> &lt; and > -> &gt; --------------------------";
akargl@42176: "--------- encode < -> &lt; and > -> &gt; --------------------------";
neuper@37906: val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
akargl@42176: if decode str = "?bdv occurs_in ?b; 0 &lt; ?n |] ==&gt; ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()
akargl@42176: else error "mathml.sml: diff.behav. in encode '<' and '>'";
neuper@37906: 
akargl@42176: (*========== inhibit exn AK110725 ================================================
neuper@37906: "----- check 'manually' the xml-output of calling functions ------";
akargl@42176: formula2xml 1 (str2term str);
neuper@37906: 
akargl@42176: (* AK110725 
akargl@42176: (*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
akargl@42176:                    Failed to parse term*)*)
akargl@42176: "~~~~~ fun str2term, args:"; val (str) = (str);
walther@59879: ThyC.get_theory "Isac_Knowledge";
akargl@42176: 
akargl@42176: parse_patt;
walther@59879: parse_patt (ThyC.get_theory "Isac_Knowledge");
walther@59879: (*parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
akargl@42176: Failed to parse term*)*)
akargl@42176: 
walther@59879: "~~~~~ fun parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
akargl@42176: (thy, str) 
walther@59879: |>> ThyC.to_ctxt
neuper@48761: (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
akargl@42176: Failed to parse term*)*)
akargl@42176: 
neuper@48761: Proof_Context.read_term_pattern;
walther@59879: (@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
neuper@48761: "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
akargl@42176: (*AK110725 To be continued...*)
akargl@42176: *)
neuper@37906: (*==================================================================*)
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
akargl@42176: ========== inhibit exn AK110725 ================================================*)
wneuper@59177: 
wneuper@59177: "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
wneuper@59177: "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
wneuper@59177: "--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
wneuper@59177: val c = "^";
walther@59997: val cs = ["^", "^", "^", "d", "e"];
wneuper@59177: if rm_doublets c [] cs = Symbol.explode "^de" 
wneuper@59177: then () else error "rm_doublets '^^^de' CHANGED";
wneuper@59177: 
walther@59997: val cs = ["a", "b", "^", "^", "^", "d", "e"];
wneuper@59177: if rm_doublets c [] cs = Symbol.explode "ab^de" 
wneuper@59177: then () else error "rm_doublets 'ab^^^de' CHANGED";
wneuper@59177: 
wneuper@59177: val cstr = 
wneuper@59177: "-4 * b ^^^^^^^^^ 2 / (a + b) + 4 * a ^^^^^^^^^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)";
wneuper@59177: val cs = Symbol.explode cstr;
wneuper@59177: if rm_doublets c [] cs = Symbol.explode 
wneuper@59177:   "-4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)"
wneuper@59177: then () else error "rm_doublets '-4 * b ^^^^^..' CHANGED";
wneuper@59177: 
wneuper@59177: "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
wneuper@59177: "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
wneuper@59177: "--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
wneuper@59177: if encode cstr = 
wneuper@59177: "-4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b) -4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b)"
wneuper@59177: then () else error "encode '-4 * b ^^^^^..' CHANGED";
wneuper@59177: 
wneuper@59224: "--------- fun xmlstr --------------------------------------------";
wneuper@59224: "--------- fun xmlstr --------------------------------------------";
wneuper@59224: "--------- fun xmlstr --------------------------------------------";
wneuper@59224: val term = @{term "aaa + bbb::real"};
wneuper@59224: val str = term |> xml_of_term_NEW |> xmlstr 0;
wneuper@59224: if str =
walther@59617: "(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"
wneuper@59224: then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
wneuper@59224: writeln str;
wneuper@59224: 
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59224: (* xml_of_term_NEW o xml_to_term_NEW = id ... not valid, 
wneuper@59224:   as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.
wneuper@59213: val t = @{term "aaa + bbb::real"};
wneuper@59213: if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
wneuper@59213: else error "xml_of_term_NEW |> xml_to_term_NEW changed"
wneuper@59224: *)
wneuper@59214: 
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
wneuper@59214: val t = @{term "aaa + bbb::real"};
wneuper@59214: val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
wneuper@59214: (* check the term structure *)
wneuper@59214: val Const ("HOL.eq", T1) $
wneuper@59214:      (Const ("Groups.plus_class.plus", T2) $ 
wneuper@59214:         Free ("aaa", T3) $ 
wneuper@59214:         Free ("bbb", _)) $
wneuper@59214:       Const ("processed_by_Isabelle_Isac", _) = ttt;
wneuper@59214: 
wneuper@59214: (* check the type structure *)
wneuper@59214: atomtyp T3;
wneuper@59214: Type ("Real.real", []);
wneuper@59214: 
wneuper@59214: atomtyp T2;
wneuper@59214: (*
wneuper@59214: *** Type (fun,[
wneuper@59214: *** . Type (Real.real,[])
wneuper@59214: *** . Type (fun,[
wneuper@59214: *** . . Type (Real.real,[])
wneuper@59214: *** . . Type (Real.real,[])
wneuper@59214: *** . . ]
wneuper@59214: *** . ]
wneuper@59214: with this ^^^ build the typ ...*)
wneuper@59214: Type ("fun", [
wneuper@59214:   Type ("Real.real", []), 
wneuper@59214:   Type ("fun", [
wneuper@59214:     Type ("Real.real", []), 
wneuper@59214:     Type ("Real.real", [])])]);
wneuper@59214: 
wneuper@59214: atomtyp T1;
wneuper@59214: (*
wneuper@59214: *** Type (fun,[
wneuper@59214: *** . Type (Real.real,[])
wneuper@59214: *** . Type (fun,[
wneuper@59214: *** . . Type (Real.real,[])
wneuper@59214: *** . . Type (HOL.bool,[])
wneuper@59214: *** . . ]
wneuper@59214: *** . ]
wneuper@59214: with this ^^^ build the typ ...*)
wneuper@59214: Type ("fun", [
wneuper@59214:   Type ("Real.real", []), 
wneuper@59214:   Type ("fun", [
wneuper@59214:     Type ("Real.real", []), 
wneuper@59214:     Type ("HOL.bool", [])])]);
wneuper@59214: 
wneuper@59214: (* now compose term + typ *)
wneuper@59214: val Const ("HOL.eq", Type ("fun", [
wneuper@59214:                        Type ("Real.real", []), 
wneuper@59214:                        Type ("fun", [
wneuper@59214:                          Type ("Real.real", []), 
wneuper@59214:                          Type ("HOL.bool", [])])])) $
wneuper@59214:      (Const ("Groups.plus_class.plus", Type ("fun", [
wneuper@59214:                                          Type ("Real.real", []), 
wneuper@59214:                                          Type ("fun", [
wneuper@59214:                                            Type ("Real.real", []), 
wneuper@59214:                                            Type ("Real.real", [])])])) $ 
wneuper@59214:         Free ("aaa", Type ("Real.real", [])) $ 
wneuper@59214:         Free ("bbb", Type ("Real.real", []))) $
wneuper@59214:       Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
wneuper@59214: 
wneuper@59214: (* match out the original term from result*)
wneuper@59214: val Const ("HOL.eq", Type ("fun", [
wneuper@59214:                        Type ("Real.real", []), 
wneuper@59214:                        Type ("fun", [
wneuper@59214:                          Type ("Real.real", []), 
wneuper@59214:                          Type ("HOL.bool", [])])])) $
wneuper@59214:       t' $
wneuper@59214:       Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
wneuper@59214: if t = t' then () else error "something with test_term changed"