4 |
4 |
5 Will be enhanced by Method later. |
5 Will be enhanced by Method later. |
6 *) |
6 *) |
7 signature METHOD_DEFINITION = |
7 signature METHOD_DEFINITION = |
8 sig |
8 sig |
9 type met |
9 type T |
10 val e_met: met |
10 (*type met*) |
11 type mets |
11 val empty: T |
12 val e_Mets: met Store.ptyp |
12 (*val e_met: T*) |
13 (*vvv check_unique*) |
13 type store |
14 val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit |
14 (*type mets*) |
|
15 val empty_store: T Store.ptyp |
|
16 (*val e_Mets: T Store.ptyp*) |
|
17 val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit |
|
18 (*val check_metguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*) |
15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
16 (*NONE*) |
20 (*NONE*) |
17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
18 (*NONE*) |
22 (*NONE*) |
19 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
23 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
22 (**) |
26 (**) |
23 structure Meth_Def(**): METHOD_DEFINITION(**) = |
27 structure Meth_Def(**): METHOD_DEFINITION(**) = |
24 struct |
28 struct |
25 (**) |
29 (**) |
26 |
30 |
27 (*/------- to Celem6 -------\*) |
|
28 (* data for methods stored in 'methods'-database*) |
31 (* data for methods stored in 'methods'-database*) |
29 type met = |
32 type T = |
30 {guh : Check_Unique.guh, (* unique within this isac-knowledge *) |
33 {guh : Check_Unique.guh, (* unique within this isac-knowledge *) |
31 mathauthors: string list, (* copyright *) |
34 mathauthors: string list, (* copyright *) |
32 init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *) |
35 init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *) |
33 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail |
36 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail |
34 TODO.WN0509 store fun itself, see 'type pbt' *) |
37 TODO.WN0509 store fun itself, see 'type pbt' *) |
48 are 'copy-named' with an identifier "*'.'". |
51 are 'copy-named' with an identifier "*'.'". |
49 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
52 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
50 see ME/calchead.sml 'fun is_copy_named'. *) |
53 see ME/calchead.sml 'fun is_copy_named'. *) |
51 pre : term list (* preconditions in where *) |
54 pre : term list (* preconditions in where *) |
52 }; |
55 }; |
53 val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord', |
56 val empty = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord', |
54 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty, |
57 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty, |
55 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog}; |
58 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog}; |
56 val e_Mets = Store.Ptyp ("e_metID", [e_met],[]); |
59 val empty_store = Store.Ptyp ("e_metID", [empty],[]); |
57 |
60 |
58 type mets = (met Store.ptyp) list; |
61 type store = (T Store.ptyp) list; |
59 (*\------- to Celem6 -------/*) |
62 (*\------- to Celem6 -------/*) |
60 |
63 |
61 val check_metguh_unique = |
64 val check_unique = |
62 Check_Unique.message (Check_Unique.collect (#guh: met -> Check_Unique.guh)); |
65 Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.guh)); |
63 |
66 |
64 (**)end(**) |
67 (**)end(**) |