wneuper/isa: test/Tools/isac/BridgeLibisabelle/mathml.sml@ac7426ab0491

     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 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

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

    12 "-----------------------------------------------------------------";

    13 "exported from struct --------------------------------------------";

    14 "-----------------------------------------------------------------";

    15 "--------- ... ---------------------------------------------------";

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

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

    21 "within struct ---------------------------------------------------";

    22 "-----------------------------------------------------------------";

    23 (*==================================================================*)

    26 "--------- fun xmlstr --------------------------------------------";

    27 "--------- fun xmlstr --------------------------------------------";

    28 "--------- fun xmlstr --------------------------------------------";

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

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

    31 if str =

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

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

    34 writeln str;

    36 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

    37 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

    38 "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";

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

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

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

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

    43 else error "xml_of_term_NEW |> xml_to_term_NEW changed"

    44 *)

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

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

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

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

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

    51 (* check the term structure *)

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

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

    54         Free ("aaa", T3) $

    55         Free ("bbb", _)) $

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

    58 (* check the type structure *)

    59 atomtyp T3;

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

    62 atomtyp T2;

    63 (*

    64 *** Type (fun,[

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

    66 *** . Type (fun,[

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

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

    69 *** . . ]

    70 *** . ]

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

    72 Type ("fun", [

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

    74   Type ("fun", [

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

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

    78 atomtyp T1;

    79 (*

    80 *** Type (fun,[

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

    82 *** . Type (fun,[

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

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

    85 *** . . ]

    86 *** . ]

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

    88 Type ("fun", [

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

    90   Type ("fun", [

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

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

    94 (* now compose term + typ *)

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

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

    97                        Type ("fun", [

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

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

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

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

   102                                          Type ("fun", [

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

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

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

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

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

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

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

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

   112                        Type ("fun", [

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

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

   115       t' $

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

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

author	wneuper <walther.neuper@jku.at>
	Tue, 20 Apr 2021 17:10:02 +0200
changeset 60244	ac7426ab0491
parent 60242	73ee61385493
child 60309	70a1d102660d
permissions	-rw-r--r--