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

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 "#Given" => #Given (ppc:'a ppc)
 | "#Where" => #Where (ppc:'a ppc)
 | "#Find" => #Find (ppc:'a ppc)
 | "#With" => #With (ppc:'a ppc)
 | "#Relate" => #Relate (ppc:'a ppc)
-| _  => raise error ("sel_ppc tried to select by '"^sel^"'");
+| _  => error ("sel_ppc tried to select by '"^sel^"'");
 fun repl_sel_ppc sel
 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
 case sel of
 "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
 | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
 | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
 | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
 | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
-| _  => raise error ("repl_sel_ppc tried to select by '"^sel^"'");
+| _  => error ("repl_sel_ppc tried to select by '"^sel^"'");
 fun add_sel_ppc thy sel
 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
 case sel of
 "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
 | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}
 | "#Find"  => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
 | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
 | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
-| _  => raise error ("add_sel_ppc tried to select by '"^sel^"'");
+| _  => error ("add_sel_ppc tried to select by '"^sel^"'");
 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
 (*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*)
 (let val (hd,args) = strip_comb t
 in if is_dsc hd
 then (hd, args)
 else (e_term, [t])    (*??? 9.01 just copied*)
 end)
-handle _ => raise error ("split_dsc: called with "^
+handle _ => error ("split_dsc: called with "^
 			   (Syntax.string_of_term (thy2ctxt' "Isac") t));
 (*
 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
 > split_dsc t1;
 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
 in (d, ts) end;*)
 (*WN.8.12.03 quick for prep_ori'*)
 fun split_dsc' t =
 (let val dsc $ var = t
 in var end)
-handle _ => raise error ("split_dsc': called with "^term2str t);
+handle _ => error ("split_dsc': called with "^term2str t);
 (*9.3.00*)
 (* split a term into description and (id | structured variable)
 for pbt, met.ppc *)
 fun split_did t =
 (let val (hd,[arg]) = strip_comb t
 in (hd,arg) end)
-handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
+handle _ => error ("split_did: doesn't match (hd,[arg]) for t = "
 ^(Syntax.string_of_term (thy2ctxt' "Script") t));
 (*create output-string for itm_*)
 else if d mem (get_dsc_in dscs "#Find")
 	 then ("#Find",d,ts)
 else if d mem (get_dsc_in dscs "#Relate")
 	      then ("#Relate",d,ts)
 	    else ("#undef",d,ts);
-(* 28.1.00      raise error ("add_field: '"^
+(* 28.1.00      error ("add_field: '"^
 			      (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 			      "' not in ppc-description ");         *)
 ------9.3. *)
 (* 9.3.00
 fun add_field thy pbt (d,ts) =
 let fun eq d pt = (d = (fst o snd) pt);
 in case filter (eq d) pbt of
 [(fi,(dsc,_))] => (fi,d,ts)
 | [] => ("#undef",d,ts)   (*may come with met.ppc*)
-| _ => raise error ("add_field: "^
+| _ => error ("add_field: "^
 			 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 			 " more than once in pbt")
 end;
 (*. take over field from met.ppc at 'Specify_Method' into ori,
 let fun eq d pt = (d = (fst o snd) pt);
 fun repl mpc (i,v,_,d,ts) =
 case filter (eq d) mpc of
 	[(fi,(dsc,_))] => [(i,v,fi,d,ts)]
 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
-(*raise error ("add_field': "^
+(*error ("add_field': "^
 		     (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 		     " not in met"*)
-| _ => raise error ("add_field': "^
+| _ => error ("add_field': "^
 			 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 			 " more than once in met");
 in (flat ((map (repl mpc)) ori)):ori list end;
 (*.mark an element with the position within a plateau;
 a plateau with length 1 is marked with 0        .*)
-fun mark eq [] = raise error "mark []"
+fun mark eq [] = error "mark []"
 | mark eq xs =
 let
 fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
 | mar xx eq (x::x'::xs) n =
 if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)
 > val xs = [1,1,1,2,4,4,4];
 > coll (op=) xs;
 val it = [1,2,4] : int list
 *)
-fun max [] = raise error "max of []"
+fun max [] = error "max of []"
 | max (y::ys) =
 let fun mx x [] = x
 	| mx x (y::ys) = if x < y then mx y ys else mx x ys;
 in mx y ys end;
-fun gen_max _ [] = raise error "gen_max of []"
+fun gen_max _ [] = error "gen_max of []"
 | gen_max ord (y::ys) =
 let fun mx x [] = x
 	| mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
 in mx y ys end;
 fun replace_0 vm [0] = intsto vm
 | replace_0 vm vs = vs;
-fun add_id [] = raise error "add_id []"
+fun add_id [] = error "add_id []"
 | add_id xs =
 let fun add n [] = []
 	| add n (x::xs) = (n,x) :: add (n+1) xs;
 in add 1 xs end;
 (*
 | prep_ori fmz thy pbt =
 let
 val ctopts = map (parse thy) fmz
 val _= (*FIXME.WN060916 improve error report*)
 	if null (filter is_none ctopts) then ()
-	else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
+	else error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
 val dts = map ((split_dts thy) o term_of o the) ctopts
 val ori = map (add_field thy pbt) dts;
 (*    val ori = map (flat3 o (pair "#undef")) dts; *)
 val ori' = add_variants ori;
 val maxv = max (map fst ori');
 (Const ("Descript.solveFor","RealDef.real => Tools.una"),
 Free ("v_","RealDef.real")))] : (string * (term * term)) list*)
 	val fi = filter (eq "#Find") dsc_dats;
 	val fi = (case fi of
-		     [] => [](*28.8.01: ["tool"] ...// raise error
+		     [] => [](*28.8.01: ["tool"] ...// error
 			("prep_pbt: no '#Find' in "^(strs2str pblID))*)
 (* val ((_,fi')::[]) = fi;
 *)
 		   | ((_,fi')::[]) =>
 		     ((map (split_did o term_of o the o (parse thy)) fi')
-		     handle _ => raise error
+		     handle _ => error
 			("prep_pbt: syntax error in '#Find' of "^
 			 (strs2str pblID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Find' in "^
+		     (error ("prep_pbt: more than one '#Find' in "^
 				  (strs2str pblID))));
 	val fi = map (pair "#Find") fi;
 	val re = filter (eq "#Relate") dsc_dats;
 	val re = (case re of
 		     [] => []
 		   | ((_,re')::[]) =>
 		     ((map (split_did o term_of o the o (parse thy)) re')
-		     handle _ => raise error
+		     handle _ => error
 			("prep_pbt: syntax error in '#Relate' of "^
 			 (strs2str pblID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Relate' in "^
+		     (error ("prep_pbt: more than one '#Relate' in "^
 				  (strs2str pblID))));
 	val re = map (pair "#Relate") re;
 	val wh = filter (eq "#Where") dsc_dats;
 	val wh = (case wh of
 		     [] => []
 		   | ((_,wh')::[]) =>
 		     ((map (parse_patt thy) wh')
-		      handle _ => raise error
+		      handle _ => error
 			("prep_pbt: syntax error in '#Where' of "^
 			 (strs2str pblID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Where' in "^
+		     (error ("prep_pbt: more than one '#Where' in "^
 				  (strs2str pblID))));
 in ({guh=guh,mathauthors=maa,init=init,
 	 thy=thy,cas= case ca of NONE => NONE
 			       | SOME s =>
 				 SOME ((term_of o the o (parse thy)) s),
 	val gi = filter (eq "#Given") ppc;
 	val gi = (case gi of
 		     [] => []
 		   | ((_,gi')::[]) =>
 		     ((map (split_did o term_of o the o (parse thy)) gi')
-		     handle _ => raise error
+		     handle _ => error
 			("prep_pbt: syntax error in '#Given' of "^
 			 (strs2str metID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Given' in "^
+		     (error ("prep_pbt: more than one '#Given' in "^
 				  (strs2str metID))));
 	val gi = map (pair "#Given") gi;
 	val fi = filter (eq "#Find") ppc;
 	val fi = (case fi of
-		     [] => [](*28.8.01: ["tool"] ...// raise error
+		     [] => [](*28.8.01: ["tool"] ...// error
 			("prep_pbt: no '#Find' in "^(strs2str metID))*)
 		   | ((_,fi')::[]) =>
 		     ((map (split_did o term_of o the o (parse thy)) fi')
-		     handle _ => raise error
+		     handle _ => error
 			("prep_pbt: syntax error in '#Find' of "^
 			 (strs2str metID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Find' in "^
+		     (error ("prep_pbt: more than one '#Find' in "^
 				  (strs2str metID))));
 	val fi = map (pair "#Find") fi;
 	val re = filter (eq "#Relate") ppc;
 	val re = (case re of
 		     [] => []
 		   | ((_,re')::[]) =>
 		     ((map (split_did o term_of o the o (parse thy)) re')
-		     handle _ => raise error
+		     handle _ => error
 			("prep_pbt: syntax error in '#Relate' of "^
 			 (strs2str metID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Relate' in "^
+		     (error ("prep_pbt: more than one '#Relate' in "^
 				  (strs2str metID))));
 	val re = map (pair "#Relate") re;
 	val wh = filter (eq "#Where") ppc;
 	val wh = (case wh of
 		     [] => []
 		   | ((_,wh')::[]) =>
 		     ((map (parse_patt thy) wh')
-		     handle _ => raise error
+		     handle _ => error
 			("prep_pbt: syntax error in '#Where' of "^
 			 (strs2str metID)))
 		   | _ =>
-		     (raise error ("prep_pbt: more than one '#Where' in "^
+		     (error ("prep_pbt: more than one '#Where' in "^
 				  (strs2str metID))));
 	val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
 in ({guh=guh,mathauthors=maa,init=init,
 	 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
 	 calc = if scr = "empty_script" then []
 *)
 | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
 (case find_first (eq1 d) pbt of
 (* val SOME (_,(_,id)) = find_first (eq1 d) pbt;
 *)
-	SOME (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
+	SOME (_,(_,id)) => error "chk_: ((i,vats,b,f,Cor ((d,vs),\
 				   \(id, pbl_ids' d vs))):itm)"
 | NONE => (i,vats,false,f,Sup (d,[vs])));
 (* chk_ thy pbt i
 *)
 | NoMatch_ => refins'' thy pblRD itms pbls' pts end;
 (*. apply a fun to a ptyps node; copied from get_py .*)
 fun app_ptyp f (d:pblID) _ [] =
-raise error ("app_ptyp not found: "^(strs2str d))
+error ("app_ptyp not found: "^(strs2str d))
 | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =
 if k=k' then f p
 else app_ptyp f d ([k]:pblRD) pys
 | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') =
 if k=k' then app_ptyp f d ks pys
 (*.make a guh from a reference to an element in the kestore;
 EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
 fun pblID2guh (pblID:pblID) =
 (((#guh o get_pbt) pblID)
-handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
+handle _ => error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
 fun metID2guh (metID:metID) =
 (((#guh o get_met) metID)
-handle _ => raise error ("metID2guh: no 'Met_' for '"^
+handle _ => error ("metID2guh: no 'Met_' for '"^
 			      strs2str' metID ^ "'"));
 fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
 | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
 | kestoreID2guh ketype kestoreID =
-raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
+error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
 		 strs2str' kestoreID ^ "'");
 fun show_pblguhs () =
 (print_depth 999;
 (tracing o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38015	67ba02dffacc
child 38036	02a9b2540eb7