61 string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt) |
61 string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt) |
62 AND |
62 AND |
63 FROM val oris = prep_ori... |
63 FROM val oris = prep_ori... |
64 TO val (oris, _) = prep_ori... |
64 TO val (oris, _) = prep_ori... |
65 *) |
65 *) |
66 "----- insert ctxt in ptree"; |
66 "----- insert ctxt in ctree"; |
67 (* datatype ppobj |
67 (* datatype ppobj |
68 FROM loc : istate option * istate option, |
68 FROM loc : istate option * istate option, |
69 TO loc : (istate * ctxt) option * (istate * ctxt) option, |
69 TO loc : (istate * ctxt) option * (istate * ctxt) option, |
70 e.g. |
70 e.g. |
71 FROM val pt = Nd (PblObj |
71 FROM val pt = Nd (PblObj |
495 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
495 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
496 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
496 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
497 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
497 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
498 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
498 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
499 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
499 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
500 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) = |
500 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = |
501 (nxt, p, [], pt); |
501 (nxt, p, [], pt); |
502 val ("ok", (_, _, ptp)) = locatetac tac (pt,p) |
502 val ("ok", (_, _, ptp)) = locatetac tac (pt,p) |
503 val (pt, p) = ptp; |
503 val (pt, p) = ptp; |
504 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
504 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
505 (p, ((pt, e_pos'),[])); |
505 (p, ((pt, e_pos'),[])); |
544 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) |
544 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) |
545 val dI = theory2theory' (maxthy thy thy'); |
545 val dI = theory2theory' (maxthy thy thy'); |
546 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
546 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
547 cas = NONE; (*true*) |
547 cas = NONE; (*true*) |
548 val hdl = pblterm dI pI; |
548 val hdl = pblterm dI pI; |
549 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) |
549 val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) |
550 (pors, (dI, pI, mI), hdl) |
550 (pors, (dI, pI, mI), hdl) |
551 val pt = update_ctxt pt [] pctxt; |
551 val pt = update_ctxt pt [] pctxt; |
552 |
552 |
553 "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl))); |
553 "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl))); |
554 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p; |
554 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p; |
602 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt; |
602 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt; |
603 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos'); |
603 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos'); |
604 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*) |
604 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*) |
605 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, |
605 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, |
606 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
606 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
607 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) = |
607 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) = |
608 (CompleteSubpbl, [], (pt',pos')); |
608 (CompleteSubpbl, [], (pt',pos')); |
609 p = ([], Res) = false; |
609 p = ([], Res) = false; |
610 member op = [Pbl,Met] p_ = false; |
610 member op = [Pbl,Met] p_ = false; |
611 val (_, c', ptp') = nxt_solve_ ptp; |
611 val (_, c', ptp') = nxt_solve_ ptp; |
612 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, |
612 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, |
615 e_metID = get_obj g_metID pt (par_pblobj pt p) = false; |
615 e_metID = get_obj g_metID pt (par_pblobj pt p) = false; |
616 val thy' = get_obj g_domID pt (par_pblobj pt p); |
616 val thy' = get_obj g_domID pt (par_pblobj pt p); |
617 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
617 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
618 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; |
618 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; |
619 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) |
619 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) |
620 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), |
620 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
621 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
621 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
622 l = [] = false; |
622 l = [] = false; |
623 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) |
623 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) |
624 BUT WE FIND IN THE CODE ABOVE IN next_tac:*) |
624 BUT WE FIND IN THE CODE ABOVE IN next_tac:*) |
625 ; |
625 ; |
649 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = |
649 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = |
650 (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete); |
650 (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete); |
651 existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false; |
651 existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false; |
652 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm)); |
652 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm)); |
653 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c; |
653 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c; |
654 (append_atomic p ist_res f r f' s) : ptree -> ptree; |
654 (append_atomic p ist_res f r f' s) : ctree -> ctree; |
655 ; |
655 ; |
656 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH |
656 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH |
657 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*) |
657 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*) |
658 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm)); |
658 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm)); |
659 val ((pt,_),_) = get_calc cI |
659 val ((pt,_),_) = get_calc cI |