1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Sun Apr 19 11:07:02 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Sun Apr 19 12:22:37 2020 +0200
1.3 @@ -2,9 +2,9 @@
1.4 Author: Walther Neuper 190823
1.5 (c) due to copyright terms
1.6
1.7 -KEStore holds Theory_Data (problems, methods, etc) and requires respective definitions.
1.8 +Know_Store holds Theory_Data (problems, methods, etc) and requires respective definitions.
1.9 *)
1.10 -theory BaseDefinitions imports KEStore
1.11 +theory BaseDefinitions imports Know_Store
1.12 begin
1.13 ML_file termC.sml
1.14 ML_file contextC.sml
2.1 --- a/src/Tools/isac/BaseDefinitions/KEStore.thy Sun Apr 19 11:07:02 2020 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,271 +0,0 @@
2.4 -(* Title: src/Tools/isac/KEStore.thy
2.5 - Author: Mathias Lehnfeld
2.6 -
2.7 -The files (in "xxxxx-def.sml") contain definitions required for KEStore;
2.8 -they also include minimal code required for other "xxxxx-def.sml" files.
2.9 -These files have companion files "xxxxx.sml" with all further code,
2.10 -located at appropriate positions in the file structure.
2.11 -
2.12 -The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
2.13 -appropriate use of polymorphic high order functions.
2.14 -*)
2.15 -
2.16 -theory KEStore imports Complex_Main
2.17 -
2.18 -begin
2.19 -ML_file libraryC.sml
2.20 -ML_file theoryC.sml
2.21 -ML_file unparseC.sml
2.22 -ML_file "rule-def.sml"
2.23 -ML_file "thmC-def.sml"
2.24 -ML_file "exec-def.sml" (*rename identifiers by use of struct.id*)
2.25 -ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
2.26 -ML_file rule.sml
2.27 -ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
2.28 -ML_file "rule-set.sml"
2.29 -
2.30 -ML_file "celem-0.sml" (*survey Celem.*)
2.31 -ML_file "celem-1.sml" (*datatype 'a ptyp*)
2.32 -ML_file "celem-2.sml" (*guh*)
2.33 -ML_file "celem-3.sml" (*spec*)
2.34 -ML_file "celem-4.sml" (*pat*)
2.35 -ML_file "celem-5.sml" (*ptyps*)
2.36 -ML_file "celem-6.sml" (*mets*)
2.37 -ML_file "celem-7.sml" (*cas_elem*)
2.38 -ML_file "celem-8.sml" (*thydata*)
2.39 -ML_file "celem-91.sml" (*check_guhs_unique*)
2.40 -ML_file "celem-92.sml" (**)
2.41 -ML_file "celem-93.sml" (**)
2.42 -
2.43 -ML_file calcelems.sml
2.44 -ML_file tracing.sml
2.45 -ML \<open>
2.46 -\<close> ML \<open>
2.47 -\<close> ML \<open>
2.48 -\<close>
2.49 -section \<open>Knowledge elements for problems and methods\<close>
2.50 -ML \<open>
2.51 -(* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
2.52 - In the front-end Knowledge comprises theories, problems and methods.
2.53 - Elements of problems and methods are defined in theories alongside
2.54 - the development of respective language elements.
2.55 - However, the structure of methods and problems is independent from theories'
2.56 - deductive structure. Thus respective structures are built in Build_Thydata.thy.
2.57 -
2.58 - Most elements of problems and methods are implemented in "Knowledge/", but some
2.59 - of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
2.60 - location in the directory structure.
2.61 -
2.62 - get_* retrieves all * of the respective theory PLUS of all ancestor theories.
2.63 -*)
2.64 -signature KESTORE_ELEMS =
2.65 -sig
2.66 - val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
2.67 - val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
2.68 - val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
2.69 - val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
2.70 - val get_cas: theory -> Celem.cas_elem list
2.71 - val add_cas: Celem.cas_elem list -> theory -> theory
2.72 - val get_ptyps: theory -> Celem.ptyps
2.73 - val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
2.74 - val get_mets: theory -> Celem.mets
2.75 - val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
2.76 - val get_thes: theory -> (Celem.thydata Celem.ptyp) list
2.77 - val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
2.78 - val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
2.79 - val get_ref_thy: unit -> theory
2.80 - val set_ref_thy: theory -> unit
2.81 -end;
2.82 -
2.83 -structure KEStore_Elems: KESTORE_ELEMS =
2.84 -struct
2.85 - fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
2.86 -
2.87 - structure Data = Theory_Data (
2.88 - type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
2.89 - val empty = [];
2.90 - val extend = I;
2.91 - val merge = Rule_Set.to_kestore;
2.92 - );
2.93 - fun get_rlss thy = Data.get thy
2.94 - fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
2.95 -
2.96 - structure Data = Theory_Data (
2.97 - type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
2.98 - val empty = [];
2.99 - val extend = I;
2.100 - val merge = merge Exec_Def.calc_eq;
2.101 - );
2.102 - fun get_calcs thy = Data.get thy
2.103 - fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
2.104 -
2.105 - structure Data = Theory_Data (
2.106 - type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
2.107 - val empty = [];
2.108 - val extend = I;
2.109 - val merge = merge Celem.cas_eq;
2.110 - );
2.111 - fun get_cas thy = Data.get thy
2.112 - fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
2.113 -
2.114 - structure Data = Theory_Data (
2.115 - type T = Celem.ptyps;
2.116 - val empty = [Celem.e_Ptyp];
2.117 - val extend = I;
2.118 - val merge = Celem.merge_ptyps;
2.119 - );
2.120 - fun get_ptyps thy = Data.get thy;
2.121 - fun add_pbts pbts thy = let
2.122 - fun add_pbt (pbt as {guh,...}, pblID) =
2.123 - (* the pblID has the leaf-element as first; better readability achieved *)
2.124 - (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
2.125 - rev pblID |> Celem.insrt pblID pbt);
2.126 - in Data.map (fold add_pbt pbts) thy end;
2.127 -
2.128 - structure Data = Theory_Data (
2.129 - type T = Celem.mets;
2.130 - val empty = [Celem.e_Mets];
2.131 - val extend = I;
2.132 - val merge = Celem.merge_ptyps;
2.133 - );
2.134 - val get_mets = Data.get;
2.135 - fun add_mets mets thy = let
2.136 - fun add_met (met as {guh,...}, metID) =
2.137 - (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
2.138 - Celem.insrt metID met metID);
2.139 - in Data.map (fold add_met mets) thy end;
2.140 -
2.141 - structure Data = Theory_Data (
2.142 - type T = (Celem.thydata Celem.ptyp) list;
2.143 - val empty = [];
2.144 - val extend = I;
2.145 - val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
2.146 - );
2.147 - fun get_thes thy = Data.get thy
2.148 - fun add_thes thes thy = let
2.149 - fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
2.150 - in Data.map (fold add_the thes) thy end;
2.151 - fun insert_fillpats fis thy =
2.152 - let
2.153 - fun update_elem (theID, fillpats) =
2.154 - let
2.155 - val hthm = Celem.get_py (Data.get thy) theID theID
2.156 - val hthm' = Celem.update_hthm hthm fillpats
2.157 - handle ERROR _ =>
2.158 - error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
2.159 - in Celem.update_ptyps theID theID hthm' end
2.160 - in Data.map (fold update_elem fis) thy end
2.161 -
2.162 - val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
2.163 - fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
2.164 - fun get_ref_thy () = Synchronized.value cur_thy;
2.165 -end;
2.166 -\<close>
2.167 -
2.168 -section \<open>Re-use existing access functions for knowledge elements\<close>
2.169 -text \<open>
2.170 - The independence of problems' and methods' structure enforces the accesse
2.171 - functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
2.172 -\<close>
2.173 -ML \<open>
2.174 -val get_ref_thy = KEStore_Elems.get_ref_thy;
2.175 -
2.176 -fun assoc_rls (rls' : Rule_Set.id) =
2.177 - case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
2.178 - SOME (_, rls) => rls
2.179 - | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
2.180 - "TODO exception hierarchy needs to be established.")
2.181 -
2.182 -fun assoc_rls' thy (rls' : Rule_Set.id) =
2.183 - case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
2.184 - SOME (_, rls) => rls
2.185 - | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
2.186 - "TODO exception hierarchy needs to be established.")
2.187 -
2.188 -fun assoc_calc thy calID = let
2.189 - fun ass ([], key) =
2.190 - error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
2.191 - | ass ((calc, (keyi, _)) :: pairs, key) =
2.192 - if key = keyi then calc else ass (pairs, key);
2.193 - in ass (thy |> KEStore_Elems.get_calcs, calID) end;
2.194 -
2.195 -fun assoc_calc' thy key = let
2.196 - fun ass ([], key') =
2.197 - error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
2.198 - | ass ((all as (keyi, _)) :: pairs, key') =
2.199 - if key' = keyi then all else ass (pairs, key');
2.200 - in ass (KEStore_Elems.get_calcs thy, key) end;
2.201 -
2.202 -fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
2.203 -
2.204 -fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
2.205 -fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
2.206 -fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
2.207 -\<close>
2.208 -setup \<open>KEStore_Elems.add_rlss
2.209 - [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
2.210 - ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
2.211 -
2.212 -section \<open>determine sequence of main parts in thehier\<close>
2.213 -setup \<open>
2.214 -KEStore_Elems.add_thes
2.215 - [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
2.216 - mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
2.217 - (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
2.218 - mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
2.219 - (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
2.220 - mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
2.221 -\<close>
2.222 -
2.223 -section \<open>Functions for checking KEStore_Elems\<close>
2.224 -ML \<open>
2.225 -fun short_string_of_rls Rule_Set.Empty = "Erls"
2.226 - | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
2.227 - "Rls {#calc = " ^ string_of_int (length calc) ^
2.228 - ", #rules = " ^ string_of_int (length rules) ^ ", ..."
2.229 - | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
2.230 - "Seq {#calc = " ^ string_of_int (length calc) ^
2.231 - ", #rules = " ^ string_of_int (length rules) ^ ", ..."
2.232 - | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
2.233 -fun check_kestore_rls (rls', (thyID, rls)) =
2.234 - "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
2.235 -
2.236 -fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
2.237 -
2.238 -(* we avoid term_to_string''' defined later *)
2.239 -fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
2.240 - "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
2.241 - (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
2.242 -
2.243 -fun count_kestore_ptyps [] = 0
2.244 - | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') =
2.245 - 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
2.246 -fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
2.247 - (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
2.248 -val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
2.249 -fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2);
2.250 -fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
2.251 -fun sort_kestore_ptyp' _ [] = []
2.252 - | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') =
2.253 - ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
2.254 - :: sort_kestore_ptyp' ordfun ps');
2.255 -val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
2.256 -
2.257 -fun metguh2str ({guh,...} : Celem.met) = guh : string;
2.258 -fun check_kestore_met (mp: Celem.met Celem.ptyp) =
2.259 - check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
2.260 -fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
2.261 -val sort_kestore_met = sort_kestore_ptyp' met_ord;
2.262 -
2.263 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
2.264 -fun write_thes thydata_list =
2.265 - thydata_list
2.266 - |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
2.267 - |> map pair2str
2.268 - |> map writeln
2.269 -\<close>
2.270 -ML \<open>
2.271 -\<close> ML \<open>
2.272 -\<close> ML \<open>
2.273 -\<close>
2.274 -end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 12:22:37 2020 +0200
3.3 @@ -0,0 +1,271 @@
3.4 +(* Title: src/Tools/isac/Know_Store.thy
3.5 + Author: Mathias Lehnfeld
3.6 +
3.7 +The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
3.8 +they also include minimal code required for other "xxxxx-def.sml" files.
3.9 +These files have companion files "xxxxx.sml" with all further code,
3.10 +located at appropriate positions in the file structure.
3.11 +
3.12 +The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
3.13 +appropriate use of polymorphic high order functions.
3.14 +*)
3.15 +
3.16 +theory Know_Store imports Complex_Main
3.17 +
3.18 +begin
3.19 +ML_file libraryC.sml
3.20 +ML_file theoryC.sml
3.21 +ML_file unparseC.sml
3.22 +ML_file "rule-def.sml"
3.23 +ML_file "thmC-def.sml"
3.24 +ML_file "exec-def.sml" (*rename identifiers by use of struct.id*)
3.25 +ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
3.26 +ML_file rule.sml
3.27 +ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
3.28 +ML_file "rule-set.sml"
3.29 +
3.30 +ML_file "celem-0.sml" (*survey Celem.*)
3.31 +ML_file "celem-1.sml" (*datatype 'a ptyp*)
3.32 +ML_file "celem-2.sml" (*guh*)
3.33 +ML_file "celem-3.sml" (*spec*)
3.34 +ML_file "celem-4.sml" (*pat*)
3.35 +ML_file "celem-5.sml" (*ptyps*)
3.36 +ML_file "celem-6.sml" (*mets*)
3.37 +ML_file "celem-7.sml" (*cas_elem*)
3.38 +ML_file "celem-8.sml" (*thydata*)
3.39 +ML_file "celem-91.sml" (*check_guhs_unique*)
3.40 +ML_file "celem-92.sml" (**)
3.41 +ML_file "celem-93.sml" (**)
3.42 +
3.43 +ML_file calcelems.sml
3.44 +ML_file tracing.sml
3.45 +ML \<open>
3.46 +\<close> ML \<open>
3.47 +\<close> ML \<open>
3.48 +\<close>
3.49 +section \<open>Knowledge elements for problems and methods\<close>
3.50 +ML \<open>
3.51 +(* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
3.52 + In the front-end Knowledge comprises theories, problems and methods.
3.53 + Elements of problems and methods are defined in theories alongside
3.54 + the development of respective language elements.
3.55 + However, the structure of methods and problems is independent from theories'
3.56 + deductive structure. Thus respective structures are built in Build_Thydata.thy.
3.57 +
3.58 + Most elements of problems and methods are implemented in "Knowledge/", but some
3.59 + of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
3.60 + location in the directory structure.
3.61 +
3.62 + get_* retrieves all * of the respective theory PLUS of all ancestor theories.
3.63 +*)
3.64 +signature KESTORE_ELEMS =
3.65 +sig
3.66 + val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
3.67 + val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
3.68 + val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
3.69 + val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
3.70 + val get_cas: theory -> Celem.cas_elem list
3.71 + val add_cas: Celem.cas_elem list -> theory -> theory
3.72 + val get_ptyps: theory -> Celem.ptyps
3.73 + val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
3.74 + val get_mets: theory -> Celem.mets
3.75 + val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
3.76 + val get_thes: theory -> (Celem.thydata Celem1.ptyp) list
3.77 + val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
3.78 + val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
3.79 + val get_ref_thy: unit -> theory
3.80 + val set_ref_thy: theory -> unit
3.81 +end;
3.82 +
3.83 +structure KEStore_Elems: KESTORE_ELEMS =
3.84 +struct
3.85 + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
3.86 +
3.87 + structure Data = Theory_Data (
3.88 + type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
3.89 + val empty = [];
3.90 + val extend = I;
3.91 + val merge = Rule_Set.to_kestore;
3.92 + );
3.93 + fun get_rlss thy = Data.get thy
3.94 + fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
3.95 +
3.96 + structure Data = Theory_Data (
3.97 + type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
3.98 + val empty = [];
3.99 + val extend = I;
3.100 + val merge = merge Exec_Def.calc_eq;
3.101 + );
3.102 + fun get_calcs thy = Data.get thy
3.103 + fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
3.104 +
3.105 + structure Data = Theory_Data (
3.106 + type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
3.107 + val empty = [];
3.108 + val extend = I;
3.109 + val merge = merge Celem.cas_eq;
3.110 + );
3.111 + fun get_cas thy = Data.get thy
3.112 + fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
3.113 +
3.114 + structure Data = Theory_Data (
3.115 + type T = Celem.ptyps;
3.116 + val empty = [Celem.e_Ptyp];
3.117 + val extend = I;
3.118 + val merge = Celem.merge_ptyps;
3.119 + );
3.120 + fun get_ptyps thy = Data.get thy;
3.121 + fun add_pbts pbts thy = let
3.122 + fun add_pbt (pbt as {guh,...}, pblID) =
3.123 + (* the pblID has the leaf-element as first; better readability achieved *)
3.124 + (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
3.125 + rev pblID |> Celem.insrt pblID pbt);
3.126 + in Data.map (fold add_pbt pbts) thy end;
3.127 +
3.128 + structure Data = Theory_Data (
3.129 + type T = Celem.mets;
3.130 + val empty = [Celem.e_Mets];
3.131 + val extend = I;
3.132 + val merge = Celem.merge_ptyps;
3.133 + );
3.134 + val get_mets = Data.get;
3.135 + fun add_mets mets thy = let
3.136 + fun add_met (met as {guh,...}, metID) =
3.137 + (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
3.138 + Celem.insrt metID met metID);
3.139 + in Data.map (fold add_met mets) thy end;
3.140 +
3.141 + structure Data = Theory_Data (
3.142 + type T = (Celem.thydata Celem1.ptyp) list;
3.143 + val empty = [];
3.144 + val extend = I;
3.145 + val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
3.146 + );
3.147 + fun get_thes thy = Data.get thy
3.148 + fun add_thes thes thy = let
3.149 + fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
3.150 + in Data.map (fold add_the thes) thy end;
3.151 + fun insert_fillpats fis thy =
3.152 + let
3.153 + fun update_elem (theID, fillpats) =
3.154 + let
3.155 + val hthm = Celem.get_py (Data.get thy) theID theID
3.156 + val hthm' = Celem.update_hthm hthm fillpats
3.157 + handle ERROR _ =>
3.158 + error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
3.159 + in Celem.update_ptyps theID theID hthm' end
3.160 + in Data.map (fold update_elem fis) thy end
3.161 +
3.162 + val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
3.163 + fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
3.164 + fun get_ref_thy () = Synchronized.value cur_thy;
3.165 +end;
3.166 +\<close>
3.167 +
3.168 +section \<open>Re-use existing access functions for knowledge elements\<close>
3.169 +text \<open>
3.170 + The independence of problems' and methods' structure enforces the accesse
3.171 + functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
3.172 +\<close>
3.173 +ML \<open>
3.174 +val get_ref_thy = KEStore_Elems.get_ref_thy;
3.175 +
3.176 +fun assoc_rls (rls' : Rule_Set.id) =
3.177 + case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
3.178 + SOME (_, rls) => rls
3.179 + | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
3.180 + "TODO exception hierarchy needs to be established.")
3.181 +
3.182 +fun assoc_rls' thy (rls' : Rule_Set.id) =
3.183 + case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
3.184 + SOME (_, rls) => rls
3.185 + | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
3.186 + "TODO exception hierarchy needs to be established.")
3.187 +
3.188 +fun assoc_calc thy calID = let
3.189 + fun ass ([], key) =
3.190 + error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
3.191 + | ass ((calc, (keyi, _)) :: pairs, key) =
3.192 + if key = keyi then calc else ass (pairs, key);
3.193 + in ass (thy |> KEStore_Elems.get_calcs, calID) end;
3.194 +
3.195 +fun assoc_calc' thy key = let
3.196 + fun ass ([], key') =
3.197 + error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
3.198 + | ass ((all as (keyi, _)) :: pairs, key') =
3.199 + if key' = keyi then all else ass (pairs, key');
3.200 + in ass (KEStore_Elems.get_calcs thy, key) end;
3.201 +
3.202 +fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
3.203 +
3.204 +fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
3.205 +fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
3.206 +fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
3.207 +\<close>
3.208 +setup \<open>KEStore_Elems.add_rlss
3.209 + [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
3.210 + ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
3.211 +
3.212 +section \<open>determine sequence of main parts in thehier\<close>
3.213 +setup \<open>
3.214 +KEStore_Elems.add_thes
3.215 + [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
3.216 + mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
3.217 + (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
3.218 + mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
3.219 + (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
3.220 + mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
3.221 +\<close>
3.222 +
3.223 +section \<open>Functions for checking KEStore_Elems\<close>
3.224 +ML \<open>
3.225 +fun short_string_of_rls Rule_Set.Empty = "Erls"
3.226 + | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
3.227 + "Rls {#calc = " ^ string_of_int (length calc) ^
3.228 + ", #rules = " ^ string_of_int (length rules) ^ ", ..."
3.229 + | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
3.230 + "Seq {#calc = " ^ string_of_int (length calc) ^
3.231 + ", #rules = " ^ string_of_int (length rules) ^ ", ..."
3.232 + | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
3.233 +fun check_kestore_rls (rls', (thyID, rls)) =
3.234 + "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
3.235 +
3.236 +fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
3.237 +
3.238 +(* we avoid term_to_string''' defined later *)
3.239 +fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
3.240 + "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
3.241 + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
3.242 +
3.243 +fun count_kestore_ptyps [] = 0
3.244 + | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
3.245 + 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
3.246 +fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
3.247 + (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
3.248 +val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
3.249 +fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
3.250 +fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
3.251 +fun sort_kestore_ptyp' _ [] = []
3.252 + | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
3.253 + ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
3.254 + :: sort_kestore_ptyp' ordfun ps');
3.255 +val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
3.256 +
3.257 +fun metguh2str ({guh,...} : Celem.met) = guh : string;
3.258 +fun check_kestore_met (mp: Celem.met Celem1.ptyp) =
3.259 + check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
3.260 +fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
3.261 +val sort_kestore_met = sort_kestore_ptyp' met_ord;
3.262 +
3.263 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
3.264 +fun write_thes thydata_list =
3.265 + thydata_list
3.266 + |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
3.267 + |> map pair2str
3.268 + |> map writeln
3.269 +\<close>
3.270 +ML \<open>
3.271 +\<close> ML \<open>
3.272 +\<close> ML \<open>
3.273 +\<close>
3.274 +end
4.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 11:07:02 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 12:22:37 2020 +0200
4.3 @@ -33,12 +33,12 @@
4.4 (*\------- to Celem3 -------/*)
4.5
4.6 (*/------- to Celem1 -------\*)
4.7 - datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
4.8 - val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
4.9 - val insrt: pblID -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
4.10 - val get_py: 'a ptyp list -> pblID -> string list -> 'a
4.11 - val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
4.12 - val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b
4.13 +(*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list\*)
4.14 + val merge_ptyps: 'a Celem1.ptyp list * 'a Celem1.ptyp list -> 'a Celem1.ptyp list
4.15 + val insrt: pblID -> 'a -> string list -> 'a Celem1.ptyp list -> 'a Celem1.ptyp list
4.16 + val get_py: 'a Celem1.ptyp list -> pblID -> string list -> 'a
4.17 + val update_ptyps: string list -> string list -> 'a -> 'a Celem1.ptyp list -> 'a Celem1.ptyp list
4.18 + val app_py: 'a Celem1.ptyp list -> ('a Celem1.ptyp -> 'b) -> pblID -> string list -> 'b
4.19 (*\------- to Celem1 -------/*)
4.20
4.21 (*/------- to Celem2 -------\*)
4.22 @@ -58,11 +58,11 @@
4.23 val thes2str: thydata list -> string
4.24 val theID2thyID: theID -> ThyC.id
4.25 val part2guh: theID -> guh
4.26 - val add_thydata: string list * string list -> thydata -> thydata ptyp list -> thydata ptyp list
4.27 + val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list
4.28 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
4.29 (*\------- to Celem8 -------/*)
4.30
4.31 - val e_Ptyp: pbt ptyp
4.32 + val e_Ptyp: pbt Celem1.ptyp
4.33 (*/------- to Celem91 -------\* )
4.34 val check_guhs_unique: bool Unsynchronized.ref
4.35 val check_pblguh_unique: guh -> pbt ptyp list -> unit
4.36 @@ -71,13 +71,13 @@
4.37 (*/------- to Celem6 -------\*)
4.38 type mets
4.39 type met
4.40 - val e_Mets: met ptyp
4.41 + val e_Mets: met Celem1.ptyp
4.42 (*\------- to Celem6 -------/*)
4.43
4.44 (*/------- to Celem91 -------\*)
4.45 val check_guhs_unique: bool Unsynchronized.ref
4.46 - val check_pblguh_unique: guh -> pbt ptyp list -> unit
4.47 - val check_metguh_unique: guh -> met ptyp list -> unit
4.48 + val check_pblguh_unique: guh -> pbt Celem1.ptyp list -> unit
4.49 + val check_metguh_unique: guh -> met Celem1.ptyp list -> unit
4.50 (*\------- to Celem91 -------/*)
4.51
4.52 val linefeed: string -> string
4.53 @@ -89,8 +89,8 @@
4.54 datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
4.55 type kestoreID
4.56 val ketype2str: ketype -> string
4.57 - val coll_pblguhs: pbt ptyp list -> guh list
4.58 - val coll_metguhs: met ptyp list -> guh list
4.59 + val coll_pblguhs: pbt Celem1.ptyp list -> guh list
4.60 + val coll_metguhs: met Celem1.ptyp list -> guh list
4.61 (*/------- to Celem4 -------\*)
4.62 type pat
4.63 val pats2str: pat list -> string
4.64 @@ -120,8 +120,8 @@
4.65
4.66 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.67 val pats2str' : pat list -> string
4.68 - val insert_fillpats: thydata ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata ptyp list ->
4.69 - thydata ptyp list
4.70 + val insert_fillpats: thydata Celem1.ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata Celem1.ptyp list ->
4.71 + thydata Celem1.ptyp list
4.72 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.73 val knowthys: unit -> theory list
4.74 (*/------- to Celem4 -------\*)
4.75 @@ -229,73 +229,11 @@
4.76 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
4.77
4.78 (*/------- to Celem1 -------\*)
4.79 -(* A tree for storing data defined in different theories
4.80 - for access from the Interpreter and from dialogue authoring
4.81 - using a string list as key.
4.82 - 'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)
4.83 -datatype 'a ptyp =
4.84 - Ptyp of string * (* element of the key *)
4.85 - 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
4.86 - presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
4.87 - ('a ptyp) list; (* the children nodes *)
4.88 -
4.89 -(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
4.90 - function for trees / ptyps *)
4.91 -fun merge_ptyps ([], pt) = pt
4.92 - | merge_ptyps (pt, []) = pt
4.93 - | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
4.94 - if k = k'
4.95 - then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
4.96 - else x' :: merge_ptyps (xs, xs');
4.97 -
4.98 -fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
4.99 - | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
4.100 - ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
4.101 - if k = k'
4.102 - then ((Ptyp (k', [pbt], ps)) :: pys)
4.103 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
4.104 - )
4.105 - | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =
4.106 - ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
4.107 - if k = k'
4.108 - then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
4.109 - else
4.110 - if length pys = 0
4.111 - then error ("insert: not found " ^ (strs2str (d : pblID)))
4.112 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
4.113 - )
4.114 - | insrt _ _ _ _ = raise ERROR "";
4.115 -
4.116 -fun app_py p f (d:pblID) (k(*:pblRD*)) =
4.117 - let
4.118 - fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);
4.119 - fun app_py' _ [] = py_err ()
4.120 - | app_py' [] _ = py_err ()
4.121 - | app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) =
4.122 - if k0 = k' then f p' else app_py' [k0] ps
4.123 - | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =
4.124 - if k0 = k'' then app_py' ks ps else app_py' k' ps';
4.125 - in app_py' k p end;
4.126 -fun get_py p =
4.127 - let
4.128 - fun extract_py (Ptyp (_, [py], _)) = py
4.129 - | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");
4.130 - in app_py p extract_py end;
4.131 -
4.132 -fun update_ptyps ID _ _ [] =
4.133 - error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
4.134 - | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
4.135 - if i = key
4.136 - then
4.137 - if length pys = 0
4.138 - then ((Ptyp (key, [data], [])) :: pyss)
4.139 - else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
4.140 - else py :: update_ptyps ID [i] data pyss
4.141 - | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
4.142 - if i = key
4.143 - then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
4.144 - else (py :: (update_ptyps ID (i :: is) data pyss))
4.145 - | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
4.146 +val merge_ptyps = Celem1.merge_ptyps;
4.147 +val insrt = Celem1.insrt;
4.148 +val app_py = Celem1.app_py;
4.149 +val get_py = Celem1.get_py;
4.150 +val update_ptyps = Celem1.update_ptyps;
4.151 (*\------- to Celem1 -------/*)
4.152
4.153 (*/------- to Celem8 -------\*)
4.154 @@ -336,8 +274,8 @@
4.155 stands for both, "thmID" and "sym_thmID"
4.156 TODO (d1) lookup from calctxt
4.157 TODO (d1) lookup from from rule set in MiniBrowser *)
4.158 -type thehier = (thydata ptyp) list;
4.159 -(* required to determine sequence of main nodes of thehier in KEStore.thy *)
4.160 +type thehier = (thydata Celem1.ptyp) list;
4.161 +(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
4.162 fun part2guh [str] = (case str of
4.163 "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
4.164 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
4.165 @@ -506,8 +444,8 @@
4.166 (*\------- to Celem5 -------/*)
4.167
4.168 (*/------- to Celem5 -------\*)
4.169 -val e_Ptyp = Ptyp ("e_pblID", [e_pbt], [])
4.170 -type ptyps = (pbt ptyp) list
4.171 +val e_Ptyp = Celem1.Ptyp ("e_pblID", [e_pbt], [])
4.172 +type ptyps = (pbt Celem1.ptyp) list
4.173 (*\------- to Celem5 -------/*)
4.174
4.175 (*/------- to Celem6 -------\*)
4.176 @@ -539,9 +477,9 @@
4.177 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
4.178 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
4.179 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
4.180 -val e_Mets = Ptyp ("e_metID", [e_met],[]);
4.181 +val e_Mets = Celem1.Ptyp ("e_metID", [e_met],[]);
4.182
4.183 -type mets = (met ptyp) list;
4.184 +type mets = (met Celem1.ptyp) list;
4.185 (*\------- to Celem6 -------/*)
4.186
4.187 (*/------- to Celem91 -------\*)
4.188 @@ -552,7 +490,7 @@
4.189
4.190 fun coll_pblguhs pbls =
4.191 let
4.192 - fun node coll (Ptyp (_, [n], ns)) = [(#guh : pbt -> guh) n] @ (nodes coll ns)
4.193 + fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : pbt -> guh) n] @ (nodes coll ns)
4.194 | node _ _ = raise ERROR "coll_pblguhs - node"
4.195 and nodes coll [] = coll
4.196 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
4.197 @@ -565,12 +503,12 @@
4.198 else ();
4.199 fun coll_metguhs mets =
4.200 let
4.201 - fun node coll (Ptyp (_, [n], ns)) = [(#guh : met -> guh) n] @ (nodes coll ns)
4.202 + fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : met -> guh) n] @ (nodes coll ns)
4.203 | node _ _ = raise ERROR "coll_pblguhs - node"
4.204 and nodes coll [] = coll
4.205 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
4.206 in nodes [] mets end;
4.207 -fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
4.208 +fun check_metguh_unique (guh:guh) (mets: (met Celem1.ptyp) list) =
4.209 if member op = (coll_metguhs mets) guh
4.210 then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
4.211 (*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
4.212 @@ -582,22 +520,22 @@
4.213 fun Html_default exist = (Html {guh = theID2guh exist,
4.214 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
4.215
4.216 -fun fill_parents (_, [i]) thydata = Ptyp (i, [thydata], [])
4.217 +fun fill_parents (_, [i]) thydata = Celem1.Ptyp (i, [thydata], [])
4.218 | fill_parents (exist, i :: is) thydata =
4.219 - Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
4.220 + Celem1.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
4.221 | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
4.222
4.223 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
4.224 - | add_thydata (exist, [i]) data (pys as (py as Ptyp (key, _, _)) :: pyss) =
4.225 + | add_thydata (exist, [i]) data (pys as (py as Celem1.Ptyp (key, _, _)) :: pyss) =
4.226 if i = key
4.227 then pys (* preserve existing thydata *)
4.228 else py :: add_thydata (exist, [i]) data pyss
4.229 - | add_thydata (exist, iss as (i :: is)) data ((py as Ptyp (key, d, pys)) :: pyss) =
4.230 + | add_thydata (exist, iss as (i :: is)) data ((py as Celem1.Ptyp (key, d, pys)) :: pyss) =
4.231 if i = key
4.232 then
4.233 if length pys = 0
4.234 - then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
4.235 - else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
4.236 + then Celem1.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
4.237 + else Celem1.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
4.238 else py :: add_thydata (exist, iss) data pyss
4.239 | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
4.240
4.241 @@ -648,7 +586,7 @@
4.242 end
4.243 fun knowthys () = (*["Isac_Knowledge", .., "Descript"]*)
4.244 let
4.245 - fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
4.246 + fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
4.247 let
4.248 val allthys = filter_out (member Context.eq_thy
4.249 [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
4.250 @@ -666,7 +604,7 @@
4.251
4.252 fun progthys () = (*["Isac_Knowledge", .., "Descript"]*)
4.253 let
4.254 - fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
4.255 + fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
4.256 let
4.257 val allthys = filter_out (member Context.eq_thy
4.258 [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 11:07:02 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 12:22:37 2020 +0200
5.3 @@ -73,7 +73,7 @@
5.4 TODO (d1) lookup from calctxt
5.5 TODO (d1) lookup from from rule set in MiniBrowser *)
5.6 type thehier = (thydata Celem1.ptyp) list;
5.7 -(* required to determine sequence of main nodes of thehier in KEStore.thy *)
5.8 +(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
5.9 fun part2guh [str] = (case str of
5.10 "Isabelle" => "thy_isab_" ^ str ^ "-part" : Celem2.guh
5.11 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
6.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Sun Apr 19 11:07:02 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Sun Apr 19 12:22:37 2020 +0200
6.3 @@ -2,7 +2,7 @@
6.4 Author: Walther Neuper
6.5 (c) due to copyright terms
6.6
6.7 -In ISAC a Rule_Set serves rewriting. KEStore holds all rule-sets for ubiquitous access.
6.8 +In ISAC a Rule_Set serves rewriting. Know_Store holds all rule-sets for ubiquitous access.
6.9 *)
6.10 signature RULE_SET =
6.11 sig
7.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Sun Apr 19 11:07:02 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Sun Apr 19 12:22:37 2020 +0200
7.3 @@ -32,7 +32,7 @@
7.4 struct
7.5 (**)
7.6
7.7 -type id = string; (* key into KEStore, without point *)
7.8 +type id = string; (* key into Know_Store, without point *)
7.9 type T = id * Thm.thm;
7.10
7.11 fun make_thm thy t = Thm.make_thm (Thm.global_cterm_of thy t);
8.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sun Apr 19 11:07:02 2020 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sun Apr 19 12:22:37 2020 +0200
8.3 @@ -14,7 +14,6 @@
8.4 ML_file interface.sml
8.5
8.6 ML \<open>
8.7 -open ThyC
8.8 \<close> ML \<open>
8.9 \<close> ML \<open>
8.10 \<close>
9.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 11:07:02 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 12:22:37 2020 +0200
9.3 @@ -33,7 +33,7 @@
9.4 (*old version with pos2filename*)
9.5 fun hierarchy pm(*"pbl" | "met"*) h =
9.6 let val j = indentation
9.7 - fun nd i p (Celem.Ptyp (id,_,ns)) =
9.8 + fun nd i p (Celem1.Ptyp (id,_,ns)) =
9.9 let val p' = Pos.lev_on p
9.10 in (indt i) ^ "<NODE>\n" ^
9.11 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.12 @@ -50,7 +50,7 @@
9.13 (*.create a hierarchy with references to the guh's.*)
9.14 fun hierarchy_pbl h =
9.15 let val j = indentation
9.16 - fun nd i p (Celem.Ptyp (id,[n as {guh,...} : Celem.pbt],ns)) =
9.17 + fun nd i p (Celem1.Ptyp (id,[n as {guh,...} : Celem.pbt],ns)) =
9.18 let val p' = Pos.lev_on p
9.19 in (indt i) ^ "<NODE>\n" ^
9.20 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.21 @@ -66,7 +66,7 @@
9.22 in nds j [0] h : Celem.xml end;
9.23 fun hierarchy_met h =
9.24 let val j = indentation
9.25 - fun nd i p (Celem.Ptyp (id,[n as {guh,...} : Celem.met],ns)) =
9.26 + fun nd i p (Celem1.Ptyp (id,[n as {guh,...} : Celem.met],ns)) =
9.27 let val p' = Pos.lev_on p
9.28 in (indt i) ^ "<NODE>\n" ^
9.29 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.30 @@ -264,7 +264,7 @@
9.31 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
9.32
9.33 (*.scan the mtree Ptyp and print the nodes using wfn.*)
9.34 -fun node (pa: Celem.filepath) ids po wfn (Celem.Ptyp (id,[n],ns)) =
9.35 +fun node (pa: Celem.filepath) ids po wfn (Celem1.Ptyp (id,[n],ns)) =
9.36 let val po' = Pos.lev_on po
9.37 in
9.38 wfn pa po' (ids@[id]) n;
10.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 11:07:02 2020 +0200
10.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 12:22:37 2020 +0200
10.3 @@ -14,7 +14,7 @@
10.4 (Celem.theID * Celem.thydata) list
10.5 val collect_thms: string -> theory -> (Celem.theID * Celem.thydata) list
10.6
10.7 - val hierarchy_guh: 'a Celem.ptyp list -> string
10.8 + val hierarchy_guh: 'a Celem1.ptyp list -> string
10.9 val insert_errpatIDs: 'a -> Celem.theID -> Error_Fill_Def.errpatID list ->
10.10 Celem.thydata * Celem.theID
10.11
10.12 @@ -45,8 +45,10 @@
10.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.14 (*NONE*)
10.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.16 - val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Celem.ptyp -> unit
10.17 - val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Celem.ptyp list -> unit
10.18 + val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
10.19 + string list -> 'a -> 'b) -> 'a Celem1.ptyp -> unit
10.20 + val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
10.21 + string list -> 'a -> 'b) -> 'a Celem1.ptyp list -> unit
10.22 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.23 end
10.24
10.25 @@ -114,7 +116,7 @@
10.26 let val thy = ThyC.get_theory thy'
10.27 in [(*TODO.WN060120 rew_ord, Eval*)]:(Celem.theID * Celem.thydata) list end;
10.28
10.29 -(* parts are: Isabelle | IsacKnowledge | IsacScripts, see KEStore.thy *)
10.30 +(* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)
10.31 fun collect_part part parent thys =
10.32 (flat (map (collect_thms part) thys)) @
10.33 (collect_rlss part (KEStore_Elems.get_rlss parent) thys) @
10.34 @@ -143,7 +145,7 @@
10.35 let
10.36 val i = indentation
10.37 val j = indentation
10.38 - fun node i p theID (Celem.Ptyp (id, _, ns)) =
10.39 + fun node i p theID (Celem1.Ptyp (id, _, ns)) =
10.40 let
10.41 val p' = Pos.lev_on p
10.42 val theID' = theID @ [id]
10.43 @@ -220,7 +222,7 @@
10.44 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
10.45
10.46 (* analoguous to 'fun node' *)
10.47 -fun thenode (pa : Celem.filepath) ids po wfn (Celem.Ptyp (id, [n], ns)) =
10.48 +fun thenode (pa : Celem.filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) =
10.49 let val po' = Pos.lev_on po
10.50 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end
10.51 and thenodes _ _ _ _ [] = ()
11.1 --- a/src/Tools/isac/Build_Isac.thy Sun Apr 19 11:07:02 2020 +0200
11.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Apr 19 12:22:37 2020 +0200
11.3 @@ -13,7 +13,7 @@
11.4
11.5 theory Build_Isac
11.6 imports
11.7 -(* theory KEStore imports Complex_Main
11.8 +(* theory Know_Store imports Complex_Main
11.9 ML_file libraryC.sml
11.10 ML_file theoryC.sml
11.11 ML_file unparseC.sml
11.12 @@ -25,7 +25,7 @@
11.13 ML_file "error-fill-def.sml"
11.14 ML_file "rule-set.sml"
11.15 ML_file calcelems.sml
11.16 - theory BaseDefinitions imports KEStore
11.17 + theory BaseDefinitions imports Know_Store
11.18 ML_file termC.sml
11.19 ML_file contextC.sml
11.20 ML_file environment.sml
11.21 @@ -147,7 +147,7 @@
11.22 \<close>
11.23 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
11.24 text \<open>
11.25 - REPLACE BY KEStore... (has been overlooked)
11.26 + REPLACE BY Know_Store... (has been overlooked)
11.27 calcelems.sml:val rew_ord' = Unsynchronized.ref ...
11.28 KEEP FOR TRACING
11.29 calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
12.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Apr 19 11:07:02 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sun Apr 19 12:22:37 2020 +0200
12.3 @@ -18,10 +18,10 @@
12.4 Istate.T * Proof.context * Program.T
12.5
12.6 val get_simplifier : Calc.T -> Rule_Set.T
12.7 - val resume_prog : ThyC.id (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
12.8 + val resume_prog : ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
12.9 (Istate.T * Proof.context) * Program.T
12.10
12.11 - val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
12.12 + val tac_from_prog : Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
12.13 val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
12.14 Program.leaf * term option
12.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Apr 19 11:07:02 2020 +0200
13.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Sun Apr 19 12:22:37 2020 +0200
13.3 @@ -219,8 +219,8 @@
13.4 end
13.5
13.6 (* packing return-values to matchTheory, contextToThy for xml-generation *)
13.7 -datatype contthy = (*also an item from KEStore on Browser ...........#*)
13.8 - EContThy (* not from KEStore ..............................*)
13.9 +datatype contthy = (*also an item from Know_Store on Browser ...........#*)
13.10 + EContThy (* not from Know_Store ..............................*)
13.11 | ContThm of (* a theorem in contex ===========================*)
13.12 {thyID : ThyC.id, (* for *2guh in sub-elems here .*)
13.13 thm : Celem.guh, (* theorem in the context .*)
14.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sun Apr 19 11:07:02 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Sun Apr 19 12:22:37 2020 +0200
14.3 @@ -48,7 +48,7 @@
14.4 \<close> ML \<open>
14.5 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
14.6 val tless_true = Rewrite_Ord.dummy_ord;
14.7 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use KEStore.xxx here, too*)
14.8 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)
14.9 [("tless_true", tless_true),
14.10 ("e_rew_ord'", tless_true),
14.11 ("dummy_ord", Rewrite_Ord.dummy_ord)]);
15.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Apr 19 11:07:02 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Apr 19 12:22:37 2020 +0200
15.3 @@ -31,13 +31,13 @@
15.4
15.5 val isabthys' = (*["Complex_Main", "Taylor", .., "Isac_Knowledge"]*)
15.6 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
15.7 - val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "KEStore"]*)
15.8 + val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
15.9 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys)
15.10 |> remove Context.eq_thy @{theory Test_Build_Thydata};
15.11
15.12 val knowthys' = (*["Isac_Knowledge", .., "Descript"]*)
15.13 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
15.14 - val progthys' = (*["Auto_Prog", .., "KEStore"]*)
15.15 + val progthys' = (*["Auto_Prog", .., "Know_Store"]*)
15.16 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
15.17 |> remove Context.eq_thy @{theory BaseDefinitions};
15.18 \<close>
15.19 @@ -62,7 +62,7 @@
15.20 text \<open>
15.21 The sequence in the (key, data) list is arbitrary, because insertion using the key
15.22 is random. The sequence of the root nodes "IsacKnowledge", "Isabelle"
15.23 - and "IsacScripts" is determined in KEStore.thy.
15.24 + and "IsacScripts" is determined in Know_Store.thy.
15.25 \<close>
15.26 text \<open>
15.27 ATTENTION: ===================================================================================
15.28 @@ -224,7 +224,7 @@
15.29 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
15.30 \<close>
15.31
15.32 -subsection \<open>Generate XML representation from SML (data in KEStore)\<close>
15.33 +subsection \<open>Generate XML representation from SML (data in Know_Store)\<close>
15.34 text \<open>
15.35 See the wiki
15.36 http://www.ist.tugraz.at/isac/Generate_representations_for_ISAC_Knowledge#Step_1:_Generate_XML_representation_from_SML
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Apr 19 11:07:02 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Apr 19 12:22:37 2020 +0200
16.3 @@ -1397,7 +1397,7 @@
16.4 };
16.5 \<close>
16.6
16.7 -subsection \<open>add to KEStore\<close>
16.8 +subsection \<open>add to Know_Store\<close>
16.9 subsubsection \<open>rule-sets\<close>
16.10 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
16.11
17.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sun Apr 19 11:07:02 2020 +0200
17.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sun Apr 19 12:22:37 2020 +0200
17.3 @@ -339,7 +339,7 @@
17.4 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
17.5 * tactic Apply_Method metID
17.6 * formula term *)
17.7 - Celem.metID * (* key for KEStore *)
17.8 + Celem.metID * (* key for Know_Store *)
17.9 term option * (* the first formula of Calc.T. TODO: rm option *)
17.10 Istate_Def.T * (* for the newly started program *)
17.11 Proof.context (* for the newly started program *)
17.12 @@ -370,7 +370,7 @@
17.13
17.14 | Init_Proof' of TermC.as_string list * Celem.spec
17.15 | Model_Problem' of (* first step in specifying *)
17.16 - Celem.pblID * (* key into KEStore *)
17.17 + Celem.pblID * (* key into Know_Store *)
17.18 Model.itm list * (* the 'untouched' pbl *)
17.19 Model.itm list (* the casually completed met *)
17.20 | Or_to_List' of term * term
18.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Sun Apr 19 11:07:02 2020 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Sun Apr 19 12:22:37 2020 +0200
18.3 @@ -44,7 +44,7 @@
18.4 val string_of_thm = ThmC_Def.string_of_thm;
18.5 val string_of_thms = ThmC_Def.string_of_thms;
18.6
18.7 -fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into KEStore*)
18.8 +fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into Know_Store*)
18.9 fun id_of_thm thm = (cut_id o Thm.get_name_hint) thm;
18.10 fun of_thm thm = (id_of_thm thm, thm);
18.11
19.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Sun Apr 19 11:07:02 2020 +0200
19.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Sun Apr 19 12:22:37 2020 +0200
19.3 @@ -230,7 +230,7 @@
19.4
19.5 (* on the fly generate a Prog from an rls for Detail_Step.go.
19.6 Types are not precise, but these are not required by LI.
19.7 - Argument "thy" is only required for lookup in KEStore.
19.8 + Argument "thy" is only required for lookup in Know_Store.
19.9 *)
19.10 fun gen thy t rls =
19.11 let
20.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sun Apr 19 11:07:02 2020 +0200
20.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Sun Apr 19 12:22:37 2020 +0200
20.3 @@ -72,7 +72,7 @@
20.4 NTH_NIL: "NTH 1 (x # xs) = x" and
20.5 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
20.6
20.7 -(* redefine together with identifiers (still) required for KEStore ..*)
20.8 +(* redefine together with identifiers (still) required for Know_Store ..*)
20.9 axiomatization where
20.10 hd_thm: "hd (x # xs) = x"
20.11
21.1 --- a/src/Tools/isac/Specify/ptyps.sml Sun Apr 19 11:07:02 2020 +0200
21.2 +++ b/src/Tools/isac/Specify/ptyps.sml Sun Apr 19 12:22:37 2020 +0200
21.3 @@ -32,7 +32,7 @@
21.4
21.5 type pblRD = string list (* for pbl-met-hierarchy.sml *)
21.6 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
21.7 - val scan : string list -> 'a Celem.ptyp list -> string list list (* for thy-hierarchy.sml *)
21.8 + val scan : string list -> 'a Celem1.ptyp list -> string list list (* for thy-hierarchy.sml *)
21.9 val itm_out : theory -> Model.itm_ -> string
21.10 val dsc_unknown : term
21.11
21.12 @@ -123,10 +123,10 @@
21.13 fun get_data ptyp =
21.14 let
21.15 fun scan [] = []
21.16 - | scan ((Celem.Ptyp ((_, data, []))) :: []) = data
21.17 - | scan ((Celem.Ptyp ((_, data, pl))) :: []) = data @ scan pl
21.18 - | scan ((Celem.Ptyp ((_, data, []))) :: ps) = data @ scan ps
21.19 - | scan ((Celem.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
21.20 + | scan ((Celem1.Ptyp ((_, data, []))) :: []) = data
21.21 + | scan ((Celem1.Ptyp ((_, data, pl))) :: []) = data @ scan pl
21.22 + | scan ((Celem1.Ptyp ((_, data, []))) :: ps) = data @ scan ps
21.23 + | scan ((Celem1.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
21.24 in scan ptyp end
21.25
21.26 fun get_fun_ids thy =
21.27 @@ -300,7 +300,7 @@
21.28 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
21.29 "pbl_" =>
21.30 let
21.31 - fun node ids gu (Celem.Ptyp (id, [{guh, ...}], ns)) =
21.32 + fun node ids gu (Celem1.Ptyp (id, [{guh, ...}], ns)) =
21.33 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
21.34 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
21.35 and nodes _ _ [] = NONE
21.36 @@ -313,7 +313,7 @@
21.37 end
21.38 | "met_" =>
21.39 let
21.40 - fun node ids gu (Celem.Ptyp (id, [{guh, ...}], ns)) =
21.41 + fun node ids gu (Celem1.Ptyp (id, [{guh, ...}], ns)) =
21.42 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
21.43 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
21.44 and nodes _ _ [] = NONE
21.45 @@ -421,10 +421,10 @@
21.46 fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
21.47
21.48 fun scan _ [] = [] (* no base case, for empty doms only *)
21.49 - | scan id ((Celem.Ptyp ((i, _, []))) :: []) = [id @ [i]]
21.50 - | scan id ((Celem.Ptyp ((i, _, pl))) :: []) = scan (id @ [i]) pl
21.51 - | scan id ((Celem.Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
21.52 - | scan id ((Celem.Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
21.53 + | scan id ((Celem1.Ptyp ((i, _, []))) :: []) = [id @ [i]]
21.54 + | scan id ((Celem1.Ptyp ((i, _, pl))) :: []) = scan (id @ [i]) pl
21.55 + | scan id ((Celem1.Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
21.56 + | scan id ((Celem1.Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
21.57
21.58 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ()); (* for tests *)
21.59 fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)
21.60 @@ -595,11 +595,11 @@
21.61 end;
21.62
21.63 (* refine a problem; construct pblRD while scanning *)
21.64 -fun refin (pblRD: pblRD) ori (Celem.Ptyp (pI, [py], [])) =
21.65 +fun refin (pblRD: pblRD) ori (Celem1.Ptyp (pI, [py], [])) =
21.66 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
21.67 then SOME ((pblRD @ [pI]): pblRD)
21.68 else NONE
21.69 - | refin pblRD ori (Celem.Ptyp (pI, [py], pys)) =
21.70 + | refin pblRD ori (Celem1.Ptyp (pI, [py], pys)) =
21.71 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
21.72 then (case refins (pblRD @ [pI]) ori pys of
21.73 SOME pblRD' => SOME pblRD'
21.74 @@ -607,13 +607,13 @@
21.75 else NONE
21.76 | refin _ _ _ = error "refin: uncovered fun def."
21.77 and refins _ _ [] = NONE
21.78 - | refins pblRD ori ((p as Celem.Ptyp _) :: pts) =
21.79 + | refins pblRD ori ((p as Celem1.Ptyp _) :: pts) =
21.80 (case refin pblRD ori p of
21.81 SOME pblRD' => SOME pblRD'
21.82 | NONE => refins pblRD ori pts);
21.83
21.84 (* refine a problem; version providing output for math-experts *)
21.85 -fun refin' (pblRD: pblRD) fmz pbls (Celem.Ptyp (pI, [py], [])) =
21.86 +fun refin' (pblRD: pblRD) fmz pbls (Celem1.Ptyp (pI, [py], [])) =
21.87 let
21.88 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
21.89 val {thy, ppc, where_, prls, ...} = py
21.90 @@ -625,7 +625,7 @@
21.91 then pbls @ [Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
21.92 else pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
21.93 end
21.94 - | refin' pblRD fmz pbls (Celem.Ptyp (pI, [py], pys)) =
21.95 + | refin' pblRD fmz pbls (Celem1.Ptyp (pI, [py], pys)) =
21.96 let
21.97 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
21.98 val {thy, ppc, where_, prls, ...} = py
21.99 @@ -641,7 +641,7 @@
21.100 end
21.101 | refin' _ _ _ _ = error "refin': uncovered fun def."
21.102 and refins' _ _ pbls [] = pbls
21.103 - | refins' pblRD fmz pbls ((p as Celem.Ptyp _) :: pts) =
21.104 + | refins' pblRD fmz pbls ((p as Celem1.Ptyp _) :: pts) =
21.105 let
21.106 val pbls' = refin' pblRD fmz pbls p
21.107 in
21.108 @@ -651,7 +651,7 @@
21.109 end;
21.110
21.111 (* refine a problem; version for tactic Refine_Problem *)
21.112 -fun refin'' _ (pblRD: pblRD) itms pbls (Celem.Ptyp (pI, [py], [])) =
21.113 +fun refin'' _ (pblRD: pblRD) itms pbls (Celem1.Ptyp (pI, [py], [])) =
21.114 let
21.115 val {thy, ppc, where_, prls, ...} = py
21.116 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
21.117 @@ -660,7 +660,7 @@
21.118 then pbls @ [Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))]
21.119 else pbls @ [Stool.NoMatch_]
21.120 end
21.121 - | refin'' _ pblRD itms pbls (Celem.Ptyp (pI, [py], pys)) =
21.122 + | refin'' _ pblRD itms pbls (Celem1.Ptyp (pI, [py], pys)) =
21.123 let
21.124 val {thy, ppc, where_, prls, ...} = py
21.125 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
21.126 @@ -671,7 +671,7 @@
21.127 end
21.128 | refin'' _ _ _ _ _ = error "refin': uncovered fun def."
21.129 and refins'' _ _ _ pbls [] = pbls
21.130 - | refins'' thy pblRD itms pbls ((p as Celem.Ptyp _) :: pts) =
21.131 + | refins'' thy pblRD itms pbls ((p as Celem1.Ptyp _) :: pts) =
21.132 let
21.133 val pbls' = refin'' thy pblRD itms pbls p
21.134 in case last_elem pbls' of
22.1 --- a/src/Tools/isac/TODO.thy Sun Apr 19 11:07:02 2020 +0200
22.2 +++ b/src/Tools/isac/TODO.thy Sun Apr 19 12:22:37 2020 +0200
22.3 @@ -26,7 +26,7 @@
22.4 (*/------- to -------\*)
22.5 (*\------- to -------/*)
22.6 \begin{itemize}
22.7 - \item ML_file "rule-set.sml" KEStore -> MathEngBasic (=ThmC, Rewrite)
22.8 + \item ML_file "rule-set.sml" Know_Store -> MathEngBasic (=ThmC, Rewrite)
22.9 probably first review calcelems.sml
22.10 \item xxx
22.11 \item replace src/ Erls Rule_Set.Empty
22.12 @@ -34,7 +34,7 @@
22.13 \item rename exec-def.sml -> eval_def.sml
22.14 calculate.sml _> evaluate.sml (struct Eval -> Evaluate?!?)
22.15 \item xxx
22.16 - \item rename KEStore -> Know_Store KNOWLEDGE_STORE + file.sml
22.17 + \item rename Know_Store -> Know_Store KNOWLEDGE_STORE + file.sml
22.18 Build_Thydata -> Build_Knowledge
22.19 \item xxx
22.20 \item rename ptyps.sml -> specify-etc.sml
22.21 @@ -211,7 +211,7 @@
22.22 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
22.23 \item Test.thy: met_test_sqrt2: deleted?!
22.24 \item xxx
22.25 - \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use KEStore.xxx, too*)
22.26 + \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx, too*)
22.27 \item xxx
22.28 \item automatically extrac rls from program-code
22.29 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
23.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sun Apr 19 11:07:02 2020 +0200
23.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sun Apr 19 12:22:37 2020 +0200
23.3 @@ -1,4 +1,4 @@
23.4 -(* KEStore holds Knowledge and Exercises in Isac's Java front-end.
23.5 +(* Know_Store holds Knowledge and Exercises in Isac's Java front-end.
23.6 In the front-end knowledge comprises theories, problems and methods.
23.7 Elements of problems and methods are defined in theories alongside
23.8 the development of respective language elements.
24.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 11:07:02 2020 +0200
24.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 12:22:37 2020 +0200
24.3 @@ -120,24 +120,24 @@
24.4 "-------- fun update_ptyps --------------------------------------------------";
24.5 "-------- fun update_ptyps --------------------------------------------------";
24.6 val pty = [
24.7 - Ptyp ("aaa", [1], [
24.8 - Ptyp ("aaa-1", [11], [])]),
24.9 - Ptyp ("bbb", [2], [
24.10 - Ptyp ("bbb-1", [21], []),
24.11 - Ptyp ("bbb-2", [22], [
24.12 - Ptyp ("bbb-21", [221], []),
24.13 - Ptyp ("bbb-22", [222], [])])]),
24.14 - Ptyp ("ccc", [3], [])] : int ptyp list
24.15 + Celem1.Ptyp ("aaa", [1], [
24.16 + Celem1.Ptyp ("aaa-1", [11], [])]),
24.17 + Celem1.Ptyp ("bbb", [2], [
24.18 + Celem1.Ptyp ("bbb-1", [21], []),
24.19 + Celem1.Ptyp ("bbb-2", [22], [
24.20 + Celem1.Ptyp ("bbb-21", [221], []),
24.21 + Celem1.Ptyp ("bbb-22", [222], [])])]),
24.22 + Celem1.Ptyp ("ccc", [3], [])] : int Celem1.ptyp list
24.23
24.24 val ID = ["ddd"];
24.25 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)
24.26
24.27 val ID = ["ccc"];
24.28 if update_ptyps ID ID 99999 pty =
24.29 - [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
24.30 - Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []),
24.31 - Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [222], [])])]),
24.32 - Ptyp ("ccc", [99999], [])]
24.33 + [Celem1.Ptyp ("aaa", [1], [Celem1.Ptyp ("aaa-1", [11], [])]),
24.34 + Celem1.Ptyp ("bbb", [2], [Celem1.Ptyp ("bbb-1", [21], []),
24.35 + Celem1.Ptyp ("bbb-2", [22], [Celem1.Ptyp ("bbb-21", [221], []), Celem1.Ptyp ("bbb-22", [222], [])])]),
24.36 + Celem1.Ptyp ("ccc", [99999], [])]
24.37 then () else error "update_ptyps has changed 1";
24.38
24.39 val ID = ["aaa"];
24.40 @@ -145,18 +145,18 @@
24.41
24.42 val ID = ["bbb", "bbb-2", "bbb-21"];
24.43 if update_ptyps ID ID 99999 pty =
24.44 - [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
24.45 - Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []), Ptyp ("bbb-2", [22],
24.46 - [Ptyp ("bbb-21", [99999], []), Ptyp ("bbb-22", [222], [])])]),
24.47 - Ptyp ("ccc", [3], [])]
24.48 + [Celem1.Ptyp ("aaa", [1], [Celem1.Ptyp ("aaa-1", [11], [])]),
24.49 + Celem1.Ptyp ("bbb", [2], [Celem1.Ptyp ("bbb-1", [21], []), Celem1.Ptyp ("bbb-2", [22],
24.50 + [Celem1.Ptyp ("bbb-21", [99999], []), Celem1.Ptyp ("bbb-22", [222], [])])]),
24.51 + Celem1.Ptyp ("ccc", [3], [])]
24.52 then () else error "update_ptyps has changed 2";
24.53
24.54 val ID = ["bbb", "bbb-2", "bbb-22"];
24.55 if update_ptyps ID ID 99999 pty =
24.56 - [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
24.57 - Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []),
24.58 - Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [99999], [])])]),
24.59 - Ptyp ("ccc", [3], [])]
24.60 + [Celem1.Ptyp ("aaa", [1], [Celem1.Ptyp ("aaa-1", [11], [])]),
24.61 + Celem1.Ptyp ("bbb", [2], [Celem1.Ptyp ("bbb-1", [21], []),
24.62 + Celem1.Ptyp ("bbb-2", [22], [Celem1.Ptyp ("bbb-21", [221], []), Celem1.Ptyp ("bbb-22", [99999], [])])]),
24.63 + Celem1.Ptyp ("ccc", [3], [])]
24.64 then () else error "update_ptyps has changed 3";
24.65
24.66 "----------- fun subst2str' --------------------------------------------------------------------";
25.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml Sun Apr 19 11:07:02 2020 +0200
25.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml Sun Apr 19 12:22:37 2020 +0200
25.3 @@ -1,4 +1,4 @@
25.4 -(* Title: tests for KEStore.thy
25.5 +(* Title: tests for Know_Store.thy
25.6 Author: Walther Neuper
25.7 Use is subject to license terms.
25.8 *)
25.9 @@ -15,8 +15,8 @@
25.10 "-------- fun check_kestore_rls ----------------------------------------------";
25.11 "-------- fun check_kestore_rls ----------------------------------------------";
25.12 "-------- fun check_kestore_rls ----------------------------------------------";
25.13 -if check_kestore_rls ("empty", ("KEStore", Rule_Set.empty)) =
25.14 - "(empty, (KEStore, Rls {#calc = 0, #rules = 0, ...))"
25.15 +if check_kestore_rls ("empty", ("Know_Store", Rule_Set.empty)) =
25.16 + "(empty, (Know_Store, Rls {#calc = 0, #rules = 0, ...))"
25.17 then () else error "check_kestore_rls changed"
25.18 ;
25.19 Test_KEStore_Elems.get_rlss @{theory Isac_Knowledge}
26.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 11:07:02 2020 +0200
26.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 12:22:37 2020 +0200
26.3 @@ -124,7 +124,7 @@
26.4 get_ptyps (); (*not = []*)
26.5 "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
26.6 (p, []: string list, [0], pbl2file, (get_ptyps ()));
26.7 -"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
26.8 +"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Celem1.Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
26.9 val po' = lev_on po;
26.10 wfn (*= pbl2file*)
26.11 "~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id:metID), (pbl as {guh,...})) =
27.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 11:07:02 2020 +0200
27.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 12:22:37 2020 +0200
27.3 @@ -90,14 +90,14 @@
27.4 "----------- search for data error in thes2file ------------------";
27.5 "----------- search for data error in thes2file ------------------";
27.6 val TESTdump = Unsynchronized.ref
27.7 - ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
27.8 + ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Celem1.Ptyp ("xxx", [], []): thydata Celem1.ptyp);
27.9
27.10 -fun TESTthenode (pa:filepath) ids po wfn (Ptyp (id, [n], ns)) TESTids =
27.11 +fun TESTthenode (pa:filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) TESTids =
27.12 let val po' = lev_on po
27.13 in
27.14 if (ids@[id]) = TESTids
27.15 then
27.16 - (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns)));
27.17 + (TESTdump := (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns)));
27.18 error "stopped before error, created TESTdump") (* this exn creates right signature*)
27.19 else
27.20 wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
27.21 @@ -120,7 +120,7 @@
27.22 handle _(* "stopped before error, created TESTdump" *) => ());
27.23 ;
27.24 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
27.25 -val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump;
27.26 +val (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns))) = ! TESTdump;
27.27 ;
27.28 "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) =
27.29 (pa, po', (ids@[id]), n);
27.30 @@ -160,12 +160,12 @@
27.31 "----------- correct theIDs for Rule_Set.empty ----------------------------";
27.32 "----------- correct theIDs for Rule_Set.empty ----------------------------";
27.33 "----------- correct theIDs for Rule_Set.empty ----------------------------";
27.34 -if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "KEStore") then ()
27.35 +if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()
27.36 else error "thy_containing_rls Rule_Set.empty changed";
27.37 show_thes ();
27.38 (*shows different assignment for "empty"...
27.39 :
27.40 - ["IsacScripts", "KEStore", "Rulesets", "empty"],
27.41 + ["IsacScripts", "Know_Store", "Rulesets", "empty"],
27.42 :*)
27.43
27.44 "----------- fun revert_sym_rule --------------------------------------";
27.45 @@ -188,7 +188,7 @@
27.46 "----------- fun thms_of_rlss ------------------------------------";
27.47 "----------- fun thms_of_rlss ------------------------------------";
27.48 val rlss =
27.49 - [("empty" : Rule_Set.id, ("KEStore": ThyC.id, Rule_Set.empty)),
27.50 + [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
27.51 ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]
27.52 ;
27.53 val [_, (thmID, term)] = thms_of_rlss thy rlss;
27.54 @@ -322,7 +322,7 @@
27.55 mathauthors = ["isac-team"], thm = _})] => ()
27.56 | _ => error "collect thydata from Test_Build_Thydata changed";
27.57 ;
27.58 -(* we store locally on MINIthehier instead on KEStore, see KEStore: *)
27.59 +(* we store locally on MINIthehier instead on Know_Store, see Know_Store: *)
27.60 fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
27.61 val thes = map (fn (a, b) => (b, a)) thydata_list
27.62 val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
27.63 @@ -361,7 +361,7 @@
27.64 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
27.65 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
27.66 (path, [], [0], thydata2file, MINIthehier);
27.67 -"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Ptyp (id, [n], ns))) =
27.68 +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Celem1.Ptyp (id, [n], ns))) =
27.69 (pa, ids, po, wfn, n);
27.70 val po' = lev_on po;
27.71 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
28.1 --- a/test/Tools/isac/Interpret/rewtools.sml Sun Apr 19 11:07:02 2020 +0200
28.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Sun Apr 19 12:22:37 2020 +0200
28.3 @@ -72,7 +72,7 @@
28.4 if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
28.5 else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
28.6 ;
28.7 -if thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "KEStore") then ()
28.8 +if thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()
28.9 else error ("thy_containing_rls changed for 'Biegelinie', 'e_rls'")
28.10 ;
28.11 if thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
29.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Sun Apr 19 11:07:02 2020 +0200
29.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Sun Apr 19 12:22:37 2020 +0200
29.3 @@ -47,11 +47,11 @@
29.4 @{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Pure"]*)
29.5 val isabthys' = (*["Complex_Main", "Taylor", .., "Pure"]*)
29.6 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
29.7 - val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "KEStore"]*)
29.8 + val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
29.9 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
29.10 val knowthys' = (*["Isac_Knowledge", .., "Descript", "Delete"]*)
29.11 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
29.12 - val progthys' = (*["Program", "Tools", "ListC", "KEStore"]*)
29.13 + val progthys' = (*["Program", "Tools", "ListC", "Know_Store"]*)
29.14 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
29.15 val isacrlsthms = (*length = 460*)
29.16 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
30.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Sun Apr 19 11:07:02 2020 +0200
30.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Sun Apr 19 12:22:37 2020 +0200
30.3 @@ -283,9 +283,9 @@
30.4
30.5 (*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*)
30.6 "~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:pblID)) = (fmz, ["LINEAR","system"]);
30.7 -"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Ptyp (pI, [py], [])): pbt ptyp)) =
30.8 +"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Celem1.Ptyp (pI, [py], [])): pbt Celem1.ptyp)) =
30.9 ((rev o tl) pblID, fmz, [(*match list*)],
30.10 - ((Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt ptyp));
30.11 + ((Celem1.Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Celem1.ptyp));
30.12 val {thy, ppc, where_, prls, ...} = py ;
30.13 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
30.14 val ctxt = Proof_Context.init_global thy;
30.15 @@ -427,10 +427,10 @@
30.16 (*default_print_depth 11;*) matches; (*default_print_depth 3;*)
30.17 (*brought: 'False "length_ es_ = 2"'*)
30.18
30.19 -(*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
30.20 -(* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
30.21 +(*-----fun refin' (pblRD:pblRD) fmz pbls ((Celem1.Ptyp (pI,[py],[])):pbt Celem1.ptyp) =
30.22 +(* val ((pblRD:pblRD), fmz, pbls, ((Celem1.Ptyp (pI,[py],[])):pbt Celem1.ptyp)) =
30.23 (rev ["LINEAR","system"], fmz, [(*match list*)],
30.24 - ((Ptyp ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt ptyp));
30.25 + ((Celem1.Ptyp ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Celem1.ptyp));
30.26 *)
30.27 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
30.28 val it = "length_ (es_::real list) = (2::real)" : string
31.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Sun Apr 19 11:07:02 2020 +0200
31.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Sun Apr 19 12:22:37 2020 +0200
31.3 @@ -306,7 +306,7 @@
31.4 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
31.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
31.6
31.7 -(*//------------------ ERROR rls "make_rooteq " missing in KEStore.
31.8 +(*//------------------ ERROR rls "make_rooteq " missing in Know_Store.
31.9 after repair (Try (Repeat (Rewrite_Set ''make_rooteq '')))
31.10 ------------------ ERROR check_elementwise: no set 1 + sqrt x = 3 -----------------------\\* )
31.11 (*val (p,_,f,nxt,_,pt) =*) me nxt p c pt;
32.1 --- a/test/Tools/isac/Specify/ptyps.sml Sun Apr 19 11:07:02 2020 +0200
32.2 +++ b/test/Tools/isac/Specify/ptyps.sml Sun Apr 19 12:22:37 2020 +0200
32.3 @@ -61,11 +61,11 @@
32.4 "----------- refin test-pbtyps -----------------------------------";
32.5 (* fragile test setup: expects ptyps as fixed *)
32.6 val level_1 = case nth 9 (get_ptyps ()) of
32.7 -Ptyp ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
32.8 +Celem1.Ptyp ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
32.9 val level_2 = case nth 4 level_1 of
32.10 -Ptyp ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
32.11 +Celem1.Ptyp ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
32.12 val pbla_branch = case level_2 of
32.13 -[Ptyp ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
32.14 +[Celem1.Ptyp ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
32.15
32.16 (*case 1: no refinement *)
32.17 case refin [] ori1 (hd pbla_branch) of
32.18 @@ -84,7 +84,7 @@
32.19 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
32.20
32.21 (*case 5: start refinement somewhere in ptyps*)
32.22 -val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = pbla_branch;
32.23 +val [Celem1.Ptyp ("pbla",_,[_, ppp as Celem1.Ptyp ("pbla2",_,_), _])] = pbla_branch;
32.24 case refin ["pbla"] ori4 ppp of
32.25 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
32.26 ==================================================================*)
32.27 @@ -423,16 +423,16 @@
32.28 val n = e_pbt;
32.29 (#guh : pbt -> guh) e_pbt;
32.30
32.31 -fun XXXnode coll (Ptyp (_,[n],ns)) =
32.32 +fun XXXnode coll (Celem1.Ptyp (_,[n],ns)) =
32.33 [(#guh : pbt -> guh) n]
32.34 and XXXnodes coll [] = coll
32.35 - | XXXnodes coll (n::ns : pbt ptyp list) = (XXXnode coll n) @
32.36 + | XXXnodes coll (n::ns : pbt Celem1.ptyp list) = (XXXnode coll n) @
32.37 (XXXnodes coll ns);
32.38 (*^^^ this works, but not this ...
32.39 -fun node coll (Ptyp (_,[n],ns)) =
32.40 +fun node coll (Celem1.Ptyp (_,[n],ns)) =
32.41 [(#guh : 'a -> guh) n]
32.42 and nodes coll [] = coll
32.43 - | nodes coll (n::ns : 'a ptyp list) = (node coll n) @ (nodes coll ns);
32.44 + | nodes coll (n::ns : 'a Celem1.ptyp list) = (node coll n) @ (nodes coll ns);
32.45
32.46 Error:
32.47 Can't unify {guh: 'a, ...} with 'b (Cannot unify with explicit type variable)
32.48 @@ -450,19 +450,19 @@
32.49 "----------- fun guh2kestoreID -----------------------------------";
32.50 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
32.51 (* ERROR: Exception Bind raised *)
32.52 -val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
32.53 - Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
32.54 +val (Celem1.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
32.55 + Celem1.Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
32.56
32.57 (*
32.58 nodes [] guh1 (get_ptyps ());
32.59 nodes [] guh2 (get_ptyps ());
32.60 *)
32.61 -val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)
32.62 +val (Celem1.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)
32.63 ::
32.64 - Ptyp (id2,[n2 as {guh=guh2,...} : pbt],
32.65 - (Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
32.66 + Celem1.Ptyp (id2,[n2 as {guh=guh2,...} : pbt],
32.67 + (Celem1.Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
32.68 ::
32.69 - Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
32.70 + Celem1.Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
32.71 ::
32.72 _ ) = (get_ptyps ());
32.73 (*