akargl@42176: (* Title: tests for mathml.sml
akargl@42176:    Author: Walther Neuper 060311
neuper@37906:    (c) isac-team 2006
neuper@37906: *)
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "exported from struct --------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "--------- ... ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "within struct ---------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: (*==================================================================*)
neuper@37906: 
wneuper@59177: 
wneuper@59224: "--------- fun xmlstr --------------------------------------------";
wneuper@59224: "--------- fun xmlstr --------------------------------------------";
wneuper@59224: "--------- fun xmlstr --------------------------------------------";
wneuper@59224: val term = @{term "aaa + bbb::real"};
wneuper@59224: val str = term |> xml_of_term_NEW |> xmlstr 0;
wneuper@59224: if str =
walther@59617: "(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"
wneuper@59224: then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
wneuper@59224: writeln str;
wneuper@59224: 
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59213: "--------- fun xml_of_term_NEW, xml_to_term_NEW ------------------";
wneuper@59224: (* xml_of_term_NEW o xml_to_term_NEW = id ... not valid, 
wneuper@59224:   as long as the latter (going: frontend \<longrightarrow> kernel) does only carry "ISA" string.
wneuper@59213: val t = @{term "aaa + bbb::real"};
wneuper@59213: if t = (t |> xml_of_term_NEW |> xml_to_term_NEW) then ()
wneuper@59213: else error "xml_of_term_NEW |> xml_to_term_NEW changed"
wneuper@59224: *)
wneuper@59214: 
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
wneuper@59214: "--------- create testdata for TestPIDE.java#testTermTransfer ----";
wneuper@59214: val t = @{term "aaa + bbb::real"};
wneuper@59214: val ttt = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
wneuper@59214: (* check the term structure *)
wenzelm@60309: val Const (\<^const_name>\<open>HOL.eq\<close>, T1) $
wenzelm@60309:      (Const (\<^const_name>\<open>plus\<close>, T2) $ 
wneuper@59214:         Free ("aaa", T3) $ 
wneuper@59214:         Free ("bbb", _)) $
wneuper@59214:       Const ("processed_by_Isabelle_Isac", _) = ttt;
wneuper@59214: 
wneuper@59214: (* check the type structure *)
Walther@60650: TermC.atom_typ @{context} T3;
wenzelm@60309: Type (\<^type_name>\<open>real\<close>, []);
wneuper@59214: 
Walther@60650: TermC.atom_typ @{context} T2;
wneuper@59214: (*
wneuper@59214: *** Type (fun,[
wneuper@59214: *** . Type (Real.real,[])
wneuper@59214: *** . Type (fun,[
wneuper@59214: *** . . Type (Real.real,[])
wneuper@59214: *** . . Type (Real.real,[])
wneuper@59214: *** . . ]
wneuper@59214: *** . ]
walther@60242: with this \<up> build the typ ...*)
wenzelm@60309: Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:   Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:   Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:     Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:     Type (\<^type_name>\<open>real\<close>, [])])]);
wneuper@59214: 
Walther@60650: TermC.atom_typ @{context} T1;
wneuper@59214: (*
wneuper@59214: *** Type (fun,[
wneuper@59214: *** . Type (Real.real,[])
wneuper@59214: *** . Type (fun,[
wneuper@59214: *** . . Type (Real.real,[])
wneuper@59214: *** . . Type (HOL.bool,[])
wneuper@59214: *** . . ]
wneuper@59214: *** . ]
walther@60242: with this \<up> build the typ ...*)
wenzelm@60309: Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:   Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:   Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:     Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:     Type (\<^type_name>\<open>bool\<close>, [])])]);
wneuper@59214: 
wneuper@59214: (* now compose term + typ *)
wenzelm@60309: val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:                        Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:                        Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:                          Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:                          Type (\<^type_name>\<open>bool\<close>, [])])])) $
wenzelm@60309:      (Const (\<^const_name>\<open>plus\<close>, Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:                                          Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:                                          Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:                                            Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:                                            Type (\<^type_name>\<open>real\<close>, [])])])) $ 
wenzelm@60309:         Free ("aaa", Type (\<^type_name>\<open>real\<close>, [])) $ 
wenzelm@60309:         Free ("bbb", Type (\<^type_name>\<open>real\<close>, []))) $
wenzelm@60309:       Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
wneuper@59214: 
wneuper@59214: (* match out the original term from result*)
wenzelm@60309: val Const (\<^const_name>\<open>HOL.eq\<close>, Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:                        Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:                        Type (\<^type_name>\<open>fun\<close>, [
wenzelm@60309:                          Type (\<^type_name>\<open>real\<close>, []), 
wenzelm@60309:                          Type (\<^type_name>\<open>bool\<close>, [])])])) $
wneuper@59214:       t' $
wenzelm@60309:       Const ("processed_by_Isabelle_Isac", Type (\<^type_name>\<open>real\<close>, [])) = ttt;
wneuper@59214: if t = t' then () else error "something with test_term changed"