1.1 --- a/test/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -176,8 +176,10 @@
1.4 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
1.5
1.6 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
1.7 -if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", str2term "- qq ?x = Q' ?x"))
1.8 -then () else error "--- WN0509 Substitute 2nd part --- changed";
1.9 +val thm = case nxt of ("Rewrite", Rewrite ("Belastung_Querkraft", thm)) => thm
1.10 +| _ => error "--- WN0509 Substitute 2nd part --- changed 1";
1.11 +if (term2str o Thm.prop_of) thm = "- qq ?x = Q' ?x" then ()
1.12 +else error "--- WN0509 Substitute 2nd part --- changed 2";
1.13
1.14
1.15 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.16 @@ -198,8 +200,8 @@
1.17 case appltacs of
1.18 [Rewrite ("radd_commute", radd_commute),
1.19 Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
1.20 - => if term2str radd_commute = "?m + ?n = ?n + ?m" andalso
1.21 - term2str add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
1.22 + => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
1.23 + (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
1.24 else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
1.25 | _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
1.26
1.27 @@ -395,7 +397,7 @@
1.28
1.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
1.30 val (p'''', pt'''') = (p, pt);
1.31 -f2str f = "x + 1 = 2"; snd nxt = Rewrite_Set "norm_equation";
1.32 +f2str f = "x + 1 = 2"; case snd nxt of Rewrite_Set "norm_equation" => () | _ => error "CHANGED";
1.33 val (p, p_) = p(* = ([1], Frm)*);
1.34 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.35 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.36 @@ -407,7 +409,8 @@
1.37
1.38 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.39 val (p'''', pt'''') = (p, pt);
1.40 -f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify";
1.41 +f2str f = "x + 1 + -1 * 2 = 0";
1.42 +case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
1.43 val (p, p_) = p(* = ([1], Res)*);
1.44 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.45 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.46 @@ -419,7 +422,9 @@
1.47
1.48 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.49 val (p'''', pt'''') = (p, pt);
1.50 -f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]);
1.51 +f2str f = "-1 + x = 0";
1.52 +case snd nxt of Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) => ()
1.53 +| _ => error "CHANGED";
1.54 val (p, p_) = p(* = ([2], Res)*);
1.55 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.56 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
1.57 @@ -448,7 +453,8 @@
1.58
1.59 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
1.60 val (p'''', pt'''') = (p, pt);
1.61 -f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv");
1.62 +f2str f = "-1 + x = 0";
1.63 +case snd nxt of Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") => () | _ => error "CHANGED";
1.64 val (p, p_) = p(* = ([3, 1], Frm)*);
1.65 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.66 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.67 @@ -460,7 +466,8 @@
1.68
1.69 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.70 val (p'''', pt'''') = (p, pt);
1.71 -f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify";
1.72 +f2str f = "x = 0 + -1 * -1";
1.73 +case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
1.74 val (p, p_) = p(* = ([3, 1], Res)*);
1.75 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.76 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.77 @@ -488,33 +495,32 @@
1.78
1.79 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1.80 val tacs = sel_rules pt ([],Pbl);
1.81 - if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
1.82 - else error "script.sml: diff.behav. in sel_rules ([],Pbl)";
1.83 + case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
1.84 + | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
1.85
1.86 val tacs = sel_rules pt ([1],Res);
1.87 - if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.88 + case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.89 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
1.90 - Check_elementwise "Assumptions"] then ()
1.91 - else error "script.sml: diff.behav. in sel_rules ([1],Res)";
1.92 + Check_elementwise "Assumptions"] => ()
1.93 + | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
1.94
1.95 val tacs = sel_rules pt ([3],Pbl);
1.96 - if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
1.97 - else error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
1.98 + case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
1.99 + | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
1.100
1.101 val tacs = sel_rules pt ([3,1],Res);
1.102 - if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
1.103 - Rewrite_Set "Test_simplify"] then ()
1.104 - else error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
1.105 + case tacs of [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
1.106 + | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
1.107
1.108 val tacs = sel_rules pt ([3],Res);
1.109 - if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.110 + case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.111 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
1.112 - Check_elementwise "Assumptions"] then ()
1.113 - else error "script.sml: diff.behav. in sel_rules ([3],Res)";
1.114 + Check_elementwise "Assumptions"] => ()
1.115 + | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
1.116
1.117 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
1.118 - if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
1.119 - else error "script.sml: diff.behav. in sel_rules ([],Res)";
1.120 + case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
1.121 + | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
1.122
1.123 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.124 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.125 @@ -534,10 +540,10 @@
1.126 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
1.127 val ((pt, _), _) = get_calc cI;
1.128 (*version 1:*)
1.129 -if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.130 +case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.131 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
1.132 - Check_elementwise "Assumptions"] then ()
1.133 -else error "fetchApplicableTactics ([1],Res) changed";
1.134 + Check_elementwise "Assumptions"] => ()
1.135 +| _ => error "fetchApplicableTactics ([1],Res) changed";
1.136 (*version 2:*)
1.137 (*WAS:
1.138 sel_appl_atomic_tacs pt p;