1.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Dec 19 09:02:41 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Dec 19 10:37:44 2016 +0100
1.3 @@ -135,7 +135,7 @@
1.4
1.5
1.6 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
1.7 - (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Ctree.taci;
1.8 + (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Generate.taci;
1.9
1.10
1.11 (*FIXME.WN050821 compare solve ... nxt_solv*)
1.12 @@ -154,7 +154,7 @@
1.13 case ini of
1.14 SOME t =>
1.15 let val (pos,c,_,pt) =
1.16 - Ctree.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
1.17 + Generate.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
1.18 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
1.19 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
1.20 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate')
1.21 @@ -168,7 +168,7 @@
1.22 Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.23 ("ok", (map step2taci ss, c', (pt',p')))
1.24 | NotLocatable =>
1.25 - let val (p,ps,f,pt) = Ctree.generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.26 + let val (p,ps,f,pt) = Generate.generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.27 in
1.28 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p)))
1.29 end
1.30 @@ -203,7 +203,7 @@
1.31 let
1.32 val is = ScrState (E,l,a,scval,scsaf,b)
1.33 val tac_ = Check_Postcond' (pI, (scval, asm))
1.34 - val (pos,ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.35 + val (pos,ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.36 in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
1.37 else
1.38 let (*resume script of parpbl, transfer value of subpbl-script*)
1.39 @@ -215,7 +215,7 @@
1.40 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
1.41 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
1.42 val ((p,p_),ps,f,pt) =
1.43 - Ctree.generate1 thy (Check_Postcond' (pI, (scval, asm)))
1.44 + Generate.generate1 thy (Check_Postcond' (pI, (scval, asm)))
1.45 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
1.46 in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)),
1.47 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
1.48 @@ -246,7 +246,7 @@
1.49 let
1.50 val ctxt = get_ctxt pt po
1.51 val ((p,p_),ps,f,pt) =
1.52 - Ctree.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.53 + Generate.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.54 m (e_istate, ctxt) (p,p_) pt;
1.55 in ("no-method-specified", (*Free_Solve*)
1.56 ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_))))
1.57 @@ -264,7 +264,7 @@
1.58 in ("ok", (map step2taci ss, c', (pt',p'))) end
1.59 | NotLocatable =>
1.60 let val (p,ps,f,pt) =
1.61 - Ctree.generate_hard (assoc_thy "Isac") m (p,p_) pt;
1.62 + Generate.generate_hard (assoc_thy "Isac") m (p,p_) pt;
1.63 in ("not-found-in-script",
1.64 ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p)))
1.65 end
1.66 @@ -288,7 +288,7 @@
1.67 val pos = ((lev_on o lev_dn) p, Frm)
1.68 val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
1.69 val (pos,c,_,pt) = (*implicit Take*)
1.70 - Ctree.generate1 thy tac_ (is, ctxt) pos pt
1.71 + Generate.generate1 thy tac_ (is, ctxt) pos pt
1.72 in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end
1.73 | NONE =>
1.74 let
1.75 @@ -323,7 +323,7 @@
1.76 val is = ScrState (E,l,a,scval,scsaf,b)
1.77 val tac_ = Check_Postcond'(pI,(scval, asm))
1.78 val ((p,p_),ps,f,pt) =
1.79 - Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.80 + Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.81 in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
1.82 else
1.83 let (*resume script of parpbl, transfer value of subpbl-script*)
1.84 @@ -336,7 +336,7 @@
1.85 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
1.86 val tac_ = Check_Postcond' (pI, (scval, asm))
1.87 val is = ScrState (E,l,a,scval,scsaf,b)
1.88 - val ((p,p_),ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
1.89 + val ((p,p_),ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
1.90 in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
1.91 end
1.92
1.93 @@ -349,7 +349,7 @@
1.94 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
1.95 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
1.96 | _ => pos
1.97 - val (pos',c,_,pt) = Ctree.generate1 (assoc_thy "Isac") tac_ is pos pt;
1.98 + val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
1.99 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
1.100
1.101 (* find the next tac from the script, nxt_solv will update the ptree *)
1.102 @@ -448,13 +448,13 @@
1.103 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
1.104 | _ =>
1.105 let
1.106 - val is = Ctree.init_istate tac t
1.107 + val is = Generate.init_istate tac t
1.108 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
1.109 is wrong for simpl, but working ?!? *)
1.110 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
1.111 val pos' = ((lev_on o lev_dn) p, Frm)
1.112 val thy = assoc_thy "Isac"
1.113 - val (_,_,_,pt') = (*implicit Take*)Ctree.generate1 thy tac_ (is, ctxt) pos' pt
1.114 + val (_,_,_,pt') = (*implicit Take*)Generate.generate1 thy tac_ (is, ctxt) pos' pt
1.115 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
1.116 val newnds = children (get_nd pt'' p)
1.117 val pt''' = ins_chn newnds pt p
1.118 @@ -469,7 +469,7 @@
1.119 *)
1.120 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
1.121 case applicable_in (p,p_) pt m of
1.122 - Chead.Notappl e => Ctree.Error' e
1.123 + Chead.Notappl e => Generate.Error' e
1.124 | Chead.Appl m =>
1.125 (* val Appl m=applicable_in (p,p_) pt m;
1.126 *)
1.127 @@ -477,5 +477,5 @@
1.128 then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt
1.129 in f end
1.130 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
1.131 - in (*f*) Ctree.EmptyMout end;
1.132 + in (*f*) Generate.EmptyMout end;
1.133