work on "sym_thm ... [.]"
1.1 --- a/src/sml/ME/calchead.sml Thu Nov 02 17:16:17 2006 +0100
1.2 +++ b/src/sml/ME/calchead.sml Thu Nov 02 19:19:09 2006 +0100
1.3 @@ -645,12 +645,14 @@
1.4 (dI,pI,mI) specification explicitly done by the user
1.5 (pbt, mpc) problem type, guard of method
1.6 .*)
1.7 -(*12.8.03:######### Refine_Problem' -> Specify_Problem'*)
1.8 +(* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.9 + val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI);
1.10 + val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
1.11 + (p_, pb, oris, (dI',pI',mI'), (probl,meth),
1.12 + (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
1.13 + *)
1.14 fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec)
1.15 ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) =
1.16 -(* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.17 - val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI);
1.18 - *)
1.19 ((*writeln"### nxt_spec Pbl";*)
1.20 if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI')
1.21 else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI')
1.22 @@ -685,6 +687,9 @@
1.23 ((*Solv 3.4.00*)Met, Apply_Method mI))))
1.24 (* val preok=pb; val (pbl, met) = (pbl,met');
1.25 val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.26 + val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
1.27 + (p_, pb, oris, (dI',pI',mI'), (probl,meth),
1.28 + (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
1.29 *)
1.30 | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
1.31 ((*writeln"### nxt_spec Met"; *)
2.1 --- a/src/sml/ME/mathengine.sml Thu Nov 02 17:16:17 2006 +0100
2.2 +++ b/src/sml/ME/mathengine.sml Thu Nov 02 19:19:09 2006 +0100
2.3 @@ -228,9 +228,9 @@
2.4 calcstate
2.5 .*)
2.6 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
2.7 - val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
2.8 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);
2.9 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
2.10 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
2.11 *)
2.12 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
2.13 let val pIopt = get_pblID (pt,ip);
2.14 @@ -278,8 +278,7 @@
2.15 at the fron-end in 05:
2.16 eg. CompleteCalcHead could be done by a separate fun !!!*)
2.17 (* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
2.18 -
2.19 - (*1*)val (c, ip, cs as (ptp as (_,p),tacis), Step s) =
2.20 + val (c, ip, cs as (ptp as (_,p),tacis), Step s) =
2.21 ([]:pos' list, pold, get_calc cI, auto);
2.22 *)
2.23 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
3.1 --- a/src/sml/ME/script.sml Thu Nov 02 17:16:17 2006 +0100
3.2 +++ b/src/sml/ME/script.sml Thu Nov 02 19:19:09 2006 +0100
3.3 @@ -1867,8 +1867,7 @@
3.4 (id, string_of_thm' thm), f,(e_term,[(*!?!8.6.03*)])),
3.5 Uistate, (e_term, Sundef))) (*next stac*)
3.6
3.7 -(*
3.8 - val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
3.9 +(* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
3.10 ((thy',srls), (pt,pos), sc, is);
3.11 *)
3.12 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
4.1 --- a/src/sml/ME/solve.sml Thu Nov 02 17:16:17 2006 +0100
4.2 +++ b/src/sml/ME/solve.sml Thu Nov 02 19:19:09 2006 +0100
4.3 @@ -420,9 +420,9 @@
4.4 (*.find the next tac from the script, nxt_solv will update the ptree.*)
4.5 (* val (ptp as (pt,pos as (p,p_))) = ptp';
4.6 val (ptp as (pt, pos as (p,p_))) = ptp'';
4.7 - val (ptp as (pt, pos as (p,p_))) = (pt,ip);
4.8 val (ptp as (pt, pos as (p,p_))) = (pt, pos);
4.9 val (ptp as (pt, pos as (p,p_))) = ptp;
4.10 + val (ptp as (pt, pos as (p,p_))) = (pt,ip);
4.11 *)
4.12 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
4.13 if e_metID = get_obj g_metID pt (par_pblobj pt p)
5.1 --- a/src/sml/ROOT.ML Thu Nov 02 17:16:17 2006 +0100
5.2 +++ b/src/sml/ROOT.ML Thu Nov 02 19:19:09 2006 +0100
5.3 @@ -115,7 +115,6 @@
5.4 cd"smltest/Scripts";
5.5 use"calculate-float.sml";
5.6 use"calculate.sml";
5.7 - use"reverse-rew.sml";
5.8 use"listg.sml";
5.9 use"scrtools.sml";
5.10 cd "../..";
6.1 --- a/src/sml/RTEST-root.sml Thu Nov 02 17:16:17 2006 +0100
6.2 +++ b/src/sml/RTEST-root.sml Thu Nov 02 19:19:09 2006 +0100
6.3 @@ -28,7 +28,6 @@
6.4 cd"smltest/Scripts";
6.5 use"calculate-float.sml";
6.6 use"calculate.sml";
6.7 - use"reverse-rew.sml";
6.8 use"listg.sml";
6.9 use"scrtools.sml";
6.10 cd "../..";
7.1 --- a/src/smltest/ME/rewtools.sml Thu Nov 02 17:16:17 2006 +0100
7.2 +++ b/src/smltest/ME/rewtools.sml Thu Nov 02 19:19:09 2006 +0100
7.3 @@ -22,6 +22,7 @@
7.4 "----------- fun guh2theID ---------------------------------------";
7.5 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
7.6 "-----------------------------------------------------------------";
7.7 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.8 "-----------------------------------------------------------------";
7.9 "-----------------------------------------------------------------";
7.10
7.11 @@ -428,3 +429,36 @@
7.12 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
7.13
7.14
7.15 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.16 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.17 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.18 +"----- these work";
7.19 +val th = sym_thm real_minus_eq_cancel;
7.20 +val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
7.21 +val th' = mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
7.22 +
7.23 +"----- but this generates [.]";
7.24 +states:=[];
7.25 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
7.26 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
7.27 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
7.28 + "FunktionsVariable x"],
7.29 + ("Biegelinie.thy",
7.30 + ["MomentBestimmte","Biegelinien"],
7.31 + ["IntegrierenUndKonstanteBestimmen"]))];
7.32 +moveActiveRoot 1;
7.33 +autoCalculate 1 CompleteCalcHead;
7.34 +autoCalculate 1 (Step 1) (*Apply_Method*);
7.35 +"--- this is still ok, when called in next_tac";
7.36 +val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
7.37 +val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
7.38 + applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
7.39 +
7.40 +autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
7.41 +"--- but this is already corrupted";
7.42 +val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
7.43 +get_obj g_tac pt p;
7.44 +
7.45 +
7.46 +
7.47 +getTactic 1 ([1],Frm);
8.1 --- a/src/smltest/Scripts/reverse-rew.sml Thu Nov 02 17:16:17 2006 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,29 +0,0 @@
8.4 -(* tests related to sml/Scripts/reverse-rew.sml
8.5 - author: Walther Neuper 060514
8.6 - (c) due to copyright terms
8.7 -
8.8 -use"../smltest/Scripts/reverse-rew.sml";
8.9 -use"reverse-rew.sml";
8.10 -*)
8.11 -"-----------------------------------------------------------------";
8.12 -"table of contents -----------------------------------------------";
8.13 -"-----------------------------------------------------------------";
8.14 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
8.15 -"-----------------------------------------------------------------";
8.16 -"-----------------------------------------------------------------";
8.17 -"-----------------------------------------------------------------";
8.18 -
8.19 -
8.20 -
8.21 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
8.22 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
8.23 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
8.24 -(*WN060514 we got
8.25 - Rewrite ("sym_real_minus_eq_cancel",
8.26 - "(?b1 = ?a1) = (- ?b1 = - ?a1) [.]")
8.27 -where this is too much in the string ~~~~~ for parsing !
8.28 -*)
8.29 -(*
8.30 ---- Bsp 7.27 autoCalculate --- in systest/../biegelinie.sml
8.31 - getTactic 1 ([1],Frm);
8.32 -*)
8.33 \ No newline at end of file