1.1 --- a/test/Tools/isac/Interpret/script.sml Fri Sep 23 09:41:11 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Sep 23 13:58:27 2011 +0200
1.3 @@ -6,12 +6,11 @@
1.4 "table of contents -----------------------------------------------";
1.5 "-----------------------------------------------------------------";
1.6 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.7 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
1.8 "----------- WN0509 Substitute 2nd part --------------------------";
1.9 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.10 "----------- fun init_form, fun get_stac -------------------------";
1.11 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
1.12 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
1.13 +"----------- Take as 1st stac in script --------------------------";
1.14 "-----------------------------------------------------------------";
1.15 "-----------------------------------------------------------------";
1.16 "-----------------------------------------------------------------";
1.17 @@ -80,66 +79,6 @@
1.18 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
1.19 ---------------------------------------------------------------------*)
1.20
1.21 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
1.22 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
1.23 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
1.24 -(*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
1.25 -val fmz = ["Traegerlaenge L",
1.26 - "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
1.27 - "Biegelinie y",
1.28 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.29 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.30 - "FunktionsVariable x"];
1.31 -val (dI',pI',mI') =
1.32 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
1.33 - ["IntegrierenUndKonstanteBestimmen"]);
1.34 -val p = e_pos'; val c = [];
1.35 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.36 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.37 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.38 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.40 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.41 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.43 -
1.44 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.45 - | _ => error "script.sml, doesnt find Substitute #2";
1.46 -
1.47 -(*========== inhibit exn AK110721 ================================================
1.48 -
1.49 -(* AK110722 f2str f is NOT working anywhere - deprecated?????*)
1.50 -
1.51 -(*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.52 - (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
1.53 - (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
1.54 -(*f2str f;
1.55 - (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
1.56 -(* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
1.57 - (* ERROR: exception Bind raised *)*)
1.58 -
1.59 - f;
1.60 - f2str;*)
1.61 -
1.62 -(* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
1.63 -(* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
1.64 -
1.65 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.66 -(* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
1.67 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.68 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.69 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.70 -(*---------------------------------------------------------------------*)
1.71 -
1.72 -case nxt of (_, End_Proof') => ()
1.73 - | _ => error "script.sml, doesnt find Substitute #3";
1.74 -(*---------------------------------------------------------------------*)
1.75 -(*the reason, that next_tac didnt find the 2nd Substitute, was that
1.76 - the Take inbetween was missing, and thus the 2nd Substitute was applied
1.77 - the last formula in ctree, and not to argument from script*)
1.78 -========== inhibit exn AK110721 ================================================*)
1.79 -
1.80 -
1.81 "----------- WN0509 Substitute 2nd part --------------------------";
1.82 "----------- WN0509 Substitute 2nd part --------------------------";
1.83 "----------- WN0509 Substitute 2nd part --------------------------";
1.84 @@ -419,6 +358,58 @@
1.85 | _ => error "script.sml x+1=2 start SubProblem from script";
1.86
1.87
1.88 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
1.89 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
1.90 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
1.91 +"----------- Take as 1st stac in script --------------------------";
1.92 +"----------- Take as 1st stac in script --------------------------";
1.93 +"----------- Take as 1st stac in script --------------------------";
1.94 +val p = e_pos'; val c = [];
1.95 +val (p,_,f,nxt,_,pt) =
1.96 + CalcTreeTEST
1.97 + [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
1.98 + ("Integrate", ["integrate","function"], ["diff","integration"]))];
1.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
1.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.102 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.103 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.104 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.105 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.106 +case nxt of (_, Apply_Method ["diff", "integration"]) => ()
1.107 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
1.108 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
1.109 +
1.110 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
1.111 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
1.112 +val (mI,m) = mk_tac'_ tac;
1.113 +val Appl m = applicable_in p pt m;
1.114 +member op = specsteps mI (*false*);
1.115 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
1.116 +"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
1.117 + (m, (pt, pos));
1.118 +val {srls, ...} = get_met mI;
1.119 + val PblObj {meth=itms, ...} = get_obj I pt p;
1.120 + val thy' = get_obj g_domID pt p;
1.121 + val thy = assoc_thy thy';
1.122 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.123 + val ini = init_form thy sc env;
1.124 + val p = lev_dn p;
1.125 +ini = NONE; (*true*)
1.126 + val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.127 + val d = e_rls (*FIXME: get simplifier from domID*);
1.128 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
1.129 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
1.130 + ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
1.131 +val thy = assoc_thy thy';
1.132 +l = [] orelse ((*init.in solve..Apply_Method...*)
1.133 + (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
1.134 +"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
1.135 + (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
1.136 + ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
1.137 + (*check: true*) term2str e = "Take (Integral f_f D v_v)";
1.138 +"~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
1.139 + (ya, ((E , l@[L,R], a,v,S,b),ss), e);
1.140 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
1.141 +(* val ctxt = get_ctxt pt (p,p_)
1.142 +exception PTREE "get_obj: pos = [0] does not exist" raised
1.143 +(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
1.144 +
1.145 +