1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/ME/solve.sml Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,579 @@
1.4 +(* solve an example by interpreting a method's script
1.5 + (c) Walther Neuper 1999
1.6 +
1.7 +use"ME/solve.sml";
1.8 +use"solve.sml";
1.9 +*)
1.10 +
1.11 +fun safe (ScrState (_,_,_,_,s,_)) = s
1.12 + | safe (RrlsState _) = Safe;
1.13 +
1.14 +type mstID = string;
1.15 +type tac'_ = mstID * tac; (*DG <-> ME*)
1.16 +val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_;
1.17 +
1.18 +fun mk_tac'_ m = case m of
1.19 + Init_Proof (ppc, spec) => ("Init_Proof", Init_Proof (ppc, spec ))
1.20 +| Model_Problem => ("Model_Problem", Model_Problem)
1.21 +| Refine_Tacitly pblID => ("Refine_Tacitly", Refine_Tacitly pblID)
1.22 +| Refine_Problem pblID => ("Refine_Problem", Refine_Problem pblID)
1.23 +| Add_Given cterm' => ("Add_Given", Add_Given cterm')
1.24 +| Del_Given cterm' => ("Del_Given", Del_Given cterm')
1.25 +| Add_Find cterm' => ("Add_Find", Add_Find cterm')
1.26 +| Del_Find cterm' => ("Del_Find", Del_Find cterm')
1.27 +| Add_Relation cterm' => ("Add_Relation", Add_Relation cterm')
1.28 +| Del_Relation cterm' => ("Del_Relation", Del_Relation cterm')
1.29 +
1.30 +| Specify_Theory domID => ("Specify_Theory", Specify_Theory domID)
1.31 +| Specify_Problem pblID => ("Specify_Problem", Specify_Problem pblID)
1.32 +| Specify_Method metID => ("Specify_Method", Specify_Method metID)
1.33 +| Apply_Method metID => ("Apply_Method", Apply_Method metID)
1.34 +| Check_Postcond pblID => ("Check_Postcond", Check_Postcond pblID)
1.35 +| Free_Solve => ("Free_Solve",Free_Solve)
1.36 +
1.37 +| Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Rewrite_Inst (subs, thm'))
1.38 +| Rewrite thm' => ("Rewrite", Rewrite thm')
1.39 +| Rewrite_Asm thm' => ("Rewrite_Asm", Rewrite_Asm thm')
1.40 +| Rewrite_Set_Inst (subs, rls')
1.41 + => ("Rewrite_Set_Inst", Rewrite_Set_Inst (subs, rls'))
1.42 +| Rewrite_Set rls' => ("Rewrite_Set", Rewrite_Set rls')
1.43 +| End_Ruleset => ("End_Ruleset", End_Ruleset)
1.44 +
1.45 +| End_Detail => ("End_Detail", End_Detail)
1.46 +| Detail_Set rls' => ("Detail_Set", Detail_Set rls')
1.47 +| Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Detail_Set_Inst (s, rls'))
1.48 +
1.49 +| Calculate op_ => ("Calculate", Calculate op_)
1.50 +| Substitute sube => ("Substitute", Substitute sube)
1.51 +| Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts')
1.52 +
1.53 +| Take cterm' => ("Take", Take cterm')
1.54 +| Take_Inst cterm' => ("Take_Inst", Take_Inst cterm')
1.55 +| Group (con, ints) => ("Group", Group (con, ints))
1.56 +| Subproblem (domID, pblID) => ("Subproblem", Subproblem (domID, pblID))
1.57 +(*
1.58 +| Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts'))
1.59 +*)
1.60 +| End_Subproblem => ("End_Subproblem",End_Subproblem)
1.61 +| CAScmd cterm' => ("CAScmd", CAScmd cterm')
1.62 +
1.63 +| Split_And => ("Split_And", Split_And)
1.64 +| Conclude_And => ("Conclude_And", Conclude_And)
1.65 +| Split_Or => ("Split_Or", Split_Or)
1.66 +| Conclude_Or => ("Conclude_Or", Conclude_Or)
1.67 +| Begin_Trans => ("Begin_Trans", Begin_Trans)
1.68 +| End_Trans => ("End_Trans", End_Trans)
1.69 +| Begin_Sequ => ("Begin_Sequ", Begin_Sequ)
1.70 +| End_Sequ => ("End_Sequ", Begin_Sequ)
1.71 +| Split_Intersect => ("Split_Intersect", Split_Intersect)
1.72 +| End_Intersect => ("End_Intersect", End_Intersect)
1.73 +| Check_elementwise cterm' => ("Check_elementwise", Check_elementwise cterm')
1.74 +| Or_to_List => ("Or_to_List", Or_to_List)
1.75 +| Collect_Trues => ("Collect_Results", Collect_Trues)
1.76 +
1.77 +| Empty_Tac => ("Empty_Tac",Empty_Tac)
1.78 +| Tac string => ("Tac",Tac string)
1.79 +| User => ("User",User)
1.80 +| End_Proof' => ("End_Proof'",End_Proof');
1.81 +
1.82 +(*Detail*)
1.83 +val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_;
1.84 +
1.85 +fun mk_tac ((_,m):tac'_) = m;
1.86 +fun mk_mstID ((mI,_):tac'_) = mI;
1.87 +
1.88 +fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms);
1.89 +(* TODO: tac2str, tac'_2str NOT tested *)
1.90 +
1.91 +
1.92 +
1.93 +type squ = ptree; (* TODO: safe etc. *)
1.94 +
1.95 +(*13.9.02--------------
1.96 +type ctr = (loc * pos) list;
1.97 +val ops = [("plus","op +"),("minus","op -"),("times","op *"),
1.98 + ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
1.99 +fun op_intern op_ =
1.100 + case assoc (ops,op_) of
1.101 + Some op' => op' | None => raise error ("op_intern: no op= "^op_);
1.102 +-----------------------*)
1.103 +
1.104 +
1.105 +
1.106 +(* use"ME/solve.sml";
1.107 + use"solve.sml";
1.108 +
1.109 +val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g";
1.110 +val ttt = (term_of o the o (parse thy))"Rewrite thmid True g";
1.111 +
1.112 + Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
1.113 + *)
1.114 +
1.115 +
1.116 +
1.117 +val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem",
1.118 + "Model_Problem",(*"Match_Problem",*)
1.119 + "Add_Given","Del_Given","Add_Find","Del_Find",
1.120 + "Add_Relation","Del_Relation",
1.121 + "Specify_Theory","Specify_Problem","Specify_Method"];
1.122 +
1.123 +"-----------------------------------------------------------------------";
1.124 +
1.125 +
1.126 +fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
1.127 + (tac_2tac tac_, tac_, (p, get_istate pt p)):taci;
1.128 +
1.129 +
1.130 +(*FIXME.WN050821 compare solve ... nxt_solv*)
1.131 +(* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
1.132 + val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
1.133 + *)
1.134 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _))
1.135 + (pt:ptree, (pos as (p,_))) =
1.136 + let val {srls,...} = get_met mI;
1.137 + val PblObj{meth=itms,...} = get_obj I pt p;
1.138 + val thy' = get_obj g_domID pt p;
1.139 + val thy = assoc_thy thy';
1.140 + val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
1.141 + val ini = init_form thy sc env;
1.142 + val p = lev_dn p;
1.143 + in
1.144 + case ini of
1.145 + Some t => (* val Some t = ini;
1.146 + *)
1.147 + let val (pos,c,_,pt) =
1.148 + generate1 thy (Apply_Method' (mI, Some t, is))
1.149 + is (lev_on p, Frm)(*implicit Take*) pt;
1.150 + in ("ok",([(Apply_Method mI, Apply_Method' (mI, Some t, is),
1.151 + ((lev_on p, Frm), is))], c, (pt,pos)):calcstate')
1.152 + end
1.153 + | None => (*execute the first tac in the Script, compare solve m*)
1.154 + let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is;
1.155 + val d = e_rls (*FIXME: get simplifier from domID*);
1.156 + in
1.157 + case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of
1.158 + Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.159 +(* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
1.160 + locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
1.161 + *)
1.162 + ("ok", (map step2taci ss, c', (pt',p')))
1.163 + | NotLocatable =>
1.164 + let val (p,ps,f,pt) =
1.165 + generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt;
1.166 + in ("not-found-in-script",
1.167 + ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
1.168 + (*just-before------------------------------------------------------
1.169 + ("ok",([(Apply_Method mI,Apply_Method'(mI,None,e_istate),
1.170 + (pos, is))],
1.171 + [], (update_env pt (fst pos) (Some is),pos)))
1.172 + -----------------------------------------------------------------*)
1.173 + end
1.174 + end
1.175 +
1.176 + | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
1.177 + let (*val _=writeln"###solve Free_Solve";*)
1.178 + val p' = lev_dn_ (p,Res);
1.179 + val pt = update_metID pt (par_pblobj pt p) e_metID;
1.180 + in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
1.181 + [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end
1.182 +
1.183 +(* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
1.184 + ( m, (pt, pos));
1.185 + *)
1.186 + | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
1.187 + let (*val _=writeln"###solve Check_Postcond";*)
1.188 + val pp = par_pblobj pt p
1.189 + val asm = (case get_obj g_tac pt p of
1.190 + Check_elementwise _ => (*collects and instantiates asms*)
1.191 + (snd o (get_obj g_result pt)) p
1.192 + | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
1.193 + handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.194 + val metID = get_obj g_metID pt pp;
1.195 + val {srls=srls,scr=sc,...} = get_met metID;
1.196 + val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
1.197 + (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
1.198 + val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
1.199 + val thy' = get_obj g_domID pt pp;
1.200 + val thy = assoc_thy thy';
1.201 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
1.202 + (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
1.203 +
1.204 + in if pp = [] then
1.205 + let val is = ScrState (E,l,a,scval,scsaf,b)
1.206 + val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.207 + val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt;
1.208 + in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
1.209 + [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end
1.210 + else
1.211 + let
1.212 + (*resume script of parpbl, transfer value of subpbl-script*)
1.213 + val ppp = par_pblobj pt (lev_up p);
1.214 + val thy' = get_obj g_domID pt ppp;
1.215 + val thy = assoc_thy thy';
1.216 + val metID = get_obj g_metID pt ppp;
1.217 + val sc = (#scr o get_met) metID;
1.218 + val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm);
1.219 + (*val _=writeln("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
1.220 + val _=writeln("### solve Check_postc, is(pt)= "^(istate2str is));
1.221 + val _=writeln("### solve Check_postc, is'= "^
1.222 + (istate2str (E,l,a,scval,scsaf,b)));*)
1.223 + val ((p,p_),ps,f,pt) =
1.224 + generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
1.225 + (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
1.226 + (*val _=writeln("### solve Check_postc, is(pt')= "^
1.227 + (istate2str (get_istate pt ([3],Res))));
1.228 + val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
1.229 + (ScrState (E,l,a,scval,scsaf,b));*)
1.230 + in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
1.231 + ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
1.232 + ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_))))
1.233 + end
1.234 + end
1.235 +(* val (msg, cs') =
1.236 + ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
1.237 + ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
1.238 + val (_,(pt',p')) = cs';
1.239 + (writeln o istate2str) (get_istate pt' p');
1.240 + (term2str o fst) (get_obj g_result pt' (fst p'));
1.241 + *)
1.242 +
1.243 +(* writeln(istate2str(get_istate pt (p,p_)));
1.244 + *)
1.245 + | solve (_,End_Proof'') (pt, (p,p_)) =
1.246 + ("end-proof",
1.247 + ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
1.248 + [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_))))
1.249 +
1.250 +(*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
1.251 + | solve (_,End_Detail' t) (pt,(p,p_)) =
1.252 + let val pr as (p',_) = (lev_up p, Res)
1.253 + val pp = par_pblobj pt p
1.254 + val r = (fst o (get_obj g_result pt)) p'
1.255 + (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
1.256 + val thy' = get_obj g_domID pt pp
1.257 + val (srls, is, sc) = from_pblobj' thy' pr pt
1.258 + val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.259 + in ("ok", ((*((pp,Frm(*???*)),is,tac_),
1.260 + Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
1.261 + tac_2tac tac_, Sundef,*)
1.262 + [(End_Detail, End_Detail' t ,
1.263 + ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end
1.264 +
1.265 + | solve (mI,m) (pt, po as (p,p_)) =
1.266 +(* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.267 + *)
1.268 + if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
1.269 + could be detail, too !!*)
1.270 + then let val ((p,p_),ps,f,pt) =
1.271 + generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.272 + m e_istate (p,p_) pt;
1.273 + in ("no-method-specified", (*Free_Solve*)
1.274 + ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
1.275 + [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end
1.276 + else
1.277 + let
1.278 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.279 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.280 +(*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
1.281 + val d = e_rls; (*FIXME: canon.simplifier for domain is missing
1.282 + 8.01: generate from domID?*)
1.283 + in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.284 + Steps (is', ss as (m',f',pt',p',c')::_) =>
1.285 +(* val Steps (is', ss as (m',f',pt',p',c')::_) =
1.286 + locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.287 + *)
1.288 + let (*val _= writeln("### solve, after locate_gen: is= ")
1.289 + val _= writeln(istate2str is')*)
1.290 + (*val nxt_ =
1.291 + case p' of (*change from solve to model subpbl*)
1.292 + (_,Pbl) => nxt_model_pbl m' (pt',p')
1.293 + | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*)
1.294 + (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
1.295 + in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*)
1.296 + map step2taci ss, c', (pt',p'))) end
1.297 + | NotLocatable =>
1.298 + let val (p,ps,f,pt) =
1.299 + generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;
1.300 + in ("not-found-in-script",
1.301 + ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
1.302 + [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
1.303 + end;
1.304 +
1.305 +
1.306 +(*FIXME.WN050821 compare solve ... nxt_solv*)
1.307 +(* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
1.308 +fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =
1.309 +(* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
1.310 + ((Apply_Method' (mI, None, e_istate)), e_istate, ptp);
1.311 + *)
1.312 + let val {srls,ppc,...} = get_met mI;
1.313 + val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
1.314 + val itms = if itms <> [] then itms
1.315 + else complete_metitms oris probl [] ppc
1.316 + val thy' = get_obj g_domID pt p;
1.317 + val thy = assoc_thy thy';
1.318 + val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
1.319 + val ini = init_form thy scr env;
1.320 + in
1.321 + case ini of
1.322 + Some t => (* val Some t = ini;
1.323 + *)
1.324 + let val pos = ((lev_on o lev_dn) p, Frm)
1.325 + val tac_ = Apply_Method' (mI, Some t, is);
1.326 + val (pos,c,_,pt) = (*implicit Take*)
1.327 + generate1 thy tac_ is pos pt
1.328 + (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
1.329 + in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end
1.330 + | None =>
1.331 + let val pt = update_env pt (fst pos) (Some is)
1.332 + val (tacis, c, ptp) = nxt_solve_ (pt, pos)
1.333 + in (tacis @
1.334 + [(Apply_Method mI, Apply_Method' (mI, None, e_istate), (pos, is))],
1.335 + c, ptp) end
1.336 + end
1.337 +(* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
1.338 + val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) =
1.339 + (tac_, is, ptp);
1.340 + *)
1.341 + (*TODO.WN050913 remove unnecessary code below*)
1.342 + | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) =
1.343 + let (*val _=writeln"###solve Check_Postcond";*)
1.344 + val pp = par_pblobj pt p
1.345 + val asm = (case get_obj g_tac pt p of
1.346 + Check_elementwise _ => (*collects and instantiates asms*)
1.347 + (snd o (get_obj g_result pt)) p
1.348 + | _ => ((map fst) o (get_assumptions_ pt)) (p,p_))
1.349 + handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.350 + val metID = get_obj g_metID pt pp;
1.351 + val {srls=srls,scr=sc,...} = get_met metID;
1.352 + val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
1.353 + (*val _= writeln("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
1.354 + val _= writeln("### solve Check_postc, is= "^(istate2str is));*)
1.355 + val thy' = get_obj g_domID pt pp;
1.356 + val thy = assoc_thy thy';
1.357 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
1.358 + (*val _= writeln("### solve Check_postc, scval= "^(term2str scval));*)
1.359 + in if pp = [] then
1.360 + let val is = ScrState (E,l,a,scval,scsaf,b)
1.361 + val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.362 + (*val _= writeln"### nxt_solv2 Apply_Method: stored is =";
1.363 + val _= writeln(istate2str is);*)
1.364 + val ((p,p_),ps,f,pt) =
1.365 + generate1 thy tac_ is (pp,Res) pt;
1.366 + in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end
1.367 + else
1.368 + let
1.369 + (*resume script of parpbl, transfer value of subpbl-script*)
1.370 + val ppp = par_pblobj pt (lev_up p);
1.371 + val thy' = get_obj g_domID pt ppp;
1.372 + val thy = assoc_thy thy';
1.373 + val metID = get_obj g_metID pt ppp;
1.374 + val {scr,...} = get_met metID;
1.375 + val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
1.376 + val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
1.377 + val is = ScrState (E,l,a,scval,scsaf,b)
1.378 + (*val _= writeln"### nxt_solv3 Apply_Method: stored is =";
1.379 + val _= writeln(istate2str is);*)
1.380 + val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
1.381 + (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
1.382 + in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end
1.383 + end
1.384 +(* writeln(istate2str(get_istate pt (p,p_)));
1.385 + *)
1.386 +
1.387 +(*.start interpreter and do one rewrite.*)
1.388 +(* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
1.389 + solve ("",Detail_Set'(thy', rls, t)) p pt;
1.390 + | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = **********
1.391 +---> FE-interface/sml.sml
1.392 +
1.393 + | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = **********
1.394 + let val pr as (p',_) = (lev_up p, Res)
1.395 + val pp = par_pblobj pt p
1.396 + val r = (fst o (get_obj g_result pt)) p'
1.397 + (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
1.398 + val thy' = get_obj g_domID pt pp
1.399 + val (srls, is, sc) = from_pblobj' thy' pr pt
1.400 + val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.401 + in (pr, ((pp,Frm(*???*)),is,tac_),
1.402 + Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
1.403 + tac_2tac tac_, Sundef, pt) end
1.404 +*)
1.405 + | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
1.406 +
1.407 + | nxt_solv tac_ is (pt, pos as (p,p_)) =
1.408 +(* val (pt, pos as (p,p_)) = ptp;
1.409 + *)
1.410 + let val pos = case pos of
1.411 + (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
1.412 + | (p, Res) => (lev_on p,Res) (*somewhere in script*)
1.413 + | _ => pos (*somewhere in script*)
1.414 + (*val _= writeln"### nxt_solv4 Apply_Method: stored is =";
1.415 + val _= writeln(istate2str is);*)
1.416 + val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt;
1.417 + in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
1.418 +
1.419 +
1.420 + (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
1.421 +
1.422 +
1.423 +(*.find the next tac from the script, nxt_solv will update the ptree.*)
1.424 +(* val (ptp as (pt,pos as (p,p_))) = ptp';
1.425 + val (ptp as (pt, pos as (p,p_))) = ptp'';
1.426 + val (ptp as (pt, pos as (p,p_))) = ptp;
1.427 + val (ptp as (pt, pos as (p,p_))) = (pt,ip);
1.428 + val (ptp as (pt, pos as (p,p_))) = (pt, pos);
1.429 + *)
1.430 +and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
1.431 + if e_metID = get_obj g_metID pt (par_pblobj pt p)
1.432 + then ([], [], (pt,(p,p_))):calcstate'
1.433 + else let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.434 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.435 + val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
1.436 + (*TODO here ^^^ return finished/helpless/ok !*)
1.437 + (* val (tac_',is',(t',_)) = next_tac (thy',srls) (pt,pos) sc is;
1.438 + *)
1.439 + in case tac_ of
1.440 + End_Detail' _ => ([(End_Detail,
1.441 + End_Detail' (t,[(*FIXME.040215*)]),
1.442 + (pos, is))], [], (pt, pos))
1.443 + | _ => nxt_solv tac_ is ptp end;
1.444 +
1.445 +(*.says how may steps of a calculation should be done by "fun autocalc".*)
1.446 +(*TODO.WN0512 redesign togehter with autocalc ?*)
1.447 +datatype auto =
1.448 + Step of int (*1 do #int steps; may stop in model/specify:
1.449 + IS VERY INEFFICIENT IN MODEL/SPECIY*)
1.450 +| CompleteModel (*2 complete modeling
1.451 + if model complete, finish specifying + start solving*)
1.452 +| CompleteCalcHead (*3 complete model/specify in one go + start solving*)
1.453 +| CompleteToSubpbl (*4 stop at the next begin of a subproblem,
1.454 + if none, complete the actual (sub)problem*)
1.455 +| CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
1.456 +| CompleteCalc; (*6 complete the calculation as a whole*)
1.457 +fun autoord (Step _ ) = 1
1.458 + | autoord CompleteModel = 2
1.459 + | autoord CompleteCalcHead = 3
1.460 + | autoord CompleteToSubpbl = 4
1.461 + | autoord CompleteSubpbl = 5
1.462 + | autoord CompleteCalc = 6;
1.463 +
1.464 +(* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);
1.465 + *)
1.466 +fun complete_solve auto c (ptp as (_, p): ptree * pos') =
1.467 + if p = ([], Res) then ("end-of-calculation", [], ptp) else
1.468 + case nxt_solve_ ptp of
1.469 + ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.470 +(* val ptp' = ptp''';
1.471 + *)
1.472 + if autoord auto < 5 then ("ok", c@c', ptp)
1.473 + else let val ptp = all_modspec ptp';
1.474 + val (_, c'', ptp) = all_solve auto (c@c') ptp;
1.475 + in complete_solve auto (c@c'@c'') ptp end
1.476 + | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.477 + if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
1.478 + else complete_solve auto (c@c') ptp'
1.479 + | ((End_Detail, _, _)::_, c', ptp') =>
1.480 + if autoord auto < 6 then ("ok", c@c', ptp')
1.481 + else complete_solve auto (c@c') ptp'
1.482 + | (_, c', ptp') => complete_solve auto (c@c') ptp'
1.483 +(* val (tacis, c', ptp') = nxt_solve_ ptp;
1.484 + val (tacis, c', ptp'') = nxt_solve_ ptp';
1.485 + val (tacis, c', ptp''') = nxt_solve_ ptp'';
1.486 + val (tacis, c', ptp'''') = nxt_solve_ ptp''';
1.487 + val (tacis, c', ptp''''') = nxt_solve_ ptp'''';
1.488 + *)
1.489 +and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
1.490 +(* val (ptp as (pt, (p,_))) = ptp;
1.491 + val (ptp as (pt, (p,_))) = ptp';
1.492 + val (ptp as (pt, (p,_))) = (pt, pos);
1.493 + *)
1.494 + let val (_,_,mI) = get_obj g_spec pt p;
1.495 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate))
1.496 + e_istate ptp;
1.497 + in complete_solve auto (c@c') ptp end;
1.498 +(*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.499 +fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
1.500 + if p = ([], Res) then ("end-of-calculation", [], ptp) else
1.501 + if p_ mem [Pbl, Met]
1.502 + then let val ptp = all_modspec ptp
1.503 + val (_, c', ptp) = all_solve auto c ptp
1.504 + in complete_solve auto (c@c') ptp end
1.505 + else case nxt_solve_ ptp of
1.506 + ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.507 + if autoord auto < 5 then ("ok", c@c', ptp)
1.508 + else let val ptp = all_modspec ptp'
1.509 + val (_, c'', ptp) = all_solve auto (c@c') ptp
1.510 + in complete_solve auto (c@c'@c'') ptp end
1.511 + | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.512 + if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
1.513 + else complete_solve auto (c@c') ptp'
1.514 + | ((End_Detail, _, _)::_, c', ptp') =>
1.515 + if autoord auto < 6 then ("ok", c@c', ptp')
1.516 + else complete_solve auto (c@c') ptp'
1.517 + | (_, c', ptp') => complete_solve auto (c@c') ptp'
1.518 +and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
1.519 + let val (_,_,mI) = get_obj g_spec pt p
1.520 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate))
1.521 + e_istate ptp
1.522 + in complete_solve auto (c@c') ptp end;
1.523 +
1.524 +(*.aux.fun for detailrls with Rrls, reverse rewriting.*)
1.525 +(* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
1.526 + *)
1.527 +fun rul_terms_2nds nds t [] = nds
1.528 + | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
1.529 + (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) ::
1.530 + (rul_terms_2nds nds t' rts);
1.531 +
1.532 +
1.533 +(*. detail steps done internally by Rewrite_Set*
1.534 + into ctree by use of a script .*)
1.535 +(* val (pt, (p,p_)) = (pt, pos);
1.536 + *)
1.537 +fun detailrls pt ((p,p_):pos') =
1.538 + let val t = get_obj g_form pt p
1.539 + val tac = get_obj g_tac pt p
1.540 + val rls = (assoc_rls o rls_of) tac
1.541 + in case rls of
1.542 +(* val Rrls {scr = Rfuns {init_state,...},...} = rls;
1.543 + *)
1.544 + Rrls {scr = Rfuns {init_state,...},...} =>
1.545 + let val (_,_,_,rul_terms) = init_state t
1.546 + val newnds = rul_terms_2nds [] t rul_terms
1.547 + val pt''' = ins_chn newnds pt p
1.548 + in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
1.549 + | _ =>
1.550 + let val is = init_istate tac t
1.551 + (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
1.552 + is wrong for simpl, but working ?!? *)
1.553 + val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
1.554 + Some t, is)
1.555 + val pos' = ((lev_on o lev_dn) p, Frm)
1.556 + val thy = assoc_thy "Isac.thy"
1.557 + val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
1.558 + val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
1.559 + val newnds = children (get_nd pt'' p)
1.560 + val pt''' = ins_chn newnds pt p
1.561 + (*complete_solve cuts branches after*)
1.562 + in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),
1.563 + (p @ [length newnds], Res):pos') end
1.564 + end;
1.565 +
1.566 +
1.567 +
1.568 +(* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*);
1.569 + get_form ((mI,m):tac'_) ((p,p_):pos') ppp;
1.570 + *)
1.571 +fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
1.572 + case applicable_in (p,p_) pt m of
1.573 + Notappl e => Error' (Error_ e)
1.574 + | Appl m =>
1.575 + (* val Appl m=applicable_in (p,p_) pt m;
1.576 + *)
1.577 + if mI mem specsteps
1.578 + then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1.579 + in f end
1.580 + else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
1.581 + in (*f*) EmptyMout end;
1.582 +