1.1 --- a/src/Tools/isac/Interpret/ctree.sml Wed May 11 16:51:30 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu May 12 08:26:02 2011 +0200
1.3 @@ -753,9 +753,11 @@
1.4 meth : itm list, (* itms automatically added to copy of probl *)
1.5 env : (istate * Proof.context) option,
1.6 (* istate only for initac in script
1.7 - context for specify phase on this node *)
1.8 - loc : (istate * Proof.context) option * (istate * Proof.context) option,
1.9 - (* like PrfObj *)
1.10 + context for specify phase on this node NO..
1.11 +..NO: this conflicts with init_form/initac: see Apply_Method without init_form
1.12 +in fun step. Replaced by hack FIXME.WN110511 fun update_pbl_ctxt, see [*] below *)
1.13 + loc : (istate * Proof.context) option * (istate * (* like PrfObj *)
1.14 + Proof.context) option, (* for spec-phase [*] *)
1.15 branch: branch, (* like PrfObj *)
1.16 result: term * term list, (* like PrfObj *)
1.17 ostate: ostate}; (* like PrfObj *)
1.18 @@ -1308,8 +1310,9 @@
1.19 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1.20 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1.21
1.22 -(*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
1.23 - FIXME.WN110511 reactivated update_loc intermed. for ctxt *)
1.24 +local
1.25 +(* update_loc is done by append_*, see generate1.
1.26 + FIXME.WN110511 used for hack (which uses loc instead env in PblObj, see [*]*)
1.27 fun update_loc pt (p, _) ((ScrState ([],[],NONE,Const ("empty",_),Sundef,false)), _) =
1.28 appl_obj (repl_loc (NONE, NONE)) pt p
1.29 | update_loc pt (p, Res) x =
1.30 @@ -1318,20 +1321,15 @@
1.31 | update_loc pt (p, _) x =
1.32 let val (_,lres) = get_obj g_loc pt p
1.33 in appl_obj (repl_loc (SOME x, lres)) pt p end;
1.34 -fun update_ctxt pt (p, Res) ctxt = (*FIXME.WN110511 intermed. for ctxt *)
1.35 +in
1.36 +fun update_pbl_ctxt pt p ctxt = (*FIXME.WN110511 for hack *)
1.37 let val (_, res) = get_obj g_loc pt p
1.38 in
1.39 case res of
1.40 SOME (istate, _) => update_loc pt (p, Res) (istate, ctxt)
1.41 | NONE => update_loc pt (p, Res) (e_istate, ctxt)
1.42 end
1.43 - | update_ctxt pt (p, p_) ctxt =
1.44 - let val (frm, _) = get_obj g_loc pt p
1.45 - in
1.46 - case frm of
1.47 - SOME (istate, _) => update_loc pt (p, p_) (istate, ctxt)
1.48 - | NONE => update_loc pt (p, p_) (e_istate, ctxt)
1.49 - end
1.50 +end
1.51
1.52 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
1.53 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
2.1 --- a/src/Tools/isac/Interpret/generate.sml Wed May 11 16:51:30 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu May 12 08:26:02 2011 +0200
2.3 @@ -479,7 +479,7 @@
2.4 let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
2.5 val (pt,c) =
2.6 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
2.7 - val pt = update_ctxt pt (p, Res) ctxt (*FIXME.WN110511*)
2.8 + val pt = update_pbl_ctxt pt p ctxt (*FIXME.WN110511*)
2.9 val f = Syntax.string_of_term (thy2ctxt thy) f;
2.10 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
2.11
3.1 --- a/src/Tools/isac/Interpret/script.sml Wed May 11 16:51:30 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Thu May 12 08:26:02 2011 +0200
3.3 @@ -367,75 +367,49 @@
3.4 then convert to a 'tac_' (as required in appy).
3.5 arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)
3.6 fun stac2tac_ pt thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =
3.7 -(* val (pt, thy, (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f)) =
3.8 - (pt, (assoc_thy th), stac);
3.9 - *)
3.10 - let val tid = (de_esc_underscore o strip_thy) thmID
3.11 - in (Rewrite (tid, (string_of_thmI o
3.12 - (assoc_thm' thy)) (tid,"")), Empty_Tac_) end
3.13 -(* val (thy,
3.14 - mm as(Const ("Script.Rewrite'_Inst",_) $ sub $ Free(thmID,_) $ _ $ f))
3.15 - = (assoc_thy th,stac);
3.16 - stac2tac_ pt thy mm;
3.17 + let
3.18 + val tid = (de_esc_underscore o strip_thy) thmID
3.19 + in (Rewrite (tid, (string_of_thmI o (assoc_thm' thy)) (tid,"")), Empty_Tac_)
3.20 + end
3.21
3.22 - assoc_thm' (assoc_thy "Isac") (tid,"");
3.23 - assoc_thm' (Thy_Info.get_theory "Isac") (tid,"");
3.24 - *)
3.25 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $
3.26 - sub $ Free (thmID,_) $ _ $ f) =
3.27 - let val subML = ((map isapair2pair) o isalist2list) sub
3.28 - val subStr = subst2subs subML
3.29 - val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
3.30 - in (Rewrite_Inst
3.31 - (subStr, (tid, (string_of_thmI o
3.32 - (assoc_thm' thy)) (tid,""))), Empty_Tac_) end
3.33 + | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) =
3.34 + let
3.35 + val subML = ((map isapair2pair) o isalist2list) sub
3.36 + val subStr = subst2subs subML
3.37 + val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
3.38 + in (Rewrite_Inst (subStr, (tid, (string_of_thmI o (assoc_thm' thy)) (tid,""))), Empty_Tac_)
3.39 + end
3.40
3.41 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f)=
3.42 - (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
3.43 + | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
3.44 + (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
3.45
3.46 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $
3.47 - sub $ Free (rls,_) $ _ $ f) =
3.48 - let val subML = ((map isapair2pair) o isalist2list) sub;
3.49 - val subStr = subst2subs subML;
3.50 - in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
3.51 + | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $ sub $ Free (rls,_) $ _ $ f) =
3.52 + let
3.53 + val subML = ((map isapair2pair) o isalist2list) sub;
3.54 + val subStr = subst2subs subML;
3.55 + in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
3.56
3.57 | stac2tac_ pt thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =
3.58 - (Calculate op_, Empty_Tac_)
3.59 + (Calculate op_, Empty_Tac_)
3.60
3.61 | stac2tac_ pt thy (Const ("Script.Take",_) $ t) =
3.62 - (Take (term2str t), Empty_Tac_)
3.63 + (Take (term2str t), Empty_Tac_)
3.64
3.65 | stac2tac_ pt thy (Const ("Script.Substitute",_) $ isasub $ arg) =
3.66 - (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
3.67 -(* val t = str2term"Substitute [x = L, M_b L = 0] (M_b x = q_0 * x + c)";
3.68 - val Const ("Script.Substitute", _) $ isasub $ arg = t;
3.69 - *)
3.70 + (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
3.71
3.72 -(*12.1.01.*)
3.73 | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $
3.74 - (set as Const ("Collect",_) $ Abs (_,_,pred))) =
3.75 - (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term
3.76 - (thy2ctxt thy)) pred),
3.77 - (*set*)Empty_Tac_)
3.78 + (set as Const ("Collect",_) $ Abs (_,_,pred))) =
3.79 + (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term
3.80 + (thy2ctxt thy)) pred), (*set*)Empty_Tac_)
3.81
3.82 | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) =
3.83 - (Or_to_List, Empty_Tac_)
3.84 + (Or_to_List, Empty_Tac_)
3.85
3.86 -(*12.1.01.for subproblem_equation_dummy in root-equation *)
3.87 + (*12.1.01.for subproblem_equation_dummy in root-equation *)
3.88 | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) =
3.89 - (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
3.90 - (*L_ will come from pt in appl_in*)
3.91 + (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
3.92
3.93 - (*3.12.03 copied from assod SubProblem*)
3.94 -(* val Const ("Script.SubProblem",_) $
3.95 - (Const ("Product_Type.Pair",_) $
3.96 - Free (dI',_) $
3.97 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.98 - str2term
3.99 - "SubProblem (EqSystem_, [linear, system], [no_met])\
3.100 - \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
3.101 - \ REAL_LIST [c, c_2]]";
3.102 -*)
3.103 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
3.104 (Const ("Product_Type.Pair",_) $Free (dI',_) $
3.105 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =