neuper@41999: (* Title: test/../script.sml neuper@41999: Author: Walther Neuper 050908 neuper@37906: (c) copyright due to lincense terms. neuper@37906: *) neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "table of contents -----------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "----------- WN0509 why does next_tac doesnt find Substitute -----"; neuper@37906: "----------- WN0509 Substitute 2nd part --------------------------"; neuper@37906: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@41969: "----------- fun init_form, fun get_stac -------------------------"; neuper@41972: "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for "; neuper@42283: "----------- Take as 1st stac in script --------------------------"; neuper@42394: "----------- 'trace_script' from outside 'fun me '----------------"; neuper@42438: "----------- fun sel_rules ---------------------------------------"; neuper@42438: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: "-----------------------------------------------------------------"; neuper@37906: neuper@42438: val thy = @{theory Isac}; neuper@42281: neuper@37906: "----------- WN0509 why does next_tac doesnt find Substitute -----"; neuper@37906: "----------- WN0509 why does next_tac doesnt find Substitute -----"; neuper@37906: "----------- WN0509 why does next_tac doesnt find Substitute -----"; neuper@37906: neuper@37906: (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*) neuper@37906: val str = (*#1#*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = " ^ akargl@42169: " (let q___q = Take (M_b v_v = q__q); " ^ akargl@42169: " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^ akargl@42169: " in True)"; akargl@42169: neuper@37906: val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; neuper@37906: neuper@37906: val str = (*#2#*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = " ^ akargl@42169: " (M1__M1::bool) = ((Substitute [v_v = 0]) @@ " ^ akargl@42169: " in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*) neuper@37906: neuper@37906: val str = (*#3#*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = " ^ akargl@42169: " (let q___q = Take (q_q v_v = q__q); " ^ akargl@42169: " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^ akargl@42169: " M1__m1 = Substitute [M_b 0 = 0] M1__M1 " ^ akargl@42169: " in True)" neuper@37906: ; neuper@37906: val str = (*#4#*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = " ^ akargl@42169: " (let q___q = Take (q_q v_v = q__q); " ^ akargl@42169: " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^ akargl@42169: " M1__M1 = Substitute [v_v = 1] q___q ; " ^ akargl@42169: " M1__M1 = Substitute [v_v = 2] q___q ; " ^ akargl@42169: " M1__M1 = Substitute [v_v = 3] q___q ; " ^ akargl@42169: " M1__M1 = Substitute [M_b 0 = 0] M1__M1 " ^ akargl@42169: " in True)" neuper@37906: ; neuper@37906: val str = (*#5#*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = " ^ akargl@42169: " (let q___q = Take (M_b v_v = q__q); " ^ akargl@42169: " (M1__M1::bool) = Substitute [v_v = 0] q___q ; " ^ akargl@42169: " M2__M2 = Take q___q ; " ^ akargl@42169: " M2__M2 = Substitute [v_v = 2] q___q " ^ akargl@42169: " in True)" neuper@37906: ; akargl@42145: neuper@37906: val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; neuper@37906: atomty sc'; akargl@42145: neuper@48790: val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; neuper@37906: (*--------------------------------------------------------------------- neuper@38031: if sc = sc' then () else error"script.sml, doesnt find Substitute #1"; neuper@37906: ---------------------------------------------------------------------*) neuper@37906: neuper@37906: "----------- WN0509 Substitute 2nd part --------------------------"; neuper@37906: "----------- WN0509 Substitute 2nd part --------------------------"; neuper@37906: "----------- WN0509 Substitute 2nd part --------------------------"; neuper@37906: (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*) neuper@37906: val str = (*Substitute ; Substitute works*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = "^ neuper@37906: (*begin after the 2nd integrate*) akargl@42169: " (let M__M = Take (M_b v_v = q__q); " ^ akargl@42169: " e1__e1 = nth_nth 1 rm_rm ; " ^ akargl@42169: " (x1__x1::real) = argument_in (lhs e1__e1); " ^ akargl@42169: " (M1__M1::bool) = Substitute [v_v = x1__x1] M__M; " ^ akargl@42169: " M1__M1 = Substitute [e1__e1] M1__M1 " ^ akargl@42169: " in True)" neuper@37906: ; neuper@37906: val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; neuper@37906: atomty sc'; akargl@42145: neuper@37906: val str = (*Substitute @@ Substitute does NOT work???*) akargl@42169: "Script BiegelinieScript " ^ akargl@42169: "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ akargl@42169: "(rb_rb::bool list) (rm_rm::bool list) = "^ neuper@37906: (*begin after the 2nd integrate*) akargl@42169: " (let M__M = Take (M_b v_v = q__q); " ^ akargl@42169: " e1__e1 = nth_nth 1 rm_rm ; " ^ akargl@42169: " (x1__x1::real) = argument_in (lhs e1__e1); " ^ akargl@42169: " (M1__M1::bool) = ((Substitute [v_v = x1__x1]) @@ " ^ akargl@42169: " (Substitute [e1__e1])) M__M " ^ akargl@42169: " in True)" neuper@37906: ; neuper@37906: neuper@48790: val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; neuper@37906: (*--------------------------------------------------------------------- akargl@42169: if sc = sc' then () else error "script.sml, doesnt find Substitute #1"; neuper@37906: ---------------------------------------------------------------------*) neuper@37906: val fmz = ["Traegerlaenge L", neuper@37906: "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)", neuper@37906: "Biegelinie y", neuper@37906: "RandbedingungenBiegung [y 0 = 0, y L = 0]", neuper@37906: "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]", neuper@37906: "FunktionsVariable x"]; neuper@37906: val (dI',pI',mI') = neuper@38058: ("Biegelinie",["MomentBestimmte","Biegelinien"], neuper@37906: ["IntegrierenUndKonstanteBestimmen"]); neuper@37906: val p = e_pos'; val c = []; neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; akargl@42169: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; akargl@42169: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; akargl@42169: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; akargl@42169: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; akargl@42169: val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@37906: case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () neuper@38031: | _ => error "script.sml, doesnt find Substitute #2"; akargl@42169: (* ERROR: caused by f2str f *) neuper@52101: trace_rewrite := false; neuper@42387: neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*); neuper@37906: trace_rewrite:=false; akargl@42169: (*Exception TYPE raised: akargl@42169: Illegal type for constant "HOL.eq" :: "[real, bool] => bool" akargl@42169: Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) = akargl@42169: ListG.nth_ (1 + -1 + -1) [] akargl@42169: Exception- akargl@42169: TYPE akargl@42169: ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"", akargl@42169: [], akargl@42169: [Const ("HOL.Trueprop", "bool => prop") $ akargl@42169: (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)]) akargl@42169: raised akargl@42169: ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))" akargl@42169: ie. the argument had not been simplified before ^^^^^^^^^^^^^^^ akargl@42169: thus corrected eval_argument_in OK*) neuper@37906: val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; neuper@42387: val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]"; akargl@42169: val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1; akargl@42169: if term2str e1__e1 = "M_b 0 = 0" akargl@42169: then () akargl@42169: else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [..."; neuper@37906: neuper@37906: (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???... akargl@42169: val x1__ = str2term"argument_in (lhs (M_b 0 = 0))"; akargl@42169: val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__; akargl@42169: (*no rewrite*) akargl@42169: calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__; akargl@42169: val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*) neuper@37906: akargl@42169: val l__l = str2term "lhs (M_b 0 = 0)"; akargl@42169: val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l; akargl@42169: val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0; neuper@42387: akargl@42169: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*); neuper@42387: if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "Biegelinie.Belastung_Querkraft")) neuper@42387: then () else error ""; neuper@37906: neuper@37906: neuper@37906: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@37906: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@37906: "----------- fun sel_appl_atomic_tacs ----------------------------"; akargl@42145: neuper@37906: states:=[]; neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; neuper@37906: autoCalculate 1 CompleteCalcHead; neuper@37906: autoCalculate 1 (Step 1); neuper@37906: autoCalculate 1 (Step 1); neuper@37906: val ((pt, p), _) = get_calc 1; show_pt pt; neuper@37906: val appltacs = sel_appl_atomic_tacs pt p; neuper@37906: if appltacs = neuper@48895: (* WN130613 neuper@48895: [Rewrite ("radd_commute", "Test.radd_commute") (*"?m + ?n = ?n + ?m"*), neuper@48895: Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), Calculate "TIMES"] *) neuper@48895: [Rewrite ("radd_commute", "Test.radd_commute"), neuper@48895: Rewrite ("add_assoc", "Groups.semigroup_add_class.add_assoc"), Calculate "TIMES"] neuper@48895: then () else error "script.sml fun sel_appl_atomic_tacs diff.behav."; neuper@37906: neuper@37906: trace_script := true; neuper@37906: trace_script := false; neuper@37906: applyTactic 1 p (hd appltacs); neuper@37906: val ((pt, p), _) = get_calc 1; show_pt pt; neuper@37906: val appltacs = sel_appl_atomic_tacs pt p; neuper@48895: (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*) neuper@37906: akargl@42169: "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs)); akargl@42169: val ((pt, _), _) = get_calc cI; akargl@42169: val p = get_pos cI 1; akargl@42169: locatetac; akargl@42169: locatetac tac; akargl@42169: akargl@42169: (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*) akargl@42169: "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip)); akargl@42169: val (mI,m) = mk_tac'_ tac; akargl@42169: applicable_in p pt m ; (*Appl*) akargl@42169: member op = specsteps mI; (*false*) akargl@42169: (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*) akargl@42169: loc_solve_; (*without _ ??? result is -> lOc writing error ???*) akargl@42169: (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*) akargl@42169: (mI,m); (*string * tac*) akargl@42169: ptp (*ptree * pos'*); akargl@42169: "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp); akargl@42169: (*val (msg, cs') = solve m (pt, pos); akargl@42169: (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) akargl@42169: m; akargl@42169: (pt, pos); akargl@42169: "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); akargl@42169: (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*) akargl@42169: akargl@42169: e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) akargl@42169: val ctxt = get_ctxt pt po; akargl@42169: akargl@42169: (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt; akargl@42169: (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) akargl@42169: (assoc_thy (get_obj g_domID pt (par_pblobj pt p))); akargl@42169: assoc_thy; akargl@42169: neuper@37906: autoCalculate 1 CompleteCalc; neuper@37906: neuper@41969: "----------- fun init_form, fun get_stac -------------------------"; neuper@41969: "----------- fun init_form, fun get_stac -------------------------"; neuper@41969: "----------- fun init_form, fun get_stac -------------------------"; neuper@41969: val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"]; neuper@41969: val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], neuper@41969: ["Test","squ-equ-test-subpbl1"]); neuper@41969: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@41969: "~~~~~ fun me, args:"; val (_,tac) = nxt; neuper@41969: "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p); neuper@41969: val (mI,m) = mk_tac'_ tac; neuper@41969: val Appl m = applicable_in p pt m; neuper@41969: member op = specsteps mI; (*false*) neuper@41969: "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp); neuper@41969: "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos); neuper@41969: val {srls, ...} = get_met mI; neuper@41969: val PblObj {meth=itms, ...} = get_obj I pt p; neuper@41969: val thy' = get_obj g_domID pt p; neuper@41969: val thy = assoc_thy thy'; neuper@41969: val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; neuper@41969: val ini = init_form thy sc env; neuper@48790: "----- fun init_form, args:"; val (Prog sc) = sc; neuper@41969: "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc); neuper@41969: case get_stac thy sc of SOME (Free ("e_e", _)) => () neuper@41969: | _ => error "script: Const (?, ?) in script (as term) changed";; neuper@41969: neuper@41972: neuper@41972: "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for "; neuper@41972: "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for "; neuper@41972: "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for "; neuper@41972: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; neuper@41972: val (dI',pI',mI') = neuper@41972: ("Test", ["sqroot-test","univariate","equation","test"], neuper@41972: ["Test","squ-equ-test-subpbl1"]); neuper@41972: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41972: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*) neuper@41972: show_pt pt; neuper@41972: "~~~~~ fun me, args:"; val (_,tac) = nxt; neuper@41973: val (pt, p) = case locatetac tac (pt,p) of neuper@41973: ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; neuper@41972: "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) neuper@41999: val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*) neuper@41972: tacis; (*= []*) neuper@41972: member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) neuper@41972: "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); neuper@41972: (*WAS stac2tac_ TODO: no match for SubProblem*) neuper@41972: val thy' = get_obj g_domID pt (par_pblobj pt p); neuper@41972: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; neuper@48790: "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)), neuper@41972: (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); neuper@41972: l; (*= [R, L, R, L, R, R]*) neuper@41972: val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v; neuper@41972: "~~~~~ dont like to go into nstep_up..."; neuper@41972: val t = str2term ("SubProblem" ^ neuper@41972: "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^ neuper@41972: "[BOOL (-1 + x = 0), REAL x]"); neuper@41972: val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*) neuper@41972: case tac_ of neuper@41972: Subproblem' _ => () neuper@41972: | _ => error "script.sml x+1=2 start SubProblem from script"; neuper@41972: neuper@41972: neuper@42283: "----------- Take as 1st stac in script --------------------------"; neuper@42283: "----------- Take as 1st stac in script --------------------------"; neuper@42283: "----------- Take as 1st stac in script --------------------------"; neuper@42283: val p = e_pos'; val c = []; neuper@42283: val (p,_,f,nxt,_,pt) = neuper@42283: CalcTreeTEST neuper@42283: [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], neuper@42283: ("Integrate", ["integrate","function"], ["diff","integration"]))]; neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*) neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@42283: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@42283: case nxt of (_, Apply_Method ["diff", "integration"]) => () neuper@42283: | _ => error "integrate.sml -- me method [diff,integration] -- spec"; neuper@42283: "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")"; neuper@42283: neuper@42283: "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); neuper@42283: "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); neuper@42283: val (mI,m) = mk_tac'_ tac; neuper@42283: val Appl m = applicable_in p pt m; neuper@42283: member op = specsteps mI (*false*); neuper@42283: "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp); neuper@42283: "~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = neuper@42283: (m, (pt, pos)); neuper@42283: val {srls, ...} = get_met mI; neuper@42283: val PblObj {meth=itms, ...} = get_obj I pt p; neuper@42283: val thy' = get_obj g_domID pt p; neuper@42283: val thy = assoc_thy thy'; neuper@42283: val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; neuper@42283: val ini = init_form thy sc env; neuper@42283: val p = lev_dn p; neuper@42283: ini = NONE; (*true*) neuper@42283: val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); neuper@42283: val d = e_rls (*FIXME: get simplifier from domID*); neuper@42283: "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), neuper@48790: (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = neuper@42283: ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); neuper@42283: val thy = assoc_thy thy'; neuper@42283: l = [] orelse ((*init.in solve..Apply_Method...*) neuper@42283: (last_elem o fst) p = 0 andalso snd p = Res); (*true*) neuper@42283: "~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss), neuper@42283: (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = neuper@42283: ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body); neuper@42283: (*check: true*) term2str e = "Take (Integral f_f D v_v)"; neuper@42283: "~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = neuper@42283: (ya, ((E , l@[L,R], a,v,S,b),ss), e); neuper@42283: val (a', STac stac) = handle_leaf "locate" thy' sr E a v t; neuper@42283: (* val ctxt = get_ctxt pt (p,p_) neuper@42283: exception PTREE "get_obj: pos = [0] does not exist" raised neuper@42283: (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*) neuper@42283: neuper@42283: neuper@42394: "----------- 'trace_script' from outside 'fun me '----------------"; neuper@42394: "----------- 'trace_script' from outside 'fun me '----------------"; neuper@42394: "----------- 'trace_script' from outside 'fun me '----------------"; neuper@42394: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; neuper@42394: val (dI',pI',mI') = neuper@42394: ("Test", ["sqroot-test","univariate","equation","test"], neuper@42394: ["Test","squ-equ-test-subpbl1"]); neuper@42394: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*) neuper@42394: (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*) neuper@42394: neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: f2str f = "x + 1 = 2"; snd nxt = Rewrite_Set "norm_equation"; neuper@42394: val (p, p_) = p(* = ([1], Frm)*); neuper@48790: val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt; neuper@42394: val (env, loc_, curry_arg, res, Safe, true) = scrstate; neuper@42394: env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]"; neuper@42394: loc_ = []; neuper@42394: curry_arg = NONE; neuper@42394: term2str res = "??.empty"; (* scrstate before starting interpretation *) neuper@48790: (*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*) neuper@42394: neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify"; neuper@42394: val (p, p_) = p(* = ([1], Res)*); neuper@48790: val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt; neuper@42394: val (env, loc_, curry_arg, res, Safe, true) = scrstate; neuper@42394: env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]"; neuper@42394: loc_ = [R, L, R, L, L, R, R]; neuper@42394: curry_arg = SOME (str2term "e_e::bool"); neuper@42394: term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *) neuper@42394: term2str (go loc_ sc) = "Rewrite_Set norm_equation False"; neuper@42394: neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]); neuper@42394: val (p, p_) = p(* = ([2], Res)*); neuper@48790: val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt; neuper@42394: val (env, loc_, curry_arg, res, Safe, false) = scrstate; neuper@42394: env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]"; neuper@42394: loc_ = [R, L, R, L, R, R]; neuper@42394: curry_arg = SOME (str2term "e_e::bool"); neuper@42394: term2str res = "-1 + x = 0"; (* scrstate after Test_simplify, before Subproblem *) neuper@42394: term2str (go loc_ sc) = "Rewrite_Set Test_simplify False"; neuper@42394: neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); (*f2str f = exception Match; ...is a model, not a formula*) neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*) neuper@42394: (*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*) neuper@42394: neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"); neuper@42394: val (p, p_) = p(* = ([3, 1], Frm)*); neuper@48790: val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt; neuper@42394: val (env, loc_, curry_arg, res, Safe, true) = scrstate; neuper@42394: env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]"; neuper@42394: loc_ = []; neuper@42394: curry_arg = NONE; neuper@42394: term2str res = "??.empty"; (* scrstate before starting interpretation *) neuper@48790: (*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*) neuper@42394: neuper@42394: val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*) neuper@42394: val (p'''', pt'''') = (p, pt); neuper@42394: f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify"; neuper@42394: val (p, p_) = p(* = ([3, 1], Res)*); neuper@48790: val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt; neuper@42394: val (env, loc_, curry_arg, res, Safe, true) = scrstate; neuper@42394: env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]"; neuper@42394: loc_ = [R, L, R, L, R, L, R]; neuper@42394: curry_arg = SOME (str2term "e_e::bool"); neuper@42394: term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *) neuper@42394: term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False"; neuper@42394: neuper@42438: "----------- fun sel_rules ---------------------------------------"; neuper@42438: "----------- fun sel_rules ---------------------------------------"; neuper@42438: "----------- fun sel_rules ---------------------------------------"; neuper@42438: (* compare test/../interface.sml neuper@42438: "--------- getTactic, fetchApplicableTactics ------------"; neuper@42438: *) neuper@42438: states:=[]; neuper@42438: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@42438: ("Test", ["sqroot-test","univariate","equation","test"], neuper@42438: ["Test","squ-equ-test-subpbl1"]))]; neuper@42438: Iterator 1; neuper@42438: moveActiveRoot 1; neuper@42438: autoCalculate 1 CompleteCalc; neuper@42438: val ((pt,_),_) = get_calc 1; neuper@42438: show_pt pt; neuper@42394: neuper@42438: (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*) neuper@42438: val tacs = sel_rules pt ([],Pbl); neuper@42438: if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then () neuper@42438: else error "script.sml: diff.behav. in sel_rules ([],Pbl)"; neuper@42438: neuper@42438: val tacs = sel_rules pt ([1],Res); neuper@42438: if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", neuper@42438: Subproblem ("Test", ["linear", "univariate", "equation", "test"]), neuper@42438: Check_elementwise "Assumptions"] then () neuper@42438: else error "script.sml: diff.behav. in sel_rules ([1],Res)"; neuper@42438: neuper@42438: val tacs = sel_rules pt ([3],Pbl); neuper@42438: if tacs = [Apply_Method ["Test", "solve_linear"]] then () neuper@42438: else error "script.sml: diff.behav. in sel_rules ([3],Pbl)"; neuper@42438: neuper@42438: val tacs = sel_rules pt ([3,1],Res); neuper@42438: if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), neuper@42438: Rewrite_Set "Test_simplify"] then () neuper@42438: else error "script.sml: diff.behav. in sel_rules ([3,1],Res)"; neuper@42438: neuper@42438: val tacs = sel_rules pt ([3],Res); neuper@42438: if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", neuper@42438: Subproblem ("Test", ["linear", "univariate", "equation", "test"]), neuper@42438: Check_elementwise "Assumptions"] then () neuper@42438: else error "script.sml: diff.behav. in sel_rules ([3],Res)"; neuper@42438: neuper@42438: val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str]; neuper@42438: if tacs = [Tac "no tactics applicable at the end of a calculation"] then () neuper@42438: else error "script.sml: diff.behav. in sel_rules ([],Res)"; neuper@42438: neuper@42438: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@42438: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@42438: "----------- fun sel_appl_atomic_tacs ----------------------------"; neuper@42438: states:=[]; neuper@42438: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@42438: ("Test", ["sqroot-test","univariate","equation","test"], neuper@42438: ["Test","squ-equ-test-subpbl1"]))]; neuper@42438: Iterator 1; neuper@42438: moveActiveRoot 1; neuper@42438: autoCalculate 1 CompleteCalc; neuper@42438: neuper@42438: (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*) neuper@42438: fetchApplicableTactics 1 99999 ([],Pbl); neuper@42438: neuper@42438: fetchApplicableTactics 1 99999 ([1],Res); neuper@42438: "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res)); neuper@42438: val ((pt, _), _) = get_calc cI; neuper@42438: (*version 1:*) neuper@42438: if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", neuper@42438: Subproblem ("Test", ["linear", "univariate", "equation", "test"]), neuper@42438: Check_elementwise "Assumptions"] then () neuper@42438: else error "fetchApplicableTactics ([1],Res) changed"; neuper@42438: (*version 2:*) neuper@42438: (*WAS: neuper@42438: sel_appl_atomic_tacs pt p; neuper@42438: ... neuper@42438: ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])' neuper@42438: ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' neuper@42438: *) neuper@42438: neuper@42438: "~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p); neuper@42438: is_spec_pos p_ = false; neuper@42438: val pp = par_pblobj pt p neuper@42438: val thy' = (get_obj g_domID pt pp):theory' neuper@42438: val thy = assoc_thy thy' neuper@42438: val metID = get_obj g_metID pt pp neuper@42438: val metID' = neuper@42438: if metID = e_metID neuper@42438: then (thd3 o snd3) (get_obj g_origin pt pp) neuper@42438: else metID neuper@48790: val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID' neuper@42438: val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_) neuper@42438: val alltacs = (*we expect at least 1 stac in a script*) neuper@42438: map ((stac2tac pt thy) o rep_stacexpr o #2 o neuper@42438: (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) neuper@42438: val f = neuper@42438: case p_ of neuper@42438: Frm => get_obj g_form pt p neuper@42438: | Res => (fst o (get_obj g_result pt)) p neuper@42438: (*WN120611 stopped and took version 1 again for fetchApplicableTactics ! neuper@42438: (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs neuper@42438: ... neuper@42438: ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])' neuper@42438: ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' neuper@42438: *) neuper@42438: