(* Title:  BaseDefinitions/kestore.sml

   Author: Walther Neuper

   Use is subject to license terms.

theory Test_Some

  imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"

*)

"-----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------";

"-----------------------------------------------------------------------------";

"-------- fun check_kestore_rls ----------------------------------------------";

"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";

"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";

"-----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------";

"-------- fun check_kestore_rls ----------------------------------------------";

"-------- fun check_kestore_rls ----------------------------------------------";

"-------- fun check_kestore_rls ----------------------------------------------";

if check_kestore_rls ("empty", ("Know_Store", Rule_Set.empty)) = 

  "(empty, (Know_Store, Rls {#calc = 0, #rules = 0, ...))"

then () else error "check_kestore_rls changed"

;

Test_KEStore_Elems.get_rlss @{theory Isac_Knowledge}

  |> map check_kestore_rls 

  |> enumerate_strings

  |> sort string_ord

(*|> map writeln*)

;

"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";

"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";

"-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";

  fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;

  fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)

val data1 = [("test", ("theory-1", Rule_Set.Empty)),

  ("test_rls", ("theory-1", 

    Rule_Set.append_rules "test_rls" Rule_Set.empty [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]

val data2 = 

  [("test_rls", ("theory-2",

    Rule_Set.append_rules "test_rls" Rule_Set.empty [Thm ("not_def", @{thm not_def})]))]

val data_3a = union rls_eq data1 data2

val data_3b = union_overwrite rls_eq data1 data2

val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3a "test_rls";

case rules of

  [Thm ("not_def", _)] => ()

| _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"

;

val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3b "test_rls";

case rules of

  [Thm ("refl", _), Thm ("subst", _)] => ()

| _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"

(* add_rlss will take union_overwrite due to argument sequence *)

"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";

"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";

"-------- ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------";

"~~~~~ fun prep_rls' , args:"; val (thy, (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, rules, errpatts, ...})) =

  (@{theory}, Poly_erls);

(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)

        val sc = 

 Auto_Prog.rules2scr_Rls thy rules;

"~~~~~ fun rules2scr_Rls , args:"; val (thy, rules) = (thy, rules);

    (*if*) Auto_Prog.contain_bdv rules (*else*);

(*+*)val t = Auto_Prog.rule2stac thy (nth 14 rules);

(*+*)UnparseC.term_in_thy @{theory} t;

(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)

 Auto_Prog.rule2stac thy (nth 17 rules);

"~~~~~ fun rule2stac , args:"; val (thy, (Rule.Eval (c, _))) = (thy, (nth 17 rules));

(*+*)val Rule.Eval ("Prog_Expr.is_num", _) = nth 17 rules;

(*+*)c = "Prog_Expr.is_num";                                   (* <<<<<------------ is NOT found *)

(*ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly*)

val "is_num" =

           assoc_calc thy c;

"~~~~~ fun assoc_calc , args:"; val (thy, calID) = (thy, c);

val calcs = 

       KEStore_Elems.get_calcs thy;

(*+*)val ("is_polyrat_in", ("Poly.is_polyrat_in", _)) = nth 17 calcs; (* <<<<<------- is_atom <> is_num *)

(*+*)map fst calcs = (*..WITH declare [[ML_print_depth = 999]]*)

   ["Test.precond_rootmet", "contains_root", "Test.precond_rootpbl", "is_f_x", "primed", "is_normSqrtTerm_in", "is_rootTerm_in", "SQRT", "is_sqrtTerm_in", "is_ratequation_in", "is_rootRatAddTerm_in", "add_new_c",

    "occur_exactly_in", "is_addUnordered", "is_polyexp", "is_poly_in", "is_polyrat_in", "POWER", "TIMES", "PLUS", "ident", "le", "is_atom", "occurs_in", "is_num", "matchsub", "Vars", "lhs", "rhs", "matches",

    "some_occur_in", "is_even", "leq", "equal", "MINUS", "DIVIDE", "boollist2sum", "is_expanded_in", "has_degree_in", "is_multUnordered", "is_expanded"];

(*+*)map (fst o snd) calcs = (*..WITH declare [[ML_print_depth = 999]]*)

   ["Test.precond_rootmet", "Test.contains_root", "Test.precond_rootpbl", "Integrate.is_f_x", "Diff.primed", "RootEq.is_normSqrtTerm_in", "RootEq.is_rootTerm_in", "NthRoot.sqrt", "RootEq.is_sqrtTerm_in",

    "RatEq.is_ratequation_in", "RootRatEq.is_rootRatAddTerm_in", "Integrate.add_new_c", "EqSystem.occur_exactly_in", "Poly.is_addUnordered", "Poly.is_polyexp", "Poly.is_poly_in", "Poly.is_polyrat_in",

    \<^const_name>\<open>realpow\<close>, "Groups.times_class.times", "Groups.plus_class.plus", "Prog_Expr.ident", "Orderings.ord_class.less", "Prog_Expr.is_atom", "Prog_Expr.occurs_in", "Prog_Expr.is_num", "Prog_Expr.matchsub",

    "Prog_Expr.Vars", "Prog_Expr.lhs", "Prog_Expr.rhs", "Prog_Expr.matches", "Prog_Expr.some_occur_in", "Prog_Expr.is_even", "Orderings.ord_class.less_eq", "HOL.eq", "Groups.minus_class.minus",

    "Rings.divide_class.divide", "Prog_Expr.boollist2sum", "Poly.is_expanded_in", "Poly.has_degree_in", "Poly.is_multUnordered", "Rational.is_expanded"];