(* Title: test for sml/xmlsrc/datatypes.sml

   Authors: Walther Neuper 2003

   (c) due to copyright terms

use"../smltest/xmlsrc/datatypes.sml";

use"datatypes.sml";

*)

"-----------------------------------------------------------------";

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

"-----------------------------------------------------------------";

"----------- fun rules2xml ---------------------------------------";

"----------- fun thm''2xml ---------------------------------------";

"----------- fun xml_of_model ------------------------------------------------------------------";

"----------- fun xml_of_tac --------------------------------------------------------------------";

"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"----------- fun rules2xml ---------------------------------------";

"----------- fun rules2xml ---------------------------------------";

"----------- fun rules2xml ---------------------------------------";

show_thes();

val thyID = "Test";

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

val thydata = Thy_Read.from_store ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];

(*AK110725 

(*val thydata = Thy_Read.from_store ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]; 

  (* ERROR: Problem.from_store not found: ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"] *)*)

"~~~~~ fun Thy_Read.from_store, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);

(*get_py  (ThyC.get_theory "Pure") theID theID (get_thes ()); 

  (* ERROR: Problem.from_store not found: ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"] *)*)

(*default_print_depth 3; 999*)

(get_thes ());

(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));*)

"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));

error ("Problem.from_store not found: "^(strs2str d));

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

*)

val Hrls {thy_rls = (_,Rule_Set.Repeat {rules = rules as rule::_,...}),...} = thydata;

(*for rule2xml...*)

val (j, thyID, Thm (thmID, thm)) = (2, thyID, rule);

val (isa, thyID') = thy_containing_thm thyID thmID;

val guh = thm2guh (isa, thyID') thmID;

writeln (rules2xml 2 "Test" rules);

"----------- fun thm''2xml ---------------------------------------";

"----------- fun thm''2xml ---------------------------------------";

"----------- fun thm''2xml ---------------------------------------";

show_thes();

val theID = ["IsacKnowledge", "Diff", "Theorems", "frac_conv"];

val thydata = Thy_Read.from_store theID;

val Hthm {guh=guh, thm=thm, mathauthors=ma, coursedesign=co} = thydata;

writeln(thydata2xml (theID, thydata));

"----- check 'manually' ...0 &lt ?n |] ==&gt ?a... -----";

"---------------------------- \<up> --------- \<up> ------------";

(* use"../smltest/xmlsrc/datatypes.sml";

   *)

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

"----------- fun xml_of_model ------------------------------------------------------------------";

"----------- fun xml_of_model ------------------------------------------------------------------";

"----------- fun xml_of_model ------------------------------------------------------------------";

(*create testdata: see --- tryrefine --- 

  xml_of_model used via refineProblem \<longrightarrow> matchpbl2xml \<longrightarrow> model2xml*)

reset_states ();

CalcTree [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)", 

	    "solveFor x", "solutions L"],

	   ("RatEq",["univariate", "equation"],["no_met"]))];

Iterator 1;

moveActiveRoot 1; autoCalculate 1 CompleteCalc;

refineProblem 1 ([1],Res) "pbl_equ_univ"; 

"~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : Check_Unique.id)) = 

  (1, ([1],Res), "pbl_equ_univ");

val pblID = Ptool.guh2kestoreID guh

	 val ((pt,_),_) = get_calc cI

	 val pp = par_pblobj pt p

	 val chd = tryrefine pblID pt (pp, p_);

"~~~~~ fun matchpbl2xml, args:"; val ((cI:calcID), (model_ok, pI, hdl, pbl, pre)) = (cI, chd);

"~~~~~ fun model2xml, args:"; val (j, (itms:I_Model.T), where_) = (i, pbl, pre);

"~~~~~ fun xml_of_model, args:"; val (itms, where_) = (pbl, pre);

val xxx = xml_of_model itms where_;

(xmlstr 0 xxx);

writeln(xmlstr 0 xxx);

if xmlstr 0 xxx = "(MODEL)\n. (GIVEN)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . equality (x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solveFor x\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/GIVEN)\n. (WHERE)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/WHERE)\n. (FIND)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solutions L\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/FIND)\n. (RELATE)\n. (/RELATE)\n(/MODEL)\n"

then () else error ("xml_of_model changed = " ^ xmlstr 0 xxx);

"----------- fun xml_of_tac --------------------------------------------------------------------";

"----------- fun xml_of_tac --------------------------------------------------------------------";

"----------- fun xml_of_tac --------------------------------------------------------------------";

(* WN150814 these are the Java objects.

import isac.util.tactics.RewriteInst

import isac.util.tactics.RewriteSet

import isac.util.tactics.RewriteSetInst

import isac.util.tactics.SimpleTactic        ...not appropriately abstracted

import isac.util.tactics.StringListTactic    ...not appropriately abstracted

import isac.util.tactics.SubProblemTactic

import isac.util.tactics.Tactic

*)

Rewrite: ThmC.T -> Tactic.input;

val tac = Rewrite("refl", @{thm refl});

if xmlstr 0 (xml_of_tac tac) =

(*---xml_of_tac------------------------------------------thm'_to_thm''--------------

"(REWRITETACTIC name=Rewrite)\n" ^ 

". (THEOREM)\n" ^ 

". . (ID)\n" ^ 

". . . refl\n" ^ 

". . (/ID)\n" ^ 

". . (FORMULA)\n" ^ 

". . . (ISA)\n" ^ 

". . . . a = a\n" ^ 

". . . (/ISA)\n" ^ 

". . . (TERM)\n" ^ 

". . . . ?t = ?t\n" ^ 

". . . (/TERM)\n" ^ 

". . (/FORMULA)\n" ^ 

". (/THEOREM)\n" ^ 

-----xml_of_tac------------------------------------------thm'_to_thm''------------*)

"(REWRITETACTIC name=Rewrite)\n" ^ 

". (THEOREM)\n" ^ 

". . (ID)\n" ^ 

". . . refl\n" ^ 

". . (/ID)\n" ^ 

". . (FORMULA)\n" ^ 

". . . ?t = ?t\n" ^ 

". . (/FORMULA)\n" ^ 

". (/THEOREM)\n" ^ 

"(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";

Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;

val tac = Rewrite_Inst(["(''bdv'', x)"], ("refl", @{thm refl}));

if xmlstr 0 (xml_of_tac tac) = 

"(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^ 

". (SUBSTITUTION)\n" ^ 

". . (PAIR)\n" ^ 

". . . (VARIABLE)\n" ^ 

". . . . (MATHML)\n" ^ (* TODO *)

". . . . . (ISA)\n" ^ 

". . . . . . bdv\n" ^ 

". . . . . (/ISA)\n" ^ 

". . . . (/MATHML)\n" ^ 

". . . (/VARIABLE)\n" ^ 

". . . (VALUE)\n" ^ 

". . . . (MATHML)\n" ^ 

". . . . . (ISA)\n" ^ 

". . . . . . x\n" ^ 

". . . . . (/ISA)\n" ^ 

". . . . (/MATHML)\n" ^ 

". . . (/VALUE)\n" ^ 

". . (/PAIR)\n" ^ 

". (/SUBSTITUTION)\n" ^ 

(*---xml_of_tac------------------------------------------thm'_to_thm''--------------

". (THEOREM)\n" ^ 

". . (ID)\n" ^ 

". . . refl\n" ^ 

". . (/ID)\n" ^ 

". . (FORMULA)\n" ^  (* OK *)

". . . (ISA)\n" ^ 

". . . . a = a\n" ^ 

". . . (/ISA)\n" ^ 

". . . (TERM)\n" ^ 

". . . ?t = ?t\n" ^ 

". . . (/TERM)\n" ^ 

". . (/FORMULA)\n" ^ 

". (/THEOREM)\n" ^ 

-----xml_of_tac------------------------------------------thm'_to_thm''------------*)

". (THEOREM)\n" ^ 

". . (ID)\n" ^ 

". . . refl\n" ^ 

". . (/ID)\n" ^ 

". . (FORMULA)\n" ^ 

". . . ?t = ?t\n" ^ 

". . (/FORMULA)\n" ^ 

". (/THEOREM)\n" ^ 

"(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";

Rewrite_Set: Rule_Set.id -> Tactic.input;

val tac = Rewrite_Set("simplify");

if xmlstr 0 (xml_of_tac tac) = "(REWRITESETTACTIC name=Rewrite_Set)\n" ^ 

". simplify\n" ^ 

"(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";

Rewrite_Set_Inst: Subst.input * Rule_Set.id -> Tactic.input;

val tac = Rewrite_Set_Inst(["(''bdv'', x)"], "simplify");

if xmlstr 0 (xml_of_tac tac) =

"(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^ 

". (SUBSTITUTION)\n" ^ 

". . (PAIR)\n" ^ 

". . . (VARIABLE)\n" ^ 

". . . . (MATHML)\n" ^ (* TODO *)

". . . . . (ISA)\n" ^ 

". . . . . . bdv\n" ^ 

". . . . . (/ISA)\n" ^ 

". . . . (/MATHML)\n" ^ 

". . . (/VARIABLE)\n" ^ 

". . . (VALUE)\n" ^ 

". . . . (MATHML)\n" ^ 

". . . . . (ISA)\n" ^ 

". . . . . . x\n" ^ 

". . . . . (/ISA)\n" ^ 

". . . . (/MATHML)\n" ^ 

". . . (/VALUE)\n" ^ 

". . (/PAIR)\n" ^ 

". (/SUBSTITUTION)\n" ^ 

". (RULESET)\n" ^ 

". . simplify\n" ^ 

". (/RULESET)\n" ^ 

"(/REWRITESETINSTTACTIC)\n"then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";

"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

"----------- these are : TermC.as_string -> tac: WN150814 THESE WELL BECOME TermTactic TERMTACTIC";

Add_Given: TermC.as_string -> Tactic.input;

Add_Find: TermC.as_string -> Tactic.input;

Add_Relation: TermC.as_string -> Tactic.input;

Check_elementwise: TermC.as_string -> Tactic.input;

Take: TermC.as_string -> Tactic.input;

Add_Given: TermC.as_string -> Tactic.input;

val tac = Add_Given("equality (x + 1 = 2)");

xml_of_tac tac;(*

<FORMTACTIC name="Add_Given">

  <MATHML>

    <ISA>equality (x + 1 = 2)</ISA>

  </MATHML>

</FORMTACTIC>*)

if xmlstr 0 (xml_of_tac tac) = "(FORMTACTIC name=Add_Given)\n. (MATHML)\n. . (ISA)\n. . . equality (x + 1 = 2)\n. . (/ISA)\n. (/MATHML)\n(/FORMTACTIC)\n"

then () else error "xml_of_tac Add_Given CHANGED";

"----------- these are : string -> tac: ";

Calculate: string -> Tactic.input;; (* should be the operator*)

Specify_Theory: ThyC.id -> Tactic.input;;

val tac = Specify_Theory("Differentiate");

xml_of_tac tac;(*

<SIMPLETACTIC name="Specify_Theory">

  <MATHML>                               NONSENSE

    <ISA>Differentiate</ISA>

  </MATHML>

</SIMPLETACTIC>*)

if xmlstr 0 (xml_of_tac tac) = "(SIMPLETACTIC name=Specify_Theory)\n. Differentiate\n(/SIMPLETACTIC)\n"

then () else error "xml_of_tac Specify_Theory CHANGED";

"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

Model_Problem: Tactic.input;

Or_to_List: Tactic.input;

Apply_Method: MethodC.id -> Tactic.input;

Refine_Tacitly: Problem.id -> Tactic.input;

Specify_Problem: Problem.id -> Tactic.input;

Specify_Method: MethodC.id -> Tactic.input;

Substitute: Subst.input -> Tactic.input;; (* Substitute: sube -> tac; Subst.string_eqs_empty: TermC.as_string list; UNCLEAR HOW TO INPUT *)

Check_Postcond: Problem.id -> Tactic.input;

Apply_Method: MethodC.id -> Tactic.input;

val tac = Apply_Method(["test", "equation", "simplify"]);

xml_of_tac tac;(*

<STRINGLISTTACTIC name="Apply_Method">

  <STRINGLIST>

    <STRING>test</STRING>

    <STRING>equation</STRING>

    <STRING>simplify</STRING>

  </STRINGLIST>

</STRINGLISTTACTIC>*)

if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Apply_Method)\n. (STRINGLIST)\n. . (STRING)\n. . . test\n. . (/STRING)\n. . (STRING)\n. . . equation\n. . (/STRING)\n. . (STRING)\n. . . simplify\n. . (/STRING)\n. (/STRINGLIST)\n(/STRINGLISTTACTIC)\n"

then () else error "xml_of_tac Apply_Method CHANGED";

"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

(* Note: tacs Substitute, Rewrite_Inst* have different substitutions,

while input in frontend is not yet clear: *)

Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;

Substitute  : Subst.input -> Tactic.input;

Subst.input_empty: Subst.input;

Subst.input_empty: Subst.input;

val subs = ["(''bdv_1'', xxx)", "(''bdv_2'', yyy)"]: TermC.as_string list;

xml_of_subs subs;(*

<SUBSTITUTION>

  <PAIR>

    <VARIABLE>

      <MATHML>

        <ISA>bdv_1</ISA>

      </MATHML>

    </VARIABLE>

    <VALUE><

      MATHML>

        <ISA>xxx</ISA>

      </MATHML>

    </VALUE>

  </PAIR>

  <PAIR>

    <VARIABLE>

      <MATHML>

        <ISA>bdv_2</ISA>

      </MATHML>

    </VARIABLE>

    <VALUE>

      <MATHML>

        <ISA>yyy</ISA>

      </MATHML>

    </VALUE>

  </PAIR>

</SUBSTITUTION>:*)

val tac = Rewrite_Inst (subs, ("diff_sin_chain", @{thm diff_sin_chain}));

val xml = xml_of_tac tac;

if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"

then () else error "xml_of_tac Rewrite_Inst CHANGED";

val Rewrite_Inst (["(''bdv_1'', xxx)", "(''bdv_2'', yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;

if (UnparseC.term o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"

then () else error "xml_to_tac Rewrite_Inst CHANGED";

val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: Subst.input;

Subst.string_eqs_empty: TermC.as_string list;

Subst.string_eqs_empty: Subst.input;

xml_of_sube sube;(*

<SUBSTITUTION>

  <PAIR>

    <VARIABLE>

      <MATHML>

        <ISA>bdv_1</ISA>

      </MATHML>

    </VARIABLE>

    <VALUE>

      <MATHML>

        <ISA>xxx</ISA>

      </MATHML>

    </VALUE>

  </PAIR>

  <PAIR>

    <VARIABLE>

      <MATHML>

        <ISA>bdv_2</ISA>

      </MATHML>

    </VARIABLE>

    <VALUE>

      <MATHML>

        <ISA>yyy</ISA>

      </MATHML>

    </VALUE>

  </PAIR>

</SUBSTITUTION>:*)

val tac = Substitute sube;

val xml = xml_of_tac tac;

if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"

then () else error "xml_of_tac Substitute CHANGED";

case xml_to_tac xml of Substitute ["bdv_1 = xxx", "bdv_2 = yyy"] => ()

| _ => error "xml_to_tac Substitute CHANGED";