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

"----------- Take as 1st stac in script --------------------------";

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

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

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

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

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

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

"----------- Take as 1st stac in script --------------------------";

"----------- Take as 1st stac in script --------------------------";

"----------- Take as 1st stac in script --------------------------";

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

val (p,_,f,nxt,_,pt) = 

    CalcTreeTEST 

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

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

val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)

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 ["diff", "integration"]) => ()

          | _ => error "integrate.sml -- me method [diff,integration] -- spec";

"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";

"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);

"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (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 ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = 

                            (m, (pt, 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;

        val p = lev_dn p;

ini = NONE; (*true*)

            val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);

	            val d = e_rls (*FIXME: get simplifier from domID*);

"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 

	                     (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 

                   ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));

val thy = assoc_thy thy';

l = [] orelse ((*init.in solve..Apply_Method...*)

			         (last_elem o fst) p = 0 andalso snd p = Res); (*true*)

"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss), 

                   (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = 

                 ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);

 (*check: true*) term2str e = "Take (Integral f_f D v_v)";

"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = 

                           (ya, ((E , l@[L,R], a,v,S,b),ss), e);

val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;

(*             val ctxt = get_ctxt pt (p,p_)

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

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