(* intermediately stores !ptyps

   WN.16.9.01

   use"tests/refine.sml";

   *)

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

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

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

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

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

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

val intermediate_ptyps = !ptyps;

ptyps:= ([]:ptyps);

store_pbt

 (prep_pbt DiffApp.thy

 (["pbla"],         

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

store_pbt

 (prep_pbt DiffApp.thy

 (["pbla1","pbla"], 

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

store_pbt

 (prep_pbt DiffApp.thy

 (["pbla2","pbla"], 

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

store_pbt

 (prep_pbt DiffApp.thy

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

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

  e_rls, None, []));

store_pbt

 (prep_pbt DiffApp.thy

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

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

  e_rls, None, []));

store_pbt

 (prep_pbt DiffApp.thy

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

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

  e_rls, None, []));

store_pbt

 (prep_pbt DiffApp.thy

 (["pbla3","pbla"],

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

  e_rls, None, []));

show_ptyps();

(*case 1: no refinement *)

val thy = Isac.thy;

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

				"fixedValues [aaa=0]");

val (d2,ts2,vs2) = 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,vs2) = 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,vs2) = 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,vs3) = 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 ----------------------------";

(*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 ----------------------------";

(*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 raise 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 ----------------------------";

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;

show_ptyps();

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

"----------------refine.sml: miniscript with mini-subpbl -------------";

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.thy","squ-equ-test-subpbl1"));

val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

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

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

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

val nxt = ("Specify_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=[Incompl "errorBound",

                 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_Given",Add_Given "errorBound (eps = #0)")*)

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

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

(*val nxt = ("Refine_Problem",Refine_Problem ["linear","univariate","equation","test"]

             kann nicht gut gehen            --------- *)

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

(*val nxt = ("Specify_Problem",Specify_Problem []) FIXXXME*)

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","equation","test"])*)

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;

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

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

(*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep

  in Script "uberdefiniert                         -^-*)

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

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

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

(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #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;

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

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

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

(*val nxt = ("Specify_Method",Specify_Method ("RatArith.thy","solve_linear"))*)

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

(*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","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 (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",Check_Postcond ["normalize","univariate","equation","test"])*)

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

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

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

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