(* tests for ME/ptyps.sml

   CAUTION: intermediately stores !ptyps THUS EVALUATE IN 1 GO

   author: Walther Neuper

   010916,

   (c) due to copyright terms

use"../smltest/ME/ptyps.sml";

use"ptyps.sml";

*)

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

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

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

"###### val intermediate_ptyps = !ptyps; #########################";

"----------- store test-pbtyps -----------------------------------";

"----------- refin test-pbtyps -----------------------------------";

"----------- refine_ori test-pbtyps ------------------------------";

"----------- refine test-pbtyps ----------------------------------";

"###### ptyps:= intermediate_ptyps;###############################";

"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";

"----------- fun coll_guhs ---------------------------------------";

"----------- fun guh2kestoreID -----------------------------------";

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

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

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

"###### val intermediate_ptyps = !ptyps; #########################";

"###### val intermediate_ptyps = !ptyps; #########################";

"###### val intermediate_ptyps = !ptyps; #########################";

val intermediate_ptyps = !ptyps;

"----------- store test-pbtyps -----------------------------------";

"----------- store test-pbtyps -----------------------------------";

"----------- store test-pbtyps -----------------------------------";

ptyps:= ([]:ptyps);

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla" [] e_pblID

 (["pbla"],         

  [("#Given", ["fixedValues a_"])], e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla1" [] e_pblID

 (["pbla1","pbla"], 

  [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla2" [] e_pblID

 (["pbla2","pbla"], 

  [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla2x" [] e_pblID

 (["pbla2x","pbla2","pbla"],

  [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])], 

  e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla2y" [] e_pblID

 (["pbla2y","pbla2","pbla"],

  [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])], 

  e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla2z" [] e_pblID

 (["pbla2z","pbla2","pbla"],

  [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])], 

  e_rls, NONE, []));

store_pbt

 (prep_pbt DiffApp.thy "pbl_pbla3" [] e_pblID

 (["pbla3","pbla"],

  [("#Given" ,["fixedValues a_","relations a3_"])], 

  e_rls, NONE, []));

show_ptyps();

(*case 1: no refinement *)

val thy = Isac.thy;

val (d1,ts1) = split_dts thy ((term_of o the o (parse thy)) 

				"fixedValues [aaa=0]");

val (d2,ts2) = split_dts thy ((term_of o the o (parse thy)) 

				"errorBound (ddd=0)");

val ori1 = [(1,[1],"#Given",d1,ts1),

	    (2,[1],"#Given",d2,ts2)]:ori list;

(*case 2: refined to pbt without children *)

val (d2,ts2) = split_dts thy ((term_of o the o (parse thy)) 

				"relations [aaa333]");

val ori2 = [(1,[1],"#Given",d1,ts1),

	    (2,[1],"#Given",d2,ts2)]:ori list;

(*case 3: refined to pbt with children *)

val (d2,ts2) = split_dts thy ((term_of o the o (parse thy)) 

				"valuesFor [aaa222]");

val ori3 = [(1,[1],"#Given",d1,ts1),

	    (2,[1],"#Given",d2,ts2)]:ori list;

(*case 4: refined to children (without child)*)

val (d3,ts3) = split_dts thy ((term_of o the o (parse thy)) 

				"boundVariable aaa222yyy");

val ori4 = [(1,[1],"#Given",d1,ts1),

	    (2,[1],"#Given",d2,ts2),

	    (3,[1],"#Given",d3,ts3)]:ori list;

"----------- refin test-pbtyps -----------------------------------";

"----------- refin test-pbtyps -----------------------------------";

"----------- refin test-pbtyps -----------------------------------";

(*case 1: no refinement *)

refin [] ori1 (hd (!ptyps));

(*val it = SOME ["pbla"] : pblID option*)

(*case 2: refined to pbt without children *)

refin [] ori2 (hd (!ptyps));

(*val it = SOME ["pbla","pbla3"] : pblID option*)

(*case 3: refined to pbt with children *)

refin [] ori3 (hd (!ptyps));

(*val it = SOME ["pbla","pbla2"] : pblID option*)

(*case 4: refined to children (without child)*)

refin [] ori4 (hd (!ptyps));

(*val it = SOME ["pbla","pbla2","pbla2y"] : pblID option*)

(*case 5: start refinement somewhere in ptyps*)

val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = !ptyps;

refin ["pbla"] ori4 ppp;

(*val it = SOME ["pbla2","pbla2y"] : pblRD option*)

"----------- refine_ori test-pbtyps ------------------------------";

"----------- refine_ori test-pbtyps ------------------------------";

"----------- refine_ori test-pbtyps ------------------------------";

(*case 1: no refinement *)

refine_ori ori1 ["pbla"];

(*val it = NONE : pblID option !!!!*)

(*case 2: refined to pbt without children *)

refine_ori ori2 ["pbla"];

(*val it = SOME ["pbla3","pbla"] : pblID option*)

(*case 3: refined to pbt with children *)

refine_ori ori3 ["pbla"];

(*val it = SOME ["pbla2","pbla"] : pblID option*)

(*case 4: refined to children (without child)*)

val opt = refine_ori ori4 ["pbla"];

if opt = SOME ["pbla2y","pbla2","pbla"] then ()

else error "new behaviour in refine.sml case 4";

(*case 5: start refinement somewhere in ptyps*)

refine_ori ori4 ["pbla2","pbla"];

(*val it = SOME ["pbla2y","pbla2","pbla"] : pblID option*)

"----------- refine test-pbtyps ----------------------------------";

"----------- refine test-pbtyps ----------------------------------";

"----------- refine test-pbtyps ----------------------------------";

val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];

val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];

val fmz3 = ["fixedValues [aaa=0]","valuesFor [aaa222]"];

val fmz4 = ["fixedValues [aaa=0]","valuesFor [aaa222]",

	    "boundVariable aaa222yyy"];

(*case 1: no refinement *)

refine fmz1 ["pbla"];

(* 

*** pass ["pbla"]

*** pass ["pbla","pbla1"]

*** pass ["pbla","pbla2"]

*** pass ["pbla","pbla3"]

val it =

  [Matches

     (["pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",

              Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla1","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

              Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",

              Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla3","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",

              Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]

  : match list*)

(*case 2: refined to pbt without children *)

refine fmz2 ["pbla"];

(* 

*** pass ["pbla"]

*** pass ["pbla","pbla1"]

*** pass ["pbla","pbla2"]

*** pass ["pbla","pbla3"]

val it =

  [Matches

     (["pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],

       Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla1","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

              Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",

              Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),

   Matches

     (["pbla3","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],

       Relate=[],Where=[],With=[]})] : match list*)

(*case 3: refined to pbt with children *)

refine fmz3 ["pbla"];

(* 

*** pass ["pbla"]

*** pass ["pbla","pbla1"]

*** pass ["pbla","pbla2"]

*** pass ["pbla","pbla2","pbla2x"]

*** pass ["pbla","pbla2","pbla2y"]

*** pass ["pbla","pbla2","pbla2z"]

*** pass ["pbla","pbla3"]

val it =

  [Matches

     (["pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],

       Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla1","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

              Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),

   Matches

     (["pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],

       Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2x","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2y","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2z","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Missing "interval a2z_"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla3","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",

              Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]

  : match list*)

(*case 4: refined to children (without child)*)

refine fmz4 ["pbla"];

(* 

*** pass ["pbla"]

*** pass ["pbla","pbla1"]

*** pass ["pbla","pbla2"]

*** pass ["pbla","pbla2","pbla2x"]

*** pass ["pbla","pbla2","pbla2y"]

val it =

  [Matches

     (["pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",

              Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla1","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

              Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],

       Relate=[],Where=[],With=[]}),

   Matches

     (["pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2x","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],

       Relate=[],Where=[],With=[]}),

   Matches

     (["pbla2y","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]

  : match list*)

(*case 5: start refinement somewhere in ptyps*)

refine fmz4 ["pbla2","pbla"];

(* 

*** pass ["pbla","pbla2"]

*** pass ["pbla","pbla2","pbla2x"]

*** pass ["pbla","pbla2","pbla2y"]

val it =

  [Matches

     (["pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

   NoMatch

     (["pbla2x","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],

       Relate=[],Where=[],With=[]}),

   Matches

     (["pbla2y","pbla2","pbla"],

      {Find=[],

       Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

              Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]

  : match list*)

"###### ptyps:= intermediate_ptyps;###############################";

"###### ptyps:= intermediate_ptyps;###############################";

"###### ptyps:= intermediate_ptyps;###############################";

ptyps:= intermediate_ptyps;

show_ptyps();

"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";

"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";

"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";

val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",

	   "errorBound (eps=0)","solutions L"];

val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],

		     ["Test","squ-equ-test-subpbl1"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Add_Find", Add_Find "solutions L")*)

val nxt = ("Specify_Problem",(*vvvv---specify a not-matching problem*)

	   Specify_Problem ["linear","univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*ML> f; 

val it = Form' (PpcKF (0,EdUndef,0,Nundef,

        (Problem ["linear","univariate","equation","test"],

         {Find=[Incompl "solutions []"],

          Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",

                 Correct "solveFor x"],Relate=[],

          Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)

                |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)

                |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)

        |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],

          With=[]}))) : mout

val nxt = ("Add_Find",Add_Find "solutions L") ????!!!!????*)

val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*NEW2*);

(*val nxt = ("Empty_Tac",Empty_Tac) 

... Refine_Problem ["linear"..] fails internally 040312: works!?!*)

val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*("Specify_Problem", Specify_Problem ["normalize", "univariate", ...])*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Specify_Theory", Specify_Theory "Test.thy")*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Apply_Method", *)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = Model_Problem ["linear","univariate","equation","test"]*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(**)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*nxt = Specify_Problem ["linear","univariate","equation","test"])*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)

val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*("Specify_Problem", Specify_Problem ["linear", "univariate", ...])*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*Check_Postcond ["normalize","univariate","equation","test"])*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;

if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()

else error "new behaviour in test:refine.sml:miniscript with mini-subpb";

"----------- fun coll_guhs ---------------------------------------";

"----------- fun coll_guhs ---------------------------------------";

"----------- fun coll_guhs ---------------------------------------";

val n = e_pbt;

(#guh : pbt -> guh) e_pbt;

fun XXXnode coll (Ptyp (_,[n],ns)) =

    [(#guh : pbt -> guh) n]

and XXXnodes coll [] = coll

  | XXXnodes coll (n::ns : pbt ptyp list) = (XXXnode coll n) @ 

					    (XXXnodes coll ns);

(*^^^ this works, but not this ...

fun node coll (Ptyp (_,[n],ns)) =

    [(#guh : 'a -> guh) n]

and nodes coll [] = coll

  | nodes coll (n::ns : 'a ptyp list) = (node coll n) @ (nodes coll ns);

Error:

Can't unify {guh: 'a, ...} with 'b (Cannot unify with explicit type variable)

   Found near #guh : 'a -> guh

i.e. there is no common fun for pbls and mets ?!?*)

coll_pblguhs (!ptyps);

sort string_ord (coll_pblguhs (!ptyps));

show_pblguhs ();

sort_pblguhs ();

"----------- fun guh2kestoreID -----------------------------------";

"----------- fun guh2kestoreID -----------------------------------";

"----------- fun guh2kestoreID -----------------------------------";

"----- we assumed the problem-hierarchy containing 3 elements on toplevel";

val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::

     Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (!ptyps);

(*

nodes [] guh1 (!ptyps);

nodes [] guh2 (!ptyps);

*)

val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)

     ::

     Ptyp (id2,[n2 as {guh=guh2,...} : pbt], 

	   (Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )

     ::

     Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)

     ::

     _ ) = (!ptyps);

(*

nodes [] guh3 (!ptyps);

nodes [] guh21 (!ptyps);

*)