intermed. ctxt ..: added ctxt to Subproblem'
intermediate hacks marked with FIXME.WN110511,
which should disappear asap.
1.1 --- a/src/Tools/isac/Interpret/appl.sml Wed May 11 14:58:07 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Wed May 11 16:51:30 2011 +0200
1.3 @@ -619,11 +619,11 @@
1.4 then (*maybe Apply_Method has already been done*)
1.5 case get_obj g_env pt p of
1.6 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
1.7 - e_term, [], subpbl domID pblID))
1.8 + e_term, [], e_ctxt, subpbl domID pblID))
1.9 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.10 else (*somewhere later in the script*)
1.11 Appl (Subproblem' ((domID, pblID, e_metID), [],
1.12 - e_term, [], subpbl domID pblID))
1.13 + e_term, [], e_ctxt, subpbl domID pblID))
1.14
1.15 | applicable_in p pt (End_Subproblem) =
1.16 error ("applicable_in: not impl. for "^
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 11 14:58:07 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 11 16:51:30 2011 +0200
2.3 @@ -1696,7 +1696,7 @@
2.4
2.5
2.6 (* called only once, if a Subproblem has been located in the script*)
2.7 -fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
2.8 +fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =
2.9 (case metID of
2.10 ["no_met"] =>
2.11 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
3.1 --- a/src/Tools/isac/Interpret/ctree.sml Wed May 11 14:58:07 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/ctree.sml Wed May 11 16:51:30 2011 +0200
3.3 @@ -596,10 +596,11 @@
3.4 | Take' of term | Take_Inst' of term
3.5 | Group' of (con * int list * term)
3.6 | Subproblem' of (spec *
3.7 - (ori list) * (*filled in assod Subproblem'*)
3.8 - term * (*-"-, headline of calc-head *)
3.9 - fmz_ *
3.10 - term) (*Subproblem(dom,pbl)*)
3.11 + (ori list) * (* filled in assod Subproblem' *)
3.12 + term * (*-"-, headline of calc-head *)
3.13 + fmz_ *
3.14 + Proof.context *(* transported from assod to generate1 *)
3.15 + term) (* Subproblem(dom,pbl) OR cascmd*)
3.16 | CAScmd' of term
3.17 | End_Subproblem' of term (*???*)
3.18 | Split_And' of term | Conclude_And' of term
3.19 @@ -682,7 +683,7 @@
3.20 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
3.21 | Group' (con, ints, _) =>
3.22 "Group' "^(pair2str (con2str con, ints2str ints))
3.23 - | Subproblem' (spec, oris, _,_,pbl_form) =>
3.24 + | Subproblem' (spec, oris, _, _, _, pbl_form) =>
3.25 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
3.26 | End_Subproblem' _ => "End_Subproblem'"
3.27 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
3.28 @@ -1195,15 +1196,14 @@
3.29 result=result,ostate=ostate}
3.30 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
3.31
3.32 -fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,
3.33 - spec=spec,probl=probl,meth=meth,env=env,loc=_,
3.34 - branch=branch,result=result,ostate=ostate}) =
3.35 - PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
3.36 - meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate}
3.37 - | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,
3.38 - branch=branch,result=result,ostate=ostate}) =
3.39 - PrfObj {cell=cell,form=form,tac=tac,loc= l,
3.40 - branch=branch,result=result,ostate=ostate};
3.41 +fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,env=env,
3.42 + loc=_,branch=branch,result=result,ostate=ostate}) =
3.43 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,env=env,
3.44 + loc=l,branch=branch,result=result,ostate=ostate}
3.45 + | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,
3.46 + loc=_,branch=branch,result=result,ostate=ostate}) =
3.47 + PrfObj {cell=cell,form=form,tac=tac,
3.48 + loc= l,branch=branch,result=result,ostate=ostate};
3.49 (*
3.50 fun uni__cid cell'
3.51 (PblObj {cell=cell,origin=origin,fmz=fmz,
3.52 @@ -1308,17 +1308,30 @@
3.53 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
3.54 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
3.55
3.56 - (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
3.57 -fun update_loc pt (p,_) (ScrState ([],[],NONE,
3.58 - Const ("empty",_),Sundef,false)) =
3.59 - appl_obj (repl_loc (NONE,NONE)) pt p
3.60 - | update_loc pt (p,Res) x =
3.61 - let val (lform,_) = get_obj g_loc pt p
3.62 - in appl_obj (repl_loc (lform,SOME x)) pt p end
3.63 -
3.64 - | update_loc pt (p,_) x =
3.65 - let val (_,lres) = get_obj g_loc pt p
3.66 - in appl_obj (repl_loc (SOME x,lres)) pt p end;-------------*)
3.67 +(*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
3.68 + FIXME.WN110511 reactivated update_loc intermed. for ctxt *)
3.69 +fun update_loc pt (p, _) ((ScrState ([],[],NONE,Const ("empty",_),Sundef,false)), _) =
3.70 + appl_obj (repl_loc (NONE, NONE)) pt p
3.71 + | update_loc pt (p, Res) x =
3.72 + let val (lform,_) = get_obj g_loc pt p
3.73 + in appl_obj (repl_loc (lform, SOME x)) pt p end
3.74 + | update_loc pt (p, _) x =
3.75 + let val (_,lres) = get_obj g_loc pt p
3.76 + in appl_obj (repl_loc (SOME x, lres)) pt p end;
3.77 +fun update_ctxt pt (p, Res) ctxt = (*FIXME.WN110511 intermed. for ctxt *)
3.78 + let val (_, res) = get_obj g_loc pt p
3.79 + in
3.80 + case res of
3.81 + SOME (istate, _) => update_loc pt (p, Res) (istate, ctxt)
3.82 + | NONE => update_loc pt (p, Res) (e_istate, ctxt)
3.83 + end
3.84 + | update_ctxt pt (p, p_) ctxt =
3.85 + let val (frm, _) = get_obj g_loc pt p
3.86 + in
3.87 + case frm of
3.88 + SOME (istate, _) => update_loc pt (p, p_) (istate, ctxt)
3.89 + | NONE => update_loc pt (p, p_) (e_istate, ctxt)
3.90 + end
3.91
3.92 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
3.93 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
4.1 --- a/src/Tools/isac/Interpret/generate.sml Wed May 11 14:58:07 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed May 11 16:51:30 2011 +0200
4.3 @@ -462,31 +462,29 @@
4.4 pt) end
4.5
4.6 | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt =
4.7 - let val (pt,c) = cappend_atomic pt p l t (Substitute (subte2sube subte))
4.8 - (t',[]) Complete;
4.9 - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef,
4.10 - term2str t')), pt)
4.11 - end
4.12 + let
4.13 + val (pt,c) =
4.14 + cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;
4.15 + in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt)
4.16 + end
4.17
4.18 | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
4.19 - let val (pt,c) = cappend_atomic pt p l (str2term f)
4.20 - (Tac id) (str2term f',[]) Complete;
4.21 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
4.22 + let
4.23 + val (pt,c) =
4.24 + cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
4.25 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
4.26
4.27 - | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f))
4.28 - l (p,p_) pt =
4.29 - let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
4.30 - val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
4.31 - (oris, (domID, pblID, metID), hdl);
4.32 - (*val pbl = init_pbl ((#ppc o get_pbt) pblID);
4.33 - val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
4.34 - (*val _= tracing("### generate1: is([3],Frm)= "^
4.35 - (istate2str (get_istate pt ([3],Frm))));*)
4.36 - val f = Syntax.string_of_term (thy2ctxt thy) f;
4.37 - in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
4.38 + | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f))
4.39 + l (p,p_) pt =
4.40 + let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
4.41 + val (pt,c) =
4.42 + cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
4.43 + val pt = update_ctxt pt (p, Res) ctxt (*FIXME.WN110511*)
4.44 + val f = Syntax.string_of_term (thy2ctxt thy) f;
4.45 + in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
4.46
4.47 | generate1 thy m' _ _ _ =
4.48 - error ("generate1: not impl.for "^(tac_2str m'))
4.49 + error ("generate1: not impl.for "^(tac_2str m'))
4.50 ;
4.51
4.52
5.1 --- a/src/Tools/isac/Interpret/script.sml Wed May 11 14:58:07 2011 +0200
5.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 11 16:51:30 2011 +0200
5.3 @@ -437,38 +437,39 @@
5.4 \ REAL_LIST [c, c_2]]";
5.5 *)
5.6 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
5.7 - (Const ("Product_Type.Pair",_) $
5.8 - Free (dI',_) $
5.9 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
5.10 -(*compare "| assod _ (Subproblem'"*)
5.11 - let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
5.12 + (Const ("Product_Type.Pair",_) $Free (dI',_) $
5.13 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
5.14 + (*compare "| assod _ (Subproblem'"*)
5.15 + let
5.16 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
5.17 val thy = maxthy (assoc_thy dI) (rootthy pt);
5.18 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
5.19 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
5.20 - val ags = isalist2list ags';
5.21 - val (pI, pors, mI) =
5.22 - if mI = ["no_met"]
5.23 - then let val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
5.24 - handle ERROR "actual args do not match formal args"
5.25 - => (match_ags_msg pI stac ags(*raise exn*);[])
5.26 - val pI' = refine_ori' pors pI;
5.27 - in (pI', pors (*refinement over models with diff.prec only*),
5.28 - (hd o #met o get_pbt) pI') end
5.29 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
5.30 - handle ERROR "actual args do not match formal args"
5.31 - => (match_ags_msg pI stac ags(*raise exn*); []),
5.32 - mI);
5.33 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
5.34 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
5.35 + val ags = isalist2list ags';
5.36 + val (pI, pors, mI) =
5.37 + if mI = ["no_met"]
5.38 + then
5.39 + let
5.40 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
5.41 + handle ERROR "actual args do not match formal args"
5.42 + => (match_ags_msg pI stac ags(*raise exn*); [])
5.43 + val pI' = refine_ori' pors pI;
5.44 + in (pI', pors (*refinement over models with diff.prec only*),
5.45 + (hd o #met o get_pbt) pI') end
5.46 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
5.47 + handle ERROR "actual args do not match formal args"
5.48 + => (match_ags_msg pI stac ags(*raise exn*); []), mI);
5.49 val (fmz_, vals) = oris2fmz_vals pors;
5.50 - val {cas,ppc,thy,...} = get_pbt pI
5.51 - val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
5.52 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
5.53 - val hdl = case cas of
5.54 - NONE => pblterm dI pI
5.55 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
5.56 + val {cas,ppc,thy,...} = get_pbt pI
5.57 + val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
5.58 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
5.59 + val hdl =
5.60 + case cas of
5.61 + NONE => pblterm dI pI
5.62 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
5.63 val f = subpbl (strip_thy dI) pI
5.64 - in (Subproblem (dI, pI),
5.65 - Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f))
5.66 - end
5.67 + in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f))
5.68 + end
5.69
5.70 | stac2tac_ pt thy t = error
5.71 ("stac2tac_ TODO: no match for " ^
5.72 @@ -490,11 +491,13 @@
5.73
5.74
5.75 datatype ass =
5.76 - Ass of tac_ * (*SubProblem gets args instantiated in assod*)
5.77 - term (*for itr_arg,result in ets*)
5.78 -| AssWeak of tac_ *
5.79 - term (*for itr_arg,result in ets*)
5.80 -| NotAss;
5.81 + Ass of
5.82 + tac_ * (* SubProblem gets args instantiated in assod *)
5.83 + term (* for itr_arg, result in ets *)
5.84 + | AssWeak of
5.85 + tac_ *
5.86 + term (*for itr_arg,result in ets*)
5.87 + | NotAss;
5.88
5.89 (*.assod: tac_ associated with stac w.r.t. d
5.90 args
5.91 @@ -508,174 +511,159 @@
5.92 tac_ SubProblem with args completed from script
5.93 .*)
5.94 fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =
5.95 - (case stac of
5.96 - (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_)=>
5.97 - if thmID = thmID_ then
5.98 - if f = f_ then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
5.99 - else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
5.100 - else ((*tracing"3### assod ..NotAss";*)NotAss)
5.101 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_)=>
5.102 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
5.103 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.104 - else NotAss
5.105 + (case stac of
5.106 + (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
5.107 + if thmID = thmID_
5.108 + then
5.109 + if f = f_
5.110 + then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
5.111 + else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
5.112 + else ((*tracing"3### assod ..NotAss";*)NotAss)
5.113 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) =>
5.114 + if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
5.115 + then
5.116 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.117 + else NotAss
5.118 | _ => NotAss)
5.119
5.120 | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac =
5.121 - (case stac of
5.122 - (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
5.123 - ((*tracing ("3### assod: stac = " ^ ter2str t);
5.124 - tracing ("3### assod: f(m)= " ^ term2str f);*)
5.125 - if thmID = thmID_ then
5.126 - if f = f_ then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
5.127 - else ((*tracing"### assod ..AssWeak";
5.128 - tracing("### assod: f(m) = " ^ term2str f);
5.129 - tracing("### assod: f(stac)= " ^ term2str f_)*)
5.130 - AssWeak (m,f'))
5.131 - else ((*tracing"3### assod ..NotAss";*)NotAss))
5.132 + (case stac of
5.133 + (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
5.134 + ((*tracing ("3### assod: stac = " ^ ter2str t);
5.135 + tracing ("3### assod: f(m)= " ^ term2str f);*)
5.136 + if thmID = thmID_
5.137 + then
5.138 + if f = f_
5.139 + then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
5.140 + else
5.141 + ((*tracing"### assod ..AssWeak";
5.142 + tracing("### assod: f(m) = " ^ term2str f);
5.143 + tracing("### assod: f(stac)= " ^ term2str f_)*)
5.144 + AssWeak (m,f'))
5.145 + else ((*tracing"3### assod ..NotAss";*)NotAss))
5.146 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
5.147 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) then
5.148 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.149 - else NotAss
5.150 + if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
5.151 + then
5.152 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.153 + else NotAss
5.154 | _ => NotAss)
5.155
5.156 -(*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
5.157 -> val f'= (term_of o the o (parse thy))"#0+(sqrt(sqrt a))^^^#2=#0";
5.158 -> val m = Rewrite'("Script","tless_true","eval_rls",false,
5.159 - ("rroot_square_inv",""),f,(f',[]));
5.160 -> val stac = (term_of o the o (parse thy))
5.161 - "Rewrite rroot_square_inv False (#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0)";
5.162 -> assod e_rls m stac;
5.163 -val it =
5.164 - (SOME (Rewrite' (#,#,#,#,#,#,#)),Const ("empty","RealDef.real"),
5.165 - Const ("empty","RealDef.real")) : tac_ option * term * term*)
5.166 -
5.167 | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
5.168 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_)=
5.169 - if id_rls rls = rls_ then
5.170 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.171 - else NotAss
5.172 + (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
5.173 + if id_rls rls = rls_
5.174 + then
5.175 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.176 + else NotAss
5.177
5.178 | assod pt d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
5.179 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_)=
5.180 - if id_rls rls = rls_ then
5.181 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.182 - else NotAss
5.183 + (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
5.184 + if id_rls rls = rls_
5.185 + then
5.186 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.187 + else NotAss
5.188
5.189 | assod pt d (m as Rewrite_Set' (thy,put,rls,f,(f',asm)))
5.190 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
5.191 - if id_rls rls = rls_ then
5.192 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.193 - else NotAss
5.194 + (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
5.195 + if id_rls rls = rls_
5.196 + then
5.197 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.198 + else NotAss
5.199
5.200 | assod pt d (m as Detail_Set' (thy,put,rls,f,(f',asm)))
5.201 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
5.202 - if id_rls rls = rls_ then
5.203 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.204 - else NotAss
5.205 + (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
5.206 + if id_rls rls = rls_
5.207 + then
5.208 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.209 + else NotAss
5.210
5.211 | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) stac =
5.212 - (case stac of
5.213 - (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
5.214 - if op_ = op__ then
5.215 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.216 - else NotAss
5.217 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_)=>
5.218 - if contains_rule (Calc (snd (assoc1 (!calclist', op_))))
5.219 - (assoc_rls rls_) then
5.220 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.221 - else NotAss
5.222 + (case stac of
5.223 + (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
5.224 + if op_ = op__
5.225 + then
5.226 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.227 + else NotAss
5.228 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) =>
5.229 + if contains_rule (Calc (snd (assoc1 (!calclist', op_)))) (assoc_rls rls_)
5.230 + then
5.231 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.232 + else NotAss
5.233 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
5.234 - if contains_rule (Calc (snd (assoc1 (!calclist', op_))))
5.235 - (assoc_rls rls_) then
5.236 - if f = f_ then Ass (m,f') else AssWeak (m,f')
5.237 - else NotAss
5.238 + if contains_rule (Calc (snd (assoc1 (!calclist', op_)))) (assoc_rls rls_)
5.239 + then
5.240 + if f = f_ then Ass (m,f') else AssWeak (m,f')
5.241 + else NotAss
5.242 | _ => NotAss)
5.243
5.244 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
5.245 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
5.246 - ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
5.247 + ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
5.248 ", consts'= "^(term2str consts'));
5.249 - atomty consts; atomty consts';*)
5.250 - if consts = consts' then ((*tracing"### assod Check'_elementwise: Ass";*)
5.251 - Ass (m, consts_chkd))
5.252 - else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
5.253 + atomty consts; atomty consts';*)
5.254 + if consts = consts'
5.255 + then ((*tracing"### assod Check'_elementwise: Ass";*) Ass (m, consts_chkd))
5.256 + else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
5.257
5.258 - | assod pt _ (m as Or_to_List' (ors, list))
5.259 - (Const ("Script.Or'_to'_List",_) $ _) =
5.260 - Ass (m, list)
5.261 + | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
5.262 + Ass (m, list)
5.263
5.264 - | assod pt _ (m as Take' term)
5.265 - (Const ("Script.Take",_) $ _) =
5.266 - Ass (m, term)
5.267 + | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) =
5.268 + Ass (m, term)
5.269
5.270 - | assod pt _ (m as Substitute' (_, _, res))
5.271 - (Const ("Script.Substitute",_) $ _ $ _) =
5.272 - Ass (m, res)
5.273 -(* val t = str2term "Substitute [(x, 3)] (x^^^2 + x + 1)";
5.274 - val (Const ("Script.Substitute",_) $ _ $ _) = t;
5.275 - *)
5.276 + | assod pt _ (m as Substitute' (_, _, res)) (Const ("Script.Substitute",_) $ _ $ _) =
5.277 + Ass (m, res)
5.278
5.279 - | assod pt _ (m as Tac_ (thy,f,id,f'))
5.280 - (Const ("Script.Tac",_) $ Free (id',_)) =
5.281 - if id = id' then Ass (m, ((term_of o the o (parse thy)) f'))
5.282 - else NotAss
5.283 + | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
5.284 + if id = id'
5.285 + then Ass (m, ((term_of o the o (parse thy)) f'))
5.286 + else NotAss
5.287
5.288 -
5.289 -(* val t = str2term
5.290 - "SubProblem (DiffApp_,[make,function],[no_met]) \
5.291 - \[REAL m_, REAL v_, BOOL_LIST rs_]";
5.292 -
5.293 - val (Subproblem' ((domID,pblID,metID),_,_,_,f)) = m;
5.294 - val (Const ("Script.SubProblem",_) $
5.295 - (Const ("Product_Type.Pair",_) $
5.296 - Free (dI',_) $
5.297 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') = stac;
5.298 - *)
5.299 - | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,f))
5.300 - (stac as Const ("Script.SubProblem",_) $
5.301 - (Const ("Product_Type.Pair",_) $
5.302 - Free (dI',_) $
5.303 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
5.304 -(*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
5.305 - let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
5.306 + | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))
5.307 + (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
5.308 + Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
5.309 + (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
5.310 + let
5.311 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
5.312 val thy = maxthy (assoc_thy dI) (rootthy pt);
5.313 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
5.314 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
5.315 - val ags = isalist2list ags';
5.316 - val (pI, pors, mI) =
5.317 - if mI = ["no_met"]
5.318 - then let val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
5.319 - handle ERROR "actual args do not match formal args"
5.320 - => (match_ags_msg pI stac ags(*raise exn*);[]);
5.321 - val pI' = refine_ori' pors pI;
5.322 - in (pI', pors (*refinement over models with diff.prec only*),
5.323 - (hd o #met o get_pbt) pI') end
5.324 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
5.325 - handle ERROR "actual args do not match formal args"
5.326 - => (match_ags_msg pI stac ags(*raise exn*);[]),
5.327 - mI);
5.328 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
5.329 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
5.330 + val ags = isalist2list ags';
5.331 + val (pI, pors, mI) =
5.332 + if mI = ["no_met"]
5.333 + then
5.334 + let
5.335 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
5.336 + handle ERROR "actual args do not match formal args"
5.337 + => (match_ags_msg pI stac ags(*raise exn*);[]);
5.338 + val pI' = refine_ori' pors pI;
5.339 + in (pI', pors (*refinement over models with diff.prec only*),
5.340 + (hd o #met o get_pbt) pI')
5.341 + end
5.342 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
5.343 + handle ERROR "actual args do not match formal args"
5.344 + => (match_ags_msg pI stac ags(*raise exn*);[]), mI);
5.345 val (fmz_, vals) = oris2fmz_vals pors;
5.346 - val {cas, ppc,...} = get_pbt pI
5.347 - val {cas, ppc, thy,...} = get_pbt pI
5.348 - val dI = theory2theory' thy (*take dI from _refined_ pbl*)
5.349 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
5.350 - val hdl = case cas of
5.351 - NONE => pblterm dI pI
5.352 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
5.353 + val {cas, ppc,...} = get_pbt pI
5.354 + val {cas, ppc, thy,...} = get_pbt pI
5.355 + val dI = theory2theory' thy (*take dI from _refined_ pbl*)
5.356 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
5.357 + val hdl =
5.358 + case cas of
5.359 + NONE => pblterm dI pI
5.360 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
5.361 val f = subpbl (strip_thy dI) pI
5.362 - in if domID = dI andalso pblID = pI
5.363 - then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f), f)
5.364 - else NotAss
5.365 - end
5.366 + in
5.367 + if domID = dI andalso pblID = pI
5.368 + then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f), f)
5.369 + else NotAss
5.370 + end
5.371
5.372 | assod pt d m t =
5.373 - (if (!trace_script)
5.374 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
5.375 - "@@@ tac_ = "^(tac_2str m))
5.376 - else ();
5.377 - NotAss);
5.378 -
5.379 -
5.380 + (if (!trace_script)
5.381 + then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
5.382 + "@@@ tac_ = "^(tac_2str m))
5.383 + else ();
5.384 + NotAss);
5.385
5.386 fun tac_2tac (Refine_Tacitly' (pI,_,_,_,_)) = Refine_Tacitly pI
5.387 | tac_2tac (Model_Problem' (pI,_,_)) = Model_Problem
5.388 @@ -716,7 +704,7 @@
5.389
5.390 | tac_2tac (Tac_ (_,f,id,f')) = Tac id
5.391
5.392 - | tac_2tac (Subproblem' ((domID, pblID, _), _, _,_,_)) =
5.393 + | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) =
5.394 Subproblem (domID, pblID)
5.395 | tac_2tac (Check_Postcond' (pblID, _)) =
5.396 Check_Postcond pblID
5.397 @@ -878,7 +866,7 @@
5.398 > lhs'=lhs;
5.399 val it = true : bool*)
5.400 | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t'))
5.401 - | rep_tac_ (Subproblem' (_,_,_,_,t')) = (Erule, (e_term, t'))
5.402 + | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
5.403 | rep_tac_ (Take' (t')) = (Erule, (e_term, t'))
5.404 | rep_tac_ (Substitute' (subst,t,t')) = (Erule, (t, t'))
5.405 | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
6.1 --- a/test/Tools/isac/Test_Isac.thy Wed May 11 14:58:07 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 11 16:51:30 2011 +0200
6.3 @@ -88,6 +88,44 @@
6.4 use "Interpret/mstools.sml" (*new 2010*)
6.5
6.6 ML {*
6.7 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.8 +val (dI',pI',mI') =
6.9 + ("Test", ["sqroot-test","univariate","equation","test"],
6.10 + ["Test","squ-equ-test-subpbl1"]);
6.11 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.12 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.13 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.14 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
6.22 +*}
6.23 +ML {*
6.24 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
6.25 +"~~~~~ fun locatetac, args:"; val (tac, ptp as (pt, p)) = (tac, (pt,p));
6.26 +val (mI,m) = mk_tac'_ tac;
6.27 +*}
6.28 +ML {*
6.29 +val Appl m = applicable_in p pt m;
6.30 +*}
6.31 +ML {*
6.32 +assod;
6.33 +e_ctxt
6.34 +*}
6.35 +ML {*
6.36 +get_obj g_loc;
6.37 +*}
6.38 +ML {*
6.39 +*}
6.40 +ML {*
6.41 +*}
6.42 +ML {*
6.43 +*}
6.44 +ML {*
6.45 *}
6.46
6.47 use "Interpret/ctree.sml" (*!...see(25)*)