1.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -60,7 +60,7 @@
1.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.6
1.7 -nxt = ("Rewrite_Set", Rewrite_Set "RatEq_eliminate");
1.8 +case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
1.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.10 (*
1.11 WN120317.TODO dropped rateq: here "x ~= 0 should go to ctxt, but it does not:
1.12 @@ -91,7 +91,7 @@
1.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.14 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
1.15 f2str f = "[x = 1 / 5]";
1.16 -nxt = ("Check_elementwise", Check_elementwise "Assumptions");
1.17 +case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
1.18 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
1.19 val (pt, p) = case locatetac tac (pt,p) of
1.20 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac";
1.21 @@ -131,7 +131,7 @@
1.22 term2str stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
1.23 "~~~~~ to appy return val:"; val ((a', STac stac)) = ((a', STac stac'));
1.24 val (m,m') = stac2tac_ pt (assoc_thy th) stac;
1.25 -m = Check_elementwise "Assumptions"; (*m' = Empty_Tac_ ???!??? *);
1.26 +case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
1.27 val (p''''', pt''''', m''''') = (p, pt, m);
1.28 "~~~~~ fun applicable_in, args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
1.29 member op = [Pbl,Met] p_; (* = false*)
1.30 @@ -170,8 +170,10 @@
1.31 else error "rateq.sml: new behaviour: [x = 1 / 5]";
1.32 (*WN120317.TODO dropped rateq*)
1.33 ============ inhibit exn WN120316 ==============================================*)
1.34 -if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[]" then ()
1.35 -else error "rateq.sml: new behaviour: [x = 1 / 5]";
1.36 +if p = ([], Res) andalso f2str f = "[]"
1.37 +then case nxt of ("End_Proof'", End_Proof') => ()
1.38 + | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"
1.39 +else error "rateq.sml: new behaviour: [x = 1 / 5] 2"
1.40
1.41 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
1.42 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
1.43 @@ -228,8 +230,8 @@
1.44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.47 -if nxt = ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) then ()
1.48 -else error "55b root specification broken";
1.49 +case nxt of ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) => ()
1.50 +| _ => error "55b root specification broken";
1.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.53 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.54 @@ -237,26 +239,26 @@
1.55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.58 -if nxt = ("Apply_Method", Apply_Method ["PolyEq", "normalize_poly"]) then ()
1.59 -else error "55b normalize_poly specification broken";
1.60 +case nxt of ("Apply_Method", Apply_Method ["PolyEq", "normalize_poly"]) => ()
1.61 +| _ => error "55b normalize_poly specification broken";
1.62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.65 -if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0")) then()
1.66 -else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
1.67 +case f of Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0")) => ()
1.68 +| _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
1.69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.73 -if nxt = ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) then ()
1.74 -else error "55b normalize_poly specification broken";
1.75 +case nxt of ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) => ()
1.76 +| _ => error "55b normalize_poly specification broken";
1.77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.81
1.82 -f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
1.83 -snd nxt = Check_elementwise "Assumptions"; (*= GUI*)
1.84 +f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
1.85 +case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*)
1.86 if terms2str (get_assumptions_ pt p) =
1.87 ("[\"~ matches (?a = 0)\n" ^
1.88 " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^
1.89 @@ -328,6 +330,8 @@
1.90 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.91 (*WN120317.TODO dropped rateq*)
1.92 ============ inhibit exn WN120316 ==============================================*)
1.93 -if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[]" then ()
1.94 -else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.95 + if p = ([], Res) andalso f2str f = "[]"
1.96 + then case nxt of ("End_Proof'", End_Proof') => ()
1.97 + | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 1"
1.98 + else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 2";
1.99