1.1 --- a/src/Tools/isac/Interpret/script.sml Fri Sep 23 09:41:11 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Sep 23 13:58:27 2011 +0200
1.3 @@ -986,7 +986,6 @@
1.4 (subst_atomic (upd_env_opt E (a',v)) t), E))
1.5 | (a', STac stac) =>
1.6 let
1.7 - val ctxt = get_ctxt pt (p,p_)
1.8 val p' =
1.9 case p_ of Frm => p
1.10 | Res => lev_on p
2.1 --- a/test/Tools/isac/Interpret/script.sml Fri Sep 23 09:41:11 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Sep 23 13:58:27 2011 +0200
2.3 @@ -6,12 +6,11 @@
2.4 "table of contents -----------------------------------------------";
2.5 "-----------------------------------------------------------------";
2.6 "----------- WN0509 why does next_tac doesnt find Substitute -----";
2.7 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.8 "----------- WN0509 Substitute 2nd part --------------------------";
2.9 "----------- fun sel_appl_atomic_tacs ----------------------------";
2.10 "----------- fun init_form, fun get_stac -------------------------";
2.11 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
2.12 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
2.13 +"----------- Take as 1st stac in script --------------------------";
2.14 "-----------------------------------------------------------------";
2.15 "-----------------------------------------------------------------";
2.16 "-----------------------------------------------------------------";
2.17 @@ -80,66 +79,6 @@
2.18 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
2.19 ---------------------------------------------------------------------*)
2.20
2.21 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.22 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.23 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
2.24 -(*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
2.25 -val fmz = ["Traegerlaenge L",
2.26 - "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
2.27 - "Biegelinie y",
2.28 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
2.29 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
2.30 - "FunktionsVariable x"];
2.31 -val (dI',pI',mI') =
2.32 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
2.33 - ["IntegrierenUndKonstanteBestimmen"]);
2.34 -val p = e_pos'; val c = [];
2.35 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.36 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.37 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.38 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.40 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.41 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.43 -
2.44 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
2.45 - | _ => error "script.sml, doesnt find Substitute #2";
2.46 -
2.47 -(*========== inhibit exn AK110721 ================================================
2.48 -
2.49 -(* AK110722 f2str f is NOT working anywhere - deprecated?????*)
2.50 -
2.51 -(*(* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.52 - (* ERROR: exception PTREE "get_obj: pos = [0] does not exist" raised
2.53 - (line 908 of "src/Tools/isac/Interpret/ctree.sml")*)*)
2.54 -(*f2str f;
2.55 - (* ERROR: exception Match raised (line 416 of "src/Tools/isac/Interpret/mathengine.sml")*)*)
2.56 -(* "~~~~~ fun f2str, args:"; val ((Form' (FormKF (_, _, _, _, cterm')))) = (f);
2.57 - (* ERROR: exception Bind raised *)*)
2.58 -
2.59 - f;
2.60 - f2str;*)
2.61 -
2.62 -(* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)
2.63 -(* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)
2.64 -
2.65 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.66 -(* *** generate1: not impl.for Empty_Tac_ !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)
2.67 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.68 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.69 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.70 -(*---------------------------------------------------------------------*)
2.71 -
2.72 -case nxt of (_, End_Proof') => ()
2.73 - | _ => error "script.sml, doesnt find Substitute #3";
2.74 -(*---------------------------------------------------------------------*)
2.75 -(*the reason, that next_tac didnt find the 2nd Substitute, was that
2.76 - the Take inbetween was missing, and thus the 2nd Substitute was applied
2.77 - the last formula in ctree, and not to argument from script*)
2.78 -========== inhibit exn AK110721 ================================================*)
2.79 -
2.80 -
2.81 "----------- WN0509 Substitute 2nd part --------------------------";
2.82 "----------- WN0509 Substitute 2nd part --------------------------";
2.83 "----------- WN0509 Substitute 2nd part --------------------------";
2.84 @@ -419,6 +358,58 @@
2.85 | _ => error "script.sml x+1=2 start SubProblem from script";
2.86
2.87
2.88 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
2.89 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
2.90 -"----------- x+1=2 set ctxt in Subproblem ------------------------";
2.91 +"----------- Take as 1st stac in script --------------------------";
2.92 +"----------- Take as 1st stac in script --------------------------";
2.93 +"----------- Take as 1st stac in script --------------------------";
2.94 +val p = e_pos'; val c = [];
2.95 +val (p,_,f,nxt,_,pt) =
2.96 + CalcTreeTEST
2.97 + [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
2.98 + ("Integrate", ["integrate","function"], ["diff","integration"]))];
2.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
2.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.102 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.103 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.104 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.105 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.106 +case nxt of (_, Apply_Method ["diff", "integration"]) => ()
2.107 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
2.108 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
2.109 +
2.110 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
2.111 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
2.112 +val (mI,m) = mk_tac'_ tac;
2.113 +val Appl m = applicable_in p pt m;
2.114 +member op = specsteps mI (*false*);
2.115 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
2.116 +"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
2.117 + (m, (pt, pos));
2.118 +val {srls, ...} = get_met mI;
2.119 + val PblObj {meth=itms, ...} = get_obj I pt p;
2.120 + val thy' = get_obj g_domID pt p;
2.121 + val thy = assoc_thy thy';
2.122 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
2.123 + val ini = init_form thy sc env;
2.124 + val p = lev_dn p;
2.125 +ini = NONE; (*true*)
2.126 + val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
2.127 + val d = e_rls (*FIXME: get simplifier from domID*);
2.128 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
2.129 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
2.130 + ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
2.131 +val thy = assoc_thy thy';
2.132 +l = [] orelse ((*init.in solve..Apply_Method...*)
2.133 + (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
2.134 +"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
2.135 + (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
2.136 + ((thy',ctxt,srls,d,Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
2.137 + (*check: true*) term2str e = "Take (Integral f_f D v_v)";
2.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) =
2.139 + (ya, ((E , l@[L,R], a,v,S,b),ss), e);
2.140 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
2.141 +(* val ctxt = get_ctxt pt (p,p_)
2.142 +exception PTREE "get_obj: pos = [0] does not exist" raised
2.143 +(line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
2.144 +
2.145 +
3.1 --- a/test/Tools/isac/Knowledge/integrate.sml Fri Sep 23 09:41:11 2011 +0200
3.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Fri Sep 23 13:58:27 2011 +0200
3.3 @@ -423,14 +423,11 @@
3.4 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
3.5 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
3.6 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
3.7 -
3.8 -(*========== inhibit exn 110719 ================================================
3.9 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.10 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.11 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.12 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
3.13 else error "integrate.sml -- me method [diff,integration] -- end";
3.14 -============ inhibit exn 110719 ==============================================*)
3.15
3.16
3.17 "----------- autoCalculate [diff,integration] -----------";
4.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Fri Sep 23 09:41:11 2011 +0200
4.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Fri Sep 23 13:58:27 2011 +0200
4.3 @@ -110,10 +110,13 @@
4.4 "----------- lin.eq degree_0 -------------------------------------";
4.5 "----------- lin.eq degree_0 -------------------------------------";
4.6 "----- d0_false ------";
4.7 -(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
4.8 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
4.9 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
4.10 ["PolyEq","solve_d0_polyeq_equation"]);
4.11 +(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
4.12 +TODO: change to "equality (x + -1*x = (0::real))"
4.13 + and search for an appropriate problem and method.
4.14 +
4.15 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.17 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.1 --- a/test/Tools/isac/Test_Some.thy Fri Sep 23 09:41:11 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Fri Sep 23 13:58:27 2011 +0200
5.3 @@ -7,135 +7,27 @@
5.4
5.5 theory Test_Some imports Isac begin
5.6
5.7 -use"../../../test/Tools/isac/Interpret/script.sml"
5.8 +use"../../../test/Tools/isac/Knowledge/integrate.sml"
5.9
5.10 ML {*
5.11 -"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
5.12 -(*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
5.13 -val fmz = ["Traegerlaenge L",
5.14 - "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
5.15 - "Biegelinie y",
5.16 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
5.17 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
5.18 - "FunktionsVariable x"];
5.19 -val (dI',pI',mI') =
5.20 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
5.21 - ["IntegrierenUndKonstanteBestimmen"]);
5.22 -val p = e_pos'; val c = [];
5.23 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.24 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.25 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.26 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.27 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.28 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.29 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.30 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.31 -
5.32 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
5.33 - | _ => error "script.sml, doesnt find Substitute #2";
5.34 -
5.35 -*}
5.36 -ML {*
5.37 -(*
5.38 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.39 -exception PTREE "get_obj: pos = [0] does not exist" raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
5.40 -*)
5.41 -*}
5.42 -ML {*
5.43 -"----------- me method [diff,integration] ---------------";
5.44 -"----------- me method [diff,integration] ---------------";
5.45 -"----------- me method [diff,integration] ---------------";
5.46 -(*exp_CalcInt_No-1.xml*)
5.47 -val p = e_pos'; val c = [];
5.48 -"----- step 0: returns nxt = Model_Problem ---";
5.49 -val (p,_,f,nxt,_,pt) =
5.50 - CalcTreeTEST
5.51 - [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
5.52 - ("Integrate", ["integrate","function"], ["diff","integration"]))];
5.53 -"----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
5.54 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
5.55 -"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
5.56 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.57 -"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
5.58 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.59 -"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
5.60 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.61 -"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
5.62 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.63 -"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
5.64 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.65 -"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
5.66 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.67 -case nxt of (_, Apply_Method ["diff", "integration"]) => ()
5.68 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
5.69 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
5.70 -
5.71 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
5.72 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
5.73 -val (mI,m) = mk_tac'_ tac;
5.74 -val Appl m = applicable_in p pt m;
5.75 -member op = specsteps mI (*false*);
5.76 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
5.77 -"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
5.78 - (m, (pt, pos));
5.79 -val {srls, ...} = get_met mI;
5.80 - val PblObj {meth=itms, ...} = get_obj I pt p;
5.81 - val thy' = get_obj g_domID pt p;
5.82 - val thy = assoc_thy thy';
5.83 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
5.84 - val ini = init_form thy sc env;
5.85 - val p = lev_dn p;
5.86 -ini = NONE; (*true*)
5.87 - val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
5.88 - val d = e_rls (*FIXME: get simplifier from domID*);
5.89 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
5.90 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
5.91 - ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
5.92 *}
5.93 ML {*
5.94 *}
5.95 ML {*
5.96 -val thy = assoc_thy thy';
5.97 -l = [] orelse ((*init.in solve..Apply_Method...*)
5.98 - (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
5.99 -"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
5.100 - (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
5.101 - (((ts,d),Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
5.102 -*}
5.103 -ML {*
5.104 -"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
5.105 - (ya, ((E , l@[L,R], a,v,S,b),ss), e);
5.106 -*}
5.107 -ML {*
5.108 -val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
5.109 -*}
5.110 -ML {*
5.111 -assod pt d m stac;
5.112 -print_depth 999;
5.113 -*}
5.114 -ML {*
5.115 -(*
5.116 - val ctxt = get_ctxt pt (p,p_)
5.117 -exception PTREE "get_obj: pos = [0] does not exist" raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
5.118 -*)
5.119 -*}
5.120 -ML {*
5.121 -lev_back (p,p_)
5.122 *}
5.123 ML {*
5.124 *}
5.125 ML {*
5.126 -
5.127 *}
5.128 ML {*
5.129 -
5.130 -*}
5.131 -ML{*
5.132 -*}
5.133 -ML{*
5.134 *}
5.135 ML {* (*=================*)
5.136 -
5.137 +*}
5.138 +ML {*
5.139 +*}
5.140 +ML {*
5.141 +*}
5.142 +ML {*
5.143 *}
5.144 ML{*
5.145 "~~~~~ fun , args:"; val () = ();