1.1 --- a/src/sml/FE-interface/interface.sml Mon Sep 25 16:55:17 2006 +0200
1.2 +++ b/src/sml/FE-interface/interface.sml Sat Sep 30 11:39:40 2006 +0200
1.3 @@ -506,6 +506,7 @@
1.4 val (cI, ifo) = (1, "x - 4711 = 0");
1.5 val (cI, ifo) = (1, "2+ -1 + x = 2");
1.6 val (cI, ifo) = (1, " x - ");
1.7 + val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)");
1.8 *)
1.9 fun appendFormula cI (ifo:cterm') =
1.10 (let val cs = get_calc cI
2.1 --- a/src/sml/IsacKnowledge/Rational.ML Mon Sep 25 16:55:17 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Rational.ML Sat Sep 30 11:39:40 2006 +0200
2.3 @@ -3755,6 +3755,61 @@
2.4 "Script SimplifyScript (t_::real) = \
2.5 \ ((Rewrite_Set norm_Rational False) t_)"
2.6 ));
2.7 +(**)
2.8 +store_met
2.9 + (prep_met Rational.thy "met_simp_rat" [] e_metID
2.10 + (["simplification","of_rationals"],
2.11 + [("#Given" ,["term t_"]),
2.12 + ("#Where" ,["t_ is_ratpolyexp"]),
2.13 + ("#Find" ,["normalform n_"])
2.14 + ],
2.15 + {rew_ord'="tless_true",
2.16 + rls' = e_rls,
2.17 + calc = [], srls = e_rls,
2.18 + prls = append_rls "simplification_of_rationals_prls" e_rls
2.19 + [(*for preds in where_*)
2.20 + Calc ("Rational.is'_ratpolyexp",
2.21 + eval_is_ratpolyexp "")],
2.22 + crls = e_rls, nrls = e_rls},
2.23 + "Script SimplifyScript (t_::real) = \
2.24 + \ ((Try (Rewrite_Set discard_minus_ False) @@ \
2.25 + \ Try (Rewrite_Set rat_mult_poly False) @@ \
2.26 + \ Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ \
2.27 + \ Try (Rewrite_Set cancel_p_rls False) @@ \
2.28 + \ Try (Rewrite_Set norm_Rational_rls False) @@ \
2.29 + \ Try (Rewrite_Set discard_parentheses_ False)) \
2.30 + \ t_)"
2.31 + ));
2.32 +(**)
2.33 +store_met
2.34 + (prep_met Rational.thy "met_simp_rat" [] e_metID
2.35 + (["simplification","of_rationals"],
2.36 + [("#Given" ,["term t_"]),
2.37 + ("#Where" ,["t_ is_ratpolyexp"]),
2.38 + ("#Find" ,["normalform n_"])
2.39 + ],
2.40 + {rew_ord'="tless_true",
2.41 + rls' = e_rls,
2.42 + calc = [], srls = e_rls,
2.43 + prls = append_rls "simplification_of_rationals_prls" e_rls
2.44 + [(*for preds in where_*)
2.45 + Calc ("Rational.is'_ratpolyexp",
2.46 + eval_is_ratpolyexp "")],
2.47 + crls = e_rls, nrls = e_rls},
2.48 +"Script SimplifyScript (t_::real) = \
2.49 +\ ((Try (Rewrite_Set discard_minus_ False) @@ \
2.50 +\ Try (Rewrite_Set rat_mult_poly False) @@ \
2.51 +\ Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ \
2.52 +\ Try (Rewrite_Set cancel_p_rls False) @@ \
2.53 +\ (Repeat \
2.54 +\ ((Try (Rewrite_Set common_nominator_p_rls False) @@ \
2.55 +\ Try (Rewrite_Set rat_mult_div_pow False) @@ \
2.56 +\ Try (Rewrite_Set make_rat_poly_with_parentheses False) @@\
2.57 +\ Try (Rewrite_Set cancel_p_rls False) @@ \
2.58 +\ Try (Rewrite_Set rat_reduce_1 False)))) @@ \
2.59 +\ Try (Rewrite_Set discard_parentheses_ False)) \
2.60 +\ t_)"
2.61 + ));
2.62
2.63 (* use"../IsacKnowledge/Rational.ML";
2.64 use"IsacKnowledge/Rational.ML";
3.1 --- a/src/sml/ME/inform.sml Mon Sep 25 16:55:17 2006 +0200
3.2 +++ b/src/sml/ME/inform.sml Sat Sep 30 11:39:40 2006 +0200
3.3 @@ -100,10 +100,10 @@
3.4
3.5 (***. handle an input calc-head .***)
3.6
3.7 -(*------------------------------------------------------------------*)
3.8 +(*------------------------------------------------------------------(**)
3.9 structure inform :INFORM =
3.10 struct
3.11 -(*------------------------------------------------------------------*)
3.12 +(**)------------------------------------------------------------------*)
3.13
3.14 datatype iitem =
3.15 Given of cterm' list
3.16 @@ -173,6 +173,8 @@
3.17
3.18 (*.check if the input term is a CAScmd and return a ptree with
3.19 a _complete_ calchead.*)
3.20 +(* val hdt =
3.21 + *)
3.22 fun cas_input hdt =
3.23 let val (h,argl) = strip_comb hdt
3.24 in case assoc (!castab, h) of
3.25 @@ -618,6 +620,10 @@
3.26 val it = () : unit
3.27 *)
3.28
3.29 +
3.30 +(*.compare inform with ctree.form at current pos by nrls;
3.31 + if found, embed the derivation generated during comparison
3.32 + if not, let the mat-engine compute the next ctree.form.*)
3.33 (*structure copied from complete_solve
3.34 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
3.35 all_modspec etc. has to be inserted at Subproblem'*)
3.36 @@ -674,6 +680,8 @@
3.37 *)
3.38 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
3.39 case parse (assoc_thy "Isac.thy") istr of
3.40 +(* val Some ifo = parse (assoc_thy "Isac.thy") istr;
3.41 + *)
3.42 Some ifo =>
3.43 let val ifo = term_of ifo
3.44 val fo = case p_ of Frm => get_obj g_form pt p
3.45 @@ -694,7 +702,7 @@
3.46 | None => ("syntax error in '"^istr^"'", e_calcstate');
3.47
3.48
3.49 -(*------------------------------------------------------------------*)
3.50 +(*------------------------------------------------------------------(**)
3.51 end
3.52 open inform;
3.53 -(*------------------------------------------------------------------*)
3.54 +(**)------------------------------------------------------------------*)
4.1 --- a/src/smltest/IsacKnowledge/rational.sml Mon Sep 25 16:55:17 2006 +0200
4.2 +++ b/src/smltest/IsacKnowledge/rational.sml Sat Sep 30 11:39:40 2006 +0200
4.3 @@ -1947,8 +1947,11 @@
4.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.6 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.7 -if f2str f = "14" then ()
4.8 -else raise error "rational.sml diff.behav. in me Schalk I No.186";
4.9 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
4.10 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
4.11 +case (f2str f, nxt) of
4.12 + ("14", ("End_Proof'", _)) => ()
4.13 + | _ => raise error "rational.sml diff.behav. in me Schalk I No.186";
4.14
4.15
4.16 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
4.17 @@ -1980,21 +1983,21 @@
4.18 moveActiveRoot 1;
4.19 autoCalculate 1 CompleteCalc;
4.20 val ((pt,p),_) = get_calc 1; show_pt pt;
4.21 -
4.22 +(*with explicit script done already... and removed [1,..] at below...
4.23 interSteps 1 ([1],Res);
4.24 val ((pt,p),_) = get_calc 1; show_pt pt;
4.25 -
4.26 -interSteps 1 ([1,2],Res);
4.27 +*)
4.28 +interSteps 1 ([2],Res);
4.29 val ((pt,p),_) = get_calc 1; show_pt pt;
4.30
4.31 -interSteps 1 ([1,2,1],Res);
4.32 +interSteps 1 ([2,1],Res);
4.33 val ((pt,p),_) = get_calc 1; show_pt pt;
4.34 -val newnds = children (get_nd pt [1,2,1]) (*see "fun detailrls"*);
4.35 +val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
4.36 (*if length newnds = 12 then () WN060905*)
4.37 if length newnds = 13 then ()
4.38 else raise error "rational.sml: interSteps cancel_p rev_rew_p";
4.39
4.40 -val p = ([1,2,1,9],Res);
4.41 +val p = ([2,1,9],Res);
4.42 getTactic 1 p;
4.43 val (_, tac, _) = pt_extract (pt, p);
4.44 (*case tac of Some (Rewrite ("sym_real_plus_binom_times1", _)) => ()
5.1 --- a/src/smltest/ME/inform.sml Mon Sep 25 16:55:17 2006 +0200
5.2 +++ b/src/smltest/ME/inform.sml Sat Sep 30 11:39:40 2006 +0200
5.3 @@ -28,6 +28,7 @@
5.4 "CAS-command:";
5.5 "--------- CAS-command on ([],Pbl) -------------------------------";
5.6 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
5.7 +"--------- inform [rational,simplification] ----------------------";
5.8 "-----------------------------------------------------------------";
5.9 "-----------------------------------------------------------------";
5.10 "-----------------------------------------------------------------";
5.11 @@ -463,3 +464,23 @@
5.12 else raise error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
5.13
5.14
5.15 +
5.16 +"--------- inform [rational,simplification] ----------------------";
5.17 +"--------- inform [rational,simplification] ----------------------";
5.18 +"--------- inform [rational,simplification] ----------------------";
5.19 +states:=[];
5.20 +CalcTree [(["term (4/x - 3/y - 1)", "normalform N"],
5.21 + ("Rational.thy",["rational","simplification"],
5.22 + ["simplification","of_rationals"]))];
5.23 +Iterator 1; moveActiveRoot 1;
5.24 +autoCalculate 1 CompleteCalcHead;
5.25 +autoCalculate 1 (Step 1);
5.26 +autoCalculate 1 (Step 1);
5.27 +autoCalculate 1 (Step 1);
5.28 +autoCalculate 1 (Step 1);
5.29 +"--- input the next formula that would be presented by mat-engine";
5.30 +appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
5.31 +
5.32 +
5.33 +"--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
5.34 +appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";
6.1 --- a/src/smltest/ME/solve.sml Mon Sep 25 16:55:17 2006 +0200
6.2 +++ b/src/smltest/ME/solve.sml Sat Sep 30 11:39:40 2006 +0200
6.3 @@ -46,6 +46,9 @@
6.4 moveActiveRoot 1;
6.5 autoCalculate 1 CompleteCalc;
6.6 val ((pt,_),_) = get_calc 1; show_pt pt;
6.7 +
6.8 +(*with "Script SimplifyScript (t_::real) = -----------------
6.9 + \ ((Rewrite_Set norm_Rational False) t_)"
6.10 case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
6.11 | _ => raise error "solve.sml: interSteps on norm_Rational 1";
6.12 interSteps 1 ([1], Res);
6.13 @@ -60,6 +63,26 @@
6.14
6.15 getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
6.16 interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
6.17 +--------------------------------------------------------------------*)
6.18 +
6.19 +case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
6.20 + | _ => raise error "solve.sml: interSteps on norm_Rational 1";
6.21 +(*these have been done now by the script ^^^ immediately...
6.22 +interSteps 1 ([1], Res);
6.23 +getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
6.24 +*)
6.25 +interSteps 1 ([6], Res);
6.26 +
6.27 +getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
6.28 +interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
6.29 +
6.30 +getTactic 1 ([3,4,1], Frm);
6.31 +val ((pt,_),_) = get_calc 1; show_pt pt;
6.32 +val (Form form, Some tac, asm) = pt_extract (pt, ([6], Res));
6.33 +case (term2str form, tac, terms2strs asm) of
6.34 + ("1 / 2", Check_Postcond ["rational", "simplification"],
6.35 + ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
6.36 + | _ => raise error "solve.sml: interSteps on norm_Rational 2";
6.37
6.38
6.39
7.1 --- a/src/smltest/Scripts/scrtools.sml Mon Sep 25 16:55:17 2006 +0200
7.2 +++ b/src/smltest/Scripts/scrtools.sml Sat Sep 30 11:39:40 2006 +0200
7.3 @@ -118,7 +118,40 @@
7.4 val Seq {scr = Script auto_script,...} = assoc_rls "norm_Rational";
7.5 writeln(term2str auto_script);
7.6 atomty auto_script;
7.7 -
7.8 +(***
7.9 +*** Const (Script.Stepwise, ['z, 'z] => 'z)
7.10 +*** . Free (t_, 'z)
7.11 +*** . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
7.12 +*** . . Const (Script.Try, ['a => 'a, 'a] => 'a)
7.13 +*** . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
7.14 +*** . . . . Free (discard_minus_, Script.ID)
7.15 +*** . . . . Const (False, bool)
7.16 +*** . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
7.17 +*** . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
7.18 +*** . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
7.19 +*** . . . . . Free (rat_mult_poly, Script.ID)
7.20 +*** . . . . . Const (False, bool)
7.21 +*** . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
7.22 +*** . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
7.23 +*** . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
7.24 +*** . . . . . . Free (make_rat_poly_with_parentheses, Script.ID)
7.25 +*** . . . . . . Const (False, bool)
7.26 +*** . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
7.27 +*** . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
7.28 +*** . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
7.29 +*** . . . . . . . Free (cancel_p_rls, Script.ID)
7.30 +*** . . . . . . . Const (False, bool)
7.31 +*** . . . . . Const (Script.Seq, ['a => 'a, 'a => 'a, 'a] => 'a)
7.32 +*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
7.33 +*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
7.34 +*** . . . . . . . . Free (norm_Rational_rls, Script.ID)
7.35 +*** . . . . . . . . Const (False, bool)
7.36 +*** . . . . . . Const (Script.Try, ['a => 'a, 'a] => 'a)
7.37 +*** . . . . . . . Const (Script.Rewrite'_Set, [Script.ID, bool, 'a] => 'a)
7.38 +*** . . . . . . . . Free (discard_parentheses_, Script.ID)
7.39 +*** . . . . . . . . Const (False, bool)
7.40 +*** . . Free (t_, 'a)
7.41 +***)
7.42 states:=[];
7.43 CalcTree
7.44 [(["term (b + a - b)", "normalform N"],
7.45 @@ -133,11 +166,12 @@
7.46
7.47 interSteps 1 ([1], Res);
7.48 val ((pt,p),_) = get_calc 1; show_pt pt;
7.49 -(*
7.50 -interSteps 1 ([1,2], Res);
7.51 -val ((pt,p),_) = get_calc 1; show_pt pt;
7.52 +
7.53 +(*with "Script SimplifyScript (t_::real) = \
7.54 + \ ((Rewrite_Set norm_Rational False) t_)"
7.55 +val (Form form, Some tac, asm) = pt_extract (pt, ([1], Res));
7.56 *)
7.57 -val (Form form, Some tac, asm) = pt_extract (pt, ([1], Res));
7.58 +val (Form form, Some tac, asm) = pt_extract (pt, ([2], Res));
7.59 case (term2str form, tac, terms2strs asm) of
7.60 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
7.61 | _ => raise error "scrtools.sml: auto-generated norm_Rational doesnt work";