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

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 (ptree * pos');    (*the calc-state resulting from the application of tacis*)
 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
-| f_mout thy _ = raise error "f_mout: not called with formula";
+| f_mout thy _ = error "f_mout: not called with formula";
 (*.is the calchead complete ?.*)
 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
 foldl and_ (true, map #3 its) andalso
 | is_error _ = true;
 (* 30.1.00 ---
 fun ct_in (Syn (c)) = c
 | ct_in (Typ (c)) = c
-| ct_in _ = raise error "ct_in called for Cor .. Sup";
+| ct_in _ = error "ct_in called for Cor .. Sup";
 --- *)
 (*#############################################################*)
 (*#############################################################*)
 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
 	    | miss => SOME (getr_ct thy (hd miss))
 else
 	 case find_first (test_subset (hd icl)) vors of
 	     (* val SOME ori = find_first (test_subset (hd icl)) vors;
 	      *)
-	     NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
+	     NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
 	   | SOME ori => SOME (geti_ct thy ori (hd icl))
 end
 end;
 fun mk_delete thy "#Given"  itm_ = Del_Given   (itm_out thy itm_)
 | mk_delete thy "#Find"   itm_ = Del_Find    (itm_out thy itm_)
 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
 | mk_delete thy str _ =
-raise error ("mk_delete: called with field '"^str^"'");
+error ("mk_delete: called with field '"^str^"'");
 fun mk_additem "#Given" ct = Add_Given ct
 | mk_additem "#Find"  ct = Add_Find ct
 | mk_additem "#Relate"ct = Add_Relation ct
 | mk_additem str _ =
-raise error ("mk_additem: called with field '"^str^"'");
+error ("mk_additem: called with field '"^str^"'");
 (*3.3.--
 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
 (id,vt,cl,sl,Cor (d,ts)):itm
 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
-raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
+error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
 	       " not not for Syn (s:cterm')")
 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
-raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
+error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
 	       " not not for Typ (s:cterm')")
 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
 (id,vt,cl,sl,Fal (d,ts))
 | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =
 (id,vt,cl,sl,Inc (d,ts))
 val complete = if eq_set op = (ts', all) then true else false;
 in case itm_ of
 (Cor _) =>
 	(if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
 	 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
-| (Syn c)     => raise error ("ori_2itm wants to overwrite "^c)
+| (Syn c)     => error ("ori_2itm wants to overwrite "^c)
-| (Typ c)     => raise error ("ori_2itm wants to overwrite "^c)
+| (Typ c)     => error ("ori_2itm wants to overwrite "^c)
 | (Inc _) => if complete
 	       then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
 	       else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
 | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
 	 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
 val _ = show_types:= s
 in msg end;
-fun maxl [] = raise error "maxl of []"
+fun maxl [] = error "maxl of []"
 | maxl (y::ys) =
 let fun mx x [] = x
 	| mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
 in mx y ys end;
 (*.match each pat of the model-pattern with an actual argument;
 precondition: copy-named vars are filtered out.*)
 fun matc thy ([]:pat list)  _  (oris:preori list) = oris
 | matc thy pbt [] _ =
 (tracing (dashs 70);
-raise error ("actual arg(s) missing for '"^pats2str pbt
+error ("actual arg(s) missing for '"^pats2str pbt
 		 ^"' i.e. should be 'copy-named' by '*_._'"))
 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
 (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
 	   (thy,  pbt',                    ags,     []);
 (*recursion..*)
 	   val vals = map sel oris
 	   val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
 else ([1], field, dsc, [t])
 	)
-handle _ => raise error ("cpy_nam: for "^(term2str t));
+handle _ => error ("cpy_nam: for "^(term2str t));
 (*.match the actual arguments of a SubProblem with a model-pattern
 and create an ori list (in root-pbl created from formalization).
 expects ags:pats = 1:1, while copy-named are filtered out of pats;
 if no 1:1 the exn raised by matc/mtc and handled at call.
 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
 fun overwrite_ppc thy itm ppc =
 let
 fun repl ppc' (_,_,_,_,itm_) [] =
-raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
+error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
 " not found")
 | repl ppc' itm (p::ppc) =
 	if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
 	else repl (ppc' @ [p]) itm ppc
 in repl [] itm ppc end;
 (*. output the headline to a ppc .*)
 fun header p_ pI mI =
 case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
 	     | Met => Method mI
-	     | pos => raise error ("header called with "^ pos_2str pos);
+	     | pos => error ("header called with "^ pos_2str pos);
 (* test-printouts ---
 val _=tracing("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
 	     nxt, Safe,pt) end
 end
 (* itms2itemppc thy [](*mpc*) pre
 *)
 | specify m' _ _ _ =
-raise error ("specify: not impl. for "^tac_2str m');
+error ("specify: not impl. for "^tac_2str m');
 (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
 val (sel, Add_Find  ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
 *)
 fun nxt_specif_additem sel ct (ptp as (pt,(p,Pbl))) =
 pre
 *)
 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
-			      handle _ => raise error ("ori2Coritm: dsc "^
+			      handle _ => error ("ori2Coritm: dsc "^
 						term2str d^
 						"in ori, but not in pbt")
 			      ,ts))):itm;
 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
 ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
 in  (*FIXXXME: check if met can still be parsed*)
 	([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
 	 (pt, pos)) end
 | nxt_specif m' _ =
-raise error ("nxt_specif: not impl. for "^tac2str m');
+error ("nxt_specif: not impl. for "^tac2str m');
 (*.get the values from oris; handle the term list w.r.t. penv.*)
 local infix mem;
 fun x mem [] = false
 	      (((head_of o term_of) given) $ (term_of formal)); WN100819*)
 fun tag_form thy (formal, given) =
 (let val gf = (head_of given) $ formal;
 val _ = cterm_of thy gf
 in gf end)
-handle _ => raise error ("calchead.tag_form: " ^
+handle _ => error ("calchead.tag_form: " ^
 Syntax.string_of_term (thy2ctxt thy) given ^
 " .. " ^
 Syntax.string_of_term (thy2ctxt thy) formal ^
 " ..types do not match");
 (* val formal = (the o (parse thy)) "[R::real]";
 	 ["no_met"] =>
 	 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
 (*all stored in tac_ itms     ^^^^^^^^^^*)
 | nxt_model_pbl tac_ _ =
-raise error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
+error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
 (* run subp_rooteq.sml ''
 until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
 > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
 (last_elem o drop_last) ets'';
 > val mst = (last_elem o drop_last) ets'';
 val pt = update_pblppc pt p pits
 	val pt = update_metppc pt p mits
 in (pt, (p,Met):pos') end
 ;
 (*| complete_mod (pt, pos as (p, Met):pos') =
-raise error ("###complete_mod: only impl.for Pbl, called with "^
+error ("###complete_mod: only impl.for Pbl, called with "^
 		 pos'2str pos);*)
 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
 fun all_modspec (pt, (p,_):pos') =
 | is_complete_mod_ itms =
 foldl and_ (true, (map #3 itms));
 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
 if (is_pblobj o (get_obj I pt)) p
 then (is_complete_mod_ o (get_obj g_pbl pt)) p
-else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
+else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
 | is_complete_mod (pt, pos as (p, Met)) =
 if (is_pblobj o (get_obj I pt)) p
 then (is_complete_mod_ o (get_obj g_met pt)) p
-else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
+else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
 | is_complete_mod (_, pos) =
-raise error ("is_complete_mod called by "^pos'2str pos^
+error ("is_complete_mod called by "^pos'2str pos^
 		 " (should be Pbl or Met)");
 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
 fun is_complete_spec (pt, pos as (p,_): pos') =
 if (not o is_pblobj o (get_obj I pt)) p
-then raise error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
+then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
 else let val (dI,pI,mI) = get_obj g_spec pt p
 	 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
 (*.complete empty items in specification from origin (pbl, met ev.refined);
 assumes 'is_complete_mod'.*)
 fun complete_spec (pt, pos as (p,_): pos') =

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