1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Tue Sep 28 13:30:29 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri Oct 01 10:23:38 2010 +0200
1.3 @@ -802,11 +802,11 @@
1.4 | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
1.5 | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
1.6
1.7 -fun show_ptyps () = (tracing o format_pblIDl o (scan [])) (!ptyps);
1.8 +fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);
1.9 (* ptyps:=[];
1.10 show_ptyps();
1.11 *)
1.12 -fun show_mets () = (tracing o format_pblIDl o (scan [])) (!mets);
1.13 +fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);
1.14
1.15
1.16
2.1 --- a/src/Tools/isac/Knowledge/Delete.thy Tue Sep 28 13:30:29 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Fri Oct 01 10:23:38 2010 +0200
2.3 @@ -12,6 +12,8 @@
2.4 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
2.5 real_mult_minus1: "-1 * z = - (z::real)"
2.6 real_mult_2: "2 * z = z + (z::real)"
2.7 + real_diff_0: "0 - x = - (x::real)"
2.8 +
2.9
2.10 ML {*
2.11 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var:
3.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Sep 28 13:30:29 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Oct 01 10:23:38 2010 +0200
3.3 @@ -1346,15 +1346,18 @@
3.4 val order_mult_ =
3.5 Rrls {id = "order_mult_",
3.6 prepat =
3.7 + (* ?p matched with the current term gives an environment,
3.8 + which evaluates (the instantiated) "p is_multUnordered" to true*)
3.9 [([(term_of o the o (parse thy)) "p is_multUnordered"],
3.10 - parse_patt thy "?p" )],
3.11 + parse_patt thy "?p :: real" )],
3.12 rew_ord = ("dummy_ord", dummy_ord),
3.13 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
3.14 [Calc ("Poly.is'_multUnordered",
3.15 eval_is_multUnordered "")],
3.16 - calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")),
3.17 - ("TIMES" , ("Groups.times_class.times" , eval_binop "#mult_")),
3.18 - ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
3.19 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
3.20 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
3.21 + ("DIVIDE", ("Rings.inverse_class.divide",
3.22 + eval_cancel "#divide_e")),
3.23 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
3.24 scr=Rfuns {init_state = init_state,
3.25 normal_form = normal_form,
4.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 13:30:29 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Oct 01 10:23:38 2010 +0200
4.3 @@ -166,6 +166,10 @@
4.4
4.5 functions for greatest common divisor and canceling
4.6 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.7 +################################################################################
4.8 +## search Isabelle2009-2/src/HOL/Multivariate_Analysis
4.9 +## Amine Chaieb, Robert Himmelmann, John Harrison.
4.10 +################################################################################
4.11 mv_gcd
4.12 factout_
4.13 factout_p_
4.14 @@ -3070,6 +3074,10 @@
4.15 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
4.16 []:(rule * (term * term list)) list;
4.17
4.18 +(* pat matched with the current term gives an environment
4.19 + (or not: hen the Rrls not applied);
4.20 + if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
4.21 + then the Rrls is applied. *)
4.22 val pat = parse_patt thy "?r/?s";
4.23 val pre1 = parse_patt thy "?r is_expanded";
4.24 val pre2 = parse_patt thy "?s is_expanded";
4.25 @@ -3218,13 +3226,14 @@
4.26 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
4.27 []:(rule * (term * term list)) list;
4.28
4.29 +(* if each pat* matches with the current term, the Rrls is applied
4.30 + (there are no preconditions to be checked, they are HOLogic.true_const) *)
4.31 val pat0 = parse_patt thy "?r/?s+?u/?v";
4.32 val pat1 = parse_patt thy "?r/?s+?u ";
4.33 val pat2 = parse_patt thy "?r +?u/?v";
4.34 val prepat = [([HOLogic.true_const], pat0),
4.35 ([HOLogic.true_const], pat1),
4.36 ([HOLogic.true_const], pat2)];
4.37 -
4.38 in
4.39
4.40 (*11.02 schnelle L"osung f"ur RL: Bruch auch gek"urzt;
4.41 @@ -3362,6 +3371,8 @@
4.42 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
4.43 []:(rule * (term * term list)) list;
4.44
4.45 +(* if each pat* matches with the current term, the Rrls is applied
4.46 + (there are no preconditions to be checked, they are HOLogic.true_const) *)
4.47 val pat0 = parse_patt thy "?r/?s+?u/?v";
4.48 val pat01 = parse_patt thy "?r/?s-?u/?v";
4.49 val pat1 = parse_patt thy "?r/?s+?u ";
5.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 13:30:29 2010 +0200
5.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 10:23:38 2010 +0200
5.3 @@ -79,7 +79,8 @@
5.4 end)
5.5 (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
5.6 and eval__true thy i asms bdv rls =
5.7 - if asms = [HOLogic.true_const] orelse asms = [] then ([], true)
5.8 + if asms = [HOLogic.true_const] orelse asms = [] then ([], true)
5.9 + (* this allows to check Rrls with prepat = ([HOLogic.true_const], pat) *)
5.10 else if asms = [HOLogic.false_const] then ([], false)
5.11 else let
5.12 fun chk indets [] = (indets, true)(*return asms<>True until false*)
5.13 @@ -96,7 +97,7 @@
5.14 (* rewrite with a rule set, which must not be the empty Erls *)
5.15 and rewrite__set_ _ _ __ Erls t =
5.16 error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
5.17 - (* rewrite with a 'reverse rule set' based on ML code *)
5.18 + (* rewrite with a 'reverse rule set' implemented by ML code *)
5.19 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
5.20 let val _= if ! trace_rewrite andalso i < ! depth
5.21 then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
5.22 @@ -182,13 +183,17 @@
5.23 in if ct = ct' then NONE else SOME (ct', distinct asm') end
5.24
5.25 and app_rev thy i rrls t =
5.26 - let (*.check a (precond, pattern) of a rev-set; stops with 1st true.*)
5.27 + let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
5.28 fun chk_prepat thy erls [] t = true
5.29 | chk_prepat thy erls prepat t =
5.30 let fun chk (pres, pat) =
5.31 (let val subst: Type.tyenv * Envir.tenv =
5.32 Pattern.match thy (pat, t)
5.33 (Vartab.empty, Vartab.empty)
5.34 + val _ = tracing ("app_rev: pres=------------------");
5.35 + val _ = tracing ("app_rev: pres=" ^ terms2str pres);
5.36 + val _ = tracing ("app_rev: pat =" ^ term2str pat);
5.37 + val _ = tracing ("app_rev: t =" ^ term2str t);
5.38 in snd (eval__true thy (i+1)
5.39 (map (Envir.subst_term subst) pres)
5.40 [] erls)
5.41 @@ -199,7 +204,7 @@
5.42 else scan_ f pps;
5.43 in scan_ chk prepat end;
5.44
5.45 - (*.apply the normal_form of a rev-set.*)
5.46 + (* apply the normal_form of a rev-set *)
5.47 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
5.48 if chk_prepat thy erls prepat t
5.49 then ((*tracing("### app_rev': t = "^(term2str t));*)
6.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 13:30:29 2010 +0200
6.2 +++ b/src/Tools/isac/ProgLang/termC.sml Fri Oct 01 10:23:38 2010 +0200
6.3 @@ -1124,8 +1124,18 @@
6.4 *** Free ( R, RealDef.real)
6.5 *** Free ( R, RealDef.real) *)
6.6
6.7 +(*fun parse_patt thy str =
6.8 +(**** prep_pbt: syntax error in '#Where' of ["equation"]
6.9 +*** Exception- TOPLEVEL_ERROR raised
6.10 +*** At command "ML" (line 172 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Poly.thy").*)
6.11 + (typ_a2real o numbers_to_string o
6.12 + ProofContext.read_term_pattern (thy2ctxt thy)) str;*)
6.13 fun parse_patt thy str =
6.14 - ProofContext.read_term_pattern (thy2ctxt thy) str;
6.15 + ProofContext.read_term_pattern (thy2ctxt thy) str;
6.16 +(*fun parse_patt thy str = (thy, str) |>> thy2ctxt
6.17 + |-> ProofContext.read_term_pattern
6.18 + |> numbers_to_string
6.19 + |> typ_a2real;*)
6.20
6.21 (*version for testing local to theories*)
6.22 fun str2term_ thy str = (term_of o the o (parse thy)) str;
7.1 --- a/src/Tools/isac/Test_Isac.thy Tue Sep 28 13:30:29 2010 +0200
7.2 +++ b/src/Tools/isac/Test_Isac.thy Fri Oct 01 10:23:38 2010 +0200
7.3 @@ -9,7 +9,7 @@
7.4 10 20 30 40 50 60 70 80
7.5 *)
7.6
7.7 -theory Test_Isac imports Isac begin
7.8 +theory Test_Isac imports "Knowledge/Isac" begin
7.9
7.10 ML{* writeln "**** run the tests **************************************" *};
7.11 ML {* Toplevel.debug := true; *}
7.12 @@ -31,18 +31,21 @@
7.13 cd"smltest/Scripts";
7.14 *)
7.15 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
7.16 -
7.17 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
7.18
7.19 -use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*part.*)
7.20 +ML {*print_depth 999;*}
7.21 +use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)
7.22 (*
7.23 use"listg.sml";
7.24 use"scrtools.sml";
7.25 use"tools.sml";
7.26 cd "../..";
7.27 cd"smltest/ME";
7.28 - use"ctree.sml";
7.29 *)
7.30 +use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)
7.31 +(* use"ctree.sml";
7.32 +*)
7.33 +use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*)
7.34 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
7.35 (*
7.36 use"calchead.sml";
7.37 @@ -63,36 +66,45 @@
7.38 *)
7.39 ML{* writeln "**** run tests on math-engine complete ******************" *};
7.40 (*
7.41 -cd"smltest/IsacKnowledge";
7.42 +cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
7.43 use"atools.sml";
7.44 - use"complex.sml";
7.45 + use"termorder.sml";
7.46 +*)
7.47 +
7.48 +ML {*
7.49 +val t = str2term "(x^^^2 * x) is_multUnordered";
7.50 +val pat = parse_patt (theory "Isac") "?p is_multUnordered";
7.51 +*}
7.52 +ML {*
7.53 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
7.54 +Envir.subst_term subst (*pres?*);
7.55 +*}
7.56 +use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
7.57 +(*
7.58 + use"rational.sml"
7.59 + use"equation.sml";
7.60 + use"root.sml";
7.61 + (*use"inssort.sml"; problems with recdef in Isabelle2002*)
7.62 + use"rooteq.sml";
7.63 + use"rateq.sml";
7.64 + use"rootrateq.sml";
7.65 +
7.66 + use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
7.67 + ? also check others without check 'diff.behav.'*);
7.68 + use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
7.69 + for simplification search MG
7.70 + erls: 98a(1) 104a(1) 104a(2) 68a *);
7.71 + use"wn.sml";
7.72 + use"trig.sml";
7.73 + use"logexp.sml";
7.74 use"diff.sml";
7.75 - use"diffapp.sml";
7.76 *)
7.77 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
7.78 (*
7.79 - use"equation.sml";
7.80 - (*use"inssort.sml"; problems with recdef in Isabelle2002*)
7.81 - use"logexp.sml";
7.82 -*)
7.83 -use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
7.84 -(*
7.85 + use"eqsystem.sml";
7.86 use"polyminus.sml";
7.87 - use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
7.88 - ? also check others without check 'diff.behav.'*);
7.89 - use"rateq.sml";
7.90 - use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
7.91 - use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
7.92 - for simplification search MG
7.93 - erls: 98a(1) 104a(1) 104a(2) 68a *);
7.94 - use"root.sml";
7.95 - use"rooteq.sml";
7.96 - use"rootrateq.sml";
7.97 - use"termorder.sml";
7.98 - use"trig.sml";
7.99 use"vect.sml";
7.100 - use"wn.sml";
7.101 - use"eqsystem.sml";
7.102 + use"diffapp.sml";
7.103 use"biegelinie.sml";
7.104 use"algein.sml";
7.105 cd "../..";
8.1 --- a/src/Tools/isac/calcelems.sml Tue Sep 28 13:30:29 2010 +0200
8.2 +++ b/src/Tools/isac/calcelems.sml Fri Oct 01 10:23:38 2010 +0200
8.3 @@ -117,17 +117,16 @@
8.4 difference: there is always _ONE_ redex rewritten in 1 call,
8.5 thus wrap Rrls by: Rls (Rls_ ...)*)
8.6
8.7 - | Rrls of (*for 'reverse rewriting' by SML-functions instead Script*)
8.8 - {id : string, (*for trace_rewrite:=true *)
8.9 - prepat : (term list *(*preconds, eval with subst from pattern *)
8.10 - term ) (*pattern matched in subterms *)
8.11 - list, (*meta-conjunction is or *)
8.12 - rew_ord : rew_ord, (*for rules *)
8.13 - erls : rls, (*for the conditions in rules and pat *)
8.14 - (* '^ because of rewrite in applicable_in
8.15 - compare type met*)
8.16 - calc : calc list, (*for Calculate in scr, set by prep_rls *)
8.17 - scr : scr}; (*Rfuns {...} (how to restrict type ???)*)
8.18 + | Rrls of (* for 'reverse rewriting' by SML-functions instead Script *)
8.19 + {id : string, (* for trace_rewrite := true *)
8.20 + prepat : (term list *(* preconds, eval with subst from pattern;
8.21 + if [HOLogic.true_const], match decides alone *)
8.22 + term ) (* pattern matched with current (sub)term *)
8.23 + list, (* meta-conjunction is or *)
8.24 + rew_ord : rew_ord, (* for rules *)
8.25 + erls : rls, (* for the conditions in rules and preconds *)
8.26 + calc : calc list, (* for Calculate in scr, set automatic.in prep_rls *)
8.27 + scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
8.28 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
8.29 from rls, and then contain both Script _AND_ Rfuns !!!*)
8.30
9.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue Sep 28 13:30:29 2010 +0200
9.2 +++ b/test/Tools/isac/Interpret/calchead.sml Fri Oct 01 10:23:38 2010 +0200
9.3 @@ -1,6 +1,5 @@
9.4 -(* tests on calchead.sml
9.5 - author: Walther Neuper
9.6 - 051013,
9.7 +(* Title: tests on calchead.sml
9.8 + Author: Walther Neuper 051013,
9.9 (c) due to copyright terms
9.10
9.11 12345678901234567890123456789012345678901234567890123456789012345678901234567890
9.12 @@ -21,7 +20,7 @@
9.13 "--------------------------------------------------------";
9.14 "--------------------------------------------------------";
9.15
9.16 -(*WN100914======================================================================
9.17 +(*========== inhibit exn =======================================================
9.18 "--------- get_interval after replace} other 2 ----------";
9.19 "--------- get_interval after replace} other 2 ----------";
9.20 "--------- get_interval after replace} other 2 ----------";
9.21 @@ -325,7 +324,7 @@
9.22 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
9.23 (*val nxt = Empty_Tac : tac*)
9.24
9.25 -====================================================================WN100914*)
9.26 +============ inhibit exn =====================================================*)
9.27
9.28 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
9.29 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
10.1 --- a/test/Tools/isac/Interpret/mstools.sml Tue Sep 28 13:30:29 2010 +0200
10.2 +++ b/test/Tools/isac/Interpret/mstools.sml Fri Oct 01 10:23:38 2010 +0200
10.3 @@ -1,20 +1,23 @@
10.4 -(* tests on mstools.sml
10.5 - author: Walther Neuper
10.6 - 051019,
10.7 - (c) due to copyright terms
10.8 +(* Title: tests for Interpret/mstools.sml
10.9 + Author: Walther Neuper 100930
10.10 + (c) copyright due to lincense terms.
10.11
10.12 -use"../smltest/ME/mstools.sml";
10.13 -use"mstools.sml";
10.14 - *)
10.15 -
10.16 -"-----------------------------------------------------------------";
10.17 -"table of contents -----------------------------------------------";
10.18 -"-----------------------------------------------------------------";
10.19 -"--------- head_precond ------------------------------------------";
10.20 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
10.21 + 10 20 30 40 50 60 70 80
10.22 +*)
10.23 +"--------------------------------------------------------";
10.24 +"table of contents --------------------------------------";
10.25 +"--------------------------------------------------------";
10.26 +"----------- fun ----------------------------------------";
10.27 +"--------------------------------------------------------";
10.28 +"--------------------------------------------------------";
10.29 +"--------------------------------------------------------";
10.30 "-----------------------------------------------------------------";
10.31
10.32
10.33
10.34 -"--------- head_precond ------------------------------------------";
10.35 -"--------- head_precond ------------------------------------------";
10.36 -"--------- head_precond ------------------------------------------";
10.37 +(*========== inhibit exn =======================================================
10.38 +============ inhibit exn =====================================================*)
10.39 +
10.40 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.41 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
11.1 --- a/test/Tools/isac/Interpret/ptyps.sml Tue Sep 28 13:30:29 2010 +0200
11.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Fri Oct 01 10:23:38 2010 +0200
11.3 @@ -8,24 +8,23 @@
11.4 use"ptyps.sml";
11.5 *)
11.6
11.7 -"-----------------------------------------------------------------";
11.8 -"table of contents -----------------------------------------------";
11.9 -"-----------------------------------------------------------------";
11.10 -"###### val intermediate_ptyps = !ptyps; #########################";
11.11 -"----------- store test-pbtyps -----------------------------------";
11.12 -"----------- refin test-pbtyps -----------------------------------";
11.13 -"----------- refine_ori test-pbtyps ------------------------------";
11.14 -"----------- refine test-pbtyps ----------------------------------";
11.15 -"###### ptyps:= intermediate_ptyps;###############################";
11.16 -"----------- Refine_Problem (aus subp-rooteq.sml) ----------------";
11.17 -"----------- fun coll_guhs ---------------------------------------";
11.18 -"----------- fun guh2kestoreID -----------------------------------";
11.19 -"-----------------------------------------------------------------";
11.20 -"-----------------------------------------------------------------";
11.21 -"-----------------------------------------------------------------";
11.22 +"--------------------------------------------------------";
11.23 +"table of contents --------------------------------------";
11.24 +"--------------------------------------------------------";
11.25 +"###### val intermediate_ptyps = !ptyps; ################";
11.26 +"----------- store test-pbtyps --------------------------";
11.27 +"----------- refin test-pbtyps --------------------------";
11.28 +"----------- refine_ori test-pbtyps ---------------------";
11.29 +"----------- refine test-pbtyps -------------------------";
11.30 +"###### ptyps:= intermediate_ptyps;######################";
11.31 +"----------- Refine_Problem (aus subp-rooteq.sml) -------";
11.32 +"----------- fun coll_guhs ------------------------------";
11.33 +"----------- fun guh2kestoreID --------------------------";
11.34 +"--------------------------------------------------------";
11.35 +"--------------------------------------------------------";
11.36 +"--------------------------------------------------------";
11.37
11.38 -
11.39 -
11.40 +(*========== inhibit exn ?======================================================
11.41 "###### val intermediate_ptyps = !ptyps; #########################";
11.42 "###### val intermediate_ptyps = !ptyps; #########################";
11.43 "###### val intermediate_ptyps = !ptyps; #########################";
11.44 @@ -393,7 +392,7 @@
11.45 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
11.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.47 (**)
11.48 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.49 +val (p,_,f,nxt,_,pt) = me nxt p c pt;2
11.50 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.52 (*nxt = Specify_Problem ["linear","univariate","equation","test"])*)
11.53 @@ -471,4 +470,9 @@
11.54 (*
11.55 nodes [] guh3 (!ptyps);
11.56 nodes [] guh21 (!ptyps);
11.57 -*)
11.58 \ No newline at end of file
11.59 +*)
11.60 +============ inhibit exn ?====================================================*)
11.61 +
11.62 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
11.63 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
11.64 +
12.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Sep 28 13:30:29 2010 +0200
12.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri Oct 01 10:23:38 2010 +0200
12.3 @@ -16,17 +16,21 @@
12.4 "--------------------------------------------------------";
12.5 "-------- check is'_polyexp is_polyexp ------------------";
12.6 "-------- build Script Expand_binoms --------------------";
12.7 -"-------- investigate new uniary minus ------------------";
12.8 -"-------- Bsple aus Schalk I ----------------------------";
12.9 +"-------- investigate (new) uniary minus ----------------";
12.10 +"-------- check make_polynomial with simple terms -------";
12.11 +"-------- fun is_multUnordered --------------------------";
12.12 +"-------- examples from textbook Schalk I ---------------";
12.13 "-------- Script 'simplification for_polynomials' -------";
12.14 "-------- check pbl 'polynomial simplification' --------";
12.15 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
12.16 +"-------- interSteps for Schalk 299a --------------------";
12.17 "-------- norm_Poly NOT COMPLETE ------------------------";
12.18 "-------- ord_make_polynomial ---------------------------";
12.19 "--------------------------------------------------------";
12.20 "--------------------------------------------------------";
12.21 "--------------------------------------------------------";
12.22
12.23 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
12.24
12.25 "-------- check is'_polyexp is_polyexp ------------------";
12.26 "-------- check is'_polyexp is_polyexp ------------------";
12.27 @@ -35,7 +39,6 @@
12.28 then error "poly.sml: check is'_polyexp is_polyexp" else ();
12.29
12.30
12.31 -(*===== inhibit exn ?===========================================================
12.32 "-------- build Script Expand_binoms -----------------------------";
12.33 "-------- build Script Expand_binoms -----------------------------";
12.34 "-------- build Script Expand_binoms -----------------------------";
12.35 @@ -72,18 +75,19 @@
12.36 " (Try (Repeat (Calculate TIMES ))) @@ " ^
12.37 " (Try (Repeat (Calculate POWER)))) " ^
12.38 " t_t)";
12.39 +(*
12.40 val scr_expand_binoms =
12.41 "Script Expand_binoms t_t = t_t";
12.42 -
12.43 +*)
12.44 val ---------------------------------------------- = "11111";
12.45 parse thy scr_expand_binoms;
12.46 val ---------------------------------------------- = "22222";
12.47 -(*----------------------------------------------
12.48
12.49 -"-------- investigate new uniary minus ---------------------------";
12.50 -"-------- investigate new uniary minus ---------------------------";
12.51 -"-------- investigate new uniary minus ---------------------------";
12.52 -val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
12.53 +
12.54 +"-------- investigate (new) uniary minus ----------------";
12.55 +"-------- investigate (new) uniary minus ----------------";
12.56 +"-------- investigate (new) uniary minus ----------------";
12.57 +val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
12.58 atomty t;
12.59 (*** -------------
12.60 *** Const ( Trueprop, bool => prop)
12.61 @@ -117,20 +121,180 @@
12.62 (**** -------------
12.63 *** Free ( -x, real)*)
12.64
12.65 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
12.66 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
12.67
12.68 -"-------- Bsple aus Schalk I -------------------------------------";
12.69 -"-------- Bsple aus Schalk I -------------------------------------";
12.70 -"-------- Bsple aus Schalk I -------------------------------------";
12.71 -(*SPB Schalk I p.63 No.267b*)
12.72 +"-------- check make_polynomial with simple terms -------";
12.73 +"-------- check make_polynomial with simple terms -------";
12.74 +"-------- check make_polynomial with simple terms -------";
12.75 +"----- check 1 ---";
12.76 +val t = str2term "2*3*a";
12.77 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
12.78 +if term2str t = "6 * a" then () else error "check make_polynomial 1";
12.79 +
12.80 +"----- check 2 ---";
12.81 +val t = str2term "2*a + 3*a";
12.82 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
12.83 +if term2str t = "5 * a" then () else error "check make_polynomial 2";
12.84 +
12.85 +"----- check 3 ---";
12.86 +val t = str2term "2*a + 3*a + 3*a";
12.87 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
12.88 +if term2str t = "8 * a" then () else error "check make_polynomial 3";
12.89 +
12.90 +"----- check 4 ---";
12.91 +val t = str2term "3*a - 2*a";
12.92 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
12.93 +if term2str t = "a" then () else error "check make_polynomial 4";
12.94 +
12.95 +"----- check 5 ---";
12.96 +val t = str2term "4*(3*a - 2*a)";
12.97 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
12.98 +if term2str t = "4 * a" then () else error "check make_polynomial 5";
12.99 +
12.100 +"----- check 6 ---";
12.101 +val t = str2term "4*(3*a^^^2 - 2*a^^^2)";
12.102 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
12.103 +if term2str t = "4 * a ^^^ 2" then () else error "check make_polynomial 6";
12.104 +
12.105 +
12.106 +"-------- fun is_multUnordered --------------------------";
12.107 +"-------- fun is_multUnordered --------------------------";
12.108 +"-------- fun is_multUnordered --------------------------";
12.109 +val thy = theory "Isac";
12.110 +(* 100928 trace_rewrite gives the following (first occurring) difference:
12.111 +:
12.112 +### rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
12.113 + (-48 * x ^^^ 4 + 8))
12.114 +###### rls: e_rls-is_multUnordered on: p is_multUnordered
12.115 +####### try calc: Poly.is'_multUnordered'
12.116 +======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
12.117 +*)
12.118 +val t = str2term "5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))";
12.119 +
12.120 +"----- is_multUnordered ---";
12.121 +val tsort = sort_variables t;
12.122 +term2str tsort = "2 * (5 * (x ^^^ 2 * x ^^^ 7)) + 3 * (5 * x ^^^ 2) + 6 * x ^^^ 7 + 9 +\n-1 * (3 * (6 * (x ^^^ 4 * x ^^^ 5))) +\n-1 * (-1 * (3 * x ^^^ 5)) +\n-48 * x ^^^ 4 +\n8";
12.123 +is_polyexp t;
12.124 +tsort = t;
12.125 +is_polyexp t andalso not (t = sort_variables t);
12.126 +if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
12.127 +
12.128 +"----- eval_is_multUnordered ---";
12.129 +val tm = str2term "(5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))) is_multUnordered";
12.130 +case eval_is_multUnordered "testid" "" tm thy of
12.131 + SOME (_, Const ("Trueprop", _) $
12.132 + (Const ("op =", _) $
12.133 + (Const ("Poly.is'_multUnordered", _) $ _) $
12.134 + Const ("True", _))) => ()
12.135 + | _ => error "poly.sml diff. eval_is_multUnordered";
12.136 +
12.137 +"----- rewrite_set_ ---";
12.138 +(*fixme*)val NONE = rewrite_set_ thy true order_mult_ tm; (*fixme*)
12.139 +
12.140 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
12.141 +
12.142 +
12.143 +"===== take simpler testdata ===";
12.144 +val t = str2term "x^^^2 * x";
12.145 +if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 2";
12.146 +val tm = str2term "(x^^^2 * x) is_multUnordered";
12.147 +case eval_is_multUnordered "testid" "" tm thy of
12.148 + SOME (_, Const ("Trueprop", _) $
12.149 + (Const ("op =", _) $
12.150 + (Const ("Poly.is'_multUnordered", _) $ _) $
12.151 + Const ("True", _))) => ()
12.152 + | _ => error "poly.sml diff. eval_is_multUnordered 2";
12.153 +
12.154 +(*fixme val NONE = rewrite_set_ thy true order_mult_ tm;*)
12.155 +"----- rewrite__set_ ---";
12.156 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
12.157 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
12.158 +"----- app_rev ---";
12.159 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
12.160 + fun chk_prepat thy erls [] t = true
12.161 + | chk_prepat thy erls prepat t =
12.162 + let fun chk (pres, pat) =
12.163 + (let val subst: Type.tyenv * Envir.tenv =
12.164 + Pattern.match thy (pat, t)
12.165 + (Vartab.empty, Vartab.empty)
12.166 + in snd (eval__true thy (i+1)
12.167 + (map (Envir.subst_term subst) pres)
12.168 + [] erls)
12.169 + end)
12.170 + handle _ => false
12.171 + fun scan_ f [] = false (*scan_ NEVER called by []*)
12.172 + | scan_ f (pp::pps) = if f pp then true
12.173 + else scan_ f pps;
12.174 + in scan_ chk prepat end;
12.175 +
12.176 + (*.apply the normal_form of a rev-set.*)
12.177 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
12.178 + if chk_prepat thy erls prepat t
12.179 + then ((*tracing("### app_rev': t = "^(term2str t));*)
12.180 + normal_form t)
12.181 + else NONE;
12.182 +(*fixme val NONE = app_rev' thy rrls t;*)
12.183 +"----- app_rev' ---";
12.184 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
12.185 +(*fixme false*) chk_prepat thy erls prepat t;
12.186 +"----- chk_prepat ---";
12.187 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
12.188 + fun chk (pres, pat) =
12.189 + (let val subst: Type.tyenv * Envir.tenv =
12.190 + Pattern.match thy (pat, t)
12.191 + (Vartab.empty, Vartab.empty)
12.192 + in snd (eval__true thy (i+1)
12.193 + (map (Envir.subst_term subst) pres)
12.194 + [] erls)
12.195 + end)
12.196 + handle _ => false;
12.197 + fun scan_ f [] = false (*scan_ NEVER called by []*)
12.198 + | scan_ f (pp::pps) = if f pp then true
12.199 + else scan_ f pps;
12.200 +tracing "=== poly.sml: scan_ chk prepat begin";
12.201 +scan_ chk prepat;
12.202 +tracing "=== poly.sml: scan_ chk prepat end";
12.203 +
12.204 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
12.205 +
12.206 +"----- chk ---";
12.207 +val [(pres, pat)] = prepat;
12.208 + val subst: Type.tyenv * Envir.tenv =
12.209 + Pattern.match thy (pat, t)
12.210 + (Vartab.empty, Vartab.empty);
12.211 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
12.212 +"----- eval__true ---";
12.213 +val asms = (map (Envir.subst_term subst) pres);
12.214 +val (thy, i, asms, bdv, rls) =
12.215 + (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
12.216 + [] : (term * term) list, erls);
12.217 +case eval__true thy i asms bdv rls of
12.218 + ([], true) => ()
12.219 + | _ => error "poly.sml: diff. is_multUnordered, eval__true";
12.220 +
12.221 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
12.222 +
12.223 +(*===== inhibit exn ?===========================================================
12.224 +
12.225 +
12.226 +
12.227 +"-------- examples from textbook Schalk I ---------------";
12.228 +"-------- examples from textbook Schalk I ---------------";
12.229 +"-------- examples from textbook Schalk I ---------------";
12.230 +"-----SPB Schalk I p.63 No.267b ---";
12.231 +trace_rewrite := true; tracing "-----SPB Schalk I p.63 No.267b ---begin";
12.232 val t = str2term
12.233 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
12.234 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.235 +term2str t;
12.236 +trace_rewrite := false; tracing "-----SPB Schalk I p.63 No.267b ---end";
12.237 if (term2str t) =
12.238 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
12.239 then ()
12.240 else error "poly.sml: diff.behav. in make_polynomial 1";
12.241
12.242 -(*SPB Schalk I p.63 No.275b*)
12.243 +"-----SPB Schalk I p.63 No.275b ---";
12.244 val t = str2term
12.245 "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
12.246 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.247 @@ -141,7 +305,7 @@
12.248 then ()
12.249 else error "poly.sml: diff.behav. in make_polynomial 2";
12.250
12.251 -(*SPB Schalk I p.63 No.279b*)
12.252 +"-----SPB Schalk I p.63 No.279b ---";
12.253 val t = str2term
12.254 "(x-a)*(x-b)*(x-c)*(x-d)";
12.255 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.256 @@ -152,7 +316,7 @@
12.257 then ()
12.258 else error "poly.sml: diff.behav. in make_polynomial 3";
12.259
12.260 -(*SPB Schalk I p.63 No.291*)
12.261 +"-----SPB Schalk I p.63 No.291 ---";
12.262 val t = str2term
12.263 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
12.264 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.265 @@ -162,7 +326,7 @@
12.266 then ()
12.267 else error "poly.sml: diff.behav. in make_polynomial 4";
12.268
12.269 -(*SPB Schalk I p.64 No.295c*)
12.270 +"-----SPB Schalk I p.64 No.295c ---";
12.271 val t = str2term
12.272 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
12.273 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.274 @@ -173,17 +337,17 @@
12.275 then ()
12.276 else error "poly.sml: diff.behav. in make_polynomial 5";
12.277
12.278 -(*SPB Schalk I p.64 No.299a*)
12.279 +"-----SPB Schalk I p.64 No.299a ---";
12.280 val t = str2term
12.281 "(x - y)*(x + y)";
12.282 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.283 term2str t;
12.284 -if (term2str t) =
12.285 -"x ^^^ 2 + -1 * y ^^^ 2"
12.286 -then ()
12.287 +(*
12.288 +if (term2str t) = "x ^^^ 2 + -1 * y ^^^ 2" then ()
12.289 else error "poly.sml: diff.behav. in make_polynomial 6";
12.290 +*)
12.291
12.292 -(*SPB Schalk I p.64 No.300c*)
12.293 +"-----SPB Schalk I p.64 No.300c ---";
12.294 val t = str2term
12.295 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
12.296 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.297 @@ -193,7 +357,7 @@
12.298 then ()
12.299 else error "poly.sml: diff.behav. in make_polynomial 7";
12.300
12.301 -(*SPB Schalk I p.64 No.302*)
12.302 +"-----SPB Schalk I p.64 No.302 ---";
12.303 val t = str2term
12.304 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
12.305 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.306 @@ -202,7 +366,7 @@
12.307 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
12.308
12.309
12.310 -(*SPB Schalk I p.64 No.306a*)
12.311 +"-----SPB Schalk I p.64 No.306a ---";
12.312 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
12.313 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.314 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
12.315 @@ -217,32 +381,32 @@
12.316 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
12.317 else error "poly.sml: diff.behav. in make_polynomial 9b";
12.318
12.319 -(*SPB Schalk I p.64 No.296a*)
12.320 +"-----SPB Schalk I p.64 No.296a ---";
12.321 val t = str2term "(x - a)^^^3";
12.322 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.323 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
12.324 then () else error "poly.sml: diff.behav. in make_polynomial 10";
12.325
12.326 -(*SPB Schalk I p.64 No.296c*)
12.327 +"-----SPB Schalk I p.64 No.296c ---";
12.328 val t = str2term "(-3*x - 4*y)^^^3";
12.329 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.330 if (term2str t) =
12.331 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
12.332 then () else error "poly.sml: diff.behav. in make_polynomial 11";
12.333
12.334 -(*SPB Schalk I p.62 No.242c*)
12.335 +"-----SPB Schalk I p.62 No.242c ---";
12.336 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
12.337 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.338 if (term2str t) = "1" then ()
12.339 else error "poly.sml: diff.behav. in make_polynomial 12";
12.340
12.341 -(*SPB Schalk I p.60 No.209a*)
12.342 +"-----SPB Schalk I p.60 No.209a ---";
12.343 val t = str2term "a^^^(7-x) * a^^^x";
12.344 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.345 if term2str t = "a ^^^ 7" then ()
12.346 else error "poly.sml: diff.behav. in make_polynomial 13";
12.347
12.348 -(*SPB Schalk I p.60 No.209d*)
12.349 +"-----SPB Schalk I p.60 No.209d ---";
12.350 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
12.351 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.352 if term2str t = "d ^^^ 3" then ()
12.353 @@ -253,7 +417,7 @@
12.354 (*------------------ Bsple bei denen es Probleme gibt------------------*)
12.355 (*---------------------------------------------------------------------*)
12.356
12.357 -(*Schalk I p.64 No.303*)
12.358 +"-----Schalk I p.64 No.303 ---";
12.359 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
12.360 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.361 if term2str t = "1280 * b ^^^ 4" then ()
12.362 @@ -264,62 +428,62 @@
12.363 (*--------------------------------------------------------------------*)
12.364 (*----------------------- Eigene Beispiele ---------------------------*)
12.365 (*--------------------------------------------------------------------*)
12.366 -(*SPO*)
12.367 +"-----SPO ---";
12.368 val t = str2term "a^^^2*a^^^(-2)";
12.369 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.370 if term2str t = "1" then ()
12.371 else error "poly.sml: diff.behav. in make_polynomial 15";
12.372 -(*SPO*)
12.373 +"-----SPO ---";
12.374 val t = str2term "a + a + a";
12.375 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.376 if term2str t = "3 * a" then ()
12.377 else error "poly.sml: diff.behav. in make_polynomial 16";
12.378 -(*SPO*)
12.379 +"-----SPO ---";
12.380 val t = str2term "a + b + b + b";
12.381 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.382 if term2str t = "a + 3 * b" then ()
12.383 else error "poly.sml: diff.behav. in make_polynomial 17";
12.384 -(*SPO*)
12.385 +"-----SPO ---";
12.386 val t = str2term "a^^^2*b*b^^^(-1)";
12.387 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.388 if term2str t = "a ^^^ 2" then ()
12.389 else error "poly.sml: diff.behav. in make_polynomial 18";
12.390 -(*SPO*)
12.391 +"-----SPO ---";
12.392 val t = str2term "a^^^2*a^^^(-2)";
12.393 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.394 if (term2str t) = "1" then ()
12.395 else error "poly.sml: diff.behav. in make_polynomial 19";
12.396 -(*SPO*)
12.397 +"-----SPO ---";
12.398 val t = str2term "b + a - b";
12.399 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.400 if (term2str t) = "a" then ()
12.401 else error "poly.sml: diff.behav. in make_polynomial 20";
12.402 -(*SPO*)
12.403 +"-----SPO ---";
12.404 val t = str2term "b * a * a";
12.405 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.406 if term2str t = "a ^^^ 2 * b" then ()
12.407 else error "poly.sml: diff.behav. in make_polynomial 21";
12.408 -(*SPO*)
12.409 +"-----SPO ---";
12.410 val t = str2term "(a^^^2)^^^3";
12.411 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.412 if term2str t = "a ^^^ 6" then ()
12.413 else error "poly.sml: diff.behav. in make_polynomial 22";
12.414 -(*SPO*)
12.415 +"-----SPO ---";
12.416 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
12.417 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.418 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
12.419 else error "poly.sml: diff.behav. in make_polynomial 23";
12.420 -(*SPO*)
12.421 +"-----SPO ---";
12.422 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
12.423 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.424 if (term2str t) = "a ^^^ 4" then ()
12.425 else error "poly.sml: diff.behav. in make_polynomial 24";
12.426 -(*SPO*)
12.427 +"-----SPO ---";
12.428 val t = str2term "a * b * b^^^(-1) + a";
12.429 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.430 if (term2str t) = "2 * a" then ()
12.431 else error "poly.sml: diff.behav. in make_polynomial 25";
12.432 -(*SPO*)
12.433 +"-----SPO ---";
12.434 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
12.435 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
12.436 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
12.437 @@ -327,7 +491,7 @@
12.438
12.439
12.440 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
12.441 -(*SPO*)
12.442 +"-----SPO ---";
12.443 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
12.444 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
12.445 term2str t;
12.446 @@ -339,9 +503,9 @@
12.447 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
12.448 then () else error "poly.sml: diff.behav. in make_polynomial 28";
12.449
12.450 -"-------- Script 'simplification for_polynomials' ----------------";
12.451 -"-------- Script 'simplification for_polynomials' ----------------";
12.452 -"-------- Script 'simplification for_polynomials' ----------------";
12.453 +"-------- Script 'simplification for_polynomials' -------";
12.454 +"-------- Script 'simplification for_polynomials' -------";
12.455 +"-------- Script 'simplification for_polynomials' -------";
12.456 val str =
12.457 "Script SimplifyScript (t_::real) = \
12.458 \ ((Rewrite_Set norm_Poly False) t_)";
12.459 @@ -349,19 +513,19 @@
12.460 atomty sc;
12.461
12.462
12.463 -"-------- check pbl 'polynomial simplification' -----------------";
12.464 -"-------- check pbl 'polynomial simplification' -----------------";
12.465 -"-------- check pbl 'polynomial simplification' -----------------";
12.466 +"-------- check pbl 'polynomial simplification' --------";
12.467 +"-------- check pbl 'polynomial simplification' --------";
12.468 +"-------- check pbl 'polynomial simplification' --------";
12.469 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
12.470 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
12.471 "normalform N"];
12.472 -(*0*)
12.473 +"-----0 ---";
12.474 case refine fmz ["polynomial","simplification"]of
12.475 [Matches (["polynomial", "simplification"], _)] => ()
12.476 | _ => error "poly.sml diff.behav. in check pbl, refine";
12.477 (*...if there is an error, then ...*)
12.478
12.479 -(*1*)
12.480 +"-----1 ---";
12.481 print_depth 7;
12.482 val pbt = get_pbt ["polynomial","simplification"];
12.483 print_depth 3;
12.484 @@ -369,13 +533,13 @@
12.485 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
12.486 ... then trace_rewrite:*)
12.487
12.488 -(*2*)
12.489 +"-----2 ---";
12.490 trace_rewrite:=true;
12.491 match_pbl fmz pbt;
12.492 trace_rewrite:=false;
12.493 (*... if there is no rewrite, then there is something wrong with prls*)
12.494
12.495 -(*3*)
12.496 +"-----3 ---";
12.497 print_depth 7;
12.498 val prls = (#prls o get_pbt) ["polynomial","simplification"];
12.499 print_depth 3;
12.500 @@ -388,7 +552,7 @@
12.501 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
12.502 (*... if this works, but (*1*) does still NOT work, check types:*)
12.503
12.504 -(*4*)
12.505 +"-----4 ---";
12.506 show_types:=true;
12.507 (*
12.508 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
12.509 @@ -398,9 +562,9 @@
12.510 show_types:=false;
12.511
12.512
12.513 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
12.514 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
12.515 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
12.516 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
12.517 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
12.518 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
12.519 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
12.520 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
12.521 "normalform N"];
12.522 @@ -424,9 +588,9 @@
12.523 then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
12.524
12.525
12.526 -"-------- interSteps for Schalk 299a -----------------------------";
12.527 -"-------- interSteps for Schalk 299a -----------------------------";
12.528 -"-------- interSteps for Schalk 299a -----------------------------";
12.529 +"-------- interSteps for Schalk 299a --------------------";
12.530 +"-------- interSteps for Schalk 299a --------------------";
12.531 +"-------- interSteps for Schalk 299a --------------------";
12.532 states:=[];
12.533 CalcTree
12.534 [(["TERM ((x - y)*(x + y))", "normalform N"],
12.535 @@ -448,18 +612,19 @@
12.536 else error "poly.sml: interSteps doesnt work again 2";
12.537
12.538
12.539 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
12.540 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
12.541 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
12.542 +"-------- norm_Poly NOT COMPLETE ------------------------";
12.543 +"-------- norm_Poly NOT COMPLETE ------------------------";
12.544 +"-------- norm_Poly NOT COMPLETE ------------------------";
12.545 trace_rewrite:=true;
12.546 val SOME (f',_) = rewrite_set_ thy false norm_Poly
12.547 (str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben")(*see poly.sml: -- norm_Poly NOT COMPLETE -- TODO MG*);
12.548 trace_rewrite:=false;
12.549 term2str f';
12.550
12.551 -"-------- ord_make_polynomial ------------------------------------";
12.552 -"-------- ord_make_polynomial ------------------------------------";
12.553 -"-------- ord_make_polynomial ------------------------------------";
12.554 +
12.555 +"-------- ord_make_polynomial ---------------------------";
12.556 +"-------- ord_make_polynomial ---------------------------";
12.557 +"-------- ord_make_polynomial ---------------------------";
12.558 val t1 = str2term "2 * b + (3 * a + 3 * b)";
12.559 val t2 = str2term "3 * a + 3 * b + 2 * b";
12.560
12.561 @@ -475,5 +640,4 @@
12.562 val t2 = str2term "3 * a + (2 * b + 3 * b)";
12.563
12.564
12.565 -----------------------------------------------*)
12.566 ===== inhibit exn ?===========================================================*)
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/ProgLang/ptyps.sml Fri Oct 01 10:23:38 2010 +0200
13.3 @@ -0,0 +1,20 @@
13.4 +(* Title: tests for Interpret/ptyps.sml
13.5 + Author: Walther Neuper 100930
13.6 + (c) copyright due to lincense terms.
13.7 +
13.8 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
13.9 + 10 20 30 40 50 60 70 80
13.10 +*)
13.11 +"--------------------------------------------------------";
13.12 +"table of contents --------------------------------------";
13.13 +"--------------------------------------------------------";
13.14 +"----------- fun ----------------------------------------";
13.15 +"--------------------------------------------------------";
13.16 +"--------------------------------------------------------";
13.17 +"--------------------------------------------------------";
13.18 +
13.19 +(*========== inhibit exn =======================================================
13.20 +============ inhibit exn =====================================================*)
13.21 +
13.22 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
13.23 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
14.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Tue Sep 28 13:30:29 2010 +0200
14.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Fri Oct 01 10:23:38 2010 +0200
14.3 @@ -1,6 +1,6 @@
14.4 -(* tests for ME/rewrite.sml
14.5 +(* Title: tests for ProgLang/rewrite.sml
14.6 TODO.WN0509 collect typical tests from systest here !!!!!
14.7 - author: Walther Neuper 050908
14.8 + Author: Walther Neuper 050908
14.9 (c) copyright due to lincense terms.
14.10
14.11 12345678901234567890123456789012345678901234567890123456789012345678901234567890
14.12 @@ -17,10 +17,13 @@
14.13 "----------- step through 'fun rewrite_terms_' ---------";
14.14 "----------- rewrite_inst_ bdvs -------------------------";
14.15 "----------- check diff 2002--2009-3 --------------------";
14.16 +"----------- fun app_rev, Rrls, prepat ------------------";
14.17 "--------------------------------------------------------";
14.18 "--------------------------------------------------------";
14.19 "--------------------------------------------------------";
14.20
14.21 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
14.22 +
14.23 "----------- assemble rewrite ---------------------------";
14.24 "----------- assemble rewrite ---------------------------";
14.25 "----------- assemble rewrite ---------------------------";
14.26 @@ -336,9 +339,102 @@
14.27 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
14.28 "--------------------------------------------------------";
14.29
14.30 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
14.31
14.32 -(*===== inhibit exn ============================================================
14.33 -===== inhibit exn ============================================================*)
14.34 +"----------- fun app_rev, Rrls, prepat ------------------";
14.35 +"----------- fun app_rev, Rrls, prepat ------------------";
14.36 +"----------- fun app_rev, Rrls, prepat ------------------";
14.37 +(* Christian Urban, 101001
14.38 +theory Test
14.39 +imports Main Complex
14.40 +begin
14.41 +
14.42 +ML {*
14.43 +let
14.44 + val parser = Args.context -- Scan.lift Args.name_source
14.45 + fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
14.46 + |> ML_Syntax.print_term |> ML_Syntax.atomic
14.47 +in
14.48 + ML_Antiquote.inline "term_pat" (parser >> term_pat)
14.49 +end
14.50 +*}
14.51 +
14.52 +ML {*
14.53 + val t = @{term "a + b * x = (0 ::real)"};
14.54 + val pat = @{term_pat "?l = (?r ::real)"};
14.55 + val precond = @{term_pat "is_polynomial (?l::real)"};
14.56 + val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
14.57 +*}
14.58 +
14.59 +ML {*
14.60 + Envir.subst_term inst precond
14.61 + |> Syntax.string_of_term @{context}
14.62 + |> writeln
14.63 +*}
14.64 +end *)
14.65 +val t = @{term "a + b * x = (0 ::real)"};
14.66 +val pat = parse_patt thy "?l = (?r ::real)";
14.67 +val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
14.68 +val precond = parse_patt thy " (?l::real) is_expanded";
14.69 +
14.70 +val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
14.71 +val preinst = Envir.subst_term inst precond;
14.72 +term2str preinst;
14.73 +
14.74 +"===== Rational.thy: cancel ===";
14.75 +(* pat matched with the current term gives an environment
14.76 + (or not: hen the Rrls not applied);
14.77 + if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
14.78 + then the Rrls is applied. *)
14.79 +val t = str2term "(a + b) / c ::real";
14.80 +val pat = parse_patt thy "?r / ?s ::real";
14.81 +val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
14.82 +val prepat = [(pres, pat)];
14.83 +val erls = rational_erls;
14.84 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
14.85 +
14.86 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
14.87 +val asms = map (Envir.subst_term subst) pres;
14.88 +if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
14.89 +then () else error "rewrite.sml: prepat cancel subst";
14.90 +if ([], true) = eval__true thy 0 asms [] erls
14.91 +then () else error "rewrite.sml: prepat cancel eval__true";
14.92 +
14.93 +"===== Rational.thy: common_nominator_p ===";
14.94 +(* if each pat* matches with the current term, the Rrls is applied
14.95 + (there are no preconditions to be checked, they are HOLogic.true_const) *)
14.96 +val t = str2term "a / b + 1 / 2";
14.97 +val pat = parse_patt thy "?r / ?s + ?u / ?v";
14.98 +val pres = [HOLogic.true_const];
14.99 +val prepat = [(pres, pat)];
14.100 +val erls = rational_erls;
14.101 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
14.102 +
14.103 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
14.104 +if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
14.105 +then () else error "rewrite.sml: prepat common_nominator_p";
14.106 +
14.107 +"===== Poly.thy: order_mult_ ===";
14.108 + (* ?p matched with the current term gives an environment,
14.109 + which evaluates (the instantiated) "p is_multUnordered" to true*)
14.110 +val t = str2term "x^^^2 * x";
14.111 +val pat = parse_patt thy "?p :: real"
14.112 +val pres = [parse_patt thy "?p is_multUnordered"];
14.113 +val prepat = [(pres, pat)];
14.114 +val erls = append_rls "e_rls-is_multUnordered" e_rls
14.115 + [Calc ("Poly.is'_multUnordered",
14.116 + eval_is_multUnordered "")];
14.117 +
14.118 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
14.119 +val asms = map (Envir.subst_term subst) pres;
14.120 +if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
14.121 +then () else error "rewrite.sml: prepat order_mult_ subst";
14.122 +if ([], true) = eval__true thy 0 asms [] erls
14.123 +then () else error "rewrite.sml: prepat order_mult_ eval__true";
14.124 +
14.125 +
14.126 +(*========== inhibit exn =======================================================
14.127 +============ inhibit exn =====================================================*)
14.128
14.129 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
14.130 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)