ad 967c8a1eb6b1: preparations for step 6 (i.e. switch ptyps to Theory_Data)
4 ML_file "~~/src/Tools/isac/library.sml"
5 ML_file "~~/src/Tools/isac/calcelems.sml"
7 section {* Knowledge elements for problems and methods *}
9 (* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
10 In the front-end Knowledge comprises theories, problems and methods.
11 Elements of problems and methods are defined in theories alongside
12 the development of respective language elements.
13 However, the structure of methods and problems is independent from theories'
14 deductive structure. Thus respective structures are built in Build_Thydata.thy.
16 Most elements of problems and methods are implemented in "Knowledge/", but some
17 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
18 location in the directory structure.
20 signature KESTORE_ELEMS =
22 val get_rlss: theory -> (rls' * (theory' * rls)) list
23 val add_rlss: (rls' * (theory' * rls)) list -> theory -> theory
24 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list
25 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory
26 val get_cas: theory -> cas_elem list
27 val add_cas: cas_elem list -> theory -> theory
28 val get_ptyps: theory -> ptyps
29 val store_pbts: (pbt * pblID) list -> theory -> theory
33 structure KEStore_Elems: KESTORE_ELEMS =
35 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
37 structure Data = Theory_Data (
38 type T = (rls' * (theory' * rls)) list;
41 val merge = merge_rlss;
43 fun get_rlss thy = Data.get thy
44 fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)
46 structure Data = Theory_Data (
47 type T = (prog_calcID * (calID * eval_fn)) list;
50 val merge = merge calc_eq;
52 fun get_calcs thy = Data.get thy
53 fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)
55 structure Data = Theory_Data (
56 type T = (term * (spec * (term list -> (term * term list) list))) list;
59 val merge = merge cas_eq;
61 fun get_cas thy = Data.get thy
62 fun add_cas cas = Data.map (union_overwrite cas_eq cas)
64 structure Data = Theory_Data (
68 val merge = merge_ptyps;
70 fun get_ptyps thy = Data.get thy;
71 fun store_pbts pbts = let
72 fun store_pbts' (pbt, pblID) = ((*map writeln pblID;*) rev pblID |> insrt pblID pbt)
73 in fold store_pbts' pbts |> Data.map end;
79 section {* Re-use existing access functions for knowledge elements *}
81 The independence of problems' and methods' structure enforces the accesse
82 functions to use "Isac", the final theory which comprises all knowledge defined.
85 (* in this phase of removing Unsynchornized.ref we do NOT overwrite the existing function! *)
86 fun assoc_rls (rls' : rls') = (*SWITCH outcommented*)
87 case AList.lookup (op =) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) rls' of
89 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
90 "TODO exception hierarchy needs to be established.")
92 fun assoc_rls' thy (rls' : rls') = (*SWITCH outcommented*)
93 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
95 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
96 "TODO exception hierarchy needs to be established.")
98 fun assoc_calc thy calID = let
100 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
101 | ass ((calc, (keyi, _)) :: pairs, key) =
102 if key = keyi then calc else ass (pairs, key);
103 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
105 fun assoc_calc' thy key = let
107 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
108 | ass ((all as (keyi, _)) :: pairs, key') =
109 if key' = keyi then all else ass (pairs, key');
110 in ass (KEStore_Elems.get_calcs thy, key) end;
112 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
114 fun get_ptyps () = ! ptyps (*KEStore_Elems.get_ptyps @{theory}*);
116 setup {* KEStore_Elems.add_rlss
117 [("e_rls", (Context.theory_name @{theory}, e_rls)),
118 ("e_rrls", (Context.theory_name @{theory}, e_rrls))] *}
120 section {* Functions for checking KEStore_Elems *}
122 fun short_string_of_rls Erls = "Erls"
123 | short_string_of_rls (Rls {calc, rules, ...}) =
124 "Rls {#calc = " ^ string_of_int (length calc) ^
125 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
126 | short_string_of_rls (Seq {calc, rules, ...}) =
127 "Seq {#calc = " ^ string_of_int (length calc) ^
128 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
129 | short_string_of_rls (Rrls _) = "Rrls {...}";
131 fun check_kestore_rls (rls', (thyID, rls)) =
132 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
134 fun check_kestore_calc ((id, (c, _)) : calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
136 fun check_kestore_cas ((t, (s, _)):cas_elem) =
137 "(" ^ (term_to_string''' @{theory} t) ^ ", " ^ (spec2str s) ^ ")";
139 fun count_kestore_ptyps [] = 0
140 | count_kestore_ptyps ((Ptyp (_, _, ps)) :: ps') =
141 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
142 fun check_kestore_ptyp ((Ptyp (key, pbts, pts)):pbt ptyp) = "Ptyp (" ^ (quote key) ^ ", " ^
143 (pbts2str pbts) ^ ", " ^ (map check_kestore_ptyp pts |> list2str) ^ ")" |> linefeed;
144 fun ptyp_ord ((Ptyp (s1, _, _)), (Ptyp (s2, _, _))) = string_ord (s1, s2);
145 fun pbt_ord ({guh = guh'1, ...} : pbt, {guh = guh'2, ...} : pbt) = string_ord (guh'1, guh'2);
146 fun sort_kestore_ptyp [] = []
147 | sort_kestore_ptyp ((Ptyp (key, pbts, ps)) :: ps') =
148 ((Ptyp (key, sort pbt_ord pbts, sort_kestore_ptyp ps |> sort ptyp_ord))
149 :: sort_kestore_ptyp ps');