1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Dec 07 16:25:49 2011 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Dec 08 23:37:50 2011 +0100
1.3 @@ -69,14 +69,16 @@
1.4 *}
1.5
1.6 ML {*
1.7 -(*("factors_from_solution", ("Partial_Fractions.factors_from_solution", eval_factors_from_solution ""))*)
1.8 -fun eval_factors_from_solution (thmid:string) _ t thy =
1.9 - (let val prod = factors_from_solution t
1.10 - in SOME (mk_thmid thmid ""
1.11 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
1.12 - Trueprop $ (mk_equality (t, prod)))
1.13 - end)
1.14 - handle _ => NONE;
1.15 +(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
1.16 +fun eval_factors_from_solution (thmid:string) _
1.17 + (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
1.18 + ((let val prod = factors_from_solution sol
1.19 + in SOME (mk_thmid thmid ""
1.20 + (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
1.21 + Trueprop $ (mk_equality (t, prod)))
1.22 + end)
1.23 + handle _ => NONE)
1.24 + | eval_factors_from_solution _ _ _ _ = NONE;
1.25 *}
1.26
1.27
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Dec 07 16:25:49 2011 +0100
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Dec 08 23:37:50 2011 +0100
2.3 @@ -331,14 +331,106 @@
2.4 # done 02.12.2011 moved to PartialFractions.thy
2.5 *}
2.6 ML {*
2.7 -(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
2.8 -fun eval_factors_from_solution (thmid:string) _ t thy =
2.9 - (let val prod = factors_from_solution t
2.10 - in SOME (mk_thmid thmid ""
2.11 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
2.12 - Trueprop $ (mk_equality (t, prod)))
2.13 - end)
2.14 - handle _ => NONE;
2.15 +(*("factors_from_solution", ("Partial_Fractions.factors_from_solution", eval_factors_from_solution ""))*)
2.16 +fun eval_factors_from_solution (thmid:string) _
2.17 + (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
2.18 + ((let val prod = factors_from_solution sol
2.19 + in SOME (mk_thmid thmid ""
2.20 + (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "",
2.21 + Trueprop $ (mk_equality (t, prod)))
2.22 + end)
2.23 + handle _ => NONE)
2.24 + | eval_factors_from_solution _ _ _ _ = NONE;
2.25 +*}
2.26 +
2.27 +text {*
2.28 +The tracing output of the calc tree after apllying this function was
2.29 +24 / factors_from_solution [z = 1/ 2, z = -1 / 4])] and the next step
2.30 + val nxt = ("Empty_Tac", ...): tac'_).
2.31 +These observations indicate, that the Lucas-Interpreter (LIP) does
2.32 +not know how to evaluate factors_from_solution, so there is something
2.33 +wrong or missing.
2.34 +
2.35 +# First we isolate the difficulty in the program as follows:
2.36 + :
2.37 + " (L_L::bool list) = (SubProblem (PolyEq'," ^
2.38 + " [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
2.39 + " [BOOL equ, REAL zzz]); " ^
2.40 + " (facs::real) = factors_from_solution L_L;" ^
2.41 + " (foo::real) = Take facs" ^
2.42 + :
2.43 +and see
2.44 + [
2.45 + (([], Frm), Problem (Isac, [inverse, Z_Transform, SignalProcessing])),
2.46 + (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
2.47 + (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
2.48 + (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
2.49 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
2.50 + (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
2.51 + (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
2.52 + z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
2.53 + (([3,2], Res), z = 1 / 2 | z = -1 / 4),
2.54 + (([3,3], Res), [z = 1 / 2, z = -1 / 4]),
2.55 + (([3,4], Res), [z = 1 / 2, z = -1 / 4]),
2.56 + (([3], Res), [z = 1 / 2, z = -1 / 4]),
2.57 + (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]
2.58 +in particular that
2.59 + (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
2.60 +shows the equation which has been created in the program by
2.61 + " (denom::real) = get_denominator funterm;" ^ (*get_denominator*)
2.62 + " (equ::bool) = (denom = (0::real));" ^
2.63 +# 'get_denominator' has been evaluated successfully, but not factors_from_solution.
2.64 +So we stepwise compare with an analogous case, get_denominator
2.65 +successfully done above: We know that LIP evaluates expressions in the
2.66 +program by use of the "srls", so we
2.67 +# try to get the original srls
2.68 +
2.69 + val {srls, ...} = get_met ["SignalProcessing","Z_Transform","inverse"];
2.70 +
2.71 +# create 2 good example terms
2.72 + val SOME t1 = parseNEW ctxt "get_denominator ((111::real) / 222)";
2.73 + val SOME t2 = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
2.74 +
2.75 +# rewrite the terms using srls
2.76 + rewrite_set_ thy true srls t1;
2.77 + rewrite_set_ thy true srls t2;
2.78 +
2.79 +and we see a difference: t1 gives SOME, t2 gives NONE.
2.80 +Now we look at the srls:
2.81 + val srls = Rls {id="srls_InverseZTransform",
2.82 + :
2.83 + rules =
2.84 + [
2.85 + :
2.86 + Calc("Rational.get_numerator",
2.87 + eval_get_numerator "Rational.get_numerator"),
2.88 + Calc("Partial_Fractions.factors_from_solution",
2.89 + eval_factors_from_solution "Partial_Fractions.factors_from_solution")
2.90 + ],
2.91 + :
2.92 +
2.93 +Here everthing is perfect. So the error can only be in the SML code of eval_factors_from_solution.
2.94 +We try to check the code with an existing test; since the code is in
2.95 +
2.96 + src/Tools/isac/Knowledge/Partial_Fractions.thy
2.97 +
2.98 +the test should be in
2.99 +
2.100 + test/Tools/isac/Knowledge/partial_fractions.sml
2.101 +
2.102 +-------------------------------------------------------------------------------
2.103 +After updating the function get_factors_from solution to a new version and
2.104 +putting a testcase to Partial_Fractions.sml we tried again to evaluate the
2.105 +term with the same result.
2.106 +We opened the test Test_Isac.thy and saw that everything is working fine.
2.107 +Also we checked that the test partial_fractions.sml is used in Test_Isac.thy
2.108 +
2.109 +--> use "Knowledge/partial_fractions.sml"
2.110 +
2.111 +and Partial_Fractions.thy is part is part of isac by evaluating
2.112 +
2.113 +val thy = @{theory Isac};
2.114 +
2.115 *}
2.116
2.117 subsubsection {*build expression*}
3.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Wed Dec 07 16:25:49 2011 +0100
3.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 08 23:37:50 2011 +0100
3.3 @@ -6,6 +6,8 @@
3.4 "--------------------------------------------------------";
3.5 "table of contents --------------------------------------";
3.6 "--------------------------------------------------------";
3.7 +"----------- Test of function factors_from_solution ---------";
3.8 +"--------------------------------------------------------";
3.9 "----------- why helpless here ? ------------------------";
3.10 "----------- why not nxt = Model_Problem here ? ---------";
3.11 "--------------------------------------------------------";
3.12 @@ -64,3 +66,14 @@
3.13 See TODO.txt
3.14 *)
3.15
3.16 +"----------- Test of function factors_from_solution ---------";
3.17 +"----------- Test of function factors_from_solution ---------";
3.18 +"----------- Test of function factors_from_solution ---------";
3.19 +
3.20 +val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
3.21 +val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
3.22 +if term2str t' =
3.23 + "factors_from_solution [z = 1 / 2, z = -1 / 4] =\n(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
3.24 +then () else error "factors_from_solution broken";
3.25 +
3.26 +