
walther@59887: (*  Title:      src/Tools/isac/Know_Store.thy
wneuper@59586:     Author:     Mathias Lehnfeld
walther@59871: 
walther@59890: Calc work on Problem employing Method; both are collected in a respective Store;
walther@59890: The collections' structure is independent from the dependency graph of Isabelle's theories
walther@59890: in Knowledge.
walther@59917: Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
walther@59890: 
walther@59887: The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
walther@59871: they also include minimal code required for other "xxxxx-def.sml" files.
walther@59871: These files have companion files "xxxxx.sml" with all further code,
walther@59871: located at appropriate positions in the file structure.
walther@59871: 
walther@59871: The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
walther@59871: appropriate use of polymorphic high order functions.
wneuper@59586: *)
wneuper@59586: 
walther@59887: theory Know_Store imports Complex_Main
wneuper@59586: 
wneuper@59586: begin
wneuper@59586: ML_file libraryC.sml
walther@59880: ML_file theoryC.sml
walther@59868: ML_file unparseC.sml
walther@59874: ML_file "rule-def.sml"
walther@59875: ML_file "thmC-def.sml"
walther@59919: ML_file "eval-def.sml"       (*rename identifiers by use of struct.id*)
walther@59867: ML_file "rewrite-order.sml"  (*rename identifiers by use of struct.id*)
wneuper@59586: ML_file rule.sml
walther@59909: ML_file "error-pattern-def.sml"
walther@59850: ML_file "rule-set.sml"
walther@59882: 
walther@59891: ML_file "store.sml"
walther@59892: ML_file "check-unique.sml"
walther@59891: ML_file "specification.sml"
walther@59945: ML_file "model-pattern.sml"
walther@59893: ML_file "problem-def.sml"
walther@59893: ML_file "method-def.sml"
walther@59893: ML_file "cas-def.sml"
walther@59917: ML_file "thy-write.sml"
walther@59882: 
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>
walther@59887: (* Knowledge (and Exercises) are held by "Know_Store" 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
walther@59887:   of them are implemented in "ProgLang/" already; thus "Know_Store.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@59879:   val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
walther@59879:   val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
walther@59919:   val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
walther@59919:   val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
walther@59896:   val get_cas: theory -> CAS_Def.T list
walther@59896:   val add_cas: CAS_Def.T list -> theory -> theory
walther@59894:   val get_ptyps: theory -> Probl_Def.store
walther@59903:   val add_pbts: (Probl_Def.T * Spec.id) list -> theory -> theory
walther@59895:   val get_mets: theory -> Meth_Def.store
walther@59903:   val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
walther@59917:   val get_thes: theory -> (Thy_Write.thydata Store.node) list
walther@59917:   val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
walther@59917:   val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in 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@59879:     type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
walther@59852:     val merge = Rule_Set.to_kestore;
wneuper@59586:     );  
wneuper@59586:   fun get_rlss thy = Data.get thy
walther@59852:   fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59919:     type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
walther@59919:     val merge = merge Eval_Def.calc_eq;
wneuper@59586:     );                                                              
wneuper@59586:   fun get_calcs thy = Data.get thy
walther@59919:   fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59903:     type T = (term * (Spec.T * (term list -> (term * term list) list))) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
walther@59896:     val merge = merge CAS_Def.equal;
wneuper@59586:     );                                                              
wneuper@59586:   fun get_cas thy = Data.get thy
walther@59896:   fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59894:     type T = Probl_Def.store;
walther@59894:     val empty = [Probl_Def.empty_store];
wneuper@59586:     val extend = I;
walther@59897:     val merge = Store.merge;
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 *)
walther@59904:                 (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
walther@59897:                   rev pblID |> Store.insert pblID pbt);
wneuper@59586:         in Data.map (fold add_pbt pbts) thy end;
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59895:     type T = Meth_Def.store;
walther@59895:     val empty = [Meth_Def.empty_store];
wneuper@59586:     val extend = I;
walther@59897:     val merge = Store.merge;
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) =
walther@59904:                 (if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
walther@59897:                   Store.insert metID met metID);
wneuper@59586:         in Data.map (fold add_met mets) thy end;
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
walther@59917:     type T = (Thy_Write.thydata Store.node) list;
wneuper@59586:     val empty = [];
wneuper@59586:     val extend = I;
walther@59897:     val merge = Store.merge; (* 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
walther@59917:     fun add_the (thydata, theID) = Thy_Write.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
walther@59897:           val hthm = Store.get (Data.get thy) theID theID
walther@59917:           val hthm' = Thy_Write.update_hthm hthm fillpats
wneuper@59586:             handle ERROR _ =>
wneuper@59586:               error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
walther@59897:         in Store.update 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@59867: fun assoc_rls (rls' : Rule_Set.id) =
walther@59879:   case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
wneuper@59586:     SOME (_, rls) => rls
walther@59887:   | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
wneuper@59586:     "TODO exception hierarchy needs to be established.")
wneuper@59586: 
walther@59867: fun assoc_rls' thy (rls' : Rule_Set.id) =
wneuper@59586:   case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
wneuper@59586:     SOME (_, rls) => rls
walther@59887:   | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\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@59852:   [("empty", (Context.theory_name @{theory}, Rule_Set.empty)), 
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
walther@59917:   [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
wneuper@59586:     mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
walther@59917:   (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
wneuper@59586:     mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
walther@59917:   (Thy_Write.Html {guh = Thy_Write.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@59851: fun short_string_of_rls Rule_Set.Empty = "Erls"
walther@59851:   | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
wneuper@59586:     "Rls {#calc = " ^ string_of_int (length calc) ^
wneuper@59586:     ", #rules = " ^ string_of_int (length rules) ^ ", ..."
walther@59878:   | short_string_of_rls (Rule_Set.Sequence {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@59852: fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc)  = "(" ^ id ^ ", (" ^ c ^ ", fn))";
wneuper@59586: 
walther@59846: (* we avoid term_to_string''' defined later *)
walther@59896: fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
walther@59846:   "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
walther@59902:   (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.to_string s ^ ")";
wneuper@59586: 
wneuper@59586: fun count_kestore_ptyps [] = 0
walther@59897:   | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
wneuper@59586:       1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
walther@59897: fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
walther@59888:       (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
walther@59894: val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
walther@59897: fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
walther@59894: fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
wneuper@59586: fun sort_kestore_ptyp' _ [] = []
walther@59897:   | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
walther@59897:      ((Store.Node (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: 
walther@59895: fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
walther@59897: fun check_kestore_met (mp: Meth_Def.T Store.node) =
wneuper@59586:       check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
walther@59895: fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
wneuper@59586: val sort_kestore_met = sort_kestore_ptyp' met_ord;
wneuper@59586: 
walther@59917: fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
wneuper@59586: fun write_thes thydata_list =
wneuper@59586:   thydata_list 
walther@59917:     |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.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




