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