7 *) |
7 *) |
8 |
8 |
9 signature MODEL = |
9 signature MODEL = |
10 sig |
10 sig |
11 (*/------- to O_Model+I_ from ModelModel -------\*) |
11 (*/------- to O_Model+I_ from ModelModel -------\*) |
12 type vats = Model_Def.vats |
12 type vats = Model_Def.variants |
13 (*\------- to O_Model+I_ from ModelModel -------/*) |
13 (*\------- to O_Model+I_ from ModelModel -------/*) |
14 (*/------- to O_Model from Model -------\*) |
14 (*/------- to O_Model from Model -------\*) |
15 type ori = Model_Def.ori |
15 type ori = Model_Def.o_model_single |
16 val oris2str: ori list -> string |
16 val oris2str: ori list -> string |
17 val e_ori: ori |
17 val e_ori: ori |
18 (*\------- to O_Model from Model -------/*) |
18 (*\------- to O_Model from Model -------/*) |
19 |
|
20 (*/------- to I_Model from Model -------\*) |
19 (*/------- to I_Model from Model -------\*) |
21 datatype itm_ = datatype Model_Def.itm_ |
20 datatype itm_ = datatype Model_Def.i_model_feedback |
22 type itm = Model_Def.itm |
21 type itm = I_Model.single |
23 val e_itm : itm |
22 val e_itm : itm |
24 (*\------- to I_Model from Model -------/*) |
23 (*\------- to I_Model from Model -------/*) |
25 |
24 |
26 datatype item |
25 datatype item |
27 = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string |
26 = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string |
251 | mkval _ [t] = t |
250 | mkval _ [t] = t |
252 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts; |
251 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts; |
253 fun mkval' x = mkval TermC.empty x; |
252 fun mkval' x = mkval TermC.empty x; |
254 |
253 |
255 (*/------- to O_Model+I_ from Mode -------\*) |
254 (*/------- to O_Model+I_ from Mode -------\*) |
256 type vats = Model_Def.vats; |
255 type vats = Model_Def.variants; |
257 (*\------- to O_Model+I_ from Model -------/*) |
256 (*\------- to O_Model+I_ from Model -------/*) |
258 |
257 |
259 (*/------- to I_Model from Model -------\*) |
258 (*/------- to I_Model from Model -------\*) |
260 (* the internal representation of a models' item |
259 (* the internal representation of a models' item |
261 4.9.01: not consistent: |
260 4.9.01: not consistent: |
262 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation |
261 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation |
263 (involves 'is_error'); |
262 (involves 'is_error'); |
264 bool in itm really necessary ???*) |
263 bool in itm really necessary ???*) |
265 datatype itm_ = datatype Model_Def.itm_; (* internal state from fun parsitm *) |
264 datatype itm_ = datatype Model_Def.i_model_feedback; (* internal state from fun parsitm *) |
266 |
265 |
267 (* data-type for working on pbl/met-ppc: |
266 (* data-type for working on pbl/met-ppc: |
268 in pbl initially holds descriptions (only) for user guidance *) |
267 in pbl initially holds descriptions (only) for user guidance *) |
269 type itm = |
268 type itm = |
270 int * (* id =0 .. untouched - descript (only) from init |
269 int * (* id =0 .. untouched - descript (only) from init |
315 |
314 |
316 |
315 |
317 (*/------- to O_Model from Model -------\*) |
316 (*/------- to O_Model from Model -------\*) |
318 (* example as provided by an author, complete w.r.t. pbt specified |
317 (* example as provided by an author, complete w.r.t. pbt specified |
319 not touched by any user action *) |
318 not touched by any user action *) |
320 type ori = Model_Def.ori; |
319 type ori = Model_Def.o_model_single; |
321 val e_ori = Model_Def.e_ori; |
320 val e_ori = Model_Def.o_model_empty; |
322 |
321 |
323 val oris2str = Model_Def.oris2str; |
322 val oris2str = Model_Def.o_model_to_string; |
324 (*\------- to O_Model from Model -------/*) |
323 (*\------- to O_Model from Model -------/*) |
325 |
324 |
326 (* an or without leading integer *) |
325 (* an or without leading integer *) |
327 type preori = (vats * string * term * term list); |
326 type preori = (vats * string * term * term list); |
328 fun preori2str (vs, fi, t, ts) = |
327 fun preori2str (vs, fi, t, ts) = |