equal
deleted
inserted
replaced
24 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list |
24 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list |
25 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory |
25 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory |
26 val get_cas: theory -> cas_elem list |
26 val get_cas: theory -> cas_elem list |
27 val add_cas: cas_elem list -> theory -> theory |
27 val add_cas: cas_elem list -> theory -> theory |
28 val get_ptyps: theory -> ptyps |
28 val get_ptyps: theory -> ptyps |
29 val store_pbts: (pbt * pblID) list -> theory -> theory |
29 val add_pbts: (pbt * pblID) list -> theory -> theory |
30 val add_pbt: (pbt * pblID) -> theory -> theory |
|
31 (*etc*) |
30 (*etc*) |
32 end; |
31 end; |
33 |
32 |
34 structure KEStore_Elems: KESTORE_ELEMS = |
33 structure KEStore_Elems: KESTORE_ELEMS = |
35 struct |
34 struct |
67 val empty = [e_Ptyp]; |
66 val empty = [e_Ptyp]; |
68 val extend = I; |
67 val extend = I; |
69 val merge = merge_ptyps; |
68 val merge = merge_ptyps; |
70 ); |
69 ); |
71 fun get_ptyps thy = Data.get thy; |
70 fun get_ptyps thy = Data.get thy; |
72 fun store_pbts pbts = let |
71 fun add_pbts pbts thy = let |
73 fun store_pbts' (pbt, pblID) = rev pblID |> insrt pblID pbt; |
72 fun add_pbt (pbt as {guh,...}, pblID) = |
74 in fold store_pbts' pbts |> Data.map end; |
73 (* the pblID has the leaf-element as first; better readability achieved *) |
75 (* the pblID has the leaf-element as first; better readability achieved *) |
74 (if (!check_guhs_unique) then check_pblguh_unique guh (Data.get thy) else (); |
76 fun add_pbt (pbt as {guh,...}, pblID) = |
75 rev pblID |> insrt pblID pbt); |
77 (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else (); |
76 in Data.map (fold add_pbt pbts) thy end; |
78 Data.map (insrt pblID pbt (rev pblID))) |
|
79 |
77 |
80 (*etc*) |
78 (*etc*) |
81 end; |
79 end; |
82 *} |
80 *} |
83 |
81 |
114 if key' = keyi then all else ass (pairs, key'); |
112 if key' = keyi then all else ass (pairs, key'); |
115 in ass (KEStore_Elems.get_calcs thy, key) end; |
113 in ass (KEStore_Elems.get_calcs thy, key) end; |
116 |
114 |
117 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key); |
115 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key); |
118 |
116 |
119 fun get_ptyps () = ! ptyps |
117 fun get_ptyps () = ! ptyps; |
120 (*SWITCH: |
118 (*SWITCH: |
121 fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*); |
119 fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*) |
122 val store_pbts = KEStore_Elems.store_pbts; |
|
123 |
120 |
124 (*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel |
121 (*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel |
125 SETUP ..* KEStore_Elems.add_pbt (.....) *.. |
122 SETUP ..* KEStore_Elems.add_pbt (.....) *.. |
126 *) |
123 *) |
127 fun store_pbt (pbt as {guh,...}, pblID) = |
124 fun store_pbt (pbt as {guh,...}, pblID) = |