1.1 --- a/src/sml/FE-interface/interface.sml Mon May 08 17:06:31 2006 +0200
1.2 +++ b/src/sml/FE-interface/interface.sml Wed May 10 17:24:51 2006 +0200
1.3 @@ -297,6 +297,7 @@
1.4
1.5
1.6 (* val (cI, iI) = (1,1);
1.7 + val (cI, ip) = (1, ([1,3], Res));
1.8 *)
1.9 fun interSteps cI (*iI*) ip =
1.10 let val ((pt,p), tacis) = get_calc cI
2.1 --- a/src/sml/IsacKnowledge/Atools.ML Mon May 08 17:06:31 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Atools.ML Wed May 10 17:24:51 2006 +0200
2.3 @@ -386,11 +386,12 @@
2.4 [("list_rls",list_rls)
2.5 ]);
2.6
2.7 -(*TODO.WN0509 remove double names: tless_true = e_rew_ord' = e_rew_ord*)
2.8 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
2.9 val tless_true = dummy_ord;
2.10 rew_ord' := overwritel (!rew_ord',
2.11 [("tless_true", tless_true),
2.12 - ("e_rew_ord'", tless_true)]);
2.13 + ("e_rew_ord'", tless_true),
2.14 + ("dummy_ord", dummy_ord)]);
2.15
2.16 val calculate_Atools =
2.17 append_rls "calculate_Atools" e_rls
3.1 --- a/src/sml/IsacKnowledge/Poly.ML Mon May 08 17:06:31 2006 +0200
3.2 +++ b/src/sml/IsacKnowledge/Poly.ML Wed May 10 17:24:51 2006 +0200
3.3 @@ -329,7 +329,7 @@
3.4 ]);
3.5
3.6
3.7 -val expand =
3.8 +val expand = prep_rls(
3.9 Rls{id = "expand", preconds = [],
3.10 rew_ord = ("dummy_ord", dummy_ord),
3.11 erls = e_rls,srls = Erls,
3.12 @@ -339,13 +339,13 @@
3.13 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
3.14 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2)
3.15 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
3.16 - ], scr = EmptyScr}:rls;
3.17 + ], scr = EmptyScr}:rls);
3.18
3.19 (*----------------- Begin: rulesets for make_polynomial_ -----------------
3.20 'rlsIDs' redefined by MG as 'rlsIDs_'
3.21 ^^^*)
3.22
3.23 -val discard_minus_ =
3.24 +val discard_minus_ = prep_rls(
3.25 Rls{id = "discard_minus_", preconds = [],
3.26 rew_ord = ("dummy_ord", dummy_ord),
3.27 erls = e_rls,srls = Erls,
3.28 @@ -355,8 +355,8 @@
3.29 (*"a - b = a + -1 * b"*)
3.30 Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
3.31 (*- ?z = "-1 * ?z"*)
3.32 - ], scr = EmptyScr}:rls;
3.33 -val expand_poly_ =
3.34 + ], scr = EmptyScr}:rls);
3.35 +val expand_poly_ = prep_rls(
3.36 Rls{id = "expand_poly_", preconds = [],
3.37 rew_ord = ("dummy_ord", dummy_ord),
3.38 erls = e_rls,srls = Erls,
3.39 @@ -384,7 +384,7 @@
3.40 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
3.41 Thm ("realpow_pow",num_str realpow_pow)
3.42 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
3.43 - ], scr = EmptyScr}:rls;
3.44 + ], scr = EmptyScr}:rls);
3.45
3.46 (*.the expression contains + - * ^ only ?
3.47 this is weaker than 'is_polynomial' !.*)
3.48 @@ -1302,6 +1302,7 @@
3.49 ruleset' := overwritelthy thy (!ruleset',
3.50 [("norm_Poly", norm_Poly),
3.51 ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*),
3.52 + ("expand", expand),
3.53 ("expand_poly", expand_poly),
3.54 ("simplify_power", simplify_power),
3.55 ("order_add_mult", order_add_mult),
4.1 --- a/src/sml/ME/generate.sml Mon May 08 17:06:31 2006 +0200
4.2 +++ b/src/sml/ME/generate.sml Wed May 10 17:24:51 2006 +0200
4.3 @@ -1,22 +1,37 @@
4.4 (* use"ME/generate.sml";
4.5 use"generate.sml";
4.6 *)
4.7 +
4.8 +(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
4.9 + *)
4.10 (*.initialize istate for Detail_Set.*)
4.11 fun init_istate (Rewrite_Set rls) =
4.12 (case assoc_rls rls of
4.13 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
4.14 + | Rls {scr=EmptyScr,...} =>
4.15 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.16 + ^"use prep_rls for storing rule-sets !")
4.17 | Rls {scr=Script s,...} =>
4.18 (* val Rls {scr=Script s,...} = assoc_rls rls;
4.19 *)
4.20 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true))
4.21 + | Seq {scr=EmptyScr,...} =>
4.22 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.23 + ^"use prep_rls for storing rule-sets !")
4.24 | Seq {srls=srls,scr=Script s,...} =>
4.25 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true)))
4.26 | init_istate (Rewrite_Set_Inst (subs, rls)) =
4.27 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
4.28 in case assoc_rls rls of
4.29 - Rls {scr=Script s,...} =>
4.30 + Rls {scr=EmptyScr,...} =>
4.31 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.32 + ^"use prep_rls for storing rule-sets !")
4.33 + | Rls {scr=Script s,...} =>
4.34 let val (a1, a2) = two_scr_arg s
4.35 in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end
4.36 + | Seq {scr=EmptyScr,...} =>
4.37 + raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
4.38 + ^"use prep_rls for storing rule-sets !")
4.39 | Seq {scr=Script s,...} =>
4.40 let val (a1, a2) = two_scr_arg s
4.41 in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end
5.1 --- a/src/sml/ME/mathengine.sml Mon May 08 17:06:31 2006 +0200
5.2 +++ b/src/sml/ME/mathengine.sml Wed May 10 17:24:51 2006 +0200
5.3 @@ -368,6 +368,7 @@
5.4 end;
5.5
5.6 (* val pos as (p,p_) = ip;
5.7 + val (pt, (pos as (p,p_):pos')) = (pt, ip);
5.8 *)
5.9 fun detailstep pt (pos as (p,p_):pos') =
5.10 let val nd = get_nd pt p
6.1 --- a/src/sml/ME/solve.sml Mon May 08 17:06:31 2006 +0200
6.2 +++ b/src/sml/ME/solve.sml Wed May 10 17:24:51 2006 +0200
6.3 @@ -499,11 +499,11 @@
6.4
6.5 (*. detail steps done internally by Rewrite_Set*
6.6 into ctree by use of a script .*)
6.7 -(* val (p,p_) = pos;
6.8 +(* val (pt, (p,p_)) = (pt, pos);
6.9 *)
6.10 fun detailrls pt ((p,p_):pos') =
6.11 let val t = get_obj g_form pt p
6.12 - val is = init_istate (get_obj g_tac pt p)
6.13 + val is = init_istate (get_obj g_tac pt p)
6.14 val tac_ = Apply_Method' (e_metID(*WN.0402: see generate1 !?!*),
6.15 Some t, is);
6.16 val pos' = ((lev_on o lev_dn) p, Frm);
7.1 --- a/src/sml/ROOT.ML Mon May 08 17:06:31 2006 +0200
7.2 +++ b/src/sml/ROOT.ML Wed May 10 17:24:51 2006 +0200
7.3 @@ -212,6 +212,7 @@
7.4 -----------------------------------------------------------------------------
7.5 su
7.6 cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux
7.7 + rm HOL-Real-Isac
7.8 cp HOL-Real HOL-Real-Isac
7.9 /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
7.10 cd"/home/neuper/proto2/isac/src/sml";
7.11 @@ -226,6 +227,7 @@
7.12
7.13 ssh ist
7.14 cd /usr/local/Isabelle2002/heaps/polyml-4.1.3_x86-linux/
7.15 + rm HOL-Real-Isac
7.16 cp HOL-Real HOL-Real-Isac
7.17 cd ~/del_graz/sml
7.18 /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
8.1 --- a/src/smltest/ME/solve.sml Mon May 08 17:06:31 2006 +0200
8.2 +++ b/src/smltest/ME/solve.sml Wed May 10 17:24:51 2006 +0200
8.3 @@ -1,31 +1,63 @@
8.4 -(* use"../systest/details.sml";
8.5 - use"systest/details.sml";
8.6 - use"details.sml";
8.7 +(* tests on solve.sml
8.8 + author: Walther Neuper
8.9 + 060508,
8.10 + (c) due to copyright terms
8.11
8.12 -########################################################
8.13 is NOT ONLY dependent on Test, but on other thys:
8.14 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8.15 uses from Rational.ML: Rrls cancel_p, Rrls cancel
8.16 which in turn
8.17 uses from Poly.ML: Rls make_polynomial, Rls expand_binom
8.18 -########################################################
8.19 +
8.20 +use"../smltest/ME/solve.sml";
8.21 +use"solve.sml";
8.22 *)
8.23 +
8.24 +"-----------------------------------------------------------------";
8.25 +"table of contents -----------------------------------------------";
8.26 +"-----------------------------------------------------------------";
8.27 +"--------- interSteps on norm_Rational ---------------------------";
8.28 (*---vvv NOT working after meNEW.04mmdd*)
8.29 +"--------- prepare pbl, met --------------------------------------";
8.30 "-------- cancel, without detail ------------------------------";
8.31 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
8.32 "-------------- cancel_p, without detail ------------------------------";
8.33 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
8.34 (*---^^^ NOT working*)
8.35 -
8.36 "on 'miniscript with mini-subpbl':";
8.37 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
8.38 "------ interSteps'detailrls' after CompleteCalc -----------------";
8.39 -
8.40 (*---vvv not brought to work 0403*)
8.41 "------ Detail_Set -----------------------------------------------";
8.42 +"-----------------------------------------------------------------";
8.43 +"-----------------------------------------------------------------";
8.44 +"-----------------------------------------------------------------";
8.45
8.46
8.47 +"--------- interSteps on norm_Rational ---------------------------";
8.48 +"--------- interSteps on norm_Rational ---------------------------";
8.49 +"--------- interSteps on norm_Rational ---------------------------";
8.50 +states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
8.51 +CalcTree [(["term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
8.52 + ("Rational.thy",
8.53 + ["rational","simplification"],
8.54 + ["simplification","of_rationals"]))];
8.55 +moveActiveRoot 1;
8.56 +autoCalculate 1 CompleteCalc;
8.57 +val ((pt,_),_) = get_calc 1;
8.58 +show_pt pt;
8.59 +case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
8.60 + | _ => raise error "solve.sml: interSteps on norm_Rational 1";
8.61 +interSteps 1 ([1], Res);
8.62 +getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
8.63 +interSteps 1 ([1,3], Res);
8.64 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
8.65
8.66 +
8.67 +
8.68 +"--------- prepare pbl, met --------------------------------------";
8.69 +"--------- prepare pbl, met --------------------------------------";
8.70 +"--------- prepare pbl, met --------------------------------------";
8.71 store_pbt
8.72 (prep_pbt Test.thy
8.73 (["test"],