(* Title:  "Specify/refine.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

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

"----------- testdata for check_match, Refine.by_o_model --------------------------------------------";

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

"----------- Refine.by_o_model test-pbtyps --requires 'setup'-----------------------------------";

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

"----------- by_o_model' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

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

"----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

"----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

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

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

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

open Test_Tool;

(** -------- testdata for check_match, Refine.by_o_model ------------------------------------------ **)

"----------- testdata for check_match, Refine.by_o_model --------------------------------------------";

"----------- testdata for check_match, Refine.by_o_model --------------------------------------------";

Test_Tool.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 (ParseC.parse_test ctxt "fixedValues [aaa = 0]");

val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "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 (ParseC.parse_test ctxt "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 (ParseC.parse_test ctxt "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 (ParseC.parse_test ctxt "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.

(** -------- check_match test-pbtyps -------requires specific 'setup'----------------------------- **)

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

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

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

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

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

val level_2 = case nth 4 level_1 of

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

val pbla_branch = case level_2 of 

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

(*case 1: no refinement *)

case check_match [] ori1 (hd pbla_branch) of 

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

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

case check_match [] ori2 (hd pbla_branch) of 

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

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

case check_match [] ori3 (hd pbla_branch) of 

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

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

case check_match [] ori4 (hd pbla_branch) of 

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

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

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

case check_match ["pbla"] ori4 ppp of 

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

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

(** -------- Refine.by_o_model test-pbtyps --requires 'setup'-------------------------------- **)

"----------- Refine.by_o_model test-pbtyps --requires 'setup'----------------------------------";

"----------- Refine.by_o_model test-pbtyps --requires 'setup'----------------------------------";

(*case 1: no refinement *)

case Refine.by_o_model @{context} ori1 ["pbla", "refine", "test"] of 

  NONE => () | _ => error "Refine.by_o_model case 1 broken";

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

case Refine.by_o_model @{context} ori2 ["pbla", "refine", "test"] of 

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

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

case Refine.by_o_model @{context} ori3 ["pbla", "refine", "test"] of 

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

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

case Refine.by_o_model @{context} ori4 ["pbla", "refine", "test"] of 

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

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

case Refine.by_o_model @{context} ori4 ["pbla2", "pbla", "refine", "test"] of 

  SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.by_o_model 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 Refine.by_formalise @{context} fmz1 ["pbla", "refine", "test"] of

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

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

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

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

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

(* 

*** pass ["pbla"]

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

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

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

val it =

  [M_Match.Matches

     (["pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

     (["pbla1", "pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

     (["pbla2", "pbla"],

      {Find=[],

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

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

   M_Match.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 Refine.by_formalise @{context} fmz2 ["pbla", "refine", "test"] of

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

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

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

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

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

(* 

*** pass ["pbla"]

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

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

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

val it =

  [M_Match.Matches

     (["pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

     (["pbla1", "pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

     (["pbla2", "pbla"],

      {Find=[],

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

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

   M_Match.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 Refine.by_formalise @{context} fmz3 ["pbla", "refine", "test"] of

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

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

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

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

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

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

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

 | _ => error "--- Refine.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 =

  [M_Match.Matches

     (["pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

     (["pbla1", "pbla"],

      {Find=[],

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

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

   M_Match.Matches

     (["pbla2", "pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

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

      {Find=[],

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

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

   M_Match.NoMatch

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

      {Find=[],

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

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

   M_Match.NoMatch

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

      {Find=[],

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

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

   M_Match.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 Refine.by_formalise @{context} fmz4 ["pbla", "refine", "test"] of

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

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

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

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

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

  | _ => error "--- Refine.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 =

  [M_Match.Matches

     (["pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

     (["pbla1", "pbla"],

      {Find=[],

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

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

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

   M_Match.Matches

     (["pbla2", "pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

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

      {Find=[],

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

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

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

   M_Match.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 Refine.by_formalise @{context} fmz4 ["pbla2", "pbla", "refine", "test"] of

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

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

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

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

(* 

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

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

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

val it =

  [M_Match.Matches

     (["pbla2", "pbla"],

      {Find=[],

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

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

   M_Match.NoMatch

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

      {Find=[],

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

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

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

   M_Match.Matches

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

      {Find=[],

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

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

  : match list*)

(** -------- by_o_model' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ---------------------- **)

"----------- by_o_model' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

"----------- by_o_model' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

(*overwrites NEW funs in Test_Theory ABOVE* )

open Refine

open M_Match

open Pre_Conds

( *overwrites NEW funs in Test_Theory ABOVE*)

(*

  refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;

  this example was the demonstrator;

  respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.

  Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---

*)

(*+*)val o_model = [

(1, [1], "#Given", @{term "equalities"},

  [@{term "[(0::real) = - 1 * c_4 / - 1]"},

   @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +  - 1 * L \<up> 4 * q_0) / - 24]"},

   @{term "[(0::real) = c_2]"},

   @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),

(*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)

(2, [1], "#Given", @{term "solveForVars"},

  [@{term "[c]  ::real list"},

   @{term "[c_2]::real list"},

   @{term "[c_3]::real list"},

   @{term "[c_4]::real list"}] ),

(3, [1], "#Find",  @{term "solution"},  [@{term "ss'''::bool list"}] )]

;

val SOME ["normalise", "4x4", "LINEAR", "system"] =

           by_o_model @{context} o_model ["LINEAR", "system"];

"~~~~~ fun by_o_model , args:"; val (ctxt, oris, pblID) =

  (@{context}, o_model, ["LINEAR", "system"]);

    val opt as SOME ["system", "LINEAR", "4x4", "normalise"]

    = find_node_elem (check_match ctxt ((rev o tl) pblID) oris) pblID (rev pblID);

(*

  find_node_elem works strangely, parameter passing is awkward.

  Present check_match knows structure of Store.T, thus we bypass find_node_elem

*)

(*!*)val pblID = ["LINEAR", "system"];(**)

val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)

           check_match ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));

"~~~~~ fun check_match , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))

  = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));

      val {where_rls, model, where_, ...} = py: Problem.T

      val model = map (Model_Pattern.adapt_to_type ctxt) model

      val where_ = map (ParseC.adapt_term_to_type ctxt) where_;

      (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);

val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))

(*follow the trace created in parallel by writeln in Store.get_node and Refine.check_match*)

(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)

val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] =

          check_match ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));

"~~~~~ fun check_match , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))

  = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));

      val {where_rls, model, where_, ...} = py: Problem.T

      val model = map (Model_Pattern.adapt_to_type ctxt) model

      val where_ = map (ParseC.adapt_term_to_type ctxt) where_

(*+*)val (**)true(** )false( **) = (*if*)

   M_Match.match_oris ctxt where_rls o_model (model, where_);

"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =

  (ctxt, where_rls, o_model, (model, where_));

    val i_model = (flat o (map (chk1_ model_pattern))) o_model;

(*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n  - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"

  = o_model |> O_Model.to_string @{context};

(*+*)if (i_model |> I_Model.to_string @{context}) = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n  0 =\n  (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n   - 1 * L \<up> 4 * q_0) /\n  - 24,\n  0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] , pen2str), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] , pen2str), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor solution ss''' , pen2str)]"

(*+*)then () else raise error "i_model CAHNGED";

(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"

  = model_pattern |> Model_Pattern.to_string @{context}

(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}

   val mvat = I_Model.variables model_pattern (I_Model.OLD_to_TEST i_model)

    val complete = chk1_mis mvat i_model model_pattern;

    val (pb as true, (** )_( **)where_'(**)) =

 Pre_Conds.check ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);

"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =

  (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));

(*+*)val [(true, xxx), (true, yyy)] = where_'

(*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n  0 =\n  (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n   - 1 * L \<up> 4 * q_0) /\n  - 24,\n  0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"

 = where_' |> map #2 |> UnparseC.terms @{context}

      val (env_model, (env_subst, env_eval)) =

           make_environments model_patt i_model;

"~~~~~ fun make_environments , args:"; val (model_patt, i_model) = (model_patt, i_model);

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt

      |> flat

    val env_model = make_env_model equal_descr_pairs

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list =

           make_envs_preconds equal_givens;

"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);

"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);

"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts)))) =

  (id, feedb);

val return_discern_typ as [] =

           discern_typ id (descr, ts);

"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));

(*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n  - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"

 = ts |> UnparseC.terms @{context}

      val ts = if Pre_Conds.is_list_descr descr

        then if TermC.is_list (hd ts)

          then ts |> map TermC.isalist2list |> flat

          else ts

        else ts

(*+*)val "[0 = - 1 * c_4 / - 1, 0 =\n(- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n- 24, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"

 = ts |> UnparseC.terms @{context};

  (*if*)  Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);

(*+*)val false = all_lhs_atoms ts

(*-------------------- contine check -----------------------------------------------------*)

     val pres_subst = map (TermC.subst_atomic_all env_subst) where_;

(*+*)if "[\"\n" ^

  "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n  - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^

  "(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]"

 = (env_model |> Subst.to_string @{context}) then () else error "env_model CAHNGED";

(*+*)val "[]" = env_eval |> Subst.to_string @{context} (*GOON \<rightarrow> []*)

      val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);

      val full_subst = if env_eval = [] then pres_subst_other

        else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)

      val evals = map (eval ctxt where_rls) full_subst

val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)

val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))

(*follow the trace created in parallel by writeln in Store.get_node and Refine.check_match*)

(*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)

val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =

          check_match ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));

(** -------- Refine_Problem (from subp-rooteq.sml) ------------------------------------------- **)

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

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

(*

  By child of 2d962612dd0a this test case revealed an undetected failure

  of Specify.find_next_step -- for_problem: these propose Tactic.Refine_Problem,

  but Step_Specify.by_tactic_input (Refine_Problem ["sqroot-test", "univariate", "equation", "test"]..

  encounters "case Refine.problem ... of NONE".

  The failure might be caused by inappropriate problem-hierarchy.

*)

val c = [];

val fmz = ["equality ((x+1)*(x+2)=x \<up> 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.init_calc @{context} [(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 --- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*)

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

(*WAS at change set b817019bfda7 and before (while Test_Isac.thy was without other errors):

val www =

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

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

   Given = [Correct "equality ((x + 1) * (x + 2) = x \<up> 2 + 8)", Correct "solveFor x"],

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

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

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

if www = "matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 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 \<up> #2 + #8)",

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

          Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)

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

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

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

          With=[]}))) : mout

*)

(*/------------------- step into me Add_Find "solutions L" ---------------------------------\*)

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

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);

(*+*)val Add_Find "solutions L" = tac;

      val (pt, p) =

  	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

  	    case Step.by_tactic tac (pt, p) of

  		    ("ok", (_, _, ptp)) => ptp

  	    | ("unsafe-ok", (_, _, ptp)) => ptp

  	    | ("not-applicable",_) => (pt, p)

  	    | ("end-of-calculation", (_, _, ptp)) => ptp

  	    | ("failure", _) => raise ERROR "sys-raise ERROR"

  	    | _ => raise ERROR "me: uncovered case Step.by_tactic"

  val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) = (*case*)

      Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));

  (*if*) Pos.on_calc_end ip (*else*);

      val (_, probl_id, _) = Calc.references (pt, p);

      val _ = (*case*) tacis (*of*);

        (*if*) probl_id = Problem.id_empty (*else*);

           switch_specify_solve p_ (pt, ip) (*return from Step.do_next*);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

  val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =

           specify_do_next (pt, input_pos);

"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

    val (_, (p_', tac)) =

  Specify.find_next_step ptp;

(*/------------------- step into find_next_step --------------------------------------------\*)

(*+ store for continuation after find_next_step*)val (p_'_'''''_', tac'''''_') = (p_', tac);

"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

      (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);

        (*if*) p_ = Pos.Pbl (*then*);

  val ("dummy", (Pbl, Add_Find "solutions L")) =

           for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met);

"~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

  (oris, (o_refs, refs), (pbl, met));

    val cpI = if pI = Problem.id_empty then pI' else pI;

    val cmI = if mI = MethodC.id_empty then mI' else mI;

    val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

    val {model = mpc, ...} = MethodC.from_store ctxt cmI

    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);

    (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);

      (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);

      val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*);

      val SOME ("#Find", "solutions L") = (*case*)

        item_to_add ctxt oris (I_Model.OLD_to_TEST pbl);

      (*if*) not preok (*then*);

(*+*)Pre_Conds.to_string @{context} xxxxx = "[\n" ^

  "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^

    "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^

    "matches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^

    "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8))]";

  (*TermC.matches  \<up> \<up> \<up> \<up>  \<up> ^ NONE, ok: why then NONE = Refine.problem below?*)

(*-------------------- stop step into find_next_step ----------------------------------------*)

(*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_')

(*\------------------- step into find_next_step --------------------------------------------/*)

(*-------------------- contiue step into specify_do_next ------------------------------------*)

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

val Add_Find "solutions L" =

    (*case*) tac (*of*);

  val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =

Step_Specify.by_tactic_input tac (pt, (p, p_'));

"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Find  ct), (ptp as (pt, pos as (p,_)))) =

  (tac, (pt, (p, p_')));

   Specify.by_Add_ "#Find" ct ptp;

"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =

  ("#Find", ct, ptp);

(*-------------------- stop step into -------------------------------------------------------*)

val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt'''''); val Add_Find "solutions L" = nxt;

(*\------------------- step into me Add_Find "solutions L" ---------------------------------/*)

(*

  WN230814

  repaired 'step into me Add_Find "solutions L"' above (ERROR was Tactic.Refine);

  But with the repair the subsequent steps repeatedly led to Add_Find "solutions L" --

  -- which was NOT repaird, too.

  So we kept the old test code below, because it leads to the correct result "[x = 2]".

---------------------- old test code from before above repair -------------------------------

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

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

(*=== refine problem ----- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)

(*[], 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" 

*)

(** -------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type ------------ **)

"----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

"----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

(*for timing copy to Test_Some.thy*)

States.reset ();

val model = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)", "solveFor x", "solutions L"];

val refs = ("PolyEq"(**), ["univariate", "equation"], ["no_met"]);

CalcTree @{context} [(model, refs)];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt, _), _) = States.get_calc 1;

val p = States.get_pos 1 1;

val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);

if UnparseC.term @{context} f = "[x = 6 / 5]" then () else error "equation for timing CHANGED"

(** -------- refine ad-hoc equation for timing: with/out adapt_to_type ----------------------- **)

"----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

"----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

(*for timing copy to Test_Some.thy*)

val model = ["equality ((x \<up> 2 - 6*x+9) - (x \<up> 2 - 3*x) = x)", "solveFor x", "solutions L"];

val (_, pbl_id, _) = ("PolyEq", ["univariate", "equation"], ["no_met"]);

Refine.by_formalise @{context} model pbl_id;

(*

*** pass ["equation", "univariate"] 

*** pass ["equation", "univariate", "rootX"] 

*** pass ["equation", "univariate", "LINEAR"] 

*** pass ["equation", "univariate", "rational"] 

*** pass ["equation", "univariate", "polynomial"] 

*** pass ["equation", "univariate", "polynomial", "degree_0"] 

*** pass ["equation", "univariate", "polynomial", "degree_1"] 

*** pass ["equation", "univariate", "polynomial", "degree_2"] 

*** pass ["equation", "univariate", "polynomial", "degree_3"] 

*** pass ["equation", "univariate", "polynomial", "degree_4"] 

*** pass ["equation", "univariate", "polynomial", "normalise"] 

*)