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

   Author: Walther Neuper 050908

   (c) copyright due to lincense terms.

*)

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

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

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

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

"----------- 'trace_script' from outside 'fun me '----------------";

"----------- fun sel_rules ---------------------------------------";

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

"----------- fun de_esc_underscore -------------------------------";

"----------- fun go ----------------------------------------------";

"----------- fun formal_args -------------------------------------";

"----------- fun dsc_valT ----------------------------------------";

"----------- fun itms2args ---------------------------------------";

"----------- fun rep_tac_ ----------------------------------------";

"----------- fun init_scrstate -----------------------------------------------------------------";

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

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

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

val thy =  @{theory Isac};

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

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

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

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

case appltacs of 

  [Rewrite ("radd_commute", radd_commute), 

  Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]

  => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso 

        (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()

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

| _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";

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;

(*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 (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_ -> ctree * (pos * pos_) -> lOc_*)

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

ptp (*ctree * 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;

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 (Prog 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,_)):ctree * pos'), (sc as Prog (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:ctree)) = (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):ctree * pos'), 

	                     (scr as Prog (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")*)

"----------- 'trace_script' from outside 'fun me '----------------";

"----------- 'trace_script' from outside 'fun me '----------------";

"----------- 'trace_script' from outside 'fun me '----------------";

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; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

(*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)

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

val (p'''', pt'''') = (p, pt);

f2str f = "x + 1 = 2"; case snd nxt of Rewrite_Set "norm_equation" => () | _ => error "CHANGED";

val (p, p_) = p(* = ([1], Frm)*);

val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;

val (env, loc_, curry_arg, res, Safe, true) = scrstate;

  env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";

  loc_ = [];

  curry_arg = NONE;

  term2str res = "??.empty";                     (* scrstate before starting interpretation *)

(*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*)

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

val (p'''', pt'''') = (p, pt);

f2str f = "x + 1 + -1 * 2 = 0";

case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";

val (p, p_) = p(* = ([1], Res)*);

val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;

val (env, loc_, curry_arg, res, Safe, true) = scrstate;

  env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";

  loc_ = [R, L, R, L, L, R, R];

  curry_arg = SOME (str2term "e_e::bool");

  term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *)

term2str (go loc_ sc) = "Rewrite_Set norm_equation False";

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

val (p'''', pt'''') = (p, pt);

f2str f = "-1 + x = 0";

case snd nxt of Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) => () 

| _ => error "CHANGED";

val (p, p_) = p(* = ([2], Res)*);

val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;

val (env, loc_, curry_arg, res, Safe, false) = scrstate;

  env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";

  loc_ = [R, L, R, L, R, R];

  curry_arg = SOME (str2term "e_e::bool");

  term2str res = "-1 + x = 0";           (* scrstate after Test_simplify, before Subproblem *)

term2str (go loc_ sc) = "Rewrite_Set Test_simplify False";

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

val (p'''', pt'''') = (p, pt);     (*f2str f = exception Match; ...is a model, not a formula*)

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

val (p'''', pt'''') = (p, pt);

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

val (p'''', pt'''') = (p, pt);

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

val (p'''', pt'''') = (p, pt);

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

val (p'''', pt'''') = (p, pt);

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

val (p'''', pt'''') = (p, pt);

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

val (p'''', pt'''') = (p, pt);

val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*)

(*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)

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

val (p'''', pt'''') = (p, pt);

f2str f = "-1 + x = 0";

case snd nxt of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => () | _ => error "CHANGED";

val (p, p_) = p(* = ([3, 1], Frm)*);

val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;

val (env, loc_, curry_arg, res, Safe, true) = scrstate;

  env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";

  loc_ = [];

  curry_arg = NONE;

  term2str res = "??.empty";                     (* scrstate before starting interpretation *)

(*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*)

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

val (p'''', pt'''') = (p, pt);

f2str f = "x = 0 + -1 * -1";

case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";

val (p, p_) = p(* = ([3, 1], Res)*);

val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;

val (env, loc_, curry_arg, res, Safe, true) = scrstate;

  env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";

  loc_ = [R, L, R, L, R, L, R];

  curry_arg = SOME (str2term "e_e::bool");

  term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)

term2str (go loc_ sc) = "Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False";

"----------- fun sel_rules ---------------------------------------";

"----------- fun sel_rules ---------------------------------------";

"----------- fun sel_rules ---------------------------------------";

(* compare test/../interface.sml

"--------- getTactic, fetchApplicableTactics ------------";

*)

 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;

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

 show_pt pt;

(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

 val tacs = sel_rules pt ([],Pbl);

 case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()

 | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";

 val tacs = sel_rules pt ([1],Res);

 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

      Check_elementwise "Assumptions"] => ()

 | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";

 val tacs = sel_rules pt ([3],Pbl);

 case tacs of [Apply_Method ["Test", "solve_linear"]] => ()

 | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";

 val tacs = sel_rules pt ([3,1],Res);

 case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()

 | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";

 val tacs = sel_rules pt ([3],Res);

 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

      Check_elementwise "Assumptions"] => ()

 | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";

 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];

 case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()

 | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";

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

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

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

 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;

(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

 fetchApplicableTactics 1 99999 ([],Pbl);

 fetchApplicableTactics 1 99999 ([1],Res);

"~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));

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

(*version 1:*)

case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

  Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

  Check_elementwise "Assumptions"] => ()

| _ => error "fetchApplicableTactics ([1],Res) changed";

(*version 2:*)

(*WAS:

sel_appl_atomic_tacs pt p;

...

### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])' 

### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' 

*)

"~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p);

is_spec_pos p_ = false;

        val pp = par_pblobj pt p

        val thy' = (get_obj g_domID pt pp):theory'

        val thy = assoc_thy thy'

        val metID = get_obj g_metID pt pp

        val metID' =

          if metID = e_metID 

          then (thd3 o snd3) (get_obj g_origin pt pp)

          else metID

        val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'

        val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)

        val alltacs = (*we expect at least 1 stac in a script*)

          map ((stac2tac pt thy) o rep_stacexpr o #2 o

           (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)

        val f =

          case p_ of

              Frm => get_obj g_form pt p

            | Res => (fst o (get_obj g_result pt)) p;

(*WN120611 stopped and took version 1 again for fetchApplicableTactics !

(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs

...

### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])' 

### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' 

*)

"----------- fun de_esc_underscore -------------------------------";

"----------- fun de_esc_underscore -------------------------------";

"----------- fun de_esc_underscore -------------------------------";

(*

> val str = "Rewrite_Set_Inst";

> val esc = esc_underscore str;

val it = "Rewrite'_Set'_Inst" : string

> val des = de_esc_underscore esc;

 val des = de_esc_underscore esc;*)

"----------- fun go ----------------------------------------------";

"----------- fun go ----------------------------------------------";

"----------- fun go ----------------------------------------------";

(*

> val t = (Thm.term_of o the o (parse thy)) "a+b";

val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term

> val plus_a = go [L] t; 

> val b = go [R] t; 

> val plus = go [L,L] t; 

> val a = go [L,R] t;

> val t = (Thm.term_of o the o (parse thy)) "a+b+c";

val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term

> val pl_pl_a_b = go [L] t; 

> val c = go [R] t; 

> val a = go [L,R,L,R] t; 

> val b = go [L,R,R] t; 

*)

"----------- fun formal_args -------------------------------------";

"----------- fun formal_args -------------------------------------";

"----------- fun formal_args -------------------------------------";

(*

> formal_args scr;

  [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),

   Free ("eqs_","bool List.list")] : term list

*)

"----------- fun dsc_valT ----------------------------------------";

"----------- fun dsc_valT ----------------------------------------";

"----------- fun dsc_valT ----------------------------------------";

(*> val t = (Thm.term_of o the o (parse thy)) "equality";

> val T = type_of t;

val T = "bool => Tools.una" : typ

> val dsc = dsc_valT t;

val dsc = "una" : string

> val t = (Thm.term_of o the o (parse thy)) "fixedValues";

> val T = type_of t;

val T = "bool List.list => Tools.nam" : typ

> val dsc = dsc_valT t;

val dsc = "nam" : string*)

"----------- fun itms2args ---------------------------------------";

"----------- fun itms2args ---------------------------------------";

"----------- fun itms2args ---------------------------------------";

(*

> val sc = ... Solve_root_equation ...

> val mI = ("Script","sqrt-equ-test");

> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];

> val ts = itms2args thy mI itms;

> map (term_to_string''' thy) ts;

["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list

*)

"----------- fun rep_tac_ ----------------------------------------";

"----------- fun rep_tac_ ----------------------------------------";

"----------- fun rep_tac_ ----------------------------------------";

(***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) = 

Fehlersuche 25.4.01

(a)----- als String zusammensetzen:

ML> term2str f; 

val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string

ML> term2str f'; 

val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string

ML> subs;

val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst

> val tt = (Thm.term_of o the o (parse thy))

  "(Rewrite_Inst[(''bdv'',x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";

> atomty tt;

ML> tracing (term2str tt); 

(Rewrite_Inst [(''bdv'',x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =

 #0 + d_d x (x ^^^ #2 + #3 * x)

(b)----- laut rep_tac_:

> val ttt=HOLogic.mk_eq (lhs,f');

> atomty ttt;

(*Fehlersuche 1-2Monate vor 4.01:*)

> val tt = (Thm.term_of o the o (parse thy))

  "Rewrite_Inst[(''bdv'',x)]square_equation_left True(x=#1+#2)";

> atomty tt;

> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";

> val f' = (Thm.term_of o the o (parse thy)) "x=#3";

> val subs = [((Thm.term_of o the o (parse thy)) "bdv",

	       (Thm.term_of o the o (parse thy)) "x")];

> val sT = (type_of o fst o hd) subs;

> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

			      (map HOLogic.mk_prod subs);

> val sT' = type_of subs';

> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT) 

  $ subs' $ Free (thmID,idT) $ @{term True} $ f;

> lhs = tt;

val it = true : bool

> rep_tac_ (Rewrite_Inst' 

	       ("Script","tless_true","eval_rls",false,subs,

		("square_equation_left",""),f,(f',[])));

*)

(****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=

> val tt = (Thm.term_of o the o (parse thy)) (*____   ____..test*)

  "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";

> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";

> val f' = (Thm.term_of o the o (parse thy)) "x=#3";

> val Thm (id,thm) = 

  rep_tac_ (Rewrite' 

   ("Script","tless_true","eval_rls",false,

    ("square_equation_left",""),f,(f',[])));

> val SOME ct = parse thy   

  "Rewrite square_equation_left True (x=#1+#2)"; 

> rewrite_ Script.thy tless_true eval_rls true thm ct;

val it = SOME ("x = #3",[]) : (cterm * cterm list) option

*)

(****************************************  | rep_tac_ (Rewrite_Set_Inst' 

WN050824: type error ...

  let val fT = type_of f;

    val sT = (type_of o fst o hd) subs;

    val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

      (map HOLogic.mk_prod subs);

    val sT' = type_of subs';

    val b = if put then @{term True} else @{term False}

    val lhs = Const ("Script.Rewrite'_Set'_Inst",

		     [sT',idT,fT,fT] ---> fT) 

      $ subs' $ Free (id_rls rls,idT) $ b $ f;

  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)

(* ... vals from Rewrite_Inst' ...

> rep_tac_ (Rewrite_Set_Inst' 

	       ("Script",false,subs,

		"isolate_bdv",f,(f',[])));

*)

(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;

*)

(**************************************   | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=

13.3.01:

val thy = assoc_thy thy';

val t = HOLogic.mk_eq (lhs,f');

make_rule thy t;

--------------------------------------------------

val lll = (Thm.term_of o the o (parse thy)) 

  "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";

--------------------------------------------------

> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";

> val f' = (Thm.term_of o the o (parse thy)) "x=#3";

> val Thm (id,thm) = 

  rep_tac_ (Rewrite_Set' 

   ("Script",false,"SqRoot_simplify",f,(f',[])));

val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string

val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm

*)

(*****************************************   | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=

> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";

  ... test-root-equ.sml: calculate ...

> val Appl m'=applicable_in p pt (Calculate "PLUS");

> val (lhs,_)=tac_2etac m';

> lhs'=lhs;

val it = true : bool*)

"----------- fun init_scrstate -----------------------------------------------------------------";

"----------- fun init_scrstate -----------------------------------------------------------------";

"----------- fun init_scrstate -----------------------------------------------------------------";

val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",

	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

	     "AbleitungBiegelinie dy"];

val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

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

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

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)

(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)

val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');

"~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);

val (ScrState st, ctxt, Prog _) = init_scrstate thy itms metID;

if scrstate2str st =

"([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], NONE, \n??.empty, Safe, true)"

then () else error "init_scrstate changed for Biegelinie";

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)

if p = ([1], Pbl) andalso (fst nxt) = "Model_Problem" then ()

else error "modeling root-problem of Biegelinie 7.70 changed";