wneuper/isa: comparison src/Tools/isac/calcelems.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
 val e_rule =
 Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
 fun id_of_thm (Thm (id, _)) = id
-| id_of_thm _ = raise error "id_of_thm";
+| id_of_thm _ = error "id_of_thm";
 fun thm_of_thm (Thm (_, thm)) = thm
-| thm_of_thm _ = raise error "thm_of_thm";
+| thm_of_thm _ = error "thm_of_thm";
 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
 (strip_thy thmid1) = (strip_thy thmid2);
 (*version typed weaker WN100910*)
 fun eq_thmI' ((thmid1, _), (thmid2, _)) =
 val e_theID = ["e_theID"];
 val theID2str = strs2str;
 (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
 fun theID2thyID (theID:theID) =
 if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
-else raise error ("theID2thyID called with "^ theID2str theID);
+else error ("theID2thyID called with "^ theID2str theID);
 (*the key into the hierarchy ob problems*)
 type pblID = string list; (* domID::...*)
 val e_pblID = ["e_pblID"]:pblID;
 val pblID2str = strs2str;
 | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
 (*asm_thm=asm_thm,*)rules=rules,scr=scr}
 | rep_rls Erls = rep_rls e_rls
 | rep_rls (Rrls {id,...})  = rep_rls e_rls
-(*raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
+(*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
 (*| rep_rls (Seq {id,...})  =
-raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
+error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
 --1.7.03*)
 fun rep_rrls
 	(Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
 	       scr=Rfuns
 		       {attach_form,init_state,locate_rule,
 			next_rule,normal_form}}) =
 {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
 rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
 | rep_rrls (Rls {id,...}) =
-raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
+error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
 | rep_rrls (Seq {id,...}) =
-raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
+error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 			rules =rs,scr=sc}) r =
 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 	 rules = rs @ r,scr=sc}:rls)
 | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 			rules =rs,scr=sc}) r =
 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 	 rules = rs @ r,scr=sc}:rls)
 | append_rls id (Rrls _) _ =
-raise error ("append_rls: not for reverse-rewrite-rule-set "^id);
+error ("append_rls: not for reverse-rewrite-rule-set "^id);
 (*. are _atomic_ rules equal ?.*)
 (*WN080102 compare eqrule ?!?*)
 fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
 | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
 	      calc=ca1 @ ((#calc o rep_rls) r2),
 	      (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
 	      rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
 	      scr=sc1}:rls)
 | merge_rls _ _ _ =
-raise error "merge_rls: not for reverse-rewrite-rule-sets\
+error "merge_rls: not for reverse-rewrite-rule-sets\
 		\and not for mixed Rls -- Seq";
 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 		     (*asm_thm=at,*)rules =rs,scr=sc}) r =
 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 	 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
 | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 		     (*asm_thm=at,*)rules =rs,scr=sc}) r =
 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
 	 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
 	 scr=sc}:rls)
-| remove_rls id (Rrls _) _ = raise error
+| remove_rls id (Rrls _) _ = error
 ("remove_rls: not for reverse-rewrite-rule-set "^id);
 (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
 val it = [1, 2] : int list*)
 fun mem_rls id rls =
 case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
 	SOME _ => true | NONE => false;*)
 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
-| memrls r _ = raise error ("memrls: incomplete impl. r= "^(rule2str r));
+| memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
 fun rls_get_thm rls (id: xstring) =
 case find_first (curry eq_rule e_rule)
 		    ((#rules o rep_rls) rls) of
 	SOME thm => SOME thm | NONE => NONE;
-fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known")
+fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
 | assoc' ((keyi, xi) :: pairs, key) =
 if key = keyi then SOME xi else assoc' (pairs, key);
 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
-handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");*)
+handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
 fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
 (theory ((implode o (curry takelast 4) o explode) thy))
-handle _ => raise error ("ME_Isa: thy '" ^ thy ^ "' not in system");
+handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
 overlays by re-using an identifier in different thys.*)
 fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
-handle _ => raise error ("ME_Isa: '"^rls^"' not in system");
+handle _ => error ("ME_Isa: '"^rls^"' not in system");
 (*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
-handle _ => raise error ("ME_Isa: '"^rls^"' not in system");*)
+handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
 (*.overwrite an element in an association list and pair it with a thyID
 in order to create the thy_hierarchy;
 overwrites existing rls' even if they are defined in a different thy;
 this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
 fun overwritelthy thy (al, bl:(rls' * rls) list) =
 let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
 in overwritel (al, bl') end;
 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
-handle _ => raise error ("ME_Isa: rew_ord '"^ro^"' not in system");
+handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
 (*get the string for stac from rule*)
-fun assoc_calc ([], key) = raise error ("assoc_calc: '"^ key ^"' not found")
+fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
 if key = keyi then calc else assoc_calc (pairs, key);
 (*only used for !calclist'...*)
-fun assoc1 ([], key) = raise error ("assoc1 (for met.calc=): '"^ key
+fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
 				    ^"' not found")
 | assoc1 ((all as (keyi, _)) :: pairs, key) =
 if key = keyi then all else assoc1 (pairs, key);
 (*TODO.WN080102 clarify usage of type cal and type calc..*)
 fun calID2calcID (calID : calID) =
-let fun ass [] = raise error ("calID2calcID: "^calID^"not in calclist'")
+let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
 	  | ass ((calci, (cali, eval_fn))::ids) =
 	    if calID = cali then calci
 	    else ass ids
 in ass (!calclist') : calcID end;

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38024	20231cdf39e7
child 38036	02a9b2540eb7