(* KEStore holds Knowledge and Exercises in Isac's Java front-end.

   In the front-end knowledge comprises theories, problems and methods.

   Elements of problems and methods are defined in theories alongside

   the development of respective language elements. 

   The structure of methods and problems is independent from theories' deductive

   structure. The respective structures are built in Build_Thydata.thy.

 *)

 signature KESTORE_ELEMS =

 sig

   val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list

   val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list -> theory -> theory

   val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list

   val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory

   (*etc*)

 end;                               

 structure Test_KEStore_Elems: KESTORE_ELEMS =

 struct

   fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;

   fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)

   structure Data = Theory_Data (

     type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list;

     val empty = [];

     val extend = I;

     val merge = merge rls_eq;

     );  

   fun get_rlss thy = Data.get thy

   fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)

   val calc_eq = rls_eq

   structure Data = Theory_Data (

     type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;

     val empty = [];

     val extend = I;

     val merge = merge calc_eq;

     );                                                              

   fun get_calcs thy = Data.get thy

   fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)

   (*etc*)

 end;