23 val add_cas: Celem7.cas_elem list -> theory -> theory |
23 val add_cas: Celem7.cas_elem list -> theory -> theory |
24 val get_ptyps: theory -> Celem5.ptyps |
24 val get_ptyps: theory -> Celem5.ptyps |
25 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory |
25 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory |
26 val get_mets: theory -> Celem6.mets |
26 val get_mets: theory -> Celem6.mets |
27 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory |
27 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory |
28 val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list |
28 val get_thes: theory -> (Celem8.thydata Store.ptyp) list |
29 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
29 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
30 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
30 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
31 type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list; |
31 type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list; |
32 val merge = merge Celem7.cas_eq; |
32 val merge = merge Celem7.cas_eq; |
33 fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas) |
33 fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas) |
34 type T = Celem5.ptyps; |
34 type T = Celem5.ptyps; |
35 val empty = [Celem5.e_Ptyp]; |
35 val empty = [Celem5.e_Ptyp]; |
36 val merge = Celem1.merge_ptyps; |
36 val merge = Store.merge_ptyps; |
37 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else (); |
37 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else (); |
38 rev pblID |> Celem1.insrt pblID pbt); |
38 rev pblID |> Store.insrt pblID pbt); |
39 type T = Celem6.mets; |
39 type T = Celem6.mets; |
40 val empty = [Celem6.e_Mets]; |
40 val empty = [Celem6.e_Mets]; |
41 val merge = Celem1.merge_ptyps; |
41 val merge = Store.merge_ptyps; |
42 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else (); |
42 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else (); |
43 Celem1.insrt metID met metID); |
43 Store.insrt metID met metID); |
44 type T = (Celem8.thydata Celem1.ptyp) list; |
44 type T = (Celem8.thydata Store.ptyp) list; |
45 val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *) |
45 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *) |
46 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata |
46 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata |
47 val hthm = Celem1.get_py (Data.get thy) theID theID |
47 val hthm = Store.get_py (Data.get thy) theID theID |
48 val hthm' = Celem8.update_hthm hthm fillpats |
48 val hthm' = Celem8.update_hthm hthm fillpats |
49 in Celem1.update_ptyps theID theID hthm' end |
49 in Store.update_ptyps theID theID hthm' end |
50 [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "", |
50 [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "", |
51 (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "", |
51 (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "", |
52 (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "", |
52 (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "", |
53 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) = |
53 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) = |
54 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")"; |
54 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")"; |
55 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') = |
55 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') = |
56 fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
56 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
57 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
57 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
58 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str; |
58 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str; |
59 fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2); |
59 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2); |
60 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2); |
60 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2); |
61 | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') = |
61 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') = |
62 ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
62 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
63 fun metguh2str ({guh,...} : Celem6.met) = guh : string; |
63 fun metguh2str ({guh,...} : Celem6.met) = guh : string; |
64 fun check_kestore_met (mp: Celem6.met Celem1.ptyp) = |
64 fun check_kestore_met (mp: Celem6.met Store.ptyp) = |
65 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2); |
65 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2); |
66 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes |
66 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes |
67 |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the)) |
67 |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the)) |
68 *) |
68 *) |
69 (*/------- to Celem0 -------\*) |
69 (*/------- to Celem0 -------\*) |