1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Sep 22 14:43:47 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Sep 23 08:30:35 2011 +0200
1.3 @@ -976,8 +976,9 @@
1.4 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
1.5 (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
1.6 NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2
1.7 - | ay => (ay))
1.8 + | ay => (ay))
1.9
1.10 + (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
1.11 | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.12 (case handle_leaf "locate" thy' sr E a v t of
1.13 (a', Expr s) =>
1.14 @@ -1494,8 +1495,6 @@
1.15 20.8.02: do NOT return safe (is only changed in locate !!!)
1.16 *)
1.17 fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
1.18 - let val ctxt = get_ctxt pt p
1.19 - in
1.20 if f = f'
1.21 then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
1.22 (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
1.23 @@ -1506,12 +1505,9 @@
1.24 (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
1.25 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
1.26 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.27 - end
1.28
1.29 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Script (h $ body))
1.30 (ScrState (E,l,a,v,s,b), ctxt) =
1.31 - let val ctxt = get_ctxt pt pos (*WN110518 we have ctxt twice -- redesign*)
1.32 - in
1.33 (case if l = []
1.34 then appy thy ptp E [R] body NONE v
1.35 else nstep_up thy ptp sc E l Skip_ a v of
1.36 @@ -1527,7 +1523,6 @@
1.37 | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
1.38 | Appy (m', scrst as (_,_,_,v,_,_)) =>
1.39 (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
1.40 - end
1.41
1.42 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
1.43
2.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Sep 22 14:43:47 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve.sml Fri Sep 23 08:30:35 2011 +0200
2.3 @@ -164,7 +164,7 @@
2.4 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
2.5 val d = e_rls (*FIXME: get simplifier from domID*);
2.6 in
2.7 - case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
2.8 + case locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
2.9 Steps (is'', ss as (m'',f',pt',p',c')::_) =>
2.10 ("ok", (map step2taci ss, c', (pt',p')))
2.11 | NotLocatable =>
3.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Sep 22 14:43:47 2011 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Sep 23 08:30:35 2011 +0200
3.3 @@ -69,10 +69,12 @@
3.4 ],
3.5 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
3.6 crls = e_rls, nrls = e_rls},
3.7 - "Script InverseZTransform (Xeq::bool) =" ^
3.8 - " (let X = Take Xeq;" ^
3.9 - " X = Rewrite ruleZY False X" ^
3.10 - " in X)"
3.11 +"Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
3.12 +" (let X = Take X_eq;" ^
3.13 +" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
3.14 +" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
3.15 +" funterm = rhs X'" ^ (*drop X'= for equation solving*)
3.16 +" in X)"
3.17 ));
3.18 *}
3.19
4.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Sep 22 14:43:47 2011 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Sep 23 08:30:35 2011 +0200
4.3 @@ -493,39 +493,42 @@
4.4 *}
4.5
4.6
4.7 -subsection {*Stepwise Check the Program*}
4.8 -text {*At this section we got the error ME_Isa: thy 'Inverse_Z_Transform' not in system ?!?!?
4.9 - when working with "theory Inverse_Z_Transform imports Isac begin".
4.10 - Thus we switched to the present setting and separated Build_Inverse_Z_Transform.thy.
4.11 -*}
4.12 +subsection {*Check the Program*}
4.13
4.14 -subsubsection {*Check the formalization and start the program*}
4.15 -ML {*
4.16 -
4.17 -
4.18 -*}
4.19 +subsubsection {*Check the formalization*}
4.20 ML {*
4.21 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
4.22 "stepResponse (x[n::real]::bool)"];
4.23 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
4.24 ["SignalProcessing","Z_Transform","inverse"]);
4.25 +
4.26 +val ([(1, [1], "#Given", Const ("Inverse_Z_Transform.filterExpression", _),
4.27 + [Const ("HOL.eq", _) $ _ $ _]),
4.28 + (2, [1], "#Find", Const ("Inverse_Z_Transform.stepResponse", _),
4.29 + [Free ("x", _) $ _])],
4.30 + _) = prep_ori fmz thy ((#ppc o get_pbt) pI);
4.31 +*}
4.32 +
4.33 +subsubsection {*Stepwise check the program*}
4.34 +ML {*
4.35 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
4.36 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
4.37 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
4.38 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
4.39 + "stepResponse (x[n::real]::bool)"];
4.40 +val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
4.41 + ["SignalProcessing","Z_Transform","inverse"]);
4.42 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
4.43 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.44 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.45 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.46 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.47 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.48 *}
4.49 ML {*
4.50 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.51 *}
4.52 ML {*
4.53 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.54 -*}
4.55 -ML {*
4.56 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.57 -*}
4.58 -ML {*
4.59 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.60 -*}
4.61 -ML {*
4.62 -val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
4.63 *}
4.64 ML {*
4.65 (*
5.1 --- a/test/Tools/isac/CLEANUP Thu Sep 22 14:43:47 2011 +0200
5.2 +++ b/test/Tools/isac/CLEANUP Fri Sep 23 08:30:35 2011 +0200
5.3 @@ -9,13 +9,49 @@
5.4 rm .#*
5.5 rm *.tar*
5.6 rm *.orig
5.7 - cd file-depend
5.8 + cd course
5.9 + rm *~
5.10 + rm #*
5.11 + rm .#*
5.12 + rm *.tar*
5.13 + rm *.orig
5.14 + cd
5.15 + cd ml_quickstart
5.16 rm *~
5.17 rm #*
5.18 rm .#*
5.19 rm *.tar*
5.20 rm *.orig
5.21 cd ..
5.22 + cd phst11
5.23 + rm *~
5.24 + rm #*
5.25 + rm .#*
5.26 + rm *.tar*
5.27 + rm *.orig
5.28 + cd ..
5.29 + cd SignalProcess
5.30 + rm *~
5.31 + rm #*
5.32 + rm .#*
5.33 + rm *.tar*
5.34 + rm *.orig
5.35 + cd ..
5.36 + cd ..
5.37 + cd file-depend
5.38 + rm *~
5.39 + rm #*
5.40 + rm .#*
5.41 + rm *.tar*
5.42 + rm *.orig
5.43 + cd ..
5.44 + cd test-depend
5.45 + rm *~
5.46 + rm #*
5.47 + rm .#*
5.48 + rm *.tar*
5.49 + rm *.orig
5.50 + cd ..
5.51 cd ..
5.52 cd ProgLang
5.53 rm *~
6.1 --- a/test/Tools/isac/Interpret/script.sml Thu Sep 22 14:43:47 2011 +0200
6.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Sep 23 08:30:35 2011 +0200
6.3 @@ -6,6 +6,7 @@
6.4 "table of contents -----------------------------------------------";
6.5 "-----------------------------------------------------------------";
6.6 "----------- WN0509 why does next_tac doesnt find Substitute -----";
6.7 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
6.8 "----------- WN0509 Substitute 2nd part --------------------------";
6.9 "----------- fun sel_appl_atomic_tacs ----------------------------";
6.10 "----------- fun init_form, fun get_stac -------------------------";
6.11 @@ -16,6 +17,7 @@
6.12 "-----------------------------------------------------------------";
6.13
6.14 val thy= @{theory Isac};
6.15 +
6.16 "----------- WN0509 why does next_tac doesnt find Substitute -----";
6.17 "----------- WN0509 why does next_tac doesnt find Substitute -----";
6.18 "----------- WN0509 why does next_tac doesnt find Substitute -----";
6.19 @@ -78,19 +80,20 @@
6.20 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
6.21 ---------------------------------------------------------------------*)
6.22
6.23 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
6.24 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
6.25 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
6.26 +(*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
6.27 val fmz = ["Traegerlaenge L",
6.28 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
6.29 "Biegelinie y",
6.30 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
6.31 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
6.32 "FunktionsVariable x"];
6.33 -
6.34 val (dI',pI',mI') =
6.35 ("Biegelinie",["MomentBestimmte","Biegelinien"],
6.36 ["IntegrierenUndKonstanteBestimmen"]);
6.37 -
6.38 val p = e_pos'; val c = [];
6.39 -
6.40 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.41 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.42 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 22 14:43:47 2011 +0200
7.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Fri Sep 23 08:30:35 2011 +0200
7.3 @@ -393,6 +393,7 @@
7.4 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.5 atomty sc;
7.6 show_mets();
7.7 +===== inhibit exn ?===========================================================*)
7.8
7.9
7.10 "----------- me method [diff,integration] ---------------";
7.11 @@ -422,7 +423,6 @@
7.12 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
7.13 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
7.14 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
7.15 -===== inhibit exn ?===========================================================*)
7.16
7.17 (*========== inhibit exn 110719 ================================================
7.18 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
8.1 --- a/test/Tools/isac/Test_Some.thy Thu Sep 22 14:43:47 2011 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Fri Sep 23 08:30:35 2011 +0200
8.3 @@ -7,33 +7,136 @@
8.4
8.5 theory Test_Some imports Isac begin
8.6
8.7 -use"../../../test/Tools/isac/Interpret/mathengine.sml"
8.8 +use"../../../test/Tools/isac/Interpret/script.sml"
8.9
8.10 ML {*
8.11 +"----------- Apply_Method: exception PTREE get_obj: pos = [0] does";
8.12 +(*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*)
8.13 +val fmz = ["Traegerlaenge L",
8.14 + "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",
8.15 + "Biegelinie y",
8.16 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
8.17 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
8.18 + "FunktionsVariable x"];
8.19 +val (dI',pI',mI') =
8.20 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
8.21 + ["IntegrierenUndKonstanteBestimmen"]);
8.22 +val p = e_pos'; val c = [];
8.23 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
8.24 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.25 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.26 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.27 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.28 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.29 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.30 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.31 +
8.32 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
8.33 + | _ => error "script.sml, doesnt find Substitute #2";
8.34
8.35 *}
8.36 ML {*
8.37 -
8.38 +(*
8.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.40 +exception PTREE "get_obj: pos = [0] does not exist" raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
8.41 +*)
8.42 *}
8.43 ML {*
8.44 +"----------- me method [diff,integration] ---------------";
8.45 +"----------- me method [diff,integration] ---------------";
8.46 +"----------- me method [diff,integration] ---------------";
8.47 +(*exp_CalcInt_No-1.xml*)
8.48 +val p = e_pos'; val c = [];
8.49 +"----- step 0: returns nxt = Model_Problem ---";
8.50 +val (p,_,f,nxt,_,pt) =
8.51 + CalcTreeTEST
8.52 + [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
8.53 + ("Integrate", ["integrate","function"], ["diff","integration"]))];
8.54 +"----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
8.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
8.56 +"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
8.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.58 +"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
8.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.60 +"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
8.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.62 +"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
8.63 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.64 +"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
8.65 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.66 +"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
8.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.68 +case nxt of (_, Apply_Method ["diff", "integration"]) => ()
8.69 + | _ => error "integrate.sml -- me method [diff,integration] -- spec";
8.70 +"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
8.71
8.72 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
8.73 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.74 +val (mI,m) = mk_tac'_ tac;
8.75 +val Appl m = applicable_in p pt m;
8.76 +member op = specsteps mI (*false*);
8.77 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
8.78 +"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
8.79 + (m, (pt, pos));
8.80 +val {srls, ...} = get_met mI;
8.81 + val PblObj {meth=itms, ...} = get_obj I pt p;
8.82 + val thy' = get_obj g_domID pt p;
8.83 + val thy = assoc_thy thy';
8.84 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
8.85 + val ini = init_form thy sc env;
8.86 + val p = lev_dn p;
8.87 +ini = NONE; (*true*)
8.88 + val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
8.89 + val d = e_rls (*FIXME: get simplifier from domID*);
8.90 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
8.91 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
8.92 + ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
8.93 *}
8.94 ML {*
8.95 -
8.96 *}
8.97 ML {*
8.98 -
8.99 +val thy = assoc_thy thy';
8.100 +l = [] orelse ((*init.in solve..Apply_Method...*)
8.101 + (last_elem o fst) p = 0 andalso snd p = Res); (*true*)
8.102 +"~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss),
8.103 + (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
8.104 + (((ts,d),Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body);
8.105 *}
8.106 ML {*
8.107 -
8.108 +"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
8.109 + (ya, ((E , l@[L,R], a,v,S,b),ss), e);
8.110 *}
8.111 ML {*
8.112 -
8.113 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
8.114 *}
8.115 ML {*
8.116 -
8.117 +assod pt d m stac;
8.118 +print_depth 999;
8.119 *}
8.120 ML {*
8.121 +(*
8.122 + val ctxt = get_ctxt pt (p,p_)
8.123 +exception PTREE "get_obj: pos = [0] does not exist" raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
8.124 +*)
8.125 +*}
8.126 +ML {*
8.127 +lev_back (p,p_)
8.128 +*}
8.129 +ML {*
8.130 +*}
8.131 +ML {*
8.132 +(*
8.133 +assy ya ((E , l@[L,R], a,v,S,b),ss) e
8.134 +(assy ((ts,d),Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
8.135 +locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt')
8.136 +solve m (pt, pos);
8.137 +loc_solve_ (mI,m) ptp
8.138 +locatetac tac (pt,p)
8.139 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
8.140 +WAS exception PTREE "get_obj: pos = [0] does not exist"
8.141 +raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")
8.142 +*)
8.143 +
8.144
8.145 *}
8.146 ML {*