Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/xmlsrc/mathml.sml
author Walther Neuper <wneuper@ist.tugraz.at>
Mon, 26 Aug 2019 17:40:27 +0200
changeset 59592 99c8d2ff63eb
parent 59471 f2b3681fafb9
permissions -rw-r--r--
rename Isac.thy --> Isac_Knowledge.thy 
     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 "-----------------------------------------------------------------";

    21 

    22 

    23 

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

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

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

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

    28 

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

    35 

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

    42 

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

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

    45 formula2xml 1 (str2term str);

    46 

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

    52 

    53 parse_patt;

    54 parse_patt (Thy_Info_get_theory "Isac_Knowledge");

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

    56 Failed to parse term*)*)

    57 

    58 "~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac_Knowledge"), 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*)*)

    63 

    64 Proof_Context.read_term_pattern;

    65 (@{theory "Isac_Knowledge"}, 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 ================================================*)

    74 

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

    82 

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

    86 

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

    93 

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

   100 

   101 "--------- fun xmlstr --------------------------------------------";

   102 "--------- fun xmlstr --------------------------------------------";

   103 "--------- fun xmlstr --------------------------------------------";

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

   105 val str = term |> xml_of_term_NEW |> xmlstr 0;

   106 if str =

   107 "(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n. . aaa + bbb\n. (/TERM)\n(/FORMULA)\n"

   108 then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";

   109 writeln str;

   110 

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

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

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

   114 (* xml_of_term_NEW o xml_to_term_NEW = id ... not valid, 

   115   as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.

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

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

   118 else error "xml_of_term_NEW |> xml_to_term_NEW changed"

   119 *)

   120 

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

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

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

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

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

   126 (* check the term structure *)

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

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

   129         Free ("aaa", T3) $ 

   130         Free ("bbb", _)) $

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

   132 

   133 (* check the type structure *)

   134 atomtyp T3;

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

   136 

   137 atomtyp T2;

   138 (*

   139 *** Type (fun,[

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

   141 *** . Type (fun,[

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

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

   144 *** . . ]

   145 *** . ]

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

   147 Type ("fun", [

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

   149   Type ("fun", [

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

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

   152 

   153 atomtyp T1;

   154 (*

   155 *** Type (fun,[

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

   157 *** . Type (fun,[

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

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

   160 *** . . ]

   161 *** . ]

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

   163 Type ("fun", [

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

   165   Type ("fun", [

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

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

   168 

   169 (* now compose term + typ *)

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

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

   172                        Type ("fun", [

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

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

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

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

   177                                          Type ("fun", [

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

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

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

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

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

   183 

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

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

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

   187                        Type ("fun", [

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

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

   190       t' $

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

   192 if t = t' then () else error "something with test_term changed"
wneuper/isa