
diff -r 106e7d8723ca -r 4616b145b1cd src/Tools/isac/BaseDefinitions/Know_Store.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 12:22:37 2020 +0200
@@ -0,0 +1,271 @@
+(*  Title:      src/Tools/isac/Know_Store.thy
+    Author:     Mathias Lehnfeld
+
+The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
+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 Know_Store 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 "Know_Store" 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 "Know_Store.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 Celem1.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 Celem1.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 Know_Store.\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 Know_Store.\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 ((Celem1.Ptyp (_, _, ps)) :: ps') =
+      1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
+fun check_kestore_ptyp' strfun (Celem1.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 ((Celem1.Ptyp (s1, _, _)), (Celem1.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 ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
+     ((Celem1.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 Celem1.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




