wneuper/isa: comparison test/Tools/isac/Knowledge/diffapp.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of (_, Specify_Method ["DiffApp","max_by_calculus"]) => ()
-	  | _ => raise error "diffapp.sml: max-exp me, nxt = Specify_Method";
+	  | _ => error "diffapp.sml: max-exp me, nxt = Specify_Method";
 val oris = fst3 (get_obj g_origin pt (fst p)); writeln(oris2str oris);
 val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits);
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val mits = get_obj g_met pt (fst p); writeln(itms2str_ ctxt mits);
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => ()
-	  | _ => raise error "diffapp.sml: max-exp me, nxt = Apply_Method";
+	  | _ => error "diffapp.sml: max-exp me, nxt = Apply_Method";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*since 0508 Apply_Method does the 1st step, if NONE init_form -------------
 (*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*)
 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;
 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 (*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*)
 ----------------------------------------------------------------------------*)
 case nxt of (_, Model_Problem(*["by_explicit", "make", "function"]*)) => ()
-	  | _ => raise error "diffapp.sml: max-exp me, nxt = Model_Problem";
+	  | _ => error "diffapp.sml: max-exp me, nxt = Model_Problem";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of (_, Apply_Method ["DiffApp", "make_fun_by_explicit"]) => ()
-	  | _ => raise error "diffapp.sml: max-exp Apply_Method ([1], Met) ";
+	  | _ => error "diffapp.sml: max-exp Apply_Method ([1], Met) ";
 (*----since WN050901 (ie. corr. mathengine#nxt_specify_ ..nxt_spec Pbl->p_
 we get at ...
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 ...
 val ((pt,p),_) = get_calc 1;
 val mits = get_obj g_met pt (fst p);
 writeln (itms2str_ ctxt mits);
 (*
 if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then ()
-else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
+else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
 *)
 (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
 (* WN051209 while extending 'fun step' for initac, this became better ...
 if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then ()
-else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
+else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
 *)
 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
 val s = subst_atomic env t;
 term2str s;
 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
 val SOME (s',_) = rewrite_set_ thy false list_rls s;
 val s'' = term2str s';
-if s''="A = a * b" then () else raise error "new behaviour with list_rls 1.1.";
+if s''="A = a * b" then () else error "new behaviour with list_rls 1.1.";
 val env = env @ [(str2term "e_::bool",str2term "A = a * b")];
 (*--- 2.line: condition alone ---*)
 val t = str2term "1 < length_ (r_s::bool list)";
 val s = subst_atomic env t;
 term2str s;
 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
 val SOME (s',_) = rewrite_set_ thy false list_rls s;
 val s'' = term2str s';
-if s''="True" then () else raise error "new behaviour with list_rls 1.2.";
+if s''="True" then () else error "new behaviour with list_rls 1.2.";
 (*--- 2.line in script ---*)
 val t = str2term
 	    "(if 1 < length_ r_s                            \
 \           then (SubProblem (Reals_,[make,function],[no_met])\
 val s'' = term2str s';
 if s'' =
 "SubProblem (Reals_, [make, function], [no_met])\n\
 \ [REAL A, REAL b,\n\
 \  BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
-else raise error "new behaviour with list_rls 1.3.";
+else error "new behaviour with list_rls 1.3.";
 val env = env @ [(str2term "t_::bool",
 		  str2term "A = (2*sqrt(r^^^2-(b/2)^^^2)) * b")];
 term2str s;
 val t = str2term
 "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
-if s' = "A = a * b" then () else raise error "new behaviour with list_rls 2.1";
+if s' = "A = a * b" then () else error "new behaviour with list_rls 2.1";
 val env = env @ [(str2term "h_::bool", str2term s')];
 (*--- 2.line in script ---*)
 val t = str2term "hd (dropWhile (ident h_) (eqs::bool list))";
 val s = subst_atomic env t;
 mem_rls "dropWhile_Cons" list_rls;
 mem_rls "Atools.ident" list_rls;
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 if s' = "(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2" then ()
-else raise error "new behaviour with list_rls 2.2";
+else error "new behaviour with list_rls 2.2";
 val env = env @ [(str2term "e_1::bool", str2term s')];
 (*--- 3.line in script ---*)
 val t = str2term "dropWhile (ident f_) (Vars (h_::bool))";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
-if s' = "[a, b]" then () else raise error "new behaviour with list_rls 2.3";
+if s' = "[a, b]" then () else error "new behaviour with list_rls 2.3";
 val env = env @ [(str2term "vs_::real list", str2term s')];
 (*--- 4.line in script ---*)
 val t = str2term "hd (dropWhile (ident v_v) v_s)";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "hd (dropWhile (ident b) [a, b])";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
-if s' = "a" then () else raise error "new behaviour with list_rls 2.4.";
+if s' = "a" then () else error "new behaviour with list_rls 2.4.";
 val env = env @ [(str2term "v_1::real", str2term s')];
 (*--- 5.line in script ---*)
 val t = str2term "(SubProblem(Reals_,[univar,equation],[no_met])\
 		 \           [BOOL e_1, REAL v_1])";
 \ (A = a * b)";
 mem_rls "Tools.rhs" list_rls;
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 if s' = "Substitute [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)] (A = a * b)"
-then () else raise error "new behaviour with list_rls 2.6.";
+then () else error "new behaviour with list_rls 2.6.";
 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
 trace_rewrite:=true;
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 trace_rewrite:=false;
 val s' = term2str t';
-if s' = "A = a * b" then() else raise error "new behaviour with list_rls 3.1.";
+if s' = "A = a * b" then() else error "new behaviour with list_rls 3.1.";
 val env = env @ [(str2term "h_::bool", str2term s')];
 (*--- 2.line in script ---*)
 val t = str2term "dropWhile (ident (h_::bool)) (eqs::bool list)";
 val s = subst_atomic env t;
 "dropWhile (ident (A = a * b))\
 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]"
-then () else raise error "new behaviour with list_rls 3.2.";
+then () else error "new behaviour with list_rls 3.2.";
 val env = env @ [(str2term "es_::bool list", str2term s')];
 (*--- 3.line in script ---*)
 val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_::bool))";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
-if s' = "[a, b]" then () else raise error "new behaviour with list_rls 3.3.";
+if s' = "[a, b]" then () else error "new behaviour with list_rls 3.3.";
 val env = env @ [(str2term "vs_::real list", str2term s')];
 (*--- 4.line in script ---*)
 val t = str2term "nth_ 1 v_s";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "nth_ 1 [a, b]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
-if s' = "a" then () else raise error "new behaviour with list_rls 3.4.";
+if s' = "a" then () else error "new behaviour with list_rls 3.4.";
 val env = env @ [(str2term "v_1", str2term s')];
 (*--- 5.line in script ---*)
 val t = str2term "nth_ 2 v_s";
 val s = subst_atomic env t;
 term2str s;
 val t = str2term "nth_ 2 [a, b]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
-if s' = "b" then () else raise error "new behaviour with list_rls 3.5.";
+if s' = "b" then () else error "new behaviour with list_rls 3.5.";
 val env = env @ [(str2term "v_2", str2term s')];
 (*--- 6.line in script ---*)
 val t = str2term "(hd o (filterVar v_1)) (es_::bool list)";
 val s = subst_atomic env t;
 val t = str2term
 	   "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 if s' = "a / 2 = r * sin alpha" then ()
-else raise error "new behaviour with list_rls 3.6.";
+else error "new behaviour with list_rls 3.6.";
 val e_1 = str2term "e_1::bool";
 val env = env @ [(e_1, str2term s')];
 (*--- 7.line in script ---*)
 val t = str2term "(hd o (filterVar v_2)) (es_::bool list)";
 val t = str2term
 	  "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
 val SOME (t',_) = rewrite_set_ thy false list_rls t;
 val s' = term2str t';
 if s' = "b / 2 = r * cos alpha" then ()
-else raise error "new behaviour with list_rls 3.7.";
+else error "new behaviour with list_rls 3.7.";
 val env = env @ [(str2term "e_2::bool", str2term s')];
 (*--- 8.line in script ---*)
 val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
 		 \            [BOOL e_1, REAL v_1])";
 \              (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";
 val SOME (s',_) = rewrite_set_ thy false list_rls s;
 val s'' = term2str s';
 if s'' =
 "Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"
-then () else raise error "new behaviour with list_rls 3.10.";
+then () else error "new behaviour with list_rls 3.10.";

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37995	fac82f29f143
child 38043	6a36acec95d9