1.1 --- a/src/sml/FE-interface/interface.sml Sun Oct 22 15:30:39 2006 +0200
1.2 +++ b/src/sml/FE-interface/interface.sml Thu Nov 02 10:56:09 2006 +0100
1.3 @@ -507,6 +507,7 @@
1.4 val (cI, ifo) = (1, "2+ -1 + x = 2");
1.5 val (cI, ifo) = (1, " x - ");
1.6 val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)");
1.7 + val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1");
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 Sun Oct 22 15:30:39 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Rational.ML Thu Nov 02 10:56:09 2006 +0100
2.3 @@ -3737,6 +3737,8 @@
2.4
2.5 (** methods **)
2.6
2.7 +(*WN061025 this methods script is copied from (auto-generated) script
2.8 + of norm_Rational in order to ease repair on inform*)
2.9 store_met
2.10 (prep_met Rational.thy "met_simp_rat" [] e_metID
2.11 (["simplification","of_rationals"],
2.12 @@ -3751,51 +3753,7 @@
2.13 [(*for preds in where_*)
2.14 Calc ("Rational.is'_ratpolyexp",
2.15 eval_is_ratpolyexp "")],
2.16 - crls = e_rls, nrls = e_rls},
2.17 - "Script SimplifyScript (t_::real) = \
2.18 - \ ((Rewrite_Set norm_Rational False) t_)"
2.19 - ));
2.20 -(**)
2.21 -store_met
2.22 - (prep_met Rational.thy "met_simp_rat" [] e_metID
2.23 - (["simplification","of_rationals"],
2.24 - [("#Given" ,["term t_"]),
2.25 - ("#Where" ,["t_ is_ratpolyexp"]),
2.26 - ("#Find" ,["normalform n_"])
2.27 - ],
2.28 - {rew_ord'="tless_true",
2.29 - rls' = e_rls,
2.30 - calc = [], srls = e_rls,
2.31 - prls = append_rls "simplification_of_rationals_prls" e_rls
2.32 - [(*for preds in where_*)
2.33 - Calc ("Rational.is'_ratpolyexp",
2.34 - eval_is_ratpolyexp "")],
2.35 - crls = e_rls, nrls = e_rls},
2.36 - "Script SimplifyScript (t_::real) = \
2.37 - \ ((Try (Rewrite_Set discard_minus_ False) @@ \
2.38 - \ Try (Rewrite_Set rat_mult_poly False) @@ \
2.39 - \ Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ \
2.40 - \ Try (Rewrite_Set cancel_p_rls False) @@ \
2.41 - \ Try (Rewrite_Set norm_Rational_rls False) @@ \
2.42 - \ Try (Rewrite_Set discard_parentheses_ False)) \
2.43 - \ t_)"
2.44 - ));
2.45 -(**)
2.46 -store_met
2.47 - (prep_met Rational.thy "met_simp_rat" [] e_metID
2.48 - (["simplification","of_rationals"],
2.49 - [("#Given" ,["term t_"]),
2.50 - ("#Where" ,["t_ is_ratpolyexp"]),
2.51 - ("#Find" ,["normalform n_"])
2.52 - ],
2.53 - {rew_ord'="tless_true",
2.54 - rls' = e_rls,
2.55 - calc = [], srls = e_rls,
2.56 - prls = append_rls "simplification_of_rationals_prls" e_rls
2.57 - [(*for preds in where_*)
2.58 - Calc ("Rational.is'_ratpolyexp",
2.59 - eval_is_ratpolyexp "")],
2.60 - crls = e_rls, nrls = e_rls},
2.61 + crls = e_rls, nrls = norm_Rational_rls},
2.62 "Script SimplifyScript (t_::real) = \
2.63 \ ((Try (Rewrite_Set discard_minus_ False) @@ \
2.64 \ Try (Rewrite_Set rat_mult_poly False) @@ \
3.1 --- a/src/sml/ME/inform.sml Sun Oct 22 15:30:39 2006 +0200
3.2 +++ b/src/sml/ME/inform.sml Thu Nov 02 10:56:09 2006 +0100
3.3 @@ -573,13 +573,18 @@
3.4
3.5 (*040214: version for concat_deriv*)
3.6 fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
3.7 -fun mk_tacis ro erls (t, r(*Thm (thmID, thm) only!*), (t', a)) =
3.8 +
3.9 +fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
3.10 (Rewrite (rule2thm' r),
3.11 Rewrite' ("Isac.thy", fst ro, erls, false,
3.12 rule2thm' r, t, (t', a)),
3.13 + (e_pos'(*to be updated before generate tacis!!!*), Uistate))
3.14 + | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
3.15 + (Rewrite_Set (rule2rls' r),
3.16 + Rewrite_Set' ("Isac.thy", false, rls, t, (t', a)),
3.17 (e_pos'(*to be updated before generate tacis!!!*), Uistate));
3.18
3.19 -(*fo = ifo excluded in inform*)
3.20 +(*fo = ifo excluded already in inform*)
3.21 fun concat_deriv rew_ord erls rules fo ifo =
3.22 let fun derivat ([]:(term * rule * (term * term list)) list) = e_term
3.23 | derivat dt = (#1 o #3 o last_elem) dt
3.24 @@ -677,6 +682,7 @@
3.25 (cs', encode ifo);
3.26 val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
3.27 (([],[],(pt,p)), (encode ifo));
3.28 + val ((cs as (_, _, ptp as (pt, pos as (p, p_)))), istr)=(cs', (encode ifo));
3.29 *)
3.30 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
3.31 case parse (assoc_thy "Isac.thy") istr of
4.1 --- a/src/sml/ME/script.sml Sun Oct 22 15:30:39 2006 +0200
4.2 +++ b/src/sml/ME/script.sml Thu Nov 02 10:56:09 2006 +0100
4.3 @@ -67,6 +67,8 @@
4.4
4.5 fun rule2thm' (Thm (id, thm)) = (id, string_of_thm thm):thm'
4.6 | rule2thm' r = raise error ("rule2thm': not defined for "^(rule2str r));
4.7 +fun rule2rls' (Rls_ rls) = id_rls rls
4.8 + | rule2rls' r = raise error ("rule2rls': not defined for "^(rule2str r));
4.9
4.10 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
4.11 complicated with current t in rrlsstate.*)
5.1 --- a/src/smltest/ME/inform.sml Sun Oct 22 15:30:39 2006 +0200
5.2 +++ b/src/smltest/ME/inform.sml Thu Nov 02 10:56:09 2006 +0100
5.3 @@ -480,6 +480,17 @@
5.4 "--- input the next formula that would be presented by mat-engine";
5.5 appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
5.6
5.7 +(*
5.8 +print_depth 9;
5.9 +print_depth 5; cs'; print_depth 3;
5.10 +val (_,_,(pptt,pp)) = cs';
5.11 +val tt = get_obj g_res pptt [4];
5.12 +term2str tt;
5.13 +
5.14 +(mk_tacis rew_ord erls) (nth 1 der);
5.15 +*)
5.16 +
5.17 +
5.18
5.19 "--- input the exact final result";(*TODO: Exception- LIST "last_elem" raised*)
5.20 appendFormula 1 "(-3 * x + 4 * y + -1 * x * y) / (x * y)";