174 in map pbt2itm pbt end |
174 in map pbt2itm pbt end |
175 |
175 |
176 (*generate 1 ppobj in ptree*) |
176 (*generate 1 ppobj in ptree*) |
177 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*) |
177 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*) |
178 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt = |
178 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt = |
179 (pos: pos', [], PpcKF (Upblmet, itms2itemppc thy [][]), |
179 (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]), |
180 case p_ of |
180 case p_ of |
181 Pbl => update_pbl pt p itmlist |
181 Pbl => update_pbl pt p itmlist |
182 | Met => update_met pt p itmlist |
182 | Met => update_met pt p itmlist |
183 | _ => error ("uncovered case " ^ pos_2str p_)) |
183 | _ => error ("uncovered case " ^ pos_2str p_)) |
184 (* WN110515 probably declare_constraints with input item (without dsc) -- |
184 (* WN110515 probably declare_constraints with input item (without dsc) -- |
185 -- important when specifying without formalisation *) |
185 -- important when specifying without formalisation *) |
186 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt = |
186 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt = |
187 (pos, [], (PpcKF (Upblmet, itms2itemppc thy [] [])), |
187 (pos, [], (PpcKF (Upblmet, Specify.itms2itemppc thy [] [])), |
188 case p_ of |
188 case p_ of |
189 Pbl => update_pbl pt p itmlist |
189 Pbl => update_pbl pt p itmlist |
190 | Met => update_met pt p itmlist |
190 | Met => update_met pt p itmlist |
191 | _ => error ("uncovered case " ^ pos_2str p_)) |
191 | _ => error ("uncovered case " ^ pos_2str p_)) |
192 (*WN110515 probably declare_constraints with input item (without dsc)*) |
192 (*WN110515 probably declare_constraints with input item (without dsc)*) |
193 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt = |
193 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt = |
194 (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), |
194 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), |
195 case p_ of |
195 case p_ of |
196 Pbl => update_pbl pt p itmlist |
196 Pbl => update_pbl pt p itmlist |
197 | Met => update_met pt p itmlist |
197 | Met => update_met pt p itmlist |
198 | _ => error ("uncovered case " ^ pos_2str p_)) |
198 | _ => error ("uncovered case " ^ pos_2str p_)) |
199 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt = |
199 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt = |
200 (pos, [] , PpcKF (Upblmet, itms2itemppc thy [] []), |
200 (pos, [] , PpcKF (Upblmet, Specify.itms2itemppc thy [] []), |
201 update_domID pt p domID) |
201 update_domID pt p domID) |
202 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt = |
202 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt = |
203 let |
203 let |
204 val pt = update_pbl pt p itms |
204 val pt = update_pbl pt p itms |
205 val pt = update_pblID pt p pI |
205 val pt = update_pblID pt p pI |
206 in |
206 in |
207 ((p, Pbl), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt) |
207 ((p, Pbl), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) |
208 end |
208 end |
209 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt = |
209 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt = |
210 let |
210 let |
211 val pt = update_oris pt p oris |
211 val pt = update_oris pt p oris |
212 val pt = update_met pt p itms |
212 val pt = update_met pt p itms |
213 val pt = update_metID pt p mID |
213 val pt = update_metID pt p mID |
214 in |
214 in |
215 ((p, Met), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt) |
215 ((p, Met), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) |
216 end |
216 end |
217 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt = |
217 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt = |
218 let |
218 let |
219 val pt = update_pbl pt p itms |
219 val pt = update_pbl pt p itms |
220 val pt = update_met pt p met |
220 val pt = update_met pt p met |
221 in |
221 in |
222 (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt) |
222 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) |
223 end |
223 end |
224 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt = |
224 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt = |
225 let |
225 let |
226 val pt = update_pbl pt p pbl |
226 val pt = update_pbl pt p pbl |
227 val pt = update_orispec pt p (domID, pIre, metID) |
227 val pt = update_orispec pt p (domID, pIre, metID) |
228 in |
228 in |
229 (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt) |
229 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) |
230 end |
230 end |
231 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt = |
231 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt = |
232 let |
232 let |
233 val (dI, _, mI) = get_obj g_spec pt p |
233 val (dI, _, mI) = get_obj g_spec pt p |
234 val pt = update_spec pt p (dI, pI, mI) |
234 val pt = update_spec pt p (dI, pI, mI) |
235 in |
235 in |
236 (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt) |
236 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) |
237 end |
237 end |
238 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt = |
238 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt = |
239 (case topt of |
239 (case topt of |
240 SOME t => |
240 SOME t => |
241 let val (pt, c) = cappend_form pt p (is, ctxt) t |
241 let val (pt, c) = cappend_form pt p (is, ctxt) t |
422 val form = get_obj g_form pt p |
422 val form = get_obj g_form pt p |
423 (*val p = lev_on p; ---------------only difference to (..,Res) below*) |
423 (*val p = lev_on p; ---------------only difference to (..,Res) below*) |
424 val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) :: |
424 val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) :: |
425 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), |
425 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), |
426 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))] |
426 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))] |
427 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p)) |
427 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p)) |
428 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res)) |
428 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res)) |
429 val pt = update_tac pt p (Derive (id_rls nrls)) |
429 val pt = update_tac pt p (Derive (id_rls nrls)) |
430 val pt = update_branch pt p TransitiveB |
430 val pt = update_branch pt p TransitiveB |
431 in (c, (pt, pos: pos')) end |
431 in (c, (pt, pos: pos')) end |
432 | embed_deriv tacis (pt, (p, Res)) = |
432 | embed_deriv tacis (pt, (p, Res)) = |
439 val (f, _) = get_obj g_result pt p |
439 val (f, _) = get_obj g_result pt p |
440 val p = lev_on p(*---------------only difference to (..,Frm) above*); |
440 val p = lev_on p(*---------------only difference to (..,Frm) above*); |
441 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) :: |
441 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) :: |
442 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), |
442 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), |
443 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]; |
443 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]; |
444 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p)) |
444 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p)) |
445 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res)) |
445 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res)) |
446 val pt = update_tac pt p (Derive (id_rls nrls)) |
446 val pt = update_tac pt p (Derive (id_rls nrls)) |
447 val pt = update_branch pt p TransitiveB |
447 val pt = update_branch pt p TransitiveB |
448 in (c, (pt, pos)) end |
448 in (c, (pt, pos)) end |
449 | embed_deriv _ _ = error "embed_deriv: uncovered definition" |
449 | embed_deriv _ _ = error "embed_deriv: uncovered definition" |