1.1 --- a/src/Tools/isac/Frontend/interface.sml Mon Dec 19 09:02:41 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Dec 19 10:37:44 2016 +0100
1.3 @@ -343,7 +343,7 @@
1.4 let
1.5 val ctxt = get_ctxt pt pold
1.6 val (p, c, _, pt) =
1.7 - Ctree.generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
1.8 + Generate.generate1 (assoc_thy "Isac") m (Uistate, ctxt) ip pt
1.9 in upd_calc cI ((pt, p), []);
1.10 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
1.11 end)
1.12 @@ -672,7 +672,7 @@
1.13 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
1.14 (_, fillform, thm, sube_opt) :: _ =>
1.15 let
1.16 - val (pt, pos') = Ctree.generate_inconsistent_rew (sube_opt, thm''_of_thm thm)
1.17 + val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, thm''_of_thm thm)
1.18 fillform (get_loc pt pos) pos pt
1.19 in
1.20 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
2.1 --- a/src/Tools/isac/Interpret/appl.sml Mon Dec 19 09:02:41 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Dec 19 10:37:44 2016 +0100
2.3 @@ -225,7 +225,7 @@
2.4 let
2.5 val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
2.6 val {ppc,...} = Specify.get_pbt pI'
2.7 - val pbl = Ctree.init_pbl ppc
2.8 + val pbl = Generate.init_pbl ppc
2.9 in Chead.Appl (Model_Problem' (pI', pbl, [])) end
2.10
2.11 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
2.12 @@ -316,7 +316,7 @@
2.13 val thy = assoc_thy (if dI' = e_domID then dI else dI');
2.14 val {ppc,where_,prls,...} = Specify.get_pbt pID;
2.15 val pbl = if pI'=e_pblID andalso pI=e_pblID
2.16 - then (false, (Ctree.init_pbl ppc, []))
2.17 + then (false, (Generate.init_pbl ppc, []))
2.18 else Specify.match_itms_oris thy itms (ppc,where_,prls) oris;
2.19 in Chead.Appl (Specify_Problem' (pID, pbl)) end
2.20 (* val Specify_Method mID = nxt; val (p,p_) = p;
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Dec 19 09:02:41 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Dec 19 10:37:44 2016 +0100
3.3 @@ -10,7 +10,7 @@
3.4 datatype appl = Appl of tac_ | Notappl of string
3.5 val nxt_specify_init_calc : fmz -> calcstate
3.6 val specify : tac_ -> pos' -> cid -> ptree ->
3.7 - (posel list * pos_) * ((posel list * pos_) * istate) * Ctree.mout * tac * safe * ptree
3.8 + (posel list * pos_) * ((posel list * pos_) * istate) * Generate.mout * tac * safe * ptree
3.9 val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
3.10 val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
3.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
3.12 @@ -69,9 +69,9 @@
3.13 *)
3.14 type calcstate =
3.15 (ptree * pos') * (* the calc-state to which the tacis could be applied *)
3.16 - (Ctree.taci list) (* ev. several (hidden) steps;
3.17 + (Generate.taci list) (* ev. several (hidden) steps;
3.18 in REVERSE order: first tac_ to apply is last_elem *)
3.19 -val e_calcstate = ((EmptyPtree, e_pos'), [Ctree.e_taci]) : calcstate;
3.20 +val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate;
3.21
3.22 (*the state used during one calculation within the mathengine; it contains
3.23 a list of [tac,istate](="tacis") which generated the the calc-state;
3.24 @@ -83,14 +83,14 @@
3.25 because the tacis hold enought information for efficiently rebuilding
3.26 this state just by "fun generate ".*)
3.27 type calcstate' =
3.28 - Ctree.taci list * (* cas. several (hidden) steps;
3.29 + Generate.taci list * (* cas. several (hidden) steps;
3.30 in REVERSE order: first tac_ to apply is last_elem *)
3.31 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
3.32 (ptree * pos') (* the calc-state resulting from the application of tacis *)
3.33 -val e_calcstate' = ([Ctree.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
3.34 +val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
3.35
3.36 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
3.37 -fun f_mout thy (Ctree.FormKF f) = (Thm.term_of o the o (parse thy)) f
3.38 +fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f
3.39 | f_mout _ _ = error "f_mout: not called with formula";
3.40
3.41 (* is the calchead complete ? *)
3.42 @@ -606,8 +606,8 @@
3.43
3.44 (* output the headline to a ppc *)
3.45 fun header p_ pI mI =
3.46 - case p_ of Pbl => Ctree.Problem (if pI = e_pblID then [] else pI)
3.47 - | Met => Ctree.Method mI
3.48 + case p_ of Pbl => Generate.Problem (if pI = e_pblID then [] else pI)
3.49 + | Met => Generate.Method mI
3.50 | pos => error ("header called with "^ pos_2str pos)
3.51
3.52 fun specify_additem sel (ct, _) (p, Met) _ pt =
3.53 @@ -630,7 +630,7 @@
3.54 | "#Find" => Add_Find' (ct, met')
3.55 | "#Relate"=> Add_Relation'(ct, met')
3.56 | str => error ("specify_additem: uncovered case with " ^ str)
3.57 - val (p, Met, pt') = case Ctree.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
3.58 + val (p, Met, pt') = case Generate.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
3.59 ((p, Met), _, _, pt') => (p, Met, pt')
3.60 | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
3.61 val pre' = check_preconds thy prls pre met'
3.62 @@ -639,7 +639,7 @@
3.63 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
3.64 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
3.65 in ((p, p_), ((p, p_), Uistate),
3.66 - Ctree.PpcKF (Ctree.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
3.67 + Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
3.68 end
3.69 | Err msg =>
3.70 let
3.71 @@ -648,7 +648,7 @@
3.72 val (p_, nxt) =
3.73 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
3.74 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
3.75 - in ((p,p_), ((p,p_),Uistate), Ctree.Error' msg, nxt, Safe,pt) end
3.76 + in ((p,p_), ((p,p_),Uistate), Generate.Error' msg, nxt, Safe,pt) end
3.77 end
3.78 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
3.79 let
3.80 @@ -670,7 +670,7 @@
3.81 | "#Find" => Add_Find' (ct, pbl')
3.82 | "#Relate"=> Add_Relation'(ct, pbl')
3.83 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
3.84 - val ((p, Pbl), _, _, pt') = Ctree.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
3.85 + val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
3.86 val pre = check_preconds thy prls where_ pbl'
3.87 val pb = foldl and_ (true, map fst pre)
3.88 val (p_, nxt) =
3.89 @@ -678,7 +678,7 @@
3.90 val ppc = if p_= Pbl then pbl' else met
3.91 in
3.92 ((p, p_), ((p, p_), Uistate),
3.93 - Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
3.94 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
3.95 end
3.96 | Err msg =>
3.97 let
3.98 @@ -687,7 +687,7 @@
3.99 val (p_, nxt) =
3.100 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
3.101 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
3.102 - in ((p, p_), ((p, p_), Uistate), Ctree.Error' msg, nxt, Safe,pt) end
3.103 + in ((p, p_), ((p, p_), Uistate), Generate.Error' msg, nxt, Safe,pt) end
3.104 end
3.105
3.106 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
3.107 @@ -705,11 +705,11 @@
3.108 case mI' of
3.109 ["no_met"] =>
3.110 (([], Pbl), (([], Pbl), Uistate),
3.111 - Ctree.PpcKF (Ctree.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.112 + Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.113 Refine_Tacitly pI', Safe, pt)
3.114 | _ =>
3.115 (([], Pbl), (([], Pbl), Uistate),
3.116 - Ctree.PpcKF (Ctree.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.117 + Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.118 Model_Problem, Safe, pt)
3.119 end
3.120 (* ONLY for STARTING modeling phase *)
3.121 @@ -725,12 +725,12 @@
3.122 val pre = check_preconds thy prls where_ pbl
3.123 val pb = foldl and_ (true, map fst pre)
3.124 val ((p, _), _, _, pt) =
3.125 - Ctree.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
3.126 + Generate.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
3.127 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
3.128 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
3.129 in
3.130 ((p, Pbl), ((p, p_), Uistate),
3.131 - Ctree.PpcKF (Ctree.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.132 + Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.133 nxt, Safe, pt)
3.134 end
3.135 (* called only if no_met is specified *)
3.136 @@ -742,19 +742,19 @@
3.137 val {met, thy,...} = Specify.get_pbt pIre
3.138 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
3.139 val ((p,_), _, _, pt) =
3.140 - Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
3.141 + Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
3.142 val (pbl, pre, _) = ([], [], false)
3.143 in ((p, Pbl), (pos, Uistate),
3.144 - Ctree.PpcKF (Ctree.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.145 + Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
3.146 Model_Problem, Safe, pt)
3.147 end
3.148 | specify (Refine_Problem' rfd) pos _ pt =
3.149 let
3.150 val ctxt = get_ctxt pt pos
3.151 val (pos, _, _, pt) =
3.152 - Ctree.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.153 + Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.154 in
3.155 - (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.RefinedKF rfd, Model_Problem, Safe, pt)
3.156 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Generate.RefinedKF rfd, Model_Problem, Safe, pt)
3.157 end
3.158 (*WN110515 initialise ctxt again from itms and add preconds*)
3.159 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
3.160 @@ -765,7 +765,7 @@
3.161 | _ => error "specify (Specify_Problem': uncovered case get_obj"
3.162 val thy = assoc_thy dI
3.163 val (p, Pbl, pt) =
3.164 - case Ctree.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
3.165 + case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
3.166 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
3.167 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
3.168 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
3.169 @@ -774,7 +774,7 @@
3.170 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
3.171 in
3.172 ((p,Pbl), (pos,Uistate),
3.173 - Ctree.PpcKF (Ctree.Problem pI, Specify.itms2itemppc dI'' itms pre),
3.174 + Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
3.175 nxt, Safe, pt)
3.176 end
3.177 (*WN110515 initialise ctxt again from itms and add preconds*)
3.178 @@ -792,12 +792,12 @@
3.179 val met = if met = [] then pbl else met
3.180 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
3.181 val (pos, _, _, pt) =
3.182 - Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.183 + Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.184 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
3.185 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
3.186 in
3.187 (pos, (pos,Uistate),
3.188 - Ctree.PpcKF (Ctree.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
3.189 + Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
3.190 nxt, Safe, pt)
3.191 end
3.192 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
3.193 @@ -826,16 +826,16 @@
3.194 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
3.195 in
3.196 ((p, p_), (pos, Uistate),
3.197 - Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
3.198 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
3.199 nxt, Safe, pt)
3.200 end
3.201 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
3.202 let
3.203 - val ((p, p_), _, _, pt) = Ctree.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
3.204 + val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
3.205 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
3.206 in
3.207 ((p,p_), (pos,Uistate),
3.208 - Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
3.209 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
3.210 nxt, Safe, pt)
3.211 end
3.212 end
3.213 @@ -861,7 +861,7 @@
3.214 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
3.215 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
3.216 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
3.217 - val (p, Pbl, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
3.218 + val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
3.219 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
3.220 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
3.221 in
3.222 @@ -890,7 +890,7 @@
3.223 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
3.224 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
3.225 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
3.226 - val (p, Met, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
3.227 + val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
3.228 ((p, Met), c, _, pt') => (p, Met, c, pt')
3.229 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
3.230 in
3.231 @@ -965,7 +965,7 @@
3.232 val thy = assoc_thy dI
3.233 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
3.234 val {cas, ppc, ...} = Specify.get_pbt pI
3.235 - val pbl = Ctree.init_pbl ppc (* fill in descriptions *)
3.236 + val pbl = Generate.init_pbl ppc (* fill in descriptions *)
3.237 (*----------------if you think, this should be done by the Dialog
3.238 in the java front-end, search there for WN060225-modelProblem----*)
3.239 val (pbl, met) = case cas of
3.240 @@ -973,7 +973,7 @@
3.241 | _ => complete_mod_ (oris, mpc, ppc, probl)
3.242 (*----------------------------------------------------------------*)
3.243 val tac_ = Model_Problem' (pI, pbl, met)
3.244 - val (pos,c,_,pt) = Ctree.generate1 thy tac_ (Uistate, ctxt) pos pt
3.245 + val (pos,c,_,pt) = Generate.generate1 thy tac_ (Uistate, ctxt) pos pt
3.246 in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
3.247 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
3.248 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
3.249 @@ -994,7 +994,7 @@
3.250 val mI = if length met = 0 then e_metID else hd met
3.251 val thy = assoc_thy dI
3.252 val (pos, c, _, pt) =
3.253 - Ctree.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
3.254 + Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
3.255 in
3.256 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
3.257 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
3.258 @@ -1013,7 +1013,7 @@
3.259 NONE => ([], [], ptp)
3.260 | SOME rfd =>
3.261 let
3.262 - val (pos,c,_,pt) = Ctree.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.263 + val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
3.264 in
3.265 ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
3.266 end
3.267 @@ -1028,10 +1028,10 @@
3.268 val {ppc,where_,prls,...} = Specify.get_pbt pI
3.269 val pbl =
3.270 if pI' = e_pblID andalso pI = e_pblID
3.271 - then (false, (Ctree.init_pbl ppc, []))
3.272 + then (false, (Generate.init_pbl ppc, []))
3.273 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
3.274 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
3.275 - val (c, pt) = case Ctree.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
3.276 + val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
3.277 ((_, Pbl), c, _, pt) => (c, pt)
3.278 | _ => error ""
3.279 in
3.280 @@ -1051,7 +1051,7 @@
3.281 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
3.282 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
3.283 val (pos, c, _, pt) =
3.284 - Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.285 + Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
3.286 in
3.287 ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
3.288 end
3.289 @@ -1059,7 +1059,7 @@
3.290 let
3.291 val ctxt = get_ctxt pt pos
3.292 val (pos, c, _, pt) =
3.293 - Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.294 + Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.295 in (*FIXXXME: check if pbl can still be parsed*)
3.296 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
3.297 (pt, pos))
3.298 @@ -1067,7 +1067,7 @@
3.299 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
3.300 let
3.301 val ctxt = get_ctxt pt pos
3.302 - val (pos, c, _, pt) = Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.303 + val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
3.304 in (*FIXXXME: check if met can still be parsed*)
3.305 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
3.306 end
3.307 @@ -1090,7 +1090,7 @@
3.308 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
3.309 ([], (dI,pI,mI), hdl)
3.310 val pt = update_spec pt [] (dI, pI, mI)
3.311 - val pits = Ctree.init_pbl' ppc
3.312 + val pits = Generate.init_pbl' ppc
3.313 val pt = update_pbl pt [] pits
3.314 in ((pt, ([] , Pbl)), []) : calcstate end
3.315 else
3.316 @@ -1102,7 +1102,7 @@
3.317 val (pt, _) =
3.318 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
3.319 val pt = update_spec pt [] (dI, pI, mI)
3.320 - val mits = Ctree.init_pbl' ppc
3.321 + val mits = Generate.init_pbl' ppc
3.322 val pt = update_met pt [] mits
3.323 in ((pt, ([], Met)), []) end
3.324 else (* new example, pepare for interactive modeling *)
4.1 --- a/src/Tools/isac/Interpret/generate.sml Mon Dec 19 09:02:41 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Mon Dec 19 10:37:44 2016 +0100
4.3 @@ -1,7 +1,7 @@
4.4 (* use"ME/generate.sml";
4.5 use"generate.sml";
4.6 *)
4.7 -signature CALC_TREE =
4.8 +signature GENERATE_CALC_TREE =
4.9 sig (*vvv request into signature is incremental with *.sml *)
4.10 (* for calchead.sml -------------------------------------------------------------- vvv *)
4.11 type taci
4.12 @@ -30,7 +30,7 @@
4.13 end
4.14
4.15 (**)
4.16 -structure Ctree(**): CALC_TREE(**) =
4.17 +structure Generate(**): GENERATE_CALC_TREE(**) =
4.18 (**)
4.19 struct
4.20 (* initialize istate for Detail_Set *)
5.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Dec 19 09:02:41 2016 +0100
5.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Dec 19 10:37:44 2016 +0100
5.3 @@ -19,7 +19,7 @@
5.4 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
5.5 val cas_input : term -> (ptree * ocalhd) option
5.6 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
5.7 - val compare_step : Ctree.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
5.8 + val compare_step : Generate.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
5.9 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
5.10 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
5.11 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
5.12 @@ -389,7 +389,7 @@
5.13 then
5.14 let
5.15 val tacis' = map (mk_tacis rew_ord erls) der;
5.16 - val (c', ptp) = Ctree.embed_deriv tacis' ptp;
5.17 + val (c', ptp) = Generate.embed_deriv tacis' ptp;
5.18 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
5.19 else
5.20 if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
6.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Dec 19 09:02:41 2016 +0100
6.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Dec 19 10:37:44 2016 +0100
6.3 @@ -9,11 +9,11 @@
6.4 signature MATH_ENGINE =
6.5 sig
6.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
6.7 - val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree
6.8 + val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * tac'_ * safe * ptree
6.9 val autocalc :
6.10 - pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')
6.11 + pos' list -> pos' -> (ptree * pos') * Generate.taci list -> auto -> string * pos' list * (ptree * pos')
6.12 val locatetac :
6.13 - tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))
6.14 + tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos'))
6.15 val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
6.16 val detailstep :
6.17 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
6.18 @@ -30,8 +30,8 @@
6.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.20 type nxt_
6.21 type lOc_
6.22 - val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree
6.23 - val f2str : Ctree.mout -> cterm'
6.24 + val CalcTreeTEST : fmz list -> pos' * NEW * Generate.mout * (string * tac) * safe * ptree
6.25 + val f2str : Generate.mout -> cterm'
6.26 val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
6.27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.28 end
6.29 @@ -62,7 +62,7 @@
6.30 let
6.31 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
6.32 in
6.33 - case f of (Ctree.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
6.34 + case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
6.35 end
6.36
6.37 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
6.38 @@ -195,7 +195,7 @@
6.39 (_::_) =>
6.40 if ip = p (*the request is done where ptp waits for*)
6.41 then
6.42 - let val (pt',c',p') = Ctree.generate tacis (pt,[],p)
6.43 + let val (pt',c',p') = Generate.generate tacis (pt,[],p)
6.44 in ("ok", (tacis, c', (pt', p'))) end
6.45 else (case (if member op = [Pbl, Met] p_
6.46 then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
6.47 @@ -368,10 +368,10 @@
6.48 val (form, _, _) = Chead.pt_extract ptp
6.49 in
6.50 case form of
6.51 - Form t => Ctree.FormKF (term2str t)
6.52 + Form t => Generate.FormKF (term2str t)
6.53 | ModSpec (_, p_, _, gfr, pre, _) =>
6.54 - Ctree.PpcKF (
6.55 - (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method []
6.56 + Generate.PpcKF (
6.57 + (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method []
6.58 | _ => error "TESTg_form: uncovered case",
6.59 Specify.itms2itemppc (assoc_thy"Isac") gfr pre))
6.60 end
6.61 @@ -422,6 +422,6 @@
6.62 end
6.63
6.64 (* for quick test-print-out, until 'type inout' is removed *)
6.65 -fun f2str (Ctree.FormKF cterm') = cterm';
6.66 +fun f2str (Generate.FormKF cterm') = cterm';
6.67
6.68 end
7.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 19 09:02:41 2016 +0100
7.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Dec 19 10:37:44 2016 +0100
7.3 @@ -8,7 +8,7 @@
7.4 signature LUCAS_INTERPRETER =
7.5 sig
7.6
7.7 - type step = tac_ * Ctree.mout * ptree * pos' * pos' list
7.8 + type step = tac_ * Generate.mout * ptree * pos' * pos' list
7.9 datatype locate = NotLocatable | Steps of istate * step list
7.10
7.11 val next_tac : (*diss: next-tactic-function*)
7.12 @@ -61,7 +61,7 @@
7.13 Assoc (scrstate, steps) => ... ass* scrstate steps *)
7.14 type step =
7.15 tac_ (*transformed from associated tac *)
7.16 - * Ctree.mout (*result with indentation etc. *)
7.17 + * Generate.mout (*result with indentation etc. *)
7.18 * ptree (*containing node created by tac_ + resp. scrstate *)
7.19 * pos' (*position in ptree; ptree * pos' is the proofstate *)
7.20 * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
7.21 @@ -80,7 +80,7 @@
7.22 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
7.23 val is = RrlsState (f', f'', rss, rts)
7.24 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
7.25 - val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
7.26 + val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt
7.27 in (is, (m, mout, pt', p', cid) :: steps) end
7.28 | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
7.29 let
7.30 @@ -89,7 +89,7 @@
7.31 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
7.32 val is = RrlsState (f', f'', rss, rts)
7.33 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
7.34 - val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
7.35 + val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt
7.36 in rts2steps ((m, mout, pt', p', cid)::steps)
7.37 ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
7.38 end
7.39 @@ -665,11 +665,11 @@
7.40 case assod pt d m stac of
7.41 Ass (m,v') =>
7.42 let val (p'',c',f',pt') =
7.43 - Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
7.44 + Generate.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
7.45 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
7.46 | AssWeak (m,v') =>
7.47 let val (p'',c',f',pt') =
7.48 - Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
7.49 + Generate.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
7.50 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
7.51 | NotAss =>
7.52 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
7.53 @@ -680,7 +680,7 @@
7.54 let
7.55 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
7.56 val (p'',c',f',pt') =
7.57 - Ctree.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt;
7.58 + Generate.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt;
7.59 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
7.60 | Chead.Notappl _ => (NasNap (v, E))
7.61 )
7.62 @@ -822,8 +822,8 @@
7.63 let val thy = assoc_thy thy';
7.64 in case if l = [] orelse (
7.65 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
7.66 - then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) body)
7.67 - else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) ) of
7.68 + then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) body)
7.69 + else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) ) of
7.70 Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>
7.71 (if strong_ass
7.72 then (Steps (ScrState is, ss))
7.73 @@ -833,7 +833,7 @@
7.74 let
7.75 val (po,p_) = p
7.76 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
7.77 - val (p'',c'',f'',pt'') = Ctree.generate1 thy m (ScrState is, ctxt) (po',p_) pt
7.78 + val (p'',c'',f'',pt'') = Generate.generate1 thy m (ScrState is, ctxt) (po',p_) pt
7.79 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
7.80 else Steps (ScrState is, ss))
7.81
8.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Dec 19 09:02:41 2016 +0100
8.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Dec 19 10:37:44 2016 +0100
8.3 @@ -135,7 +135,7 @@
8.4
8.5
8.6 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
8.7 - (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Ctree.taci;
8.8 + (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Generate.taci;
8.9
8.10
8.11 (*FIXME.WN050821 compare solve ... nxt_solv*)
8.12 @@ -154,7 +154,7 @@
8.13 case ini of
8.14 SOME t =>
8.15 let val (pos,c,_,pt) =
8.16 - Ctree.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
8.17 + Generate.generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
8.18 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
8.19 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
8.20 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate')
8.21 @@ -168,7 +168,7 @@
8.22 Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) =>
8.23 ("ok", (map step2taci ss, c', (pt',p')))
8.24 | NotLocatable =>
8.25 - let val (p,ps,f,pt) = Ctree.generate_hard (assoc_thy "Isac") m (p,Frm) pt;
8.26 + let val (p,ps,f,pt) = Generate.generate_hard (assoc_thy "Isac") m (p,Frm) pt;
8.27 in
8.28 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p)))
8.29 end
8.30 @@ -203,7 +203,7 @@
8.31 let
8.32 val is = ScrState (E,l,a,scval,scsaf,b)
8.33 val tac_ = Check_Postcond' (pI, (scval, asm))
8.34 - val (pos,ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
8.35 + val (pos,ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
8.36 in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
8.37 else
8.38 let (*resume script of parpbl, transfer value of subpbl-script*)
8.39 @@ -215,7 +215,7 @@
8.40 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
8.41 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
8.42 val ((p,p_),ps,f,pt) =
8.43 - Ctree.generate1 thy (Check_Postcond' (pI, (scval, asm)))
8.44 + Generate.generate1 thy (Check_Postcond' (pI, (scval, asm)))
8.45 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
8.46 in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)),
8.47 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
8.48 @@ -246,7 +246,7 @@
8.49 let
8.50 val ctxt = get_ctxt pt po
8.51 val ((p,p_),ps,f,pt) =
8.52 - Ctree.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
8.53 + Generate.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
8.54 m (e_istate, ctxt) (p,p_) pt;
8.55 in ("no-method-specified", (*Free_Solve*)
8.56 ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_))))
8.57 @@ -264,7 +264,7 @@
8.58 in ("ok", (map step2taci ss, c', (pt',p'))) end
8.59 | NotLocatable =>
8.60 let val (p,ps,f,pt) =
8.61 - Ctree.generate_hard (assoc_thy "Isac") m (p,p_) pt;
8.62 + Generate.generate_hard (assoc_thy "Isac") m (p,p_) pt;
8.63 in ("not-found-in-script",
8.64 ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p)))
8.65 end
8.66 @@ -288,7 +288,7 @@
8.67 val pos = ((lev_on o lev_dn) p, Frm)
8.68 val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
8.69 val (pos,c,_,pt) = (*implicit Take*)
8.70 - Ctree.generate1 thy tac_ (is, ctxt) pos pt
8.71 + Generate.generate1 thy tac_ (is, ctxt) pos pt
8.72 in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end
8.73 | NONE =>
8.74 let
8.75 @@ -323,7 +323,7 @@
8.76 val is = ScrState (E,l,a,scval,scsaf,b)
8.77 val tac_ = Check_Postcond'(pI,(scval, asm))
8.78 val ((p,p_),ps,f,pt) =
8.79 - Ctree.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
8.80 + Generate.generate1 thy tac_ (is, ctxt) (pp,Res) pt;
8.81 in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
8.82 else
8.83 let (*resume script of parpbl, transfer value of subpbl-script*)
8.84 @@ -336,7 +336,7 @@
8.85 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
8.86 val tac_ = Check_Postcond' (pI, (scval, asm))
8.87 val is = ScrState (E,l,a,scval,scsaf,b)
8.88 - val ((p,p_),ps,f,pt) = Ctree.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
8.89 + val ((p,p_),ps,f,pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
8.90 in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
8.91 end
8.92
8.93 @@ -349,7 +349,7 @@
8.94 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
8.95 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
8.96 | _ => pos
8.97 - val (pos',c,_,pt) = Ctree.generate1 (assoc_thy "Isac") tac_ is pos pt;
8.98 + val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
8.99 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
8.100
8.101 (* find the next tac from the script, nxt_solv will update the ptree *)
8.102 @@ -448,13 +448,13 @@
8.103 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
8.104 | _ =>
8.105 let
8.106 - val is = Ctree.init_istate tac t
8.107 + val is = Generate.init_istate tac t
8.108 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
8.109 is wrong for simpl, but working ?!? *)
8.110 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
8.111 val pos' = ((lev_on o lev_dn) p, Frm)
8.112 val thy = assoc_thy "Isac"
8.113 - val (_,_,_,pt') = (*implicit Take*)Ctree.generate1 thy tac_ (is, ctxt) pos' pt
8.114 + val (_,_,_,pt') = (*implicit Take*)Generate.generate1 thy tac_ (is, ctxt) pos' pt
8.115 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
8.116 val newnds = children (get_nd pt'' p)
8.117 val pt''' = ins_chn newnds pt p
8.118 @@ -469,7 +469,7 @@
8.119 *)
8.120 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
8.121 case applicable_in (p,p_) pt m of
8.122 - Chead.Notappl e => Ctree.Error' e
8.123 + Chead.Notappl e => Generate.Error' e
8.124 | Chead.Appl m =>
8.125 (* val Appl m=applicable_in (p,p_) pt m;
8.126 *)
8.127 @@ -477,5 +477,5 @@
8.128 then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt
8.129 in f end
8.130 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
8.131 - in (*f*) Ctree.EmptyMout end;
8.132 + in (*f*) Generate.EmptyMout end;
8.133