1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml Wed Aug 28 11:21:26 2019 +0200
1.3 @@ -0,0 +1,192 @@
1.4 +(* Title: tests for mathml.sml
1.5 + Author: Walther Neuper 060311
1.6 + (c) isac-team 2006
1.7 +*)
1.8 +"-----------------------------------------------------------------";
1.9 +"table of contents -----------------------------------------------";
1.10 +"-----------------------------------------------------------------";
1.11 +"within struct ---------------------------------------------------";
1.12 +"-----------------------------------------------------------------";
1.13 +"--------- encode ^^^ -> ^ ---------------------------------------";
1.14 +"--------- encode < -> < and > -> > --------------------------";
1.15 +"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.16 +"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.17 +"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
1.18 +"--------- create testdata for TestPIDE.java#testTermTransfer ----";
1.19 +"-----------------------------------------------------------------";
1.20 +"exported from struct --------------------------------------------";
1.21 +"-----------------------------------------------------------------";
1.22 +"--------- ... ---------------------------------------------------";
1.23 +"-----------------------------------------------------------------";
1.24 +
1.25 +
1.26 +
1.27 +"-----------------------------------------------------------------";
1.28 +"within struct ---------------------------------------------------";
1.29 +"-----------------------------------------------------------------";
1.30 +(*==================================================================*)
1.31 +
1.32 +"--------- encode ^^^ -> ^ ---------------------------------------";
1.33 +"--------- encode ^^^ -> ^ ---------------------------------------";
1.34 +"--------- encode ^^^ -> ^ ---------------------------------------";
1.35 +val str = "a^^^2+b^^^2=c^^^2";
1.36 +if decode str = "a^2+b^2=c^2" then ()
1.37 +else error "mathml.sml: diff.behav. in encode ^^^ -> ^";
1.38 +
1.39 +"--------- encode < -> < and > -> > --------------------------";
1.40 +"--------- encode < -> < and > -> > --------------------------";
1.41 +"--------- encode < -> < and > -> > --------------------------";
1.42 +val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n";
1.43 +if decode str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n" then ()
1.44 +else error "mathml.sml: diff.behav. in encode '<' and '>'";
1.45 +
1.46 +(*========== inhibit exn AK110725 ================================================
1.47 +"----- check 'manually' the xml-output of calling functions ------";
1.48 +formula2xml 1 (str2term str);
1.49 +
1.50 +(* AK110725
1.51 +(*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
1.52 + Failed to parse term*)*)
1.53 +"~~~~~ fun str2term, args:"; val (str) = (str);
1.54 +Thy_Info_get_theory "Isac_Knowledge";
1.55 +
1.56 +parse_patt;
1.57 +parse_patt (Thy_Info_get_theory "Isac_Knowledge");
1.58 +(*parse_patt (Thy_Info_get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
1.59 +Failed to parse term*)*)
1.60 +
1.61 +"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac_Knowledge"), str);
1.62 +(thy, str)
1.63 +|>> thy2ctxt
1.64 +(*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
1.65 +Failed to parse term*)*)
1.66 +
1.67 +Proof_Context.read_term_pattern;
1.68 +(@{theory "Isac_Knowledge"}, str) |>> thy2ctxt;
1.69 +"~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
1.70 +(*AK110725 To be continued...*)
1.71 +*)
1.72 +(*==================================================================*)
1.73 +"-----------------------------------------------------------------";
1.74 +"exported from struct --------------------------------------------";
1.75 +"-----------------------------------------------------------------";
1.76 +========== inhibit exn AK110725 ================================================*)
1.77 +
1.78 +"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.79 +"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.80 +"--------- fun rm_doublets '-4 * b ^^^^^^^^^ 2 / (...' -----------";
1.81 +val c = "^";
1.82 +val cs = ["^","^","^","d","e"];
1.83 +if rm_doublets c [] cs = Symbol.explode "^de"
1.84 +then () else error "rm_doublets '^^^de' CHANGED";
1.85 +
1.86 +val cs = ["a","b","^","^","^","d","e"];
1.87 +if rm_doublets c [] cs = Symbol.explode "ab^de"
1.88 +then () else error "rm_doublets 'ab^^^de' CHANGED";
1.89 +
1.90 +val cstr =
1.91 +"-4 * b ^^^^^^^^^ 2 / (a + b) + 4 * a ^^^^^^^^^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)";
1.92 +val cs = Symbol.explode cstr;
1.93 +if rm_doublets c [] cs = Symbol.explode
1.94 + "-4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b) -4 * b ^ 2 / (a + b) + 4 * a ^ 2 / (a + b)"
1.95 +then () else error "rm_doublets '-4 * b ^^^^^..' CHANGED";
1.96 +
1.97 +"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.98 +"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.99 +"--------- fun decode '-4 * b ^^^^^^^^^ 2 / (...' ----------------";
1.100 +if encode cstr =
1.101 +"-4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b) -4 * b ^^^ 2 / (a + b) + 4 * a ^^^ 2 / (a + b)"
1.102 +then () else error "encode '-4 * b ^^^^^..' CHANGED";
1.103 +
1.104 +"--------- fun xmlstr --------------------------------------------";
1.105 +"--------- fun xmlstr --------------------------------------------";
1.106 +"--------- fun xmlstr --------------------------------------------";
1.107 +val term = @{term "aaa + bbb::real"};
1.108 +val str = term |> xml_of_term_NEW |> xmlstr 0;
1.109 +if str =
1.110 +"(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n. . aaa + bbb\n. (/TERM)\n(/FORMULA)\n"
1.111 +then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
1.112 +writeln str;
1.113 +
1.114 +"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
1.115 +"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
1.116 +"--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
1.117 +(* xml_of_term_NEW o xml_to_term_NEW = id ... not valid,
1.118 + as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.
1.119 +val t = @{term "aaa + bbb::real"};
1.120 +if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
1.121 +else error "xml_of_term_NEW |> xml_to_term_NEW changed"
1.122 +*)
1.123 +
1.124 +"--------- create testdata for TestPIDE.java#testTermTransfer ----";
1.125 +"--------- create testdata for TestPIDE.java#testTermTransfer ----";
1.126 +"--------- create testdata for TestPIDE.java#testTermTransfer ----";
1.127 +val t = @{term "aaa + bbb::real"};
1.128 +val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
1.129 +(* check the term structure *)
1.130 +val Const ("HOL.eq", T1) $
1.131 + (Const ("Groups.plus_class.plus", T2) $
1.132 + Free ("aaa", T3) $
1.133 + Free ("bbb", _)) $
1.134 + Const ("processed_by_Isabelle_Isac", _) = ttt;
1.135 +
1.136 +(* check the type structure *)
1.137 +atomtyp T3;
1.138 +Type ("Real.real", []);
1.139 +
1.140 +atomtyp T2;
1.141 +(*
1.142 +*** Type (fun,[
1.143 +*** . Type (Real.real,[])
1.144 +*** . Type (fun,[
1.145 +*** . . Type (Real.real,[])
1.146 +*** . . Type (Real.real,[])
1.147 +*** . . ]
1.148 +*** . ]
1.149 +with this ^^^ build the typ ...*)
1.150 +Type ("fun", [
1.151 + Type ("Real.real", []),
1.152 + Type ("fun", [
1.153 + Type ("Real.real", []),
1.154 + Type ("Real.real", [])])]);
1.155 +
1.156 +atomtyp T1;
1.157 +(*
1.158 +*** Type (fun,[
1.159 +*** . Type (Real.real,[])
1.160 +*** . Type (fun,[
1.161 +*** . . Type (Real.real,[])
1.162 +*** . . Type (HOL.bool,[])
1.163 +*** . . ]
1.164 +*** . ]
1.165 +with this ^^^ build the typ ...*)
1.166 +Type ("fun", [
1.167 + Type ("Real.real", []),
1.168 + Type ("fun", [
1.169 + Type ("Real.real", []),
1.170 + Type ("HOL.bool", [])])]);
1.171 +
1.172 +(* now compose term + typ *)
1.173 +val Const ("HOL.eq", Type ("fun", [
1.174 + Type ("Real.real", []),
1.175 + Type ("fun", [
1.176 + Type ("Real.real", []),
1.177 + Type ("HOL.bool", [])])])) $
1.178 + (Const ("Groups.plus_class.plus", Type ("fun", [
1.179 + Type ("Real.real", []),
1.180 + Type ("fun", [
1.181 + Type ("Real.real", []),
1.182 + Type ("Real.real", [])])])) $
1.183 + Free ("aaa", Type ("Real.real", [])) $
1.184 + Free ("bbb", Type ("Real.real", []))) $
1.185 + Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
1.186 +
1.187 +(* match out the original term from result*)
1.188 +val Const ("HOL.eq", Type ("fun", [
1.189 + Type ("Real.real", []),
1.190 + Type ("fun", [
1.191 + Type ("Real.real", []),
1.192 + Type ("HOL.bool", [])])])) $
1.193 + t' $
1.194 + Const ("processed_by_Isabelle_Isac", Type ("Real.real", [])) = ttt;
1.195 +if t = t' then () else error "something with test_term changed"