(* Title:  test/../script.sml

   Author: Walther Neuper 050908

   (c) copyright due to lincense terms.

*)

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

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

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

"----------- WN0509 why does next_tac doesnt find Substitute -----";

"----------- WN0509 Substitute 2nd part --------------------------";

"----------- fun sel_appl_atomic_tacs ----------------------------";

"----------- fun init_form, fun get_stac -------------------------";

"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";

"----------- x+1=2 set ctxt in Subproblem ------------------------";

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

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

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

"----------- WN0509 why does next_tac doesnt find Substitute -----";

"----------- WN0509 why does next_tac doesnt find Substitute -----";

"----------- WN0509 why does next_tac doesnt find Substitute -----";

(*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)

val str = (*#1#*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  \

\  (let q___ = Take (M_b v_v = q__);                                          \

\       (M1__::bool) = ((Substitute [v_ = 0])) q___           \

\ in True)";

(*========== inhibit exn 110721 ================================================

val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;

(========= inhibit exn 110721 ================================================*)

val str = (*#2#*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  \

\  (let q___ = Take (q_ v_v = q__);                                          \

\       (M1__::bool) = ((Substitute [v_ = 0]) @@ \

\                       (Substitute [M_b 0 = 0]))  q___          \

\ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)

val str = (*#3#*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  \

\  (let q___ = Take (q_ v_v = q__);                                          \

\      (M1__::bool) = Substitute [v_ = 0]      q___ ;        \

\       M1__ =        Substitute [M_b 0 = 0]  M1__           \

\ in True)"

;

val str = (*#4#*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  \

\  (let q___ = Take (q_ v_v = q__);                                          \

\      (M1__::bool) = Substitute [v_ = 0]      q___ ;        \

\       M1__ =        Substitute [v_ = 1]      q___ ;        \

\       M1__ =        Substitute [v_ = 2]      q___ ;        \

\       M1__ =        Substitute [v_ = 3]      q___ ;        \

\       M1__ =        Substitute [M_b 0 = 0]  M1__           \

\ in True)"

;

val str = (*#5#*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  \

\  (let q___ = Take (M_b v_v = q__);                                          \

\      (M1__::bool) = Substitute [v_ = 0]      q___ ;        \

\       M2__ = Take q___ ;                                     \

\       M2__ =        Substitute [v_ = 2]      q___           \

\ in True)"

;

(*========== inhibit exn 110721 ================================================

val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty sc';

========== inhibit exn 110721 ================================================*)

val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];

(*---------------------------------------------------------------------

if sc = sc' then () else error"script.sml, doesnt find Substitute #1";

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

val fmz = ["Traegerlaenge L",

	   "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",

	   "Biegelinie y",

	   "RandbedingungenBiegung [y 0 = 0, y L = 0]",

	   "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

	   "FunktionsVariable x"];

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

  ("Biegelinie",["MomentBestimmte","Biegelinien"],

   ["IntegrierenUndKonstanteBestimmen"]);

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

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

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

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

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

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

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

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

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

case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()

	  | _ => error "script.sml, doesnt find Substitute #2";

(*========== inhibit exn 110721 ================================================

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

(* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)

(* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)

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

(* *** generate1: not impl.for Empty_Tac_  !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)

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

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

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

(*---------------------------------------------------------------------*)

case nxt of (_, End_Proof') => () 

	  | _ => error "script.sml, doesnt find Substitute #3";

(*---------------------------------------------------------------------*)

(*the reason, that next_tac didnt find the 2nd Substitute, was that

  the Take inbetween was missing, and thus the 2nd Substitute was applied

  the last formula in ctree, and not to argument from script*)

========== inhibit exn 110721 ================================================*)

"----------- WN0509 Substitute 2nd part --------------------------";

"----------- WN0509 Substitute 2nd part --------------------------";

"----------- WN0509 Substitute 2nd part --------------------------";

(*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)

val str = (*Substitute ; Substitute works*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  "^

(*begin after the 2nd integrate*)

"  (let M__ = Take (M_b v_v = q__);                                     \

\       e1__ = nth_ 1 rm_ ;                                         \

\       (x1__::real) = argument_in (lhs e1__);                       \

\       (M1__::bool) = Substitute [v_ = x1__] M__;                   \

\        M1__        = Substitute [e1__] M1__                    \

\ in True)"

;

(*========== inhibit exn 110721 ================================================

(*---^^^-OK-----------------------------------------------------------------*)

val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty sc';

(*---vvv-NOT ok-------------------------------------------------------------*)

========== inhibit exn 110721 ================================================*)

val str = (*Substitute @@ Substitute does NOT work???*)

"Script BiegelinieScript                                             \

\(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

\(rb_::bool list) (rm_::bool list) =                                  "^

(*begin after the 2nd integrate*)

"  (let M__ = Take (M_b v_v = q__);                                     \

\       e1__ = nth_ 1 rm_ ;                                         \

\       (x1__::real) = argument_in (lhs e1__);                       \

\       (M1__::bool) = ((Substitute [v_ = x1__]) @@ \

\                       (Substitute [e1__]))        M__           \

\ in True)"

;

val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];

(*---------------------------------------------------------------------

if sc = sc' then () else error"script.sml, doesnt find Substitute #1";

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

val fmz = ["Traegerlaenge L",

	   "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",

	   "Biegelinie y",

	   "RandbedingungenBiegung [y 0 = 0, y L = 0]",

	   "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

	   "FunktionsVariable x"];

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

  ("Biegelinie",["MomentBestimmte","Biegelinien"],

   ["IntegrierenUndKonstanteBestimmen"]);

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

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

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

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

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

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

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

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

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

case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()

	  | _ => error "script.sml, doesnt find Substitute #2";

(*========== inhibit exn 110721 ================================================

trace_rewrite:=true;

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

trace_rewrite:=false;

(*Exception TYPE raised:

Illegal type for constant "HOL.eq" :: "[real, bool] => bool"

Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =

ListG.nth_ (1 + -1 + -1) []

Exception-

   TYPE

      ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",

         [],

         [Const ("HOL.Trueprop", "bool => prop") $

               (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])

   raised

... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"

ie. the argument had not been simplified before          ^^^^^^^^^^^^^^^

thus corrected eval_argument_in OK*)

========== inhibit exn 110721 ================================================*)

val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];

val e1__ = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";

(*========== inhibit exn 110721 ================================================

val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;

if term2str e1__ = "M_b 0 = 0" then () else 

error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";

========== inhibit exn 110721 ================================================*)

(*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...

val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";

val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;

(*no rewrite*)

calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;

val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)

val l__ = str2term"lhs (M_b 0 = 0)";

(*========== inhibit exn 110721 ================================================

val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;

val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;

trace_rewrite:=true;

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

trace_rewrite:=false;

========== inhibit exn 110721 ================================================*)

show_mets();

"----------- fun sel_appl_atomic_tacs ----------------------------";

"----------- fun sel_appl_atomic_tacs ----------------------------";

"----------- fun sel_appl_atomic_tacs ----------------------------";

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 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

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

val appltacs = sel_appl_atomic_tacs pt p;

(*

(*These SHOULD be the same*)

 print_depth(999);

 appltacs;

 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),

    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),

    Calculate "times"];*)

(*========== inhibit exn 110721 ================================================

if appltacs = 

   [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),

    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),

    Calculate "times"] then ()

else error "script.sml fun sel_appl_atomic_tacs diff.behav.";

========== inhibit exn 110721 ================================================*)

trace_script := true;

trace_script := false;

applyTactic 1 p (hd appltacs);

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

val appltacs = sel_appl_atomic_tacs pt p;

(*========== inhibit exn 110721 ================================================

"----- WN080102 these vvv do not work, because locatetac starts the search\

 \1 stac too low";

(* ERROR: assy: call by ([3], Pbl) *)

applyTactic 1 p (hd appltacs);

autoCalculate 1 CompleteCalc;

============ inhibit exn 110721 ==============================================*)

"----------- fun init_form, fun get_stac -------------------------";

"----------- fun init_form, fun get_stac -------------------------";

"----------- fun init_form, fun get_stac -------------------------";

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

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

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

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

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

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

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

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

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

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

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

"~~~~~ fun me, args:"; val (_,tac) = nxt;

"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);

val (mI,m) = mk_tac'_ tac;

val Appl m = applicable_in p pt m;

member op = specsteps mI; (*false*)

"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);

"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);

val {srls, ...} = get_met mI;

val PblObj {meth=itms, ...} = get_obj I pt p;

val thy' = get_obj g_domID pt p;

val thy = assoc_thy thy';

val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;

val ini = init_form thy sc env;

"----- fun init_form, args:"; val (Script sc) = sc;

"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);

case get_stac thy sc of SOME (Free ("e_e", _)) => ()

| _ => error "script: Const (?, ?) in script (as term) changed";;

"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";

"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";

"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";

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

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

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

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

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

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)

show_pt pt;

"~~~~~ fun me, args:"; val (_,tac) = nxt;

val (pt, p) = case locatetac tac (pt,p) of

	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";

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

val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)

tacis; (*= []*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)

"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

                                 (*WAS stac2tac_ TODO: no match for SubProblem*)

val thy' = get_obj g_domID pt (par_pblobj pt p);

val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;

"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)), 

	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);

l; (*= [R, L, R, L, R, R]*)

val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;

"~~~~~ dont like to go into nstep_up...";

val t = str2term ("SubProblem" ^ 

  "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^

  "[BOOL (-1 + x = 0), REAL x]");

val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)

case tac_ of 

  Subproblem' _ => ()

| _ => error "script.sml x+1=2 start SubProblem from script";

"----------- x+1=2 set ctxt in Subproblem ------------------------";

"----------- x+1=2 set ctxt in Subproblem ------------------------";

"----------- x+1=2 set ctxt in Subproblem ------------------------";