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/BridgeLibisabelle/mathml.sml
author wneuper <walther.neuper@jku.at>
Tue, 20 Apr 2021 16:58:44 +0200
changeset 60242 73ee61385493
parent 60230 0ca0f9363ad3
child 60244 ac7426ab0491
permissions -rw-r--r--
replace power ^^^ by \<up> 
     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 \<up> -> ^ ---------------------------------------";

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

    12 "--------- fun rm_doublets '-4 * b \<up>\<up>\<up> 2 / (...' -----------";

    13 "--------- fun decode '-4 * b \<up>\<up>\<up> 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 \<up> -> ^ ---------------------------------------";

    30 "--------- encode \<up> -> ^ ---------------------------------------";

    31 "--------- encode \<up> -> ^ ---------------------------------------";

    32 val str = "a\<up>2+b\<up>2=c\<up>2";

    33 if decode str = "a\<up>2+b\<up>2=c\<up>2" then ()

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

    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  \<up>  ?n = ?a * ?b  \<up>  - ?n";

    40 if decode str = "?bdv occurs_in ?b; 0 &lt; ?n |] ==&gt; ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?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 (TermC.str2term str);

    46 

    47 (* AK110725 

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

    49                    Failed to TermC.parse term*)*)

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

    51 ThyC.get_theory "Isac_Knowledge";

    52 

    53 TermC.parse_patt;

    54 TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");

    55 (*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

    56 Failed to TermC.parse term*)*)

    57 

    58 "~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);

    59 (thy, str) 

    60 |>> ThyC.to_ctxt

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

    62 Failed to TermC.parse term*)*)

    63 

    64 Proof_Context.read_term_pattern;

    65 (@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;

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

    76 "--------- fun xmlstr --------------------------------------------";

    77 "--------- fun xmlstr --------------------------------------------";

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

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

    80 if str =

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

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

    83 writeln str;

    84 

    85 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

    86 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

    87 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

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

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

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

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

    92 else error "xml_of_term_NEW |> xml_to_term_NEW changed"

    93 *)

    94 

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

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

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

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

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

   100 (* check the term structure *)

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

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

   103         Free ("aaa", T3) $ 

   104         Free ("bbb", _)) $

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

   106 

   107 (* check the type structure *)

   108 atomtyp T3;

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

   110 

   111 atomtyp T2;

   112 (*

   113 *** Type (fun,[

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

   115 *** . Type (fun,[

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

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

   118 *** . . ]

   119 *** . ]

   120 with this \<up> build the typ ...*)

   121 Type ("fun", [

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

   123   Type ("fun", [

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

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

   126 

   127 atomtyp T1;

   128 (*

   129 *** Type (fun,[

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

   131 *** . Type (fun,[

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

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

   134 *** . . ]

   135 *** . ]

   136 with this \<up> build the typ ...*)

   137 Type ("fun", [

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

   139   Type ("fun", [

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

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

   142 

   143 (* now compose term + typ *)

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

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

   146                        Type ("fun", [

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

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

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

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

   151                                          Type ("fun", [

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

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

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

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

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

   157 

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

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

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

   161                        Type ("fun", [

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

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

   164       t' $

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

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