1.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 19:20:05 2020 +0200
1.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Sat Apr 04 12:11:32 2020 +0200
1.3 @@ -8,8 +8,8 @@
1.4 ML_file libraryC.sml
1.5 ML_file "rule-def.sml"
1.6 ML_file rule.sml
1.7 +ML_file "rule-set.sml"
1.8 ML_file calcelems.sml
1.9 -
1.10 ML \<open>
1.11 \<close> ML \<open>
1.12 \<close> ML \<open>
1.13 @@ -31,10 +31,10 @@
1.14 *)
1.15 signature KESTORE_ELEMS =
1.16 sig
1.17 - val get_rlss: theory -> (Rule.rls' * (Rule.theory' * Rule.rls)) list
1.18 - val add_rlss: (Rule.rls' * (Rule.theory' * Rule.rls)) list -> theory -> theory
1.19 - val get_calcs: theory -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
1.20 - val add_calcs: (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
1.21 + val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list
1.22 + val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list -> theory -> theory
1.23 + val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
1.24 + val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
1.25 val get_cas: theory -> Celem.cas_elem list
1.26 val add_cas: Celem.cas_elem list -> theory -> theory
1.27 val get_ptyps: theory -> Celem.ptyps
1.28 @@ -53,22 +53,22 @@
1.29 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
1.30
1.31 structure Data = Theory_Data (
1.32 - type T = (Rule.rls' * (Rule.theory' * Rule.rls)) list;
1.33 + type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list;
1.34 val empty = [];
1.35 val extend = I;
1.36 - val merge = Celem.merge_rlss;
1.37 + val merge = Rule_Set.merge_rlss;
1.38 );
1.39 fun get_rlss thy = Data.get thy
1.40 - fun add_rlss rlss = Data.map (union_overwrite Celem.rls_eq rlss)
1.41 + fun add_rlss rlss = Data.map (union_overwrite Rule_Set.rls_eq rlss)
1.42
1.43 structure Data = Theory_Data (
1.44 - type T = (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
1.45 + type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
1.46 val empty = [];
1.47 val extend = I;
1.48 - val merge = merge Rule.calc_eq;
1.49 + val merge = merge Rule_Set.calc_eq;
1.50 );
1.51 fun get_calcs thy = Data.get thy
1.52 - fun add_calcs calcs = Data.map (union_overwrite Rule.calc_eq calcs)
1.53 + fun add_calcs calcs = Data.map (union_overwrite Rule_Set.calc_eq calcs)
1.54
1.55 structure Data = Theory_Data (
1.56 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
1.57 @@ -141,13 +141,13 @@
1.58 ML \<open>
1.59 val get_ref_thy = KEStore_Elems.get_ref_thy;
1.60
1.61 -fun assoc_rls (rls' : Rule.rls') =
1.62 +fun assoc_rls (rls' : Rule_Set.rls') =
1.63 case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) rls' of
1.64 SOME (_, rls) => rls
1.65 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
1.66 "TODO exception hierarchy needs to be established.")
1.67
1.68 -fun assoc_rls' thy (rls' : Rule.rls') =
1.69 +fun assoc_rls' thy (rls' : Rule_Set.rls') =
1.70 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
1.71 SOME (_, rls) => rls
1.72 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
1.73 @@ -174,8 +174,8 @@
1.74 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
1.75 \<close>
1.76 setup \<open>KEStore_Elems.add_rlss
1.77 - [("e_rls", (Context.theory_name @{theory}, Rule.e_rls)),
1.78 - ("e_rrls", (Context.theory_name @{theory}, Rule.e_rrls))]\<close>
1.79 + [("e_rls", (Context.theory_name @{theory}, Rule_Set.e_rls)),
1.80 + ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
1.81
1.82 section \<open>determine sequence of main parts in thehier\<close>
1.83 setup \<open>
1.84 @@ -190,18 +190,18 @@
1.85
1.86 section \<open>Functions for checking KEStore_Elems\<close>
1.87 ML \<open>
1.88 -fun short_string_of_rls Rule.Erls = "Erls"
1.89 - | short_string_of_rls (Rule.Rls {calc, rules, ...}) =
1.90 +fun short_string_of_rls Rule_Set.Erls = "Erls"
1.91 + | short_string_of_rls (Rule_Set.Rls {calc, rules, ...}) =
1.92 "Rls {#calc = " ^ string_of_int (length calc) ^
1.93 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
1.94 - | short_string_of_rls (Rule.Seq {calc, rules, ...}) =
1.95 + | short_string_of_rls (Rule_Set.Seq {calc, rules, ...}) =
1.96 "Seq {#calc = " ^ string_of_int (length calc) ^
1.97 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
1.98 - | short_string_of_rls (Rule.Rrls _) = "Rrls {...}";
1.99 + | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
1.100 fun check_kestore_rls (rls', (thyID, rls)) =
1.101 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
1.102
1.103 -fun check_kestore_calc ((id, (c, _)) : Rule.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
1.104 +fun check_kestore_calc ((id, (c, _)) : Rule_Set.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
1.105
1.106 (* we avoid term_to_string''' defined later *)
1.107 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =