594 | Apply_Assumption' of term list * term |
594 | Apply_Assumption' of term list * term |
595 |
595 |
596 | Take' of term | Take_Inst' of term |
596 | Take' of term | Take_Inst' of term |
597 | Group' of (con * int list * term) |
597 | Group' of (con * int list * term) |
598 | Subproblem' of (spec * |
598 | Subproblem' of (spec * |
599 (ori list) * (*filled in assod Subproblem'*) |
599 (ori list) * (* filled in assod Subproblem' *) |
600 term * (*-"-, headline of calc-head *) |
600 term * (*-"-, headline of calc-head *) |
601 fmz_ * |
601 fmz_ * |
602 term) (*Subproblem(dom,pbl)*) |
602 Proof.context *(* transported from assod to generate1 *) |
|
603 term) (* Subproblem(dom,pbl) OR cascmd*) |
603 | CAScmd' of term |
604 | CAScmd' of term |
604 | End_Subproblem' of term (*???*) |
605 | End_Subproblem' of term (*???*) |
605 | Split_And' of term | Conclude_And' of term |
606 | Split_And' of term | Conclude_And' of term |
606 | Split_Or' of term | Conclude_Or' of term |
607 | Split_Or' of term | Conclude_Or' of term |
607 | Begin_Trans' of term | End_Trans' of (term * (term list)) |
608 | Begin_Trans' of term | End_Trans' of (term * (term list)) |
680 |
681 |
681 | Take' cterm' => "Take' "(*^(quote cterm' )*) |
682 | Take' cterm' => "Take' "(*^(quote cterm' )*) |
682 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*) |
683 | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*) |
683 | Group' (con, ints, _) => |
684 | Group' (con, ints, _) => |
684 "Group' "^(pair2str (con2str con, ints2str ints)) |
685 "Group' "^(pair2str (con2str con, ints2str ints)) |
685 | Subproblem' (spec, oris, _,_,pbl_form) => |
686 | Subproblem' (spec, oris, _, _, _, pbl_form) => |
686 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*) |
687 "Subproblem' "(*^(pair2str (domID, strs2str ,...))*) |
687 | End_Subproblem' _ => "End_Subproblem'" |
688 | End_Subproblem' _ => "End_Subproblem'" |
688 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*) |
689 | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*) |
689 |
690 |
690 | Empty_Tac_ => "Empty_Tac_" |
691 | Empty_Tac_ => "Empty_Tac_" |
1193 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl, |
1194 PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl, |
1194 meth=meth,env=env,loc=loc,branch=branch, |
1195 meth=meth,env=env,loc=loc,branch=branch, |
1195 result=result,ostate=ostate} |
1196 result=result,ostate=ostate} |
1196 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj"; |
1197 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj"; |
1197 |
1198 |
1198 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz, |
1199 fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,env=env, |
1199 spec=spec,probl=probl,meth=meth,env=env,loc=_, |
1200 loc=_,branch=branch,result=result,ostate=ostate}) = |
1200 branch=branch,result=result,ostate=ostate}) = |
1201 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,env=env, |
1201 PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl, |
1202 loc=l,branch=branch,result=result,ostate=ostate} |
1202 meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate} |
1203 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac, |
1203 | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_, |
1204 loc=_,branch=branch,result=result,ostate=ostate}) = |
1204 branch=branch,result=result,ostate=ostate}) = |
1205 PrfObj {cell=cell,form=form,tac=tac, |
1205 PrfObj {cell=cell,form=form,tac=tac,loc= l, |
1206 loc= l,branch=branch,result=result,ostate=ostate}; |
1206 branch=branch,result=result,ostate=ostate}; |
|
1207 (* |
1207 (* |
1208 fun uni__cid cell' |
1208 fun uni__cid cell' |
1209 (PblObj {cell=cell,origin=origin,fmz=fmz, |
1209 (PblObj {cell=cell,origin=origin,fmz=fmz, |
1210 spec=spec,probl=probl,meth=meth,env=env,loc=loc, |
1210 spec=spec,probl=probl,meth=meth,env=env,loc=loc, |
1211 branch=branch,result=result,ostate=ostate}) = |
1211 branch=branch,result=result,ostate=ostate}) = |
1306 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos; |
1306 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos; |
1307 |
1307 |
1308 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos; |
1308 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos; |
1309 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos; |
1309 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos; |
1310 |
1310 |
1311 (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented |
1311 (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented |
1312 fun update_loc pt (p,_) (ScrState ([],[],NONE, |
1312 FIXME.WN110511 reactivated update_loc intermed. for ctxt *) |
1313 Const ("empty",_),Sundef,false)) = |
1313 fun update_loc pt (p, _) ((ScrState ([],[],NONE,Const ("empty",_),Sundef,false)), _) = |
1314 appl_obj (repl_loc (NONE,NONE)) pt p |
1314 appl_obj (repl_loc (NONE, NONE)) pt p |
1315 | update_loc pt (p,Res) x = |
1315 | update_loc pt (p, Res) x = |
1316 let val (lform,_) = get_obj g_loc pt p |
1316 let val (lform,_) = get_obj g_loc pt p |
1317 in appl_obj (repl_loc (lform,SOME x)) pt p end |
1317 in appl_obj (repl_loc (lform, SOME x)) pt p end |
1318 |
1318 | update_loc pt (p, _) x = |
1319 | update_loc pt (p,_) x = |
1319 let val (_,lres) = get_obj g_loc pt p |
1320 let val (_,lres) = get_obj g_loc pt p |
1320 in appl_obj (repl_loc (SOME x, lres)) pt p end; |
1321 in appl_obj (repl_loc (SOME x,lres)) pt p end;-------------*) |
1321 fun update_ctxt pt (p, Res) ctxt = (*FIXME.WN110511 intermed. for ctxt *) |
|
1322 let val (_, res) = get_obj g_loc pt p |
|
1323 in |
|
1324 case res of |
|
1325 SOME (istate, _) => update_loc pt (p, Res) (istate, ctxt) |
|
1326 | NONE => update_loc pt (p, Res) (e_istate, ctxt) |
|
1327 end |
|
1328 | update_ctxt pt (p, p_) ctxt = |
|
1329 let val (frm, _) = get_obj g_loc pt p |
|
1330 in |
|
1331 case frm of |
|
1332 SOME (istate, _) => update_loc pt (p, p_) (istate, ctxt) |
|
1333 | NONE => update_loc pt (p, p_) (e_istate, ctxt) |
|
1334 end |
1322 |
1335 |
1323 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*) |
1336 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*) |
1324 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p; |
1337 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p; |
1325 |
1338 |
1326 (*13.8.02--------------------------- |
1339 (*13.8.02--------------------------- |