1.1 --- a/src/sml/ME/solve.sml Mon Sep 08 23:05:34 2003 +0200
1.2 +++ b/src/sml/ME/solve.sml Tue Sep 09 09:00:24 2003 +0200
1.3 @@ -260,6 +260,8 @@
1.4 (* val (mI,(p,p_)) = ("xxx",p);
1.5 *)
1.6 | solve (mI,m) (p,p_) pt =
1.7 +(* val ((mI,m), (p,p_)) = (m, pos);
1.8 + *)
1.9 if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
1.10 could be detail, too !!*)
1.11 then let val ((p,p_),ps,f,pt) =
1.12 @@ -275,9 +277,9 @@
1.13 8.01: generate from domID?*)
1.14 in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.15 Steps (is', (m',f',pt',p',c')::ss) =>
1.16 - (* val Steps (is', (m',f',pt',p',c')::ss) =
1.17 - locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.18 - *)
1.19 +(* val Steps (is', (m',f',pt',p',c')::ss) =
1.20 + locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.21 + *)
1.22 let val nxt_ =
1.23 case p' of (*change from solve to model subprobl#####*)
1.24 (_,Pbl) => nxt_model_pbl m' (pt',p')
1.25 @@ -290,7 +292,9 @@
1.26 in (p,(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) end
1.27 end;
1.28
1.29 -fun nxt_solv ("Apply_Method",Apply_Method' (mI,_)) (pos as (p,_)) (pt:ptree) =
1.30 +fun nxt_solv (Apply_Method' (mI,_)) (pt:ptree, pos as (p,_)) =
1.31 +(* val
1.32 + *)
1.33 let val {srls,...} = get_met mI;
1.34 val PblObj{meth=itms,...} = get_obj I pt p;
1.35 val thy' = get_obj g_domID pt p;
1.36 @@ -306,35 +310,22 @@
1.37 val f = Sign.string_of_term (sign_of (assoc_thy thy')) t;
1.38 (*val (pt,ps) = cappend_form pt p is t*)
1.39 (*writes to pt without asking user !!!?*)
1.40 + val tac_ = Apply_Method' (mI, Some (t, is));
1.41 val ((p,p_),_,_,pt) = (*implicit Take*)
1.42 - generate1 thy (Apply_Method' (mI,Some (t, is)))
1.43 - is(*Uistate.19.8.03*) (lev_on p,Frm) pt
1.44 - val {srls,...} = get_met mI
1.45 - val (nx,is,_) = next_tac (thy',srls) (pt,(p,p_)) scr is
1.46 - in ((p,p_), ((lev_onFrm o lev_dnRes) pos, is, nx),
1.47 - Form' (FormKF (~1,EdUndef,(length p), Nundef, f)),
1.48 - tac_2tac nx, Safe, pt) end
1.49 + generate1 thy tac_ is(*Uistate.19.8.03*) (lev_on p,Frm) pt
1.50 + in ((pt, (p,p_)), [(Apply_Method mI, tac_, ((lev_on p,Frm), is))])
1.51 + (*(p,p_), ((lev_onFrm o lev_dnRes) pos, is, nx),
1.52 + Form' (FormKF (~1,EdUndef,(length p), Nundef, f)),
1.53 + tac_2tac nx, Safe, pt*) end
1.54 | None =>
1.55 - let val m = fst3 (next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is);
1.56 - val f = case m of
1.57 - Subproblem' ((domID, pblID,_),_,_) =>
1.58 - Form' (FormKF (~1,EdUndef,(length p), Nundef,
1.59 - (Sign.string_of_term (sign_of (assoc_thy thy'))
1.60 - (subpbl domID pblID))))
1.61 - | _ => EmptyMout;
1.62 (*nothing written to pt !!!*)
1.63 - in ((p,p_), (lev_dnRes pos, is, m), f, tac_2tac m, Safe, pt) end
1.64 + ((pt, (lev_dnRes pos)),
1.65 + [(Apply_Method mI, Apply_Method' (mI, None), ((lev_on p,Frm), is))])
1.66 end
1.67
1.68 - | nxt_solv ("Free_Solve", Free_Solve') (p,_) pt =
1.69 - let val _=writeln"###solve Free_Solve";
1.70 - val p' = lev_dn_ (p,Res);
1.71 - val pt = update_metID pt (par_pblobj pt p) e_metID;
1.72 - in (p', (p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe, pt) end
1.73 -
1.74 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
1.75 *)
1.76 - | nxt_solv ("Check_Postcond",Check_Postcond' (pI,_)) (pos as (p,p_)) pt =
1.77 + | nxt_solv (Check_Postcond' (pI,_)) (pt, pos as (p,p_)) =
1.78 let (*val _=writeln"###solve Check_Postcond";*)
1.79 val pp = par_pblobj pt p
1.80 val asm = (case get_obj g_tac pt p of
1.81 @@ -357,7 +348,8 @@
1.82 generate1 thy (Check_Postcond'(pI,(scval,
1.83 map term2str asm)))
1.84 is (pp,Res) pt;
1.85 - in ((p,p_), (([],Res),is,End_Proof''), f, End_Proof', scsaf, pt) end
1.86 + in ((pt, (p,p_)), [(*FIXXXXME@@@@@@@@@@@@@@@@@@@@@@@@@*)])
1.87 + (*(p,p_), (([],Res),is,End_Proof''), f, End_Proof', scsaf, pt*) end
1.88 else
1.89 let
1.90 (*resume script of parpbl, transfer value of subpbl-script*)
1.91 @@ -378,40 +370,23 @@
1.92 (istate2str (get_istate pt ([3],Res))));*)
1.93 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
1.94 (ScrState (E,l,a,scval,scsaf,b));
1.95 - in ((p,p_), ((pp,Res),is',nx), f, tac_2tac nx, scsaf, pt) end
1.96 + in ((pt, (p,p_)), [(*FIXXXXME@@@@@@@@@@@@@@@@@@@@@@@@@*)])
1.97 + (*(p,p_), ((pp,Res),is',nx), f, tac_2tac nx, scsaf, pt*) end
1.98 end
1.99 (* writeln(istate2str(get_istate pt (p,p_)));
1.100 *)
1.101
1.102 - | nxt_solv (_,End_Proof'') (p,p_) pt =
1.103 - ((p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt)
1.104 + | nxt_solv (End_Proof'') ptp = (ptp, [])
1.105 +;
1.106 + (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
1.107
1.108 (*.start interpreter and do one rewrite.*)
1.109 (* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_);
1.110 solve ("",Detail_Set'(thy', rls, t)) p pt;
1.111 - *)
1.112 - | nxt_solv (_,Detail_Set'(thy', rls, t)) p pt =
1.113 - let (*val rls = the (assoc(!ruleset',rls'))
1.114 - handle _ => raise error ("solve: '"^rls'^"' not known");*)
1.115 - val thy = assoc_thy thy';
1.116 - val (srls, sc, is) =
1.117 - case rls of
1.118 - Rrls {scr=sc as Rfuns {init_state=ii,...},...} =>
1.119 - (e_rls, sc, RrlsState (ii t))
1.120 - | Rls {srls=srls,scr=sc as Script s,...} =>
1.121 - (srls, sc, ScrState ([(one_scr_arg s,t)], [],
1.122 - None, e_term, Sundef, true));
1.123 - val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
1.124 - val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
1.125 - val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
1.126 - val aopt = applicable_in p pt nx;
1.127 - in case aopt of
1.128 - Notappl s => raise error ("solve Detail_Set: "^s)
1.129 - (* val Appl m = aopt;
1.130 - *)
1.131 - | Appl m => solve ("discardFIXME",m) p pt end
1.132 + | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
1.133 +---> FE-interface/sml.sml
1.134
1.135 - | nxt_solv (_,End_Detail' t) (p,p_) pt =
1.136 + | nxt_solv (End_Detail' t) (pt, (p,p_)) =
1.137 let val pr as (p',_) = (lev_up p, Res)
1.138 val pp = par_pblobj pt p
1.139 val r = (fst o (get_obj g_result pt)) p'
1.140 @@ -421,49 +396,18 @@
1.141 val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.142 in (pr, ((pp,Frm(*???*)),is,tac_),
1.143 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
1.144 - tac_2tac tac_, Sundef, pt)end
1.145 -(* val (mI,(p,p_)) = ("xxx",p);
1.146 - *)
1.147 - | nxt_solv (mI,m) (p,p_) pt =
1.148 - if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
1.149 - could be detail, too !!*)
1.150 - then let val ((p,p_),ps,f,pt) =
1.151 + tac_2tac tac_, Sundef, pt) end
1.152 +*)
1.153 +
1.154 +
1.155 +(*Kommentare sind NUR ZULETZT veraenderter Code: in sml.sml ueberschrieben*)
1.156 +fun nxt_solve_ (*mI,m*) (pt,pos as (p,p_)) =
1.157 + if e_metID = get_obj g_metID pt (par_pblobj pt p)
1.158 + then (*let val ((p,p_),ps,f,pt) =
1.159 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.160 m e_istate (p,p_) pt;
1.161 - in ((p,p_),((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) end
1.162 - else
1.163 - let
1.164 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.165 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.166 -(*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
1.167 - val d = e_rls; (*FIXME: canon.simplifier for domain is missing
1.168 - 8.01: generate from domID?*)
1.169 - in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.170 - Steps (is', (m',f',pt',p',c')::ss) =>
1.171 - (* val Steps (is', (m',f',pt',p',c')::ss) =
1.172 - locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.173 - *)
1.174 - let val nxt_ =
1.175 - case p' of (*change from solve to model subprobl#####*)
1.176 - (_,Pbl) => nxt_model_pbl m' (pt',p')
1.177 - | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');
1.178 - (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
1.179 - in (p',(p',is',nxt_), f', tac_2tac nxt_, safe is', pt'(*'*)) end
1.180 - | NotLocatable =>
1.181 - let val (p,ps,f,pt) =
1.182 - generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;
1.183 - in (p,(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt) end
1.184 - end;
1.185 -
1.186 -(*Kommentare sind NUR ZULETZT veraenderter Code*)
1.187 -fun nxt_solve_ (mI,m) (pt,pos as (p,p_)) =
1.188 - if e_metID = get_obj g_metID pt (par_pblobj pt p)
1.189 - then let val ((p,p_),ps,f,pt) =
1.190 - generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.191 - m e_istate (p,p_) pt;
1.192 - in (*((p,p_),((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt)*)
1.193 + in (((p,p_),((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe, pt)*)
1.194 (*NEU*) ((pt,(p,p_)),[]):calcstate
1.195 - end
1.196 else
1.197 let
1.198 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.199 @@ -471,13 +415,15 @@
1.200 val d = e_rls;
1.201 in (*case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.202 Steps (is', (m',f',pt',p',c')::ss) =>*)
1.203 - let val nxt_ =
1.204 - case (*p'*)pos of
1.205 + let val (nxt_,is,_) =
1.206 + (*case p' of
1.207 (_,Pbl) => nxt_model_pbl m(*'*) (*pt',p'*) (pt,pos)
1.208 - | _ => fst3 (next_tac (thy',srls) (*pt',p'*) (pt,pos)
1.209 - sc is(*'*));
1.210 + | _ =>fst3*)(next_tac (thy',srls) (*pt',p'*) (pt,pos)
1.211 + sc is(*'*))
1.212 + val (pos',_,_,pt) = generate1 (assoc_thy "Isac.thy")
1.213 + nxt_ is pos pt
1.214 in (*(p',(p',is',nxt_), f', tac_2tac nxt_, safe is', pt')*)
1.215 - (*NEU*) ((pt,(p,p_)),[]):calcstate
1.216 + (*NEU*) ((pt,pos'),[(tac_2tac nxt_, nxt_, (pos,is))]):calcstate
1.217 (*RICHTIG: nxt_solv nxt_ ptp*) end
1.218 (*| NotLocatable =>
1.219 let val (p,ps,f,pt) =