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

  (*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)

  (*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;

*}

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 string_of_calc ((id, (c, _)) : calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))"

*}

end