wneuper/isa: test/Tools/isac/xmlsrc/mathml.sml@5ce72a592f7f

     1 (* Title: tests for mathml.sml

     2    Author: Walther Neuper 060311

     3    (c) isac-team 2006

     4 *)

     5 "-----------------------------------------------------------------";

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

     7 "-----------------------------------------------------------------";

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

     9 "-----------------------------------------------------------------";

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

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

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

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

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

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

    16 "-----------------------------------------------------------------";

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

    18 "-----------------------------------------------------------------";

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

    20 "-----------------------------------------------------------------";

    24 "-----------------------------------------------------------------";

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

    26 "-----------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    45 formula2xml 1 (str2term str);

    47 (* AK110725

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

    49                    Failed to parse term*)*)

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

    51 Thy_Info.get_theory "Isac";

    53 parse_patt;

    54 parse_patt (Thy_Info.get_theory "Isac");

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

    56 Failed to parse term*)*)

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

    59 (thy, str)

    60 |>> thy2ctxt

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

    62 Failed to parse term*)*)

    64 Proof_Context.read_term_pattern;

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

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

    67 (*AK110725 To be continued...*)

    68 *)

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

    70 "-----------------------------------------------------------------";

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

    72 "-----------------------------------------------------------------";

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

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

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

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

    78 val c = "^";

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

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

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

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

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

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

    87 val cstr =

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

    89 val cs = Symbol.explode cstr;

    90 if rm_doublets c [] cs = Symbol.explode

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

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

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

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

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

    97 if encode cstr =

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

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

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

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

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

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

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

   106 else error "xml_of_term_NEW |> xml_to_term_NEW changed"

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

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

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

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

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

   113 (* check the term structure *)

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

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

   116         Free ("aaa", T3) $

   117         Free ("bbb", _)) $

   118       Const ("processed_by_Isabelle_Isac", _) = ttt;

   120 (* check the type structure *)

   121 atomtyp T3;

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

   124 atomtyp T2;

   125 (*

   126 *** Type (fun,[

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

   128 *** . Type (fun,[

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

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

   131 *** . . ]

   132 *** . ]

   133 with this ^^^ build the typ ...*)

   134 Type ("fun", [

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

   136   Type ("fun", [

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

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

   140 atomtyp T1;

   141 (*

   142 *** Type (fun,[

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

   144 *** . Type (fun,[

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

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

   147 *** . . ]

   148 *** . ]

   149 with this ^^^ build the typ ...*)

   150 Type ("fun", [

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

   152   Type ("fun", [

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

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

   156 (* now compose term + typ *)

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

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

   159                        Type ("fun", [

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

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

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

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

   164                                          Type ("fun", [

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

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

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

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

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

   171 (* match out the original term from result*)

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

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

   174                        Type ("fun", [

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

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

   177       t' $

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

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

author	Walther Neuper <wneuper@ist.tugraz.at>
	Fri, 05 Feb 2016 16:05:11 +0100
changeset 59214	5ce72a592f7f
parent 59213	80d2d4d80618
child 59224	bb8ceff84b96
permissions	-rw-r--r--