1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Fri Jan 06 10:50:33 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Fri Jan 06 11:32:57 2023 +0100
1.3 @@ -42,7 +42,6 @@
1.4 ML_file "method-def.sml"
1.5 ML_file "formalise.sml"
1.6 ML_file "example.sml"
1.7 -ML_file "thy-write.sml"
1.8
1.9 ML \<open>
1.10 \<close> ML \<open>
1.11 @@ -84,9 +83,6 @@
1.12 val add_mets: Proof.context -> (Meth_Def.T * References_Def.id) list -> theory -> theory
1.13 val get_expls: theory -> Example.store
1.14 val add_expls: (Example.T * Store.key) list -> theory -> theory
1.15 - val get_thes: theory -> (Thy_Write.thydata Store.node) list
1.16 - val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory
1.17 - val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.18 val get_ref_last_thy: unit -> theory
1.19 val set_ref_last_thy: theory -> unit
1.20 val get_via_last_thy: ThyC.id -> theory (*only used for (Sub-)problem retrieving respective thy*)
1.21 @@ -165,25 +161,6 @@
1.22 fun add_expl (expl, expl_id) = Store.insert expl_id expl expl_id;
1.23 in Data.map (fold add_expl expls) thy end;
1.24
1.25 - structure Data = Theory_Data (
1.26 - type T = (Thy_Write.thydata Store.node) list;
1.27 - val empty = [];
1.28 - val merge = Store.merge;
1.29 - );
1.30 - fun get_thes thy = Data.get thy
1.31 - fun add_thes thes thy = let
1.32 - fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
1.33 - in Data.map (fold add_the thes) thy end;
1.34 - fun insert_fillpats fis thy =
1.35 - let
1.36 - fun update_elem (theID, fillpats) =
1.37 - let
1.38 - val hthm = Store.get (Data.get thy) theID theID
1.39 - val hthm' = Thy_Write.update_hthm hthm fillpats
1.40 - handle ERROR _ =>
1.41 - raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.42 - in Store.update theID theID hthm' end
1.43 - in Data.map (fold update_elem fis) thy end
1.44
1.45 val last_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.46 fun set_ref_last_thy thy = Synchronized.change last_thy (fn _ => thy); (* never RE-set ! *)
1.47 @@ -322,7 +299,6 @@
1.48
1.49 fun get_pbls () = get_ref_last_thy () |> Know_Store.get_pbls;
1.50 fun get_mets () = get_ref_last_thy () |> Know_Store.get_mets;
1.51 -fun get_thes () = get_ref_last_thy () |> Know_Store.get_thes;
1.52 fun get_expls () = get_ref_last_thy () |> Know_Store.get_expls;
1.53 \<close>
1.54
1.55 @@ -330,17 +306,6 @@
1.56 empty = \<open>Rule_Set.empty\<close> and
1.57 e_rrls = \<open>Rule_Set.e_rrls\<close>
1.58
1.59 -section \<open>determine sequence of main parts in thehier\<close>
1.60 -setup \<open>
1.61 -Know_Store.add_thes
1.62 - [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
1.63 - mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
1.64 - (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
1.65 - mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
1.66 - (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
1.67 - mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
1.68 -\<close>
1.69 -
1.70 section \<open>Functions for checking Know_Store\<close>
1.71 ML \<open>
1.72 fun short_string_of_rls Rule_Set.Empty = "Erls"
1.73 @@ -380,14 +345,8 @@
1.74 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.75 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
1.76 val sort_kestore_met = sort_kestore_ptyp' met_ord;
1.77 +\<close>
1.78
1.79 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
1.80 -fun write_thes thydata_list =
1.81 - thydata_list
1.82 - |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
1.83 - |> map pair2str
1.84 - |> map writeln
1.85 -\<close>
1.86 ML \<open>
1.87 \<close> ML \<open>
1.88 \<close> ML \<open>
2.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Fri Jan 06 10:50:33 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Fri Jan 06 11:32:57 2023 +0100
2.3 @@ -2,7 +2,7 @@
2.4 Author: Walther Neuper
2.5 (c) due to copyright terms
2.6
2.7 -A tree for storing collections of Problem, MethodC and Thy_Write.
2.8 +A tree for storing collections of Problem and MethodC.
2.9 *)
2.10 signature STORE_TREE =
2.11 sig
3.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml Fri Jan 06 10:50:33 2023 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,190 +0,0 @@
3.4 -(* Title: BaseDefinitions/celem-8.sml
3.5 - Author: Walther Neuper
3.6 - (c) due to copyright terms
3.7 -
3.8 -Here is a minimum of code required for Know_Store.thy.
3.9 -For main code see structure Thy_Write and structure Thy_Present.
3.10 -
3.11 -The latter is legacy for HTML representation of theory data in Isac's Java front end.
3.12 -*)
3.13 -signature THEORY_DATA_STORE_WRITE =
3.14 -sig
3.15 - type authors
3.16 - datatype thydata
3.17 - = Hcal of {calc: Rule_Def.eval_ml_from_prog, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
3.18 - | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rewrite_Ord.function}
3.19 - | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
3.20 - | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
3.21 - | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
3.22 - type theID
3.23 - val theID2str: string list -> string
3.24 - val the2str: thydata -> string
3.25 - val thes2str: thydata list -> string
3.26 - val theID2thyID: theID -> ThyC.id
3.27 -
3.28 - val part2guh: theID -> Check_Unique.id
3.29 - val thy2guh: theID -> Check_Unique.id
3.30 - val thypart2guh: theID -> Check_Unique.id
3.31 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.id
3.32 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.id
3.33 - val cal2guh: string * ThyC.id -> string -> Check_Unique.id
3.34 - val ord2guh: string * ThyC.id -> string -> Check_Unique.id
3.35 - val theID2guh: theID -> Check_Unique.id
3.36 -
3.37 - val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
3.38 - val update_hthm: thydata -> Error_Pattern_Def.fill_in list -> thydata
3.39 -end
3.40 -
3.41 -(**)
3.42 -structure Thy_Write(**): THEORY_DATA_STORE_WRITE(**) =
3.43 -struct
3.44 -(**)
3.45 -
3.46 -(*the key into the hierarchy ob theory elements*)
3.47 -type theID = string list;
3.48 -val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
3.49 -fun theID2thyID theID =
3.50 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
3.51 - else raise ERROR ("theID2thyID called with " ^ theID2str theID);
3.52 -type authors = string list;
3.53 -(* datatype for collecting thydata for hierarchy *)
3.54 -(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
3.55 -datatype thydata =
3.56 - Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}
3.57 -| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
3.58 - thm: thm} (* here no sym_thm, thus no thmID required *)
3.59 -| Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
3.60 -| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.eval_ml_from_prog}
3.61 -| Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
3.62 - ord: (Proof.context -> subst -> (term * term) -> bool)};
3.63 -fun the2str (Html {guh, ...}) = guh
3.64 - | the2str (Hthm {guh, ...}) = guh
3.65 - | the2str (Hrls {guh, ...}) = guh
3.66 - | the2str (Hcal {guh, ...}) = guh
3.67 - | the2str (Hord {guh, ...}) = guh
3.68 -fun thes2str thes = map the2str thes |> list2str;
3.69 -
3.70 -(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
3.71 - (a): thehier does not contain sym_thmID theorems
3.72 - (b): lookup for sym_thmID directly from Isabelle using sym_thm
3.73 - (within math-engine NO lookup in thehier -- within java in *.xml only!)
3.74 -TODO (c): export from thehier to xml
3.75 -TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
3.76 -TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
3.77 -TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
3.78 - stands for both, "thmID" and "sym_thmID"
3.79 -TODO (d1) lookup from calctxt
3.80 -TODO (d1) lookup from from rule set in MiniBrowser *)
3.81 -type thehier = (thydata Store.node) list;
3.82 -(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
3.83 -fun part2guh [str] = (case str of
3.84 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.id
3.85 - | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
3.86 - | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
3.87 - | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
3.88 - | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
3.89 -
3.90 -fun thy2guh [part, thyID] = (case part of
3.91 - "Isabelle" => "thy_isab_" ^ thyID
3.92 - | "IsacScripts" => "thy_scri_" ^ thyID
3.93 - | "IsacKnowledge" => "thy_isac_" ^ thyID
3.94 - | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
3.95 - | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
3.96 -
3.97 -fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
3.98 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.id
3.99 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
3.100 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
3.101 - | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
3.102 - | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
3.103 -
3.104 -
3.105 -(* convert the data got via contextToThy to a globally unique handle.
3.106 - there is another way to get the guh: get out of the 'theID' in the hierarchy *)
3.107 -fun thm2guh (isa, thyID) thmID = case isa of
3.108 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.id
3.109 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
3.110 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
3.111 - | _ => raise ERROR
3.112 - ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
3.113 -
3.114 -fun rls2guh (isa, thyID) rls' = case isa of
3.115 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.id
3.116 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
3.117 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
3.118 - | _ => raise ERROR
3.119 - ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
3.120 -
3.121 -fun cal2guh (isa, thyID) calID = case isa of
3.122 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.id
3.123 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
3.124 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
3.125 - | _ => raise ERROR
3.126 - ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
3.127 -
3.128 -fun ord2guh (isa, thyID) rew_ord = case isa of
3.129 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord : Check_Unique.id
3.130 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord
3.131 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord
3.132 - | _ => raise ERROR
3.133 - ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord ^ "\"");
3.134 -
3.135 -(* TODO
3.136 -fun theID2guh theID = case length theID of
3.137 - 0 => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
3.138 - | 1 => part2guh theID
3.139 - | 2 => thy2guh theID
3.140 - | 3 => thypart2guh theID
3.141 - | 4 =>
3.142 - let val [isa, thyID, typ, elemID] = theID
3.143 - in case typ of
3.144 - "Theorems" => thm2guh (isa, thyID) elemID
3.145 - | "Rulesets" => rls2guh (isa, thyID) elemID
3.146 - | "Calculations" => cal2guh (isa, thyID) elemID
3.147 - | "Orders" => ord2guh (isa, thyID) elemID
3.148 - | "Theorems" => thy2guh [isa, thyID]
3.149 - | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
3.150 - end
3.151 - | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
3.152 -*)
3.153 -(* not only for thydata, but also for thy's etc *)
3.154 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
3.155 - | theID2guh [str] = part2guh [str]
3.156 - | theID2guh [s1, s2] = thy2guh [s1, s2]
3.157 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
3.158 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
3.159 - "Theorems" => thm2guh (isa, thyID) elemID
3.160 - | "Rulesets" => rls2guh (isa, thyID) elemID
3.161 - | "Calculations" => cal2guh (isa, thyID) elemID
3.162 - | "Orders" => ord2guh (isa, thyID) elemID
3.163 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
3.164 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
3.165 -
3.166 -fun Html_default exist = (Html {guh = theID2guh exist,
3.167 - coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
3.168 -
3.169 -fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
3.170 - | fill_parents (exist, i :: is) thydata =
3.171 - Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
3.172 - | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
3.173 -
3.174 -fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
3.175 - | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) =
3.176 - if i = key
3.177 - then pys (* preserve existing thydata *)
3.178 - else py :: add_thydata (exist, [i]) data pyss
3.179 - | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
3.180 - if i = key
3.181 - then
3.182 - if length pys = 0
3.183 - then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
3.184 - else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
3.185 - else py :: add_thydata (exist, iss) data pyss
3.186 - | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
3.187 -
3.188 -fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
3.189 - Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
3.190 - fillpats = fillpats', thm = thm}
3.191 - | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
3.192 -
3.193 -(**)end(**)
4.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Jan 06 10:50:33 2023 +0100
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Jan 06 11:32:57 2023 +0100
4.3 @@ -8,14 +8,6 @@
4.4
4.5 (*** convert sml-datatypes to xml for kbase ***)
4.6
4.7 -fun calc2xml j (thyID, (scrop, (rewop, _))) =
4.8 - indt j ^ "<CALC>\n" ^
4.9 - indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
4.10 - indt (j+i) ^ "<GUH>\n" ^ Thy_Write.cal2guh ("IsacKnowledge",
4.11 - thyID) scrop ^ "</GUH>\n" ^
4.12 - indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
4.13 - indt j ^ "</CALC>\n";
4.14 -
4.15 fun filterpbl str =
4.16 let fun filt [] = []
4.17 | filt ((s, (t1, t2)) :: ps) =
4.18 @@ -44,16 +36,6 @@
4.19 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
4.20 (indt j) ^ "</RELATE>\n");
4.21
4.22 -fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
4.23 - indt j ^ "<CALCREF>\n" ^
4.24 - indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
4.25 - indt (j+i) ^ "<GUH> " ^ Thy_Write.cal2guh ("IsacKnowledge",
4.26 - thyID) scrop ^ " </GUH>\n" ^
4.27 - indt j ^ "</CALCREF>\n";
4.28 -fun calcrefs2xml _ (_,[]) = ""
4.29 - | calcrefs2xml j (thyID, cal::cs) =
4.30 - calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
4.31 -
4.32 fun prepa12xml j (terms, term) =
4.33 indt j ^"<PREPAT>\n"^
4.34 indt (j+i) ^"<PRECONDS>\n"^
4.35 @@ -283,27 +265,6 @@
4.36 XML.Elem (("ASM", []), [xml_of_term asm]),
4.37 XML.Elem (("VALUE", []), [xml_of_term vl])])
4.38
4.39 -(* reference to an element in the theory hierarchy *)
4.40 -fun theref2xml j thyID typ xstring =
4.41 - let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
4.42 - val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
4.43 - in indt j ^ "<KESTOREREF>\n" ^
4.44 - indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
4.45 - indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
4.46 - indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
4.47 - indt j ^ "</KESTOREREF>\n"
4.48 - end;
4.49 -fun xml_of_theref thyid typ xstring =
4.50 - let
4.51 - val guh = Thy_Write.theID2guh ["IsacKnowledge", thyid, typ, xstring]
4.52 - val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
4.53 - in
4.54 - XML.Elem (("KESTOREREF", []),[
4.55 - XML.Elem (("TAG", []), [XML.Text typ']),
4.56 - XML.Elem (("ID", []), [XML.Text xstring]),
4.57 - XML.Elem (("GUH", []), [XML.Text guh])])
4.58 - end
4.59 -
4.60 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, where_) =
4.61 XML.Elem (("CONTEXTDATA", []), [
4.62 XML.Elem (("GUH", []), [(XML.Text "would-need-ctxt")(*XML.Text (Ptool.pblID2guh pI)*)]),
5.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Jan 06 10:50:33 2023 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,189 +0,0 @@
5.4 -(* Title: "BridgeLibisabelle/thy-hierarchy.sml"
5.5 - Author: Walther Neuper 0601
5.6 - (c) due to copyright terms
5.7 -
5.8 -Tools to Build_Thydata of theorems and rule-sets defined in Knowledge/ and ProgLang/
5.9 -*)
5.10 -
5.11 -signature THEORY_HIERARCHY =
5.12 -sig
5.13 - val collect_cals: string * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
5.14 - val collect_isab: string -> string * thm -> Thy_Write.theID * Thy_Write.thydata
5.15 - val collect_ords: 'a * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
5.16 - val collect_part: string -> theory -> theory list -> (Thy_Write.theID * Thy_Write.thydata) list
5.17 - val collect_rlss: string -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory list ->
5.18 - (Thy_Write.theID * Thy_Write.thydata) list
5.19 - val collect_thms: string -> theory -> (Thy_Write.theID * Thy_Write.thydata) list
5.20 -
5.21 - val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->
5.22 - Thy_Write.thydata * Thy_Write.theID
5.23 -
5.24 - val thms_of_rls : Rule_Set.T -> Rule.rule list
5.25 - val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
5.26 - (string * thm) list
5.27 -
5.28 -\<^isac_test>\<open>
5.29 - val hierarchy_guh: 'a Store.T -> string
5.30 - val get_fun_ids: theory -> (string * typ) list
5.31 -\<close>
5.32 -end
5.33 -
5.34 -(**)
5.35 -structure Thy_Hierarchy(**): THEORY_HIERARCHY(**) =
5.36 -struct
5.37 -(**)
5.38 -open TermC (* allows contains_one_of to be infix *)
5.39 -
5.40 -fun fun_id_of ({program = prog, ...} : MethodC.T) =
5.41 - case prog of
5.42 - Rule.Empty_Prog => NONE
5.43 - | Rule.Prog t =>
5.44 - (case t of
5.45 - Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
5.46 - | _ => SOME (Program.get_fun_id t))
5.47 - | Rule.Rfuns _ => NONE
5.48 -fun get_fun_ids thy =
5.49 - let
5.50 - val mets = Store.get_all (Know_Store.get_mets thy)
5.51 - (* all mets of the respective theory PLUS of all ancestor theories*)
5.52 - val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
5.53 - in
5.54 - filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
5.55 - end
5.56 -
5.57 -(* copy from mutabelle_extra.ML, fun thms_of *)
5.58 -fun thms_of thy = (* das ist zu verbessern *)
5.59 - let
5.60 - val fun_ids = get_fun_ids thy
5.61 - in
5.62 - filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
5.63 - andalso not (thm contains_one_of fun_ids)
5.64 - andalso not (ThmC.id_of_thm thm = "mono"))
5.65 - (* created in Biegelinie by partial_function ^^^^^^*)
5.66 - (map snd (Global_Theory.all_thms_of thy false))
5.67 - end
5.68 -
5.69 -(* wrap theory-data into the uniform type thydata *)
5.70 -
5.71 -fun makeHthm (part : string, thyID : ThyC.id) (thm : thm) =
5.72 - let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Thy_Write.theID
5.73 - in (theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID, coursedesign = [],
5.74 - mathauthors = ["isac-team"], fillpats = [], thm = thm})
5.75 - end;
5.76 -fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, _): ThyC.id * Rule_Set.T) =
5.77 - let val theID = [part, thyID,"Rulesets"] @ [rls'] : Thy_Write.theID
5.78 - in (theID, Thy_Write.Hrls {guh = Thy_Write.theID2guh theID, coursedesign = [],
5.79 - mathauthors = ["isac-team"], thy_rls = thy_rls})
5.80 - end;
5.81 -fun makeHcal (part : string, thyID : ThyC.id) (calID, cal) =
5.82 - let val theID = [part, thyID,"Operations"] @ [calID] : Thy_Write.theID
5.83 - in (theID, Thy_Write.Hcal {guh = Thy_Write.theID2guh theID, coursedesign=[],
5.84 - mathauthors = ["isac-team"], calc = cal})
5.85 - end;
5.86 -
5.87 -(* get all theorems in a rule set (recursivley containing rule sets) *)
5.88 -fun thm_of_rule Rule.Erule = []
5.89 - | thm_of_rule (thm as Rule.Thm _) = [thm]
5.90 - | thm_of_rule (Rule.Eval _) = []
5.91 - | thm_of_rule (Rule.Cal1 _) = []
5.92 - | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
5.93 -and thms_of_rls Rule_Set.Empty = []
5.94 - | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules
5.95 - | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
5.96 - | thms_of_rls (Rule_Set.Rrls _) = []
5.97 -
5.98 -(* get all theorems from the list of rule-sets (defined in Knowledge) *)
5.99 -fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
5.100 - |> map (thms_of_rls o #2 o #2)
5.101 - |> flat
5.102 - |> map (ThmC.revert_sym_rule thy)
5.103 - |> map (fn Rule.Thm (thmID, thm) => (thmID, thm)
5.104 - | _ => raise ERROR "thms_of_rlss: uncovered case")
5.105 - |> distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
5.106 - : ThmC.T list
5.107 -
5.108 -(* collect all thydata defined in in a theory *)
5.109 -
5.110 -fun collect_thms part thy =
5.111 - map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
5.112 -fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
5.113 - |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
5.114 - |> map (makeHrls part)
5.115 -fun collect_cals (part, thy') =
5.116 - let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
5.117 - in map (makeHcal (part, thy')) cals end;
5.118 -fun collect_ords (_, _) =
5.119 - [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list
5.120 -
5.121 -(* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)
5.122 -fun collect_part part parent thys =
5.123 - (flat (map (collect_thms part) thys)) @
5.124 - (collect_rlss part (Know_Store.get_rlss parent) thys) @
5.125 - [(*TODO: collect_cals, collect_ords*)]
5.126 -
5.127 -(* collect theorems defined in Isabelle *)
5.128 -fun collect_isab isa (thmDeriv, thm) =
5.129 - let val theID =
5.130 - [isa, ThyC.cut_id thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
5.131 - in
5.132 - (theID: Thy_Write.theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID,
5.133 - mathauthors = ["Isabelle team, TU Munich"],
5.134 - coursedesign = [],
5.135 - fillpats = [],
5.136 - thm = thm})
5.137 - end
5.138 -
5.139 -
5.140 -(* for dialog-authoring *)
5.141 -fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
5.142 - let
5.143 - val rls' =
5.144 - case rls of
5.145 - Rule_Def.Repeat {id, preconds, rew_ord, asm_rls, prog_rls, calc, rules, program, ...}
5.146 - => Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls,
5.147 - calc = calc, rules = rules, program = program, errpatts = errpatIDs}
5.148 - | Rule_Set.Sequence {id, preconds, rew_ord, asm_rls, prog_rls, calc, rules, program, ...}
5.149 - => Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls,
5.150 - calc = calc, rules = rules, program = program, errpatts = errpatIDs}
5.151 - | Rule_Set.Rrls {id, prepat, rew_ord, asm_rls, calc, program, ...}
5.152 - => Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, asm_rls = asm_rls, calc = calc,
5.153 - program = program, errpatts = errpatIDs}
5.154 - | Erls => Erls
5.155 - in
5.156 - Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
5.157 - thy_rls = (thyID, rls')}
5.158 - end
5.159 - | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
5.160 -
5.161 -fun insert_errpatIDs _(*thy*) theID errpatIDs = (* TODO: redo like insert_fillpatts *)
5.162 - let
5.163 - val hrls = Thy_Read.for_thy_hierarchy theID
5.164 - val hrls' = update_hrls hrls errpatIDs
5.165 - handle ERROR _ => raise ERROR ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
5.166 - in (hrls', theID) end
5.167 -
5.168 -(*keep tests of interaction Java-frontend <-> Kernel running*)
5.169 -\<^isac_test>\<open>
5.170 -(* create an xml-hierarchy where the filname is created from the guh *)
5.171 -val indentation = 2;
5.172 -fun hierarchy_guh h =
5.173 - let
5.174 - val j = indentation
5.175 - fun node i p theID (Store.Node (id, _, ns)) =
5.176 - let
5.177 - val p' = Pos.lev_on p
5.178 - val theID' = theID @ [id]
5.179 - in
5.180 - (indt i) ^ "<NODE>\n" ^
5.181 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
5.182 - (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
5.183 - (indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Write.theID2guh theID' ^ " </CONTENTREF>\n" ^
5.184 - (nodes (i+j) (Pos.lev_dn p') theID' ns) ^
5.185 - (indt i) ^ "</NODE>\n"
5.186 - end
5.187 - and nodes _ _ _ [] = ""
5.188 - | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);
5.189 - in nodes j [0] [] h end;
5.190 -\<close>
5.191 -
5.192 -(**)end(**)
6.1 --- a/src/Tools/isac/Interpret/thy-read.sml Fri Jan 06 10:50:33 2023 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,127 +0,0 @@
6.4 -(* Interpret/thy-read.sml
6.5 - authors: Walther Neuper 2002, 2006
6.6 - (c) due to copyright terms
6.7 -
6.8 -tools for rewriting, reverse rewriting, context to thy concerning rewriting
6.9 -*)
6.10 -
6.11 -signature THEORY_STORE_READ =
6.12 -sig
6.13 - val thy_containing_thm : string -> string * ThmC.id
6.14 - val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
6.15 - val thy_containing_cal : ThyC.id -> Eval_Def.prog_id -> string * string
6.16 -
6.17 - val for_thy_hierarchy : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
6.18 - val from_store : Proof.context -> Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
6.19 -(*from isac_test for Minisubpbl*)
6.20 - val partID': ThyC.id -> string
6.21 -
6.22 -\<^isac_test>\<open>
6.23 - val isabthys: unit -> theory list
6.24 - val knowthys: unit -> theory list
6.25 -\<close>
6.26 -end
6.27 -(**)
6.28 -structure Thy_Read(**): THEORY_STORE_READ(**) =
6.29 -struct
6.30 -(**)
6.31 -
6.32 -(*
6.33 - group the theories defined in Isac for generation of the tree(!) of theories,
6.34 - compare Build_Thydata: section "Get and group the theories defined in Isac"
6.35 -*)
6.36 -fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
6.37 - let
6.38 - val allthys = Theory.ancestors_of (ThyC.get_theory "Build_Thydata")
6.39 - in
6.40 - drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys)
6.41 - end
6.42 -fun knowthys () = (*["Isac_Knowledge", .., "Input_Descript"]*)
6.43 - let
6.44 - fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
6.45 - let
6.46 - val allthys = filter_out (member Context.eq_thy
6.47 - [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
6.48 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
6.49 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
6.50 - in
6.51 - take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys),
6.52 - allthys)
6.53 - end
6.54 - val isacthys' = isacthys ()
6.55 - val proglang_parent = ThyC.get_theory "ProgLang"
6.56 - in
6.57 - take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
6.58 - end
6.59 -fun progthys () = (*["Isac_Knowledge", .., "Input_Descript"]*)
6.60 - let
6.61 - fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
6.62 - let
6.63 - val allthys = filter_out (member Context.eq_thy
6.64 - [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
6.65 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
6.66 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
6.67 - in
6.68 - take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys),
6.69 - allthys)
6.70 - end
6.71 - val isacthys' = isacthys ()
6.72 - val proglang_parent = ThyC.get_theory "ProgLang"
6.73 - in
6.74 - drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
6.75 - end
6.76 -fun partID thy =
6.77 - if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
6.78 - else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
6.79 - else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
6.80 - else raise ERROR ("closure of thys in Isac is broken by " ^ Context.theory_name thy)
6.81 -fun partID' thy' = partID (ThyC.get_theory thy')
6.82 -
6.83 -fun thy_containing_thm thmDeriv =
6.84 - let
6.85 - val isabthys' = map Context.theory_name (isabthys ());
6.86 - in
6.87 - if member op= isabthys' (ThyC.cut_id thmDeriv)
6.88 - then ("Isabelle", ThyC.cut_id thmDeriv)
6.89 - else ("IsacKnowledge", ThyC.cut_id thmDeriv)
6.90 - end
6.91 -
6.92 -(* which theory in ancestors of thy' contains a ruleset *)
6.93 -fun thy_containing_rls thy' rls' =
6.94 - let
6.95 - val thy = ThyC.get_theory thy'
6.96 - in
6.97 - case AList.lookup op= (Know_Store.get_rlss thy) rls' of
6.98 - SOME (thy'', _) => (partID' thy'', thy'')
6.99 - | _ => raise ERROR ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
6.100 - end
6.101 -
6.102 -(* this function cannot work as long as the datastructure does not contain thy' *)
6.103 -fun thy_containing_cal thy' sop =
6.104 - let
6.105 - val thy = ThyC.get_theory thy'
6.106 - in
6.107 - case AList.lookup op= (Know_Store.get_calcs thy) sop of
6.108 - SOME (_(*\<^const_name>\<open>plus\<close>*), _) => ("IsacKnowledge", "Base_Tools")
6.109 - | _ => raise ERROR ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
6.110 - end
6.111 -
6.112 -fun for_thy_hierarchy theID = Store.get (get_thes ()) theID theID;
6.113 -
6.114 -(* adapt_fillpat: Proof.context -> Error_Pattern.fill_in -> Error_Pattern.fill_in*)
6.115 -fun adapt_fillpat ctxt (fill_in_id, term, id) =
6.116 - (fill_in_id, Model_Pattern.adapt_term_to_type ctxt term, id)
6.117 -
6.118 -fun adapt_to_type ctxt (Thy_Write.Hthm {coursedesign, fillpats, guh, mathauthors, thm}) =
6.119 - (Thy_Write.Hthm {coursedesign = coursedesign, fillpats = (map (adapt_fillpat ctxt)) fillpats,
6.120 - guh = guh, mathauthors = mathauthors, thm = thm})
6.121 - | adapt_to_type _ the = the;
6.122 -
6.123 -fun from_store ctxt id =
6.124 - let
6.125 - val the = Store.get (get_thes ()) id id
6.126 - in adapt_to_type ctxt the end
6.127 - handle ERROR _ =>
6.128 - raise error ("*** ERROR Thy_Read.from_store ctxt " ^ strs2str id ^ " not found");
6.129 -
6.130 -(**)end(**)
7.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Jan 06 10:50:33 2023 +0100
7.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Jan 06 11:32:57 2023 +0100
7.3 @@ -42,102 +42,6 @@
7.4 between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.
7.5
7.6 \<close>
7.7 -subsubsection \<open>Get and group the theories defined in Isac\<close>
7.8 -ML \<open>
7.9 - (* we don't use "fun isacthys ()" etc HERE,
7.10 - because Thy_Info.get_theory only works with session Isac, not with Build_Isac.thy *)
7.11 - val knowledge_parent = @{theory}
7.12 - val proglang_parent = @{theory ProgLang}
7.13 -
7.14 - val allthys = Theory.ancestors_of @{theory};
7.15 - val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
7.16 - [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory MathEngine},
7.17 - @{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Isac_Knowledge"]*)
7.18 -
7.19 - val isabthys' = (*["Complex_Main", "Taylor", .., "Isac_Knowledge"]*)
7.20 - drop ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) allthys), allthys);
7.21 - val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
7.22 - take ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) allthys), allthys)
7.23 - |> remove Context.eq_thy @{theory Test_Build_Thydata};
7.24 -
7.25 - val knowthys' = (*["Isac_Knowledge", .., "Input_Descript"]*)
7.26 - take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
7.27 - val progthys' = (*["Auto_Prog", .., "Know_Store"]*)
7.28 - drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
7.29 - |> remove Context.eq_thy @{theory BaseDefinitions};
7.30 -\<close>
7.31 -declare[[ML_print_depth = 999]]
7.32 -ML \<open>
7.33 -\<close> ML \<open>
7.34 -\<close> ML \<open>
7.35 -\<close>
7.36 -
7.37 -subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
7.38 -text \<open>
7.39 - val isacrlsthms = (*length = 460*)
7.40 - Thy_Hierarchy.thms_of_rlss @ {theory} (Know_Store.get_rlss knowledge_parent) : ThmC.T list
7.41 -
7.42 - val rlsthmsNOTisac = isacrlsthms (*length = 36*)
7.43 - |> filter (fn (deriv, _) =>
7.44 - member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
7.45 - : ThmC.T list
7.46 -\<close>
7.47 -
7.48 -subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>
7.49 -text \<open>
7.50 - The sequence in the (key, data) list is arbitrary, because insertion using the key
7.51 - is random. The sequence of the root nodes "IsacKnowledge", "Isabelle"
7.52 - and "IsacScripts" is determined in Know_Store.thy.
7.53 -\<close>
7.54 -text \<open>
7.55 - ATTENTION: ===================================================================================
7.56 - the code below does NOT terminate in x86_64_32 mode of Poly/ML 5.8.
7.57 - Nevertheless, Build_Isac.thy should (and can!) be used in this mode,
7.58 - while preferences ML_system_64 = "true" never reaches Build_Isac.thy.
7.59 - ==============================================================================================
7.60 - See "etc/preferences".
7.61 -\<close>
7.62 -text \<open>
7.63 -val thydata_list = (* SEE NOTE ABOVE *)
7.64 - Thy_Hierarchy.collect_part "IsacKnowledge" knowledge_parent knowthys' @
7.65 - (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @
7.66 - Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys'
7.67 -: (Thy_Write.theID * Thy_Write.thydata) list
7.68 -\<close>
7.69 -ML \<open>
7.70 -map Context.theory_name knowthys'
7.71 -\<close> ML \<open>
7.72 -Context.theory_name knowledge_parent
7.73 -\<close> text \<open>
7.74 - collect_part "IsacKnowledge" knowledge_parent knowthys'
7.75 -\<close> ML \<open>
7.76 -"~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
7.77 -\<close> text \<open>
7.78 - val xxx = (flat (map (Thy_Hierarchy.collect_thms part) thys))
7.79 -\<close> text \<open>
7.80 -val 34 = length thys;
7.81 -val 479 = length xxx;
7.82 -\<close> text \<open>
7.83 - (collect_rlss part (Know_Store.get_rlss parent) thys)
7.84 -\<close> text \<open>
7.85 -"~~~~~ fun collect_rlss , args:"; val (part, rlss, thys) = (part, (Know_Store.get_rlss parent), thys);
7.86 -\<close> text \<open>
7.87 -(* Build_Thydata.thy in jedit leads to "Exception- Size raised" <<<===============================
7.88 - =============================== but batch process =============================================
7.89 - ~~$ ./bin/isabelle build -o browser_info -v -b Isac
7.90 - =============================== works =========================================================
7.91 -*)
7.92 -Know_Store.get_rlss parent
7.93 -
7.94 -setup \<open>Know_Store.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
7.95 -\<close>
7.96 -
7.97 -
7.98 -section \<open>interface for dialog-authoring\<close>
7.99 -text \<open>
7.100 - Dialog authoring needs re-dsign since error patterns went to theories they are defined in.
7.101 -\<close>
7.102 -
7.103
7.104 section \<open>Link Know_Store to completed IsacKnowledge\<close>
7.105 ML \<open>Know_Store.set_ref_last_thy @{theory}\<close>
8.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Jan 06 10:50:33 2023 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,133 +0,0 @@
8.4 -(* Title: "BridgeLibisabelle/thy-hierarchy.sml"
8.5 - Authors: Walther Neuper 060113
8.6 - (c) due to copyright terms
8.7 -
8.8 -theory Test_Some imports Isac.Build_Thydata begin
8.9 -ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
8.10 -ML_file "xmlsrc/thy-hierarchy.sml"
8.11 -
8.12 -CAUTION with testing *2file functions -- they are actually writing to ~/tmp
8.13 -*)
8.14 -
8.15 -val thy = @{theory "Isac_Knowledge"};
8.16 -
8.17 -"-----------------------------------------------------------------------------------------------";
8.18 -"table of contents -----------------------------------------------";
8.19 -"-----------------------------------------------------------------";
8.20 -"----------- fun thms_of_rlss ------------------------------------";
8.21 -"----------- fun get_fun_ids -------------------------------------------------------------------";
8.22 -"-----------------------------------------------------------------";
8.23 -"----------- gen.minimal Know_Store from Test_Build_Thydata.thy";
8.24 -"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
8.25 -"-----------------------------------------------------------------";
8.26 -"-----------------------------------------------------------------";
8.27 -"-----------------------------------------------------------------";
8.28 -
8.29 -"----------- fun thms_of_rlss ------------------------------------";
8.30 -"----------- fun thms_of_rlss ------------------------------------";
8.31 -"----------- fun thms_of_rlss ------------------------------------";
8.32 -
8.33 -val rlss =
8.34 - [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),
8.35 - ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))];
8.36 -
8.37 -val [_, (thmID, term)] = Thy_Hierarchy.thms_of_rlss thy rlss;
8.38 -
8.39 -if thmID = "Poly.real_mult_minus1_sym"
8.40 -then () else error "thms_of_rlss changed";
8.41 -
8.42 -"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
8.43 -val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
8.44 - |> map (Thy_Hierarchy.thms_of_rls o #2 o #2)
8.45 - (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"),
8.46 - Thm ("sym_real_mult_minus1", "- ?z1 = - 1 * ?z1")]]*)
8.47 - |> flat
8.48 - (* = [Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"),
8.49 - Thm ("sym_real_mult_minus1", "- ?z1 = - 1 * ?z1")]*)
8.50 - |> map (ThmC.revert_sym_rule thy)
8.51 - (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + - 1 * ?b"),
8.52 - Thm ("Delete.real_mult_minus1", "- 1 * ?z = - ?z")] : rule list*)
8.53 - |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
8.54 - (* = [("Poly.real_diff_minus", Const (\<^const_name>\<open>Trueprop\<close>, "bool \<Rightarrow> prop") $ ...,
8.55 - ("Delete.real_mult_minus1", Const (\<^const_name>\<open>Trueprop\<close>, ...)] : (string * term) list*)
8.56 - |> distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
8.57 -
8.58 -
8.59 -"----------- fun get_fun_ids -------------------------------------------------------------------";
8.60 -"----------- fun get_fun_ids -------------------------------------------------------------------";
8.61 -"----------- fun get_fun_ids -------------------------------------------------------------------";
8.62 -val met_fun_ids = Thy_Hierarchy.get_fun_ids @{theory Biegelinie};
8.63 -if map fst (Thy_Hierarchy.get_fun_ids @{theory Biegelinie}) =
8.64 - ["Biegelinie.function_to_equality", "Biegelinie.biegelinie", "Biegelinie.belastung_zu_biegelinie",
8.65 - "Biegelinie.setzte_randbedingungen"] then () else error "get_fun_ids changed"
8.66 -
8.67 -
8.68 -"----------- gen.minimal Know_Store from Test_Build_Thydata.thy";
8.69 -"----------- gen.minimal Know_Store from Test_Build_Thydata.thy";
8.70 -"----------- gen.minimal Know_Store from Test_Build_Thydata.thy";
8.71 - val isacrlsthms = Know_Store.get_rlss @{theory Test_Build_Thydata}
8.72 -(* CHANGE FOR CODE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> *)
8.73 - |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "prog_expr" (*unpleasant in test*)
8.74 - |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls" (*unpleasant in test*)
8.75 - |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "empty" (*unpleasant in test*)
8.76 - |> Thy_Hierarchy.thms_of_rlss @{theory} (*length = 4*)
8.77 -
8.78 - val rlsthmsNOTisac = isacrlsthms (*length = 2*)
8.79 - |> filter (fn (deriv, _) =>
8.80 - member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
8.81 -;
8.82 -val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
8.83 -;
8.84 -val thydata_list =
8.85 - Thy_Hierarchy.collect_part "IsacKnowledge" knowledge_parent knowthys' @
8.86 - (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @
8.87 - Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
8.88 -;
8.89 -case thydata_list of (*length = 8*)
8.90 - [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
8.91 - Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
8.92 - mathauthors = ["isac-team"], thm = _}),
8.93 - (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
8.94 - Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
8.95 - mathauthors = ["isac-team"], thm = _}),
8.96 - (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
8.97 - Thy_Write.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
8.98 - mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
8.99 - (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
8.100 - Thy_Write.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
8.101 - mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
8.102 - (["Isabelle", "HOL", "Theorems", "refl"],
8.103 - Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
8.104 - mathauthors = ["Isabelle team, TU Munich"], thm = _}),
8.105 - (["Isabelle", "Fun", "Theorems", "o_def"], Thy_Write.Hthm {coursedesign = [], fillpats = [],
8.106 - guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
8.107 - (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
8.108 - Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
8.109 - mathauthors = ["isac-team"], thm = _}),
8.110 - (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
8.111 - Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
8.112 - mathauthors = ["isac-team"], thm = _})] => ()
8.113 -| _ => error "collect thydata from Test_Build_Thydata changed";
8.114 -;
8.115 -(* we store locally on MINIthehier instead on Know_Store, see Know_Store: *)
8.116 - fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata;
8.117 -val thes = map (fn (a, b) => (b, a)) thydata_list
8.118 -val MINIthehier = (fold add_the thes) (Know_Store.get_thes @{theory Test_Build_Thydata});
8.119 -
8.120 -"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
8.121 -"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
8.122 -"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
8.123 -fun MINIget_the (theID : Thy_Write.theID) = Store.get MINIthehier theID theID (*see ptyps.sml*)
8.124 -fun MINIthy_hierarchy2file (path:Pbl_Met_Hierarchy.filepath) =
8.125 - (*Pbl_Met_Hierarchy.str2file*) (path ^ "thy_hierarchy.xml",
8.126 - "<NODE>\n" ^
8.127 - " <ID> theory hierarchy </ID>\n" ^
8.128 - " <NO> 1 </NO>\n" ^
8.129 - " <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
8.130 - (Thy_Hierarchy.hierarchy_guh MINIthehier) ^
8.131 - "</NODE>");
8.132 -if MINIthy_hierarchy2file "xxx/" =
8.133 - ("xxx/thy_hierarchy.xml",
8.134 - "<NODE>\n <ID> theory hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_ROOT </CONTENTREF>\n <NODE>\n <ID> IsacKnowledge </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isac_IsacKnowledge-part </CONTENTREF>\n <NODE>\n <ID> Test_Build_Thydata </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata </CONTENTREF>\n <NODE>\n <ID> Theorems </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata-Theorems </CONTENTREF>\n <NODE>\n <ID> thm111 </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata-thm-thm111 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> thm222 </ID>\n <NO> 2 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata-thm-thm222 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Rulesets </ID>\n <NO> 2 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata-Rulesets </CONTENTREF>\n <NODE>\n <ID> rls111 </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata-rls-rls111 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> rls222 </ID>\n <NO> 2 </NO>\n <CONTENTREF> thy_isac_Test_Build_Thydata-rls-rls222 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Isabelle </ID>\n <NO> 2 </NO>\n <CONTENTREF> thy_isab_Isabelle-part </CONTENTREF>\n <NODE>\n <ID> HOL </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isab_HOL </CONTENTREF>\n <NODE>\n <ID> Theorems </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isab_HOL-Theorems </CONTENTREF>\n <NODE>\n <ID> refl </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isab_HOL-thm-refl </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Fun </ID>\n <NO> 2 </NO>\n <CONTENTREF> thy_isab_Fun </CONTENTREF>\n <NODE>\n <ID> Theorems </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isab_Fun-Theorems </CONTENTREF>\n <NODE>\n <ID> o_def </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_isab_Fun-thm-o_def </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> IsacScripts </ID>\n <NO> 3 </NO>\n <CONTENTREF> thy_scri_IsacScripts-part </CONTENTREF>\n <NODE>\n <ID> Test_Build_Thydata </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_scri_Test_Build_Thydata </CONTENTREF>\n <NODE>\n <ID> Theorems </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_scri_Test_Build_Thydata-Theorems </CONTENTREF>\n <NODE>\n <ID> thm111 </ID>\n <NO> 1 </NO>\n <CONTENTREF> thy_scri_Test_Build_Thydata-thm-thm111 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> thm222 </ID>\n <NO> 2 </NO>\n <CONTENTREF> thy_scri_Test_Build_Thydata-thm-thm222 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
8.135 -then () else error "MINIthy_hierarchy2file CHANGED";
8.136 -
9.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Fri Jan 06 10:50:33 2023 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,139 +0,0 @@
9.4 -(* Title: BridgeLibisabelle/thy-present.sml
9.5 - Author: Walther Neuper
9.6 - (c) due to copyright terms
9.7 -*)
9.8 -
9.9 -"--------------------------------------------------------";
9.10 -"--------------------------------------------------------";
9.11 -"table of contents --------------------------------------";
9.12 -"--------------------------------------------------------";
9.13 -"----------- fun thy_containing_rls ---------------------";
9.14 -"----------- apply thy_containing_rls -------------------";
9.15 -"----------- fun thy_containing_cal ---------------------";
9.16 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
9.17 -"--------------------------------------------------------";
9.18 -(*============ inhibit exn WN120321 ==============================================
9.19 -"--------------------------------------------------------";
9.20 -"----------- fun filter_appl_rews -----------------------";
9.21 -============ inhibit exn WN120321 ==============================================*)
9.22 -"----------- fun is_contained_in ------------------------";
9.23 -"--------------------------------------------------------";
9.24 -"--------------------------------------------------------";
9.25 -
9.26 -"----------- fun thy_containing_rls ---------------------";
9.27 -"----------- fun thy_containing_rls ---------------------";
9.28 -"----------- fun thy_containing_rls ---------------------";
9.29 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
9.30 -if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
9.31 -else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
9.32 -;
9.33 -"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
9.34 - val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
9.35 -val xxx = AList.lookup op= (Know_Store.get_rlss thy) rls';
9.36 -val SOME (thy'', _) = xxx;
9.37 -val SOME ("Poly", _) = xxx;
9.38 -if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
9.39 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
9.40 -if Thy_Read.partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
9.41 -;
9.42 -"~~~~~ fun partID', args:"; val (thy') = (thy');
9.43 -ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
9.44 -;
9.45 -"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
9.46 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
9.47 -Thy_Read.knowthys ()
9.48 -;
9.49 -"~~~~~ fun knowthys , args:"; val () = ();
9.50 - val allthys = filter_out (member Context.eq_thy
9.51 - [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
9.52 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
9.53 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
9.54 -length allthys = 152; (*in Isabelle2015/Isac*)
9.55 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
9.56 -ThyC.get_theory "Complex_Main";*)
9.57 -Thy_Info.get_theory "Complex_Main";;
9.58 -
9.59 -"----------- apply thy_containing_rls -------------------";
9.60 -"----------- apply thy_containing_rls -------------------";
9.61 -"----------- apply thy_containing_rls -------------------";
9.62 -if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
9.63 -else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
9.64 -;
9.65 -if Thy_Read.thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()
9.66 -else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'")
9.67 -;
9.68 -if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
9.69 -(**)("IsacKnowledge", "Base_Tools")(**)
9.70 -(** )("IsacScripts", "Prog_Expr")( **)
9.71 -then () else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
9.72 -
9.73 -"----------- fun thy_containing_cal ---------------------";
9.74 -"----------- fun thy_containing_cal ---------------------";
9.75 -"----------- fun thy_containing_cal ---------------------";
9.76 -(* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)
9.77 -if Thy_Read.thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")
9.78 -then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
9.79 -
9.80 -
9.81 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
9.82 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
9.83 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
9.84 -"----- initContext -----";
9.85 -States.reset ();
9.86 -CalcTree @{context}
9.87 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
9.88 - ("Test",
9.89 - ["LINEAR", "univariate", "equation", "test"],
9.90 - ["Test", "solve_linear"]))];
9.91 -Iterator 1; moveActiveRoot 1;
9.92 -autoCalculate 1 CompleteCalcHead;
9.93 -
9.94 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
9.95 -if is_curr_endof_calc pt ([1],Frm) then ()
9.96 -else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
9.97 -
9.98 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
9.99 -
9.100 -if not (is_curr_endof_calc pt ([1],Frm)) then ()
9.101 -else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
9.102 -if is_curr_endof_calc pt ([1],Res) then ()
9.103 -else error "rewtools.sml is_curr_endof_calc ([1],Res)";
9.104 -
9.105 -(*//----------------- dropped with "purge code for theory-hierarchy" * )
9.106 -initContext 1 Ptool.Thy_ ([1],Res);
9.107 -
9.108 -"----- checkContext -----";
9.109 -States.reset ();
9.110 -CalcTree @{context}
9.111 - [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
9.112 - ("Test",
9.113 - ["LINEAR", "univariate", "equation", "test"],
9.114 - ["Test", "solve_linear"]))];
9.115 -Iterator 1; moveActiveRoot 1;
9.116 -autoCalculate 1 CompleteCalc;
9.117 -interSteps 1 ([1],Res);
9.118 -
9.119 -val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
9.120 -checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
9.121 -
9.122 -interSteps 1 ([2],Res);
9.123 -val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
9.124 -
9.125 -checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
9.126 -checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
9.127 -( *//----------------- dropped with "purge code for theory-hierarchy" *)
9.128 -
9.129 -"----------- fun is_contained_in ------------------------";
9.130 -"----------- fun is_contained_in ------------------------";
9.131 -"----------- fun is_contained_in ------------------------";
9.132 -val r1 = Thm ("real_diff_minus", @{thm real_diff_minus});
9.133 -if Rule_Set.contains r1 Test_simplify then ()
9.134 -else error "rewtools.sml Rule_Set.contains Thm";
9.135 -
9.136 -val r1 = Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_");
9.137 -if Rule_Set.contains r1 Test_simplify then ()
9.138 -else error "rewtools.sml Rule_Set.contains Eval";
9.139 -
9.140 -val r1 = Eval (\<^const_name>\<open>minus\<close>, Calc_Binop.numeric "#add_");
9.141 -if not (Rule_Set.contains r1 Test_simplify) then ()
9.142 -else error "rewtools.sml Rule_Set.contains Eval";
10.1 --- a/test/Tools/isac/Test_Isac.thy Fri Jan 06 10:50:33 2023 +0100
10.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Jan 06 11:32:57 2023 +0100
10.3 @@ -297,10 +297,8 @@
10.4 ML_file "MathEngine/messages.sml"
10.5 ML_file "MathEngine/states.sml"
10.6
10.7 - ML_file "BridgeLibisabelle/thy-present.sml"
10.8 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
10.9 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
10.10 - ML_file "BridgeLibisabelle/thy-hierarchy.sml"
10.11 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
10.12 ML_file "BridgeLibisabelle/interface.sml"
10.13
10.14 @@ -348,7 +346,6 @@
10.15 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
10.16 ML_file "Knowledge/inssort.sml"
10.17 ML_file "Knowledge/isac.sml"
10.18 - ML_file "Knowledge/build_thydata.sml"
10.19
10.20 ML_file "Test_Code/test-code.sml"
10.21
11.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Jan 06 10:50:33 2023 +0100
11.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Jan 06 11:32:57 2023 +0100
11.3 @@ -297,10 +297,8 @@
11.4 ML_file "MathEngine/messages.sml"
11.5 ML_file "MathEngine/states.sml"
11.6
11.7 - ML_file "BridgeLibisabelle/thy-present.sml"
11.8 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
11.9 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
11.10 - ML_file "BridgeLibisabelle/thy-hierarchy.sml"
11.11 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
11.12 ML_file "BridgeLibisabelle/interface.sml"
11.13
11.14 @@ -348,7 +346,6 @@
11.15 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
11.16 ML_file "Knowledge/inssort.sml"
11.17 ML_file "Knowledge/isac.sml"
11.18 - ML_file "Knowledge/build_thydata.sml"
11.19
11.20 ML_file "Test_Code/test-code.sml"
11.21