neuper@37906: (* solve an example by interpreting a method's script neuper@37906: (c) Walther Neuper 1999 neuper@37906: neuper@37906: use"ME/solve.sml"; neuper@37906: use"solve.sml"; neuper@37906: *) neuper@37906: neuper@37906: fun safe (ScrState (_,_,_,_,s,_)) = s neuper@37906: | safe (RrlsState _) = Safe; neuper@37906: neuper@37906: type mstID = string; neuper@37906: type tac'_ = mstID * tac; (*DG <-> ME*) neuper@37906: val e_tac'_ = ("Empty_Tac", Empty_Tac):tac'_; neuper@37906: neuper@37906: fun mk_tac'_ m = case m of neuper@37906: Init_Proof (ppc, spec) => ("Init_Proof", Init_Proof (ppc, spec )) neuper@37906: | Model_Problem => ("Model_Problem", Model_Problem) neuper@37906: | Refine_Tacitly pblID => ("Refine_Tacitly", Refine_Tacitly pblID) neuper@37906: | Refine_Problem pblID => ("Refine_Problem", Refine_Problem pblID) neuper@37906: | Add_Given cterm' => ("Add_Given", Add_Given cterm') neuper@37906: | Del_Given cterm' => ("Del_Given", Del_Given cterm') neuper@37906: | Add_Find cterm' => ("Add_Find", Add_Find cterm') neuper@37906: | Del_Find cterm' => ("Del_Find", Del_Find cterm') neuper@37906: | Add_Relation cterm' => ("Add_Relation", Add_Relation cterm') neuper@37906: | Del_Relation cterm' => ("Del_Relation", Del_Relation cterm') neuper@37906: neuper@37906: | Specify_Theory domID => ("Specify_Theory", Specify_Theory domID) neuper@37906: | Specify_Problem pblID => ("Specify_Problem", Specify_Problem pblID) neuper@37906: | Specify_Method metID => ("Specify_Method", Specify_Method metID) neuper@37906: | Apply_Method metID => ("Apply_Method", Apply_Method metID) neuper@37906: | Check_Postcond pblID => ("Check_Postcond", Check_Postcond pblID) neuper@37906: | Free_Solve => ("Free_Solve",Free_Solve) neuper@37906: neuper@37906: | Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Rewrite_Inst (subs, thm')) neuper@37906: | Rewrite thm' => ("Rewrite", Rewrite thm') neuper@37906: | Rewrite_Asm thm' => ("Rewrite_Asm", Rewrite_Asm thm') neuper@37906: | Rewrite_Set_Inst (subs, rls') neuper@37906: => ("Rewrite_Set_Inst", Rewrite_Set_Inst (subs, rls')) neuper@37906: | Rewrite_Set rls' => ("Rewrite_Set", Rewrite_Set rls') neuper@37906: | End_Ruleset => ("End_Ruleset", End_Ruleset) neuper@37906: neuper@37906: | End_Detail => ("End_Detail", End_Detail) neuper@37906: | Detail_Set rls' => ("Detail_Set", Detail_Set rls') neuper@37906: | Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Detail_Set_Inst (s, rls')) neuper@37906: neuper@37906: | Calculate op_ => ("Calculate", Calculate op_) neuper@37906: | Substitute sube => ("Substitute", Substitute sube) neuper@37906: | Apply_Assumption cts' => ("Apply_Assumption", Apply_Assumption cts') neuper@37906: neuper@37906: | Take cterm' => ("Take", Take cterm') neuper@37906: | Take_Inst cterm' => ("Take_Inst", Take_Inst cterm') neuper@37906: | Group (con, ints) => ("Group", Group (con, ints)) neuper@37906: | Subproblem (domID, pblID) => ("Subproblem", Subproblem (domID, pblID)) neuper@37906: (* neuper@37906: | Subproblem_Full(spec,cts')=> ("Subproblem_Full", Subproblem_Full(spec,cts')) neuper@37906: *) neuper@37906: | End_Subproblem => ("End_Subproblem",End_Subproblem) neuper@37906: | CAScmd cterm' => ("CAScmd", CAScmd cterm') neuper@37906: neuper@37906: | Split_And => ("Split_And", Split_And) neuper@37906: | Conclude_And => ("Conclude_And", Conclude_And) neuper@37906: | Split_Or => ("Split_Or", Split_Or) neuper@37906: | Conclude_Or => ("Conclude_Or", Conclude_Or) neuper@37906: | Begin_Trans => ("Begin_Trans", Begin_Trans) neuper@37906: | End_Trans => ("End_Trans", End_Trans) neuper@37906: | Begin_Sequ => ("Begin_Sequ", Begin_Sequ) neuper@37906: | End_Sequ => ("End_Sequ", Begin_Sequ) neuper@37906: | Split_Intersect => ("Split_Intersect", Split_Intersect) neuper@37906: | End_Intersect => ("End_Intersect", End_Intersect) neuper@37906: | Check_elementwise cterm' => ("Check_elementwise", Check_elementwise cterm') neuper@37906: | Or_to_List => ("Or_to_List", Or_to_List) neuper@37906: | Collect_Trues => ("Collect_Results", Collect_Trues) neuper@37906: neuper@37906: | Empty_Tac => ("Empty_Tac",Empty_Tac) neuper@37906: | Tac string => ("Tac",Tac string) neuper@37906: | User => ("User",User) neuper@37906: | End_Proof' => ("End_Proof'",End_Proof'); neuper@37906: neuper@37906: (*Detail*) neuper@37906: val empty_tac'_ = (mk_tac'_ Empty_Tac):tac'_; neuper@37906: neuper@37906: fun mk_tac ((_,m):tac'_) = m; neuper@37906: fun mk_mstID ((mI,_):tac'_) = mI; neuper@37906: neuper@37906: fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms); neuper@37906: (* TODO: tac2str, tac'_2str NOT tested *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: type squ = ptree; (* TODO: safe etc. *) neuper@37906: neuper@37906: (*13.9.02-------------- neuper@37906: type ctr = (loc * pos) list; neuper@38014: val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","op *"), neuper@37906: ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; neuper@37980: ML {* neuper@37980: @{term "PLUS"}; (*Free ("PLUS", "'a") : term*) neuper@37980: @{term "plus"}; (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*) neuper@37980: @{term "MINUS"}; (*Free ("MINUS", "'a")*) neuper@37980: @{term "minus"}; (*Const ("Groups.minus_class.minus", "'a => 'a => 'a")*) neuper@37980: @{term "TIMES"}; (*Free ("TIMES", "'a")*) neuper@37980: @{term "times"}; (*Const ("Groups.times_class.times", "'a => 'a => 'a")*) neuper@37980: @{term "CANCEL"}; (*Free ("CANCEL", "'a")*) neuper@37980: @{term "cancel"}; (*Free ("cancel", "'a")*) neuper@37980: @{term "POWER"}; (*Free ("POWER", "'a")*) neuper@37980: @{term "pow"}; (*Free ("pow", "'a")*) neuper@37980: @{term "SQRT"}; (*Free ("SQRT", "'a")*) neuper@37980: @{term "sqrt"}; (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*) neuper@37980: *} neuper@37906: fun op_intern op_ = neuper@37980: case assoc (ops, op_) of neuper@38031: SOME op' => op' | NONE => error ("op_intern: no op= "^op_); neuper@37906: -----------------------*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* use"ME/solve.sml"; neuper@37906: use"solve.sml"; neuper@37906: neuper@37906: val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g"; neuper@37906: val ttt = (term_of o the o (parse thy))"Rewrite thmid True g"; neuper@37906: neuper@37906: Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f' neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: val specsteps = ["Init_Proof","Refine_Tacitly","Refine_Problem", neuper@37906: "Model_Problem",(*"Match_Problem",*) neuper@37906: "Add_Given","Del_Given","Add_Find","Del_Find", neuper@37906: "Add_Relation","Del_Relation", neuper@37906: "Specify_Theory","Specify_Problem","Specify_Method"]; neuper@37906: neuper@37906: "-----------------------------------------------------------------------"; neuper@37906: neuper@37906: neuper@37906: fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*) neuper@37906: (tac_2tac tac_, tac_, (p, get_istate pt p)):taci; neuper@37906: neuper@37906: neuper@37906: (*FIXME.WN050821 compare solve ... nxt_solv*) neuper@37906: (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); neuper@37906: val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos); neuper@37906: *) neuper@37906: fun solve ("Apply_Method", m as Apply_Method' (mI, _, _)) neuper@37906: (pt:ptree, (pos as (p,_))) = neuper@37906: let val {srls,...} = get_met mI; neuper@37906: val PblObj{meth=itms,...} = get_obj I pt p; neuper@37906: val thy' = get_obj g_domID pt p; neuper@37906: val thy = assoc_thy thy'; neuper@37906: val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI; neuper@37906: val ini = init_form thy sc env; neuper@37906: val p = lev_dn p; neuper@37906: in neuper@37906: case ini of neuper@37926: SOME t => (* val SOME t = ini; neuper@37906: *) neuper@37906: let val (pos,c,_,pt) = neuper@37926: generate1 thy (Apply_Method' (mI, SOME t, is)) neuper@37906: is (lev_on p, Frm)(*implicit Take*) pt; neuper@37926: in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is), neuper@37906: ((lev_on p, Frm), is))], c, (pt,pos)):calcstate') neuper@37906: end neuper@37926: | NONE => (*execute the first tac in the Script, compare solve m*) neuper@37906: let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is; neuper@37906: val d = e_rls (*FIXME: get simplifier from domID*); neuper@37906: in neuper@37906: case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of neuper@37906: Steps (is'', ss as (m'',f',pt',p',c')::_) => neuper@37906: (* val Steps (is'', ss as (m'',f',pt',p',c')::_) = neuper@37906: locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is'; neuper@37906: *) neuper@37906: ("ok", (map step2taci ss, c', (pt',p'))) neuper@37906: | NotLocatable => neuper@37906: let val (p,ps,f,pt) = neuper@37906: generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt; neuper@37906: in ("not-found-in-script", neuper@37906: ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end neuper@37906: (*just-before------------------------------------------------------ neuper@37926: ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate), neuper@37906: (pos, is))], neuper@37926: [], (update_env pt (fst pos) (SOME is),pos))) neuper@37906: -----------------------------------------------------------------*) neuper@37906: end neuper@37906: end neuper@37906: neuper@37906: | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) = neuper@38015: let (*val _=tracing"###solve Free_Solve";*) neuper@37906: val p' = lev_dn_ (p,Res); neuper@37906: val pt = update_metID pt (par_pblobj pt p) e_metID; neuper@37906: in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*) neuper@37906: [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end neuper@37906: neuper@37906: (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) = neuper@37906: ( m, (pt, pos)); neuper@37906: *) neuper@37906: | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) = neuper@38015: let (*val _=tracing"###solve Check_Postcond";*) neuper@37906: val pp = par_pblobj pt p neuper@37906: val asm = (case get_obj g_tac pt p of neuper@37906: Check_elementwise _ => (*collects and instantiates asms*) neuper@37906: (snd o (get_obj g_result pt)) p neuper@37906: | _ => ((map fst) o (get_assumptions_ pt)) (p,p_)) neuper@37906: handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) neuper@37906: val metID = get_obj g_metID pt pp; neuper@37906: val {srls=srls,scr=sc,...} = get_met metID; neuper@37906: val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); neuper@38015: (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); neuper@38015: val _= tracing("### solve Check_postc, is= "^(istate2str is));*) neuper@37906: val thy' = get_obj g_domID pt pp; neuper@37906: val thy = assoc_thy thy'; neuper@37906: val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; neuper@38015: (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*) neuper@37906: neuper@37906: in if pp = [] then neuper@37906: let val is = ScrState (E,l,a,scval,scsaf,b) neuper@37906: val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) neuper@37906: val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt; neuper@37906: in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*) neuper@37906: [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end neuper@37906: else neuper@37906: let neuper@37906: (*resume script of parpbl, transfer value of subpbl-script*) neuper@37906: val ppp = par_pblobj pt (lev_up p); neuper@37906: val thy' = get_obj g_domID pt ppp; neuper@37906: val thy = assoc_thy thy'; neuper@37906: val metID = get_obj g_metID pt ppp; neuper@37906: val sc = (#scr o get_met) metID; neuper@37906: val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm); neuper@38015: (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm))); neuper@38015: val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is)); neuper@38015: val _=tracing("### solve Check_postc, is'= "^ neuper@37906: (istate2str (E,l,a,scval,scsaf,b)));*) neuper@37906: val ((p,p_),ps,f,pt) = neuper@37906: generate1 thy (Check_Postcond' (pI, (scval, map term2str asm))) neuper@37906: (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt; neuper@38015: (*val _=tracing("### solve Check_postc, is(pt')= "^ neuper@37906: (istate2str (get_istate pt ([3],Res)))); neuper@37906: val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc neuper@37906: (ScrState (E,l,a,scval,scsaf,b));*) neuper@37906: in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*) neuper@37906: ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)), neuper@37906: ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_)))) neuper@37906: end neuper@37906: end neuper@37906: (* val (msg, cs') = neuper@37906: ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))), neuper@37906: ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_)))); neuper@37906: val (_,(pt',p')) = cs'; neuper@38015: (tracing o istate2str) (get_istate pt' p'); neuper@37906: (term2str o fst) (get_obj g_result pt' (fst p')); neuper@37906: *) neuper@37906: neuper@38015: (* tracing(istate2str(get_istate pt (p,p_))); neuper@37906: *) neuper@37906: | solve (_,End_Proof'') (pt, (p,p_)) = neuper@37906: ("end-proof", neuper@37906: ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*) neuper@37906: [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_)))) neuper@37906: neuper@37906: (*-----------vvvvvvvvvvv could be done by generate1 ?!?*) neuper@37906: | solve (_,End_Detail' t) (pt,(p,p_)) = neuper@37906: let val pr as (p',_) = (lev_up p, Res) neuper@37906: val pp = par_pblobj pt p neuper@37906: val r = (fst o (get_obj g_result pt)) p' neuper@37906: (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) neuper@37906: val thy' = get_obj g_domID pt pp neuper@37906: val (srls, is, sc) = from_pblobj' thy' pr pt neuper@37906: val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is neuper@37906: in ("ok", ((*((pp,Frm(*???*)),is,tac_), neuper@37906: Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)), neuper@37906: tac_2tac tac_, Sundef,*) neuper@37906: [(End_Detail, End_Detail' t , neuper@37906: ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end neuper@37906: neuper@37906: | solve (mI,m) (pt, po as (p,p_)) = neuper@37906: (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); neuper@37906: *) neuper@37906: if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: neuper@37906: could be detail, too !!*) neuper@37906: then let val ((p,p_),ps,f,pt) = neuper@37906: generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) neuper@37906: m e_istate (p,p_) pt; neuper@37906: in ("no-method-specified", (*Free_Solve*) neuper@37906: ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) neuper@37906: [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end neuper@37906: else neuper@37906: let neuper@37906: val thy' = get_obj g_domID pt (par_pblobj pt p); neuper@37906: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; neuper@38015: (*val _= tracing("### solve, before locate_gen p="^(pos'2str(p,p_)));*) neuper@37906: val d = e_rls; (*FIXME: canon.simplifier for domain is missing neuper@37906: 8.01: generate from domID?*) neuper@37906: in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of neuper@37906: Steps (is', ss as (m',f',pt',p',c')::_) => neuper@37906: (* val Steps (is', ss as (m',f',pt',p',c')::_) = neuper@37906: locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; neuper@37906: *) neuper@38015: let (*val _= tracing("### solve, after locate_gen: is= ") neuper@38015: val _= tracing(istate2str is')*) neuper@37906: (*val nxt_ = neuper@37906: case p' of (*change from solve to model subpbl*) neuper@37906: (_,Pbl) => nxt_model_pbl m' (pt',p') neuper@37906: | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*) neuper@37906: (*27.8.02:next_tac may change to other branches in pt FIXXXXME*) neuper@37906: in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*) neuper@37906: map step2taci ss, c', (pt',p'))) end neuper@37906: | NotLocatable => neuper@37906: let val (p,ps,f,pt) = neuper@37906: generate_hard (assoc_thy "Isac.thy") m (p,p_) pt; neuper@37906: in ("not-found-in-script", neuper@37906: ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) neuper@37906: [(tac_2tac m, m, (po,is))], ps, (pt,p))) end neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: (*FIXME.WN050821 compare solve ... nxt_solv*) neuper@37906: (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) neuper@37906: fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) = neuper@37906: (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) = neuper@37926: ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp); neuper@37906: *) neuper@37906: let val {srls,ppc,...} = get_met mI; neuper@37906: val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p; neuper@37906: val itms = if itms <> [] then itms neuper@37906: else complete_metitms oris probl [] ppc neuper@37906: val thy' = get_obj g_domID pt p; neuper@37906: val thy = assoc_thy thy'; neuper@37906: val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI; neuper@37906: val ini = init_form thy scr env; neuper@37906: in neuper@37906: case ini of neuper@37926: SOME t => (* val SOME t = ini; neuper@37906: *) neuper@37906: let val pos = ((lev_on o lev_dn) p, Frm) neuper@37926: val tac_ = Apply_Method' (mI, SOME t, is); neuper@37906: val (pos,c,_,pt) = (*implicit Take*) neuper@37906: generate1 thy tac_ is pos pt neuper@37906: (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*) neuper@37906: in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end neuper@37926: | NONE => neuper@37926: let val pt = update_env pt (fst pos) (SOME is) neuper@37906: val (tacis, c, ptp) = nxt_solve_ (pt, pos) neuper@37906: in (tacis @ neuper@37926: [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))], neuper@37906: c, ptp) end neuper@37906: end neuper@37906: (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m); neuper@37906: val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) = neuper@37906: (tac_, is, ptp); neuper@37906: *) neuper@37906: (*TODO.WN050913 remove unnecessary code below*) neuper@37906: | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) = neuper@38015: let (*val _=tracing"###solve Check_Postcond";*) neuper@37906: val pp = par_pblobj pt p neuper@37906: val asm = (case get_obj g_tac pt p of neuper@37906: Check_elementwise _ => (*collects and instantiates asms*) neuper@37906: (snd o (get_obj g_result pt)) p neuper@37906: | _ => ((map fst) o (get_assumptions_ pt)) (p,p_)) neuper@37906: handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) neuper@37906: val metID = get_obj g_metID pt pp; neuper@37906: val {srls=srls,scr=sc,...} = get_met metID; neuper@37906: val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); neuper@38015: (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); neuper@38015: val _= tracing("### solve Check_postc, is= "^(istate2str is));*) neuper@37906: val thy' = get_obj g_domID pt pp; neuper@37906: val thy = assoc_thy thy'; neuper@37906: val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; neuper@38015: (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*) neuper@37906: in if pp = [] then neuper@37906: let val is = ScrState (E,l,a,scval,scsaf,b) neuper@37906: val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) neuper@38015: (*val _= tracing"### nxt_solv2 Apply_Method: stored is ="; neuper@38015: val _= tracing(istate2str is);*) neuper@37906: val ((p,p_),ps,f,pt) = neuper@37906: generate1 thy tac_ is (pp,Res) pt; neuper@37906: in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end neuper@37906: else neuper@37906: let neuper@37906: (*resume script of parpbl, transfer value of subpbl-script*) neuper@37906: val ppp = par_pblobj pt (lev_up p); neuper@37906: val thy' = get_obj g_domID pt ppp; neuper@37906: val thy = assoc_thy thy'; neuper@37906: val metID = get_obj g_metID pt ppp; neuper@37906: val {scr,...} = get_met metID; neuper@37906: val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm) neuper@37906: val tac_ = Check_Postcond' (pI, (scval, map term2str asm)) neuper@37906: val is = ScrState (E,l,a,scval,scsaf,b) neuper@38015: (*val _= tracing"### nxt_solv3 Apply_Method: stored is ="; neuper@38015: val _= tracing(istate2str is);*) neuper@37906: val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt; neuper@37906: (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*) neuper@37906: in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end neuper@37906: end neuper@38015: (* tracing(istate2str(get_istate pt (p,p_))); neuper@37906: *) neuper@37906: neuper@37906: (*.start interpreter and do one rewrite.*) neuper@37906: (* val (_,Detail_Set'(thy',rls,t)) = (mI,m); val p = (p,p_); neuper@37906: solve ("",Detail_Set'(thy', rls, t)) p pt; neuper@37906: | nxt_solv (Detail_Set'(thy', rls, t)) _ (pt, p) = ********** neuper@37947: ---> Frontend/sml.sml neuper@37906: neuper@37906: | nxt_solv (End_Detail' t) _ (pt, (p,p_)) = ********** neuper@37906: let val pr as (p',_) = (lev_up p, Res) neuper@37906: val pp = par_pblobj pt p neuper@37906: val r = (fst o (get_obj g_result pt)) p' neuper@37906: (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) neuper@37906: val thy' = get_obj g_domID pt pp neuper@37906: val (srls, is, sc) = from_pblobj' thy' pr pt neuper@37906: val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is neuper@37906: in (pr, ((pp,Frm(*???*)),is,tac_), neuper@37906: Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)), neuper@37906: tac_2tac tac_, Sundef, pt) end neuper@37906: *) neuper@37906: | nxt_solv (End_Proof'') _ ptp = ([], [], ptp) neuper@37906: neuper@37906: | nxt_solv tac_ is (pt, pos as (p,p_)) = neuper@37906: (* val (pt, pos as (p,p_)) = ptp; neuper@37906: *) neuper@37906: let val pos = case pos of neuper@37906: (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*) neuper@37906: | (p, Res) => (lev_on p,Res) (*somewhere in script*) neuper@37906: | _ => pos (*somewhere in script*) neuper@38015: (*val _= tracing"### nxt_solv4 Apply_Method: stored is ="; neuper@38015: val _= tracing(istate2str is);*) neuper@37906: val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt; neuper@37906: in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end neuper@37906: neuper@37906: neuper@37906: (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*) neuper@37906: neuper@37906: neuper@37906: (*.find the next tac from the script, nxt_solv will update the ptree.*) neuper@37906: (* val (ptp as (pt,pos as (p,p_))) = ptp'; neuper@37906: val (ptp as (pt, pos as (p,p_))) = ptp''; neuper@37906: val (ptp as (pt, pos as (p,p_))) = ptp; neuper@37906: val (ptp as (pt, pos as (p,p_))) = (pt,ip); neuper@37906: val (ptp as (pt, pos as (p,p_))) = (pt, pos); neuper@37906: *) neuper@37906: and nxt_solve_ (ptp as (pt, pos as (p,p_))) = neuper@37906: if e_metID = get_obj g_metID pt (par_pblobj pt p) neuper@37906: then ([], [], (pt,(p,p_))):calcstate' neuper@37906: else let val thy' = get_obj g_domID pt (par_pblobj pt p); neuper@37906: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; neuper@37906: val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; neuper@37906: (*TODO here ^^^ return finished/helpless/ok !*) neuper@37906: (* val (tac_',is',(t',_)) = next_tac (thy',srls) (pt,pos) sc is; neuper@37906: *) neuper@37906: in case tac_ of neuper@37906: End_Detail' _ => ([(End_Detail, neuper@37906: End_Detail' (t,[(*FIXME.040215*)]), neuper@37906: (pos, is))], [], (pt, pos)) neuper@37906: | _ => nxt_solv tac_ is ptp end; neuper@37906: neuper@37906: (*.says how may steps of a calculation should be done by "fun autocalc".*) neuper@37906: (*TODO.WN0512 redesign togehter with autocalc ?*) neuper@37906: datatype auto = neuper@37906: Step of int (*1 do #int steps; may stop in model/specify: neuper@37906: IS VERY INEFFICIENT IN MODEL/SPECIY*) neuper@37906: | CompleteModel (*2 complete modeling neuper@37906: if model complete, finish specifying + start solving*) neuper@37906: | CompleteCalcHead (*3 complete model/specify in one go + start solving*) neuper@37906: | CompleteToSubpbl (*4 stop at the next begin of a subproblem, neuper@37906: if none, complete the actual (sub)problem*) neuper@37906: | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*) neuper@37906: | CompleteCalc; (*6 complete the calculation as a whole*) neuper@37906: fun autoord (Step _ ) = 1 neuper@37906: | autoord CompleteModel = 2 neuper@37906: | autoord CompleteCalcHead = 3 neuper@37906: | autoord CompleteToSubpbl = 4 neuper@37906: | autoord CompleteSubpbl = 5 neuper@37906: | autoord CompleteCalc = 6; neuper@37906: neuper@37906: (* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp); neuper@37906: *) neuper@37906: fun complete_solve auto c (ptp as (_, p): ptree * pos') = neuper@37906: if p = ([], Res) then ("end-of-calculation", [], ptp) else neuper@37906: case nxt_solve_ ptp of neuper@37906: ((Subproblem _, tac_, (_, is))::_, c', ptp') => neuper@37906: (* val ptp' = ptp'''; neuper@37906: *) neuper@37906: if autoord auto < 5 then ("ok", c@c', ptp) neuper@37906: else let val ptp = all_modspec ptp'; neuper@37906: val (_, c'', ptp) = all_solve auto (c@c') ptp; neuper@37906: in complete_solve auto (c@c'@c'') ptp end neuper@37906: | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) => neuper@37906: if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp') neuper@37906: else complete_solve auto (c@c') ptp' neuper@37906: | ((End_Detail, _, _)::_, c', ptp') => neuper@37906: if autoord auto < 6 then ("ok", c@c', ptp') neuper@37906: else complete_solve auto (c@c') ptp' neuper@37906: | (_, c', ptp') => complete_solve auto (c@c') ptp' neuper@37906: (* val (tacis, c', ptp') = nxt_solve_ ptp; neuper@37906: val (tacis, c', ptp'') = nxt_solve_ ptp'; neuper@37906: val (tacis, c', ptp''') = nxt_solve_ ptp''; neuper@37906: val (tacis, c', ptp'''') = nxt_solve_ ptp'''; neuper@37906: val (tacis, c', ptp''''') = nxt_solve_ ptp''''; neuper@37906: *) neuper@37906: and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = neuper@37906: (* val (ptp as (pt, (p,_))) = ptp; neuper@37906: val (ptp as (pt, (p,_))) = ptp'; neuper@37906: val (ptp as (pt, (p,_))) = (pt, pos); neuper@37906: *) neuper@37906: let val (_,_,mI) = get_obj g_spec pt p; neuper@37926: val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) neuper@37906: e_istate ptp; neuper@37906: in complete_solve auto (c@c') ptp end; neuper@37906: (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) neuper@37906: fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = neuper@37906: if p = ([], Res) then ("end-of-calculation", [], ptp) else neuper@37935: if member op = [Pbl,Met] p_ neuper@37906: then let val ptp = all_modspec ptp neuper@37906: val (_, c', ptp) = all_solve auto c ptp neuper@37906: in complete_solve auto (c@c') ptp end neuper@37906: else case nxt_solve_ ptp of neuper@37906: ((Subproblem _, tac_, (_, is))::_, c', ptp') => neuper@37906: if autoord auto < 5 then ("ok", c@c', ptp) neuper@37906: else let val ptp = all_modspec ptp' neuper@37906: val (_, c'', ptp) = all_solve auto (c@c') ptp neuper@37906: in complete_solve auto (c@c'@c'') ptp end neuper@37906: | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) => neuper@37906: if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp') neuper@37906: else complete_solve auto (c@c') ptp' neuper@37906: | ((End_Detail, _, _)::_, c', ptp') => neuper@37906: if autoord auto < 6 then ("ok", c@c', ptp') neuper@37906: else complete_solve auto (c@c') ptp' neuper@37906: | (_, c', ptp') => complete_solve auto (c@c') ptp' neuper@37906: and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = neuper@37906: let val (_,_,mI) = get_obj g_spec pt p neuper@37926: val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) neuper@37906: e_istate ptp neuper@37906: in complete_solve auto (c@c') ptp end; neuper@37906: neuper@37906: (*.aux.fun for detailrls with Rrls, reverse rewriting.*) neuper@37906: (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms); neuper@37906: *) neuper@37906: fun rul_terms_2nds nds t [] = nds neuper@37906: | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) = neuper@37906: (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) :: neuper@37906: (rul_terms_2nds nds t' rts); neuper@37906: neuper@37906: neuper@37906: (*. detail steps done internally by Rewrite_Set* neuper@37906: into ctree by use of a script .*) neuper@37906: (* val (pt, (p,p_)) = (pt, pos); neuper@37906: *) neuper@37906: fun detailrls pt ((p,p_):pos') = neuper@37906: let val t = get_obj g_form pt p neuper@37906: val tac = get_obj g_tac pt p neuper@37906: val rls = (assoc_rls o rls_of) tac neuper@37906: in case rls of neuper@37906: (* val Rrls {scr = Rfuns {init_state,...},...} = rls; neuper@37906: *) neuper@37906: Rrls {scr = Rfuns {init_state,...},...} => neuper@37906: let val (_,_,_,rul_terms) = init_state t neuper@37906: val newnds = rul_terms_2nds [] t rul_terms neuper@37906: val pt''' = ins_chn newnds pt p neuper@37906: in ("detailrls", pt''', (p @ [length newnds], Res):pos') end neuper@37906: | _ => neuper@37906: let val is = init_istate tac t neuper@37906: (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] neuper@37906: is wrong for simpl, but working ?!? *) neuper@37906: val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), neuper@37926: SOME t, is) neuper@37906: val pos' = ((lev_on o lev_dn) p, Frm) neuper@37906: val thy = assoc_thy "Isac.thy" neuper@37906: val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt neuper@37906: val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos') neuper@37906: val newnds = children (get_nd pt'' p) neuper@37906: val pt''' = ins_chn newnds pt p neuper@37906: (*complete_solve cuts branches after*) neuper@37906: in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*), neuper@37906: (p @ [length newnds], Res):pos') end neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* val(mI,m)=m;val ppp=p;(*!!!*)val(p,p_)=pos;val(_,pt,_)=ppp(*!!!*); neuper@37906: get_form ((mI,m):tac'_) ((p,p_):pos') ppp; neuper@37906: *) neuper@37906: fun get_form ((mI,m):tac'_) ((p,p_):pos') pt = neuper@37906: case applicable_in (p,p_) pt m of neuper@37906: Notappl e => Error' (Error_ e) neuper@37906: | Appl m => neuper@37906: (* val Appl m=applicable_in (p,p_) pt m; neuper@37906: *) neuper@37935: if member op = specsteps mI neuper@37906: then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt neuper@37906: in f end neuper@37906: else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_)) neuper@37906: in (*f*) EmptyMout end; neuper@37906: