diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/ME/generate.sml --- a/src/Tools/isac/ME/generate.sml Wed Aug 25 15:15:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,586 +0,0 @@ -(* use"ME/generate.sml"; - use"generate.sml"; - *) - -(*.initialize istate for Detail_Set.*) -(* -fun init_istate (Rewrite_Set rls) = -(* val (Rewrite_Set rls) = (get_obj g_tac pt p); - *) - (case assoc_rls rls of - Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) -(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; - *) - | Rls {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") - | Rls {scr=Script s,...} => -(* val Rls {scr=Script s,...} = assoc_rls rls; - *) - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) - | Seq {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") - | Seq {srls=srls,scr=Script s,...} => - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) - | init_istate (Rewrite_Set_Inst (subs, rls)) = -(* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p); - *) - let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs - in case assoc_rls rls of - Rls {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") - | Rls {scr=Script s,...} => - let val (a1, a2) = two_scr_arg s - in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end - | Seq {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") -(* val Seq {scr=Script s,...} = assoc_rls rls; - *) - | Seq {scr=Script s,...} => - let val (a1, a2) = two_scr_arg s - in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end - end; -*) -(*~~~~~~~~~~~~~~~~~~~~~~copy for dev. until del.~~~~~~~~~~~~~~~~~~~~~~~~~*) -fun init_istate (Rewrite_Set rls) t = -(* val (Rewrite_Set rls) = (get_obj g_tac pt p); - *) - (case assoc_rls rls of - Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) -(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; - *) - | Rls {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") - | Rls {scr=Script s,...} => -(* val Rls {scr=Script s,...} = assoc_rls rls; - *) - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) - | Seq {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") - | Seq {srls=srls,scr=Script s,...} => - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) -(* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t); - *) - | init_istate (Rewrite_Set_Inst (subs, rls)) t = - let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs - (*...we suppose the substitution of only _one_ bound variable*) - in case assoc_rls rls of - Rls {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") - | Rls {scr=Script s,...} => - let val (form, bdv) = two_scr_arg s - in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) - end - | Seq {scr=EmptyScr,...} => - raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." - ^"use prep_rls for storing rule-sets !") -(* val Seq {scr=Script s,...} = assoc_rls rls; - *) - | Seq {scr=Script s,...} => - let val (form, bdv) = two_scr_arg s - in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) - end - end; - - -(*.a taci holds alle information required to build a node in the calc-tree; - a taci is assumed to be used efficiently such that the calc-tree - resulting from applying a taci need not be stored separately; - see "type calcstate".*) -(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate" - TODO.WN0512 ? redesign this _list_: - # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs - # the latter problem may be resolved automatically if "fun autocalc" is - not any more used for the specify-phase and for changing the phases*) -type taci = - (tac * (*for comparison with input tac*) - tac_ * (*for ptree generation*) - (pos' * (*after applying tac_, for ptree generation*) - istate)); (*after applying tac_, for ptree generation*) -val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci; -(* val (tac, tac_, (pos', istate))::_ = tacis'; - *) -fun taci2str ((tac, tac_, (pos', istate)):taci) = - "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos' - ^", "^istate2str istate^" ))"; -fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis; - -datatype pblmet = (*%^%*) - Upblmet (*undefined*) - | Problem of pblID (*%^%*) - | Method of metID; (*%^%*) -fun pblmet2str (Problem pblID) = "Problem "^(strs2str pblID)(*%^%*) - | pblmet2str (Method metID) = "Method "^(metID2str metID);(*%^%*) - (*%^%*) (*26.6. moved to sequent.sml: fun ~~~~~~~~~; was here below*) - - -(* copy from 03.60.usecases.sml 15.11.99 *) -datatype user_cmd = - Accept | NotAccept | Example -| YourTurn | MyTurn (* internal use only 7.6.02 java-sml*) -| Rules -| DontKnow (*| HowComes | WhatFor 7.6.02 java-sml*) -| Undo (*| Back | Forward 7.6.02 java-sml*) -| EndProof | EndSession -| ActivePlus | ActiveMinus | SpeedPlus | SpeedMinus - (*Stepwidth...7.6.02 java-sml*) -| Auto | NotAuto | Details; -(* for test-print-outs *) -fun user_cmd2str Accept ="Accept" - | user_cmd2str NotAccept ="NotAccept" - | user_cmd2str Example ="Example" - | user_cmd2str MyTurn ="MyTurn" - | user_cmd2str YourTurn ="YourTurn" - | user_cmd2str Rules ="Rules" -(*| user_cmd2str HowComes ="HowComes"*) - | user_cmd2str DontKnow ="DontKnow" -(*| user_cmd2str WhatFor ="WhatFor" - | user_cmd2str Back ="Back"*) - | user_cmd2str Undo ="Undo" -(*| user_cmd2str Forward ="Forward"*) - | user_cmd2str EndProof ="EndProof" - | user_cmd2str EndSession ="EndSession" - | user_cmd2str ActivePlus = "ActivePlus" - | user_cmd2str ActiveMinus = "ActiveMinus" - | user_cmd2str SpeedPlus = "SpeedPlus" - | user_cmd2str SpeedMinus = "SpeedMinus" - | user_cmd2str Auto = "Auto" - | user_cmd2str NotAuto = "NotAuto" - | user_cmd2str Details = "Details"; - - - -(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) -datatype foppFK = (* in DG cases div 2 *) - EmptyFoppFK (*DG internal*) -| FormFK of cterm' -| PpcFK of cterm' ppc; -fun foppFK2str (FormFK ct') ="FormFK "^ct' - | foppFK2str (PpcFK ppc) ="PpcFK "^(ppc2str ppc) - | foppFK2str EmptyFoppFK ="EmptyFoppFK"; - - -datatype nest = Open | Closed | Nundef; -fun nest2str Open = "Open" - | nest2str Closed = "Closed" - | nest2str Nundef = "Nundef"; - -type indent = int; -datatype edit = EdUndef | Write | Protect; - (* bridge --> kernel *) - (* bridge <-> kernel *) -(* needed in dialog.sml *) (* bridge <-- kernel *) -fun edit2str EdUndef = "EdUndef" - | edit2str Write = "Write" - | edit2str Protect = "Protect"; - - -datatype inout = - New_User | End_User (*<->*) -| New_Proof | End_Proof (*<->*) -| Command of user_cmd (*-->*) -| Request of string | Message of string (*<--*) -| Error_ of string | System of string (*<--*) -| FoPpcFK of foppFK (*-->*) -| FormKF of cellID * edit * indent * nest * cterm' (*<--*) -| PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*) -| RuleFK of tac (*-->*) -| RuleKF of edit * tac (*<--*) -| RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*) -| Select of tac list (*<--*) -| RefineKF of match list (*<--*) -| Speed of int (*<--*) -| Active of int (*<--*) -| Domain of domID; (*<--*) - -fun inout2str End_Proof = "End_Proof" - | inout2str (Command user_cmd) = "Command "^(user_cmd2str user_cmd) - | inout2str (Request s) = "Request "^s - | inout2str (Message s) = "Message "^s - | inout2str (Error_ s) = "Error_ "^s - | inout2str (System s) = "System "^s - | inout2str (FoPpcFK foppFK) = "FoPpcFK "^(foppFK2str foppFK) - | inout2str (FormKF (cellID, edit, indent, nest, ct')) = - "FormKF ("^(string_of_int cellID)^"," - ^(edit2str edit)^","^(string_of_int indent)^"," - ^(nest2str nest)^",(" - ^ct' ^")" - | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) = - "PpcKF ("^(string_of_int cellID)^"," - ^(edit2str edit)^","^(string_of_int indent)^"," - ^(nest2str nest)^",(" - ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))" - | inout2str (RuleKF (edit,tac)) = "RuleKF "^ - pair2str(edit2str edit,tac2str tac) - | inout2str (RuleFK tac) = "RuleFK "^(tac2str tac) - | inout2str (Select tacs)= - "Select "^((strs2str' o (map tac2str)) tacs) - | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms) - | inout2str (Speed i) = "Speed "^(string_of_int i) - | inout2str (Active i) = "Active "^(string_of_int i) - | inout2str (Domain dI) = "Domain "^dI; -fun inouts2str ios = (strs2str' o (map inout2str)) ios; - -datatype mout = - Form' of inout (* packing cterm' | cterm' ppc *) -| Problems of inout (* passes specify (and solve) *) -| Error' of inout -| EmptyMout; - -fun mout2str (Form' inout) ="Form' "^(inout2str inout) - | mout2str (Error' inout) ="Error' "^(inout2str inout) - | mout2str (EmptyMout ) ="EmptyMout"; - -(*fun Form'2str (Form' )*) - - - - - -(* init pbl with ...,dsc,empty | [] *) -fun init_pbl pbt = - let - fun pbt2itm (f,(d,t)) = - ((0,[],false,f,Inc((d,[]),(e_term,[]))):itm); - in map pbt2itm pbt end; -(*take formal parameters from pbt, for transfer from pbl/met-hierarchy*) -fun init_pbl' pbt = - let - fun pbt2itm (f,(d,t)) = - ((0,[],false,f,Inc((d,[t]),(e_term,[]))):itm); - in map pbt2itm pbt end; - - -(*generate 1 ppobj in ptree*) -(*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*) -fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt = - (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef, - (Upblmet,itms2itemppc thy [][]))), - case p_ of Pbl => update_pbl pt p itmlist - | Met => update_met pt p itmlist) - | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt = - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), - case p_ of Pbl => update_pbl pt p itmlist - | Met => update_met pt p itmlist) - | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt = - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), - case p_ of Pbl => update_pbl pt p itmlist - | Met => update_met pt p itmlist) - - | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt = - (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), - update_domID pt p domID) - - | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate - (pos as (p,_)) pt = - let val pt = update_pbl pt p itms - val pt = update_pblID pt p pI - in ((p,Pbl),[], - Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), - pt) end - - | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate - (pos as (p,_)) pt = - let val pt = update_oris pt p oris - val pt = update_met pt p itms - val pt = update_metID pt p mID - in ((p,Met),[], - Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), - pt) end - - | generate1 thy (Model_Problem' (_, itms, met)) Uistate (pos as (p,_)) pt = -(* val (itms,pos as (p,_)) = (pbl, pos); - *) - let val pt = update_pbl pt p itms - val pt = update_met pt p met - in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, - (Upblmet,itms2itemppc thy [][]))), pt) end - - | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl)) - Uistate (pos as (p,_)) pt = - let val pt = update_pbl pt p pbl - val pt = update_orispec pt p (domID,pIre,metID) - in (pos,[], - Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))), - pt) end - - | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt = - let val (dI,_,mI) = get_obj g_spec pt p - val pt = update_spec pt p (dI, pI, mI) - in (pos,[], - Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt) - end - - | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt = - ((*writeln("###generate1 Apply_Method': pos = "^pos'2str (p,p_)); - writeln("###generate1 Apply_Method': topt= "^termopt2str topt); - writeln("###generate1 Apply_Method': is = "^istate2str is);*) - case topt of - SOME t => - let val (pt,c) = cappend_form pt p is t - (*val _= writeln("###generate1 Apply_Method: after cappend")*) - in (pos,c, EmptyMout,pt) - end - | NONE => - (pos,[],EmptyMout,update_env pt p (SOME is))) -(* val (thy, (Take' t), l, (p,p_), pt) = - ((assoc_thy "Isac.thy"), tac_, is, pos, pt); - *) - | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *) - let (*val _=writeln("### generate1: Take' pos="^pos'2str (p,p_));*) - val p = let val (ps,p') = split_last p(*no connex to prev.ppobj*) - in if p'=0 then ps@[1] else p end; - val (pt,c) = cappend_form pt p l t; - in ((p,Frm):pos', c, - Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end - -(* val (l, (p,p_)) = (RrlsState is, p); - - val (thy, Begin_Trans' t, l, (p,Frm), pt) = - (assoc_thy "Isac.thy", tac_, is, p, pt); - *) - | generate1 thy (Begin_Trans' t) l (p,Frm) pt = - let (* print_depth 99; - map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; - *) - val (pt,c) = cappend_form pt p l t - (* print_depth 99; - map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; - *) - val pt = update_branch pt p TransitiveB (*040312*) - (*replace the old PrfOjb ~~~~~*) - val p = (lev_on o lev_dn(*starts with [...,0]*)) p; - val (pt,c') = cappend_form pt p l t(*FIXME.0402 same istate ???*); - in ((p,Frm), c @ c', Form' (FormKF (~1,EdUndef,(length p), Nundef, - term2str t)), pt) end - - (* val (thy, Begin_Trans' t, l, (p,Res), pt) = - (assoc_thy "Isac.thy", tac_, is, p, pt); - *) - | generate1 thy (Begin_Trans' t) l (p ,Res) pt = - (*append after existing PrfObj _________*) - generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt - - | generate1 thy (End_Trans' tasm) l (p,p_) pt = - let val p' = lev_up p - val (pt,c) = append_result pt p' l tasm Complete; - in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), - pt) end - - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt = - let (*val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*) - val (pt,c) = cappend_atomic pt p l f - (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete; - val pt = update_branch pt p TransitiveB (*040312*) - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*) - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), - pt) end - - | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt = - let (*val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))*) - val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete - val pt = update_branch pt p TransitiveB (*040312*) - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*) - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), - pt)end - - | generate1 thy (Rewrite_Asm' all) l p pt = - generate1 thy (Rewrite' all) l p pt - - | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt = -(* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = - (assoc_thy "Isac.thy", tac_, is, pos, pt); - *) - let (*val _=writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*) - val (pt,c) = cappend_atomic pt p l f - (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete - val pt = update_branch pt p TransitiveB (*040312*) - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*) - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), - pt) end - - | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) l (p,p_) pt = - let val (pt,c) = cappend_form pt p l f - val pt = update_branch pt p TransitiveB (*040312*) - - val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f - val tac_ = Apply_Method' (e_metID, SOME t, is) - val pos' = ((lev_on o lev_dn) p, Frm) - in (*implicit Take*) generate1 thy tac_ is pos' pt end - - | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt = - let (*val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*) - val (pt,c) = cappend_atomic pt p l f - (Rewrite_Set (id_rls rls')) (f',asm) Complete - val pt = update_branch pt p TransitiveB (*040312*) - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*) - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), - pt) end - - | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) l (p,p_) pt = - let val (pt,c) = cappend_form pt p l f - val pt = update_branch pt p TransitiveB (*040312*) - - val is = init_istate (Rewrite_Set (id_rls rls)) f - val tac_ = Apply_Method' (e_metID, SOME t, is) - val pos' = ((lev_on o lev_dn) p, Frm) - in (*implicit Take*) generate1 thy tac_ is pos' pt end - - | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt = - let (*val _=writeln("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*) - (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*) - val (pt,c) = append_result pt p l (scval,map str2term asm) Complete - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), - Nundef, term2str scval)), pt) end - - | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt = - let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete; - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), - pt) end - - | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt = - let(*val _=writeln("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*) - val (pt,c) = cappend_atomic pt p l consts - (Check_elementwise pred) (f',asm) Complete; - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), - pt) end - - | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt = - let val (pt,c) = cappend_atomic pt p l ors - Or_to_List (list,[]) Complete; - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), - pt) end - - | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt = - let val (pt,c) = cappend_atomic pt p l t (Substitute (subte2sube subte)) - (t',[]) Complete; - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, - term2str t')), pt) - end - - | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt = - let val (pt,c) = cappend_atomic pt p l (str2term f) - (Tac id) (str2term f',[]) Complete; - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end - - | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f)) - l (p,p_) pt = - let (*val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))*) - val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) - (oris, (domID, pblID, metID), hdl); - (*val pbl = init_pbl ((#ppc o get_pbt) pblID); - val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*) - (*val _= writeln("### generate1: is([3],Frm)= "^ - (istate2str (get_istate pt ([3],Frm))));*) - val f = Syntax.string_of_term (thy2ctxt thy) f; - in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end - - | generate1 thy m' _ _ _ = - raise error ("generate1: not impl.for "^(tac_2str m')) -; - - -fun generate_hard thy m' (p,p_) pt = - let - val p = case p_ of Frm => p | Res => lev_on p - | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_))); - in generate1 thy m' e_istate (p,p_) pt end; - - - -(*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*) -(* val (tacis, (pt, _)) = (tacis, ptp); - - val (tacis, (pt, c, _)) = (rev tacis, (pt, [], (p, Res))); - *) -fun generate ([]: taci list) ptp = ptp - | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))= - let val (tacis', (_, tac_, (p, is))) = split_last tacis - (* for recursion ... - (tacis', (_, tac_, (p, is))) = split_last tacis'; - *) - val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt - in generate tacis' (pt', c@c', p') end; - - - -(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls * - * of for connecting a user-input formula with the current calc-state. * - *# It is somewhat incompatible with the rest of the math-engine: * - * (1) it is not created by a script * - * (2) thus there cannot be another user-input within a derivation * - *# It suffers particularily from the not-well-foundedness of the math-engine* - * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' * - * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) * - * (3) FIXME and eventually 'lev_back' * - *# SOME improvements are evident FIXME.040215 '_deriv'ation: * - * (1) FIXME nest Rls_ in 'make_deriv' * - * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus * - * user-input will become possible in this part of a derivation * - * (3) FIXME do (2) only if a derivation has been found -- for efficiency, * - * while a non-derivable inform requires to step until End_Proof' * - * (4) FIXME find criteria on when _not_ to step until End_Proof' * - * (5) FIXME -.*) -(*.update pos in tacis for embedding by generate.*) -(* val - *) -fun insert_pos _ [] = [] - | insert_pos (p:pos) (((tac,tac_,(_, ist))::tacis):taci list) = - ((tac,tac_,((p, Res), ist)):taci) - ::((insert_pos (lev_on p) tacis):taci list); - -fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm) - | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm) - | res_from_taci (_, tac_, _) = - raise error ("res_from_taci: called with" ^ tac_2str tac_); - -(*.embed the tacis created by a '_deriv'ation; sys.form <> input.form - tacis are in order, thus are reverted for generate.*) -(* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp); - *) -fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') = - (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402 - and transfer the istate (from _after_ compare_deriv) from Frm to Res*) - let val (res, asm) = (res_from_taci o last_elem) tacis - val (SOME ist,_) = get_obj g_loc pt p - val form = get_obj g_form pt p - (*val p = lev_on p; ---------------only difference to (..,Res) below*) - val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate)) - ::(insert_pos ((lev_on o lev_dn) p) tacis) - @ [(End_Trans, End_Trans' (res, asm), - (pos_plus (length tacis) (lev_dn p, Res), - new_val res ist))] - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p)) - val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res)) - val pt = update_tac pt p (Derive (id_rls nrls)) - (*FIXME.040216 struct.ctree*) - val pt = update_branch pt p TransitiveB - in (c, (pt, pos:pos')) end - -(* val (tacis, (pt, (p, Res))) = (tacis', ptp); - *) - | embed_deriv tacis (pt, (p, Res)) = - (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ? - and transfer the istate (from _after_ compare_deriv) from Res to new Res*) - let val (res, asm) = (res_from_taci o last_elem) tacis - val (_, SOME ist) = get_obj g_loc pt p - val (f,a) = get_obj g_result pt p - val p = lev_on p(*---------------only difference to (..,Frm) above*); - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate)) - ::(insert_pos ((lev_on o lev_dn) p) tacis) - @ [(End_Trans, End_Trans' (res, asm), - (pos_plus (length tacis) (lev_dn p, Res), - new_val res ist))]; - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p)) - val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res)) - val pt = update_tac pt p (Derive (id_rls nrls)) - (*FIXME.040216 struct.ctree*) - val pt = update_branch pt p TransitiveB - in (c, (pt, pos)) end;