wneuper@59586: (*  Title:      src/Tools/isac/KEStore.thy
wneuper@59586:     Author:     Mathias Lehnfeld
wneuper@59586: *)
wneuper@59586: 
wneuper@59586: theory KEStore imports Complex_Main
wneuper@59586: 
wneuper@59586: begin
wneuper@59586: ML_file libraryC.sml
walther@59848: ML_file "rule-def.sml"
wneuper@59586: ML_file rule.sml
walther@59850: ML_file "rule-set.sml"
wneuper@59586: ML_file calcelems.sml
wneuper@59586: ML \<open>
wneuper@59586: \<close> ML \<open>
wneuper@59587: \<close> ML \<open>
wneuper@59586: \<close>
wneuper@59586: section \<open>Knowledge elements for problems and methods\<close>
wneuper@59586: ML \<open>
wneuper@59586: (* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
wneuper@59586:   In the front-end Knowledge comprises theories, problems and methods.
wneuper@59586:   Elements of problems and methods are defined in theories alongside
wneuper@59586:   the development of respective language elements. 
wneuper@59586:   However, the structure of methods and problems is independent from theories' 
wneuper@59586:   deductive structure. Thus respective structures are built in Build_Thydata.thy.
wneuper@59586: 
wneuper@59586:   Most elements of problems and methods are implemented in "Knowledge/", but some
wneuper@59586:   of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
wneuper@59586:   location in the directory structure.
wneuper@59586: 
wneuper@59586:   get_* retrieves all * of the respective theory PLUS of all ancestor theories.
wneuper@59586: *)
wneuper@59586: signature KESTORE_ELEMS =
wneuper@59586: sig
walther@59850:   val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list
walther@59850:   val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list -> theory -> theory
walther@59850:   val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
walther@59850:   val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
wneuper@59586:   val get_cas: theory -> Celem.cas_elem list
wneuper@59586:   val add_cas: Celem.cas_elem list -> theory -> theory
wneuper@59586:   val get_ptyps: theory -> Celem.ptyps
wneuper@59586:   val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
wneuper@59586:   val get_mets: theory -> Celem.mets
wneuper@59586:   val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
wneuper@59586:   val get_thes: theory -> (Celem.thydata Celem.ptyp) list
wneuper@59586:   val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
wneuper@59586:   val insert_fillpats: (Celem.theID * Celem.fillpat list) list -> theory -> theory 
wneuper@59586:   val get_ref_thy: unit -> theory
wneuper@59586:   val set_ref_thy: theory -> unit
wneuper@59586: end;                               
wneuper@59586: 
wneuper@59586: structure KEStore_Elems: KESTORE_ELEMS =
wneuper@59586: struct
wneuper@59586:   fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59850:     type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
walther@59850:     val merge = Rule_Set.merge_rlss;
wneuper@59586:     );  
wneuper@59586:   fun get_rlss thy = Data.get thy
walther@59850:   fun add_rlss rlss = Data.map (union_overwrite Rule_Set.rls_eq rlss)
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59850:     type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
walther@59850:     val merge = merge Rule_Set.calc_eq;
wneuper@59586:     );                                                              
wneuper@59586:   fun get_calcs thy = Data.get thy
walther@59850:   fun add_calcs calcs = Data.map (union_overwrite Rule_Set.calc_eq calcs)
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
wneuper@59586:     type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
wneuper@59586:     val merge = merge Celem.cas_eq;
wneuper@59586:     );                                                              
wneuper@59586:   fun get_cas thy = Data.get thy
wneuper@59586:   fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
wneuper@59586:     type T = Celem.ptyps;
wneuper@59586:     val empty = [Celem.e_Ptyp];
wneuper@59586:     val extend = I;
wneuper@59586:     val merge = Celem.merge_ptyps;
wneuper@59586:     );
wneuper@59586:   fun get_ptyps thy = Data.get thy;
wneuper@59586:   fun add_pbts pbts thy = let
wneuper@59586:           fun add_pbt (pbt as {guh,...}, pblID) =
wneuper@59586:                 (* the pblID has the leaf-element as first; better readability achieved *)
wneuper@59586:                 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
wneuper@59586:                   rev pblID |> Celem.insrt pblID pbt);
wneuper@59586:         in Data.map (fold add_pbt pbts) thy end;
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
wneuper@59586:     type T = Celem.mets;
wneuper@59586:     val empty = [Celem.e_Mets];
wneuper@59586:     val extend = I;
wneuper@59586:     val merge = Celem.merge_ptyps;
wneuper@59586:     );
wneuper@59586:   val get_mets = Data.get;
wneuper@59586:   fun add_mets mets thy = let
wneuper@59586:           fun add_met (met as {guh,...}, metID) =
wneuper@59586:                 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
wneuper@59586:                   Celem.insrt metID met metID);
wneuper@59586:         in Data.map (fold add_met mets) thy end;
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
wneuper@59586:     type T = (Celem.thydata Celem.ptyp) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
wneuper@59586:     val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
wneuper@59586:     );                                                              
wneuper@59586:   fun get_thes thy = Data.get thy
wneuper@59586:   fun add_thes thes thy = let
wneuper@59586:     fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
wneuper@59586:   in Data.map (fold add_the thes) thy end;
wneuper@59586:   fun insert_fillpats fis thy =
wneuper@59586:     let
wneuper@59586:       fun update_elem (theID, fillpats) =
wneuper@59586:         let
wneuper@59586:           val hthm = Celem.get_py (Data.get thy) theID theID
wneuper@59586:           val hthm' = Celem.update_hthm hthm fillpats
wneuper@59586:             handle ERROR _ =>
wneuper@59586:               error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
wneuper@59586:         in Celem.update_ptyps theID theID hthm' end
wneuper@59586:     in Data.map (fold update_elem fis) thy end
wneuper@59586: 
wneuper@59586:   val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
wneuper@59586:   fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
wneuper@59586:   fun get_ref_thy () = Synchronized.value cur_thy;
wneuper@59586: end;
wneuper@59586: \<close>
wneuper@59586: 
wneuper@59586: section \<open>Re-use existing access functions for knowledge elements\<close>
wneuper@59586: text \<open>
wneuper@59586:   The independence of problems' and methods' structure enforces the accesse
wneuper@59592:   functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
wneuper@59586: \<close>
wneuper@59586: ML \<open>
wneuper@59586: val get_ref_thy = KEStore_Elems.get_ref_thy;
wneuper@59586: 
walther@59850: fun assoc_rls (rls' : Rule_Set.rls') =
wneuper@59592:   case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) rls' of
wneuper@59586:     SOME (_, rls) => rls
wneuper@59586:   | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
wneuper@59586:     "TODO exception hierarchy needs to be established.")
wneuper@59586: 
walther@59850: fun assoc_rls' thy (rls' : Rule_Set.rls') =
wneuper@59586:   case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
wneuper@59586:     SOME (_, rls) => rls
wneuper@59586:   | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
wneuper@59586:     "TODO exception hierarchy needs to be established.")
wneuper@59586: 
wneuper@59586: fun assoc_calc thy calID = let
wneuper@59586:     fun ass ([], key) =
wneuper@59586:           error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
wneuper@59586:       | ass ((calc, (keyi, _)) :: pairs, key) =
wneuper@59586:           if key = keyi then calc else ass (pairs, key);
wneuper@59586:   in ass (thy |> KEStore_Elems.get_calcs, calID) end;
wneuper@59586: 
wneuper@59586: fun assoc_calc' thy key = let
wneuper@59586:     fun ass ([], key') =
wneuper@59586:           error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
wneuper@59586:       | ass ((all as (keyi, _)) :: pairs, key') =
wneuper@59586:           if key' = keyi then all else ass (pairs, key');
wneuper@59586:   in ass (KEStore_Elems.get_calcs thy, key) end;
wneuper@59586: 
wneuper@59586: fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
wneuper@59586: 
wneuper@59586: fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
wneuper@59586: fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
wneuper@59586: fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
wneuper@59586: \<close>
wneuper@59586: setup \<open>KEStore_Elems.add_rlss 
walther@59850:   [("e_rls", (Context.theory_name @{theory}, Rule_Set.e_rls)), 
walther@59850:   ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
wneuper@59586: 
wneuper@59586: section \<open>determine sequence of main parts in thehier\<close>
wneuper@59586: setup \<open>
wneuper@59586: KEStore_Elems.add_thes
wneuper@59586:   [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
wneuper@59586:     mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
wneuper@59586:   (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
wneuper@59586:     mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
wneuper@59586:   (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
wneuper@59586:     mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
wneuper@59586: \<close>
wneuper@59586: 
wneuper@59586: section \<open>Functions for checking KEStore_Elems\<close>
wneuper@59586: ML \<open>
walther@59850: fun short_string_of_rls Rule_Set.Erls = "Erls"
walther@59850:   | short_string_of_rls (Rule_Set.Rls {calc, rules, ...}) =
wneuper@59586:     "Rls {#calc = " ^ string_of_int (length calc) ^
wneuper@59586:     ", #rules = " ^ string_of_int (length rules) ^ ", ..."
walther@59850:   | short_string_of_rls (Rule_Set.Seq {calc, rules, ...}) =
wneuper@59586:     "Seq {#calc = " ^ string_of_int (length calc) ^
wneuper@59586:     ", #rules = " ^ string_of_int (length rules) ^ ", ..."
walther@59850:   | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
wneuper@59586: fun check_kestore_rls (rls', (thyID, rls)) =
wneuper@59586:   "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
wneuper@59586: 
walther@59850: fun check_kestore_calc ((id, (c, _)) : Rule_Set.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
wneuper@59586: 
walther@59846: (* we avoid term_to_string''' defined later *)
wneuper@59586: fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
walther@59846:   "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
walther@59846:   (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
wneuper@59586: 
wneuper@59586: fun count_kestore_ptyps [] = 0
wneuper@59586:   | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =
wneuper@59586:       1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
wneuper@59586: fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
wneuper@59586:       (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
wneuper@59586: val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
wneuper@59586: fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2);
wneuper@59586: fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
wneuper@59586: fun sort_kestore_ptyp' _ [] = []
wneuper@59586:   | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') =
wneuper@59586:      ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
wneuper@59586:        :: sort_kestore_ptyp' ordfun ps');
wneuper@59586: val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
wneuper@59586: 
wneuper@59586: fun metguh2str ({guh,...} : Celem.met) = guh : string;
wneuper@59586: fun check_kestore_met (mp: Celem.met Celem.ptyp) =
wneuper@59586:       check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
wneuper@59586: fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
wneuper@59586: val sort_kestore_met = sort_kestore_ptyp' met_ord;
wneuper@59586: 
wneuper@59586: fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
wneuper@59586: fun write_thes thydata_list =
wneuper@59586:   thydata_list 
wneuper@59586:     |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
wneuper@59586:     |> map pair2str
wneuper@59586:     |> map writeln
wneuper@59586: \<close>
wneuper@59586: ML \<open>
wneuper@59586: \<close> ML \<open>
wneuper@59586: \<close> ML \<open>
wneuper@59586: \<close>
wneuper@59586: end