theory KEStore 

 imports Complex_Main

 begin

   ML_file "~~/src/Tools/isac/library.sml"

   ML_file "~~/src/Tools/isac/calcelems.sml"

 section {* Knowledge elements for problems and methods *}

 ML {*

 (* Knowledge (and Exercises) are held by "KEStore" 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. 

   However, the structure of methods and problems is independent from theories' 

   deductive structure. Thus respective structures are built in Build_Thydata.thy.

   Most elements of problems and methods are implemented in "Knowledge/", but some

   of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this

   location in the directory structure.

 *)

 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

   val get_cas: theory -> cas_elem list

   val add_cas: cas_elem list -> theory -> theory

   val get_ptyps: theory -> ptyps

   val add_pbts: (pbt * pblID) list -> theory -> theory

   (*etc*)

 end;                               

 structure KEStore_Elems: KESTORE_ELEMS =

 struct

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

   structure Data = Theory_Data (

     type T = (rls' * (theory' * rls)) list;

     val empty = [];

     val extend = I;

     val merge = merge_rlss;

     );  

   fun get_rlss thy = Data.get thy

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

   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)

   structure Data = Theory_Data (

     type T = (term * (spec * (term list -> (term * term list) list))) list;

     val empty = [];

     val extend = I;

     val merge = merge cas_eq;

     );                                                              

   fun get_cas thy = Data.get thy

   fun add_cas cas = Data.map (union_overwrite cas_eq cas)

   structure Data = Theory_Data (

     type T = ptyps;

     val empty = [e_Ptyp];

     val extend = I;

     val merge = merge_ptyps;

     );

   fun get_ptyps thy = Data.get thy;

   fun add_pbts pbts thy = let

           fun add_pbt (pbt as {guh,...}, pblID) =

                 (* the pblID has the leaf-element as first; better readability achieved *)

                 (if (!check_guhs_unique) then check_pblguh_unique guh (Data.get thy) else ();

                   rev pblID |> insrt pblID pbt);

         in Data.map (fold add_pbt pbts) thy end;

   (*etc*)

 end;

 *}

 section {* Re-use existing access functions for knowledge elements *}

 text {*

   The independence of problems' and methods' structure enforces the accesse

   functions to use "Isac", the final theory which comprises all knowledge defined.

 *}

 ML {*

 (* in this phase of removing Unsynchornized.ref we do NOT overwrite the existing function! *)

 fun assoc_rls (rls' : rls') = (*SWITCH outcommented*)

   case AList.lookup (op =) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) rls' of

     SOME (_, rls) => rls

   | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^

     "TODO exception hierarchy needs to be established.")

 fun assoc_rls' thy (rls' : rls') = (*SWITCH outcommented*)

   case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of

     SOME (_, rls) => rls

   | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^

     "TODO exception hierarchy needs to be established.")

 fun assoc_calc thy calID = let

     fun ass ([], key) =

           error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))

       | ass ((calc, (keyi, _)) :: pairs, key) =

           if key = keyi then calc else ass (pairs, key);

   in ass (thy |> KEStore_Elems.get_calcs, calID) end;

 fun assoc_calc' thy key = let

     fun ass ([], key') =

           error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))

       | ass ((all as (keyi, _)) :: pairs, key') =

           if key' = keyi then all else ass (pairs, key');

   in ass (KEStore_Elems.get_calcs thy, key) end;

 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);

 fun get_ptyps () = ! ptyps;

 (*SWITCH:

 fun get_ptyps () = Thy_Info.get_theory "Build_Knowledge" |> KEStore_Elems.get_ptyps*)

 (*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel 

   SETUP ..* KEStore_Elems.add_pbt (.....) *.. 

 *)

 fun store_pbt (pbt as {guh,...}, pblID) = 

     (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else ();

      ptyps:= insrt pblID pbt (rev pblID) (! ptyps));

 *}

 setup {* KEStore_Elems.add_rlss 

   [("e_rls", (Context.theory_name @{theory}, e_rls)), 

   ("e_rrls", (Context.theory_name @{theory}, e_rrls))] *}

 section {* Functions for checking KEStore_Elems *}

 ML {*

 fun short_string_of_rls Erls = "Erls"

   | short_string_of_rls (Rls {calc, rules, ...}) =

     "Rls {#calc = " ^ string_of_int (length calc) ^

     ", #rules = " ^ string_of_int (length rules) ^ ", ..."

   | short_string_of_rls (Seq {calc, rules, ...}) =

     "Seq {#calc = " ^ string_of_int (length calc) ^

     ", #rules = " ^ string_of_int (length rules) ^ ", ..."

   | short_string_of_rls (Rrls _) = "Rrls {...}";

 fun check_kestore_rls (rls', (thyID, rls)) =

   "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";

 fun check_kestore_calc ((id, (c, _)) : calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";

 fun check_kestore_cas ((t, (s, _)):cas_elem) =

   "(" ^ (term_to_string''' @{theory} t) ^ ", " ^ (spec2str s) ^ ")";

 fun count_kestore_ptyps [] = 0

   | count_kestore_ptyps ((Ptyp (_, _, ps)) :: ps') =

       1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';

 fun check_kestore_ptyp ((Ptyp (key, pbts, pts)):pbt ptyp) = "Ptyp (" ^ (quote key) ^ ", " ^

       (pbts2str pbts) ^ ", " ^ (map check_kestore_ptyp pts |> list2str) ^ ")" |> linefeed;

 fun ptyp_ord ((Ptyp (s1, _, _)), (Ptyp (s2, _, _))) = string_ord (s1, s2);

 fun pbt_ord ({guh = guh'1, ...} : pbt, {guh = guh'2, ...} : pbt) = string_ord (guh'1, guh'2);

 fun sort_kestore_ptyp [] = []

   | sort_kestore_ptyp ((Ptyp (key, pbts, ps)) :: ps') =

      ((Ptyp (key, sort pbt_ord pbts, sort_kestore_ptyp ps |> sort ptyp_ord))

        :: sort_kestore_ptyp ps');

 *}

 end