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