(* 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 -> (rls' * (theory' * rls)) list

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

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

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

  (*etc*)

end;                               

structure 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 = (rls' * (theory' * 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 = (prog_calcID * (calID * 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;