1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Apr 20 15:54:19 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Apr 20 16:47:01 2020 +0200
1.3 @@ -33,10 +33,10 @@
1.4 ML_file "check-unique.sml"
1.5 ML_file "specification.sml"
1.6 ML_file "celem-4.sml" (*pat*)
1.7 -ML_file "celem-5.sml" (*ptyps*)
1.8 -ML_file "celem-6.sml" (*mets*)
1.9 -ML_file "celem-7.sml" (*cas_elem*)
1.10 -ML_file "celem-8.sml" (*thydata*)
1.11 +ML_file "problem-def.sml"
1.12 +ML_file "method-def.sml"
1.13 +ML_file "cas-def.sml"
1.14 +ML_file "thy-html.sml"
1.15
1.16 ML_file tracing.sml
1.17 ML \<open>
1.18 @@ -64,15 +64,15 @@
1.19 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
1.20 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
1.21 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
1.22 - val get_cas: theory -> Celem7.cas_elem list
1.23 - val add_cas: Celem7.cas_elem list -> theory -> theory
1.24 - val get_ptyps: theory -> Celem5.ptyps
1.25 - val add_pbts: (Celem5.pbt * Spec.pblID) list -> theory -> theory
1.26 - val get_mets: theory -> Celem6.mets
1.27 - val add_mets: (Celem6.met * Spec.metID) list -> theory -> theory
1.28 - val get_thes: theory -> (Celem8.thydata Store.ptyp) list
1.29 - val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.30 - val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.31 + val get_cas: theory -> CAS_Def.cas_elem list
1.32 + val add_cas: CAS_Def.cas_elem list -> theory -> theory
1.33 + val get_ptyps: theory -> Probl_Def.ptyps
1.34 + val add_pbts: (Probl_Def.pbt * Spec.pblID) list -> theory -> theory
1.35 + val get_mets: theory -> Meth_Def.mets
1.36 + val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
1.37 + val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
1.38 + val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.39 + val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.40 val get_ref_thy: unit -> theory
1.41 val set_ref_thy: theory -> unit
1.42 end;
1.43 @@ -103,14 +103,14 @@
1.44 type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
1.45 val empty = [];
1.46 val extend = I;
1.47 - val merge = merge Celem7.cas_eq;
1.48 + val merge = merge CAS_Def.cas_eq;
1.49 );
1.50 fun get_cas thy = Data.get thy
1.51 - fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
1.52 + fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
1.53
1.54 structure Data = Theory_Data (
1.55 - type T = Celem5.ptyps;
1.56 - val empty = [Celem5.e_Ptyp];
1.57 + type T = Probl_Def.ptyps;
1.58 + val empty = [Probl_Def.e_Ptyp];
1.59 val extend = I;
1.60 val merge = Store.merge_ptyps;
1.61 );
1.62 @@ -118,39 +118,39 @@
1.63 fun add_pbts pbts thy = let
1.64 fun add_pbt (pbt as {guh,...}, pblID) =
1.65 (* the pblID has the leaf-element as first; better readability achieved *)
1.66 - (if (!Check_Unique.check_guhs_unique) then Celem5.check_pblguh_unique guh (Data.get thy) else ();
1.67 + (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_pblguh_unique guh (Data.get thy) else ();
1.68 rev pblID |> Store.insrt pblID pbt);
1.69 in Data.map (fold add_pbt pbts) thy end;
1.70
1.71 structure Data = Theory_Data (
1.72 - type T = Celem6.mets;
1.73 - val empty = [Celem6.e_Mets];
1.74 + type T = Meth_Def.mets;
1.75 + val empty = [Meth_Def.e_Mets];
1.76 val extend = I;
1.77 val merge = Store.merge_ptyps;
1.78 );
1.79 val get_mets = Data.get;
1.80 fun add_mets mets thy = let
1.81 fun add_met (met as {guh,...}, metID) =
1.82 - (if (!Check_Unique.check_guhs_unique) then Celem6.check_metguh_unique guh (Data.get thy) else ();
1.83 + (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_metguh_unique guh (Data.get thy) else ();
1.84 Store.insrt metID met metID);
1.85 in Data.map (fold add_met mets) thy end;
1.86
1.87 structure Data = Theory_Data (
1.88 - type T = (Celem8.thydata Store.ptyp) list;
1.89 + type T = (Thy_Html.thydata Store.ptyp) list;
1.90 val empty = [];
1.91 val extend = I;
1.92 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
1.93 );
1.94 fun get_thes thy = Data.get thy
1.95 fun add_thes thes thy = let
1.96 - fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
1.97 + fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata
1.98 in Data.map (fold add_the thes) thy end;
1.99 fun insert_fillpats fis thy =
1.100 let
1.101 fun update_elem (theID, fillpats) =
1.102 let
1.103 val hthm = Store.get_py (Data.get thy) theID theID
1.104 - val hthm' = Celem8.update_hthm hthm fillpats
1.105 + val hthm' = Thy_Html.update_hthm hthm fillpats
1.106 handle ERROR _ =>
1.107 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.108 in Store.update_ptyps theID theID hthm' end
1.109 @@ -209,11 +209,11 @@
1.110 section \<open>determine sequence of main parts in thehier\<close>
1.111 setup \<open>
1.112 KEStore_Elems.add_thes
1.113 - [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
1.114 + [(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacKnowledge"], html = "",
1.115 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
1.116 - (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
1.117 + (Thy_Html.Html {guh = Thy_Html.part2guh ["Isabelle"], html = "",
1.118 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
1.119 - (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
1.120 + (Thy_Html.Html {guh = Thy_Html.part2guh ["IsacScripts"], html = "",
1.121 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
1.122 \<close>
1.123
1.124 @@ -233,7 +233,7 @@
1.125 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
1.126
1.127 (* we avoid term_to_string''' defined later *)
1.128 -fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
1.129 +fun check_kestore_cas ((t, (s, _)) : CAS_Def.cas_elem) =
1.130 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
1.131 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
1.132
1.133 @@ -242,25 +242,25 @@
1.134 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.135 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.136 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
1.137 -val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
1.138 +val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.pbts2str;
1.139 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.140 -fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
1.141 +fun pbt_ord ({guh = guh'1, ...} : Probl_Def.pbt, {guh = guh'2, ...} : Probl_Def.pbt) = string_ord (guh'1, guh'2);
1.142 fun sort_kestore_ptyp' _ [] = []
1.143 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
1.144 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.145 :: sort_kestore_ptyp' ordfun ps');
1.146 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.147
1.148 -fun metguh2str ({guh,...} : Celem6.met) = guh : string;
1.149 -fun check_kestore_met (mp: Celem6.met Store.ptyp) =
1.150 +fun metguh2str ({guh,...} : Meth_Def.met) = guh : string;
1.151 +fun check_kestore_met (mp: Meth_Def.met Store.ptyp) =
1.152 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.153 -fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
1.154 +fun met_ord ({guh = guh'1, ...} : Meth_Def.met, {guh = guh'2, ...} : Meth_Def.met) = string_ord (guh'1, guh'2);
1.155 val sort_kestore_met = sort_kestore_ptyp' met_ord;
1.156
1.157 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
1.158 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
1.159 fun write_thes thydata_list =
1.160 thydata_list
1.161 - |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))
1.162 + |> map (fn (id, the) => (Thy_Html.theID2str id, Thy_Html.the2str the))
1.163 |> map pair2str
1.164 |> map writeln
1.165 \<close>