1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 28 16:51:36 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 28 17:50:18 2020 +0200
1.3 @@ -4,7 +4,7 @@
1.4 Calc work on Problem employing Method; both are collected in a respective Store;
1.5 The collections' structure is independent from the dependency graph of Isabelle's theories
1.6 in Knowledge.
1.7 -Store is also used by Thy_Html, required for Isac's Java front end, irrelevant for PIDE.
1.8 +Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
1.9
1.10 The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
1.11 they also include minimal code required for other "xxxxx-def.sml" files.
1.12 @@ -36,7 +36,7 @@
1.13 ML_file "problem-def.sml"
1.14 ML_file "method-def.sml"
1.15 ML_file "cas-def.sml"
1.16 -ML_file "thy-html.sml"
1.17 +ML_file "thy-write.sml"
1.18
1.19 ML \<open>
1.20 \<close> ML \<open>
1.21 @@ -69,9 +69,9 @@
1.22 val add_pbts: (Probl_Def.T * Spec.id) list -> theory -> theory
1.23 val get_mets: theory -> Meth_Def.store
1.24 val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
1.25 - val get_thes: theory -> (Thy_Html.thydata Store.node) list
1.26 - val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.27 - val insert_fillpats: (Thy_Html.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.28 + val get_thes: theory -> (Thy_Write.thydata Store.node) list
1.29 + val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.30 + val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.31 val get_ref_thy: unit -> theory
1.32 val set_ref_thy: theory -> unit
1.33 end;
1.34 @@ -135,21 +135,21 @@
1.35 in Data.map (fold add_met mets) thy end;
1.36
1.37 structure Data = Theory_Data (
1.38 - type T = (Thy_Html.thydata Store.node) list;
1.39 + type T = (Thy_Write.thydata Store.node) list;
1.40 val empty = [];
1.41 val extend = I;
1.42 val merge = Store.merge; (* relevant for store_thm, store_rls *)
1.43 );
1.44 fun get_thes thy = Data.get thy
1.45 fun add_thes thes thy = let
1.46 - fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata
1.47 + fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
1.48 in Data.map (fold add_the thes) thy end;
1.49 fun insert_fillpats fis thy =
1.50 let
1.51 fun update_elem (theID, fillpats) =
1.52 let
1.53 val hthm = Store.get (Data.get thy) theID theID
1.54 - val hthm' = Thy_Html.update_hthm hthm fillpats
1.55 + val hthm' = Thy_Write.update_hthm hthm fillpats
1.56 handle ERROR _ =>
1.57 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.58 in Store.update theID theID hthm' end
1.59 @@ -208,11 +208,11 @@
1.60 section \<open>determine sequence of main parts in thehier\<close>
1.61 setup \<open>
1.62 KEStore_Elems.add_thes
1.63 - [(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacKnowledge"], html = "",
1.64 + [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
1.65 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
1.66 - (Thy_Html.Html {guh = Thy_Html.part2guh ["Isabelle"], html = "",
1.67 + (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
1.68 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
1.69 - (Thy_Html.Html {guh = Thy_Html.part2guh ["IsacScripts"], html = "",
1.70 + (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
1.71 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
1.72 \<close>
1.73
1.74 @@ -256,10 +256,10 @@
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
1.78 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
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_Html.theID2str id, Thy_Html.the2str the))
1.83 + |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
1.84 |> map pair2str
1.85 |> map writeln
1.86 \<close>
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 28 16:51:36 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 28 17:50:18 2020 +0200
2.3 @@ -17,7 +17,7 @@
2.4 val maxthy: theory -> theory -> theory
2.5
2.6 type pbt_ = string * (term * term)
2.7 - val update_hrls: Thy_Html.thydata -> Error_Pattern_Def.id list -> Thy_Html.thydata
2.8 + val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
2.9
2.10 end
2.11
2.12 @@ -39,7 +39,7 @@
2.13 term)); (* id | struct-var *)
2.14
2.15 (* for dialog-authoring *)
2.16 -fun update_hrls (Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
2.17 +fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
2.18 let
2.19 val rls' =
2.20 case rls of
2.21 @@ -54,7 +54,7 @@
2.22 scr = scr, errpatts = errpatIDs}
2.23 | Erls => Erls
2.24 in
2.25 - Thy_Html.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
2.26 + Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
2.27 thy_rls = (thyID, rls')}
2.28 end
2.29 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
3.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Tue Apr 28 16:51:36 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Tue Apr 28 17:50:18 2020 +0200
3.3 @@ -2,7 +2,7 @@
3.4 Author: Walther Neuper
3.5 (c) due to copyright terms
3.6
3.7 -A tree for storing collections of Problem, Method and Thy_Html.
3.8 +A tree for storing collections of Problem, Method and Thy_Write.
3.9 *)
3.10 signature STORE_TREE =
3.11 sig
4.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Tue Apr 28 16:51:36 2020 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,205 +0,0 @@
4.4 -(* Title: BaseDefinitions/celem-8.sml
4.5 - Author: Walther Neuper
4.6 - (c) due to copyright terms
4.7 -
4.8 -Legacy for HTML representation of theory data in Isac's Java front end.
4.9 -*)
4.10 -signature HTML_FOR_THEORY_DATA =
4.11 -sig
4.12 - type authors
4.13 - datatype thydata
4.14 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
4.15 - | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
4.16 - | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
4.17 - | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
4.18 - | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
4.19 - type theID
4.20 - val theID2str: string list -> string
4.21 - val the2str: thydata -> string
4.22 - val thes2str: thydata list -> string
4.23 - val theID2thyID: theID -> ThyC.id
4.24 -
4.25 - val part2guh: theID -> Check_Unique.id
4.26 - val thy2guh: theID -> Check_Unique.id
4.27 - val thypart2guh: theID -> Check_Unique.id
4.28 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.id
4.29 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.id
4.30 - val cal2guh: string * ThyC.id -> string -> Check_Unique.id
4.31 - val ord2guh: string * ThyC.id -> string -> Check_Unique.id
4.32 - val theID2guh: theID -> Check_Unique.id
4.33 -
4.34 - val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
4.35 - val update_hthm: thydata -> Error_Pattern_Def.fill_in list -> thydata
4.36 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.37 - (*NONE*)
4.38 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.39 - (*NONE*)
4.40 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.41 -end
4.42 -
4.43 -(**)
4.44 -structure Thy_Html(**): HTML_FOR_THEORY_DATA(**) =
4.45 -struct
4.46 -(**)
4.47 -
4.48 -(*the key into the hierarchy ob theory elements*)
4.49 -type theID = string list;
4.50 -val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
4.51 -fun theID2thyID theID =
4.52 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
4.53 - else error ("theID2thyID called with " ^ theID2str theID);
4.54 -type authors = string list;
4.55 -(* datatype for collecting thydata for hierarchy *)
4.56 -(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
4.57 -datatype thydata =
4.58 - Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}
4.59 -| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
4.60 - thm: thm} (* here no sym_thm, thus no thmID required *)
4.61 -| Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
4.62 -| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
4.63 -| Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
4.64 - ord: (subst -> (term * term) -> bool)};
4.65 -fun the2str (Html {guh, ...}) = guh
4.66 - | the2str (Hthm {guh, ...}) = guh
4.67 - | the2str (Hrls {guh, ...}) = guh
4.68 - | the2str (Hcal {guh, ...}) = guh
4.69 - | the2str (Hord {guh, ...}) = guh
4.70 -fun thes2str thes = map the2str thes |> list2str;
4.71 -
4.72 -(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
4.73 - (a): thehier does not contain sym_thmID theorems
4.74 - (b): lookup for sym_thmID directly from Isabelle using sym_thm
4.75 - (within math-engine NO lookup in thehier -- within java in *.xml only!)
4.76 -TODO (c): export from thehier to xml
4.77 -TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
4.78 -TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
4.79 -TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
4.80 - stands for both, "thmID" and "sym_thmID"
4.81 -TODO (d1) lookup from calctxt
4.82 -TODO (d1) lookup from from rule set in MiniBrowser *)
4.83 -type thehier = (thydata Store.node) list;
4.84 -(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
4.85 -fun part2guh [str] = (case str of
4.86 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.id
4.87 - | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
4.88 - | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
4.89 - | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
4.90 - | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
4.91 -
4.92 -fun thy2guh [part, thyID] = (case part of
4.93 - "Isabelle" => "thy_isab_" ^ thyID
4.94 - | "IsacScripts" => "thy_scri_" ^ thyID
4.95 - | "IsacKnowledge" => "thy_isac_" ^ thyID
4.96 - | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
4.97 - | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
4.98 -
4.99 -fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
4.100 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.id
4.101 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
4.102 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
4.103 - | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
4.104 - | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
4.105 -
4.106 -
4.107 -(* convert the data got via contextToThy to a globally unique handle.
4.108 - there is another way to get the guh: get out of the 'theID' in the hierarchy *)
4.109 -fun thm2guh (isa, thyID) thmID = case isa of
4.110 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.id
4.111 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
4.112 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
4.113 - | _ => raise ERROR
4.114 - ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
4.115 -
4.116 -fun rls2guh (isa, thyID) rls' = case isa of
4.117 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.id
4.118 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
4.119 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
4.120 - | _ => raise ERROR
4.121 - ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
4.122 -
4.123 -fun cal2guh (isa, thyID) calID = case isa of
4.124 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.id
4.125 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
4.126 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
4.127 - | _ => raise ERROR
4.128 - ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
4.129 -
4.130 -fun ord2guh (isa, thyID) rew_ord' = case isa of
4.131 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.id
4.132 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
4.133 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
4.134 - | _ => raise ERROR
4.135 - ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
4.136 -
4.137 -(* TODO
4.138 -fun theID2guh theID = case length theID of
4.139 - 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
4.140 - | 1 => part2guh theID
4.141 - | 2 => thy2guh theID
4.142 - | 3 => thypart2guh theID
4.143 - | 4 =>
4.144 - let val [isa, thyID, typ, elemID] = theID
4.145 - in case typ of
4.146 - "Theorems" => thm2guh (isa, thyID) elemID
4.147 - | "Rulesets" => rls2guh (isa, thyID) elemID
4.148 - | "Calculations" => cal2guh (isa, thyID) elemID
4.149 - | "Orders" => ord2guh (isa, thyID) elemID
4.150 - | "Theorems" => thy2guh [isa, thyID]
4.151 - | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
4.152 - end
4.153 - | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
4.154 -*)
4.155 -(* not only for thydata, but also for thy's etc *)
4.156 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
4.157 - | theID2guh [str] = part2guh [str]
4.158 - | theID2guh [s1, s2] = thy2guh [s1, s2]
4.159 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
4.160 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
4.161 - "Theorems" => thm2guh (isa, thyID) elemID
4.162 - | "Rulesets" => rls2guh (isa, thyID) elemID
4.163 - | "Calculations" => cal2guh (isa, thyID) elemID
4.164 - | "Orders" => ord2guh (isa, thyID) elemID
4.165 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
4.166 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
4.167 -
4.168 -(* not only for thydata, but also for thy's etc *)
4.169 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
4.170 - | theID2guh [str] = part2guh [str]
4.171 - | theID2guh [s1, s2] = thy2guh [s1, s2]
4.172 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
4.173 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
4.174 - "Theorems" => thm2guh (isa, thyID) elemID
4.175 - | "Rulesets" => rls2guh (isa, thyID) elemID
4.176 - | "Calculations" => cal2guh (isa, thyID) elemID
4.177 - | "Orders" => ord2guh (isa, thyID) elemID
4.178 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
4.179 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
4.180 -
4.181 -fun Html_default exist = (Html {guh = theID2guh exist,
4.182 - coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
4.183 -
4.184 -fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
4.185 - | fill_parents (exist, i :: is) thydata =
4.186 - Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
4.187 - | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
4.188 -
4.189 -fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
4.190 - | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) =
4.191 - if i = key
4.192 - then pys (* preserve existing thydata *)
4.193 - else py :: add_thydata (exist, [i]) data pyss
4.194 - | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
4.195 - if i = key
4.196 - then
4.197 - if length pys = 0
4.198 - then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
4.199 - else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
4.200 - else py :: add_thydata (exist, iss) data pyss
4.201 - | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
4.202 -
4.203 -fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
4.204 - Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
4.205 - fillpats = fillpats', thm = thm}
4.206 - | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
4.207 -
4.208 -(**)end(**)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml Tue Apr 28 17:50:18 2020 +0200
5.3 @@ -0,0 +1,205 @@
5.4 +(* Title: BaseDefinitions/celem-8.sml
5.5 + Author: Walther Neuper
5.6 + (c) due to copyright terms
5.7 +
5.8 +Legacy for HTML representation of theory data in Isac's Java front end.
5.9 +*)
5.10 +signature THEORY_DATA_STORE_WRITE =
5.11 +sig
5.12 + type authors
5.13 + datatype thydata
5.14 + = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
5.15 + | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
5.16 + | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
5.17 + | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
5.18 + | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
5.19 + type theID
5.20 + val theID2str: string list -> string
5.21 + val the2str: thydata -> string
5.22 + val thes2str: thydata list -> string
5.23 + val theID2thyID: theID -> ThyC.id
5.24 +
5.25 + val part2guh: theID -> Check_Unique.id
5.26 + val thy2guh: theID -> Check_Unique.id
5.27 + val thypart2guh: theID -> Check_Unique.id
5.28 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.id
5.29 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.id
5.30 + val cal2guh: string * ThyC.id -> string -> Check_Unique.id
5.31 + val ord2guh: string * ThyC.id -> string -> Check_Unique.id
5.32 + val theID2guh: theID -> Check_Unique.id
5.33 +
5.34 + val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
5.35 + val update_hthm: thydata -> Error_Pattern_Def.fill_in list -> thydata
5.36 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.37 + (*NONE*)
5.38 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.39 + (*NONE*)
5.40 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.41 +end
5.42 +
5.43 +(**)
5.44 +structure Thy_Write(**): THEORY_DATA_STORE_WRITE(**) =
5.45 +struct
5.46 +(**)
5.47 +
5.48 +(*the key into the hierarchy ob theory elements*)
5.49 +type theID = string list;
5.50 +val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
5.51 +fun theID2thyID theID =
5.52 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
5.53 + else error ("theID2thyID called with " ^ theID2str theID);
5.54 +type authors = string list;
5.55 +(* datatype for collecting thydata for hierarchy *)
5.56 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
5.57 +datatype thydata =
5.58 + Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}
5.59 +| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
5.60 + thm: thm} (* here no sym_thm, thus no thmID required *)
5.61 +| Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
5.62 +| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
5.63 +| Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
5.64 + ord: (subst -> (term * term) -> bool)};
5.65 +fun the2str (Html {guh, ...}) = guh
5.66 + | the2str (Hthm {guh, ...}) = guh
5.67 + | the2str (Hrls {guh, ...}) = guh
5.68 + | the2str (Hcal {guh, ...}) = guh
5.69 + | the2str (Hord {guh, ...}) = guh
5.70 +fun thes2str thes = map the2str thes |> list2str;
5.71 +
5.72 +(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
5.73 + (a): thehier does not contain sym_thmID theorems
5.74 + (b): lookup for sym_thmID directly from Isabelle using sym_thm
5.75 + (within math-engine NO lookup in thehier -- within java in *.xml only!)
5.76 +TODO (c): export from thehier to xml
5.77 +TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
5.78 +TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
5.79 +TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
5.80 + stands for both, "thmID" and "sym_thmID"
5.81 +TODO (d1) lookup from calctxt
5.82 +TODO (d1) lookup from from rule set in MiniBrowser *)
5.83 +type thehier = (thydata Store.node) list;
5.84 +(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
5.85 +fun part2guh [str] = (case str of
5.86 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.id
5.87 + | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
5.88 + | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
5.89 + | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
5.90 + | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
5.91 +
5.92 +fun thy2guh [part, thyID] = (case part of
5.93 + "Isabelle" => "thy_isab_" ^ thyID
5.94 + | "IsacScripts" => "thy_scri_" ^ thyID
5.95 + | "IsacKnowledge" => "thy_isac_" ^ thyID
5.96 + | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
5.97 + | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
5.98 +
5.99 +fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
5.100 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.id
5.101 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
5.102 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
5.103 + | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
5.104 + | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
5.105 +
5.106 +
5.107 +(* convert the data got via contextToThy to a globally unique handle.
5.108 + there is another way to get the guh: get out of the 'theID' in the hierarchy *)
5.109 +fun thm2guh (isa, thyID) thmID = case isa of
5.110 + "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.id
5.111 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
5.112 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
5.113 + | _ => raise ERROR
5.114 + ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
5.115 +
5.116 +fun rls2guh (isa, thyID) rls' = case isa of
5.117 + "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.id
5.118 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
5.119 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
5.120 + | _ => raise ERROR
5.121 + ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
5.122 +
5.123 +fun cal2guh (isa, thyID) calID = case isa of
5.124 + "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.id
5.125 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
5.126 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
5.127 + | _ => raise ERROR
5.128 + ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
5.129 +
5.130 +fun ord2guh (isa, thyID) rew_ord' = case isa of
5.131 + "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.id
5.132 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
5.133 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
5.134 + | _ => raise ERROR
5.135 + ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
5.136 +
5.137 +(* TODO
5.138 +fun theID2guh theID = case length theID of
5.139 + 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
5.140 + | 1 => part2guh theID
5.141 + | 2 => thy2guh theID
5.142 + | 3 => thypart2guh theID
5.143 + | 4 =>
5.144 + let val [isa, thyID, typ, elemID] = theID
5.145 + in case typ of
5.146 + "Theorems" => thm2guh (isa, thyID) elemID
5.147 + | "Rulesets" => rls2guh (isa, thyID) elemID
5.148 + | "Calculations" => cal2guh (isa, thyID) elemID
5.149 + | "Orders" => ord2guh (isa, thyID) elemID
5.150 + | "Theorems" => thy2guh [isa, thyID]
5.151 + | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
5.152 + end
5.153 + | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
5.154 +*)
5.155 +(* not only for thydata, but also for thy's etc *)
5.156 +fun theID2guh [] = raise ERROR ("theID2guh: called with []")
5.157 + | theID2guh [str] = part2guh [str]
5.158 + | theID2guh [s1, s2] = thy2guh [s1, s2]
5.159 + | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
5.160 + | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
5.161 + "Theorems" => thm2guh (isa, thyID) elemID
5.162 + | "Rulesets" => rls2guh (isa, thyID) elemID
5.163 + | "Calculations" => cal2guh (isa, thyID) elemID
5.164 + | "Orders" => ord2guh (isa, thyID) elemID
5.165 + | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
5.166 + | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
5.167 +
5.168 +(* not only for thydata, but also for thy's etc *)
5.169 +fun theID2guh [] = raise ERROR ("theID2guh: called with []")
5.170 + | theID2guh [str] = part2guh [str]
5.171 + | theID2guh [s1, s2] = thy2guh [s1, s2]
5.172 + | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
5.173 + | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
5.174 + "Theorems" => thm2guh (isa, thyID) elemID
5.175 + | "Rulesets" => rls2guh (isa, thyID) elemID
5.176 + | "Calculations" => cal2guh (isa, thyID) elemID
5.177 + | "Orders" => ord2guh (isa, thyID) elemID
5.178 + | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
5.179 + | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
5.180 +
5.181 +fun Html_default exist = (Html {guh = theID2guh exist,
5.182 + coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
5.183 +
5.184 +fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
5.185 + | fill_parents (exist, i :: is) thydata =
5.186 + Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
5.187 + | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
5.188 +
5.189 +fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
5.190 + | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) =
5.191 + if i = key
5.192 + then pys (* preserve existing thydata *)
5.193 + else py :: add_thydata (exist, [i]) data pyss
5.194 + | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
5.195 + if i = key
5.196 + then
5.197 + if length pys = 0
5.198 + then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
5.199 + else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
5.200 + else py :: add_thydata (exist, iss) data pyss
5.201 + | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
5.202 +
5.203 +fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
5.204 + Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
5.205 + fillpats = fillpats', thm = thm}
5.206 + | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
5.207 +
5.208 +(**)end(**)
6.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Tue Apr 28 16:51:36 2020 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Tue Apr 28 17:50:18 2020 +0200
6.3 @@ -6,6 +6,7 @@
6.4 theory BridgeLibisabelle
6.5 imports "~~/src/Tools/isac/MathEngine/MathEngine"
6.6 begin
6.7 + ML_file "thy-present.sml"
6.8 ML_file mathml.sml
6.9 ML_file datatypes.sml
6.10 ML_file "pbl-met-hierarchy.sml"
7.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 28 16:51:36 2020 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 28 17:50:18 2020 +0200
7.3 @@ -8,7 +8,7 @@
7.4 val authors2xml : int -> string -> string list -> xml
7.5 val calc2xml : int -> ThyC.id * Rule_Def.calc -> xml
7.6 val calcrefs2xml : int -> ThyC.id * Rule_Def.calc list -> xml
7.7 - val contthy2xml : int -> Rtools.contthy -> xml
7.8 + val contthy2xml : int -> Thy_Present.contthy -> xml
7.9 val extref2xml : int -> string -> string -> xml
7.10 val filterpbl :
7.11 ''a -> (''a * (Term.term * Term.term)) list -> Term.term list
7.12 @@ -79,7 +79,7 @@
7.13 fun calc2xml j (thyID, (scrop, (rewop, _))) =
7.14 indt j ^ "<CALC>\n" ^
7.15 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
7.16 - indt (j+i) ^ "<GUH>\n" ^ Thy_Html.cal2guh ("IsacKnowledge",
7.17 + indt (j+i) ^ "<GUH>\n" ^ Thy_Write.cal2guh ("IsacKnowledge",
7.18 thyID) scrop ^ "</GUH>\n" ^
7.19 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
7.20 indt j ^ "</CALC>\n";
7.21 @@ -98,7 +98,7 @@
7.22 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
7.23 indt (j+i) ^ "<STRING> " ^ ThmC.cut_id thmDeriv ^ " </STRING>\n" ^
7.24 indt (j+i) ^ "<GUH> " ^
7.25 - Thy_Html.thm2guh (Thy_Read.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
7.26 + Thy_Write.thm2guh (Thy_Read.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
7.27 indt j ^ "</RULE>\n"
7.28 | rule2xml _ _ (Rule.Eval (_(*termop*), _)) = ""
7.29 (*FIXXXXXXXME.WN060714 in rls make Eval : calc -> rule [add scriptop!]
7.30 @@ -116,7 +116,7 @@
7.31 indt j ^ "<RULE>\n" ^
7.32 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
7.33 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
7.34 - indt (j+i) ^ "<GUH> " ^ Thy_Html.rls2guh (Thy_Read.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
7.35 + indt (j+i) ^ "<GUH> " ^ Thy_Write.rls2guh (Thy_Read.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
7.36 indt j ^ "</RULE>\n"
7.37 end;
7.38 fun rules2xml _ _ [] = ""
7.39 @@ -161,7 +161,7 @@
7.40 indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
7.41 indt j ^ "</EXTREF>\n";
7.42 fun theref2xml j thyID typ xstring =
7.43 - let val guh = Thy_Html.theID2guh ["IsacKnowledge", thyID, typ, xstring]
7.44 + let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
7.45 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
7.46 in indt j ^ "<KESTOREREF>\n" ^
7.47 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
7.48 @@ -204,7 +204,7 @@
7.49 fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
7.50 indt j ^ "<CALCREF>\n" ^
7.51 indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
7.52 - indt (j+i) ^ "<GUH> " ^ Thy_Html.cal2guh ("IsacKnowledge",
7.53 + indt (j+i) ^ "<GUH> " ^ Thy_Write.cal2guh ("IsacKnowledge",
7.54 thyID) scrop ^ " </GUH>\n" ^
7.55 indt j ^ "</CALCREF>\n";
7.56 fun calcrefs2xml _ (_,[]) = ""
7.57 @@ -244,13 +244,13 @@
7.58 indt (j+i) ^"<ERLS>\n" ^
7.59 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
7.60 indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
7.61 - indt (j+2*i) ^ "<GUH> " ^ Thy_Html.rls2guh ("IsacKnowledge", thyID)
7.62 + indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID)
7.63 (Rule_Set.id erls) ^ " </GUH>\n" ^
7.64 indt (j+i) ^"</ERLS>\n" ^
7.65 indt (j+i) ^"<SRLS>\n" ^
7.66 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
7.67 indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
7.68 - indt (j+2*i) ^ "<GUH> " ^ Thy_Html.rls2guh ("IsacKnowledge", thyID)
7.69 + indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID)
7.70 (Rule_Set.id srls) ^ " </GUH>\n" ^
7.71 indt (j+i) ^"</SRLS>\n" ^
7.72 calcrefs2xml (j+i) (thyID, calc) ^
7.73 @@ -275,7 +275,7 @@
7.74 indt (j+i) ^"<ERLS> " ^
7.75 indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
7.76 indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
7.77 - indt (j+2*i) ^ "<GUH> " ^ Thy_Html.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id erls) ^ " </GUH>\n" ^
7.78 + indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id erls) ^ " </GUH>\n" ^
7.79 indt (j+i) ^"</ERLS>\n" ^
7.80 calcrefs2xml (j+i) (thyID, calc) ^
7.81 indt (j+i) ^"<SCRIPT>\n"^
7.82 @@ -665,7 +665,7 @@
7.83 (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
7.84 *)
7.85 fun theref2xml j thyID typ xstring =
7.86 - let val guh = Thy_Html.theID2guh ["IsacKnowledge", thyID, typ, xstring]
7.87 + let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
7.88 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
7.89 in indt j ^ "<KESTOREREF>\n" ^
7.90 indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
7.91 @@ -675,7 +675,7 @@
7.92 end;
7.93 fun xml_of_theref thyid typ xstring =
7.94 let
7.95 - val guh = Thy_Html.theID2guh ["IsacKnowledge", thyid, typ, xstring]
7.96 + val guh = Thy_Write.theID2guh ["IsacKnowledge", thyid, typ, xstring]
7.97 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
7.98 in
7.99 XML.Elem (("KESTOREREF", []),[
7.100 @@ -684,10 +684,10 @@
7.101 XML.Elem (("GUH", []), [XML.Text guh])])
7.102 end
7.103
7.104 -fun xml_of_contthy Rtools.EContThy =
7.105 +fun xml_of_contthy Thy_Present.EContThy =
7.106 error "contthy2xml called with EContThy"
7.107
7.108 - | xml_of_contthy (Rtools.ContThm {thyID, thm, applto, applat, reword,
7.109 + | xml_of_contthy (Thy_Present.ContThm {thyID, thm, applto, applat, reword,
7.110 asms,lhs, rhs, result, resasms, asmrls}) =
7.111 XML.Elem (("CONTEXTDATA", []), [
7.112 XML.Elem (("GUH", []), [XML.Text thm]),
7.113 @@ -704,7 +704,7 @@
7.114 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
7.115 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
7.116
7.117 - | xml_of_contthy (Rtools.ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
7.118 + | xml_of_contthy (Thy_Present.ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
7.119 reword, asms, lhs, rhs, result, resasms, asmrls}) =
7.120 XML.Elem (("CONTEXTDATA", []), [
7.121 XML.Elem (("GUH", []), [XML.Text thm]),
7.122 @@ -724,14 +724,14 @@
7.123 XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
7.124 XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
7.125
7.126 - | xml_of_contthy (Rtools.ContRls {thyID = _, rls, applto, result, asms}) =
7.127 + | xml_of_contthy (Thy_Present.ContRls {thyID = _, rls, applto, result, asms}) =
7.128 XML.Elem (("CONTEXTDATA", []), [
7.129 XML.Elem (("GUH", []), [XML.Text rls]),
7.130 XML.Elem (("APPLTO", []), [xml_of_term applto]),
7.131 XML.Elem (("RESULT", []), [xml_of_term result]),
7.132 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
7.133
7.134 - | xml_of_contthy (Rtools.ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
7.135 + | xml_of_contthy (Thy_Present.ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
7.136 XML.Elem (("CONTEXTDATA", []), [
7.137 XML.Elem (("GUH", []), [XML.Text rls]),
7.138 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
7.139 @@ -741,12 +741,12 @@
7.140 XML.Elem (("RESULT", []), [xml_of_term result]),
7.141 XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
7.142
7.143 - | xml_of_contthy (Rtools.ContNOrew {thyID = _, thm_rls, applto}) =
7.144 + | xml_of_contthy (Thy_Present.ContNOrew {thyID = _, thm_rls, applto}) =
7.145 XML.Elem (("CONTEXTDATA", []), [
7.146 XML.Elem (("GUH", []), [XML.Text thm_rls]),
7.147 XML.Elem (("APPLTO", []), [xml_of_term applto])])
7.148
7.149 - | xml_of_contthy (Rtools.ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
7.150 + | xml_of_contthy (Thy_Present.ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
7.151 XML.Elem (("CONTEXTDATA", []), [
7.152 XML.Elem (("GUH", []), [XML.Text thm_rls]),
7.153 XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
8.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Apr 28 16:51:36 2020 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Apr 28 17:50:18 2020 +0200
8.3 @@ -326,13 +326,13 @@
8.4 if member op = [Pbl, Met] p_
8.5 then message2xml cI "thy-context not to calchead"
8.6 else if ip = ([], Res) then message2xml cI "no thy-context at result"
8.7 - else if Rtools.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
8.8 + else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
8.9 else
8.10 ((let
8.11 val (ptp as (pt, pold), _) = get_calc cI
8.12 val is = get_istate_LI pt ip
8.13 - val subs = Rtools.subs_from is "dummy" guh
8.14 - val tac = Rtools.guh2rewtac guh subs
8.15 + val subs = Thy_Present.subs_from is "dummy" guh
8.16 + val tac = Thy_Present.guh2rewtac guh subs
8.17 in
8.18 case Step.by_tactic tac (pt, ip) of (*='fun setNextTactic'+step*)
8.19 ("ok", (tacis, c, ptp as (_, p))) =>
8.20 @@ -580,10 +580,10 @@
8.21 then
8.22 let
8.23 val pos' = lev_on' pt pos
8.24 - val tac = Rtools.get_tac_checked pt pos'
8.25 + val tac = Thy_Present.get_tac_checked pt pos'
8.26 in
8.27 if Tactic.is_rewtac tac
8.28 - then contextthyOK2xml cI (Rtools.context_thy (pt, pos) tac)
8.29 + then contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac)
8.30 else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
8.31 end
8.32 else if is_curr_endof_calc pt pos
8.33 @@ -593,7 +593,7 @@
8.34 let val tac = fst3 (last_elem tacis)
8.35 in
8.36 if Tactic.is_rewtac tac
8.37 - then contextthyOK2xml cI (Rtools.context_thy ptp tac)
8.38 + then contextthyOK2xml cI (Thy_Present.context_thy ptp tac)
8.39 else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
8.40 end
8.41 | (msg, _) => message2xml cI msg
8.42 @@ -625,14 +625,14 @@
8.43 if member op = [Pbl, Met] p_
8.44 then message2xml cI "thy-context not to calchead"
8.45 else if pos = ([],Res) then message2xml cI "no thy-context at result"
8.46 - else if Rtools.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
8.47 + else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
8.48 else
8.49 ((let
8.50 val ((pt,_),_) = get_calc cI
8.51 val is = get_istate_LI pt pos
8.52 - val subs = Rtools.subs_from is "dummy" guh
8.53 - val tac = Rtools.guh2rewtac guh subs
8.54 - in contextthyOK2xml cI (Rtools.context_thy (pt, pos) tac) end
8.55 + val subs = Thy_Present.subs_from is "dummy" guh
8.56 + val tac = Thy_Present.guh2rewtac guh subs
8.57 + in contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac) end
8.58 ) handle _ => sysERROR2xml cI "error in kernel 34")
8.59 (*.match the model of a problem at pos p
8.60 with the model-pattern of the problem with pblID.*)
9.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 16:51:36 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
9.3 @@ -183,7 +183,7 @@
9.4 (**. write pbls from hierarchy to files.**)
9.5 fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Method.id) (pbl as {guh,...}) =
9.6 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos);
9.7 - ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
9.8 + ((str2file (path ^ Thy_Present.guh2filename guh)) o (pbl2xml id)) pbl
9.9 );
9.10
9.11 (**. write mets from hierarchy to files.**)
9.12 @@ -261,7 +261,7 @@
9.13 (*.write the files using the guh as filename.*)
9.14 fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) (met as {guh,...}) =
9.15 (writeln ("### met2file: id = " ^ strs2str id);
9.16 - ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
9.17 + ((str2file (path ^ Thy_Present.guh2filename guh)) o (met2xml id)) met);
9.18
9.19 (*.scan the mtree Ptyp and print the nodes using wfn.*)
9.20 fun node (pa: Celem.filepath) ids po wfn (Store.Node (id,[n],ns)) =
10.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 16:51:36 2020 +0200
10.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
10.3 @@ -6,32 +6,32 @@
10.4
10.5 signature THEORY_HIERARCHY =
10.6 sig
10.7 - val collect_cals: string * ThyC.id -> (Thy_Html.theID * Thy_Html.thydata) list
10.8 - val collect_isab: string -> string * thm -> Thy_Html.theID * Thy_Html.thydata
10.9 - val collect_ords: 'a * ThyC.id -> (Thy_Html.theID * Thy_Html.thydata) list
10.10 - val collect_part: string -> theory -> theory list -> (Thy_Html.theID * Thy_Html.thydata) list
10.11 + val collect_cals: string * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
10.12 + val collect_isab: string -> string * thm -> Thy_Write.theID * Thy_Write.thydata
10.13 + val collect_ords: 'a * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
10.14 + val collect_part: string -> theory -> theory list -> (Thy_Write.theID * Thy_Write.thydata) list
10.15 val collect_rlss: string -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory list ->
10.16 - (Thy_Html.theID * Thy_Html.thydata) list
10.17 - val collect_thms: string -> theory -> (Thy_Html.theID * Thy_Html.thydata) list
10.18 + (Thy_Write.theID * Thy_Write.thydata) list
10.19 + val collect_thms: string -> theory -> (Thy_Write.theID * Thy_Write.thydata) list
10.20
10.21 val hierarchy_guh: 'a Store.T -> string
10.22 - val insert_errpatIDs: 'a -> Thy_Html.theID -> Error_Pattern_Def.id list ->
10.23 - Thy_Html.thydata * Thy_Html.theID
10.24 + val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->
10.25 + Thy_Write.thydata * Thy_Write.theID
10.26
10.27 - val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Html.theID * Thy_Html.thydata
10.28 + val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Write.theID * Thy_Write.thydata
10.29 val makeHord: string * ThyC.id -> string * Rule_Def.rew_ord_ ->
10.30 - Thy_Html.theID * Thy_Html.thydata
10.31 + Thy_Write.theID * Thy_Write.thydata
10.32 val makeHrls: string -> Rule_Set.id * (ThyC.id * Rule_Def.rule_set) ->
10.33 - Thy_Html.theID * Thy_Html.thydata
10.34 - val makeHthm: string * ThyC.id -> thm -> Thy_Html.theID * Thy_Html.thydata
10.35 - val make_cal: theory -> Rule_Def.calc -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
10.36 - val make_isa: theory -> ThyC.id * ThyC.id -> Thy_Html.authors ->
10.37 - Thy_Html.thydata * Thy_Html.theID
10.38 - val make_ord: theory -> Rule_Def.rew_ord_ -> Thy_Html.authors ->
10.39 - Thy_Html.thydata * Thy_Html.theID
10.40 - val make_rls: theory -> Rule_Def.rule_set -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
10.41 - val make_thm: theory -> string -> string * thm -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
10.42 - val make_thy: theory -> Thy_Html.authors -> Thy_Html.thydata * Thy_Html.theID
10.43 + Thy_Write.theID * Thy_Write.thydata
10.44 + val makeHthm: string * ThyC.id -> thm -> Thy_Write.theID * Thy_Write.thydata
10.45 + val make_cal: theory -> Rule_Def.calc -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
10.46 + val make_isa: theory -> ThyC.id * ThyC.id -> Thy_Write.authors ->
10.47 + Thy_Write.thydata * Thy_Write.theID
10.48 + val make_ord: theory -> Rule_Def.rew_ord_ -> Thy_Write.authors ->
10.49 + Thy_Write.thydata * Thy_Write.theID
10.50 + val make_rls: theory -> Rule_Def.rule_set -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
10.51 + val make_thm: theory -> string -> string * thm -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
10.52 + val make_thy: theory -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
10.53
10.54 val show_thes: unit -> unit
10.55
10.56 @@ -40,8 +40,8 @@
10.57 val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
10.58 (string * thm) list
10.59 val thy_hierarchy2file: Celem.filepath -> unit
10.60 - val thydata2file: Celem.filepath -> Pos.pos -> Thy_Html.theID -> Thy_Html.thydata -> unit
10.61 - val thydata2xml: Thy_Html.theID * Thy_Html.thydata -> xml
10.62 + val thydata2file: Celem.filepath -> Pos.pos -> Thy_Write.theID -> Thy_Write.thydata -> unit
10.63 + val thydata2xml: Thy_Write.theID * Thy_Write.thydata -> xml
10.64 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.65 (*NONE*)
10.66 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.67 @@ -73,29 +73,29 @@
10.68 (* wrap theory-data into the uniform type thydata *)
10.69
10.70 fun makeHthm (part : string, thyID : ThyC.id) (thm : thm) =
10.71 - let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Thy_Html.theID
10.72 - in (theID, Thy_Html.Hthm {guh = Thy_Html.theID2guh theID, coursedesign = [],
10.73 + let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Thy_Write.theID
10.74 + in (theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID, coursedesign = [],
10.75 mathauthors = ["isac-team"], fillpats = [], thm = thm})
10.76 end;
10.77 fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.id * Rule_Set.T) =
10.78 - let val theID = [part, thyID,"Rulesets"] @ [rls'] : Thy_Html.theID
10.79 - in (theID, Thy_Html.Hrls {guh = Thy_Html.theID2guh theID, coursedesign = [],
10.80 + let val theID = [part, thyID,"Rulesets"] @ [rls'] : Thy_Write.theID
10.81 + in (theID, Thy_Write.Hrls {guh = Thy_Write.theID2guh theID, coursedesign = [],
10.82 mathauthors = ["isac-team"], thy_rls = thy_rls})
10.83 end;
10.84 fun makeHcal (part : string, thyID : ThyC.id) (calID, cal) =
10.85 - let val theID = [part, thyID,"Operations"] @ [calID] : Thy_Html.theID
10.86 - in (theID, Thy_Html.Hcal {guh = Thy_Html.theID2guh theID, coursedesign=[],
10.87 + let val theID = [part, thyID,"Operations"] @ [calID] : Thy_Write.theID
10.88 + in (theID, Thy_Write.Hcal {guh = Thy_Write.theID2guh theID, coursedesign=[],
10.89 mathauthors = ["isac-team"], calc = cal})
10.90 end;
10.91 fun makeHord (part : string, thyID : ThyC.id) (ordID, ord) =
10.92 - let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Thy_Html.theID
10.93 - in (theID, Thy_Html.Hord {guh = Thy_Html.theID2guh theID, coursedesign=[],
10.94 + let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Thy_Write.theID
10.95 + in (theID, Thy_Write.Hord {guh = Thy_Write.theID2guh theID, coursedesign=[],
10.96 mathauthors = ["isac-team"], ord = ord})
10.97 end;
10.98
10.99 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
10.100 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
10.101 - |> map (Rtools.thms_of_rls o #2 o #2)
10.102 + |> map (Thy_Present.thms_of_rls o #2 o #2)
10.103 |> flat
10.104 |> map (ThmC.revert_sym_rule thy)
10.105 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
10.106 @@ -114,7 +114,7 @@
10.107 in map (makeHcal (part, thy')) cals end;
10.108 fun collect_ords (part, thy') =
10.109 let val thy = ThyC.get_theory thy'
10.110 - in [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Html.theID * Thy_Html.thydata) list end;
10.111 + in [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list end;
10.112
10.113 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)
10.114 fun collect_part part parent thys =
10.115 @@ -127,7 +127,7 @@
10.116 let val theID =
10.117 [isa, ThyC.cut_id thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
10.118 in
10.119 - (theID: Thy_Html.theID, Thy_Html.Hthm {guh = Thy_Html.theID2guh theID,
10.120 + (theID: Thy_Write.theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID,
10.121 mathauthors = ["Isabelle team, TU Munich"],
10.122 coursedesign = [],
10.123 fillpats = [],
10.124 @@ -153,7 +153,7 @@
10.125 (indt i) ^ "<NODE>\n" ^
10.126 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
10.127 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
10.128 - (indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Html.theID2guh theID' ^ " </CONTENTREF>\n" ^
10.129 + (indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Write.theID2guh theID' ^ " </CONTENTREF>\n" ^
10.130 (nodes (i+j) (Pos.lev_dn p') theID' ns) ^
10.131 (indt i) ^ "</NODE>\n"
10.132 end
10.133 @@ -173,7 +173,7 @@
10.134 (* create the xml-files for the thydata in the hierarchy *)
10.135 val i = indentation;
10.136 (* analoguous to 'fun met2xml' *)
10.137 -fun thydata2xml (theID: Thy_Html.theID, Thy_Html.Html {guh, coursedesign, mathauthors, html}) =
10.138 +fun thydata2xml (theID: Thy_Write.theID, Thy_Write.Html {guh, coursedesign, mathauthors, html}) =
10.139 "<HTMLDATA>\n" ^
10.140 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.141 id2xml i theID ^
10.142 @@ -181,7 +181,7 @@
10.143 authors2xml i "MATHAUTHORS" mathauthors ^
10.144 authors2xml i "COURSEDESIGNS" coursedesign ^
10.145 "</HTMLDATA>\n" : xml
10.146 - | thydata2xml (theID, Thy_Html.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
10.147 + | thydata2xml (theID, Thy_Write.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
10.148 "<THEOREMDATA>\n" ^
10.149 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.150 id2xml i theID ^
10.151 @@ -195,7 +195,7 @@
10.152 authors2xml i "MATHAUTHORS" mathauthors ^
10.153 authors2xml i "COURSEDESIGNS" coursedesign ^
10.154 "</THEOREMDATA>\n"
10.155 - | thydata2xml (theID, Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
10.156 + | thydata2xml (theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
10.157 "<RULESETDATA>\n" ^
10.158 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.159 id2xml i theID ^
10.160 @@ -204,11 +204,11 @@
10.161 authors2xml i "MATHAUTHORS" mathauthors ^
10.162 authors2xml i "COURSEDESIGNS" coursedesign ^
10.163 "</RULESETDATA>\n"
10.164 - | thydata2xml (theID, Thy_Html.Hcal {guh, coursedesign, mathauthors, calc}) =
10.165 + | thydata2xml (theID, Thy_Write.Hcal {guh, coursedesign, mathauthors, calc}) =
10.166 "<RULESETDATA>\n" ^
10.167 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.168 id2xml i theID ^
10.169 - calc2xml i (Thy_Html.theID2thyID theID, calc) ^
10.170 + calc2xml i (Thy_Write.theID2thyID theID, calc) ^
10.171 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.172 authors2xml i "MATHAUTHORS" mathauthors ^
10.173 authors2xml i "COURSEDESIGNS" coursedesign ^
10.174 @@ -217,9 +217,9 @@
10.175 error ("thydata2xml: not implemented for "^ strs2str' theID);
10.176
10.177 (* analoguous to 'fun met2file' *)
10.178 -fun thydata2file (path : Celem.filepath) (pos : Pos.pos) (theID : Thy_Html.theID) thydata =
10.179 +fun thydata2file (path : Celem.filepath) (pos : Pos.pos) (theID : Thy_Write.theID) thydata =
10.180 (writeln ("### thes2file: id = " ^ strs2str theID);
10.181 - str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
10.182 + str2file (path ^ Thy_Present.theID2filename theID) (thydata2xml (theID, thydata)));
10.183
10.184 (* analoguous to 'fun node' *)
10.185 fun thenode (pa : Celem.filepath) ids po wfn (Store.Node (id, [n], ns)) =
10.186 @@ -236,52 +236,52 @@
10.187 (***.store a single theory element in the hierarchy.***)
10.188
10.189 (*.for mathauthors only, other html is added to xml exported from here.*)
10.190 -fun make_isa thy (part, thypart) (mathauthors : Thy_Html.authors) =
10.191 +fun make_isa thy (part, thypart) (mathauthors : Thy_Write.authors) =
10.192 let
10.193 val theID = [part, Context.theory_name thy, thypart]
10.194 val guh = case theID of
10.195 - [part] => Thy_Html.part2guh theID
10.196 - | [part, thyID, thypart] => Thy_Html.thypart2guh theID
10.197 - val theID = Rtools.guh2theID guh
10.198 - val the = Thy_Html.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
10.199 + [part] => Thy_Write.part2guh theID
10.200 + | [part, thyID, thypart] => Thy_Write.thypart2guh theID
10.201 + val theID = Thy_Present.guh2theID guh
10.202 + val the = Thy_Write.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
10.203 in (the, theID) end
10.204
10.205 -fun make_thy thy (mathauthors : Thy_Html.authors) =
10.206 +fun make_thy thy (mathauthors : Thy_Write.authors) =
10.207 let
10.208 - val guh = Thy_Html.thy2guh ["IsacKnowledge", Context.theory_name thy]
10.209 - val theID = Rtools.guh2theID guh
10.210 - val the = Thy_Html.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
10.211 + val guh = Thy_Write.thy2guh ["IsacKnowledge", Context.theory_name thy]
10.212 + val theID = Thy_Present.guh2theID guh
10.213 + val the = Thy_Write.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
10.214 in (the, theID) end
10.215
10.216 -fun make_thm thy part (thmID : ThmC.id, thm) (mathauthors : Thy_Html.authors) =
10.217 +fun make_thm thy part (thmID : ThmC.id, thm) (mathauthors : Thy_Write.authors) =
10.218 let
10.219 - val guh = Thy_Html.thm2guh (part, Context.theory_name thy) thmID
10.220 - val theID = Rtools.guh2theID guh
10.221 - val the = Thy_Html.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
10.222 + val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
10.223 + val theID = Thy_Present.guh2theID guh
10.224 + val the = Thy_Write.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
10.225 mathauthors = mathauthors, fillpats = [], thm = thm}
10.226 in (the, theID) end
10.227
10.228 -fun make_rls thy rls (mathauthors : Thy_Html.authors) =
10.229 +fun make_rls thy rls (mathauthors : Thy_Write.authors) =
10.230 let
10.231 - val guh = Thy_Html.rls2guh ("IsacKnowledge", Context.theory_name thy) ((#id o Rule_Set.rep) rls)
10.232 - val theID = Rtools.guh2theID guh
10.233 - val the = Thy_Html.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
10.234 + val guh = Thy_Write.rls2guh ("IsacKnowledge", Context.theory_name thy) ((#id o Rule_Set.rep) rls)
10.235 + val theID = Thy_Present.guh2theID guh
10.236 + val the = Thy_Write.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
10.237 thy_rls = (Context.theory_name thy, rls)}
10.238 (*needs no (!check_guhs_unique) because guh is generated automatically*)
10.239 in (the, theID) end
10.240
10.241 -fun make_cal thy cal (mathauthors : Thy_Html.authors) =
10.242 +fun make_cal thy cal (mathauthors : Thy_Write.authors) =
10.243 let
10.244 - val guh = Thy_Html.cal2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_cal")
10.245 - val theID = Rtools.guh2theID guh
10.246 - val the = Thy_Html.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
10.247 + val guh = Thy_Write.cal2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_cal")
10.248 + val theID = Thy_Present.guh2theID guh
10.249 + val the = Thy_Write.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
10.250 in (the, theID) end
10.251
10.252 -fun make_ord thy ord (mathauthors : Thy_Html.authors) =
10.253 +fun make_ord thy ord (mathauthors : Thy_Write.authors) =
10.254 let
10.255 - val guh = Thy_Html.ord2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_ord")
10.256 - val theID = Rtools.guh2theID guh
10.257 - val the = Thy_Html.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
10.258 + val guh = Thy_Write.ord2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_ord")
10.259 + val theID = Thy_Present.guh2theID guh
10.260 + val the = Thy_Write.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
10.261 in (the, theID) end
10.262
10.263 fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-present.sml Tue Apr 28 17:50:18 2020 +0200
11.3 @@ -0,0 +1,324 @@
11.4 +(*
11.5 + authors: Walther Neuper 2002, 2006
11.6 + (c) due to copyright terms
11.7 +
11.8 +tools for rewriting, reverse rewriting, context to thy concerning rewriting
11.9 +*)
11.10 +
11.11 +signature THEORY_DATA_PRESENTATION =
11.12 +sig
11.13 +
11.14 + datatype contthy
11.15 + = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
11.16 + | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
11.17 + | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
11.18 + | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
11.19 + | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
11.20 + lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
11.21 + thm: Check_Unique.id, thyID: ThyC.id}
11.22 + | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
11.23 + bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
11.24 + rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
11.25 + | EContThy
11.26 + val guh2filename : Check_Unique.id -> Celem.filename
11.27 + val thms_of_rls : Rule_Set.T -> Rule.rule list
11.28 + val theID2filename : Thy_Write.theID -> Celem.filename
11.29 + val no_thycontext : Check_Unique.id -> bool
11.30 + val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input
11.31 + val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input
11.32 + val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
11.33 + val context_thy : Calc.T -> Tactic.input -> contthy
11.34 + val guh2theID : Check_Unique.id -> Thy_Write.theID
11.35 +
11.36 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.37 + (* NONE *)
11.38 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.39 + (* NONE *)
11.40 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.41 +end
11.42 +(**)
11.43 +structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) =
11.44 +struct
11.45 +(**)
11.46 +
11.47 +(* packing return-values to matchTheory, contextToThy for xml-generation *)
11.48 +datatype contthy = (*also an item from Know_Store on Browser ...........#*)
11.49 + EContThy (* not from Know_Store ..............................*)
11.50 + | ContThm of (* a theorem in contex ===========================*)
11.51 + {thyID : ThyC.id, (* for *2guh in sub-elems here .*)
11.52 + thm : Check_Unique.id, (* theorem in the context .*)
11.53 + applto : term, (* applied to formula ... .*)
11.54 + applat : term, (* ... with lhs inserted .*)
11.55 + reword : Rewrite_Ord.rew_ord', (* order used for rewrite .*)
11.56 + asms : (term (* asumption instantiated .*)
11.57 + * term) list, (* asumption evaluated .*)
11.58 + lhs : term (* lhs of the theorem ... #*)
11.59 + * term, (* ... instantiated .*)
11.60 + rhs : term (* rhs of the theorem ... #*)
11.61 + * term, (* ... instantiated .*)
11.62 + result : term, (* resulting from the rewrite .*)
11.63 + resasms : term list, (* ... with asms stored .*)
11.64 + asmrls : Rule_Set.id (* ruleset for evaluating asms .*)
11.65 + }
11.66 + | ContThmInst of (* a theorem with bdvs in contex ============ *)
11.67 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
11.68 + thm : Check_Unique.id, (*theorem in the context .*)
11.69 + bdvs : subst, (*bound variables to modify... .*)
11.70 + thminst : term, (*... theorem instantiated .*)
11.71 + applto : term, (*applied to formula ... .*)
11.72 + applat : term, (*... with lhs inserted .*)
11.73 + reword : Rewrite_Ord.rew_ord', (*order used for rewrite .*)
11.74 + asms : (term (*asumption instantiated .*)
11.75 + * term) list, (*asumption evaluated .*)
11.76 + lhs : term (*lhs of the theorem ... #*)
11.77 + * term, (*... instantiated .*)
11.78 + rhs : term (*rhs of the theorem ... #*)
11.79 + * term, (*... instantiated .*)
11.80 + result : term, (*resulting from the rewrite .*)
11.81 + resasms : term list, (*... with asms stored .*)
11.82 + asmrls : Rule_Set.id (*ruleset for evaluating asms .*)
11.83 + }
11.84 + | ContRls of (* a rule set in contex ========================= *)
11.85 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
11.86 + rls : Check_Unique.id, (*rule set in the context .*)
11.87 + applto : term, (*rewrite this formula .*)
11.88 + result : term, (*resulting from the rewrite .*)
11.89 + asms : term list (*... with asms stored .*)
11.90 + }
11.91 + | ContRlsInst of (* a rule set with bdvs in contex =========== *)
11.92 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
11.93 + rls : Check_Unique.id, (*rule set in the context .*)
11.94 + bdvs : subst, (*for bound variables in thms .*)
11.95 + applto : term, (*rewrite this formula .*)
11.96 + result : term, (*resulting from the rewrite .*)
11.97 + asms : term list (*... with asms stored .*)
11.98 + }
11.99 + | ContNOrew of (* no rewrite for thm or rls ================== *)
11.100 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
11.101 + thm_rls : Check_Unique.id, (*thm or rls in the context .*)
11.102 + applto : term (*rewrite this formula .*)
11.103 + }
11.104 + | ContNOrewInst of (* no rewrite for some instantiation ====== *)
11.105 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
11.106 + thm_rls : Check_Unique.id, (*thm or rls in the context .*)
11.107 + bdvs : subst, (*for bound variables in thms .*)
11.108 + thminst : term, (*... theorem instantiated .*)
11.109 + applto : term (*rewrite this formula .*)
11.110 + }
11.111 +
11.112 +(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
11.113 + pass other tacs unchanged.*)
11.114 +fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;
11.115 +
11.116 +(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
11.117 +fun context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite thm'') =
11.118 + let
11.119 + val thm_deriv = ThmC.long_id thm''
11.120 + in
11.121 + (case Applicable.applicable_in pos pt tac of
11.122 + Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
11.123 + ContThm
11.124 + {thyID = thy',
11.125 + thm = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
11.126 + applto = f, applat = TermC.empty, reword = ord',
11.127 + asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
11.128 + result = res, resasms = asm, asmrls = Rule_Set.id erls}
11.129 + | Applicable.Notappl _ =>
11.130 + let
11.131 + val pp = Ctree.par_pblobj pt p
11.132 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
11.133 + val f = case p_ of
11.134 + Pos.Frm => Ctree.get_obj Ctree.g_form pt p
11.135 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
11.136 + | _ => error "context_thy: uncovered position"
11.137 + in
11.138 + ContNOrew
11.139 + {thyID = thy',
11.140 + thm_rls =
11.141 + Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
11.142 + applto = f}
11.143 + end
11.144 + | _ => error "context_thy..Rewrite: uncovered case 2")
11.145 + end
11.146 + | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =
11.147 + let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID
11.148 + in
11.149 + (case Applicable.applicable_in pos pt tac of
11.150 + Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
11.151 + let
11.152 + val thm_deriv = Thm.get_name_hint thm
11.153 + val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
11.154 + in
11.155 + ContThmInst
11.156 + {thyID = thy',
11.157 + thm =
11.158 + Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
11.159 + bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
11.160 + asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
11.161 + result = res, resasms = asm, asmrls = Rule_Set.id erls}
11.162 + end
11.163 + | Applicable.Notappl _ =>
11.164 + let
11.165 + val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
11.166 + val thm_deriv = Thm.get_name_hint thm
11.167 + val pp = Ctree.par_pblobj pt p
11.168 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
11.169 + val subst = Subst.T_from_input (ThyC.get_theory thy') subs
11.170 + val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
11.171 + val f = case p_ of
11.172 + Pos.Frm => Ctree.get_obj Ctree.g_form pt p
11.173 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
11.174 + | _ => error "context_thy: uncovered case 3"
11.175 + in
11.176 + ContNOrewInst
11.177 + {thyID = thy',
11.178 + thm_rls = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
11.179 + bdvs = subst, thminst = thminst, applto = f}
11.180 + end
11.181 + | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
11.182 + end
11.183 + | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =
11.184 + (case Applicable.applicable_in p pt tac of
11.185 + Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
11.186 + ContRls
11.187 + {thyID = thy',
11.188 + rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
11.189 + applto = f, result = res, asms = asm}
11.190 + | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
11.191 + | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
11.192 + (case Applicable.applicable_in p pt tac of
11.193 + Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
11.194 + ContRlsInst
11.195 + {thyID = thy',
11.196 + rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
11.197 + bdvs = subst, applto = f, result = res, asms = asm}
11.198 + | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
11.199 + | context_thy (_, p) tac =
11.200 + error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)
11.201 +
11.202 +(* get all theorems in a rule set (recursivley containing rule sets) *)
11.203 +fun thm_of_rule Rule.Erule = []
11.204 + | thm_of_rule (thm as Rule.Thm _) = [thm]
11.205 + | thm_of_rule (Rule.Eval _) = []
11.206 + | thm_of_rule (Rule.Cal1 _) = []
11.207 + | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
11.208 +and thms_of_rls Rule_Set.Empty = []
11.209 + | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules
11.210 + | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
11.211 + | thms_of_rls (Rule_Set.Rrls _) = []
11.212 +
11.213 +
11.214 +(* filenames not only for thydata, but also for thy's etc *)
11.215 +fun theID2filename theID = Thy_Write.theID2guh theID ^ ".xml"
11.216 +
11.217 +fun guh2theID guh =
11.218 + let
11.219 + val guh' = Symbol.explode guh
11.220 + val part = implode (take_fromto 1 4 guh')
11.221 + val isa = implode (take_fromto 5 9 guh')
11.222 + in
11.223 + if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
11.224 + then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")
11.225 + else
11.226 + let
11.227 + val chap = case isa of
11.228 + "isab_" => "Isabelle"
11.229 + | "scri_" => "IsacScripts"
11.230 + | "isac_" => "IsacKnowledge"
11.231 + | _ =>
11.232 + raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")
11.233 + val rest = takerest (9, guh')
11.234 + val thyID = takewhile [] (not o (curry op= "-")) rest
11.235 + val rest' = dropuntil (curry op = "-") rest
11.236 + in case implode rest' of
11.237 + "-part" => [chap] : Thy_Write.theID
11.238 + | "" => [chap, implode thyID]
11.239 + | "-Theorems" => [chap, implode thyID, "Theorems"]
11.240 + | "-Rulesets" => [chap, implode thyID, "Rulesets"]
11.241 + | "-Operations" => [chap, implode thyID, "Operations"]
11.242 + | "-Orders" => [chap, implode thyID, "Orders"]
11.243 + | _ =>
11.244 + let val sect = implode (take_fromto 1 5 rest')
11.245 + val sect' = case sect of
11.246 + "-thm-" => "Theorems"
11.247 + | "-rls-" => "Rulesets"
11.248 + | "-cal-" => "Operations"
11.249 + | "-ord-" => "Orders"
11.250 + | _ =>
11.251 + raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")
11.252 + in
11.253 + [chap, implode thyID, sect', implode (takerest (5, rest'))]
11.254 + end
11.255 + end
11.256 + end
11.257 +
11.258 +fun guh2filename guh = guh ^ ".xml";
11.259 +
11.260 +fun guh2rewtac guh [] =
11.261 + let
11.262 + val (_, thy, sect, xstr) = case guh2theID guh of
11.263 + [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
11.264 + | _ => error "guh2rewtac: uncovered case"
11.265 + in case sect of
11.266 + "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr)
11.267 + | "Rulesets" => Tactic.Rewrite_Set xstr
11.268 + | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
11.269 + end
11.270 + | guh2rewtac guh subs =
11.271 + let
11.272 + val (_, thy, sect, xstr) = case guh2theID guh of
11.273 + [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
11.274 + | _ => error "guh2rewtac: uncovered case"
11.275 + in case sect of
11.276 + "Theorems" =>
11.277 + Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr))
11.278 + | "Rulesets" => Tactic.Rewrite_Set_Inst (subs, xstr)
11.279 + | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
11.280 + end
11.281 +
11.282 +(* the front-end may request a context for any element of the hierarchy *)
11.283 +fun no_thycontext guh = (guh2theID guh; false)
11.284 + handle ERROR _ => true;
11.285 +
11.286 +(* get the substitution of bound variables for matchTheory:
11.287 + # lookup the thm|rls' in the script
11.288 + # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
11.289 + # instantiate this subs with the istates env to [(bdv, x),..]
11.290 + # otherwise []
11.291 + WN060617 hack assuming that all scripts use only one bound variable
11.292 + and use 'v_' as the formal argument for this bound variable*)
11.293 +fun subs_from (Istate.Pstate ({env, ...})) _ guh =
11.294 + let
11.295 + val (_, _, thyID, sect, xstr) = case guh2theID guh of
11.296 + theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
11.297 + | _ => error "subs_from: uncovered case"
11.298 + in
11.299 + case sect of
11.300 + "Theorems" =>
11.301 + let val thm = Global_Theory.get_thm (ThyC.get_theory thyID) xstr
11.302 + in
11.303 + if Auto_Prog.contains_bdv thm
11.304 + then
11.305 + let
11.306 + val formal_arg = TermC.str2term "v_"
11.307 + val value = subst_atomic env formal_arg
11.308 + in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
11.309 + else []
11.310 + end
11.311 + | "Rulesets" =>
11.312 + let
11.313 + val rules = (Rule_Set.get_rules o assoc_rls) xstr
11.314 + in
11.315 + if Auto_Prog.contain_bdv rules
11.316 + then
11.317 + let
11.318 + val formal_arg = TermC.str2term "v_"
11.319 + val value = subst_atomic env formal_arg
11.320 + in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
11.321 + else []
11.322 + end
11.323 + | str => error ("subs_from: uncovered case with " ^ str)
11.324 + end
11.325 + | subs_from _ _ guh = error ("subs_from: uncovered case with " ^ guh)
11.326 +
11.327 +(**)end(**)
12.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Apr 28 16:51:36 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Apr 28 17:50:18 2020 +0200
12.3 @@ -12,7 +12,6 @@
12.4 ML_file istate.sml
12.5 ML_file "sub-problem.sml"
12.6 ML_file "thy-read.sml"
12.7 - ML_file rewtools.sml
12.8 ML_file "error-pattern.sml"
12.9 ML_file derive.sml
12.10 ML_file "li-tool.sml"
13.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Tue Apr 28 16:51:36 2020 +0200
13.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Tue Apr 28 17:50:18 2020 +0200
13.3 @@ -23,13 +23,13 @@
13.4
13.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.6 val find_fill_patterns: Calc.T -> id -> record list
13.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
13.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.9 val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
13.10 val fill_from_store: Subst.input option * (term * term) list -> term -> id -> thm ->
13.11 record list
13.12 val fill_form: Subst.input option * (term * term) list -> thm * term -> id -> fill_in ->
13.13 record option
13.14 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.15 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.16 end
13.17
13.18 (**)
13.19 @@ -104,7 +104,7 @@
13.20 val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
13.21 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
13.22 val fillpats = case Specify.get_the theID of
13.23 - Thy_Html.Hthm {fillpats, ...} => fillpats
13.24 + Thy_Write.Hthm {fillpats, ...} => fillpats
13.25 | _ => raise ERROR "fill_from_store: uncovered case of get_the"
13.26 val some = map (fill_form subst (thm, form) id) fillpats
13.27 in some |> filter is_some |> map the end
13.28 @@ -162,7 +162,7 @@
13.29 | _ => "empty"
13.30 val (part, thyID) = Thy_Read.thy_containing_rls "Isac_Knowledge" rlsID;
13.31 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
13.32 - Thy_Html.Hrls {thy_rls = (_, rls), ...} => rls
13.33 + Thy_Write.Hrls {thy_rls = (_, rls), ...} => rls
13.34 | _ => raise ERROR "from_store: uncovered case of get_the"
13.35 in case rls of
13.36 Rule_Def.Repeat {errpatts, ...} => errpatts
14.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Apr 28 16:51:36 2020 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,324 +0,0 @@
14.4 -(*
14.5 - authors: Walther Neuper 2002, 2006
14.6 - (c) due to copyright terms
14.7 -
14.8 -tools for rewriting, reverse rewriting, context to thy concerning rewriting
14.9 -*)
14.10 -
14.11 -signature REWRITE_TOOLS =
14.12 -sig
14.13 -
14.14 - datatype contthy
14.15 - = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
14.16 - | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
14.17 - | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
14.18 - | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
14.19 - | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
14.20 - lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
14.21 - thm: Check_Unique.id, thyID: ThyC.id}
14.22 - | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
14.23 - bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
14.24 - rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
14.25 - | EContThy
14.26 - val guh2filename : Check_Unique.id -> Celem.filename
14.27 - val thms_of_rls : Rule_Set.T -> Rule.rule list
14.28 - val theID2filename : Thy_Html.theID -> Celem.filename
14.29 - val no_thycontext : Check_Unique.id -> bool
14.30 - val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input
14.31 - val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input
14.32 - val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
14.33 - val context_thy : Calc.T -> Tactic.input -> contthy
14.34 - val guh2theID : Check_Unique.id -> Thy_Html.theID
14.35 -
14.36 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.37 - (* NONE *)
14.38 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
14.39 - (* NONE *)
14.40 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.41 -end
14.42 -(**)
14.43 -structure Rtools(**): REWRITE_TOOLS(**) =
14.44 -struct
14.45 -(**)
14.46 -
14.47 -(* packing return-values to matchTheory, contextToThy for xml-generation *)
14.48 -datatype contthy = (*also an item from Know_Store on Browser ...........#*)
14.49 - EContThy (* not from Know_Store ..............................*)
14.50 - | ContThm of (* a theorem in contex ===========================*)
14.51 - {thyID : ThyC.id, (* for *2guh in sub-elems here .*)
14.52 - thm : Check_Unique.id, (* theorem in the context .*)
14.53 - applto : term, (* applied to formula ... .*)
14.54 - applat : term, (* ... with lhs inserted .*)
14.55 - reword : Rewrite_Ord.rew_ord', (* order used for rewrite .*)
14.56 - asms : (term (* asumption instantiated .*)
14.57 - * term) list, (* asumption evaluated .*)
14.58 - lhs : term (* lhs of the theorem ... #*)
14.59 - * term, (* ... instantiated .*)
14.60 - rhs : term (* rhs of the theorem ... #*)
14.61 - * term, (* ... instantiated .*)
14.62 - result : term, (* resulting from the rewrite .*)
14.63 - resasms : term list, (* ... with asms stored .*)
14.64 - asmrls : Rule_Set.id (* ruleset for evaluating asms .*)
14.65 - }
14.66 - | ContThmInst of (* a theorem with bdvs in contex ============ *)
14.67 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
14.68 - thm : Check_Unique.id, (*theorem in the context .*)
14.69 - bdvs : subst, (*bound variables to modify... .*)
14.70 - thminst : term, (*... theorem instantiated .*)
14.71 - applto : term, (*applied to formula ... .*)
14.72 - applat : term, (*... with lhs inserted .*)
14.73 - reword : Rewrite_Ord.rew_ord', (*order used for rewrite .*)
14.74 - asms : (term (*asumption instantiated .*)
14.75 - * term) list, (*asumption evaluated .*)
14.76 - lhs : term (*lhs of the theorem ... #*)
14.77 - * term, (*... instantiated .*)
14.78 - rhs : term (*rhs of the theorem ... #*)
14.79 - * term, (*... instantiated .*)
14.80 - result : term, (*resulting from the rewrite .*)
14.81 - resasms : term list, (*... with asms stored .*)
14.82 - asmrls : Rule_Set.id (*ruleset for evaluating asms .*)
14.83 - }
14.84 - | ContRls of (* a rule set in contex ========================= *)
14.85 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
14.86 - rls : Check_Unique.id, (*rule set in the context .*)
14.87 - applto : term, (*rewrite this formula .*)
14.88 - result : term, (*resulting from the rewrite .*)
14.89 - asms : term list (*... with asms stored .*)
14.90 - }
14.91 - | ContRlsInst of (* a rule set with bdvs in contex =========== *)
14.92 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
14.93 - rls : Check_Unique.id, (*rule set in the context .*)
14.94 - bdvs : subst, (*for bound variables in thms .*)
14.95 - applto : term, (*rewrite this formula .*)
14.96 - result : term, (*resulting from the rewrite .*)
14.97 - asms : term list (*... with asms stored .*)
14.98 - }
14.99 - | ContNOrew of (* no rewrite for thm or rls ================== *)
14.100 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
14.101 - thm_rls : Check_Unique.id, (*thm or rls in the context .*)
14.102 - applto : term (*rewrite this formula .*)
14.103 - }
14.104 - | ContNOrewInst of (* no rewrite for some instantiation ====== *)
14.105 - {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
14.106 - thm_rls : Check_Unique.id, (*thm or rls in the context .*)
14.107 - bdvs : subst, (*for bound variables in thms .*)
14.108 - thminst : term, (*... theorem instantiated .*)
14.109 - applto : term (*rewrite this formula .*)
14.110 - }
14.111 -
14.112 -(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
14.113 - pass other tacs unchanged.*)
14.114 -fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;
14.115 -
14.116 -(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
14.117 -fun context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite thm'') =
14.118 - let
14.119 - val thm_deriv = ThmC.long_id thm''
14.120 - in
14.121 - (case Applicable.applicable_in pos pt tac of
14.122 - Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
14.123 - ContThm
14.124 - {thyID = thy',
14.125 - thm = Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
14.126 - applto = f, applat = TermC.empty, reword = ord',
14.127 - asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
14.128 - result = res, resasms = asm, asmrls = Rule_Set.id erls}
14.129 - | Applicable.Notappl _ =>
14.130 - let
14.131 - val pp = Ctree.par_pblobj pt p
14.132 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
14.133 - val f = case p_ of
14.134 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
14.135 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
14.136 - | _ => error "context_thy: uncovered position"
14.137 - in
14.138 - ContNOrew
14.139 - {thyID = thy',
14.140 - thm_rls =
14.141 - Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
14.142 - applto = f}
14.143 - end
14.144 - | _ => error "context_thy..Rewrite: uncovered case 2")
14.145 - end
14.146 - | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =
14.147 - let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID
14.148 - in
14.149 - (case Applicable.applicable_in pos pt tac of
14.150 - Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
14.151 - let
14.152 - val thm_deriv = Thm.get_name_hint thm
14.153 - val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
14.154 - in
14.155 - ContThmInst
14.156 - {thyID = thy',
14.157 - thm =
14.158 - Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
14.159 - bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
14.160 - asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
14.161 - result = res, resasms = asm, asmrls = Rule_Set.id erls}
14.162 - end
14.163 - | Applicable.Notappl _ =>
14.164 - let
14.165 - val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
14.166 - val thm_deriv = Thm.get_name_hint thm
14.167 - val pp = Ctree.par_pblobj pt p
14.168 - val thy' = Ctree.get_obj Ctree.g_domID pt pp
14.169 - val subst = Subst.T_from_input (ThyC.get_theory thy') subs
14.170 - val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
14.171 - val f = case p_ of
14.172 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
14.173 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
14.174 - | _ => error "context_thy: uncovered case 3"
14.175 - in
14.176 - ContNOrewInst
14.177 - {thyID = thy',
14.178 - thm_rls = Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
14.179 - bdvs = subst, thminst = thminst, applto = f}
14.180 - end
14.181 - | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
14.182 - end
14.183 - | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =
14.184 - (case Applicable.applicable_in p pt tac of
14.185 - Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
14.186 - ContRls
14.187 - {thyID = thy',
14.188 - rls = Thy_Html.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
14.189 - applto = f, result = res, asms = asm}
14.190 - | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
14.191 - | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
14.192 - (case Applicable.applicable_in p pt tac of
14.193 - Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
14.194 - ContRlsInst
14.195 - {thyID = thy',
14.196 - rls = Thy_Html.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
14.197 - bdvs = subst, applto = f, result = res, asms = asm}
14.198 - | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
14.199 - | context_thy (_, p) tac =
14.200 - error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)
14.201 -
14.202 -(* get all theorems in a rule set (recursivley containing rule sets) *)
14.203 -fun thm_of_rule Rule.Erule = []
14.204 - | thm_of_rule (thm as Rule.Thm _) = [thm]
14.205 - | thm_of_rule (Rule.Eval _) = []
14.206 - | thm_of_rule (Rule.Cal1 _) = []
14.207 - | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
14.208 -and thms_of_rls Rule_Set.Empty = []
14.209 - | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules
14.210 - | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
14.211 - | thms_of_rls (Rule_Set.Rrls _) = []
14.212 -
14.213 -
14.214 -(* filenames not only for thydata, but also for thy's etc *)
14.215 -fun theID2filename theID = Thy_Html.theID2guh theID ^ ".xml"
14.216 -
14.217 -fun guh2theID guh =
14.218 - let
14.219 - val guh' = Symbol.explode guh
14.220 - val part = implode (take_fromto 1 4 guh')
14.221 - val isa = implode (take_fromto 5 9 guh')
14.222 - in
14.223 - if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
14.224 - then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")
14.225 - else
14.226 - let
14.227 - val chap = case isa of
14.228 - "isab_" => "Isabelle"
14.229 - | "scri_" => "IsacScripts"
14.230 - | "isac_" => "IsacKnowledge"
14.231 - | _ =>
14.232 - raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")
14.233 - val rest = takerest (9, guh')
14.234 - val thyID = takewhile [] (not o (curry op= "-")) rest
14.235 - val rest' = dropuntil (curry op = "-") rest
14.236 - in case implode rest' of
14.237 - "-part" => [chap] : Thy_Html.theID
14.238 - | "" => [chap, implode thyID]
14.239 - | "-Theorems" => [chap, implode thyID, "Theorems"]
14.240 - | "-Rulesets" => [chap, implode thyID, "Rulesets"]
14.241 - | "-Operations" => [chap, implode thyID, "Operations"]
14.242 - | "-Orders" => [chap, implode thyID, "Orders"]
14.243 - | _ =>
14.244 - let val sect = implode (take_fromto 1 5 rest')
14.245 - val sect' = case sect of
14.246 - "-thm-" => "Theorems"
14.247 - | "-rls-" => "Rulesets"
14.248 - | "-cal-" => "Operations"
14.249 - | "-ord-" => "Orders"
14.250 - | _ =>
14.251 - raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")
14.252 - in
14.253 - [chap, implode thyID, sect', implode (takerest (5, rest'))]
14.254 - end
14.255 - end
14.256 - end
14.257 -
14.258 -fun guh2filename guh = guh ^ ".xml";
14.259 -
14.260 -fun guh2rewtac guh [] =
14.261 - let
14.262 - val (_, thy, sect, xstr) = case guh2theID guh of
14.263 - [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
14.264 - | _ => error "guh2rewtac: uncovered case"
14.265 - in case sect of
14.266 - "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr)
14.267 - | "Rulesets" => Tactic.Rewrite_Set xstr
14.268 - | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
14.269 - end
14.270 - | guh2rewtac guh subs =
14.271 - let
14.272 - val (_, thy, sect, xstr) = case guh2theID guh of
14.273 - [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
14.274 - | _ => error "guh2rewtac: uncovered case"
14.275 - in case sect of
14.276 - "Theorems" =>
14.277 - Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr))
14.278 - | "Rulesets" => Tactic.Rewrite_Set_Inst (subs, xstr)
14.279 - | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
14.280 - end
14.281 -
14.282 -(* the front-end may request a context for any element of the hierarchy *)
14.283 -fun no_thycontext guh = (guh2theID guh; false)
14.284 - handle ERROR _ => true;
14.285 -
14.286 -(* get the substitution of bound variables for matchTheory:
14.287 - # lookup the thm|rls' in the script
14.288 - # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst
14.289 - # instantiate this subs with the istates env to [(bdv, x),..]
14.290 - # otherwise []
14.291 - WN060617 hack assuming that all scripts use only one bound variable
14.292 - and use 'v_' as the formal argument for this bound variable*)
14.293 -fun subs_from (Istate.Pstate ({env, ...})) _ guh =
14.294 - let
14.295 - val (_, _, thyID, sect, xstr) = case guh2theID guh of
14.296 - theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
14.297 - | _ => error "subs_from: uncovered case"
14.298 - in
14.299 - case sect of
14.300 - "Theorems" =>
14.301 - let val thm = Global_Theory.get_thm (ThyC.get_theory thyID) xstr
14.302 - in
14.303 - if Auto_Prog.contains_bdv thm
14.304 - then
14.305 - let
14.306 - val formal_arg = TermC.str2term "v_"
14.307 - val value = subst_atomic env formal_arg
14.308 - in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
14.309 - else []
14.310 - end
14.311 - | "Rulesets" =>
14.312 - let
14.313 - val rules = (Rule_Set.get_rules o assoc_rls) xstr
14.314 - in
14.315 - if Auto_Prog.contain_bdv rules
14.316 - then
14.317 - let
14.318 - val formal_arg = TermC.str2term "v_"
14.319 - val value = subst_atomic env formal_arg
14.320 - in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
14.321 - else []
14.322 - end
14.323 - | str => error ("subs_from: uncovered case with " ^ str)
14.324 - end
14.325 - | subs_from _ _ guh = error ("subs_from: uncovered case with " ^ guh)
14.326 -
14.327 -(**)end(**)
15.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Tue Apr 28 16:51:36 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Tue Apr 28 17:50:18 2020 +0200
15.3 @@ -77,7 +77,7 @@
15.4 collect_part "IsacKnowledge" knowledge_parent knowthys' @
15.5 (map (collect_isab "Isabelle") rlsthmsNOTisac) @
15.6 collect_part "IsacScripts" proglang_parent progthys'
15.7 -: (Thy_Html.theID * Thy_Html.thydata) list
15.8 +: (Thy_Write.theID * Thy_Write.thydata) list
15.9 \<close>
15.10 ML \<open>
15.11 map Context.theory_name knowthys'
16.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue Apr 28 16:51:36 2020 +0200
16.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 28 17:50:18 2020 +0200
16.3 @@ -28,7 +28,7 @@
16.4 val get_pbt : Problem.id -> Problem.T
16.5 val get_met : Method.id -> Method.T (* for generate.sml *)
16.6 val get_met' : theory -> Method.id -> Method.T (* for pbl-met-hierarchy.sml *)
16.7 - val get_the : Thy_Html.theID -> Thy_Html.thydata (* for inform.sml *)
16.8 + val get_the : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
16.9
16.10 type pblRD = string list (* for pbl-met-hierarchy.sml *)
16.11 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
17.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 16:51:36 2020 +0200
17.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
17.3 @@ -131,7 +131,7 @@
17.4 (pa, po', (ids@[id]), n);
17.5 strs2str id = "[\"e_pblID\"]"; (*true*)
17.6 pos2str pos = "[1]"; (*true*)
17.7 -path ^ guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
17.8 +path ^ Thy_Present.guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
17.9 "~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
17.10 (id, pbl);
17.11 "~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id);
18.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 16:51:36 2020 +0200
18.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 17:50:18 2020 +0200
18.3 @@ -74,7 +74,7 @@
18.4 thydata2xml (theID, thydata) (*reported Exception- Match in question*);
18.5 val i = 2;
18.6 ;
18.7 -val (theID: Thy_Html.theID, Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
18.8 +val (theID: Thy_Write.theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
18.9 rls2xml i thy_rls (*reported Exception- Match in question*);
18.10 ;
18.11 val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);
18.12 @@ -90,7 +90,7 @@
18.13 "----------- search for data error in thes2file ------------------";
18.14 "----------- search for data error in thes2file ------------------";
18.15 val TESTdump = Unsynchronized.ref
18.16 - ("path": filepath, ["ids"]: Thy_Html.theID, []: pos, thydata2file, Store.Node ("xxx", [], []): Thy_Html.thydata Store.node);
18.17 + ("path": filepath, ["ids"]: Thy_Write.theID, []: pos, thydata2file, Store.Node ("xxx", [], []): Thy_Write.thydata Store.node);
18.18
18.19 fun TESTthenode (pa:filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids =
18.20 let val po' = lev_on po
18.21 @@ -122,10 +122,10 @@
18.22 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
18.23 val (pa, ids, po', wfn, (Store.Node (id, [n], ns))) = ! TESTdump;
18.24 ;
18.25 -"~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:Thy_Html.theID), thydata) =
18.26 +"~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:Thy_Write.theID), thydata) =
18.27 (pa, po', (ids@[id]), n);
18.28 -"~~~~~ fun thydata2xml, args:"; val (theID, Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
18.29 - (theID:Thy_Html.theID, thydata);
18.30 +"~~~~~ fun thydata2xml, args:"; val (theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
18.31 + (theID:Thy_Write.theID, thydata);
18.32 "~~~~~ fun rls2xml, args:"; val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);
18.33 "~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
18.34 srls, calc, errpatts, rules, scr})) = (j, (thyID, "Rule_Set.Sequence", data));
18.35 @@ -147,12 +147,12 @@
18.36 "----------- fun ThmC_Def.make_thm ------------------------------------";
18.37 "----------- fun ThmC_Def.make_thm ------------------------------------";
18.38 "----------- fun ThmC_Def.make_thm ------------------------------------";
18.39 -"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Html.authors)) =
18.40 +"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Write.authors)) =
18.41 (@{theory "Biegelinie"}, "IsacKnowledge",
18.42 ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
18.43 ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
18.44 - val guh = Thy_Html.thm2guh (part, Context.theory_name thy) thmID
18.45 - val theID = guh2theID guh;
18.46 + val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
18.47 + val theID = Thy_Present.guh2theID guh;
18.48 if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
18.49 theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
18.50 then () else error "store_thm: guh | theID changed";
18.51 @@ -160,8 +160,8 @@
18.52 "----------- correct theIDs for Rule_Set.empty ----------------------------";
18.53 "----------- correct theIDs for Rule_Set.empty ----------------------------";
18.54 "----------- correct theIDs for Rule_Set.empty ----------------------------";
18.55 -if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()
18.56 -else error "thy_containing_rls Rule_Set.empty changed";
18.57 +if Thy_Read.thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()
18.58 +else error "Thy_Read.thy_containing_rls Rule_Set.empty changed";
18.59 show_thes ();
18.60 (*shows different assignment for "empty"...
18.61 :
18.62 @@ -199,7 +199,7 @@
18.63 ;
18.64 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
18.65 val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
18.66 - |> map (thms_of_rls o #2 o #2)
18.67 + |> map (Thy_Present.thms_of_rls o #2 o #2)
18.68 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
18.69 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
18.70 |> flat
18.71 @@ -298,39 +298,39 @@
18.72 ;
18.73 case thydata_list of (*length = 8*)
18.74 [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
18.75 - Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
18.76 + Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
18.77 mathauthors = ["isac-team"], thm = _}),
18.78 (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
18.79 - Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
18.80 + Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
18.81 mathauthors = ["isac-team"], thm = _}),
18.82 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
18.83 - Thy_Html.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
18.84 + Thy_Write.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
18.85 mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
18.86 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
18.87 - Thy_Html.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
18.88 + Thy_Write.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
18.89 mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
18.90 (["Isabelle", "HOL", "Theorems", "refl"],
18.91 - Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
18.92 + Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
18.93 mathauthors = ["Isabelle team, TU Munich"], thm = _}),
18.94 - (["Isabelle", "Fun", "Theorems", "o_def"], Thy_Html.Hthm {coursedesign = [], fillpats = [],
18.95 + (["Isabelle", "Fun", "Theorems", "o_def"], Thy_Write.Hthm {coursedesign = [], fillpats = [],
18.96 guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
18.97 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
18.98 - Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
18.99 + Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
18.100 mathauthors = ["isac-team"], thm = _}),
18.101 (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
18.102 - Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
18.103 + Thy_Write.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
18.104 mathauthors = ["isac-team"], thm = _})] => ()
18.105 | _ => error "collect thydata from Test_Build_Thydata changed";
18.106 ;
18.107 (* we store locally on MINIthehier instead on Know_Store, see Know_Store: *)
18.108 - fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata;
18.109 + fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata;
18.110 val thes = map (fn (a, b) => (b, a)) thydata_list
18.111 val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
18.112
18.113 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
18.114 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
18.115 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
18.116 -fun MINIget_the (theID : Thy_Html.theID) = Store.get MINIthehier theID theID (*see ptyps.sml*)
18.117 +fun MINIget_the (theID : Thy_Write.theID) = Store.get MINIthehier theID theID (*see ptyps.sml*)
18.118 fun MINIthy_hierarchy2file (path:filepath) =
18.119 str2file (path ^ "thy_hierarchy.xml")
18.120 ("<NODE>\n" ^
18.121 @@ -345,7 +345,7 @@
18.122 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
18.123 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
18.124 case MINIget_the ["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"] of
18.125 - Thy_Html.Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()
18.126 + Thy_Write.Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()
18.127 | _ => error "MINIget_the thm111 changed"
18.128 ;
18.129 val path = "/tmp/"
18.130 @@ -369,12 +369,12 @@
18.131 (* we take (theID, thydata) from thydata_list ABOVE: *)
18.132 case hd thydata_list of
18.133 (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
18.134 - Thy_Html.Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
18.135 + Thy_Write.Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
18.136 | _ => error "a change inhibits successful continuation of this test";
18.137 val (theID, thydata) = hd thydata_list;
18.138 -"~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : Thy_Html.theID), thydata) =
18.139 +"~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : Thy_Write.theID), thydata) =
18.140 (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
18.141 -"~~~~~ fun thydata2xml, args:"; val ((theID, Thy_Html.Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
18.142 +"~~~~~ fun thydata2xml, args:"; val ((theID, Thy_Write.Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
18.143 ((theID, thydata));
18.144 "~~~~~ to str2file return val:"; val (xml) =
18.145 "<THEOREMDATA>\n" ^
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Tue Apr 28 17:50:18 2020 +0200
19.3 @@ -0,0 +1,361 @@
19.4 +(* Title: test for rewtools.sml
19.5 + authors: Walther Neuper 2000, 2006
19.6 +
19.7 +theory Test_Some imports Isac.Build_Thydata begin
19.8 +ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
19.9 +ML {* KEStore_Elems.set_ref_thy @{theory};
19.10 + fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
19.11 +ML_file "Interpret/rewtools.sml"
19.12 +*)
19.13 +
19.14 +"--------------------------------------------------------";
19.15 +"--------------------------------------------------------";
19.16 +"table of contents --------------------------------------";
19.17 +"--------------------------------------------------------";
19.18 +"----------- fun thy_containing_rls ---------------------";
19.19 +"----------- apply thy_containing_rls -------------------";
19.20 +"----------- fun thy_containing_cal ---------------------";
19.21 +"----------- initContext Thy_ Integration-demo ----------";
19.22 +"----------- initContext..Thy_, fun context_thm ---------";
19.23 +"----------- initContext..Thy_, fun context_rls ---------";
19.24 +"----------- checkContext..Thy_, fun context_thy --------";
19.25 +"----------- checkContext..Thy_, fun context_rls --------";
19.26 +"----------- checkContext..Thy_ on last formula ---------";
19.27 +"----------- fun guh2theID ------------------------------";
19.28 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
19.29 +"--------------------------------------------------------";
19.30 +(*============ inhibit exn WN120321 ==============================================
19.31 +"--------------------------------------------------------";
19.32 +"----------- fun filter_appl_rews -----------------------";
19.33 +============ inhibit exn WN120321 ==============================================*)
19.34 +"----------- fun is_contained_in ------------------------";
19.35 +"--------------------------------------------------------";
19.36 +"--------------------------------------------------------";
19.37 +
19.38 +"----------- fun thy_containing_rls ---------------------";
19.39 +"----------- fun thy_containing_rls ---------------------";
19.40 +"----------- fun thy_containing_rls ---------------------";
19.41 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
19.42 +if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
19.43 +else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
19.44 +;
19.45 +"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
19.46 + val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
19.47 +val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';
19.48 +val SOME (thy'', _) = xxx;
19.49 +val SOME ("Poly", _) = xxx;
19.50 +if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
19.51 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
19.52 +if Thy_Read.partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
19.53 +;
19.54 +"~~~~~ fun partID', args:"; val (thy') = (thy');
19.55 +ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
19.56 +;
19.57 +"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
19.58 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
19.59 +Thy_Read.knowthys ()
19.60 +;
19.61 +"~~~~~ fun knowthys , args:"; val () = ();
19.62 + val allthys = filter_out (Library.member Context.eq_thy
19.63 + [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
19.64 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
19.65 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
19.66 +length allthys = 152; (*in Isabelle2015/Isac*)
19.67 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
19.68 +ThyC.get_theory "Complex_Main";*)
19.69 +Thy_Info.get_theory "Complex_Main";;
19.70 +
19.71 +"----------- apply thy_containing_rls -------------------";
19.72 +"----------- apply thy_containing_rls -------------------";
19.73 +"----------- apply thy_containing_rls -------------------";
19.74 +if Thy_Read.thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
19.75 +else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
19.76 +;
19.77 +if Thy_Read.thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()
19.78 +else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'")
19.79 +;
19.80 +if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
19.81 + ("IsacKnowledge", "Base_Tools") then ()
19.82 +else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
19.83 +
19.84 +"----------- fun thy_containing_cal ---------------------";
19.85 +"----------- fun thy_containing_cal ---------------------";
19.86 +"----------- fun thy_containing_cal ---------------------";
19.87 +(* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)
19.88 +if Thy_Read.thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")
19.89 +then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
19.90 +
19.91 +"----------- initContext Thy_ Integration-demo ----------";
19.92 +"----------- initContext Thy_ Integration-demo ----------";
19.93 +"----------- initContext Thy_ Integration-demo ----------";
19.94 +reset_states ();
19.95 +CalcTree
19.96 +[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
19.97 + ("Integrate",["integrate","function"],
19.98 + ["diff","integration"]))];
19.99 +Iterator 1;
19.100 +moveActiveRoot 1;
19.101 +autoCalculate 1 CompleteCalc;
19.102 +interSteps 1 ([1],Res);
19.103 +interSteps 1 ([1,1],Res);
19.104 +val ((pt,p),_) = get_calc 1; show_pt pt;
19.105 +if existpt' ([1,1,1], Frm) pt then ()
19.106 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
19.107 +initContext 1 Thy_ ([1,1,1], Frm);
19.108 +
19.109 +"----------- initContext..Thy_, fun context_thm ---------";
19.110 +"----------- initContext..Thy_, fun context_thm ---------";
19.111 +"----------- initContext..Thy_, fun context_thm ---------";
19.112 +reset_states (); (*start of calculation, return No.1*)
19.113 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.114 + ("Test", ["sqroot-test","univariate","equation","test"],
19.115 + ["Test","squ-equ-test-subpbl1"]))];
19.116 +Iterator 1; moveActiveRoot 1;
19.117 +autoCalculate 1 CompleteCalc;
19.118 +
19.119 +"----- no thy-context at result -----";
19.120 +val p = ([], Res);
19.121 +initContext 1 Thy_ p;
19.122 +val ((pt,_),_) = get_calc 1; show_pt pt; (* 11 lines with subpbl *)
19.123 +
19.124 +interSteps 1 ([2], Res);
19.125 +val ((pt,_),_) = get_calc 1; show_pt pt; (* added [2,1]..[2,6] *)
19.126 +interSteps 1 ([3,1], Res);
19.127 +val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *)
19.128 +
19.129 +val p = ([2,4], Res);
19.130 +"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
19.131 + Library.member op = [Pbl,Met] p_ = false;
19.132 + pos = ([],Res) = false;
19.133 + val cs as (ptp as (pt,_),_) = get_calc cI;
19.134 + exist_lev_on' pt pos = true;
19.135 + val pos' = lev_on' pt pos
19.136 + val tac = Thy_Present.get_tac_checked pt pos';
19.137 + is_rewtac tac = true;
19.138 +"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
19.139 + ((pt, pos), tac);
19.140 + val Appl (Rewrite' (thy', ord', erls, _, (thmID, thm), f, (res,asm))) = applicable_in pos pt tac
19.141 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
19.142 + val thm_deriv = Thm.get_name_hint thm;
19.143 +
19.144 +if Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
19.145 + = "thy_isac_Test-thm-radd_left_commute" then ()
19.146 +else error "context_thy mini-subpbl ([2,4], Res) changed";
19.147 +(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
19.148 +-rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*)
19.149 +
19.150 +
19.151 +val p = ([3,1,1], Frm);
19.152 +"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
19.153 + Library.member op = [Pbl,Met] p_ = false;
19.154 + pos = ([],Res) = false;
19.155 + val cs as (ptp as (pt,_),_) = get_calc cI;
19.156 + exist_lev_on' pt pos = true;
19.157 + val pos' = lev_on' pt pos
19.158 + val tac = Thy_Present.get_tac_checked pt pos';
19.159 + is_rewtac tac = true;
19.160 +"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=
19.161 + ((pt, pos), tac);
19.162 +val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
19.163 + applicable_in pos pt tac
19.164 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
19.165 + val thm_deriv = Thm.get_name_hint thm;
19.166 +if Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
19.167 + "thy_isac_Test-thm-risolate_bdv_add" then ()
19.168 +else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
19.169 +(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
19.170 +-rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*)
19.171 +
19.172 +
19.173 +val p = ([2,5], Res);
19.174 +"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
19.175 + Library.member op = [Pbl,Met] p_ = false;
19.176 + pos = ([],Res) = false;
19.177 + val cs as (ptp as (pt,_),_) = get_calc cI;
19.178 + exist_lev_on' pt pos = true;
19.179 + val pos' = lev_on' pt pos
19.180 + val tac = Thy_Present.get_tac_checked pt pos';
19.181 +if is_rewtac tac = false then ()
19.182 +else error "initContext: context_thy .. Calculate PLUS .. TO BE IMPLEMENTED"
19.183 +
19.184 +"----------- initContext..Thy_, fun context_rls ---------";
19.185 +"----------- initContext..Thy_, fun context_rls ---------";
19.186 +"----------- initContext..Thy_, fun context_rls ---------";
19.187 +(*using pt from above*)
19.188 +val p = ([1], Res);
19.189 +val tac = Rewrite_Set "Test_simplify";
19.190 +initContext 1 Thy_ p;
19.191 +(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
19.192 + --- in initContext..Thy_ ---*)
19.193 +val Thy_Present.ContRls {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
19.194 +if rls = "thy_isac_Test-rls-Test_simplify"
19.195 + andalso UnparseC.term result = "-1 + x = 0" then ()
19.196 +else error "rewtools.sml initContext..Th_ thy_isac_Test-rls-Test_simplify";
19.197 +
19.198 +val p = ([3,1], Frm);
19.199 +val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
19.200 +initContext 1 Thy_ p;
19.201 +(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
19.202 + --- in initContext..Thy_ ---*)
19.203 +val Thy_Present.ContRlsInst {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
19.204 +if rls = "thy_isac_Test-rls-isolate_bdv"
19.205 + andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
19.206 +else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
19.207 +
19.208 +"----------- checkContext..Thy_, fun context_thy --------";
19.209 +"----------- checkContext..Thy_, fun context_thy --------";
19.210 +"----------- checkContext..Thy_, fun context_thy --------";
19.211 +(*using pt from above*)
19.212 +val p = ([2,4], Res);
19.213 +val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
19.214 +checkContext 1 p "thy_Test-thm-radd_left_commute";
19.215 +(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
19.216 + --- in checkContext..Thy_ ---*)
19.217 +val Thy_Present.ContThm {thm,result,...} = Thy_Present.context_thy (pt,p) tac;
19.218 +if thm = "thy_isac_Test-thm-radd_left_commute"
19.219 + andalso UnparseC.term result = "-2 + (1 + x) = 0" then ()
19.220 +else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
19.221 +
19.222 +val p = ([3,1,1], Frm);
19.223 +val tac = Rewrite_Inst (["(''bdv'',x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
19.224 +checkContext 1 p "thy_Test-thm-risolate_bdv_add";
19.225 +(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
19.226 + --- in checkContext..Thy_ ---*)
19.227 +val Thy_Present.ContThmInst {thm,result,...} = Thy_Present.context_thy (pt,p) tac;
19.228 +if thm = "thy_isac_Test-thm-risolate_bdv_add"
19.229 + andalso UnparseC.term result = "x = 0 + - 1 * -1" then ()
19.230 +else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
19.231 +
19.232 +val p = ([2,5], Res);
19.233 +val tac = Calculate "plus";
19.234 +(*checkContext..Thy_ 1 ([2,5], Res);*)
19.235 +(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
19.236 +checkContext 1 p ;
19.237 +(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
19.238 + --- in checkContext..Thy_ ---*)
19.239 +
19.240 +"----------- checkContext..Thy_, fun context_rls --------";
19.241 +"----------- checkContext..Thy_, fun context_rls --------";
19.242 +"----------- checkContext..Thy_, fun context_rls --------";
19.243 +(*using pt from above*)
19.244 +val p = ([1], Res);
19.245 +val tac = Rewrite_Set "Test_simplify";
19.246 +checkContext 1 p "thy_isac_Test-rls-Test_simplify";
19.247 +(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
19.248 + --- in checkContext..Thy_ ---*)
19.249 +val Thy_Present.ContRls {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
19.250 +if rls = "thy_isac_Test-rls-Test_simplify"
19.251 + andalso UnparseC.term result = "-1 + x = 0" then ()
19.252 +else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
19.253 +
19.254 +val p = ([3,1], Frm);
19.255 +val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
19.256 +checkContext 1 p "thy_Test-rls-isolate_bdv";
19.257 +val Thy_Present.ContRlsInst {rls,result,...} = Thy_Present.context_thy (pt,p) tac;
19.258 +if rls = "thy_isac_Test-rls-isolate_bdv"
19.259 + andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
19.260 +else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
19.261 +
19.262 +"----------- checkContext..Thy_ on last formula ---------";
19.263 +"----------- checkContext..Thy_ on last formula ---------";
19.264 +"----------- checkContext..Thy_ on last formula ---------";
19.265 +reset_states (); (*start of calculation, return No.1*)
19.266 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.267 + ("Test", ["sqroot-test","univariate","equation","test"],
19.268 + ["Test","squ-equ-test-subpbl1"]))];
19.269 +Iterator 1; moveActiveRoot 1;
19.270 +
19.271 +autoCalculate 1 CompleteCalcHead;
19.272 +autoCalculate 1 (Steps 1);
19.273 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
19.274 +initContext 1 Thy_ ([1], Frm);
19.275 +checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
19.276 +
19.277 +autoCalculate 1 (Steps 1);
19.278 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
19.279 +initContext 1 Thy_ ([1], Res);
19.280 +checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
19.281 +
19.282 +"----------- fun guh2theID ------------------------------";
19.283 +"----------- fun guh2theID ------------------------------";
19.284 +"----------- fun guh2theID ------------------------------";
19.285 +val guh = "thy_scri_ListG-thm-zip_Nil";
19.286 +(*default_print_depth 3; 999*)
19.287 +take_fromto 1 4 (Symbol.explode guh);
19.288 +take_fromto 5 9 (Symbol.explode guh);
19.289 +val rest = takerest (9,(Symbol.explode guh));
19.290 +
19.291 +separate "-" rest;
19.292 +space_implode "-" rest;
19.293 +commas rest;
19.294 +
19.295 +val delim = "-";
19.296 +val thyID = takewhile [] (not o (curry op= delim)) rest;
19.297 +val rest' = dropuntil (curry op= delim) rest;
19.298 +val setc = take_fromto 1 5 rest';
19.299 +val xstr = takerest (5, rest');
19.300 +
19.301 +if Thy_Present.guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
19.302 +else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
19.303 +
19.304 +
19.305 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
19.306 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
19.307 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
19.308 +"----- initContext -----";
19.309 +reset_states ();
19.310 +CalcTree
19.311 + [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
19.312 + ("Test",
19.313 + ["LINEAR","univariate","equation","test"],
19.314 + ["Test","solve_linear"]))];
19.315 +Iterator 1; moveActiveRoot 1;
19.316 +autoCalculate 1 CompleteCalcHead;
19.317 +
19.318 +autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
19.319 +if is_curr_endof_calc pt ([1],Frm) then ()
19.320 +else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
19.321 +
19.322 +autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
19.323 +
19.324 +if not (is_curr_endof_calc pt ([1],Frm)) then ()
19.325 +else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
19.326 +if is_curr_endof_calc pt ([1],Res) then ()
19.327 +else error "rewtools.sml is_curr_endof_calc ([1],Res)";
19.328 +
19.329 +initContext 1 Thy_ ([1],Res);
19.330 +
19.331 +"----- checkContext -----";
19.332 +reset_states ();
19.333 +CalcTree
19.334 + [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
19.335 + ("Test",
19.336 + ["LINEAR","univariate","equation","test"],
19.337 + ["Test","solve_linear"]))];
19.338 +Iterator 1; moveActiveRoot 1;
19.339 +autoCalculate 1 CompleteCalc;
19.340 +interSteps 1 ([1],Res);
19.341 +
19.342 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
19.343 +checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
19.344 +
19.345 +interSteps 1 ([2],Res);
19.346 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
19.347 +
19.348 +checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
19.349 +checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
19.350 +
19.351 +"----------- fun is_contained_in ------------------------";
19.352 +"----------- fun is_contained_in ------------------------";
19.353 +"----------- fun is_contained_in ------------------------";
19.354 +val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus});
19.355 +if Rule_Set.contains r1 Test_simplify then ()
19.356 +else error "rewtools.sml Rule_Set.contains Thm";
19.357 +
19.358 +val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_");
19.359 +if Rule_Set.contains r1 Test_simplify then ()
19.360 +else error "rewtools.sml Rule_Set.contains Eval";
19.361 +
19.362 +val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_");
19.363 +if not (Rule_Set.contains r1 Test_simplify) then ()
19.364 +else error "rewtools.sml Rule_Set.contains Eval";
20.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Apr 28 16:51:36 2020 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,361 +0,0 @@
20.4 -(* Title: test for rewtools.sml
20.5 - authors: Walther Neuper 2000, 2006
20.6 -
20.7 -theory Test_Some imports Isac.Build_Thydata begin
20.8 -ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
20.9 -ML {* KEStore_Elems.set_ref_thy @{theory};
20.10 - fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
20.11 -ML_file "Interpret/rewtools.sml"
20.12 -*)
20.13 -
20.14 -"--------------------------------------------------------";
20.15 -"--------------------------------------------------------";
20.16 -"table of contents --------------------------------------";
20.17 -"--------------------------------------------------------";
20.18 -"----------- fun thy_containing_rls ---------------------";
20.19 -"----------- apply thy_containing_rls -------------------";
20.20 -"----------- fun thy_containing_cal ---------------------";
20.21 -"----------- initContext Thy_ Integration-demo ----------";
20.22 -"----------- initContext..Thy_, fun context_thm ---------";
20.23 -"----------- initContext..Thy_, fun context_rls ---------";
20.24 -"----------- checkContext..Thy_, fun context_thy --------";
20.25 -"----------- checkContext..Thy_, fun context_rls --------";
20.26 -"----------- checkContext..Thy_ on last formula ---------";
20.27 -"----------- fun guh2theID ------------------------------";
20.28 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
20.29 -"--------------------------------------------------------";
20.30 -(*============ inhibit exn WN120321 ==============================================
20.31 -"--------------------------------------------------------";
20.32 -"----------- fun filter_appl_rews -----------------------";
20.33 -============ inhibit exn WN120321 ==============================================*)
20.34 -"----------- fun is_contained_in ------------------------";
20.35 -"--------------------------------------------------------";
20.36 -"--------------------------------------------------------";
20.37 -
20.38 -"----------- fun thy_containing_rls ---------------------";
20.39 -"----------- fun thy_containing_rls ---------------------";
20.40 -"----------- fun thy_containing_rls ---------------------";
20.41 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
20.42 -if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
20.43 -else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
20.44 -;
20.45 -"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
20.46 - val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
20.47 -val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';
20.48 -val SOME (thy'', _) = xxx;
20.49 -val SOME ("Poly", _) = xxx;
20.50 -if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
20.51 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
20.52 -if Thy_Read.partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
20.53 -;
20.54 -"~~~~~ fun partID', args:"; val (thy') = (thy');
20.55 -ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
20.56 -;
20.57 -"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
20.58 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
20.59 -Thy_Read.knowthys ()
20.60 -;
20.61 -"~~~~~ fun knowthys , args:"; val () = ();
20.62 - val allthys = filter_out (Library.member Context.eq_thy
20.63 - [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
20.64 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
20.65 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
20.66 -length allthys = 152; (*in Isabelle2015/Isac*)
20.67 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
20.68 -ThyC.get_theory "Complex_Main";*)
20.69 -Thy_Info.get_theory "Complex_Main";;
20.70 -
20.71 -"----------- apply thy_containing_rls -------------------";
20.72 -"----------- apply thy_containing_rls -------------------";
20.73 -"----------- apply thy_containing_rls -------------------";
20.74 -if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
20.75 -else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
20.76 -;
20.77 -if thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()
20.78 -else error ("thy_containing_rls changed for 'Biegelinie', 'e_rls'")
20.79 -;
20.80 -if thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
20.81 - ("IsacKnowledge", "Base_Tools") then ()
20.82 -else error ("thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
20.83 -
20.84 -"----------- fun thy_containing_cal ---------------------";
20.85 -"----------- fun thy_containing_cal ---------------------";
20.86 -"----------- fun thy_containing_cal ---------------------";
20.87 -(* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)
20.88 -if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")
20.89 -then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
20.90 -
20.91 -"----------- initContext Thy_ Integration-demo ----------";
20.92 -"----------- initContext Thy_ Integration-demo ----------";
20.93 -"----------- initContext Thy_ Integration-demo ----------";
20.94 -reset_states ();
20.95 -CalcTree
20.96 -[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
20.97 - ("Integrate",["integrate","function"],
20.98 - ["diff","integration"]))];
20.99 -Iterator 1;
20.100 -moveActiveRoot 1;
20.101 -autoCalculate 1 CompleteCalc;
20.102 -interSteps 1 ([1],Res);
20.103 -interSteps 1 ([1,1],Res);
20.104 -val ((pt,p),_) = get_calc 1; show_pt pt;
20.105 -if existpt' ([1,1,1], Frm) pt then ()
20.106 -else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
20.107 -initContext 1 Thy_ ([1,1,1], Frm);
20.108 -
20.109 -"----------- initContext..Thy_, fun context_thm ---------";
20.110 -"----------- initContext..Thy_, fun context_thm ---------";
20.111 -"----------- initContext..Thy_, fun context_thm ---------";
20.112 -reset_states (); (*start of calculation, return No.1*)
20.113 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
20.114 - ("Test", ["sqroot-test","univariate","equation","test"],
20.115 - ["Test","squ-equ-test-subpbl1"]))];
20.116 -Iterator 1; moveActiveRoot 1;
20.117 -autoCalculate 1 CompleteCalc;
20.118 -
20.119 -"----- no thy-context at result -----";
20.120 -val p = ([], Res);
20.121 -initContext 1 Thy_ p;
20.122 -val ((pt,_),_) = get_calc 1; show_pt pt; (* 11 lines with subpbl *)
20.123 -
20.124 -interSteps 1 ([2], Res);
20.125 -val ((pt,_),_) = get_calc 1; show_pt pt; (* added [2,1]..[2,6] *)
20.126 -interSteps 1 ([3,1], Res);
20.127 -val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *)
20.128 -
20.129 -val p = ([2,4], Res);
20.130 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
20.131 - Library.member op = [Pbl,Met] p_ = false;
20.132 - pos = ([],Res) = false;
20.133 - val cs as (ptp as (pt,_),_) = get_calc cI;
20.134 - exist_lev_on' pt pos = true;
20.135 - val pos' = lev_on' pt pos
20.136 - val tac = get_tac_checked pt pos';
20.137 - is_rewtac tac = true;
20.138 -"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
20.139 - ((pt, pos), tac);
20.140 - val Appl (Rewrite' (thy', ord', erls, _, (thmID,thm), f, (res,asm))) = applicable_in pos pt tac
20.141 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
20.142 - val thm_deriv = Thm.get_name_hint thm;
20.143 -
20.144 -if Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
20.145 - = "thy_isac_Test-thm-radd_left_commute" then ()
20.146 -else error "context_thy mini-subpbl ([2,4], Res) changed";
20.147 -(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
20.148 --rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*)
20.149 -
20.150 -
20.151 -val p = ([3,1,1], Frm);
20.152 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
20.153 - Library.member op = [Pbl,Met] p_ = false;
20.154 - pos = ([],Res) = false;
20.155 - val cs as (ptp as (pt,_),_) = get_calc cI;
20.156 - exist_lev_on' pt pos = true;
20.157 - val pos' = lev_on' pt pos
20.158 - val tac = get_tac_checked pt pos';
20.159 - is_rewtac tac = true;
20.160 -"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=
20.161 - ((pt, pos), tac);
20.162 -val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
20.163 - applicable_in pos pt tac
20.164 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
20.165 - val thm_deriv = Thm.get_name_hint thm;
20.166 -if Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
20.167 - "thy_isac_Test-thm-risolate_bdv_add" then ()
20.168 -else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
20.169 -(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
20.170 --rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*)
20.171 -
20.172 -
20.173 -val p = ([2,5], Res);
20.174 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
20.175 - Library.member op = [Pbl,Met] p_ = false;
20.176 - pos = ([],Res) = false;
20.177 - val cs as (ptp as (pt,_),_) = get_calc cI;
20.178 - exist_lev_on' pt pos = true;
20.179 - val pos' = lev_on' pt pos
20.180 - val tac = get_tac_checked pt pos';
20.181 -if is_rewtac tac = false then ()
20.182 -else error "initContext: context_thy .. Calculate PLUS .. TO BE IMPLEMENTED"
20.183 -
20.184 -"----------- initContext..Thy_, fun context_rls ---------";
20.185 -"----------- initContext..Thy_, fun context_rls ---------";
20.186 -"----------- initContext..Thy_, fun context_rls ---------";
20.187 -(*using pt from above*)
20.188 -val p = ([1], Res);
20.189 -val tac = Rewrite_Set "Test_simplify";
20.190 -initContext 1 Thy_ p;
20.191 -(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
20.192 - --- in initContext..Thy_ ---*)
20.193 -val ContRls {rls,result,...} = context_thy (pt,p) tac;
20.194 -if rls = "thy_isac_Test-rls-Test_simplify"
20.195 - andalso UnparseC.term result = "-1 + x = 0" then ()
20.196 -else error "rewtools.sml initContext..Th_ thy_isac_Test-rls-Test_simplify";
20.197 -
20.198 -val p = ([3,1], Frm);
20.199 -val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
20.200 -initContext 1 Thy_ p;
20.201 -(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
20.202 - --- in initContext..Thy_ ---*)
20.203 -val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
20.204 -if rls = "thy_isac_Test-rls-isolate_bdv"
20.205 - andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
20.206 -else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
20.207 -
20.208 -"----------- checkContext..Thy_, fun context_thy --------";
20.209 -"----------- checkContext..Thy_, fun context_thy --------";
20.210 -"----------- checkContext..Thy_, fun context_thy --------";
20.211 -(*using pt from above*)
20.212 -val p = ([2,4], Res);
20.213 -val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
20.214 -checkContext 1 p "thy_Test-thm-radd_left_commute";
20.215 -(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
20.216 - --- in checkContext..Thy_ ---*)
20.217 -val ContThm {thm,result,...} = context_thy (pt,p) tac;
20.218 -if thm = "thy_isac_Test-thm-radd_left_commute"
20.219 - andalso UnparseC.term result = "-2 + (1 + x) = 0" then ()
20.220 -else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
20.221 -
20.222 -val p = ([3,1,1], Frm);
20.223 -val tac = Rewrite_Inst (["(''bdv'',x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
20.224 -checkContext 1 p "thy_Test-thm-risolate_bdv_add";
20.225 -(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
20.226 - --- in checkContext..Thy_ ---*)
20.227 -val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
20.228 -if thm = "thy_isac_Test-thm-risolate_bdv_add"
20.229 - andalso UnparseC.term result = "x = 0 + - 1 * -1" then ()
20.230 -else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
20.231 -
20.232 -val p = ([2,5], Res);
20.233 -val tac = Calculate "plus";
20.234 -(*checkContext..Thy_ 1 ([2,5], Res);*)
20.235 -(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
20.236 -checkContext 1 p ;
20.237 -(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
20.238 - --- in checkContext..Thy_ ---*)
20.239 -
20.240 -"----------- checkContext..Thy_, fun context_rls --------";
20.241 -"----------- checkContext..Thy_, fun context_rls --------";
20.242 -"----------- checkContext..Thy_, fun context_rls --------";
20.243 -(*using pt from above*)
20.244 -val p = ([1], Res);
20.245 -val tac = Rewrite_Set "Test_simplify";
20.246 -checkContext 1 p "thy_isac_Test-rls-Test_simplify";
20.247 -(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
20.248 - --- in checkContext..Thy_ ---*)
20.249 -val ContRls {rls,result,...} = context_thy (pt,p) tac;
20.250 -if rls = "thy_isac_Test-rls-Test_simplify"
20.251 - andalso UnparseC.term result = "-1 + x = 0" then ()
20.252 -else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
20.253 -
20.254 -val p = ([3,1], Frm);
20.255 -val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
20.256 -checkContext 1 p "thy_Test-rls-isolate_bdv";
20.257 -val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
20.258 -if rls = "thy_isac_Test-rls-isolate_bdv"
20.259 - andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
20.260 -else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
20.261 -
20.262 -"----------- checkContext..Thy_ on last formula ---------";
20.263 -"----------- checkContext..Thy_ on last formula ---------";
20.264 -"----------- checkContext..Thy_ on last formula ---------";
20.265 -reset_states (); (*start of calculation, return No.1*)
20.266 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
20.267 - ("Test", ["sqroot-test","univariate","equation","test"],
20.268 - ["Test","squ-equ-test-subpbl1"]))];
20.269 -Iterator 1; moveActiveRoot 1;
20.270 -
20.271 -autoCalculate 1 CompleteCalcHead;
20.272 -autoCalculate 1 (Steps 1);
20.273 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
20.274 -initContext 1 Thy_ ([1], Frm);
20.275 -checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
20.276 -
20.277 -autoCalculate 1 (Steps 1);
20.278 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
20.279 -initContext 1 Thy_ ([1], Res);
20.280 -checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
20.281 -
20.282 -"----------- fun guh2theID ------------------------------";
20.283 -"----------- fun guh2theID ------------------------------";
20.284 -"----------- fun guh2theID ------------------------------";
20.285 -val guh = "thy_scri_ListG-thm-zip_Nil";
20.286 -(*default_print_depth 3; 999*)
20.287 -take_fromto 1 4 (Symbol.explode guh);
20.288 -take_fromto 5 9 (Symbol.explode guh);
20.289 -val rest = takerest (9,(Symbol.explode guh));
20.290 -
20.291 -separate "-" rest;
20.292 -space_implode "-" rest;
20.293 -commas rest;
20.294 -
20.295 -val delim = "-";
20.296 -val thyID = takewhile [] (not o (curry op= delim)) rest;
20.297 -val rest' = dropuntil (curry op= delim) rest;
20.298 -val setc = take_fromto 1 5 rest';
20.299 -val xstr = takerest (5, rest');
20.300 -
20.301 -if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
20.302 -else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
20.303 -
20.304 -
20.305 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
20.306 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
20.307 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
20.308 -"----- initContext -----";
20.309 -reset_states ();
20.310 -CalcTree
20.311 - [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
20.312 - ("Test",
20.313 - ["LINEAR","univariate","equation","test"],
20.314 - ["Test","solve_linear"]))];
20.315 -Iterator 1; moveActiveRoot 1;
20.316 -autoCalculate 1 CompleteCalcHead;
20.317 -
20.318 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
20.319 -if is_curr_endof_calc pt ([1],Frm) then ()
20.320 -else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
20.321 -
20.322 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
20.323 -
20.324 -if not (is_curr_endof_calc pt ([1],Frm)) then ()
20.325 -else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
20.326 -if is_curr_endof_calc pt ([1],Res) then ()
20.327 -else error "rewtools.sml is_curr_endof_calc ([1],Res)";
20.328 -
20.329 -initContext 1 Thy_ ([1],Res);
20.330 -
20.331 -"----- checkContext -----";
20.332 -reset_states ();
20.333 -CalcTree
20.334 - [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
20.335 - ("Test",
20.336 - ["LINEAR","univariate","equation","test"],
20.337 - ["Test","solve_linear"]))];
20.338 -Iterator 1; moveActiveRoot 1;
20.339 -autoCalculate 1 CompleteCalc;
20.340 -interSteps 1 ([1],Res);
20.341 -
20.342 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
20.343 -checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
20.344 -
20.345 -interSteps 1 ([2],Res);
20.346 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
20.347 -
20.348 -checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
20.349 -checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
20.350 -
20.351 -"----------- fun is_contained_in ------------------------";
20.352 -"----------- fun is_contained_in ------------------------";
20.353 -"----------- fun is_contained_in ------------------------";
20.354 -val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus});
20.355 -if Rule_Set.contains r1 Test_simplify then ()
20.356 -else error "rewtools.sml Rule_Set.contains Thm";
20.357 -
20.358 -val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_");
20.359 -if Rule_Set.contains r1 Test_simplify then ()
20.360 -else error "rewtools.sml Rule_Set.contains Eval";
20.361 -
20.362 -val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_");
20.363 -if not (Rule_Set.contains r1 Test_simplify) then ()
20.364 -else error "rewtools.sml Rule_Set.contains Eval";
21.1 --- a/test/Tools/isac/Test_Isac.thy Tue Apr 28 16:51:36 2020 +0200
21.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Apr 28 17:50:18 2020 +0200
21.3 @@ -191,7 +191,7 @@
21.4 (*called by Know_Store*)
21.5 ML_file "BaseDefinitions/calcelems.sml"
21.6 ML_file "BaseDefinitions/termC.sml"
21.7 - ML_file substitution.sml
21.8 + ML_file "BaseDefinitions/substitution.sml"
21.9 ML_file "BaseDefinitions/contextC.sml"
21.10 ML_file "BaseDefinitions/environment.sml"
21.11 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
22.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Apr 28 16:51:36 2020 +0200
22.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Apr 28 17:50:18 2020 +0200
22.3 @@ -100,7 +100,6 @@
22.4 open Error_Pattern;
22.5 open Error_Pattern_Def;
22.6 open In_Chead;
22.7 - open Rtools;
22.8 open Chead; pt_extract;
22.9 open Generate; (* NONE *)
22.10 open Ctree; append_problem;
22.11 @@ -250,7 +249,6 @@
22.12
22.13 ML_file "Interpret/istate.sml"
22.14 ML_file "Interpret/sub-problem.sml"
22.15 - ML_file "Interpret/rewtools.sml"
22.16 ML_file "Interpret/error-pattern.sml"
22.17 ML_file "Interpret/li-tool.sml"
22.18 ML_file "Interpret/lucas-interpreter.sml"
22.19 @@ -263,6 +261,7 @@
22.20 ML_file "MathEngine/messages.sml"
22.21 ML_file "MathEngine/states.sml"
22.22
22.23 + ML_file "BridgeLibisabelle/thy-present.sml"
22.24 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
22.25 ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
22.26 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
23.1 --- a/test/Tools/isac/Test_Some.thy Tue Apr 28 16:51:36 2020 +0200
23.2 +++ b/test/Tools/isac/Test_Some.thy Tue Apr 28 17:50:18 2020 +0200
23.3 @@ -20,7 +20,6 @@
23.4 open Error_Pattern;
23.5 open Error_Pattern_Def;
23.6 open In_Chead;
23.7 - open Rtools;
23.8 open Chead; pt_extract;
23.9 open Generate; (* NONE *)
23.10 open Ctree; append_problem;
23.11 @@ -96,418 +95,6 @@
23.12 section \<open>===================================================================================\<close>
23.13 ML \<open>
23.14 \<close> ML \<open>
23.15 -(* Title: test for rewtools.sml
23.16 - authors: Walther Neuper 2000, 2006
23.17 -
23.18 -theory Test_Some imports Isac.Build_Thydata begin
23.19 -ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
23.20 -ML {* KEStore_Elems.set_ref_thy @{theory};
23.21 - fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
23.22 -ML_file "Interpret/rewtools.sml"
23.23 -*)
23.24 -
23.25 -"--------------------------------------------------------";
23.26 -"--------------------------------------------------------";
23.27 -"table of contents --------------------------------------";
23.28 -"--------------------------------------------------------";
23.29 -"----------- fun thy_containing_rls ---------------------";
23.30 -"----------- apply thy_containing_rls -------------------";
23.31 -"----------- fun thy_containing_cal ---------------------";
23.32 -"----------- initContext Thy_ Integration-demo ----------";
23.33 -"----------- initContext..Thy_, fun context_thm ---------";
23.34 -"----------- initContext..Thy_, fun context_rls ---------";
23.35 -"----------- checkContext..Thy_, fun context_thy --------";
23.36 -"----------- checkContext..Thy_, fun context_rls --------";
23.37 -"----------- checkContext..Thy_ on last formula ---------";
23.38 -"----------- fun guh2theID ------------------------------";
23.39 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
23.40 -"--------------------------------------------------------";
23.41 -(*============ inhibit exn WN120321 ==============================================
23.42 -"--------------------------------------------------------";
23.43 -"----------- fun filter_appl_rews -----------------------";
23.44 -============ inhibit exn WN120321 ==============================================*)
23.45 -"----------- fun is_contained_in ------------------------";
23.46 -"--------------------------------------------------------";
23.47 -"--------------------------------------------------------";
23.48 -
23.49 -\<close> ML \<open>
23.50 -"----------- fun thy_containing_rls ---------------------";
23.51 -"----------- fun thy_containing_rls ---------------------";
23.52 -"----------- fun thy_containing_rls ---------------------";
23.53 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
23.54 -if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
23.55 -else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
23.56 -;
23.57 -"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
23.58 - val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
23.59 -val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';
23.60 -val SOME (thy'', _) = xxx;
23.61 -val SOME ("Poly", _) = xxx;
23.62 -if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
23.63 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
23.64 -if partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
23.65 -;
23.66 -"~~~~~ fun partID', args:"; val (thy') = (thy');
23.67 -ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
23.68 -;
23.69 -"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
23.70 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
23.71 -knowthys ()
23.72 -;
23.73 -"~~~~~ fun knowthys , args:"; val () = ();
23.74 - val allthys = filter_out (Library.member Context.eq_thy
23.75 - [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
23.76 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
23.77 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
23.78 -length allthys = 152; (*in Isabelle2015/Isac*)
23.79 -(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
23.80 -ThyC.get_theory "Complex_Main";*)
23.81 -Thy_Info.get_theory "Complex_Main";;
23.82 -
23.83 -\<close> ML \<open>
23.84 -"----------- apply thy_containing_rls -------------------";
23.85 -"----------- apply thy_containing_rls -------------------";
23.86 -"----------- apply thy_containing_rls -------------------";
23.87 -if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
23.88 -else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
23.89 -;
23.90 -if thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()
23.91 -else error ("thy_containing_rls changed for 'Biegelinie', 'e_rls'")
23.92 -;
23.93 -if thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
23.94 - ("IsacKnowledge", "Base_Tools") then ()
23.95 -else error ("thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
23.96 -
23.97 -\<close> ML \<open>
23.98 -"----------- fun thy_containing_cal ---------------------";
23.99 -"----------- fun thy_containing_cal ---------------------";
23.100 -"----------- fun thy_containing_cal ---------------------";
23.101 -(* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)
23.102 -if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")
23.103 -then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
23.104 -
23.105 -\<close> ML \<open>
23.106 -"----------- initContext Thy_ Integration-demo ----------";
23.107 -"----------- initContext Thy_ Integration-demo ----------";
23.108 -"----------- initContext Thy_ Integration-demo ----------";
23.109 -reset_states ();
23.110 -CalcTree
23.111 -[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
23.112 - ("Integrate",["integrate","function"],
23.113 - ["diff","integration"]))];
23.114 -Iterator 1;
23.115 -moveActiveRoot 1;
23.116 -autoCalculate 1 CompleteCalc;
23.117 -interSteps 1 ([1],Res);
23.118 -interSteps 1 ([1,1],Res);
23.119 -val ((pt,p),_) = get_calc 1; show_pt pt;
23.120 -if existpt' ([1,1,1], Frm) pt then ()
23.121 -else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
23.122 -initContext 1 Thy_ ([1,1,1], Frm);
23.123 -
23.124 -\<close> ML \<open>
23.125 -"----------- initContext..Thy_, fun context_thm ---------";
23.126 -"----------- initContext..Thy_, fun context_thm ---------";
23.127 -"----------- initContext..Thy_, fun context_thm ---------";
23.128 -reset_states (); (*start of calculation, return No.1*)
23.129 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
23.130 - ("Test", ["sqroot-test","univariate","equation","test"],
23.131 - ["Test","squ-equ-test-subpbl1"]))];
23.132 -Iterator 1; moveActiveRoot 1;
23.133 -autoCalculate 1 CompleteCalc;
23.134 -
23.135 -"----- no thy-context at result -----";
23.136 -val p = ([], Res);
23.137 -initContext 1 Thy_ p;
23.138 -val ((pt,_),_) = get_calc 1; show_pt pt; (* 11 lines with subpbl *)
23.139 -
23.140 -interSteps 1 ([2], Res);
23.141 -val ((pt,_),_) = get_calc 1; show_pt pt; (* added [2,1]..[2,6] *)
23.142 -interSteps 1 ([3,1], Res);
23.143 -val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *)
23.144 -
23.145 -val p = ([2,4], Res);
23.146 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
23.147 - Library.member op = [Pbl,Met] p_ = false;
23.148 - pos = ([],Res) = false;
23.149 - val cs as (ptp as (pt,_),_) = get_calc cI;
23.150 - exist_lev_on' pt pos = true;
23.151 - val pos' = lev_on' pt pos
23.152 - val tac = get_tac_checked pt pos';
23.153 - is_rewtac tac = true;
23.154 -"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
23.155 - ((pt, pos), tac);
23.156 - val Appl (Rewrite' (thy', ord', erls, _, (thmID,thm), f, (res,asm))) = applicable_in pos pt tac
23.157 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
23.158 - val thm_deriv = Thm.get_name_hint thm;
23.159 -
23.160 -if Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
23.161 - = "thy_isac_Test-thm-radd_left_commute" then ()
23.162 -else error "context_thy mini-subpbl ([2,4], Res) changed";
23.163 -(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
23.164 --rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*)
23.165 -
23.166 -
23.167 -val p = ([3,1,1], Frm);
23.168 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
23.169 - Library.member op = [Pbl,Met] p_ = false;
23.170 - pos = ([],Res) = false;
23.171 - val cs as (ptp as (pt,_),_) = get_calc cI;
23.172 - exist_lev_on' pt pos = true;
23.173 - val pos' = lev_on' pt pos
23.174 - val tac = get_tac_checked pt pos';
23.175 - is_rewtac tac = true;
23.176 -"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=
23.177 - ((pt, pos), tac);
23.178 -val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
23.179 - applicable_in pos pt tac
23.180 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
23.181 - val thm_deriv = Thm.get_name_hint thm;
23.182 -if Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
23.183 - "thy_isac_Test-thm-risolate_bdv_add" then ()
23.184 -else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
23.185 -(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
23.186 --rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*)
23.187 -
23.188 -
23.189 -val p = ([2,5], Res);
23.190 -"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
23.191 - Library.member op = [Pbl,Met] p_ = false;
23.192 - pos = ([],Res) = false;
23.193 - val cs as (ptp as (pt,_),_) = get_calc cI;
23.194 - exist_lev_on' pt pos = true;
23.195 - val pos' = lev_on' pt pos
23.196 - val tac = get_tac_checked pt pos';
23.197 -if is_rewtac tac = false then ()
23.198 -else error "initContext: context_thy .. Calculate PLUS .. TO BE IMPLEMENTED"
23.199 -
23.200 -\<close> ML \<open>
23.201 -"----------- initContext..Thy_, fun context_rls ---------";
23.202 -"----------- initContext..Thy_, fun context_rls ---------";
23.203 -"----------- initContext..Thy_, fun context_rls ---------";
23.204 -(*using pt from above*)
23.205 -val p = ([1], Res);
23.206 -val tac = Rewrite_Set "Test_simplify";
23.207 -initContext 1 Thy_ p;
23.208 -(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
23.209 - --- in initContext..Thy_ ---*)
23.210 -val ContRls {rls,result,...} = context_thy (pt,p) tac;
23.211 -if rls = "thy_isac_Test-rls-Test_simplify"
23.212 - andalso UnparseC.term result = "-1 + x = 0" then ()
23.213 -else error "rewtools.sml initContext..Th_ thy_isac_Test-rls-Test_simplify";
23.214 -
23.215 -val p = ([3,1], Frm);
23.216 -val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
23.217 -initContext 1 Thy_ p;
23.218 -(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
23.219 - --- in initContext..Thy_ ---*)
23.220 -val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
23.221 -if rls = "thy_isac_Test-rls-isolate_bdv"
23.222 - andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
23.223 -else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
23.224 -
23.225 -\<close> ML \<open>
23.226 -"----------- checkContext..Thy_, fun context_thy --------";
23.227 -"----------- checkContext..Thy_, fun context_thy --------";
23.228 -"----------- checkContext..Thy_, fun context_thy --------";
23.229 -(*using pt from above*)
23.230 -val p = ([2,4], Res);
23.231 -val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
23.232 -checkContext 1 p "thy_Test-thm-radd_left_commute";
23.233 -(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
23.234 - --- in checkContext..Thy_ ---*)
23.235 -val ContThm {thm,result,...} = context_thy (pt,p) tac;
23.236 -\<close> ML \<open>
23.237 -(*+*)val Rewrite ("radd_left_commute", _) = tac
23.238 -\<close> ML \<open>
23.239 -(*+*)thm = ("thy_isac_radd_left_commute-thm-radd_left_commute": ThmC.id);
23.240 -\<close> ML \<open>
23.241 -(*+*)UnparseC.term result = "-2 + (1 + x) = 0";
23.242 -\<close> ML \<open>
23.243 -"~~~~~ fun context_thy , args:"; val ((pt, pos as (p,p_)), (tac as Tactic.Rewrite thm'')) =
23.244 - ((pt,p), tac);
23.245 -\<close> ML \<open>
23.246 - val thm_deriv = ThmC.deriv_of_thm'' thm''
23.247 -\<close> ML \<open>
23.248 -"~~~~~ fun deriv_of_thm'' , args:"; val (thmID, _) = (thm'');
23.249 -\<close> ML \<open>
23.250 -(*+*)(thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint) = "Test.radd_left_commute";
23.251 -\<close> ML \<open>
23.252 - val id = thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint |> cut_id
23.253 -\<close> ML \<open>
23.254 - (*if*) thmID = id
23.255 -\<close> ML \<open>
23.256 -"~~~~~ from fun deriv_of_thm'' \<longrightarrow>fun context_thy, return:"; val (thm_deriv) = (id);
23.257 -\<close> ML \<open>
23.258 - val Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =
23.259 - (*case*) Applicable.applicable_in pos pt tac (*of*);
23.260 -\<close> ML \<open>
23.261 -(*+*)(ThmC.cut_id thm_deriv) = "radd_left_commute";
23.262 -\<close> ML \<open>
23.263 -(*+*)(thy_containing_thm thm_deriv) = ("IsacKnowledge", "radd_left_commute");
23.264 -\<close> ML \<open>
23.265 -Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
23.266 -\<close> ML \<open>
23.267 -\<close> ML \<open>
23.268 -\<close> ML \<open>
23.269 -\<close> ML \<open>
23.270 -\<close> ML \<open>
23.271 -\<close> ML \<open>
23.272 -thm = "thy_isac_radd_left_commute-thm-radd_left_commute";
23.273 -\<close> ML \<open>(*\------- end new code -------/*)
23.274 -if thm = "thy_isac_Test-thm-radd_left_commute"
23.275 - andalso UnparseC.term result = "-2 + (1 + x) = 0" then ()
23.276 -else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
23.277 -
23.278 -\<close> ML \<open>
23.279 -val p = ([3,1,1], Frm);
23.280 -val tac = Rewrite_Inst (["(''bdv'',x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
23.281 -checkContext 1 p "thy_Test-thm-risolate_bdv_add";
23.282 -(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
23.283 - --- in checkContext..Thy_ ---*)
23.284 -val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
23.285 -if thm = "thy_isac_Test-thm-risolate_bdv_add"
23.286 - andalso UnparseC.term result = "x = 0 + - 1 * -1" then ()
23.287 -else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
23.288 -
23.289 -val p = ([2,5], Res);
23.290 -val tac = Calculate "plus";
23.291 -(*checkContext..Thy_ 1 ([2,5], Res);*)
23.292 -(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
23.293 -checkContext 1 p ;
23.294 -(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
23.295 - --- in checkContext..Thy_ ---*)
23.296 -
23.297 -\<close> ML \<open>
23.298 -"----------- checkContext..Thy_, fun context_rls --------";
23.299 -"----------- checkContext..Thy_, fun context_rls --------";
23.300 -"----------- checkContext..Thy_, fun context_rls --------";
23.301 -(*using pt from above*)
23.302 -val p = ([1], Res);
23.303 -val tac = Rewrite_Set "Test_simplify";
23.304 -checkContext 1 p "thy_isac_Test-rls-Test_simplify";
23.305 -(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
23.306 - --- in checkContext..Thy_ ---*)
23.307 -val ContRls {rls,result,...} = context_thy (pt,p) tac;
23.308 -if rls = "thy_isac_Test-rls-Test_simplify"
23.309 - andalso UnparseC.term result = "-1 + x = 0" then ()
23.310 -else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
23.311 -
23.312 -val p = ([3,1], Frm);
23.313 -val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
23.314 -checkContext 1 p "thy_Test-rls-isolate_bdv";
23.315 -val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
23.316 -if rls = "thy_isac_Test-rls-isolate_bdv"
23.317 - andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
23.318 -else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
23.319 -
23.320 -\<close> ML \<open>
23.321 -"----------- checkContext..Thy_ on last formula ---------";
23.322 -"----------- checkContext..Thy_ on last formula ---------";
23.323 -"----------- checkContext..Thy_ on last formula ---------";
23.324 -reset_states (); (*start of calculation, return No.1*)
23.325 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
23.326 - ("Test", ["sqroot-test","univariate","equation","test"],
23.327 - ["Test","squ-equ-test-subpbl1"]))];
23.328 -Iterator 1; moveActiveRoot 1;
23.329 -
23.330 -autoCalculate 1 CompleteCalcHead;
23.331 -autoCalculate 1 (Steps 1);
23.332 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
23.333 -initContext 1 Thy_ ([1], Frm);
23.334 -checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
23.335 -
23.336 -autoCalculate 1 (Steps 1);
23.337 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
23.338 -initContext 1 Thy_ ([1], Res);
23.339 -checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
23.340 -
23.341 -\<close> ML \<open>
23.342 -"----------- fun guh2theID ------------------------------";
23.343 -"----------- fun guh2theID ------------------------------";
23.344 -"----------- fun guh2theID ------------------------------";
23.345 -val guh = "thy_scri_ListG-thm-zip_Nil";
23.346 -(*default_print_depth 3; 999*)
23.347 -take_fromto 1 4 (Symbol.explode guh);
23.348 -take_fromto 5 9 (Symbol.explode guh);
23.349 -val rest = takerest (9,(Symbol.explode guh));
23.350 -
23.351 -separate "-" rest;
23.352 -space_implode "-" rest;
23.353 -commas rest;
23.354 -
23.355 -val delim = "-";
23.356 -val thyID = takewhile [] (not o (curry op= delim)) rest;
23.357 -val rest' = dropuntil (curry op= delim) rest;
23.358 -val setc = take_fromto 1 5 rest';
23.359 -val xstr = takerest (5, rest');
23.360 -
23.361 -if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
23.362 -else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
23.363 -
23.364 -
23.365 -\<close> ML \<open>
23.366 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
23.367 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
23.368 -"----------- debugging on Tests/solve_linear_as_rootpbl -";
23.369 -"----- initContext -----";
23.370 -reset_states ();
23.371 -CalcTree
23.372 - [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
23.373 - ("Test",
23.374 - ["LINEAR","univariate","equation","test"],
23.375 - ["Test","solve_linear"]))];
23.376 -Iterator 1; moveActiveRoot 1;
23.377 -autoCalculate 1 CompleteCalcHead;
23.378 -
23.379 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
23.380 -if is_curr_endof_calc pt ([1],Frm) then ()
23.381 -else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
23.382 -
23.383 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
23.384 -
23.385 -if not (is_curr_endof_calc pt ([1],Frm)) then ()
23.386 -else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
23.387 -if is_curr_endof_calc pt ([1],Res) then ()
23.388 -else error "rewtools.sml is_curr_endof_calc ([1],Res)";
23.389 -
23.390 -initContext 1 Thy_ ([1],Res);
23.391 -
23.392 -"----- checkContext -----";
23.393 -reset_states ();
23.394 -CalcTree
23.395 - [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
23.396 - ("Test",
23.397 - ["LINEAR","univariate","equation","test"],
23.398 - ["Test","solve_linear"]))];
23.399 -Iterator 1; moveActiveRoot 1;
23.400 -autoCalculate 1 CompleteCalc;
23.401 -interSteps 1 ([1],Res);
23.402 -
23.403 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
23.404 -checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
23.405 -
23.406 -interSteps 1 ([2],Res);
23.407 -val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
23.408 -
23.409 -checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
23.410 -checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
23.411 -
23.412 -\<close> ML \<open>
23.413 -"----------- fun is_contained_in ------------------------";
23.414 -"----------- fun is_contained_in ------------------------";
23.415 -"----------- fun is_contained_in ------------------------";
23.416 -val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus});
23.417 -if Rule_Set.contains r1 Test_simplify then ()
23.418 -else error "rewtools.sml Rule_Set.contains Thm";
23.419 -
23.420 -val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_");
23.421 -if Rule_Set.contains r1 Test_simplify then ()
23.422 -else error "rewtools.sml Rule_Set.contains Eval";
23.423 -
23.424 -val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_");
23.425 -if not (Rule_Set.contains r1 Test_simplify) then ()
23.426 -else error "rewtools.sml Rule_Set.contains Eval";
23.427 \<close> ML \<open>
23.428 \<close>
23.429