1.1 --- a/test/Tools/isac/Test_Some.thy Tue Mar 06 14:25:08 2012 +0100
1.2 +++ b/test/Tools/isac/Test_Some.thy Thu Mar 08 14:33:34 2012 +0100
1.3 @@ -1,50 +1,31 @@
1.4
1.5 theory Test_Some imports Isac begin
1.6
1.7 -use"../../../test/Tools/isac/Knowledge/biegelinie.sml"
1.8 +use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
1.9
1.10 ML {*
1.11 -val thy = @{theory "Biegelinie"};
1.12 *}
1.13 ML {*
1.14 -val ctxt = thy2ctxt' "Biegelinie";
1.15 *}
1.16 ML {*
1.17 -"----------- Bsp 7.27 me -----------------------------------------";
1.18 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.19 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.20 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.21 - "FunktionsVariable x"];
1.22 -val (dI',pI',mI') =
1.23 - ("Biegelinie",["MomentBestimmte","Biegelinien"],
1.24 - ["IntegrierenUndKonstanteBestimmen"]);
1.25 -val p = e_pos'; val c = [];
1.26 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.27 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.28 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.29 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.30 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.31 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.32 -
1.33 -val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
1.34 -(*if itms2str_ ctxt pits = ... all 5 model-items*)
1.35 -val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
1.36 -if itms2str_ ctxt mits = "[]" then ()
1.37 -else error "biegelinie.sml: Bsp 7.27 #2";
1.38 -
1.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.40 -case nxt of (_,Add_Given "FunktionsVariable x") => ()
1.41 - | _ => error "biegelinie.sml: Bsp 7.27 #4a";
1.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.43 +*}
1.44 +ML {*
1.45 *}
1.46 ML {*
1.47 -val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
1.48 *}
1.49 ML {*
1.50 -(*if itms2str_ ctxt mits = ... all 6 guard-items*)
1.51 -case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
1.52 - | _ => error "biegelinie.sml: Bsp 7.27 #4b";
1.53 -(*=========================^^^ correct until here ^^^===========================*)
1.54 +*}
1.55 +ML {* (*==================*)
1.56 +*}
1.57 +ML {*
1.58 +*}
1.59 +ML {*
1.60 +*}
1.61 +ML {*
1.62 +*}
1.63 +ML {*
1.64 +*}
1.65 +ML {* (*==================*)
1.66 *}
1.67 ML {*
1.68 *}
1.69 @@ -53,87 +34,12 @@
1.70 ML {*
1.71 *}
1.72 ML {*
1.73 -*}
1.74 -ML {*
1.75 -*}
1.76 -ML {*
1.77 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.78 -*}
1.79 -ML {*
1.80 -nxt
1.81 -*}
1.82 -ML {*
1.83 -print_depth 999;
1.84 -val ("Empty_Tac", xxx) = nxt; (*<<<-----------------------------------------------*)
1.85 -print_depth 999;
1.86 -*}
1.87 -ML {*
1.88 -*}
1.89 -ML {* (*==================*)
1.90 -"----------- Bsp 7.27 autoCalculate ------------------------------";
1.91 - states:=[];
1.92 - CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.93 - "RandbedingungenBiegung [y 0 = 0, y L = 0]",
1.94 - "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
1.95 - "FunktionsVariable x"],
1.96 - ("Biegelinie",
1.97 - ["MomentBestimmte","Biegelinien"],
1.98 - ["IntegrierenUndKonstanteBestimmen"]))];
1.99 - moveActiveRoot 1;
1.100 - autoCalculate 1 CompleteCalcHead;
1.101 -
1.102 - fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
1.103 -(*
1.104 -> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
1.105 -> is = e_scrstate;
1.106 -val it = true : bool
1.107 -*)
1.108 - autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
1.109 - val ((pt,_),_) = get_calc 1;
1.110 - case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
1.111 - | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
1.112 -
1.113 - autoCalculate 1 CompleteCalc;
1.114 -val ((pt,p),_) = get_calc 1;
1.115 -(*=== inhibit exn 110722=============================================================
1.116 -if p = ([], Res) andalso length (children pt) = 23 andalso
1.117 -term2str (get_obj g_res pt (fst p)) =
1.118 -"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
1.119 -then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.120 -=== inhibit exn 110722=============================================================*)
1.121 -
1.122 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.123 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.124 - show_pt pt;
1.125 -
1.126 -(*check all formulae for getTactic*)
1.127 - getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
1.128 - getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
1.129 - getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
1.130 - getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
1.131 - getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
1.132 - getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
1.133 -*}
1.134 -ML {*
1.135 -*}
1.136 -ML {*
1.137 -
1.138 -*}
1.139 -ML {*
1.140 -*}
1.141 -ML {* (*==================*)
1.142 -*}
1.143 -ML {*
1.144 -*}
1.145 -ML {*
1.146 "~~~~~ fun , args:"; val () = ();
1.147 *}
1.148 end
1.149
1.150 -
1.151 -(*============ inhibit exn WN120305 ==============================================
1.152 -============ inhibit exn WN120305 ==============================================*)
1.153 -
1.154 +(*============ inhibit exn WN120306 ==============================================
1.155 +============ inhibit exn WN120306 ==============================================*)
1.156
1.157 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.158 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)