(* Title:  "Specify/refine.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

"refine.thy: store test-pbtyps by 'setup' ------------------------------------------------------";

"----------- testdata for refin, Specify.refine_ori --------------------------------------------";

(*"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";*)

"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";

"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

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

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

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

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

"----------- testdata for refin, Specify.refine_ori --------------------------------------------";

"----------- testdata for refin, Specify.refine_ori --------------------------------------------";

"----------- testdata for refin, Specify.refine_ori --------------------------------------------";

Specify.show_ptyps();

val thy = @{theory "Isac_Knowledge"};

val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};

(*case 1: no refinement *)

val (d1,ts1) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "fixedValues [aaa = 0]");

val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "errorBound (ddd = 0)");

val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;

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

val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "relations [aaa333]");

val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;

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

val (d2,ts2) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "valuesFor [aaa222]");

val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;

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

val (d3,ts3) = Input_Descript.split ((Thm.term_of o the o (TermC.parse thy)) "boundVariable aaa222yyy");

val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;

(*=================================================================

This test expects pbls at a certain position in the tree.

Since parallel evaluation (i.e. Theory_Data) this cannot be expected.

Solutions would be

* provide an access function for a branch (not only leaves)

* sort the tree of pbls.

"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";

"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";

"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";

(* fragile test setup: expects ptyps as fixed *)

val level_1 = case nth 9 (get_ptyps ()) of

Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"

val level_2 = case nth 4 level_1 of

Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"

val pbla_branch = case level_2 of 

[Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";

(*case 1: no refinement *)

case refin [] ori1 (hd pbla_branch) of 

  SOME ["pbla"] => () | _ => error "refin case 1 broken";

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

case refin [] ori2 (hd pbla_branch) of 

  SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";

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

case refin [] ori3 (hd pbla_branch) of 

  SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";

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

case refin [] ori4 (hd pbla_branch) of 

  SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";

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

val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;

case refin ["pbla"] ori4 ppp of 

  SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";

==================================================================*)

"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";

"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";

"----------- Specify.refine_ori test-pbtyps --requires 'setup'----------------------------------";

(*case 1: no refinement *)

case Specify.refine_ori ori1 ["pbla", "refine", "test"] of 

  NONE => () | _ => error "Specify.refine_ori case 1 broken";

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

case Specify.refine_ori ori2 ["pbla", "refine", "test"] of 

  SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 2 broken";

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

case Specify.refine_ori ori3 ["pbla", "refine", "test"] of 

  SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 3 broken";

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

case Specify.refine_ori ori4 ["pbla", "refine", "test"] of 

  SOME ["pbla2y","pbla2","pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 4 broken";

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

case Specify.refine_ori ori4 ["pbla2","pbla", "refine", "test"] of 

  SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Specify.refine_ori case 5 broken";

"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

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 *)

case Specify.refine fmz1 ["pbla", "refine", "test"] of

  [Model.Matches (["pbla", "refine", "test"], _), 

   Model.NoMatch (["pbla1", "pbla", "refine", "test"], _), 

   Model.NoMatch (["pbla2", "pbla", "refine", "test"], _), 

   Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()

 | _ => error "--- Specify.refine test-pbtyps --- broken with case 1";

(* 

*** pass ["pbla"]

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

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

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

val it =

  [Model.Matches

     (["pbla"],

      {Find=[],

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

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

   Model.NoMatch

     (["pbla1","pbla"],

      {Find=[],

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

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

   Model.NoMatch

     (["pbla2","pbla"],

      {Find=[],

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

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

   Model.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 *)

case Specify.refine fmz2 ["pbla", "refine", "test"] of

  [Model.Matches (["pbla", "refine", "test"], _),

   Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),

   Model.NoMatch (["pbla2", "pbla", "refine", "test"], _),

   Model.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()

 | _ => error "--- Specify.refine test-pbtyps --- broken with case 2";

(* 

*** pass ["pbla"]

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

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

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

val it =

  [Model.Matches

     (["pbla"],

      {Find=[],

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

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

   Model.NoMatch

     (["pbla1","pbla"],

      {Find=[],

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

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

   Model.NoMatch

     (["pbla2","pbla"],

      {Find=[],

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

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

   Model.Matches

     (["pbla3","pbla"],

      {Find=[],

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

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

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

case Specify.refine fmz3 ["pbla", "refine", "test"] of

  [Model.Matches (["pbla", "refine", "test"], _),

   Model.NoMatch (["pbla1", "pbla", "refine", "test"], _),

   Model.Matches (["pbla2", "pbla", "refine", "test"], _),

   Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),

   Model.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),

   Model.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),

   Model.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()

 | _ => error "--- Specify.refine test-pbtyps --- broken with case 3";

(* 

*** 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 =

  [Model.Matches

     (["pbla"],

      {Find=[],

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

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

   Model.NoMatch

     (["pbla1","pbla"],

      {Find=[],

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

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

   Model.Matches

     (["pbla2","pbla"],

      {Find=[],

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

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

   Model.NoMatch

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

      {Find=[],

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

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

   Model.NoMatch

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

      {Find=[],

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

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

   Model.NoMatch

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

      {Find=[],

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

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

   Model.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)*)

case Specify.refine fmz4 ["pbla", "refine", "test"] of

    [Model.Matches (["pbla", "refine", "test"], _), 

     Model.NoMatch (["pbla1", "pbla", "refine", "test"], _), 

     Model.Matches (["pbla2", "pbla", "refine", "test"], _), 

     Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), 

     Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- Specify.refine test-pbtyps --- broken with case 4";

(* 

*** pass ["pbla"]

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

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

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

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

val it =

  [Model.Matches

     (["pbla"],

      {Find=[],

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

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

   Model.NoMatch

     (["pbla1","pbla"],

      {Find=[],

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

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

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

   Model.Matches

     (["pbla2","pbla"],

      {Find=[],

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

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

   Model.NoMatch

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

      {Find=[],

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

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

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

   Model.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*)

case Specify.refine fmz4 ["pbla2","pbla", "refine", "test"] of

    [Model.Matches (["pbla2", "pbla", "refine", "test"], _), 

     Model.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), 

     Model.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- Specify.refine test-pbtyps --- broken with case 5";

(* 

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

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

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

val it =

  [Model.Matches

     (["pbla2","pbla"],

      {Find=[],

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

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

   Model.NoMatch

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

      {Find=[],

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

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

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

   Model.Matches

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

      {Find=[],

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

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

  : match list*)

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

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

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

val c = [];

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

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

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

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

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

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)

(*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

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

(*=== specify a not-matching problem ---^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)

val www =

case f of Test_Out.PpcKF (Test_Out.Problem [],

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

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

   Where = [False www(*! ! ! ! ! !*)],

   Relate = [],...}) => www(*! ! !*)

| _ => error "--- Refine_Problem broken 1";

if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"

then () else error "--- Refine_Problem broken 2";

(*ML> f; 

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

        (Problem ["LINEAR","univariate","equation","test"],   <<<<<===== diff.to above WN120313

         {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

*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*Empty_Tac ?!?*);

(*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

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

(*=== refine problem -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;

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

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

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

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

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

val Test_Out.FormKF res = f;

if res = "[x = 2]"

then case nxt of End_Proof' => ()

  | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"

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