(* Title: tests on calchead.sml

   Author: Walther Neuper 051013,

   (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

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

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

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

"--------- get_interval after replace} other 2 ----------";

"--------- maximum example with 'specify' ---------------";

"--------- maximum example with 'specify', fmz <> [] ----";

"--------- maximum example with 'specify', fmz = [] -----";

"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";

"--------- regression test fun is_copy_named ------------";

"--------- regr.test fun cpy_nam ------------------------";

"--------- check specify phase --------------------------";

"--------- check: fmz matches pbt -----------------------";

"--------- fun typeless ---------------------------------";

"--------- fun variants_in ------------------------------";

"--------- fun has_list_type ----------------------------";

"--------- fun tag_form ---------------------------------";

"--------- fun foldr1, foldl1 ---------------------------";

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

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

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

"--------- get_interval after replace} other 2 ----------";

"--------- get_interval after replace} other 2 ----------";

"--------- get_interval after replace} other 2 ----------";

reset_states ();

 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 

   ("Test", ["sqroot-test","univariate","equation","test"],

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

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

 replaceFormula 1 "x = 1"; 

 (*... returns calcChangedEvent with ...*)

 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));

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

default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;

if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 

    [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 

     ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

      ([3, 2], Res)] then () else

error "calchead.sml: diff.behav. get_interval after replace} other 2 a";

default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;

if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 

    [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else

error "modspec.sml: diff.behav. get_interval after replace} other 2 b";

"--------- maximum example with 'specify' ------------------------";

"--------- maximum example with 'specify' ------------------------";

"--------- maximum example with 'specify' ------------------------";

(*"              Specify_Problem (match_itms_oris)       ";*)

val fmz =

    ["fixedValues [r=Arbfix]","maximum A",

     "valuesFor [a,b::real]",

     "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",

     "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]",

     "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos alpha]",

     "boundVariable a","boundVariable b","boundVariable alpha",

     "interval {x::real. 0 <= x & x <= 2*r}",

     "interval {x::real. 0 <= x & x <= 2*r}",

     "interval {x::real. 0 <= x & x <= pi}",

     "errorBound (eps=(0::real))"];

val (dI',pI',mI') =

  ("DiffApp",["maximum_of","function"],

   ["DiffApp","max_by_calculus"]);

val c = []:cid;

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

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(**)

val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

if ppc<>(Problem [],  

         {Find=[Incompl "maximum",Incompl "valuesFor [a]"],

	  Given=[Correct "fixedValues [r = Arbfix]"],

	  Relate=[Incompl "relations"], Where=[],With=[]})

then error "test-maximum.sml: model stepwise - different behaviour" 

else ();

val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)"); 

(* WN1130630 THE maximum example WORKS IN isabisac09-2; 

  MOST LIKELY IT IS BROKEN BY INTRODUCING  ctxt. 

  Some tests have been broken much earlier, 

  see test/../calchead.sml "inhibit exn 010830". *)

(*========== inhibit exn WN1130630 maximum example broken =========================

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

============ inhibit exn WN1130630 maximum example broken =======================*)

val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); 

(*========== inhibit exn WN1130630 maximum example broken =========================

(* ERROR: Exception Bind raised *)

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

============ inhibit exn WN1130630 maximum example broken =======================*)

val m = Specify_Problem ["maximum_of","function"];

val nxt = tac2tac_ pt p m; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*========== inhibit exn WN1130630 maximum example broken =========================

if ppc<>(Problem ["maximum_of","function"],  

         {Find=[Incompl "maximum",Incompl "valuesFor"],

	  Given=[Correct "fixedValues [r = Arbfix]"],

	  Relate=[Incompl "relations []"], Where=[],With=[]})

then error "diffappl.sml: Specify_Problem different behaviour" 

else ();

(* WN.3.9.03 (#391) Model_Specify did init_pbl newly 

if ppc<>(Problem ["maximum_of","function"],

   {Find=[Missing "maximum m_",Missing "valuesFor vs_"],

    Given=[Correct "fixedValues [r = Arbfix]"],

    Relate=[Missing "relations rs_"],Where=[],With=[]})

then error "diffappl.sml: Specify_Problem different behaviour" 

else ();*)

============ inhibit exn WN1130630 maximum example broken =======================*)

val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*========== inhibit exn WN1130630 maximum example broken =========================

if ppc<>(Method ["DiffApp","max_by_calculus"],

	 {Find=[Incompl "maximum",Incompl "valuesFor"],

	  Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",

		 Missing "interval itv_",Missing "errorBound err_"],

	  Relate=[Incompl "relations []"],Where=[],With=[]})

then error "diffappl.sml: Specify_Method different behaviour" 

else ();

(* WN.3.9.03 (#391) Model_Specify did init_pbl newly 

if ppc<>(Method ["DiffApp","max_by_calculus"],

   {Find=[Missing "maximum m_",Missing "valuesFor vs_"],

    Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v",

           Missing "interval itv_",Missing "errorBound err_"],

    Relate=[Missing "relations rs_"],Where=[],With=[]})

then error "diffappl.sml: Specify_Method different behaviour" 

else ();*)

============ inhibit exn WN1130630 maximum example broken =======================*)

"--------- maximum example with 'specify', fmz <> [] -------------";

"--------- maximum example with 'specify', fmz <> [] -------------";

"--------- maximum example with 'specify', fmz <> [] -------------";

val fmz =

    ["fixedValues [r=Arbfix]","maximum A",

     "valuesFor [a,b]",

     "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

     "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

     "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

     "boundVariable a","boundVariable b","boundVariable alpha",

     "interval {x::real. 0 <= x & x <= 2*r}",

     "interval {x::real. 0 <= x & x <= 2*r}",

     "interval {x::real. 0 <= x & x <= pi}",

     "errorBound (eps=(0::real))"];

val (dI',pI',mI') =

  ("DiffApp",["maximum_of","function"],

   ["DiffApp","max_by_calculus"]);

val c = []:cid;

(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)

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

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt;

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "maximum (A::bool)" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Relation "relations [A = a * b]" *)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)

(*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!

  nxt_specif <> specify ?!

if nxt<>(Add_Relation 

 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")

then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

------------------------------ FIXXXXME.meNEW !!! ---*)

(*val nxt = Specify_Theory "DiffApp" : tac*)

val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Problem ["maximum_of","function"]*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "boundVariable a" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "errorBound (eps = #0)" : tac*)

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)

case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()

| _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";

"--------- maximum example with 'specify', fmz = [] --------------";

"--------- maximum example with 'specify', fmz = [] --------------";

"--------- maximum example with 'specify', fmz = [] --------------";

val fmz = [];

val (dI',pI',mI') = empty_spec;

val c = []:cid;

val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)

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

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] 

  EmptyPtree;

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Theory "e_domID" : tac*)

val nxt = Specify_Theory "DiffApp";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Problem ["e_pblID"] : tac*)

val nxt = Specify_Problem ["maximum_of","function"];

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "fixedValues" : tac*)

val nxt = Add_Given "fixedValues [r=Arbfix]";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "maximum" : tac*)

val nxt = Add_Find "maximum A";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Find "valuesFor" : tac*)

val nxt = Add_Find "valuesFor [a]";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Relation "relations" --- 

  --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)

(*========== inhibit exn 010830 =======================================================*)

(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....

if nxt<>(Add_Relation "relations []")

then error "test specify, fmz <> []: nxt <> Add_Relation.." 

else (); (*different with show_types !!!*)

*)

(*========== inhibit exn 010830 =======================================================*)

val nxt = Add_Relation "relations [(A=a+b)]";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Specify_Method ("e_domID","e_metID") : tac*)

val nxt = Specify_Method ["DiffApp","max_by_calculus"];

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "boundVariable" : tac*)

val nxt = Add_Given "boundVariable alpha";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "interval" : tac*)

val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Add_Given "errorBound" : tac*)

val nxt = Add_Given "errorBound (eps=999)";

val nxt = tac2tac_ pt p nxt; 

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;

(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)

(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....

if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))

then error "test specify, fmz <> []: nxt <> Add_Relation.." 

else ();

*)

(* 2.4.00 nach Transfer specify -> hard_gen

val nxt = Apply_Method ("DiffApp","max_by_calculus");

val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *)

(*val nxt = Empty_Tac : tac*)

"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";

"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";

"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";

val Const ("Script.SubProblem",_) $

	  (Const ("Product_Type.Pair",_) $

		 Free (dI',_) $ 

		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (EqSystem', [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^

        "      REAL_LIST [c, c_2]]");

val ags = isalist2list ags';

val pI = ["LINEAR","system"];

val pats = (#ppc o get_pbt) pI;

"-a1-----------------------------------------------------";

(*match_ags = fn : theory -> pat list -> term list -> ori list*)

val xxx = match_ags @{theory "EqSystem"} pats ags;

"-a2-----------------------------------------------------";

case match_ags @{theory  "Isac"} pats ags of 

    [(1, [1], "#Given", Const ("Descript.equalities", _), _),

     (2, [1], "#Given", Const ("EqSystem.solveForVars", _),

      [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] 

    =>()

  | _ => error "calchead.sml match_ags 2 args Nok ----------------";

"-b------------------------------------------------------";

val Const ("Script.SubProblem",_) $

	  (Const ("Product_Type.Pair",_) $

		 Free (dI',_) $ 

		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (EqSystem', [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^

        "      REAL_LIST [c, c_2], BOOL_LIST ss''']");

val ags = isalist2list ags';

val pI = ["LINEAR","system"];

val pats = (#ppc o get_pbt) pI;

"-b1-----------------------------------------------------";

val xxx = match_ags @{theory  "Isac"} pats ags;

"-b2-----------------------------------------------------";

case match_ags @{theory "EqSystem"} pats ags of 

    [(1, [1], "#Given", Const ("Descript.equalities", _), _),

     (2, [1], "#Given", Const ("EqSystem.solveForVars", _),

         [_ $ Free ("c", _) $ _,

          _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]

    (*         type of Find:            [Free ("ss'''", "bool List.list")]*)

    =>()

  | _ => error "calchead.sml match_ags copy-named dropped --------";

"-c---ERROR case: stac is missing #Given equalities e_s--";

val stac as Const ("Script.SubProblem",_) $

	 (Const ("Product_Type.Pair",_) $

		Free (dI',_) $ 

		(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^

        "     [REAL_LIST [c, c_2]]");

val ags = isalist2list ags'; 

val pI = ["LINEAR","system"];

val pats = (#ppc o get_pbt) pI;

(*============ inhibit exn AK110726 ==============================================

val xxx - match_ags (theory "EqSystem") pats ags;

============ inhibit exn AK110726 ==============================================*)

"-c1-----------------------------------------------------";

"--------------------------step through code match_ags---";

val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);

fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

	val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)

	val cy = filter is_copy_named pbt;       (*=solution*)

(*============ inhibit exn AK110726 ==============================================

	val oris' - matc thy pbt' ags [];

============ inhibit exn AK110726 ==============================================*)

"-------------------------------step through code matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);

(is_copy_named_idstr o free2str) t;

"---if False:...";

(*============ inhibit exn AK110726 ==============================================

val opt - mtc thy p a;

============ inhibit exn AK110726 ==============================================*)

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);

Thm.global_cterm_of;

val ttt = (dsc $ var);

(*============ inhibit exn AK110726 ==============================================

Thm.global_cterm_of thy (dsc $ var);

============ inhibit exn AK110726 ==============================================*)

"-------------------------------------step through end---";

"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";

val Const ("Script.SubProblem",_) $

	  (Const ("Product_Type.Pair",_) $

		 Free (dI',_) $ 

		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (EqSystem', [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^

        "      REAL_LIST [c, c_2]]");

val ags = isalist2list ags';

val pI = ["LINEAR","system"];

val pats = (#ppc o get_pbt) pI;

"-a1-----------------------------------------------------";

(*match_ags = fn : theory -> pat list -> term list -> ori list*)

val xxx = match_ags @{theory "EqSystem"} pats ags;

"-a2-----------------------------------------------------";

case match_ags @{theory  "Isac"} pats ags of 

    [(1, [1], "#Given", Const ("Descript.equalities", _), _),

     (2, [1], "#Given", Const ("EqSystem.solveForVars", _),

      [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] 

    =>()

  | _ => error "calchead.sml match_ags 2 args Nok ----------------";

"-b------------------------------------------------------";

val Const ("Script.SubProblem",_) $

	  (Const ("Product_Type.Pair",_) $

		 Free (dI',_) $ 

		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (EqSystem', [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^

        "      REAL_LIST [c, c_2], BOOL_LIST ss''']");

val ags = isalist2list ags';

val pI = ["LINEAR","system"];

val pats = (#ppc o get_pbt) pI;

"-b1-----------------------------------------------------";

val xxx = match_ags @{theory  "Isac"} pats ags;

"-b2-----------------------------------------------------";

case match_ags @{theory "EqSystem"} pats ags of 

    [(1, [1], "#Given", Const ("Descript.equalities", _), _),

     (2, [1], "#Given", Const ("EqSystem.solveForVars", _),

         [_ $ Free ("c", _) $ _,

          _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])]

    (*         type of Find:            [Free ("ss'''", "bool List.list")]*)

    =>()

  | _ => error "calchead.sml match_ags copy-named dropped --------";

"-c---ERROR case: stac is missing #Given equalities e_s--";

val stac as Const ("Script.SubProblem",_) $

	 (Const ("Product_Type.Pair",_) $

		Free (dI',_) $ 

		(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^

        "     [REAL_LIST [c, c_2]]");

val ags = isalist2list ags'; 

val pI = ["LINEAR","system"];

val pats = (#ppc o get_pbt) pI;

(*============ inhibit exn AK110726 ==============================================

val xxx - match_ags (theory "EqSystem") pats ags;

-------------------------------------------------------------------*)

"-c1-----------------------------------------------------";

"--------------------------step through code match_ags---";

val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags);

fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

	val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)

	val cy = filter is_copy_named pbt;       (*=solution*)

(*============ inhibit exn AK110726 ==============================================

	val oris' - matc thy pbt' ags [];

-------------------------------------------------------------------*)

"-------------------------------step through code matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);

(is_copy_named_idstr o free2str) t;

"---if False:...";

(*============ inhibit exn AK110726 ==============================================

val opt - mtc thy p a;

-------------------------------------------------------------------*)

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);

Thm.global_cterm_of;

val ttt = (dsc $ var);

(*============ inhibit exn AK110726 ==============================================

Thm.global_cterm_of thy (dsc $ var);

-------------------------------------------------------------------*)

"-------------------------------------step through end---";

case ((match_ags @{theory "EqSystem"} pats ags)

      handle ERROR _ => []) of (*why not TYPE ?WN100920*)

    [] => match_ags_msg pI stac ags

  | _ => error "calchead.sml match_ags 1st arg missing --------";

"-d------------------------------------------------------";

val stac as Const ("Script.SubProblem",_) $

	 (Const ("Product_Type.Pair",_) $

		Free (dI',_) $ 

		(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (Test',[univariate,equation,test]," ^

        "             [no_met]) [BOOL (x+1=2), REAL x]");

val AGS = isalist2list ags';

val pI = ["univariate","equation","test"];

case ((match_ags @{theory "EqSystem"} pats ags)

      handle ERROR _ => []) of (*why not TYPE ?WN100920*)

    [] => match_ags_msg pI stac ags

  | _ => error "calchead.sml match_ags 1st arg missing --------";

"-d------------------------------------------------------";

val stac as Const ("Script.SubProblem",_) $

	 (Const ("Product_Type.Pair",_) $

		Free (dI',_) $ 

		(Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =

    (*...copied from stac2tac_*)

    str2term (

	"SubProblem (Test',[univariate,equation,test]," ^

        "             [no_met]) [BOOL (x+1=2), REAL x]");

val AGS = isalist2list ags';

val pI = ["univariate","equation","test"];

val PATS = (#ppc o get_pbt) pI;

"-d1-----------------------------------------------------";

"--------------------------step through code match_ags---";

val (thy, pbt:pat list, ags) = (@{theory "Test"}, PATS, AGS);

fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

	val pbt' = filter_out is_copy_named pbt; 

	val cy = filter is_copy_named pbt;       

	val oris' = matc thy pbt' ags [];

"-------------------------------step through code matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);

(is_copy_named_idstr o free2str) t;

"---if False:...";

val opt = mtc thy p a;

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);

val ttt = (dsc $ var);

Thm.global_cterm_of thy (dsc $ var);

val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);

"-d2-----------------------------------------------------";

pbt = [];  (*false*)

"-------------------------------step through code matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);

(is_copy_named_idstr o free2str) t;

"---if False:...";

val opt = mtc thy p a;

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);

val ttt = (dsc $ var);

Thm.global_cterm_of thy (dsc $ var);

val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);

"-d3-----------------------------------------------------";

pbt = [];  (*true, base case*)

"-----------------continue step through code match_ags---";

	val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)

"--------------------------------step through cpy_nam----";

val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy);

(*t = "v_v'i'" : term             OLD: t = "v_i_"*)

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

fun is_copy_named_generating_idstr str =

    if is_copy_named_idstr str

    then case (rev o Symbol.explode) str of

      (*"_"::"_"::"_"::_ => false*)

	"'"::"'"::"'"::_ => false

      | _ => true

    else false;

fun is_copy_named_generating (_, (_, t)) = 

    (is_copy_named_generating_idstr o free2str) t;

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

is_copy_named_generating p (*true*);

           fun sel (_,_,d,ts) = comp_ts (d, ts);

	   val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;

               (*"v_v"             OLD: "v_"*)

	   val ext = (last_elem o drop_last o Symbol.explode o free2str) t;

               (*"i"               OLD: "i"*)

	   val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);

               (*["e_e", "v_v"]    OLD: ["e_", "v_"]*)

	   val vals = map sel oris;

               (*[x+1=2, x]        OLD: [x+1=2, x] : term list*)

vars' ~~ vals;

(*[("e_e", [x+1=2), ("v_v", x)]    OLD: [("e_", [x+1=2), ("v_", x)]*)

(assoc (vars'~~vals, cy'));

(*SOME (Free ("x", "Real.real")) : term option*)

	   val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;

               (*x_i*)

"-----------------continue step through code match_ags---";

	val cy' = map (cpy_nam pbt' oris') cy;

               (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)

"-------------------------------------step through end---";

case match_ags thy PATS AGS of

[(1, [1], "#Given", Const ("Descript.equality", _),

  [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $

		Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),

 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),

 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]

    => ()

  | _ => error "calchead.sml match_ags [univariate,equation,test]--";

"--------- regression test fun is_copy_named ------------";

"--------- regression test fun is_copy_named ------------";

"--------- regression test fun is_copy_named ------------";

val trm = (1, (2, @{term "v'i'"}));

if is_copy_named trm then () else error "regr. is_copy_named 1";

val trm = (1, (2, @{term "e_e"}));

if is_copy_named trm then error "regr. is_copy_named 2" else ();

val trm = (1, (2, @{term "L'''"}));

if is_copy_named trm then () else error "regr. is_copy_named 3";

(* out-comment 'structure CalcHead'...

val trm = (1, (2, @{term "v'i'"}));

if is_copy_named_generating trm then () else error "regr. is_copy_named";

val trm = (1, (2, @{term "L'''"}));

if is_copy_named_generating trm then error "regr. is_copy_named" else ();

*)

"--------- regr.test fun cpy_nam ------------------------";

"--------- regr.test fun cpy_nam ------------------------";

"--------- regr.test fun cpy_nam ------------------------";

(*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*)

(*the model-pattern, is_copy_named are filter_out*)

pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),

       ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];

(*the model specific for an example*)

oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]),

	([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];

cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];

(*...all must be true*)

case cpy_nam pbt oris (hd cy) of 

    ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => ()

  | _ => error "calchead.sml regr.test cpy_nam-1-";

(*new data: cpy_nam without changing the name*)

@{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};

@{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};

@{term "solution"}; type_of @{term "ss''' :: bool list"};

(*the model-pattern for ["LINEAR", "system"], is_copy_named are filter_out*)

val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),

       ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];

(*the model specific for an example*)

val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]),

    ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];

val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))

        (*could be more than 1*)];

case cpy_nam pbt oris (hd cy) of

    ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()

  | _ => error "calchead.sml regr.test cpy_nam-2-";

"--------- check specify phase --------------------------";

"--------- check specify phase --------------------------";

"--------- check specify phase --------------------------";

(*val fmz = ["functionTerm (x^^^2 + 1)",*)

val fmz = ["functionTerm (x + 1)", 

	   "integrateBy x","antiDerivative FF"];

val (dI',pI',mI') =

  ("Integrate",["integrate","function"],

   ["diff","integration"]);

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

"--- step 1 --";

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

(*> val it = "--- step 1 --" : string

val f =

  Form'

   (PpcKF

    (0, EdUndef, 0, Nundef,

     (Problem [],

	      {Find = [], With = [], Given = [], Where = [], Relate = []})))

: mout

val nxt = ("Model_Problem", Model_Problem) : string * tac

val p = ([], Pbl) : pos'

val pt =

   Nd (PblObj

       {env = None, fmz =

       (["functionTerm (x^^^2 + 1)", "integrateBy x",

	 "antiDerivative FF"],

	("Integrate", ["integrate", "function"],

	 ["diff", "integration"])),

       loc =

       (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),

	None),

       cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),

       probl = [], branch = TransitiveB,

       origin =

       ([(1, [1], "#Given",

	     Const ("Descript.functionTerm", "Real.real => Tools.una"),

	     [Const ("op +", 

		     "["Real.real, "Real.real] => "Real.real") $

		     (Const ("Atools.pow",

			     "["Real.real, "Real.real] => "Real.real") $

		     Free ("x", "Real.real") $ Free ("2", "Real.real")) $

		     Free ("1", "Real.real")]),

	 (2, [1], "#Given",

	     Const ("Integrate.integrateBy", "Real.real => Tools.una"),

	     [Free ("x", "Real.real")]),

	 (3, [1], "#Find",

	     Const ("Integrate.antiDerivative", "Real.real => Tools.una"),

	     [Free ("FF", "Real.real")])],

	("Integrate", ["integrate", "function"], ["diff", "integration"]),

	Const ("Integrate.Integrate",

	       "("Real.real, "Real.real) * => "Real.real") $

	       (Const ("Product_Type.Pair",

		       "["Real.real, "Real.real]

                                  => ("Real.real, "Real.real) *") $

		 (Const ("op +",

			 "["Real.real, "Real.real] => "Real.real") $

		     (Const ("Atools.pow",

			     "["Real.real, "Real.real] => "Real.real") $

		      Free ("x", "Real.real") $ Free ("2", "Real.real")) $

		     Free ("1", "Real.real")) $

		    Free ("x", "Real.real"))),

       ostate = Incomplete, result = (Const ("empty", "'a"), [])},

       []) : ctree*)

"----- WN101007 worked until here (checked same as isac2002) ---";

case nxt of ("Model_Problem", Model_Problem) => ()

| _ => error "clchead.sml: check specify phase step 1";

"--- step 2 --";

val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)

(*val it = "--- step 2 --" : string

val p = ([], Pbl) : pos'

val f =

   Form'

      (PpcKF

         (0, EdUndef, 0, Nundef,

            (Problem [],

               {Find = [Incompl "Integrate.antiDerivative"],

                  With = [],

                  Given = [Incompl "functionTerm", Incompl "integrateBy"],

                  Where = [],

                  Relate = []}))) : mout

val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_

val pt =

   Nd (PblObj

       {env = None, fmz =

       (["functionTerm (x^^^2 + 1)", "integrateBy x",

	 "antiDerivative FF"],

	("Integrate", ["integrate", "function"],

	 ["diff", "integration"])),

       loc =

       (Some

	(ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),

	None),

       cell = None, meth = [], spec = 

       ("e_domID", ["e_pblID"], ["e_metID"]), probl =

       [(0, [], false, "#Given",

	    Inc ((Const ("Descript.functionTerm",

			 "Real.real => Tools.una"),[]),

		 (Const ("empty", "'a"), []))),

	(0, [], false, "#Given",

	    Inc ((Const ("Integrate.integrateBy",

			 "Real.real => Tools.una"),[]),

		 (Const ("empty", "'a"), []))),

	(0, [], false, "#Find",

	    Inc ((Const ("Integrate.antiDerivative",

			 "Real.real => Tools.una"),[]),

		 (Const ("empty", "'a"), [])))],

       branch = TransitiveB, origin =

       ([(1, [1], "#Given",

	     Const ("Descript.functionTerm", "Real.real => Tools.una"),

	     [Const ("op +",

		     "["Real.real, "Real.real] => "Real.real") $

	       (Const ("Atools.pow",

		       "["Real.real, "Real.real] => "Real.real") $

		      Free ("x", "Real.real") $ Free ("2", "Real.real")) $

		     Free ("1", "Real.real")]),

	 (2, [1], "#Given",

	     Const ("Integrate.integrateBy", "Real.real => Tools.una"),

	     [Free ("x", "Real.real")]),

	 (3, [1], "#Find",

	     Const ("Integrate.antiDerivative", "Real.real => Tools.una"),

	     [Free ("FF", "Real.real")])],

	("Integrate", ["integrate", "function"], ["diff", "integration"]),

	Const ("Integrate.Integrate",

	       "("Real.real, "Real.real) * => "Real.real") $

	   (Const ("Product_Type.Pair",

		   "["Real.real, "Real.real]

                         => ("Real.real, "Real.real) *") $

	     (Const ("op +",

		     "["Real.real, "Real.real] => "Real.real") $

		     (Const ("Atools.pow",

			     "["Real.real, "Real.real] => "Real.real") $

		     Free ("x", "Real.real") $ Free ("2", "Real.real")) $

		   Free ("1", "Real.real")) $

                        Free ("x", "Real.real"))),

       ostate = Incomplete, result = (Const ("empty", "'a"), [])},

       []) : ctree*)

"----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED";

case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => ()

| _ => error "clchead.sml: check specify phase step 2";

"--- step 3 --";

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

"----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED";

case nxt of ("Add_Given", Add_Given "integrateBy x") => ()

| _ => error "clchead.sml: check specify phase step 2";

"--------- check: fmz matches pbt -----------------------";

"--------- check: fmz matches pbt -----------------------";

"--------- check: fmz matches pbt -----------------------";

"101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";

"the following fmz caused the above error";

val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];

val pI = ["plus_minus","polynom","vereinfachen"];

"----- this fmz is transformed to this internal format (TERM --> Pure.term):";

val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),

      (*#############################^^^^^^^^^ defined by Isabelle*)

      (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),

                            [Free ("N", _ (*"Real.real"*))])],

     _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);

"#undef means: the element with description TERM in fmz did not match ";

"with any element of pbl (fetched by pI), because there we have Simplify.Term";

"defined in Simplify.thy";

"So we try out how to create Simplify.Term:";

"----- trial 1";

val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt";

"           ^^^^^^^^^ see above";

atomwy t;

"----- trial 2";

val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt";

"   ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)";

atomwy t;

"----- trial 3";

val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt";

"           ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined ";

"                          and unsed in pbl [plus_minus,polynom,vereinfachen]";

atomwy t;

"----- so this is the correct fmz:";

val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];

val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]),

      (*########################^^^^^^^^^ defined in Simplify.thy*)

      (2, [1], "#Find", Const ("Simplify.normalform", _ ),

                            [Free ("N", _ )])],

     _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);

"----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";

val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),

     ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;

"--------- fun typeless ---------------------------------";

"--------- fun typeless ---------------------------------";

"--------- fun typeless ---------------------------------";

(*

> val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";

> val (_,t1) = split_dsc_t hs (Thm.term_of ct);

> val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";

> val (_,t2) = split_dsc_t hs (Thm.term_of ct);

> typeless t1 = typeless t2;

val it = true : bool

*)

"--------- fun variants_in ------------------------------";

"--------- fun variants_in ------------------------------";

"--------- fun variants_in ------------------------------";

(*

> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;

val it = ([3],[4,5,5,5,5,5]) : int list * int list

> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];

val it = [1,3,1,5] : int list

*)

"--------- fun tag_form ---------------------------------";

"--------- fun tag_form ---------------------------------";

"--------- fun tag_form ---------------------------------";

(* val formal = (the o (parse thy)) "[R::real]";

> val given = (the o (parse thy)) "fixed_values (cs::real list)";

> tag_form thy (formal, given);

val it = "fixed_values [R]" : cterm

*)

"--------- fun foldr1, foldl1 ---------------------------";

"--------- fun foldr1, foldl1 ---------------------------";

"--------- fun foldr1, foldl1 ---------------------------";

(*

> val (SOME ct) = parse thy "[a=b,c=d,e=f]";

> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));

> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));

> Thm.global_cterm_of thy conj;

val it = "(a = b & c = d) & e = f" : cterm

*)

(*

> val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";

> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));

> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));

> Thm.global_cterm_of thy conj;

val it = "a = b & c = d & e = f & g = h" : cterm

*)