1.1 --- a/src/sml/IsacKnowledge/Poly.ML Fri Jun 02 18:20:21 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Poly.ML Mon Jun 05 17:39:08 2006 +0200
1.3 @@ -1319,10 +1319,13 @@
1.4 ("reduce_012_mult_", prep_rls reduce_012_mult_),
1.5 ("collect_numerals_", prep_rls collect_numerals_),
1.6 ("reduce_012_", prep_rls reduce_012_),
1.7 - ("discard_parentheses_",prep_rls discard_parentheses_)
1.8 + ("discard_parentheses_",prep_rls discard_parentheses_),
1.9 + ("order_mult_rls_", prep_rls order_mult_rls_),
1.10 + ("order_add_rls_", prep_rls order_add_rls_)
1.11 (*("", prep_rls ),
1.12 ("", prep_rls ),
1.13 - ("", prep_rls ),*)
1.14 + ("", prep_rls )
1.15 + *)
1.16 ]);
1.17
1.18 calclist':= overwritel (!calclist',
2.1 --- a/src/sml/ME/generate.sml Fri Jun 02 18:20:21 2006 +0200
2.2 +++ b/src/sml/ME/generate.sml Mon Jun 05 17:39:08 2006 +0200
2.3 @@ -23,6 +23,8 @@
2.4 | Seq {srls=srls,scr=Script s,...} =>
2.5 (ScrState ([(one_scr_arg s, t)], [], None, e_term, Sundef, true)))
2.6 | init_istate (Rewrite_Set_Inst (subs, rls)) =
2.7 +(* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
2.8 + *)
2.9 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
2.10 in case assoc_rls rls of
2.11 Rls {scr=EmptyScr,...} =>
2.12 @@ -34,6 +36,8 @@
2.13 | Seq {scr=EmptyScr,...} =>
2.14 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
2.15 ^"use prep_rls for storing rule-sets !")
2.16 +(* val Seq {scr=Script s,...} = assoc_rls rls;
2.17 + *)
2.18 | Seq {scr=Script s,...} =>
2.19 let val (a1, a2) = two_scr_arg s
2.20 in (ScrState ([(a1, v), (a2, t)],[], None, e_term, Sundef,true)) end
3.1 --- a/src/sml/ME/mathengine.sml Fri Jun 02 18:20:21 2006 +0200
3.2 +++ b/src/sml/ME/mathengine.sml Mon Jun 05 17:39:08 2006 +0200
3.3 @@ -58,10 +58,10 @@
3.4
3.5
3.6
3.7 -(*------------------------------------------------------------------*)
3.8 +(*------------------------------------------------------------------(**)
3.9 structure MathEngine : MATHENGINE =
3.10 struct
3.11 -(*------------------------------------------------------------------*)
3.12 +(**)------------------------------------------------------------------*)
3.13
3.14 fun get_pblID (pt, (p,_):pos') =
3.15 let val p' = par_pblobj pt p
3.16 @@ -246,6 +246,8 @@
3.17 handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
3.18 of cs as ([],_,_) => ("helpless", cs)
3.19 | cs => ("ok", cs))
3.20 +(* val [] = tacis;
3.21 + *)
3.22 | _ => (case pIopt of
3.23 None => ("no-fmz-spec", ([], [], ptp))
3.24 | Some pI =>
3.25 @@ -461,8 +463,8 @@
3.26
3.27
3.28
3.29 -(*------------------------------------------------------------------*)
3.30 +(*------------------------------------------------------------------(**)
3.31 end
3.32 open MathEngine;
3.33 -(*------------------------------------------------------------------*)
3.34 +(**)------------------------------------------------------------------*)
3.35
4.1 --- a/src/sml/ME/solve.sml Fri Jun 02 18:20:21 2006 +0200
4.2 +++ b/src/sml/ME/solve.sml Mon Jun 05 17:39:08 2006 +0200
4.3 @@ -323,8 +323,7 @@
4.4 val (pos,c,_,pt) = (*implicit Take*)
4.5 generate1 thy tac_ is pos pt
4.6 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
4.7 - in ([(Apply_Method mI, tac_, (pos, is))],
4.8 - c, (pt, pos)):calcstate' end
4.9 + in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end
4.10 | None =>
4.11 let val pt = update_env pt (fst pos) (Some is)
4.12 val (tacis, c, ptp) = nxt_solve_ (pt, pos)
4.13 @@ -422,7 +421,7 @@
4.14 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
4.15 (* val (pt,pos as (p,p_)) = ptp;
4.16 val (pt,pos as (p,p_)) = ptp';
4.17 - val (pt,pos as (p,p_)) = ptp'';
4.18 + val (ptp as (pt, pos as (p,p_))) = ptp'';
4.19 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
4.20 *)
4.21 if e_metID = get_obj g_metID pt (par_pblobj pt p)
4.22 @@ -480,8 +479,6 @@
4.23 | ((End_Detail, _, _)::_, c', ptp') =>
4.24 if autoord auto < 6 then ("ok", c@c', ptp')
4.25 else complete_solve auto (c@c') ptp'
4.26 -(* val (_, c', ptp') = nxt_solve_ ptp;
4.27 - *)
4.28 | (_, c', ptp') => complete_solve auto (c@c') ptp'
4.29 (* val (tacis, c', ptp') = nxt_solve_ ptp;
4.30 val (tacis, c', ptp'') = nxt_solve_ ptp';
4.31 @@ -510,8 +507,9 @@
4.32 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
4.33 is wrong for simpl, but working ?!? *)
4.34 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
4.35 - Some t, is);
4.36 - val pos' = ((lev_on o lev_dn) p, Frm);
4.37 + Some t, is)
4.38 + val pos' = ((lev_on o lev_dn) p, Frm)
4.39 + val thy = assoc_thy "Isac.thy"
4.40 val (_,_,_,pt') = (*implicit Take*) generate1 thy tac_ is pos' pt;
4.41 val (_, _, (pt'',_)) = complete_solve CompleteSubpbl [] (pt', pos');
4.42 val newnds =children (get_nd pt'' p)
5.1 --- a/src/sml/ROOT.ML Fri Jun 02 18:20:21 2006 +0200
5.2 +++ b/src/sml/ROOT.ML Mon Jun 05 17:39:08 2006 +0200
5.3 @@ -120,6 +120,7 @@
5.4 use"calculate.sml";
5.5 use"reverse-rew.sml";
5.6 use"listg.sml";
5.7 + use"scrtools.sml";
5.8 cd "../..";
5.9 cd"smltest/ME";
5.10 use"calchead.sml";
6.1 --- a/src/sml/RTEST-root.sml Fri Jun 02 18:20:21 2006 +0200
6.2 +++ b/src/sml/RTEST-root.sml Mon Jun 05 17:39:08 2006 +0200
6.3 @@ -31,6 +31,7 @@
6.4 use"calculate.sml";
6.5 use"reverse-rew.sml";
6.6 use"listg.sml";
6.7 + use"scrtools.sml";
6.8 cd "../..";
6.9 cd"smltest/ME";
6.10 use"calchead.sml";
7.1 --- a/src/sml/Scripts/scrtools.sml Fri Jun 02 18:20:21 2006 +0200
7.2 +++ b/src/sml/Scripts/scrtools.sml Mon Jun 05 17:39:08 2006 +0200
7.3 @@ -151,7 +151,7 @@
7.4 fun one_scr_arg (Const _ $ arg $ _) = arg
7.5 | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));
7.6 fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
7.7 - | two_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));
7.8 + | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t));
7.9
7.10
7.11 (**.generate calc from a script.**)
7.12 @@ -326,7 +326,9 @@
7.13 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
7.14 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
7.15 \ (Try (Repeat (Rewrite real_mult_commute False)))) \
7.16 - \ t_)";
7.17 + \ t_)";
7.18 +(*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
7.19 +are inconsistent !!!*)
7.20 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
7.21 ((inst_abs thy) o term_of o the o (parse thy))
7.22 "Script Stepwise_inst (t_::'z) (v_::real) =\
8.1 --- a/src/sml/systest/ctree.sml Fri Jun 02 18:20:21 2006 +0200
8.2 +++ b/src/sml/systest/ctree.sml Mon Jun 05 17:39:08 2006 +0200
8.3 @@ -602,12 +602,11 @@
8.4 moveActiveDown 1;
8.5 moveActiveDown 1;
8.6 moveActiveDown 1;
8.7 - refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
8.8 + refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
8.9
8.10 interSteps 1 ([2],Res);
8.11
8.12 - val ((pt,_),_) = get_calc 1;
8.13 - show_pt pt;
8.14 + val ((pt,_),_) = get_calc 1; show_pt pt;
8.15 val p = get_pos 1 1;
8.16
8.17 val p = move_up [] pt p; (*([2, 6], Res)*);
9.1 --- a/src/smltest/IsacKnowledge/integrate.sml Fri Jun 02 18:20:21 2006 +0200
9.2 +++ b/src/smltest/IsacKnowledge/integrate.sml Mon Jun 05 17:39:08 2006 +0200
9.3 @@ -23,6 +23,7 @@
9.4 "----------- me method [Diff,integration] ------------------------";
9.5 "----------- me method [Diff,integration,named] ------------------";
9.6 "----------- me method [Diff,integration,named] Biegelinie.Q -----";
9.7 +"----------- interSteps [Diff,integration] -----------------------";
9.8 "-----------------------------------------------------------------";
9.9 "-----------------------------------------------------------------";
9.10 "-----------------------------------------------------------------";
9.11 @@ -427,6 +428,32 @@
9.12 if f2str f = "Q x = c + -1 * q_0 * x" then()
9.13 else raise error "integrate.sml: method [Diff,integration,named] .Q";
9.14
9.15 +
9.16 +"----------- interSteps [Diff,integration] -----------------------";
9.17 +"----------- interSteps [Diff,integration] -----------------------";
9.18 +"----------- interSteps [Diff,integration] -----------------------";
9.19 +states:=[];
9.20 +CalcTree
9.21 +[(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
9.22 + ("Integrate.thy",["integrate","function"],
9.23 + ["Diff","integration"]))];
9.24 +Iterator 1;
9.25 +moveActiveRoot 1;
9.26 +autoCalculate 1 CompleteCalc;
9.27 +val ((pt,p),_) = get_calc 1; show_pt pt;
9.28 +
9.29 +interSteps 1 ([1],Res);
9.30 +(*...lead to
9.31 +*** one_scr_arg: called by Script Stepwise t_ =
9.32 +*** (Try (Rewrite_Set integration_rules False) @@
9.33 +*** Try (Rewrite_Set add_new_c False) @@
9.34 +*** Try (Rewrite_Set simplify_Integral False))
9.35 +*** t_
9.36 +
9.37 +TODO.WN060605 postponed until general decision how to model bound variables*)
9.38 +
9.39 +
9.40 +
9.41 (*
9.42 use"../smltest/IsacKnowledge/integrate.sml";
9.43 *)
10.1 --- a/src/smltest/IsacKnowledge/poly.sml Fri Jun 02 18:20:21 2006 +0200
10.2 +++ b/src/smltest/IsacKnowledge/poly.sml Mon Jun 05 17:39:08 2006 +0200
10.3 @@ -17,7 +17,6 @@
10.4 "-------- Script 'simplification for_polynomials' ----------------";
10.5 "-------- check pbl 'polynomial simplification' -----------------";
10.6 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
10.7 -"-------- interSteps for Schalk 299a -----------------------------";
10.8 "-----------------------------------------------------------------";
10.9 "-----------------------------------------------------------------";
10.10 "-----------------------------------------------------------------";
10.11 @@ -394,7 +393,9 @@
10.12 autoCalculate 1 CompleteCalc;
10.13 val ((pt,p),_) = get_calc 1; show_pt pt;
10.14
10.15 -interSteps 1 ([1],Res);
10.16 +interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
10.17 +val ((pt,p),_) = get_calc 1; show_pt pt;
10.18 (*
10.19 -writeln(istate2str is);
10.20 +if existpt' ([1,1], Frm) pt then ()
10.21 +else raise error "poly.sml: interSteps doesnt work again";
10.22 *)
10.23 \ No newline at end of file
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/smltest/Scripts/scrtools.sml Mon Jun 05 17:39:08 2006 +0200
11.3 @@ -0,0 +1,127 @@
11.4 +(* tests on tools for scripts
11.5 + author: Walther Neuper
11.6 + 060605,
11.7 + (c) due to copyright terms
11.8 +
11.9 +use"../smltest/Scripts/scrtools.sml";
11.10 +use"scrtools.sml";
11.11 +*)
11.12 +"-----------------------------------------------------------------";
11.13 +"table of contents -----------------------------------------------";
11.14 +"-----------------------------------------------------------------";
11.15 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
11.16 +"-------- test the same called by interSteps norm_Poly -----------";
11.17 +"-------- test the same called by interSteps norm_Rational -------";
11.18 +"-----------------------------------------------------------------";
11.19 +"-----------------------------------------------------------------";
11.20 +"-----------------------------------------------------------------";
11.21 +
11.22 +
11.23 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
11.24 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
11.25 +"-------- test auto-generated script '(Repeat (Calculate times))'-";
11.26 +val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
11.27 +writeln(term2str auto_script);
11.28 +atomty auto_script;
11.29 +
11.30 +store_met
11.31 + (prep_met Test.thy
11.32 + (["Test","test_interSteps_1"]:metID,
11.33 + [("#Given" ,["term t_"]),
11.34 + ("#Find" ,["normalform n_"])
11.35 + ],
11.36 + {rew_ord'="dummy_ord",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
11.37 + crls=tval_rls, nrls=e_rls},
11.38 +"Script Stepwise t_ = \
11.39 + \(Try (Rewrite_Set discard_minus_ False) @@ \
11.40 + \ Try (Rewrite_Set expand_poly_ False) @@ \
11.41 + \ Try (Repeat (Calculate times)) @@ \
11.42 + \ Try (Rewrite_Set order_mult_rls_ False) @@ \
11.43 + \ Try (Rewrite_Set simplify_power_ False) @@ \
11.44 + \ Try (Rewrite_Set calc_add_mult_pow_ False) @@\
11.45 + \ Try (Rewrite_Set reduce_012_mult_ False) @@ \
11.46 + \ Try (Rewrite_Set order_add_rls_ False) @@ \
11.47 + \ Try (Rewrite_Set collect_numerals_ False) @@ \
11.48 + \ Try (Rewrite_Set reduce_012_ False) @@ \
11.49 + \ Try (Rewrite_Set discard_parentheses_ False))\
11.50 + \ t_"
11.51 +(*presently this script cannot become equal in types to auto_script, because:
11.52 + this t_ must be either 'real' or 'bool' #1#,
11.53 + while the auto_script must be 'z and type-instantiated before usage*)
11.54 + ));
11.55 +show_mets();
11.56 +val {scr = Script s2,...} = get_met ["Test","test_interSteps_1"];
11.57 +s = s2; term2str s = term2str s2;
11.58 +atomty s;
11.59 +atomty s2;
11.60 +
11.61 +(*because of #1# the following test is useless...*)
11.62 +states:=[];
11.63 +CalcTree
11.64 +[(["term (b + a - b)",(*this is Schalk 299b*)
11.65 + "normalform N"],
11.66 + ("Poly.thy",["polynomial","simplification"],
11.67 + ["Test","test_interSteps_1"]))];
11.68 +Iterator 1;
11.69 +moveActiveRoot 1;
11.70 +autoCalculate 1 CompleteCalcHead;
11.71 +
11.72 +fetchProposedTactic 1 (*..Apply_Method*);
11.73 +autoCalculate 1 (Step 1);
11.74 +getFormulaeFromTo 1 ([], Frm) ([1], Frm) 000 false (*implicit Take*);
11.75 +getTactic 1 ([1], Frm) (*still empty*);
11.76 +
11.77 +autoCalculate 1 (Step 1);
11.78 +getFormulaeFromTo 1 ([1], Frm) ([1], Res) 000 false;
11.79 +getTactic 1 ([1], Frm) (*discard_minus_*);
11.80 +
11.81 +autoCalculate 1 CompleteCalc;
11.82 +
11.83 +val ((pt,p),_) = get_calc 1; show_pt pt;
11.84 +(*
11.85 +if existpt' ([1], Frm) pt then ()
11.86 +else raise error "scrtools.sml: auto-generated script doesnt work";
11.87 +*)
11.88 +
11.89 +"-------- test the same called by interSteps norm_Poly -----------";
11.90 +"-------- test the same called by interSteps norm_Poly -----------";
11.91 +"-------- test the same called by interSteps norm_Poly -----------";
11.92 +val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
11.93 +writeln(term2str auto_script);
11.94 +atomty auto_script;
11.95 +states:=[];
11.96 +CalcTree
11.97 +[(["term (b + a - b)", "normalform N"],
11.98 + ("Poly.thy",["polynomial","simplification"],
11.99 + ["simplification","for_polynomials"]))];
11.100 +Iterator 1;
11.101 +moveActiveRoot 1;
11.102 +autoCalculate 1 CompleteCalc;
11.103 +
11.104 +interSteps 1 ([], Res);
11.105 +val ((pt,p),_) = get_calc 1; show_pt pt;
11.106 +
11.107 +interSteps 1 ([1], Res);
11.108 +
11.109 +"-------- test the same called by interSteps norm_Rational -------";
11.110 +"-------- test the same called by interSteps norm_Rational -------";
11.111 +"-------- test the same called by interSteps norm_Rational -------";
11.112 +val Rls {scr = Script auto_script,...} = assoc_rls "norm_Rational";
11.113 +writeln(term2str auto_script);
11.114 +atomty auto_script;
11.115 +
11.116 +states:=[];
11.117 +CalcTree
11.118 +[(["term (b + a - b)", "normalform N"],
11.119 + ("Poly.thy",["polynomial","simplification"],
11.120 + ["simplification","of_rationals"]))];
11.121 +Iterator 1;
11.122 +moveActiveRoot 1;
11.123 +autoCalculate 1 CompleteCalc;
11.124 +
11.125 +interSteps 1 ([], Res);
11.126 +val ((pt,p),_) = get_calc 1; show_pt pt;
11.127 +
11.128 +interSteps 1 ([1], Res);
11.129 +val ((pt,p),_) = get_calc 1; show_pt pt;
11.130 +