(* tests on calchead.sml

   author: Walther Neuper

   051013,

   (c) due to copyright terms

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

use"calchead.sml";

*)

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

"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 (!)-----------";

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

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

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

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

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

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

 states:=[];

 CalcTree

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

   ("Test.thy", 

    ["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;

print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);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

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

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

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

raise 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]",

     "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.thy",["maximum_of","function"],

   ["DiffApp","max_by_calculus"]);

val c = []:cid;

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

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

*)

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

val nxt = tac2tac_ pt p nxt; 

val(p,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

(**)

(*---6.5.03

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

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

(*uncaught exception TYPE 6.5.03*)

if ppc<>(Problem [],  

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

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

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

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

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

6.5.03---*)

(*-----appl_add should not create Error', but accept as Sup,Syn

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

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

(**)

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

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

(**)---*)

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

val nxt = tac2tac_ pt p m; 

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

(**)

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

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

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

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

then raise 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 raise error "diffappl.sml: Specify_Problem different behaviour" 

else ();*)

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

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

(**)

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

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

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

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

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

then raise 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_",

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

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

then raise error "diffappl.sml: Specify_Method different behaviour" 

else ();*)

"--------- 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.thy",["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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;

val nxt = tac2tac_ pt p nxt; 

val(p,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

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

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = tac2tac_ pt p nxt; 

val(p,_,Form'(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 raise error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)

val nxt = tac2tac_ pt p nxt; 

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

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

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

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

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = tac2tac_ pt p nxt; 

val(p,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

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

val nxt = tac2tac_ pt p nxt; 

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

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

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

then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();

"--------- 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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] 

  EmptyPtree;

val nxt = tac2tac_ pt p nxt; 

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

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

val nxt = Specify_Theory "DiffApp.thy";

val nxt = tac2tac_ pt p nxt; 

val(p,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

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

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

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

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

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

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

*)

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

val nxt = tac2tac_ pt p nxt; 

val(p,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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,_,Form'(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.thy","max_by_calculus"))

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

else ();

*)

(* 2.4.00 nach Transfer specify -> hard_gen

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

val(p,_,Form'(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 ("Pair",_) $

		 Free (dI',_) $ 

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

case match_ags Isac.thy 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___", _)])] 

    =>()

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

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

	  (Const ("Pair",_) $

		 Free (dI',_) $ 

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

case match_ags Isac.thy 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")]*)

    =>()

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

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

	 (Const ("Pair",_) $

		Free (dI',_) $ 

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

case ((match_ags Isac.thy pats ags)

      handle TYPE _ => []) of 

    [] => match_ags_msg pI stac ags

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

(*

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

*)

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

	 (Const ("Pair",_) $

		Free (dI',_) $ 

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

case match_ags Isac.thy pats ags of

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

      Const ("Descript.equality", _),

      [Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]),

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

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

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

    => ()

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