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

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

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

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

val thy= @{theory Isac};

"----------- 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_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^ 

"(rb_rb::bool list) (rm_rm::bool list) =                             " ^

"  (let q___q = Take (M_b v_v = q__q);                               " ^

"       (M1__M1::bool) = ((Substitute [v_v = 0])) q___q              " ^

" in True)";

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

val str = (*#2#*)

"Script BiegelinieScript                                             " ^ 

"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^ 

"(rb_rb::bool list) (rm_rm::bool list) =                             " ^ 

"       (M1__M1::bool) = ((Substitute [v_v = 0]) @@                  " ^

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

val str = (*#3#*)

"Script BiegelinieScript                                             " ^

"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^

"(rb_rb::bool list) (rm_rm::bool list) =                             " ^

"  (let q___q = Take (q_q v_v = q__q);                               " ^

"      (M1__M1::bool) = Substitute [v_v = 0]      q___q ;            " ^

"       M1__m1 =        Substitute [M_b 0 = 0]  M1__M1               " ^

" in True)"

;

val str = (*#4#*)

"Script BiegelinieScript                                             " ^

"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^

"(rb_rb::bool list) (rm_rm::bool list) =                             " ^

"  (let q___q = Take (q_q v_v = q__q);                               " ^

"      (M1__M1::bool) = Substitute [v_v = 0]      q___q ;            " ^

"       M1__M1 =        Substitute [v_v = 1]      q___q ;            " ^

"       M1__M1 =        Substitute [v_v = 2]      q___q ;            " ^

"       M1__M1 =        Substitute [v_v = 3]      q___q ;            " ^

"       M1__M1 =        Substitute [M_b 0 = 0]  M1__M1               " ^

" in True)"

;

val str = (*#5#*)

"Script BiegelinieScript                                             " ^

"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^

"(rb_rb::bool list) (rm_rm::bool list) =                             " ^

"  (let q___q = Take (M_b v_v = q__q);                               " ^

"      (M1__M1::bool) = Substitute [v_v = 0]      q___q ;            " ^

"       M2__M2 = Take q___q ;                                        " ^

"       M2__M2 =        Substitute [v_v = 2]      q___q              " ^

" in True)"

;

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

atomty sc';

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

(* AK110722 f2str f is NOT working anywhere - deprecated?????*)

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

  (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised 

            (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)

(*f2str f;

  (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)

(* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);

  (* ERROR: exception Bind raised *)*)

 f;

 f2str;*)

(* *** 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 AK110721 ================================================*)

"----------- 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_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^

"(rb_rb::bool list) (rm_rm::bool list) =                             "^

(*begin after the 2nd integrate*)

"  (let M__M = Take (M_b v_v = q__q);                                " ^

"       e1__e1 = nth_nth 1 rm_rm ;                                   " ^

"       (x1__x1::real) = argument_in (lhs e1__e1);                   " ^

"       (M1__M1::bool) = Substitute [v_v = x1__x1] M__M;             " ^

"        M1__M1        = Substitute [e1__e1] M1__M1                  " ^

" in True)"

;

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

atomty sc';

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

"Script BiegelinieScript                                             " ^

"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)              " ^

"(rb_rb::bool list) (rm_rm::bool list) =                             "^

(*begin after the 2nd integrate*)

"  (let M__M = Take (M_b v_v = q__q);                                " ^

"       e1__e1 = nth_nth 1 rm_rm ;                                   " ^

"       (x1__x1::real) = argument_in (lhs e1__e1);                   " ^

"       (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@             " ^

"                       (Substitute [e1__e1]))        M__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 AK110721 ================================================

(* ERROR: caused by f2str f *)

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

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

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

val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;

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

(*AK110722

 TRIAL: Should be the same

 term2str e1__e1 = "M_b 0 = 0";

 term2str e1__e1;*)

if term2str e1__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__l = str2term "lhs (M_b 0 = 0)";

(*AK110722 eval_listexpr_ is prob. without _ ????*)

val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;

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

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

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;

(*========== inhibit exn AK110721 ================================================

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

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

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;

(*(* AK110722 Debugging start*)

(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)

"~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));

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

val p = get_pos cI 1;

locatetac;

locatetac tac;

locatetac tac;

(*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)

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

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

applicable_in p pt m ; (*Appl*)

member op = specsteps mI; (*false*)

(*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)

loc_solve_; (*without _ ??? result is -> lOc writing error ???*)

(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)

(mI,m); (*string * tac*)

ptp (*ptree * pos'*);

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

(*val (msg, cs') = solve m (pt, pos);

(*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)

m;

(pt, pos);

"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));

(*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)

e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)

val ctxt = get_ctxt pt po;

(*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;

(*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)

(assoc_thy (get_obj g_domID pt (par_pblobj pt p)));

assoc_thy;

(*not finished - error continues in fun generate1*)

(* AK110722 Debugging end*)*)

(*========== inhibit exn AK110721 ================================================

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

 "1 stac too low";

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

applyTactic 1 p (hd appltacs);

============ inhibit exn AK110721 ==============================================*)

autoCalculate 1 CompleteCalc;

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