diff -r ee68ccda7977 -r 56762e8a672e src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Mon Dec 12 18:08:13 2016 +0100 +++ b/src/Tools/isac/Interpret/solve.sml Wed Dec 14 09:37:01 2016 +0100 @@ -135,7 +135,7 @@ fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*) - (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)):taci; + (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Ctree.taci; (*FIXME.WN050821 compare solve ... nxt_solv*) @@ -154,7 +154,7 @@ case ini of SOME t => let val (pos,c,_,pt) = - generate1 thy (Apply_Method' (mI, SOME t, is, ctxt)) + Ctree.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt)) (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt; in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate') @@ -168,7 +168,7 @@ Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) => ("ok", (map step2taci ss, c', (pt',p'))) | NotLocatable => - let val (p,ps,f,pt) = generate_hard (assoc_thy "Isac") m (p,Frm) pt; + let val (p,ps,f,pt) = Ctree.generate_hard (assoc_thy "Isac") m (p,Frm) pt; in ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end @@ -203,7 +203,7 @@ let val is = ScrState (E,l,a,scval,scsaf,b) val tac_ = Check_Postcond' (pI, (scval, asm)) - val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt; + val (pos,ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt; in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end else let (*resume script of parpbl, transfer value of subpbl-script*) @@ -215,7 +215,7 @@ val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); val ctxt'' = from_subpbl_to_caller ctxt scval ctxt' val ((p,p_),ps,f,pt) = - generate1 thy (Check_Postcond' (pI, (scval, asm))) + Ctree.generate1 thy (Check_Postcond' (pI, (scval, asm))) (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt; in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)), ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_)))) @@ -246,7 +246,7 @@ let val ctxt = get_ctxt pt po val ((p,p_),ps,f,pt) = - generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) + Ctree.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt; in ("no-method-specified", (*Free_Solve*) ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_)))) @@ -264,7 +264,7 @@ in ("ok", (map step2taci ss, c', (pt',p'))) end | NotLocatable => let val (p,ps,f,pt) = - generate_hard (assoc_thy "Isac") m (p,p_) pt; + Ctree.generate_hard (assoc_thy "Isac") m (p,p_) pt; in ("not-found-in-script", ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p))) end @@ -288,7 +288,7 @@ val pos = ((lev_on o lev_dn) p, Frm) val tac_ = Apply_Method' (mI, SOME t, is, ctxt); val (pos,c,_,pt) = (*implicit Take*) - generate1 thy tac_ (is, ctxt) pos pt + Ctree.generate1 thy tac_ (is, ctxt) pos pt in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end | NONE => let @@ -323,7 +323,7 @@ val is = ScrState (E,l,a,scval,scsaf,b) val tac_ = Check_Postcond'(pI,(scval, asm)) val ((p,p_),ps,f,pt) = - generate1 thy tac_ (is, ctxt) (pp,Res) pt; + Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt; in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end else let (*resume script of parpbl, transfer value of subpbl-script*) @@ -336,7 +336,7 @@ val ctxt'' = from_subpbl_to_caller ctxt scval ctxt' val tac_ = Check_Postcond' (pI, (scval, asm)) val is = ScrState (E,l,a,scval,scsaf,b) - val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt; + val ((p,p_),ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt'') (pp, Res) pt; in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end end @@ -349,7 +349,7 @@ (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*) | (p, Res) => (lev_on p,Res) (*somewhere in script*) | _ => pos - val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt; + val (pos',c,_,pt) = Ctree.generate1 (assoc_thy "Isac") tac_ is pos pt; in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end (* find the next tac from the script, nxt_solv will update the ptree *) @@ -448,13 +448,13 @@ in ("detailrls", pt''', (p @ [length newnds], Res):pos') end | _ => let - val is = init_istate tac t + val is = Ctree.init_istate tac t (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] is wrong for simpl, but working ?!? *) val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt) val pos' = ((lev_on o lev_dn) p, Frm) val thy = assoc_thy "Isac" - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt + val (_,_,_,pt') = (*implicit Take*)Ctree.generate1 thy tac_ (is, ctxt) pos' pt val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos') val newnds = children (get_nd pt'' p) val pt''' = ins_chn newnds pt p @@ -469,7 +469,7 @@ *) fun get_form ((mI,m):tac'_) ((p,p_):pos') pt = case applicable_in (p,p_) pt m of - Chead.Notappl e => Error' (Error_ e) + Chead.Notappl e => Ctree.Error' (Ctree.Error_ e) | Chead.Appl m => (* val Appl m=applicable_in (p,p_) pt m; *) @@ -477,5 +477,5 @@ then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt in f end else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_)) - in (*f*) EmptyMout end; + in (*f*) Ctree.EmptyMout end;