1.1 --- a/src/Tools/isac/ME/solve.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,579 +0,0 @@
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 member op = [Pbl,Met] p_
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 member op = specsteps mI
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 -