1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 12:22:37 2020 +0200
1.3 @@ -0,0 +1,271 @@
1.4 +(* Title: src/Tools/isac/Know_Store.thy
1.5 + Author: Mathias Lehnfeld
1.6 +
1.7 +The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
1.8 +they also include minimal code required for other "xxxxx-def.sml" files.
1.9 +These files have companion files "xxxxx.sml" with all further code,
1.10 +located at appropriate positions in the file structure.
1.11 +
1.12 +The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
1.13 +appropriate use of polymorphic high order functions.
1.14 +*)
1.15 +
1.16 +theory Know_Store imports Complex_Main
1.17 +
1.18 +begin
1.19 +ML_file libraryC.sml
1.20 +ML_file theoryC.sml
1.21 +ML_file unparseC.sml
1.22 +ML_file "rule-def.sml"
1.23 +ML_file "thmC-def.sml"
1.24 +ML_file "exec-def.sml" (*rename identifiers by use of struct.id*)
1.25 +ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
1.26 +ML_file rule.sml
1.27 +ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
1.28 +ML_file "rule-set.sml"
1.29 +
1.30 +ML_file "celem-0.sml" (*survey Celem.*)
1.31 +ML_file "celem-1.sml" (*datatype 'a ptyp*)
1.32 +ML_file "celem-2.sml" (*guh*)
1.33 +ML_file "celem-3.sml" (*spec*)
1.34 +ML_file "celem-4.sml" (*pat*)
1.35 +ML_file "celem-5.sml" (*ptyps*)
1.36 +ML_file "celem-6.sml" (*mets*)
1.37 +ML_file "celem-7.sml" (*cas_elem*)
1.38 +ML_file "celem-8.sml" (*thydata*)
1.39 +ML_file "celem-91.sml" (*check_guhs_unique*)
1.40 +ML_file "celem-92.sml" (**)
1.41 +ML_file "celem-93.sml" (**)
1.42 +
1.43 +ML_file calcelems.sml
1.44 +ML_file tracing.sml
1.45 +ML \<open>
1.46 +\<close> ML \<open>
1.47 +\<close> ML \<open>
1.48 +\<close>
1.49 +section \<open>Knowledge elements for problems and methods\<close>
1.50 +ML \<open>
1.51 +(* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
1.52 + In the front-end Knowledge comprises theories, problems and methods.
1.53 + Elements of problems and methods are defined in theories alongside
1.54 + the development of respective language elements.
1.55 + However, the structure of methods and problems is independent from theories'
1.56 + deductive structure. Thus respective structures are built in Build_Thydata.thy.
1.57 +
1.58 + Most elements of problems and methods are implemented in "Knowledge/", but some
1.59 + of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
1.60 + location in the directory structure.
1.61 +
1.62 + get_* retrieves all * of the respective theory PLUS of all ancestor theories.
1.63 +*)
1.64 +signature KESTORE_ELEMS =
1.65 +sig
1.66 + val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
1.67 + val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
1.68 + val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
1.69 + val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
1.70 + val get_cas: theory -> Celem.cas_elem list
1.71 + val add_cas: Celem.cas_elem list -> theory -> theory
1.72 + val get_ptyps: theory -> Celem.ptyps
1.73 + val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
1.74 + val get_mets: theory -> Celem.mets
1.75 + val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
1.76 + val get_thes: theory -> (Celem.thydata Celem1.ptyp) list
1.77 + val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.78 + val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.79 + val get_ref_thy: unit -> theory
1.80 + val set_ref_thy: theory -> unit
1.81 +end;
1.82 +
1.83 +structure KEStore_Elems: KESTORE_ELEMS =
1.84 +struct
1.85 + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
1.86 +
1.87 + structure Data = Theory_Data (
1.88 + type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
1.89 + val empty = [];
1.90 + val extend = I;
1.91 + val merge = Rule_Set.to_kestore;
1.92 + );
1.93 + fun get_rlss thy = Data.get thy
1.94 + fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
1.95 +
1.96 + structure Data = Theory_Data (
1.97 + type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
1.98 + val empty = [];
1.99 + val extend = I;
1.100 + val merge = merge Exec_Def.calc_eq;
1.101 + );
1.102 + fun get_calcs thy = Data.get thy
1.103 + fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
1.104 +
1.105 + structure Data = Theory_Data (
1.106 + type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
1.107 + val empty = [];
1.108 + val extend = I;
1.109 + val merge = merge Celem.cas_eq;
1.110 + );
1.111 + fun get_cas thy = Data.get thy
1.112 + fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
1.113 +
1.114 + structure Data = Theory_Data (
1.115 + type T = Celem.ptyps;
1.116 + val empty = [Celem.e_Ptyp];
1.117 + val extend = I;
1.118 + val merge = Celem.merge_ptyps;
1.119 + );
1.120 + fun get_ptyps thy = Data.get thy;
1.121 + fun add_pbts pbts thy = let
1.122 + fun add_pbt (pbt as {guh,...}, pblID) =
1.123 + (* the pblID has the leaf-element as first; better readability achieved *)
1.124 + (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
1.125 + rev pblID |> Celem.insrt pblID pbt);
1.126 + in Data.map (fold add_pbt pbts) thy end;
1.127 +
1.128 + structure Data = Theory_Data (
1.129 + type T = Celem.mets;
1.130 + val empty = [Celem.e_Mets];
1.131 + val extend = I;
1.132 + val merge = Celem.merge_ptyps;
1.133 + );
1.134 + val get_mets = Data.get;
1.135 + fun add_mets mets thy = let
1.136 + fun add_met (met as {guh,...}, metID) =
1.137 + (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
1.138 + Celem.insrt metID met metID);
1.139 + in Data.map (fold add_met mets) thy end;
1.140 +
1.141 + structure Data = Theory_Data (
1.142 + type T = (Celem.thydata Celem1.ptyp) list;
1.143 + val empty = [];
1.144 + val extend = I;
1.145 + val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
1.146 + );
1.147 + fun get_thes thy = Data.get thy
1.148 + fun add_thes thes thy = let
1.149 + fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
1.150 + in Data.map (fold add_the thes) thy end;
1.151 + fun insert_fillpats fis thy =
1.152 + let
1.153 + fun update_elem (theID, fillpats) =
1.154 + let
1.155 + val hthm = Celem.get_py (Data.get thy) theID theID
1.156 + val hthm' = Celem.update_hthm hthm fillpats
1.157 + handle ERROR _ =>
1.158 + error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.159 + in Celem.update_ptyps theID theID hthm' end
1.160 + in Data.map (fold update_elem fis) thy end
1.161 +
1.162 + val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.163 + fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
1.164 + fun get_ref_thy () = Synchronized.value cur_thy;
1.165 +end;
1.166 +\<close>
1.167 +
1.168 +section \<open>Re-use existing access functions for knowledge elements\<close>
1.169 +text \<open>
1.170 + The independence of problems' and methods' structure enforces the accesse
1.171 + functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
1.172 +\<close>
1.173 +ML \<open>
1.174 +val get_ref_thy = KEStore_Elems.get_ref_thy;
1.175 +
1.176 +fun assoc_rls (rls' : Rule_Set.id) =
1.177 + case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
1.178 + SOME (_, rls) => rls
1.179 + | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
1.180 + "TODO exception hierarchy needs to be established.")
1.181 +
1.182 +fun assoc_rls' thy (rls' : Rule_Set.id) =
1.183 + case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
1.184 + SOME (_, rls) => rls
1.185 + | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
1.186 + "TODO exception hierarchy needs to be established.")
1.187 +
1.188 +fun assoc_calc thy calID = let
1.189 + fun ass ([], key) =
1.190 + error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
1.191 + | ass ((calc, (keyi, _)) :: pairs, key) =
1.192 + if key = keyi then calc else ass (pairs, key);
1.193 + in ass (thy |> KEStore_Elems.get_calcs, calID) end;
1.194 +
1.195 +fun assoc_calc' thy key = let
1.196 + fun ass ([], key') =
1.197 + error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
1.198 + | ass ((all as (keyi, _)) :: pairs, key') =
1.199 + if key' = keyi then all else ass (pairs, key');
1.200 + in ass (KEStore_Elems.get_calcs thy, key) end;
1.201 +
1.202 +fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
1.203 +
1.204 +fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
1.205 +fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
1.206 +fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
1.207 +\<close>
1.208 +setup \<open>KEStore_Elems.add_rlss
1.209 + [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
1.210 + ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
1.211 +
1.212 +section \<open>determine sequence of main parts in thehier\<close>
1.213 +setup \<open>
1.214 +KEStore_Elems.add_thes
1.215 + [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
1.216 + mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
1.217 + (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
1.218 + mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
1.219 + (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
1.220 + mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
1.221 +\<close>
1.222 +
1.223 +section \<open>Functions for checking KEStore_Elems\<close>
1.224 +ML \<open>
1.225 +fun short_string_of_rls Rule_Set.Empty = "Erls"
1.226 + | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
1.227 + "Rls {#calc = " ^ string_of_int (length calc) ^
1.228 + ", #rules = " ^ string_of_int (length rules) ^ ", ..."
1.229 + | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
1.230 + "Seq {#calc = " ^ string_of_int (length calc) ^
1.231 + ", #rules = " ^ string_of_int (length rules) ^ ", ..."
1.232 + | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
1.233 +fun check_kestore_rls (rls', (thyID, rls)) =
1.234 + "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
1.235 +
1.236 +fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
1.237 +
1.238 +(* we avoid term_to_string''' defined later *)
1.239 +fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
1.240 + "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
1.241 + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
1.242 +
1.243 +fun count_kestore_ptyps [] = 0
1.244 + | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
1.245 + 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.246 +fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.247 + (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
1.248 +val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
1.249 +fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.250 +fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
1.251 +fun sort_kestore_ptyp' _ [] = []
1.252 + | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
1.253 + ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.254 + :: sort_kestore_ptyp' ordfun ps');
1.255 +val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.256 +
1.257 +fun metguh2str ({guh,...} : Celem.met) = guh : string;
1.258 +fun check_kestore_met (mp: Celem.met Celem1.ptyp) =
1.259 + check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.260 +fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
1.261 +val sort_kestore_met = sort_kestore_ptyp' met_ord;
1.262 +
1.263 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
1.264 +fun write_thes thydata_list =
1.265 + thydata_list
1.266 + |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
1.267 + |> map pair2str
1.268 + |> map writeln
1.269 +\<close>
1.270 +ML \<open>
1.271 +\<close> ML \<open>
1.272 +\<close> ML \<open>
1.273 +\<close>
1.274 +end