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

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 * pos'       (*position in ptree; ptree * pos' is the proofstate*)
 * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
 fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
-| rule2thm' r = raise error ("rule2thm': not defined for "^(rule2str r));
+| rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
 fun rule2rls' (Rls_ rls) = id_rls rls
-| rule2rls' r = raise error ("rule2rls': not defined for "^(rule2str r));
+| rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
 complicated with current t in rrlsstate.*)
 fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] =
 let val thy = assoc_thy thy'
 (*go at a location in a script and fetch the contents*)
 fun go [] t = t
 | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
 | go (L::p) (t1 $ t2) = go p t1
 | go (R::p) (t1 $ t2) = go p t2
-| go l _ = raise error ("go: no "^(loc_2str l));
+| go l _ = error ("go: no "^(loc_2str l));
 (*
 > val t = (term_of o the o (parse thy)) "a+b";
 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
 > val plus_a = go [L] t;
 > val b = go [R] t;
 (*FIXME: get 1st stac by next_stac [] instead of ... ?? 29.7.02*)
 (* val Script sc = scr;
 *)
 fun init_form thy (Script sc) env =
 (case get_stac thy sc of
-NONE => NONE (*raise error ("init_form: no 1st stac in "^
+NONE => NONE (*error ("init_form: no 1st stac in "^
 			  (Syntax.string_of_term (thy2ctxt thy) sc))*)
 | SOME stac => SOME (subst_atomic env stac))
-| init_form _ _ _ = raise error "init_form: no match";
+| init_form _ _ _ = error "init_form: no match";
 (* use"ME/script.sml";
 use"script.sml";
 *)
 | itr_arg _ (Const ("Script.Calculate",_) $ _ $ v) = v
 | itr_arg _ (Const ("Script.Check'_elementwise",_) $ consts $ _) = consts
 | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term
 | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
-| itr_arg thy t = raise error
+| itr_arg thy t = error
 ("itr_arg not impl. for "^
 (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
 > itr_arg "Script.thy" t;
 val it = Free ("e_","RealDef.real") : term
 val dsc = "nam" : string*)
 (*.from penv in itm_ make args for script depending on type of description.*)
 (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
-fun mk_arg thy d [] = raise error ("mk_arg: no data for "^
+fun mk_arg thy d [] = error ("mk_arg: no data for "^
 			       (Syntax.string_of_term (thy2ctxt thy) d))
 | mk_arg thy d [t] =
 (case dsc_valT d of
 	 "una" => [t]
 | "nam" =>
 	 [case t of
 	      r as (Const ("op =",_) $ _ $ _) => r
-	    | _ => raise error
+	    | _ => error
 			     ("mk_arg: dsc-typ 'nam' applied to non-equality "^
 			      (Syntax.string_of_term (thy2ctxt thy) t))]
-| s => raise error ("mk_arg: not impl. for "^s))
+| s => error ("mk_arg: not impl. for "^s))
 | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
 (*
 val d = d_in itm_;
 val [t] = ts_in itm_;
 	val itms = filter (okv mvat) itms
 	fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_)
 	fun itm2arg itms (_,(d,_)) =
 	    case find_first (test_dsc d) itms of
 		NONE =>
-		raise error ("itms2args: '"^term2str d^"' not in itms")
+		error ("itms2args: '"^term2str d^"' not in itms")
 	      (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
 penv postponed; presently penv holds already env for script*)
 	      | SOME (_,_,_,_,itm_) => penvval_in itm_
 	fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")
 	val pats = (#ppc o get_met) mI
 (*["BOOL (1+x=2)","REAL x"] --match_ags--> oris
 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
 fun oris2fmz_vals oris =
 let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
 	    ((term2str o comp_dts') (dsc, ts), last_elem ts)
-	    handle _ => raise error ("ori2fmz_env called with "^terms2str ts)
+	    handle _ => error ("ori2fmz_env called with "^terms2str ts)
 in (split_list o (map ori2fmz_vals)) oris end;
 (*detour necessary, because generate1 delivers a string-result*)
 fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
 (term_of o the o (parse (assoc_thy thy))) res
 val f = subpbl (strip_thy dI) pI
 in (Subproblem (dI, pI),
 	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f))
 end
-| stac2tac_ pt thy t = raise error
+| stac2tac_ pt thy t = error
 ("stac2tac_ TODO: no match for "^
 (Syntax.string_of_term (thy2ctxt thy) t));
 (*
 > val t = (term_of o the o (parse thy))
 "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)";
 val pred = if pred <> Const ("Script.Assumptions",bool)
 		 then pred
 	       else (mk_and o (map fst)) (get_assumptions_ pt (p,Res))
 in (bdv, pred) end
 | rep_set thy _ _ set =
-raise error ("check_elementwise: no set "^ (*from script*)
+error ("check_elementwise: no set "^ (*from script*)
 		 (Syntax.string_of_term (thy2ctxt thy) set));
 (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}";
 > val p = [];
 > val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]),
 ("#0 <= #9 + #4 * x",[22]),
 | tac_2tac (Check_Postcond' (pblID, _)) =
 		  Check_Postcond pblID
 | tac_2tac Empty_Tac_ = Empty_Tac
 | tac_2tac m =
-raise error ("tac_2tac: not impl. for "^(tac_2str m));
+error ("tac_2tac: not impl. for "^(tac_2str m));
 (** decompose tac_ to a rule and to (lhs,rhs)
 | rep_tac_ (Check_elementwise' (t,str,(t',asm)))  = (Erule, (e_term, t'))
 | rep_tac_ (Subproblem' (_,_,_,_,t'))  = (Erule, (e_term, t'))
 | rep_tac_ (Take' (t'))  = (Erule, (e_term, t'))
 | rep_tac_ (Substitute' (subst,t,t'))  = (Erule, (t, t'))
 | rep_tac_ (Or_to_List' (t, t'))  = (Erule, (t, t'))
-| rep_tac_ m = raise error ("rep_tac_: not impl.for "^
+| rep_tac_ m = error ("rep_tac_: not impl.for "^
 				 (tac_2str m));
 (*"N.3.6.03------
 fun tac_2rule m = (fst o rep_tac_) m;
 fun tac_2etac m = (snd o rep_tac_) m;
 	      (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
 	       NasNap (v, E) =>
 	       assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
 	     | ay => ay)
 	    | ay =>(ay))
-| NasApp _ => raise error ("assy: FIXXXME ///must not return NasApp///")
+| NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
 | ay => (ay))
 | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
 (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
 	 NasNap (v, E) =>
 (* val (_,STac stac) = subst_stacexpr E a v t;
 *)
 | (a', STac stac) =>
 	let (*val _=tracing("### assy, stac = "^term2str stac);*)
 	    val p' = case p_ of Frm => p | Res => lev_on p
-			      | _ => raise error ("assy: call by "^
+			      | _ => error ("assy: call by "^
 						  (pos'2str (p,p_)));
 	in case assod pt d m stac of
 	 Ass (m,v') =>
 	 let (*val _=tracing("### assy: Ass ("^tac_2str m^", "^
 			       term2str v'^")");*)
 | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) =
 astep_up y ((E, (drop_last l), a,v,S,b),ss)
 | ass_up y iss t =
-raise error ("ass_up not impl for t= "^(term2str t))
+error ("ass_up not impl for t= "^(term2str t))
 (* 9.6.03
 val (ys as (_,_,Script sc,_), ss) =
 ((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list);
 astep_up ys ((E,l,a,v,S,b),ss);
 val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
 	      (*drop the intermediate steps !*)
 	      in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
 	 else Steps (ScrState is, ss))
 | NasApp _ (*[((E,l,a,v,S,bb),(m',f',pt',p',c'))] =>
-	   raise error ("locate_gen: should not have got NasApp, ets =")*)
+	   error ("locate_gen: should not have got NasApp, ets =")*)
 => NotLocatable
 | NasNap (_,_) =>
 if l=[] then NotLocatable
 else (*scan from begin of script for rew_only*)
 	   (case assy ((ts,d),Aundef) ((E,[R],a,v,Unsafe,b),
 		     else NotLocatable)
 	      | _ => ((*tracing ("#### locate_gen: after Fini");*)
 		      NotLocatable))
 end
 | locate_gen _ m _ (sc,_) is =
-raise error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
+error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
 		 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is));
 (** find the next stactic in a script **)
 	    Appy lr => Appy lr
 	  | Napp E => nstep_up thy ptp scr E up Napp_ a v
 	  | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
 | nxt_up (thy,_) ptp scr E l ay t a v =
-raise error ("nxt_up not impl for "^
+error ("nxt_up not impl for "^
 	       (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t))
 (* val (thy, ptp, (Script sc), E, l, ay,    a, v)=
 (thy, ptp, scr,         E, l, Skip_, a, v);
 val (thy, ptp, (Script sc), E, l, ay,    a, v)=
 	 | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), e_istate, (v,s)))
 | Napp _ => (Empty_Tac_, e_istate, (e_term, Sundef))         (*helpless*)
 | Appy (m', scrst as (_,_,_,v,_,_)) => (m', ScrState scrst,
 			   (v, Sundef)))                         (*next stac*)
-| next_tac _ _ _ is = raise error ("next_tac: not impl for "^
+| next_tac _ _ _ is = error ("next_tac: not impl for "^
 				     (istate2str is));
 val formals = formal_args sc
 	(*expects same sequence of (actual) args in itms
 and (formal) args in met*)
 	fun relate_args env [] [] = env
 	  | relate_args env _ [] =
-	    raise error ("ERROR in creating the environment for '"
+	    error ("ERROR in creating the environment for '"
 			 ^id_of_scr sc^"' from \nthe items of the guard of "
 			 ^metID2str metID^",\n\
 			 \formal arg(s), from the script,\
 			 \ miss actual arg(s), from the guards env:\n"
 			 ^(string_of_int o length) formals
 			 ^" actuals: "^terms2str actuals)
 	  | relate_args env [] actual_finds = env (*may drop Find!*)
 	  | relate_args env (a::aa) (f::ff) =
 	    if type_of a = type_of f
 	    then relate_args (env @ [(a, f)]) aa ff else
-	    raise error ("ERROR in creating the environment for '"
+	    error ("ERROR in creating the environment for '"
 			 ^id_of_scr sc^"' from \nthe items of the guard of "
 			 ^metID2str metID^",\n\
 			 \different types of formal arg, from the script,\
 			 \ and actual arg, from the guards env:'\n\
 			 \formal: '"^term2str a^"::"^(type2str o type_of) a^"'\n\
 (* val (thy', (p,p_), pt) = (thy', (p,p_), pt);
 *)
 fun from_pblobj_or_detail' thy' (p,p_) pt =
 if member op = [Pbl,Met] p_
 then case get_obj g_env pt p of
-	     NONE => raise error "from_pblobj_or_detail': no istate"
+	     NONE => error "from_pblobj_or_detail': no istate"
 	   | SOME is =>
 	     let val metID = get_obj g_metID pt p
 		 val {srls,...} = get_met metID
 	     in (srls, is, (#scr o get_met) metID) end
 else

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38029	bd062a85ec67
child 38050	4c52ad406c20