221 let |
221 let |
222 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, []))) |
222 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, []))) |
223 in map pbt2itm pbt end |
223 in map pbt2itm pbt end |
224 |
224 |
225 (* |
225 (* |
226 Design decision: |
226 NEW design decision: |
227 * Now the Model in Specification is intialised such that the placement of items can be |
227 * Now the Model in Specification is intialised such that the placement of items can be |
228 maximally stable during interactive input to the Specification. |
228 maximally stable during interactive input to the Specification. |
229 * Template.show provides the initial output to the user and thus determines what will be parsed |
229 * Template.show provides the initial output to the user and thus determines what will be parsed |
230 by Outer_Syntax later during interaction. |
230 by Outer_Syntax later during interaction. |
231 * The relation between O_Model.T and I_Model.T becomes much simpler. |
231 * The relation between O_Model.T and I_Model.T becomes much simpler. |
232 *) |
232 *) |
233 (**) |
233 (**) |
234 fun pat_to_item ctxt o_model (_, (descriptor, _)) = |
234 fun patt_to_item ctxt o_model (_, (descriptor, _)) = |
235 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of |
235 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of |
236 NONE => raise ERROR ("I_Model.pat_to_item NONE for " ^ UnparseC.term ctxt descriptor) |
236 NONE => raise ERROR ("I_Model.patt_to_item NONE for " ^ UnparseC.term ctxt descriptor) |
237 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field, |
237 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field, |
238 (Inc_TEST (descr, []), Position.none)) |
238 (Inc_TEST (descr, []), Position.none)) |
239 fun init_TEST ctxt o_model model_patt = |
239 fun init_TEST ctxt o_model model_patt = |
240 let |
240 let |
241 val pre_items = map (pat_to_item ctxt o_model) model_patt |
241 val pre_items = map (patt_to_item ctxt o_model) model_patt |
242 in |
242 in |
243 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)) |
243 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)) |
244 end |
244 end |
245 |
245 |
246 |
246 |
247 val unique = Syntax.read_term\<^context> "UnIqE_tErM"; |
247 val unique = Syntax.read_term\<^context> "UnIqE_tErM"; |
248 (*/-wait for intro-fn into M_Match-\*) |
248 (*DANGEROUS: do NOT use "UnIqE_tErM" *) |
249 fun descriptor (Cor ((d ,_), _)) = d |
249 fun descriptor (Cor ((d ,_), _)) = d |
250 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique) |
250 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique) |
251 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique) |
251 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique) |
252 | descriptor (Inc ((d, _), _)) = d |
252 | descriptor (Inc ((d, _), _)) = d |
253 | descriptor (Sup (d, _)) = d |
253 | descriptor (Sup (d, _)) = d |
254 | descriptor (Mis (d, _)) = d |
254 | descriptor (Mis (d, _)) = d |
255 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def."; |
255 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def."; |
256 (*\-wait for intro-fn into M_Match-/*) |
256 (*DANGEROUS: do NOT use "UnIqE_tErM" *) |
257 fun descriptor_TEST (Cor_TEST (d ,_)) = d |
257 fun descriptor_TEST (Cor_TEST (d ,_)) = d |
258 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique) |
258 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique) |
259 | descriptor_TEST (Inc_TEST (d, _)) = d |
259 | descriptor_TEST (Inc_TEST (d, _)) = d |
260 | descriptor_TEST (Sup_TEST (d, _)) = d |
260 | descriptor_TEST (Sup_TEST (d, _)) = d |
261 |
261 |
513 NONE => |
513 NONE => |
514 (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*) |
514 (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*) |
515 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*) |
515 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*) |
516 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*) |
516 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*) |
517 |
517 |
|
518 (*fill method from items already input*) |
518 fun fill_method o_model (pbl_imod, met_imod) met_patt = |
519 fun fill_method o_model (pbl_imod, met_imod) met_patt = |
519 let |
520 let |
520 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod |
521 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod |
521 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*) |
522 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*) |
522 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*) |
523 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*) |