1.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Dec 19 09:02:41 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Dec 19 10:37:44 2016 +0100
1.3 @@ -10,7 +10,7 @@
1.4 datatype appl = Appl of tac_ | Notappl of string
1.5 val nxt_specify_init_calc : fmz -> calcstate
1.6 val specify : tac_ -> pos' -> cid -> ptree ->
1.7 - (posel list * pos_) * ((posel list * pos_) * istate) * Ctree.mout * tac * safe * ptree
1.8 + (posel list * pos_) * ((posel list * pos_) * istate) * Generate.mout * tac * safe * ptree
1.9 val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
1.10 val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
1.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
1.12 @@ -69,9 +69,9 @@
1.13 *)
1.14 type calcstate =
1.15 (ptree * pos') * (* the calc-state to which the tacis could be applied *)
1.16 - (Ctree.taci list) (* ev. several (hidden) steps;
1.17 + (Generate.taci list) (* ev. several (hidden) steps;
1.18 in REVERSE order: first tac_ to apply is last_elem *)
1.19 -val e_calcstate = ((EmptyPtree, e_pos'), [Ctree.e_taci]) : calcstate;
1.20 +val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate;
1.21
1.22 (*the state used during one calculation within the mathengine; it contains
1.23 a list of [tac,istate](="tacis") which generated the the calc-state;
1.24 @@ -83,14 +83,14 @@
1.25 because the tacis hold enought information for efficiently rebuilding
1.26 this state just by "fun generate ".*)
1.27 type calcstate' =
1.28 - Ctree.taci list * (* cas. several (hidden) steps;
1.29 + Generate.taci list * (* cas. several (hidden) steps;
1.30 in REVERSE order: first tac_ to apply is last_elem *)
1.31 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
1.32 (ptree * pos') (* the calc-state resulting from the application of tacis *)
1.33 -val e_calcstate' = ([Ctree.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.34 +val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.35
1.36 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
1.37 -fun f_mout thy (Ctree.FormKF f) = (Thm.term_of o the o (parse thy)) f
1.38 +fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f
1.39 | f_mout _ _ = error "f_mout: not called with formula";
1.40
1.41 (* is the calchead complete ? *)
1.42 @@ -606,8 +606,8 @@
1.43
1.44 (* output the headline to a ppc *)
1.45 fun header p_ pI mI =
1.46 - case p_ of Pbl => Ctree.Problem (if pI = e_pblID then [] else pI)
1.47 - | Met => Ctree.Method mI
1.48 + case p_ of Pbl => Generate.Problem (if pI = e_pblID then [] else pI)
1.49 + | Met => Generate.Method mI
1.50 | pos => error ("header called with "^ pos_2str pos)
1.51
1.52 fun specify_additem sel (ct, _) (p, Met) _ pt =
1.53 @@ -630,7 +630,7 @@
1.54 | "#Find" => Add_Find' (ct, met')
1.55 | "#Relate"=> Add_Relation'(ct, met')
1.56 | str => error ("specify_additem: uncovered case with " ^ str)
1.57 - val (p, Met, pt') = case Ctree.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
1.58 + val (p, Met, pt') = case Generate.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
1.59 ((p, Met), _, _, pt') => (p, Met, pt')
1.60 | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
1.61 val pre' = check_preconds thy prls pre met'
1.62 @@ -639,7 +639,7 @@
1.63 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.64 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
1.65 in ((p, p_), ((p, p_), Uistate),
1.66 - Ctree.PpcKF (Ctree.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
1.67 + Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
1.68 end
1.69 | Err msg =>
1.70 let
1.71 @@ -648,7 +648,7 @@
1.72 val (p_, nxt) =
1.73 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.74 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
1.75 - in ((p,p_), ((p,p_),Uistate), Ctree.Error' msg, nxt, Safe,pt) end
1.76 + in ((p,p_), ((p,p_),Uistate), Generate.Error' msg, nxt, Safe,pt) end
1.77 end
1.78 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
1.79 let
1.80 @@ -670,7 +670,7 @@
1.81 | "#Find" => Add_Find' (ct, pbl')
1.82 | "#Relate"=> Add_Relation'(ct, pbl')
1.83 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
1.84 - val ((p, Pbl), _, _, pt') = Ctree.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.85 + val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.86 val pre = check_preconds thy prls where_ pbl'
1.87 val pb = foldl and_ (true, map fst pre)
1.88 val (p_, nxt) =
1.89 @@ -678,7 +678,7 @@
1.90 val ppc = if p_= Pbl then pbl' else met
1.91 in
1.92 ((p, p_), ((p, p_), Uistate),
1.93 - Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
1.94 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
1.95 end
1.96 | Err msg =>
1.97 let
1.98 @@ -687,7 +687,7 @@
1.99 val (p_, nxt) =
1.100 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.101 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.102 - in ((p, p_), ((p, p_), Uistate), Ctree.Error' msg, nxt, Safe,pt) end
1.103 + in ((p, p_), ((p, p_), Uistate), Generate.Error' msg, nxt, Safe,pt) end
1.104 end
1.105
1.106 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
1.107 @@ -705,11 +705,11 @@
1.108 case mI' of
1.109 ["no_met"] =>
1.110 (([], Pbl), (([], Pbl), Uistate),
1.111 - Ctree.PpcKF (Ctree.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.112 + Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.113 Refine_Tacitly pI', Safe, pt)
1.114 | _ =>
1.115 (([], Pbl), (([], Pbl), Uistate),
1.116 - Ctree.PpcKF (Ctree.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.117 + Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.118 Model_Problem, Safe, pt)
1.119 end
1.120 (* ONLY for STARTING modeling phase *)
1.121 @@ -725,12 +725,12 @@
1.122 val pre = check_preconds thy prls where_ pbl
1.123 val pb = foldl and_ (true, map fst pre)
1.124 val ((p, _), _, _, pt) =
1.125 - Ctree.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.126 + Generate.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.127 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.128 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
1.129 in
1.130 ((p, Pbl), ((p, p_), Uistate),
1.131 - Ctree.PpcKF (Ctree.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.132 + Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.133 nxt, Safe, pt)
1.134 end
1.135 (* called only if no_met is specified *)
1.136 @@ -742,19 +742,19 @@
1.137 val {met, thy,...} = Specify.get_pbt pIre
1.138 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.139 val ((p,_), _, _, pt) =
1.140 - Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.141 + Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.142 val (pbl, pre, _) = ([], [], false)
1.143 in ((p, Pbl), (pos, Uistate),
1.144 - Ctree.PpcKF (Ctree.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.145 + Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.146 Model_Problem, Safe, pt)
1.147 end
1.148 | specify (Refine_Problem' rfd) pos _ pt =
1.149 let
1.150 val ctxt = get_ctxt pt pos
1.151 val (pos, _, _, pt) =
1.152 - Ctree.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.153 + Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.154 in
1.155 - (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.RefinedKF rfd, Model_Problem, Safe, pt)
1.156 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Generate.RefinedKF rfd, Model_Problem, Safe, pt)
1.157 end
1.158 (*WN110515 initialise ctxt again from itms and add preconds*)
1.159 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
1.160 @@ -765,7 +765,7 @@
1.161 | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.162 val thy = assoc_thy dI
1.163 val (p, Pbl, pt) =
1.164 - case Ctree.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
1.165 + case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
1.166 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
1.167 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.168 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
1.169 @@ -774,7 +774,7 @@
1.170 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
1.171 in
1.172 ((p,Pbl), (pos,Uistate),
1.173 - Ctree.PpcKF (Ctree.Problem pI, Specify.itms2itemppc dI'' itms pre),
1.174 + Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
1.175 nxt, Safe, pt)
1.176 end
1.177 (*WN110515 initialise ctxt again from itms and add preconds*)
1.178 @@ -792,12 +792,12 @@
1.179 val met = if met = [] then pbl else met
1.180 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
1.181 val (pos, _, _, pt) =
1.182 - Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.183 + Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.184 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
1.185 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
1.186 in
1.187 (pos, (pos,Uistate),
1.188 - Ctree.PpcKF (Ctree.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
1.189 + Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
1.190 nxt, Safe, pt)
1.191 end
1.192 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.193 @@ -826,16 +826,16 @@
1.194 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.195 in
1.196 ((p, p_), (pos, Uistate),
1.197 - Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.198 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.199 nxt, Safe, pt)
1.200 end
1.201 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.202 let
1.203 - val ((p, p_), _, _, pt) = Ctree.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.204 + val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.205 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.206 in
1.207 ((p,p_), (pos,Uistate),
1.208 - Ctree.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.209 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.210 nxt, Safe, pt)
1.211 end
1.212 end
1.213 @@ -861,7 +861,7 @@
1.214 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.215 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.216 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
1.217 - val (p, Pbl, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
1.218 + val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
1.219 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
1.220 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.221 in
1.222 @@ -890,7 +890,7 @@
1.223 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.224 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.225 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
1.226 - val (p, Met, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
1.227 + val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
1.228 ((p, Met), c, _, pt') => (p, Met, c, pt')
1.229 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.230 in
1.231 @@ -965,7 +965,7 @@
1.232 val thy = assoc_thy dI
1.233 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
1.234 val {cas, ppc, ...} = Specify.get_pbt pI
1.235 - val pbl = Ctree.init_pbl ppc (* fill in descriptions *)
1.236 + val pbl = Generate.init_pbl ppc (* fill in descriptions *)
1.237 (*----------------if you think, this should be done by the Dialog
1.238 in the java front-end, search there for WN060225-modelProblem----*)
1.239 val (pbl, met) = case cas of
1.240 @@ -973,7 +973,7 @@
1.241 | _ => complete_mod_ (oris, mpc, ppc, probl)
1.242 (*----------------------------------------------------------------*)
1.243 val tac_ = Model_Problem' (pI, pbl, met)
1.244 - val (pos,c,_,pt) = Ctree.generate1 thy tac_ (Uistate, ctxt) pos pt
1.245 + val (pos,c,_,pt) = Generate.generate1 thy tac_ (Uistate, ctxt) pos pt
1.246 in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
1.247 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.248 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1.249 @@ -994,7 +994,7 @@
1.250 val mI = if length met = 0 then e_metID else hd met
1.251 val thy = assoc_thy dI
1.252 val (pos, c, _, pt) =
1.253 - Ctree.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1.254 + Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1.255 in
1.256 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.257 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.258 @@ -1013,7 +1013,7 @@
1.259 NONE => ([], [], ptp)
1.260 | SOME rfd =>
1.261 let
1.262 - val (pos,c,_,pt) = Ctree.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.263 + val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.264 in
1.265 ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.266 end
1.267 @@ -1028,10 +1028,10 @@
1.268 val {ppc,where_,prls,...} = Specify.get_pbt pI
1.269 val pbl =
1.270 if pI' = e_pblID andalso pI = e_pblID
1.271 - then (false, (Ctree.init_pbl ppc, []))
1.272 + then (false, (Generate.init_pbl ppc, []))
1.273 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
1.274 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.275 - val (c, pt) = case Ctree.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.276 + val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.277 ((_, Pbl), c, _, pt) => (c, pt)
1.278 | _ => error ""
1.279 in
1.280 @@ -1051,7 +1051,7 @@
1.281 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1.282 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
1.283 val (pos, c, _, pt) =
1.284 - Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.285 + Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.286 in
1.287 ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
1.288 end
1.289 @@ -1059,7 +1059,7 @@
1.290 let
1.291 val ctxt = get_ctxt pt pos
1.292 val (pos, c, _, pt) =
1.293 - Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.294 + Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.295 in (*FIXXXME: check if pbl can still be parsed*)
1.296 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
1.297 (pt, pos))
1.298 @@ -1067,7 +1067,7 @@
1.299 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
1.300 let
1.301 val ctxt = get_ctxt pt pos
1.302 - val (pos, c, _, pt) = Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.303 + val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.304 in (*FIXXXME: check if met can still be parsed*)
1.305 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
1.306 end
1.307 @@ -1090,7 +1090,7 @@
1.308 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
1.309 ([], (dI,pI,mI), hdl)
1.310 val pt = update_spec pt [] (dI, pI, mI)
1.311 - val pits = Ctree.init_pbl' ppc
1.312 + val pits = Generate.init_pbl' ppc
1.313 val pt = update_pbl pt [] pits
1.314 in ((pt, ([] , Pbl)), []) : calcstate end
1.315 else
1.316 @@ -1102,7 +1102,7 @@
1.317 val (pt, _) =
1.318 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1.319 val pt = update_spec pt [] (dI, pI, mI)
1.320 - val mits = Ctree.init_pbl' ppc
1.321 + val mits = Generate.init_pbl' ppc
1.322 val pt = update_met pt [] mits
1.323 in ((pt, ([], Met)), []) end
1.324 else (* new example, pepare for interactive modeling *)