diff -r 2c2fdf9dd52d -r e794e1fbe6da src/Tools/isac/BaseDefinitions/Know_Store.thy --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 15:37:39 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 15:51:31 2020 +0200 @@ -35,7 +35,6 @@ ML_file "celem-8.sml" (*thydata*) ML_file "celem-91.sml" (*check_guhs_unique*) -ML_file calcelems.sml ML_file tracing.sml ML \ \ ML \ @@ -62,15 +61,15 @@ val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory - val get_cas: theory -> Celem.cas_elem list - val add_cas: Celem.cas_elem list -> theory -> theory - val get_ptyps: theory -> Celem.ptyps - val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory - val get_mets: theory -> Celem.mets - val add_mets: (Celem.met * Celem.metID) list -> theory -> theory - val get_thes: theory -> (Celem.thydata Celem1.ptyp) list - val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *) - val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory + val get_cas: theory -> Celem7.cas_elem list + val add_cas: Celem7.cas_elem list -> theory -> theory + val get_ptyps: theory -> Celem5.ptyps + val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory + val get_mets: theory -> Celem6.mets + val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory + val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list + val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *) + val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory val get_ref_thy: unit -> theory val set_ref_thy: theory -> unit end; @@ -98,17 +97,17 @@ fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs) structure Data = Theory_Data ( - type T = (term * (Celem.spec * (term list -> (term * term list) list))) list; + type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list; val empty = []; val extend = I; - val merge = merge Celem.cas_eq; + val merge = merge Celem7.cas_eq; ); fun get_cas thy = Data.get thy - fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas) + fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas) structure Data = Theory_Data ( - type T = Celem.ptyps; - val empty = [Celem.e_Ptyp]; + type T = Celem5.ptyps; + val empty = [Celem5.e_Ptyp]; val extend = I; val merge = Celem1.merge_ptyps; ); @@ -116,39 +115,39 @@ fun add_pbts pbts thy = let fun add_pbt (pbt as {guh,...}, pblID) = (* the pblID has the leaf-element as first; better readability achieved *) - (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else (); + (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else (); rev pblID |> Celem1.insrt pblID pbt); in Data.map (fold add_pbt pbts) thy end; structure Data = Theory_Data ( - type T = Celem.mets; - val empty = [Celem.e_Mets]; + type T = Celem6.mets; + val empty = [Celem6.e_Mets]; val extend = I; val merge = Celem1.merge_ptyps; ); val get_mets = Data.get; fun add_mets mets thy = let fun add_met (met as {guh,...}, metID) = - (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else (); + (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else (); Celem1.insrt metID met metID); in Data.map (fold add_met mets) thy end; structure Data = Theory_Data ( - type T = (Celem.thydata Celem1.ptyp) list; + type T = (Celem8.thydata Celem1.ptyp) list; val empty = []; val extend = I; val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *) ); fun get_thes thy = Data.get thy fun add_thes thes thy = let - fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata + fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata in Data.map (fold add_the thes) thy end; fun insert_fillpats fis thy = let fun update_elem (theID, fillpats) = let val hthm = Celem1.get_py (Data.get thy) theID theID - val hthm' = Celem.update_hthm hthm fillpats + val hthm' = Celem8.update_hthm hthm fillpats handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") in Celem1.update_ptyps theID theID hthm' end @@ -207,11 +206,11 @@ section \determine sequence of main parts in thehier\ setup \ KEStore_Elems.add_thes - [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "", + [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "", mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]), - (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "", + (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "", mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]), - (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "", + (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "", mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])] \ @@ -231,31 +230,31 @@ fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))"; (* we avoid term_to_string''' defined later *) -fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) = +fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) = "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false - (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")"; + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")"; fun count_kestore_ptyps [] = 0 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') = 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; -val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str; +val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str; fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2); -fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2); +fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2); fun sort_kestore_ptyp' _ [] = [] | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') = ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) :: sort_kestore_ptyp' ordfun ps'); val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; -fun metguh2str ({guh,...} : Celem.met) = guh : string; -fun check_kestore_met (mp: Celem.met Celem1.ptyp) = +fun metguh2str ({guh,...} : Celem6.met) = guh : string; +fun check_kestore_met (mp: Celem6.met Celem1.ptyp) = check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; -fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2); +fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2); val sort_kestore_met = sort_kestore_ptyp' met_ord; -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes fun write_thes thydata_list = thydata_list |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))