(* Know_Store 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.id * (ThyC.id * Rule_Set.T)) list

   val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory

   val get_calcs: theory -> Eval.ml_from_prog list

   val add_calcs: Eval.ml_from_prog list -> theory -> theory

   (*etc*)

 end;                               

 structure Test_KEStore_Elems: KESTORE_ELEMS =

 struct

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

   structure Data = Theory_Data (

     type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;

     val empty = [];

     val extend = I;

     val merge = merge rls_eq;

     );  

   fun get_rlss thy = Data.get thy

   fun add_rlss rlss = Data.map (curry (Library.merge rls_eq) rlss)

   val calc_eq = rls_eq

   structure Data = Theory_Data (

     type T = Eval.ml_from_prog list;

     val empty = [];

     val extend = I;

     val merge = merge calc_eq;

     );                                                              

   fun get_calcs thy = Data.get thy

   fun add_calcs calcs = Data.map (curry (Library.merge calc_eq) calcs)

   (*etc*)

 end;