wneuper/isa: comparison src/Tools/isac/Interpret/appl.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 (rew_ord':rew_ord',erls,ca)
 | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
 (rew_ord',erls,ca)
 | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
 (rew_ord',erls, ca)
-| rew_info rls = raise error ("rew_info called with '"^rls2str rls^"'");
+| rew_info rls = error ("rew_info called with '"^rls2str rls^"'");
 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
 fun from_pblobj_or_detail_thm thm' p pt =
 let val (pbl,p',rls') = par_pbl_det pt p
 in if pbl
 		 then [pred]
 	       else (map fst) (get_assumptions_ pt (p,Res))
 in (bdv, pred) end
 | mk_set thy _ _ l _ =
-raise error ("check_elementwise: no set "^
+error ("check_elementwise: no set "^
 		 (Syntax.string_of_term (thy2ctxt thy) l));
 (*> val consts = str2term "[x=#4]";
 > val pred = str2term "Assumptions";
 > val pt = union_asm pt p
 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
 val {rew_ord'=ro',erls=erls,...} =
 get_met (get_obj g_metID pt pp);
 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
 Frm => (get_obj g_form pt p, p)
 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
-	    | _ => raise error ("applicable_in: call by "^
+	    | _ => error ("applicable_in: call by "^
 				(pos'2str (p,p_)));
 in
 let val subst = subs2subst thy subs;
 	val subs' = subst2subs' subst;
 in case rewrite_inst_ thy (assoc_rew_ord ro') erls
 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
 val thy = assoc_thy thy';
 val f = case p_ of
 Frm => get_obj g_form pt p
 	    | Res => (fst o (get_obj g_result pt)) p
-	    | _ => raise error ("applicable_in Rewrite: call by "^
+	    | _ => error ("applicable_in Rewrite: call by "^
 				(pos'2str (p,p_)));
 in if msg = "OK"
 then
 ((*tracing("### applicable_in rls'= "^rls');*)
 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
 get_met (get_obj g_metID pt pp);
 (*val put_asm = true;*)
 val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)
 Frm => (get_obj g_form pt p, p)
 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
-	    | _ => raise error ("applicable_in: call by "^
+	    | _ => error ("applicable_in: call by "^
 				(pos'2str (p,p_)));
 in case rewrite_ thy (assoc_rew_ord ro') erls
 		   (*put_asm*)false (assoc_thm' thy thm') f of
 SOME (f',asm) => Appl (
 	   Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
 val thy' = (get_obj g_domID pt pp):theory';
 val thy = assoc_thy thy';
 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
 val f = case p_ of Frm => get_obj g_form pt p
 		     | Res => (fst o (get_obj g_result pt)) p
-		     | _ => raise error ("applicable_in: call by "^
+		     | _ => error ("applicable_in: call by "^
 					 (pos'2str (p,p_)));
 in
 let val subst = subs2subst thy subs
 	  val subs' = subst2subs' subst
 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
 val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
 get_met (get_obj g_metID pt pp);
 val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)
 Frm => (get_obj g_form pt p, p)
 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
-	    | _ => raise error ("applicable_in: call by "^
+	    | _ => error ("applicable_in: call by "^
 				(pos'2str (p,p_)));
 in
 let val subst = subs2subst thy subs;
 	val subs' = subst2subs' subst;
 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
 val pp = par_pblobj pt p;
 val thy' = (get_obj g_domID pt pp):theory';
 val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)
 Frm => (get_obj g_form pt p, p)
 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
-	    | _ => raise error ("applicable_in: call by "^
+	    | _ => error ("applicable_in: call by "^
 				(pos'2str (p,p_)));
 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
 SOME (f',asm) =>
 	((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
 	 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
 	let val pp = par_pblobj pt p
 	    val thy' = (get_obj g_domID pt pp):theory'
 	    val f = case p_ of
 			Frm => get_obj g_form pt p
 		      | Res => (fst o (get_obj g_result pt)) p
-		      | _ => raise error ("applicable_in: call by "^
+		      | _ => error ("applicable_in: call by "^
 					  (pos'2str (p,p_)));
 	in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
 	       SOME (f',asm) =>
 	       Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
 	     | NONE => Notappl (rls^" not applicable") end
 | applicable_in p pt (End_Ruleset) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str End_Ruleset))
 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
 *)
 | applicable_in (p,p_) pt (m as Calculate op_) =
 	    | NONE => Notappl (sube2str sube^" not applicable")
 end
 ------------------*)
 | applicable_in p pt (Apply_Assumption cts') =
-(raise error ("applicable_in: not impl. for "^
+(error ("applicable_in: not impl. for "^
 	       (tac2str (Apply_Assumption cts'))))
 (*'logical' applicability wrt. script in locate: Inconsistent?*)
 | applicable_in (p,p_) pt (m as Take ct') =
 if member op = [Pbl,Met] p_
 	       SOME ct => Appl (Take' (term_of ct))
 	     | NONE => Notappl ("syntax error in "^ct'))
 end
 | applicable_in p pt (Take_Inst ct') =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Take_Inst ct')))
 | applicable_in p pt (Group (con, ints)) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Group (con, ints))))
 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
 if member op = [Pbl,Met] p_
 then (*maybe Apply_Method has already been done*)
 else (*somewhere later in the script*)
 Appl (Subproblem' ((domID, pblID, e_metID), [],
 			  e_term, [], subpbl domID pblID))
 | applicable_in p pt (End_Subproblem) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (End_Subproblem)))
 | applicable_in p pt (CAScmd ct') =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (CAScmd ct')))
 | applicable_in p pt (Split_And) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Split_And)))
 | applicable_in p pt (Conclude_And) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Conclude_And)))
 | applicable_in p pt (Split_Or) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Split_Or)))
 | applicable_in p pt (Conclude_Or) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Conclude_Or)))
 | applicable_in (p,p_) pt (Begin_Trans) =
 let
 val (f,p) = case p_ of   (*p 12.4.00 unnecessary*)
 	                             (*_____ implizit Take in gen*)
 	Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
-| _ => raise error ("applicable_in: call by "^
+| _ => error ("applicable_in: call by "^
 				(pos'2str (p,p_)));
 val thy' = get_obj g_domID pt (par_pblobj pt p);
 in (Appl (Begin_Trans' f))
-handle _ => raise error ("applicable_in: Begin_Trans finds \
+handle _ => error ("applicable_in: Begin_Trans finds \
 \syntaxerror in '"^(term2str f)^"'") end
 (*TODO: check parent branches*)
 | applicable_in (p,p_) pt (End_Trans) =
 let val thy' = get_obj g_domID pt (par_pblobj pt p);
 	\the beginning of a transitive sequence"
 	 (*TODO: check parent branches*)
 end
 | applicable_in p pt (Begin_Sequ) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Begin_Sequ)))
 | applicable_in p pt (End_Sequ) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (End_Sequ)))
 | applicable_in p pt (Split_Intersect) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Split_Intersect)))
 | applicable_in p pt (End_Intersect) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (End_Intersect)))
 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
 val (vvv,ppp) = vp;
 val Check_elementwise pred = m;
 in Appl (Or_to_List' (f, ls)) end)
 handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
 end
 | applicable_in p pt (Collect_Trues) =
-raise error ("applicable_in: not impl. for "^
+error ("applicable_in: not impl. for "^
 	       (tac2str (Collect_Trues)))
 | applicable_in p pt (Empty_Tac) =
 Notappl "Empty_Tac is not applicable"
 | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
 | applicable_in p pt End_Proof' = Appl End_Proof''
 | applicable_in _ _ m =
-raise error ("applicable_in called for "^(tac2str m));
+error ("applicable_in called for "^(tac2str m));
 (*WN060614 unused*)
 fun tac2tac_ pt p m =
 case applicable_in p pt m of
 	Appl (m') => m'
-| Notappl _ => raise error ("tac2mstp': fails with"^
+| Notappl _ => error ("tac2mstp': fails with"^
 				  (tac2str m));

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38015	67ba02dffacc
child 38050	4c52ad406c20