1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 15:51:31 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 16:17:27 2020 +0200
1.3 @@ -1,6 +1,11 @@
1.4 (* Title: src/Tools/isac/Know_Store.thy
1.5 Author: Mathias Lehnfeld
1.6
1.7 +Calc work on Problem employing Method; both are collected in a respective Store;
1.8 +The collections' structure is independent from the dependency graph of Isabelle's theories
1.9 +in Knowledge.
1.10 +Store is also used by Thy_Html, required for Isac's Java front end, irrelevant for PIDE.
1.11 +
1.12 The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
1.13 they also include minimal code required for other "xxxxx-def.sml" files.
1.14 These files have companion files "xxxxx.sml" with all further code,
1.15 @@ -67,7 +72,7 @@
1.16 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
1.17 val get_mets: theory -> Celem6.mets
1.18 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
1.19 - val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list
1.20 + val get_thes: theory -> (Celem8.thydata Store.ptyp) list
1.21 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.22 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.23 val get_ref_thy: unit -> theory
1.24 @@ -109,34 +114,34 @@
1.25 type T = Celem5.ptyps;
1.26 val empty = [Celem5.e_Ptyp];
1.27 val extend = I;
1.28 - val merge = Celem1.merge_ptyps;
1.29 + val merge = Store.merge_ptyps;
1.30 );
1.31 fun get_ptyps thy = Data.get thy;
1.32 fun add_pbts pbts thy = let
1.33 fun add_pbt (pbt as {guh,...}, pblID) =
1.34 (* the pblID has the leaf-element as first; better readability achieved *)
1.35 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
1.36 - rev pblID |> Celem1.insrt pblID pbt);
1.37 + rev pblID |> Store.insrt pblID pbt);
1.38 in Data.map (fold add_pbt pbts) thy end;
1.39
1.40 structure Data = Theory_Data (
1.41 type T = Celem6.mets;
1.42 val empty = [Celem6.e_Mets];
1.43 val extend = I;
1.44 - val merge = Celem1.merge_ptyps;
1.45 + val merge = Store.merge_ptyps;
1.46 );
1.47 val get_mets = Data.get;
1.48 fun add_mets mets thy = let
1.49 fun add_met (met as {guh,...}, metID) =
1.50 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
1.51 - Celem1.insrt metID met metID);
1.52 + Store.insrt metID met metID);
1.53 in Data.map (fold add_met mets) thy end;
1.54
1.55 structure Data = Theory_Data (
1.56 - type T = (Celem8.thydata Celem1.ptyp) list;
1.57 + type T = (Celem8.thydata Store.ptyp) list;
1.58 val empty = [];
1.59 val extend = I;
1.60 - val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
1.61 + val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
1.62 );
1.63 fun get_thes thy = Data.get thy
1.64 fun add_thes thes thy = let
1.65 @@ -146,11 +151,11 @@
1.66 let
1.67 fun update_elem (theID, fillpats) =
1.68 let
1.69 - val hthm = Celem1.get_py (Data.get thy) theID theID
1.70 + val hthm = Store.get_py (Data.get thy) theID theID
1.71 val hthm' = Celem8.update_hthm hthm fillpats
1.72 handle ERROR _ =>
1.73 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.74 - in Celem1.update_ptyps theID theID hthm' end
1.75 + in Store.update_ptyps theID theID hthm' end
1.76 in Data.map (fold update_elem fis) thy end
1.77
1.78 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.79 @@ -235,21 +240,21 @@
1.80 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
1.81
1.82 fun count_kestore_ptyps [] = 0
1.83 - | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
1.84 + | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
1.85 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.86 -fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.87 +fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.88 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
1.89 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
1.90 -fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.91 +fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.92 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
1.93 fun sort_kestore_ptyp' _ [] = []
1.94 - | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
1.95 - ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.96 + | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
1.97 + ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.98 :: sort_kestore_ptyp' ordfun ps');
1.99 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.100
1.101 fun metguh2str ({guh,...} : Celem6.met) = guh : string;
1.102 -fun check_kestore_met (mp: Celem6.met Celem1.ptyp) =
1.103 +fun check_kestore_met (mp: Celem6.met Store.ptyp) =
1.104 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.105 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
1.106 val sort_kestore_met = sort_kestore_ptyp' met_ord;