89 val set_ref_thy: theory -> unit |
89 val set_ref_thy: theory -> unit |
90 end; |
90 end; |
91 |
91 |
92 structure KEStore_Elems(**): KESTORE_ELEMS(**) = |
92 structure KEStore_Elems(**): KESTORE_ELEMS(**) = |
93 struct |
93 struct |
94 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
|
95 |
|
96 structure Data = Theory_Data ( |
94 structure Data = Theory_Data ( |
97 type T = (string * (LibraryC.subst -> term * term -> bool)) list; |
95 type T = (string * (LibraryC.subst -> term * term -> bool)) list; |
98 val empty = []; |
96 val empty = []; |
99 val extend = I; |
97 val extend = I; |
100 val merge = merge Rewrite_Ord.equal; |
98 val merge = merge Rewrite_Ord.equal; |
101 ); |
99 ); |
102 fun get_rew_ord thy = Data.get thy |
100 fun get_rew_ord thy = Data.get thy |
103 fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss) |
101 fun add_rew_ord rlss = Data.map (curry (Library.merge Rewrite_Ord.equal) rlss) |
104 |
102 |
105 structure Data = Theory_Data ( |
103 structure Data = Theory_Data ( |
106 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list; |
104 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list; |
107 val empty = []; |
105 val empty = []; |
108 val extend = I; |
106 val extend = I; |
109 val merge = Rule_Set.to_kestore; |
107 val merge = Rule_Set.to_kestore; |
110 ); |
108 ); |
111 fun get_rlss thy = Data.get thy |
109 fun get_rlss thy = Data.get thy |
112 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss) |
110 fun add_rlss rlss = Data.map (curry (Library.merge Rule_Set.equal) rlss) |
113 |
111 |
114 structure Data = Theory_Data ( |
112 structure Data = Theory_Data ( |
115 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list; |
113 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list; |
116 val empty = []; |
114 val empty = []; |
117 val extend = I; |
115 val extend = I; |
118 val merge = merge Eval_Def.calc_eq; |
116 val merge = merge Eval_Def.calc_eq; |
119 ); |
117 ); |
120 fun get_calcs thy = Data.get thy |
118 fun get_calcs thy = Data.get thy |
121 fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs) |
119 fun add_calcs calcs = Data.map (curry (Library.merge Eval_Def.calc_eq) calcs) |
122 |
120 |
123 structure Data = Theory_Data ( |
121 structure Data = Theory_Data ( |
124 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list; |
122 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list; |
125 val empty = []; |
123 val empty = []; |
126 val extend = I; |
124 val extend = I; |
127 val merge = merge CAS_Def.equal; |
125 val merge = merge CAS_Def.equal; |
128 ); |
126 ); |
129 fun get_cas thy = Data.get thy |
127 fun get_cas thy = Data.get thy |
130 fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas) |
128 fun add_cas cas = Data.map (curry (Library.merge CAS_Def.equal) cas) |
131 |
129 |
132 structure Data = Theory_Data ( |
130 structure Data = Theory_Data ( |
133 type T = Probl_Def.store; |
131 type T = Probl_Def.store; |
134 val empty = [Probl_Def.empty_store]; |
132 val empty = [Probl_Def.empty_store]; |
135 val extend = I; |
133 val extend = I; |
356 |> map pair2str |
354 |> map pair2str |
357 |> map writeln |
355 |> map writeln |
358 \<close> |
356 \<close> |
359 ML \<open> |
357 ML \<open> |
360 \<close> ML \<open> |
358 \<close> ML \<open> |
|
359 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
|
360 \<close> ML \<open> |
|
361 union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list; |
|
362 merge : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list |
|
363 \<close> ML \<open> |
|
364 val eq = op=; |
|
365 val l1 = [1,2,3,4,5]; |
|
366 val l2 = [4,5,6,7,8]; |
|
367 \<close> ML \<open> |
|
368 union_overwrite eq l1 l2 = [8, 7, 6, 1, 2, 3, 4, 5]; |
|
369 Library.merge eq (l1, l2) = [6, 7, 8, 1, 2, 3, 4, 5] |
|
370 \<close> ML \<open> |
|
371 \<close> ML \<open> |
|
372 Library.merge eq (*: _a list * _a list -> _a list*); |
|
373 curry (Library.merge eq)(*: _a list -> _a list -> _a list*) |
|
374 \<close> ML \<open> |
|
375 \<close> ML \<open> |
361 \<close> ML \<open> |
376 \<close> ML \<open> |
362 \<close> |
377 \<close> |
363 end |
378 end |