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

     Author:     Mathias Lehnfeld

 The files (in "xxxxx-def.sml") contain definitions required for KEStore;

 they also include minimal code required for other "xxxxx-def.sml" files.

 These files have companion files "xxxxx.sml" with all further code,

 located at appropriate positions in the file structure.

 The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by

 appropriate use of polymorphic high order functions.

 *)

 theory KEStore imports Complex_Main

 begin

 ML_file libraryC.sml

 ML_file theoryC.sml

 ML_file unparseC.sml

 ML_file "rule-def.sml"

 ML_file "thmC-def.sml"

 ML_file "exec-def.sml"       (*rename identifiers by use of struct.id*)

 ML_file "rewrite-order.sml"  (*rename identifiers by use of struct.id*)

 ML_file rule.sml

 ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)

 ML_file "rule-set.sml"

 ML_file "celem-0.sml"  (*survey Celem.*)

 ML_file "celem-1.sml"  (*datatype 'a ptyp*)

 ML_file "celem-2.sml"  (*guh*)

 ML_file "celem-3.sml"  (*spec*)

 ML_file "celem-4.sml"  (*pat*)

 ML_file "celem-5.sml"  (*ptyps*)

 ML_file "celem-6.sml"  (*mets*)

 ML_file "celem-7.sml"  (*cas_elem*)

 ML_file "celem-8.sml"  (*thydata*)

 ML_file "celem-91.sml" (*check_guhs_unique*)

 ML_file "celem-92.sml" (**)

 ML_file "celem-93.sml" (**)

 ML_file calcelems.sml

 ML_file tracing.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.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 -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list

   val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.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 * Error_Fill_Def.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.id * (ThyC.id * 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 = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;

     val empty = [];

     val extend = I;

     val merge = merge Exec_Def.calc_eq;

     );                                                              

   fun get_calcs thy = Data.get thy

   fun add_calcs calcs = Data.map (union_overwrite Exec_Def.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.id) =

   case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.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.id) =

   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.Sequence {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