1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 12:22:37 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 15:37:39 2020 +0200
1.3 @@ -34,8 +34,6 @@
1.4 ML_file "celem-7.sml" (*cas_elem*)
1.5 ML_file "celem-8.sml" (*thydata*)
1.6 ML_file "celem-91.sml" (*check_guhs_unique*)
1.7 -ML_file "celem-92.sml" (**)
1.8 -ML_file "celem-93.sml" (**)
1.9
1.10 ML_file calcelems.sml
1.11 ML_file tracing.sml
1.12 @@ -112,34 +110,34 @@
1.13 type T = Celem.ptyps;
1.14 val empty = [Celem.e_Ptyp];
1.15 val extend = I;
1.16 - val merge = Celem.merge_ptyps;
1.17 + val merge = Celem1.merge_ptyps;
1.18 );
1.19 fun get_ptyps thy = Data.get thy;
1.20 fun add_pbts pbts thy = let
1.21 fun add_pbt (pbt as {guh,...}, pblID) =
1.22 (* the pblID has the leaf-element as first; better readability achieved *)
1.23 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
1.24 - rev pblID |> Celem.insrt pblID pbt);
1.25 + rev pblID |> Celem1.insrt pblID pbt);
1.26 in Data.map (fold add_pbt pbts) thy end;
1.27
1.28 structure Data = Theory_Data (
1.29 type T = Celem.mets;
1.30 val empty = [Celem.e_Mets];
1.31 val extend = I;
1.32 - val merge = Celem.merge_ptyps;
1.33 + val merge = Celem1.merge_ptyps;
1.34 );
1.35 val get_mets = Data.get;
1.36 fun add_mets mets thy = let
1.37 fun add_met (met as {guh,...}, metID) =
1.38 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
1.39 - Celem.insrt metID met metID);
1.40 + Celem1.insrt metID met metID);
1.41 in Data.map (fold add_met mets) thy end;
1.42
1.43 structure Data = Theory_Data (
1.44 type T = (Celem.thydata Celem1.ptyp) list;
1.45 val empty = [];
1.46 val extend = I;
1.47 - val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
1.48 + val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
1.49 );
1.50 fun get_thes thy = Data.get thy
1.51 fun add_thes thes thy = let
1.52 @@ -149,11 +147,11 @@
1.53 let
1.54 fun update_elem (theID, fillpats) =
1.55 let
1.56 - val hthm = Celem.get_py (Data.get thy) theID theID
1.57 + val hthm = Celem1.get_py (Data.get thy) theID theID
1.58 val hthm' = Celem.update_hthm hthm fillpats
1.59 handle ERROR _ =>
1.60 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.61 - in Celem.update_ptyps theID theID hthm' end
1.62 + in Celem1.update_ptyps theID theID hthm' end
1.63 in Data.map (fold update_elem fis) thy end
1.64
1.65 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.66 @@ -241,7 +239,7 @@
1.67 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
1.68 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.69 fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.70 - (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed;
1.71 + (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
1.72 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
1.73 fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.74 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
1.75 @@ -260,7 +258,7 @@
1.76 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
1.77 fun write_thes thydata_list =
1.78 thydata_list
1.79 - |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))
1.80 + |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))
1.81 |> map pair2str
1.82 |> map writeln
1.83 \<close>
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 12:22:37 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 15:37:39 2020 +0200
2.3 @@ -16,8 +16,11 @@
2.4 (*\------- to Celem7 -------/*)
2.5
2.6 (*/------- to Celem5 -------\*)
2.7 - type pbt
2.8 - type ptyps
2.9 + type pbt = Celem5.pbt
2.10 + val e_pbt: pbt;
2.11 + val e_Ptyp: pbt Celem1.ptyp
2.12 + type ptyps = Celem5.ptyps
2.13 + val pbts2str: pbt list -> string
2.14 (*\------- to Celem5 -------/*)
2.15
2.16 (*/------- to Celem3 -------\*)
2.17 @@ -46,53 +49,50 @@
2.18 (*\------- to Celem2 -------/*)
2.19
2.20 (*/------- to Celem8 -------\*)
2.21 - type authors
2.22 - datatype thydata
2.23 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: guh, mathauthors: authors}
2.24 - | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
2.25 - | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
2.26 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: guh, mathauthors: authors, thm: thm}
2.27 - | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
2.28 - type theID
2.29 + type authors = Celem8.authors
2.30 + datatype thydata = datatype Celem8.thydata
2.31 + type theID = Celem8.theID
2.32 + val theID2str: string list -> string
2.33 val the2str: thydata -> string
2.34 val thes2str: thydata list -> string
2.35 val theID2thyID: theID -> ThyC.id
2.36 +
2.37 val part2guh: theID -> guh
2.38 + val thy2guh: theID -> guh
2.39 + val thypart2guh: theID -> guh
2.40 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> guh
2.41 + val rls2guh: string * ThyC.id -> Rule_Set.id -> guh
2.42 + val cal2guh: string * ThyC.id -> string -> guh
2.43 + val ord2guh: string * ThyC.id -> string -> string
2.44 + val theID2guh: theID -> guh
2.45 +
2.46 val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list
2.47 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
2.48 (*\------- to Celem8 -------/*)
2.49
2.50 - val e_Ptyp: pbt Celem1.ptyp
2.51 -(*/------- to Celem91 -------\* )
2.52 - val check_guhs_unique: bool Unsynchronized.ref
2.53 - val check_pblguh_unique: guh -> pbt ptyp list -> unit
2.54 -( *\------- to Celem91 -------/*)
2.55 -
2.56 (*/------- to Celem6 -------\*)
2.57 - type mets
2.58 - type met
2.59 + type met = Celem6.met
2.60 + type mets = Celem6.mets
2.61 val e_Mets: met Celem1.ptyp
2.62 (*\------- to Celem6 -------/*)
2.63
2.64 (*/------- to Celem91 -------\*)
2.65 val check_guhs_unique: bool Unsynchronized.ref
2.66 + val coll_pblguhs: pbt Celem1.ptyp list -> guh list
2.67 val check_pblguh_unique: guh -> pbt Celem1.ptyp list -> unit
2.68 + val coll_metguhs: met Celem1.ptyp list -> guh list
2.69 val check_metguh_unique: guh -> met Celem1.ptyp list -> unit
2.70 (*\------- to Celem91 -------/*)
2.71
2.72 val linefeed: string -> string
2.73 - val pbts2str: pbt list -> string
2.74 - val theID2str: string list -> string
2.75 val trace_calc: bool Unsynchronized.ref
2.76 val trace_rewrite: bool Unsynchronized.ref
2.77 val depth: int Unsynchronized.ref
2.78 datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
2.79 type kestoreID
2.80 val ketype2str: ketype -> string
2.81 - val coll_pblguhs: pbt Celem1.ptyp list -> guh list
2.82 - val coll_metguhs: met Celem1.ptyp list -> guh list
2.83 (*/------- to Celem4 -------\*)
2.84 - type pat
2.85 + type pat = Celem4.pat
2.86 val pats2str: pat list -> string
2.87 (*\------- to Celem4 -------/*)
2.88 val maxthy: theory -> theory -> theory
2.89 @@ -100,20 +100,11 @@
2.90 val lim_deriv: int Unsynchronized.ref
2.91 val isabthys: unit -> theory list
2.92 val partID': ThyC.id -> string
2.93 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> guh
2.94 - val rls2guh: string * ThyC.id -> Rule_Set.id -> guh
2.95 -(*/------- to Celem8 -------\*)
2.96 - val theID2guh: theID -> guh
2.97 -(*\------- to Celem8 -------/*)
2.98 type pbt_ = string * (term * term)
2.99 eqtype xml
2.100 - val cal2guh: string * ThyC.id -> string -> guh
2.101 val ketype2str': ketype -> string
2.102 val str2ketype': string -> ketype
2.103 eqtype filepath
2.104 - val thy2guh: theID -> guh
2.105 - val thypart2guh: theID -> guh
2.106 - val ord2guh: string * ThyC.id -> string -> string
2.107 val update_hrls: thydata -> Error_Fill_Def.errpatID list -> thydata
2.108 eqtype iterID
2.109 eqtype calcID
2.110 @@ -124,10 +115,9 @@
2.111 thydata Celem1.ptyp list
2.112 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.113 val knowthys: unit -> theory list
2.114 -(*/------- to Celem4 -------\*)
2.115 - val e_pbt: pbt
2.116 -(*\------- to Celem4 -------/*)
2.117 +(*/------- to Celem6 -------\*)
2.118 val e_met: met
2.119 +(*\------- to Celem6 -------/*)
2.120 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.121
2.122 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
2.123 @@ -146,7 +136,7 @@
2.124 type calcID = int;
2.125
2.126 (*/------- to Celem2 -------\*)
2.127 -type guh = string;
2.128 +type guh = Celem2.guh;
2.129 (*\------- to Celem2 -------/*)
2.130 type xml = string; (* rm together with old code replaced by XML.tree *)
2.131
2.132 @@ -180,32 +170,20 @@
2.133
2.134 (*/------- to Celem3 -------\*)
2.135 (*the key into the hierarchy ob problems*)
2.136 -type pblID = string list; (* domID :: ...*)
2.137 -val e_pblID = ["e_pblID"];
2.138 -
2.139 -(*the key into the hierarchy ob methods*)
2.140 -type metID = string list;
2.141 -type spec = ThyC.id * pblID * metID;
2.142 -fun spec2str (dom, pbl, met) =
2.143 - "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
2.144 -val e_metID = ["e_metID"];
2.145 -val metID2str = strs2str;
2.146 -val empty_spec = (ThyC.id_empty, e_pblID, e_metID);
2.147 -val e_spec = empty_spec;
2.148 +type pblID = Celem3.pblID;
2.149 +val e_pblID = Celem3.e_pblID;
2.150 +type metID = Celem3.metID;
2.151 +type spec = Celem3.spec;
2.152 +val spec2str = Celem3.spec2str;
2.153 +val e_metID = Celem3.e_metID;
2.154 +val metID2str = Celem3.metID2str;
2.155 +val empty_spec = Celem3.empty_spec;
2.156 +val e_spec = Celem3.e_spec;
2.157 (*\------- to Celem3 -------/*)
2.158
2.159 (*/------- to Celem7 -------\*)
2.160 -(* association list with cas-commands, for generating a complete calc-head *)
2.161 -type generate_fn =
2.162 - (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
2.163 - (term * (* description of an element *)
2.164 - term list) (* value of the element (always put into a list) *)
2.165 - list) (* of elements in the formalization *)
2.166 -type cas_elem =
2.167 - (term * (* cas-command, eg. 'solve' *)
2.168 - (spec * (* theory, problem, method *)
2.169 - generate_fn))
2.170 -fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
2.171 +type cas_elem = Celem7.cas_elem;
2.172 +val cas_eq = Celem7.cas_eq;
2.173 (*\------- to Celem7 -------/*)
2.174
2.175 (*either theID or pblID or metID*)
2.176 @@ -237,128 +215,25 @@
2.177 (*\------- to Celem1 -------/*)
2.178
2.179 (*/------- to Celem8 -------\*)
2.180 -(*the key into the hierarchy ob theory elements*)
2.181 -type theID = string list;
2.182 -val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
2.183 -fun theID2thyID theID =
2.184 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
2.185 - else error ("theID2thyID called with " ^ theID2str theID);
2.186 -type authors = string list;
2.187 -(* datatype for collecting thydata for hierarchy *)
2.188 -(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
2.189 -datatype thydata =
2.190 - Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
2.191 -| Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
2.192 - thm: thm} (* here no sym_thm, thus no thmID required *)
2.193 -| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
2.194 -| Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
2.195 -| Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
2.196 - ord: (UnparseC.subst -> (term * term) -> bool)};
2.197 -fun the2str (Html {guh, ...}) = guh
2.198 - | the2str (Hthm {guh, ...}) = guh
2.199 - | the2str (Hrls {guh, ...}) = guh
2.200 - | the2str (Hcal {guh, ...}) = guh
2.201 - | the2str (Hord {guh, ...}) = guh
2.202 -fun thes2str thes = map the2str thes |> list2str;
2.203 -(*\------- to Celem8 -------/*)
2.204 +type authors = Celem8.authors;
2.205 +datatype thydata = datatype Celem8.thydata;
2.206 +type theID = Celem8.theID;
2.207 +val theID2str = Celem8.theID2str;
2.208 +val the2str = Celem8.the2str;
2.209 +val thes2str = Celem8.thes2str;
2.210 +val theID2thyID = Celem8.theID2thyID;
2.211
2.212 -(*/------- to Celem8 -------\*)
2.213 -(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
2.214 - (a): thehier does not contain sym_thmID theorems
2.215 - (b): lookup for sym_thmID directly from Isabelle using sym_thm
2.216 - (within math-engine NO lookup in thehier -- within java in *.xml only!)
2.217 -TODO (c): export from thehier to xml
2.218 -TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
2.219 -TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
2.220 -TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
2.221 - stands for both, "thmID" and "sym_thmID"
2.222 -TODO (d1) lookup from calctxt
2.223 -TODO (d1) lookup from from rule set in MiniBrowser *)
2.224 -type thehier = (thydata Celem1.ptyp) list;
2.225 -(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
2.226 -fun part2guh [str] = (case str of
2.227 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
2.228 - | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
2.229 - | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
2.230 - | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
2.231 - | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
2.232 +val part2guh = Celem8.part2guh;
2.233 +val thy2guh = Celem8.thy2guh;
2.234 +val thypart2guh = Celem8.thypart2guh;
2.235 +val thm2guh = Celem8.thm2guh;
2.236 +val rls2guh = Celem8.rls2guh;
2.237 +val cal2guh = Celem8.cal2guh;
2.238 +val ord2guh = Celem8.ord2guh;
2.239 +val theID2guh = Celem8.theID2guh;
2.240
2.241 -fun thy2guh [part, thyID] = (case part of
2.242 - "Isabelle" => "thy_isab_" ^ thyID
2.243 - | "IsacScripts" => "thy_scri_" ^ thyID
2.244 - | "IsacKnowledge" => "thy_isac_" ^ thyID
2.245 - | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
2.246 - | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
2.247 -
2.248 -fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
2.249 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
2.250 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
2.251 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
2.252 - | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
2.253 - | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
2.254 -
2.255 -
2.256 -(* convert the data got via contextToThy to a globally unique handle.
2.257 - there is another way to get the guh: get out of the 'theID' in the hierarchy *)
2.258 -fun thm2guh (isa, thyID) thmID = case isa of
2.259 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : guh
2.260 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
2.261 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
2.262 - | _ => raise ERROR
2.263 - ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
2.264 -
2.265 -fun rls2guh (isa, thyID) rls' = case isa of
2.266 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : guh
2.267 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
2.268 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
2.269 - | _ => raise ERROR
2.270 - ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
2.271 -
2.272 -fun cal2guh (isa, thyID) calID = case isa of
2.273 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : guh
2.274 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
2.275 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
2.276 - | _ => raise ERROR
2.277 - ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
2.278 -
2.279 -fun ord2guh (isa, thyID) rew_ord' = case isa of
2.280 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : guh
2.281 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
2.282 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
2.283 - | _ => raise ERROR
2.284 - ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
2.285 -
2.286 -(* not only for thydata, but also for thy's etc *)
2.287 -(* TODO
2.288 -fun theID2guh theID = case length theID of
2.289 - 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
2.290 - | 1 => part2guh theID
2.291 - | 2 => thy2guh theID
2.292 - | 3 => thypart2guh theID
2.293 - | 4 =>
2.294 - let val [isa, thyID, typ, elemID] = theID
2.295 - in case typ of
2.296 - "Theorems" => thm2guh (isa, thyID) elemID
2.297 - | "Rulesets" => rls2guh (isa, thyID) elemID
2.298 - | "Calculations" => cal2guh (isa, thyID) elemID
2.299 - | "Orders" => ord2guh (isa, thyID) elemID
2.300 - | "Theorems" => thy2guh [isa, thyID]
2.301 - | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
2.302 - end
2.303 - | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
2.304 -*)
2.305 -(* not only for thydata, but also for thy's etc *)
2.306 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
2.307 - | theID2guh [str] = part2guh [str]
2.308 - | theID2guh [s1, s2] = thy2guh [s1, s2]
2.309 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
2.310 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
2.311 - "Theorems" => thm2guh (isa, thyID) elemID
2.312 - | "Rulesets" => rls2guh (isa, thyID) elemID
2.313 - | "Calculations" => cal2guh (isa, thyID) elemID
2.314 - | "Orders" => ord2guh (isa, thyID) elemID
2.315 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
2.316 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
2.317 +val add_thydata = Celem8.add_thydata;
2.318 +val update_hthm = Celem8.update_hthm;
2.319 (*\------- to Celem8 -------/*)
2.320
2.321 type filepath = string;
2.322 @@ -394,16 +269,9 @@
2.323
2.324 (*/------- to Celem4 -------\*)
2.325 (* the pattern for an item of a problems model or a methods guard *)
2.326 -type pat =
2.327 - (string * (* field *)
2.328 - (term * (* description *)
2.329 - term)) (* id | arbitrary term *);
2.330 -fun pat2str ((field, (dsc, id)) : pat) =
2.331 - pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id))
2.332 -fun pats2str pats = (strs2str o (map pat2str)) pats
2.333 -fun pat2str' ((field, (dsc, id)) : pat) =
2.334 - pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n"
2.335 -fun pats2str' pats = (strs2str o (map pat2str')) pats
2.336 +type pat = Celem4.pat;
2.337 +val pats2str = Celem4.pats2str;
2.338 +val pats2str' = Celem4.pats2str';
2.339 (*\------- to Celem4 -------/*)
2.340
2.341 (* types for problems models (TODO rename to specification models) *)
2.342 @@ -412,108 +280,26 @@
2.343 (term * (* description *)
2.344 term)); (* id | struct-var *)
2.345 (*/------- to Celem5 -------\*)
2.346 -type pbt =
2.347 - {guh : guh, (* unique within this isac-knowledge *)
2.348 - mathauthors : string list, (* copyright *)
2.349 - init : pblID, (* to start refinement with *)
2.350 - thy : theory, (* which allows to compile that pbt
2.351 - TODO: search generalized for subthy (ref.p.69*)
2.352 - (*^^^ WN050912 NOT used during application of the problem,
2.353 - because applied terms may be from 'subthy' as well as from super;
2.354 - thus we take 'maxthy'; see match_ags ! *)
2.355 - cas : term option, (* 'CAS-command' *)
2.356 - met : metID list, (* methods solving the pbt *)
2.357 -(*TODO: abstract to ?pre_model?...*)
2.358 - prls : Rule_Set.T, (* for preds in where_ *)
2.359 - where_ : term list, (* where - predicates *)
2.360 - ppc : pat list (* this is the model-pattern;
2.361 - it contains "#Given","#Where","#Find","#Relate"-patterns
2.362 - for constraints on identifiers see "fun cpy_nam" *)
2.363 -}
2.364 -
2.365 -val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
2.366 - cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
2.367 -fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
2.368 - prls = prls', thy = thy', where_ = w'} : pbt)
2.369 - = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
2.370 - ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
2.371 - ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
2.372 - ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
2.373 - ^ (UnparseC.terms w') ^ "}" |> linefeed;
2.374 -fun pbts2str pbts = map pbt2str pbts |> list2str;
2.375 -(*\------- to Celem5 -------/*)
2.376 -
2.377 -(*/------- to Celem5 -------\*)
2.378 -val e_Ptyp = Celem1.Ptyp ("e_pblID", [e_pbt], [])
2.379 -type ptyps = (pbt Celem1.ptyp) list
2.380 +type pbt = Celem5.pbt;
2.381 +val e_pbt = Celem5.e_pbt;
2.382 +val e_Ptyp = Celem5.e_Ptyp;
2.383 +val pbts2str = Celem5.pbts2str;
2.384 +type ptyps = Celem5.ptyps;
2.385 (*\------- to Celem5 -------/*)
2.386
2.387 (*/------- to Celem6 -------\*)
2.388 -(* data for methods stored in 'methods'-database*)
2.389 -type met =
2.390 - {guh : guh, (* unique within this isac-knowledge *)
2.391 - mathauthors: string list, (* copyright *)
2.392 - init : pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
2.393 - rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
2.394 - TODO.WN0509 store fun itself, see 'type pbt' *)
2.395 - erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
2.396 - instead erls in "fun prep_met" *)
2.397 - srls : Rule_Set.T, (* for evaluating list expressions in scr *)
2.398 - crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
2.399 - nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
2.400 - errpats : Error_Fill_Def.errpat list,(* error patterns expected in this method *)
2.401 - calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
2.402 - (*branch : TransitiveB set in append_problem at generation ob pblobj *)
2.403 - scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
2.404 -(*TODO: abstract to ?pre_model?...*)
2.405 - prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
2.406 - ppc : pat list, (* items in given, find, relate;
2.407 - items (in "#Find") which need not occur in the arg-list of a SubProblem
2.408 - are 'copy-named' with an identifier "*'.'".
2.409 - copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
2.410 - see ME/calchead.sml 'fun is_copy_named'. *)
2.411 - pre : term list (* preconditions in where *)
2.412 - };
2.413 -val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
2.414 - erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
2.415 - errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
2.416 -val e_Mets = Celem1.Ptyp ("e_metID", [e_met],[]);
2.417 -
2.418 +type met = Celem6.met;
2.419 +val e_met = Celem6.e_met;
2.420 +val e_Mets = Celem6.e_Mets;
2.421 type mets = (met Celem1.ptyp) list;
2.422 (*\------- to Celem6 -------/*)
2.423
2.424 (*/------- to Celem91 -------\*)
2.425 -(* switch for checking guhs unique before storing a pbl or met;
2.426 - set true at startup (done at begin of ROOT.ML)
2.427 - set false for editing IsacKnowledge (done at end of ROOT.ML) *)
2.428 -val check_guhs_unique = Unsynchronized.ref true;
2.429 -
2.430 -fun coll_pblguhs pbls =
2.431 - let
2.432 - fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : pbt -> guh) n] @ (nodes coll ns)
2.433 - | node _ _ = raise ERROR "coll_pblguhs - node"
2.434 - and nodes coll [] = coll
2.435 - | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
2.436 - in nodes [] pbls end;
2.437 -fun check_pblguh_unique guh pbls =
2.438 - if member op = (coll_pblguhs pbls) guh
2.439 - then error ("check_guh_unique failed with \""^ guh ^"\";\n"^
2.440 - "use \"sort_pblguhs()\" for a list of guhs;\n"^
2.441 - "consider setting \"check_guhs_unique := false\"")
2.442 - else ();
2.443 -fun coll_metguhs mets =
2.444 - let
2.445 - fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : met -> guh) n] @ (nodes coll ns)
2.446 - | node _ _ = raise ERROR "coll_pblguhs - node"
2.447 - and nodes coll [] = coll
2.448 - | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
2.449 - in nodes [] mets end;
2.450 -fun check_metguh_unique (guh:guh) (mets: (met Celem1.ptyp) list) =
2.451 - if member op = (coll_metguhs mets) guh
2.452 - then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
2.453 - (*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
2.454 - "consider setting \"check_guhs_unique := false\"")
2.455 - else ();
2.456 +val check_guhs_unique = Celem91.check_guhs_unique;
2.457 +val coll_pblguhs = Celem91.coll_pblguhs;
2.458 +val check_pblguh_unique = Celem91.check_pblguh_unique;
2.459 +val coll_metguhs = Celem91.coll_metguhs;
2.460 +val check_metguh_unique = Celem91.check_metguh_unique;
2.461 (*\------- to Celem91 -------/*)
2.462
2.463 (*/------- to Celem8 -------\*)
3.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 12:22:37 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 15:37:39 2020 +0200
3.3 @@ -10,9 +10,11 @@
3.4 (*/------- to Celem5 -------\*)
3.5 type pbt
3.6 type ptyps
3.7 + val pbts2str: pbt list -> string
3.8 + val e_Ptyp: pbt Celem1.ptyp
3.9 (*\------- to Celem5 -------/*)
3.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.11 - (*NONE*)
3.12 + val e_pbt: pbt
3.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.14 (*NONE*)
3.15 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.1 --- a/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 12:22:37 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 15:37:39 2020 +0200
4.3 @@ -8,8 +8,9 @@
4.4 (*\------- to Celem6 -------/*)
4.5 sig
4.6 (*/------- to Celem6 -------\*)
4.7 + type met
4.8 + val e_met: met
4.9 type mets
4.10 - type met
4.11 val e_Mets: met Celem1.ptyp
4.12 (*\------- to Celem6 -------/*)
4.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 12:22:37 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 15:37:39 2020 +0200
5.3 @@ -16,9 +16,20 @@
5.4 | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Celem2.guh, mathauthors: authors, thm: thm}
5.5 | Html of {coursedesign: authors, guh: Celem2.guh, html: string, mathauthors: authors}
5.6 type theID
5.7 + val theID2str: string list -> string
5.8 val the2str: thydata -> string
5.9 val thes2str: thydata list -> string
5.10 val theID2thyID: theID -> ThyC.id
5.11 +
5.12 + val part2guh: theID -> Celem2.guh
5.13 + val thy2guh: theID -> Celem2.guh
5.14 + val thypart2guh: theID -> Celem2.guh
5.15 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Celem2.guh
5.16 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Celem2.guh
5.17 + val cal2guh: string * ThyC.id -> string -> Celem2.guh
5.18 + val ord2guh: string * ThyC.id -> string -> Celem2.guh
5.19 + val theID2guh: theID -> Celem2.guh
5.20 +
5.21 val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list
5.22 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
5.23 (*\------- to Celem8 -------/*)
6.1 --- a/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 12:22:37 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 15:37:39 2020 +0200
6.3 @@ -11,6 +11,8 @@
6.4 val check_guhs_unique: bool Unsynchronized.ref
6.5 val check_pblguh_unique: Celem2.guh -> Celem5.pbt Celem1.ptyp list -> unit
6.6 val check_metguh_unique: Celem2.guh -> Celem6.met Celem1.ptyp list -> unit
6.7 + val coll_pblguhs: Celem5.pbt Celem1.ptyp list -> Celem2.guh list
6.8 + val coll_metguhs: Celem6.met Celem1.ptyp list -> Celem2.guh list
6.9 (*\------- to Celem91 -------/*)
6.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.11 (*NONE*)
7.1 --- a/src/Tools/isac/BaseDefinitions/celem-92.sml Sun Apr 19 12:22:37 2020 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,25 +0,0 @@
7.4 -(* Title: BaseDefinitions/celem-92.sml
7.5 - Author: Walther Neuper
7.6 - (c) due to copyright terms
7.7 -
7.8 - *)
7.9 -signature CALCELEMENT_92 =
7.10 -(*/------- to Celem92 -------\*)
7.11 -(*\------- to Celem92 -------/*)
7.12 -sig
7.13 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.14 - (*NONE*)
7.15 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.16 - (*NONE*)
7.17 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.18 -end
7.19 -
7.20 -(**)
7.21 -structure Celem92(**): CALCELEMENT_92(**) =
7.22 -struct
7.23 -(**)
7.24 -
7.25 -(*/------- to Celem92 -------\*)
7.26 -(*\------- to Celem92 -------/*)
7.27 -
7.28 -(**)end(**)
8.1 --- a/src/Tools/isac/BaseDefinitions/celem-93.sml Sun Apr 19 12:22:37 2020 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,26 +0,0 @@
8.4 -(* Title: BaseDefinitions/celem-93.sml
8.5 - Author: Walther Neuper
8.6 - (c) due to copyright terms
8.7 -
8.8 - *)
8.9 -signature CALCELEMENT_93 =
8.10 -(*/------- to Celem93 -------\*)
8.11 -(*\------- to Celem93 -------/*)
8.12 -sig
8.13 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.14 - (*NONE*)
8.15 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.16 - (*NONE*)
8.17 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.18 -end
8.19 -
8.20 -
8.21 -(**)
8.22 -structure Celem93(**): CALCELEMENT_93(**) =
8.23 -struct
8.24 -(**)
8.25 -
8.26 -(*/------- to Celem93 -------\*)
8.27 -(*\------- to Celem93 -------/*)
8.28 -
8.29 -(**)end(**)
9.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sun Apr 19 12:22:37 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sun Apr 19 15:37:39 2020 +0200
9.3 @@ -14,7 +14,11 @@
9.4 ML_file interface.sml
9.5
9.6 ML \<open>
9.7 +open Celem6
9.8 \<close> ML \<open>
9.9 +val e_met = {guh = "met_empty", mathauthors = [], init = Celem3.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
9.10 + erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
9.11 + errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
9.12 \<close> ML \<open>
9.13 \<close>
9.14 end
9.15 \ No newline at end of file