1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Sep 12 17:46:32 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Sep 12 18:02:44 2022 +0200
1.3 @@ -267,14 +267,6 @@
1.4 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
1.5 "\nTODO exception hierarchy needs to be established.")
1.6
1.7 -(*: theory -> string -> Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)* )
1.8 -fun assoc_calc' thy key = let
1.9 - fun ass ([], key') =
1.10 - raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
1.11 - | ass ((all as (keyi, _)) :: pairs, key') =
1.12 - if key' = keyi then all else ass (pairs, key');
1.13 - in ass (KEStore_Elems.get_calcs thy, key) end;
1.14 -( **)
1.15 (*val get_calc: Proof.context -> Eval_Def.prog_id ->
1.16 Eval_Def.prog_id * (Eval_Def.const_id * Eval_Def.ml_fun)*)
1.17 fun get_calc ctxt (id: Eval_Def.prog_id) =
1.18 @@ -284,14 +276,6 @@
1.19 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
1.20 "\nTODO exception hierarchy needs to be established.")
1.21
1.22 -(*: theory -> Eval_Def.const_id -> Eval_Def.prog_id* )
1.23 -fun assoc_calc thy calID = let
1.24 - fun ass ([], key) =
1.25 - raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
1.26 - | ass ((calc, (keyi, _)) :: pairs, key) =
1.27 - if key = keyi then calc else ass (pairs, key);
1.28 - in ass (thy |> KEStore_Elems.get_calcs, calID) end;
1.29 -( **)
1.30 (*val get_calc_prog_id: Proof.context -> Eval_Def.const_id -> Eval_Def.prog_id*)
1.31 fun get_calc_prog_id ctxt (const_id: Eval_Def.const_id) =
1.32 let
1.33 @@ -304,9 +288,6 @@
1.34 if key = const_id then prog_id else assoc (pairs, key);
1.35 in assoc (ctxt |> Proof_Context.theory_of |> KEStore_Elems.get_calcs, const_id) end;
1.36
1.37 -(** )
1.38 -fun assoc_cas thy key = assoc (KEStore_Elems.get_cass thy, key);
1.39 -( **)
1.40 (*val get_cas: Proof.context -> term -> References_Def.T * CAS_Def.generate_fn*)
1.41 fun get_cas ctxt tm =
1.42 case AList.lookup (op =) (KEStore_Elems.get_cass (Proof_Context.theory_of ctxt)) tm of
1.43 @@ -315,10 +296,9 @@
1.44 UnparseC.term_in_thy (get_ref_thy ()) tm ^ "\" missing in theory \"" ^
1.45 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
1.46 "\nTODO exception hierarchy needs to be established.")
1.47 +
1.48 (*for starting an Exmaple by CAS_Cmd*)
1.49 (*val get_cas_global: term -> References_Def.T * CAS_Def.generate_fn*)
1.50 -val get_cas_global = AList.lookup (op =) (KEStore_Elems.get_cass (get_ref_thy ()))
1.51 -
1.52 fun get_cas_global tm =
1.53 let
1.54 val thy = get_ref_thy ()
2.1 --- a/src/Tools/isac/Build_Isac.thy Mon Sep 12 17:46:32 2022 +0200
2.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Sep 12 18:02:44 2022 +0200
2.3 @@ -195,7 +195,7 @@
2.4
2.5 section \<open>State of approaching Isabelle by Isac\<close>
2.6 text \<open>
2.7 - Mathias Lehnfeld gives the following list in his thesis in section
2.8 + Mathias Lehnfeld gives the following list in his thesis in section
2.9 4.2.3 Relation to Ongoing Isabelle Development.
2.10 \<close>
2.11 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
3.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Mon Sep 12 17:46:32 2022 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Mon Sep 12 18:02:44 2022 +0200
3.3 @@ -24,7 +24,7 @@
3.4 srls = Rule_Set.Empty, calc = [], errpatts = [],
3.5 rules = [Rule.Thm ("sym_thm111", @{thm thm111} RS @{thm sym}), Rule.Thm ("o_def", @{thm o_def})],
3.6 scr = Rule.Empty_Prog};
3.7 -\<close> ML \<open>
3.8 +
3.9 val prep_rls' = Auto_Prog.prep_rls @{theory};
3.10 \<close>
3.11
4.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml Mon Sep 12 17:46:32 2022 +0200
4.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml Mon Sep 12 18:02:44 2022 +0200
4.3 @@ -12,7 +12,7 @@
4.4 "-----------------------------------------------------------------------------";
4.5 "-------- fun check_kestore_rls ----------------------------------------------";
4.6 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";
4.7 -"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
4.8 +"-------- ERROR get_calc: 'Prog_Expr.is_num' not found in theory Poly ------";
4.9 "-----------------------------------------------------------------------------";
4.10 "-----------------------------------------------------------------------------";
4.11
4.12 @@ -63,7 +63,7 @@
4.13 "~~~~~ fun prep_rls' , args:"; val (thy, (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, rules, errpatts, ...})) =
4.14 (@{theory}, Poly_erls);
4.15
4.16 -(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)
4.17 +(*ERROR get_calc: 'Prog_Expr.is_num' not found in theory Poly*)
4.18 val sc =
4.19 Auto_Prog.rules2scr_Rls thy rules;
4.20 "~~~~~ fun rules2scr_Rls , args:"; val (thy, rules) = (thy, rules);
4.21 @@ -72,14 +72,14 @@
4.22 (*+*)val t = Auto_Prog.rule2stac thy (nth 14 rules);
4.23 (*+*)UnparseC.term_in_thy @{theory} t;
4.24
4.25 -(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)
4.26 +(*ERROR get_calc: 'Prog_Expr.is_num' not found in theory Poly*)
4.27 Auto_Prog.rule2stac thy (nth 17 rules);
4.28 "~~~~~ fun rule2stac , args:"; val (thy, (Rule.Eval (c, _))) = (thy, (nth 17 rules));
4.29
4.30 (*+* )val Eval ("Prog_Expr.is_num", _) = nth 17 rules( *+*);
4.31 (*+*)c = "Prog_Expr.is_num"; (* <<<<<------------ is NOT found *)
4.32
4.33 -(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)
4.34 +(*ERROR get_calc: 'Prog_Expr.is_num' not found in theory Poly*)
4.35 (*+* )get_calc (Proof_Context.init_global thy) c( *+*);
4.36 "~~~~~ fun get_calc , args:"; val (thy, calID) = ( thy, c);
4.37 val calcs =