wneuper/isa: comparison test/Tools/isac/Interpret/solve.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 val ((pt,_),_) = get_calc 1; show_pt pt;
 (*with "Script SimplifyScript (t_::real) =       -----------------
 \  ((Rewrite_Set norm_Rational False) t_)"
 case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
-	 | _ => raise error  "solve.sml: interSteps on norm_Rational 1";
+	 | _ => error  "solve.sml: interSteps on norm_Rational 1";
 interSteps 1 ([1], Res);
 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
 interSteps 1 ([1,3], Res);
 getTactic 1 ([1,4], Res)  (*here get the tactic, and ...*);
 getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
 interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
 --------------------------------------------------------------------*)
 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
-	 | _ => raise error  "solve.sml: interSteps on norm_Rational 1";
+	 | _ => error  "solve.sml: interSteps on norm_Rational 1";
 (*these have been done now by the script ^^^ immediately...
 interSteps 1 ([1], Res);
 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
 *)
 interSteps 1 ([6], Res);
 val ((pt,_),_) = get_calc 1; show_pt pt;
 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
 case (term2str form, tac, terms2strs asm) of
 ("1 / 2", Check_Postcond ["rational", "simplification"],
 ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
-| _ => raise error "solve.sml: interSteps on norm_Rational 2";
+| _ => error "solve.sml: interSteps on norm_Rational 2";
 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*"(3 + -1 * x) / (3 + x)"*)
 if nxt = ("End_Proof'",End_Proof') then ()
-else raise error "details.sml, changed behaviour in: without detail";
+else error "details.sml, changed behaviour in: without detail";
 val str = pr_ptree pr_short pt;
 writeln str;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
 andalso nxt = ("End_Proof'",End_Proof') then ()
-else raise error "new behaviour in details.sml, \
+else error "new behaviour in details.sml, \
 		 \cancel, rev-rew (cancel) afterwards";
 FIXXXXXME.040216 #####################################################*)
 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*"(3 + -1 * x) / (3 + x)"*)
 if nxt = ("End_Proof'",End_Proof') then ()
-else raise error "details.sml, changed behaviour in: cancel_p, without detail";
+else error "details.sml, changed behaviour in: cancel_p, without detail";
 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
 (* val p = e_pos'; val c = [];
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 if nxt = ("End_Detail",End_Detail) then ()
-else raise error "details.sml: new behav. in Detail make_polynomial";
+else error "details.sml: new behav. in Detail make_polynomial";
 ----------------------------------------------------------------------*)
 (*---------------
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
 andalso nxt = ("End_Proof'",End_Proof') then ()
-else raise error "new behaviour in details.sml, cancel_p afterwards";
+else error "new behaviour in details.sml, cancel_p afterwards";
 ----------------*)
 interSteps 1 ([],Res);
 val [(_,(((pt,_),_),[(_,ip)]))] = !states;
 val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
 (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3),(_,_,t4),(_,_,t5),(_,_,t6)] =>
 	    (writeln o terms2str) [t1,t2,t3,t4,t5,t6]
-	  | _ => raise error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()
+	  | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()
-else raise error "details.sml: diff.behav. in interSteps'donesteps' 1";
+else error "details.sml: diff.behav. in interSteps'donesteps' 1";
 moveActiveDown 1;
 moveActiveDown 1;
 moveActiveDown 1;
 moveActiveDown 1;
 interSteps 1 ([3],Pbl) (*subproblem*);
 val [(_,(((pt,_),_),[(_,ip)]))] = !states;
 val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
 (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3)] =>
 	    (writeln o terms2str) [t1,t2,t3]
-	  | _ => raise error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()
+	  | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()
-else raise error "details.sml: diff.behav. in interSteps'donesteps' 1";
+else error "details.sml: diff.behav. in interSteps'donesteps' 1";
 (* val [(_,(((pt,_),_),[(_,ip)]))] = !states;
 writeln (pr_ptree pr_short pt);
 get_obj g_tac pt [4];
 refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)
 interSteps 1 ([2],Res);
 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
 if length (children (get_nd pt p)) = 6 then ()
-else raise error "details.sml: diff.behav. in interSteps'detailrls' 1";
+else error "details.sml: diff.behav. in interSteps'detailrls' 1";
 moveActiveDown 1;
 moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA>  *);
 interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);
 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
 if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)
-else raise error "details.sml: diff.behav. in interSteps'detailrls' 2";
+else error "details.sml: diff.behav. in interSteps'detailrls' 2";
 moveActiveDown 1;
 refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)
 interSteps 1 ([3,1],Res);
 refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)
 interSteps 1 ([3,2],Res);
 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
 if length (children (get_nd pt p)) = 2 then ()
-else raise error "details.sml: diff.behav. in interSteps'detailrls' 3";
+else error "details.sml: diff.behav. in interSteps'detailrls' 3";
 val ((pt,p),_) = get_calc 1; show_pt pt;
 "------ interSteps after appendFormula ---------------------------";
 interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*);
 (*...and these are the internals*)
 val ((pt,p),_) = get_calc 1; show_pt pt;
 val (_,_,lastpos) =detailstep pt p;
 if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()
-else raise error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
+else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
 "------ Detail_Set -----------------------------------------------";
 "------ Detail_Set -----------------------------------------------";
 "------ Detail_Set -----------------------------------------------";

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37967	bd4f7a35e892
child 38043	6a36acec95d9