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

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 let datatype switch = Appl | Noap
 	fun rew_once lim rts t Noap [] =
 	    (case goal of
 		 NONE => rts
 	       | SOME g =>
-		 raise error ("make_deriv: no derivation for "^(term2str t)))
+		 error ("make_deriv: no derivation for "^(term2str t)))
 	  | rew_once lim rts t Appl [] =
 	    (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
 	  (*| Seq _ => rts) FIXXXXXME 14.3.03*)
 	  | rew_once lim rts t apno rs' =
 	    (case goal of
 			    val _ = if not (!trace_rewrite) then () else
 				    tracing("### calc. to: " ^ (term2str t'))
 			    val r' = Thm (thmid, tm)
 			in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
 			end)
-		       handle _ => raise error "derive_norm, Calc: no rewrite"
+		       handle _ => error "derive_norm, Calc: no rewrite"
 		end
 (* TODO.WN080222: see rewrite__set_
 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
 | Cal1 (cc as (op_,_)) =>
 	  (let val _= if !trace_rewrite andalso i < ! depth then
 	       let
 		 val pairopt =
 		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
 		   ((#erls o rep_rls) rls) put_asm thm' ct;
 		 val _ = if pairopt <> NONE then ()
-			 else raise error("rewrite_set_, rewrite_ \""^
+			 else error("rewrite_set_, rewrite_ \""^
 			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
 		 val _ = if ! trace_rewrite andalso i < ! depth
 			   then tracing((idt"="(i+1))^" cal1. to: "^
 					(term2str ((fst o the) pairopt)))
 			 else()
 Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat,
 	  rew_ord=rew_ord};
 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)
 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
-| sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
+| sym_Thm r = error ("sym_Thm: not for "^(rule2str r));
 (*
 val th =  Thm ("real_one_collect",num_str @{thm real_one_collect});
 sym_Thm th;
 val th =
 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
 fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2
 | eq_Thm (Thm (id1,_), _) = false
 | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2
 | eq_Thm (Rls_ r1, _) = false
-| eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^
+| eq_Thm (r1, r2) = error ("eq_Thm: called with '"^
 				(rule2str r1)^"' '"^(rule2str r2)^"'");
 fun distinct_Thm r = gen_distinct eq_Thm r;
 fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))
 handle _ => false;
 fun part2guh ([str]:theID) =
 (case str of
 	"Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
-| str => raise error ("thy2guh: called with '"^str^"'"))
+| str => error ("thy2guh: called with '"^str^"'"))
-| part2guh theID = raise error ("part2guh called with theID = "
+| part2guh theID = error ("part2guh called with theID = "
 				  ^ theID2str theID);
 fun part2filename str = part2guh str ^ ".xml" : filename;
 fun thy2guh ([part, thyID]:theID) =
 (case part of
 	"Isabelle" => "thy_isab_" ^ thyID : guh
 | "IsacScripts" => "thy_scri_" ^ thyID
 | "IsacKnowledge" => "thy_isac_" ^ thyID
-| str => raise error ("thy2guh: called with '"^str^"'"))
+| str => error ("thy2guh: called with '"^str^"'"))
-| thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'");
+| thy2guh theID = error ("thy2guh called with '"^strs2str' theID^"'");
 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;
 fun thypart2guh ([part, thyID, thypart]:theID) =
 case part of
 	"Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
-| str => raise error ("thypart2guh: called with '"^str^"'");
+| str => error ("thypart2guh: called with '"^str^"'");
 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;
 (*.convert the data got via contextToThy to a globally unique handle
 there is another way to get the guh out of the 'theID' in the hierarchy.*)
 fun thm2guh (isa, thyID:thyID) (thmID:thmID) =
 	"thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
 | "IsacKnowledge" =>
 	"thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
 | "IsacScripts" =>
 	"thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
-| str => raise error ("thm2guh called with isa = '"^isa^
+| str => error ("thm2guh called with isa = '"^isa^
 			  "' for thm = "^thmID^"'");
 fun thm2filename (isa_thyID: string * thyID) thmID =
 (thm2guh isa_thyID thmID) ^ ".xml" : filename;
 fun rls2guh (isa, thyID:thyID) (rls':rls') =
 	    "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh
 | "IsacKnowledge" =>
 	    "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
 | "IsacScripts" =>
 	    "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'
-| str => raise error ("rls2guh called with isa = '"^isa^
+| str => error ("rls2guh called with isa = '"^isa^
 			  "' for rls = '"^rls'^"'");
 	fun rls2filename (isa, thyID) rls' =
 rls2guh (isa, thyID) rls' ^ ".xml" : filename;
 fun cal2guh (isa, thyID:thyID) calID =
 	"thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh
 | "IsacKnowledge" =>
 	"thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
 | "IsacScripts" =>
 	"thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID
-| str => raise error ("cal2guh called with isa = '"^isa^
+| str => error ("cal2guh called with isa = '"^isa^
 			  "' for cal = '"^calID^"'");
 fun cal2filename (isa, thyID:thyID) calID =
 cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;
 fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =
 	"thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
 | "IsacKnowledge" =>
 	"thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
 | "IsacScripts" =>
 	"thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'
-| str => raise error ("ord2guh called with isa = '"^isa^
+| str => error ("ord2guh called with isa = '"^isa^
 			  "' for ord = '"^rew_ord'^"'");
 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =
 ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;
 in case find_first (thy_contains_thm str) startsearch of
 	   SOME (thy',_) => ("IsacKnowledge", thy')
 	 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
 		     SOME (thyID,_) => ("Isabelle", thyID)
 		   | NONE =>
-		     raise error ("thy_containing_thm: theorem '"^str^
+		     error ("thy_containing_thm: theorem '"^str^
 				  "' not in !theory' above thy '"^thy'^"'"))
 end;
 (*.which theory below thy' contains a ruleset;
 				      ((#1 o #2) : rls' * (theory' * rls)
 						   -> theory'))
 				     (rev (!ruleset'))
 in case assoc (startsearch, rls') of
 	   SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
-	 | _ => raise error ("thy_containing_rls : rls '"^rls'^
+	 | _ => error ("thy_containing_rls : rls '"^rls'^
 			     "' not in !rulset' above thy '"^thy'^"'")
 end;
 (* val (thy', termop) = (thyID, termop);
 *)
 fun thy_containing_cal (thy':theory') termop =
 			    dropthys
 	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
 				      (#1 : calc -> string)) (rev (!calclist'))
 in case assoc (startsearch, strip_thy termop) of
 	   SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
-	 | _ => raise error ("thy_containing_rls : rls '"^termop^
+	 | _ => error ("thy_containing_rls : rls '"^termop^
 			     "' not in !calclist' above thy '"^thy'^"'")
 end
 end;
 (* print_depth 99; map #1 startsearch; print_depth 3;
 (*.not only for thydata, but also for thy's etc.*)
 fun theID2guh (theID:theID) =
 case length theID of
-	0 => raise error ("theID2guh: called with theID = "^strs2str' theID)
+	0 => error ("theID2guh: called with theID = "^strs2str' theID)
 | 1 => part2guh theID
 | 2 => thy2guh theID
 | 3 => thypart2guh theID
 | 4 => let val [isa, thyID, typ, elemID] = theID
 	     in case typ of
 		    "Theorems" => thm2guh (isa, thyID) elemID
 		  | "Rulesets" => rls2guh (isa, thyID) elemID
 		  | "Calculations" => cal2guh (isa, thyID) elemID
 		  | "Orders" => ord2guh (isa, thyID) elemID
 		  | "Theorems" => thy2guh [isa, thyID]
-		  | str => raise error ("theID2guh: called with theID = "^
+		  | str => error ("theID2guh: called with theID = "^
 					strs2str' theID)
 	     end
-| n => raise error ("theID2guh called with theID = "^strs2str' theID);
+| n => error ("theID2guh called with theID = "^strs2str' theID);
 (*.filenames not only for thydata, but also for thy's etc.*)
 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;
 fun guh2theID (guh:guh) =
 let val guh' = explode guh
 	val part = implode (take_fromto 1 4 guh')
 	val isa = implode (take_fromto 5 9 guh')
 in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
-then raise error ("guh '"^guh^"' does not begin with \
+then error ("guh '"^guh^"' does not begin with \
 				     \exp_ | thy_ | pbl_ | met_")
 else let val chap = case isa of
 				"isab_" => "Isabelle"
 			      | "scri_" => "IsacScripts"
 			      | "isac_" => "IsacKnowledge"
 			      | _ =>
-				raise error ("guh2theID: '"^guh^
+				error ("guh2theID: '"^guh^
 					     "' does not have isab_ | scri_ | \
 					     \isac_ at position 5..9")
 		val rest = takerest (9, guh')
 		val thyID = takewhile [] (not o (curry op= "-")) rest
 		val rest' = dropuntil (curry op= "-") rest
 			       "-thm-" => "Theorems"
 			     | "-rls-" => "Rulesets"
 			     | "-cal-" => "Operations"
 			     | "-ord-" => "Orders"
 			     | str =>
-			       raise error ("guh2theID: '"^guh^"' has '"^sect^
+			       error ("guh2theID: '"^guh^"' has '"^sect^
 					    "' instead -thm- | -rls- | \
 					    \-cal- | -ord-")
 		   in [chap, implode thyID, sect', implode
 						       (takerest (5, rest'))]
 		   end
 fun guh2rewtac (guh:guh) ([] : subs) =
 let val [isa, thy, sect, xstr] = guh2theID guh
 in case sect of
 	   "Theorems" => Rewrite (xstr, "")
 	 | "Rulesets" => Rewrite_Set xstr
-	 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
+	 | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
 end
 | guh2rewtac (guh:guh) subs =
 let val [isa, thy, sect, xstr] = guh2theID guh
 in case sect of
 	   "Theorems" => Rewrite_Inst (subs, (xstr, ""))
 	 | "Rulesets" => Rewrite_Set_Inst (subs,  xstr)
-	 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'")
+	 | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
 end;
 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
 val it = Rewrite ("constant_mult_square", "") : tac
 > guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];
 val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac

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