(*  Title:      src/Tools/isac/KEStore.thy

    Author:     Mathias Lehnfeld

*)

theory KEStore imports Complex_Main

begin

ML_file libraryC.sml

ML_file "rule-def.sml"

ML_file rule.sml

ML_file "rule-set.sml"

ML_file calcelems.sml

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

section \<open>Knowledge elements for problems and methods\<close>

ML \<open>

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

  get_* retrieves all * of the respective theory PLUS of all ancestor theories.

*)

signature KESTORE_ELEMS =

sig

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

  val add_rlss: (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) 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

  val get_cas: theory -> Celem.cas_elem list

  val add_cas: Celem.cas_elem list -> theory -> theory

  val get_ptyps: theory -> Celem.ptyps

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

  val get_mets: theory -> Celem.mets

  val add_mets: (Celem.met * Celem.metID) list -> theory -> theory

  val get_thes: theory -> (Celem.thydata Celem.ptyp) list

  val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)

  val insert_fillpats: (Celem.theID * Celem.fillpat list) list -> theory -> theory 

  val get_ref_thy: unit -> theory

  val set_ref_thy: theory -> unit

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 = (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list;

    val empty = [];

    val extend = I;

    val merge = Rule_Set.to_kestore;

    );  

  fun get_rlss thy = Data.get thy

  fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)

  structure Data = Theory_Data (

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

    val empty = [];

    val extend = I;

    val merge = merge Rule_Set.calc_eq;

    );                                                              

  fun get_calcs thy = Data.get thy

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

  structure Data = Theory_Data (

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

    val empty = [];

    val extend = I;

    val merge = merge Celem.cas_eq;

    );                                                              

  fun get_cas thy = Data.get thy

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

  structure Data = Theory_Data (

    type T = Celem.ptyps;

    val empty = [Celem.e_Ptyp];

    val extend = I;

    val merge = Celem.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 (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();

                  rev pblID |> Celem.insrt pblID pbt);

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

  structure Data = Theory_Data (

    type T = Celem.mets;

    val empty = [Celem.e_Mets];

    val extend = I;

    val merge = Celem.merge_ptyps;

    );

  val get_mets = Data.get;

  fun add_mets mets thy = let

          fun add_met (met as {guh,...}, metID) =

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

                  Celem.insrt metID met metID);

        in Data.map (fold add_met mets) thy end;

  structure Data = Theory_Data (

    type T = (Celem.thydata Celem.ptyp) list;

    val empty = [];

    val extend = I;

    val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)

    );                                                              

  fun get_thes thy = Data.get thy

  fun add_thes thes thy = let

    fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata

  in Data.map (fold add_the thes) thy end;

  fun insert_fillpats fis thy =

    let

      fun update_elem (theID, fillpats) =

        let

          val hthm = Celem.get_py (Data.get thy) theID theID

          val hthm' = Celem.update_hthm hthm fillpats

            handle ERROR _ =>

              error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")

        in Celem.update_ptyps theID theID hthm' end

    in Data.map (fold update_elem fis) thy end

  val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};

  fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)

  fun get_ref_thy () = Synchronized.value cur_thy;

end;

\<close>

section \<open>Re-use existing access functions for knowledge elements\<close>

text \<open>

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

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

\<close>

ML \<open>

val get_ref_thy = KEStore_Elems.get_ref_thy;

fun assoc_rls (rls' : Rule_Set.identifier) =

  case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) 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' : Rule_Set.identifier) =

  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 () = get_ref_thy () |> KEStore_Elems.get_ptyps;

fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;

fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;

\<close>

setup \<open>KEStore_Elems.add_rlss 

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

  ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>

section \<open>determine sequence of main parts in thehier\<close>

setup \<open>

KEStore_Elems.add_thes

  [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",

    mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),

  (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",

    mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),

  (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",

    mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]

\<close>

section \<open>Functions for checking KEStore_Elems\<close>

ML \<open>

fun short_string_of_rls Rule_Set.Empty = "Erls"

  | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =

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

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

  | short_string_of_rls (Rule_Set.Seqence {calc, rules, ...}) =

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

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

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

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

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

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

(* we avoid term_to_string''' defined later *)

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

  "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false

  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";

fun count_kestore_ptyps [] = 0

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

      1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';

fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^

      (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;

val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;

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

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

fun sort_kestore_ptyp' _ [] = []

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

     ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))

       :: sort_kestore_ptyp' ordfun ps');

val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;

fun metguh2str ({guh,...} : Celem.met) = guh : string;

fun check_kestore_met (mp: Celem.met Celem.ptyp) =

      check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;

fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);

val sort_kestore_met = sort_kestore_ptyp' met_ord;

fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes

fun write_thes thydata_list =

  thydata_list 

    |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))

    |> map pair2str

    |> map writeln

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end