walther@59887: (*  Title:      src/Tools/isac/Know_Store.thy
wneuper@59586:     Author:     Mathias Lehnfeld
walther@59871: 
walther@60154: Calc work on Problem employing MethodC; 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: 
wenzelm@60286: theory Know_Store
wenzelm@60286:   imports Complex_Main
wenzelm@60313:   keywords "rule_set_knowledge" "calculation" :: thy_decl
wenzelm@60223: begin
wneuper@59586: 
wenzelm@60223: setup \<open>
wenzelm@60223:   ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
wenzelm@60223:     (fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
wenzelm@60223: \<close>
wenzelm@60223: 
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@59985: ML_file "references-def.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@60505: ML_file "formalise.sml"
Walther@60505: ML_file "example.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@60509:   val get_rew_ord: theory -> Rewrite_Ord.T list
Walther@60509:   val add_rew_ord: Rewrite_Ord.T list -> theory -> theory
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@60495:   val get_pbls: theory -> Probl_Def.store
Walther@60502:   val add_pbls: Proof.context -> (Probl_Def.T * References_Def.id) list -> theory -> theory
walther@59895:   val get_mets: theory -> Meth_Def.store
Walther@60502:   val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
Walther@60505:   val get_expls: theory -> Example.store
Walther@60505:   val add_expls: (Example.T * Store.key) 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
Walther@60508: end;
wneuper@59586: 
Walther@60506: 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@60506:     type T = (string * (LibraryC.subst -> term * term -> bool)) list;
Walther@60506:     val empty = [];
Walther@60506:     val extend = I;
Walther@60506:     val merge = merge Rewrite_Ord.equal;
Walther@60506:     );  
Walther@60506:   fun get_rew_ord thy = Data.get thy
Walther@60506:   fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)
Walther@60506: 
Walther@60506:   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@59985:     type T = (term * (References_Def.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:     );
Walther@60495:   fun get_pbls thy = Data.get thy;
Walther@60502:   fun add_pbls ctxt pbts thy =
Walther@60502:     let
Walther@60502:       fun add_pbt (pbt as {guh,...}, pblID) =
Walther@60502:         (* the pblID has the leaf-element as first; better readability achieved *)
Walther@60502:         (if (Config.get ctxt check_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
Walther@60502:           rev pblID |> Store.insert pblID pbt);
Walther@60502:     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;
Walther@60502:   fun add_mets ctxt mets thy =
Walther@60502:     let
Walther@60502:       fun add_met (met as {guh,...}, metID) =
Walther@60502:         (if (Config.get ctxt check_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
Walther@60502:           Store.insert metID met metID);
Walther@60502:     in Data.map (fold add_met mets) thy end;
wneuper@59586: 
wneuper@59586:   structure Data = Theory_Data (
Walther@60505:     type T = Example.store;
Walther@60505:     val empty = [Example.empty_store];
Walther@60505:     val extend = I;
Walther@60505:     val merge = Store.merge;
Walther@60505:     );
Walther@60505:   val get_expls = Data.get;
Walther@60505:   fun add_expls expls thy =
Walther@60505:     let
Walther@60505:       fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
Walther@60505:     in Data.map (fold add_expl expls) thy end;
Walther@60505: 
Walther@60505:   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 _ =>
walther@59962:               raise 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;
Walther@60506: (**)end(**);
wneuper@59586: \<close>
wneuper@59586: 
wenzelm@60286: 
wenzelm@60286: subsection \<open>Isar command syntax\<close>
wenzelm@60286: 
wenzelm@60286: ML \<open>
wenzelm@60286: local
wenzelm@60286: 
wenzelm@60286: val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
wenzelm@60286: 
wenzelm@60286: val ml = ML_Lex.read;
wenzelm@60286: 
wenzelm@60286: fun ml_rule thy (name, source) =
wenzelm@60286:   ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
wenzelm@60286:   ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
wenzelm@60286:   ML_Lex.read_source source @ ml "))";
wenzelm@60286: 
wenzelm@60286: fun ml_rules thy args =
wenzelm@60286:   ml "Theory.setup (KEStore_Elems.add_rlss [" @
wenzelm@60286:     flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
wenzelm@60286: 
wenzelm@60286: val _ =
wenzelm@60289:   Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
wenzelm@60286:     (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
wenzelm@60286:       thy |> Context.theory_map
wenzelm@60286:         (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
wenzelm@60286: 
wenzelm@60313: val calc_name =
wenzelm@60313:   Parse.name -- (\<^keyword>\<open>(\<close> |-- Parse.const --| \<^keyword>\<open>)\<close>) ||
wenzelm@60313:   Scan.ahead Parse.name -- Parse.const;
wenzelm@60313: 
wenzelm@60313: val _ =
wenzelm@60313:   Outer_Syntax.command \<^command_keyword>\<open>calculation\<close>
wenzelm@60313:     "prepare ISAC calculation and register it to Knowledge Store"
wenzelm@60313:     (calc_name -- (\<^keyword>\<open>=\<close> |-- Parse.!!! Parse.ML_source) >> (fn ((calcID, const), source) =>
wenzelm@60313:       Toplevel.theory (fn thy =>
wenzelm@60313:         let
wenzelm@60313:           val ctxt = Proof_Context.init_global thy;
wenzelm@60313:           val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt const;
wenzelm@60314:           val set_data =
wenzelm@60313:             ML_Context.expression (Input.pos_of source)
wenzelm@60313:               (ml "Theory.setup (Eval_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
wenzelm@60313:             |> Context.theory_map;
wenzelm@60314:           val eval = Eval_Def.the_data (set_data thy);
wenzelm@60313:         in KEStore_Elems.add_calcs [(calcID, (c, eval))] thy end)))
wenzelm@60313: 
wenzelm@60286: in end;
wenzelm@60286: \<close>
wenzelm@60286: 
wenzelm@60286: 
wneuper@59586: section \<open>Re-use existing access functions for knowledge elements\<close>
wneuper@59586: text \<open>
Walther@60508:   The independence of problems' and methods' structure from theory dependency structure
Walther@60508:   enforces the access functions to use "Isac_Knowledge",
Walther@60508:   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@60506: fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
Walther@60506:   | assoc' ((keyi, xi) :: pairs, key) =
Walther@60506:     if key = keyi then SOME xi else assoc' (pairs, key);
Walther@60506: fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
Walther@60506:   handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
Walther@60506: 
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) =
walther@59962:           raise 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') =
walther@59962:           raise 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: 
Walther@60495: fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
wneuper@59586: fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
wneuper@59586: fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
Walther@60505: fun get_expls () = get_ref_thy () |> KEStore_Elems.get_expls;
wneuper@59586: \<close>
wenzelm@60286: 
wenzelm@60289: rule_set_knowledge
wenzelm@60286:   empty = \<open>Rule_Set.empty\<close> and
wenzelm@60286:   e_rrls = \<open>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@59985:   (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.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