2 Author: Walther Neuper 191026 |
2 Author: Walther Neuper 191026 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 signature MODEL_DEFINITION = |
5 signature MODEL_DEFINITION = |
6 sig |
6 sig |
7 type vats |
7 (* vats*) |
8 type ori |
8 type variants |
9 val oris2str : ori list -> string |
9 (* ori list*) |
10 val e_ori : ori |
10 type o_model |
11 datatype itm_ = Cor of (term * (term list)) * (term * (term list)) |
11 (* ori *) |
12 | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list)) |
12 type o_model_single |
13 | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string |
13 (* oris2str*) |
14 type itm |
14 val o_model_to_string : o_model_single list -> string |
15 val e_itm : itm |
15 (* e_ori*) |
|
16 val o_model_empty : o_model_single |
|
17 |
|
18 (* itm_ *) |
|
19 datatype i_model_feedback = Cor of (term * (term list)) * (term * (term list)) |
|
20 | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list)) |
|
21 | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string |
|
22 (* itm*) |
|
23 type i_model_single |
|
24 (*\<rightarrow> T*) |
|
25 type i_model |
|
26 (* e_itm*) |
|
27 val i_model_empty : i_model_single |
16 end |
28 end |
17 |
29 |
18 (**) |
30 (**) |
19 structure Model_Def(**): MODEL_DEFINITION(**) = |
31 structure Model_Def(**): MODEL_DEFINITION(**) = |
20 struct |
32 struct |
21 (**) |
33 (**) |
22 |
34 |
23 type vats = int list; (* variants in formalizations *) |
35 type variants = int list; (* variants in formalizations *) |
24 |
36 |
25 (* example as provided by an author, complete w.r.t. pbt specified |
37 (* example as provided by an author, complete w.r.t. pbt specified |
26 not touched by any user action *) |
38 not touched by any user action *) |
27 type ori = |
39 type o_model_single = |
28 (int * (* id: 10.3.00ff impl. only <>0 .. touched |
40 (int * (* id: 10.3.00ff impl. only <>0 .. touched |
29 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *) |
41 21.3.02: insert_ppc needs it ! ?:purpose maintain order in item ppc ??? *) |
30 vats * (* variants 21.3.02: related to pbt..discard ? *) |
42 variants * (* variants 21.3.02: related to pbt..discard ? *) |
31 string * (* #Given | #Find | #Relate 21.3.02: discard ? *) |
43 string * (* #Given | #Find | #Relate 21.3.02: discard ? *) |
32 term * (* description *) |
44 term * (* description *) |
33 term list (* isalist2list t | [t] *) |
45 term list (* isalist2list t | [t] *) |
34 ); |
46 ); |
35 val e_ori = (0, [], "", TermC.empty, [TermC.empty]) : ori; |
47 type o_model = o_model_single list; |
|
48 val o_model_empty = (0, [], "", TermC.empty, [TermC.empty]) : o_model_single; |
36 |
49 |
37 fun ori2str (i, vs, fi, t, ts) = |
50 fun ori2str (i, vs, fi, t, ts) = |
38 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^ |
51 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^ |
39 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; |
52 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; |
40 val oris2str = strs2str' o (map (linefeed o ori2str)); |
53 val o_model_to_string = strs2str' o (map (linefeed o ori2str)); |
41 |
54 |
42 |
55 |
43 (* the internal representation of a models' item |
56 (* the internal representation of a models' item |
44 4.9.01: not consistent: |
57 4.9.01: not consistent: |
45 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation |
58 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation |
46 (involves 'is_error'); |
59 (involves 'is_error'); |
47 bool in itm really necessary ???*) |
60 bool in i_model_single really necessary ???*) |
48 datatype itm_ = |
61 datatype i_model_feedback = |
49 Cor of (term * (* description *) |
62 Cor of (term * (* description *) |
50 (term list)) * (* for list: elem-wise input *) |
63 (term list)) * (* for list: elem-wise input *) |
51 (term * (term list)) (* elem of penv ---- penv delayed to future *) |
64 (term * (term list)) (* elem of penv ---- penv delayed to future *) |
52 | Syn of TermC.as_string |
65 | Syn of TermC.as_string |
53 | Typ of TermC.as_string |
66 | Typ of TermC.as_string |
57 | Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*) |
70 | Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*) |
58 | Par of TermC.as_string; (* internal state from fun parsitm *) |
71 | Par of TermC.as_string; (* internal state from fun parsitm *) |
59 |
72 |
60 (* data-type for working on pbl/met-ppc: |
73 (* data-type for working on pbl/met-ppc: |
61 in pbl initially holds descriptions (only) for user guidance *) |
74 in pbl initially holds descriptions (only) for user guidance *) |
62 type itm = |
75 type i_model_single = |
63 int * (* id =0 .. untouched - descript (only) from init |
76 int * (* id =0 .. untouched - descript (only) from init |
64 seems to correspond to ori (fun insert_ppc) <> maintain order in item ppc? *) |
77 seems to correspond to o_model_single (fun insert_ppc) <> maintain order in item ppc? *) |
65 vats * (* variants - copy from ori *) |
78 variants * (* variants - copy from o_model_single *) |
66 bool * (* input on this item is not/complete *) |
79 bool * (* input on this item is not/complete *) |
67 string * (* #Given | #Find | #Relate *) |
80 string * (* #Given | #Find | #Relate *) |
68 itm_; (* *) |
81 i_model_feedback; (* *) |
69 val e_itm = (0, [], false, "e_itm", Syn "e_itm"); |
82 type i_model = i_model_single list; |
|
83 val i_model_empty = (0, [], false, "i_model_empty", Syn "i_model_empty"); |
70 |
84 |
71 (**)end(**) |
85 (**)end(**) |